[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Smruti Padhy <smruti.padhy@xxxxxxxxx>*Date*: Mon, 23 Nov 2020 21:54:24 -0800 (PST)*References*: <09339bc6-eea4-4480-a6ee-75567f92bb4an@googlegroups.com> <58556ffe-17ae-81f0-6c06-9261d4a85225@lemmster.de> <7039e237-bf47-4c72-9941-6edd25188ee8n@googlegroups.com> <a9b78c6b-b5ae-a8af-f281-d95cfd586c1f@lemmster.de> <14047959-eaa6-4691-995d-4d6aa27cbec5n@googlegroups.com> <9BDED377-1BA4-4A2F-944B-E58D3D2D1A26@gmail.com> <13d52375-2f27-4120-831e-867de5fae8a1n@googlegroups.com> <3E5BF84F-15DC-4087-B7D6-AC914F980EBC@gmail.com> <2c130114-1919-4a45-abf9-4690252a34e6n@googlegroups.com> <4A8D7376-BC4E-470D-9D3B-B11E5136268F@gmail.com>

Thank you so much Stephan. It really helped me.

On Thursday, November 19, 2020 at 11:35:49 AM UTC-6 Stephan Merz wrote:

When you write "BY DEF IInv", the prover replaces the predicate IInv by the conjunction "TypeInvariant /\ SafetyProperty". If you need to expand these predicates as well (and you do in your proof), write "BY DEF IInv, TypeInvariant, SafetyProperty". You can easily test this by launching the prover with only IInv expanded. When the proof fails, the window with the failed proof obligation displays exactly the TLA+ formula that is sent to the back-end provers.In the future, we may enable some expansions of definitions to happen automatically to avoid the tedium of having to indicate exactly which definitions should be used. But for now, the prover will only expand definitions of the operators that you indicate explicitly, except for built-in operators such as logical connectives and elementary arithmetic. (You can write "USE DEF ..." so that certain operators are always expanded from the USE step up to the end of the scope in which the USE directive occurs.)Regards,StephanOn 19 Nov 2020, at 18:22, Smruti Padhy <smruti...@xxxxxxxxx> wrote:Hi Stephan,Thank you so much for all the explanations. One more question - in some of the proofs, it is required to use DEF IInv, TypeInvariant, SafetyProperty. But IInv == TypeInvariant /\ SafetyProperty. By using DEF IInv only should be enough wherever we need assertion to be proved using TypeInvariant or SafetyProperty. I think I am not sure how TLAPS backend expands the definition, handles the duplications of the predicates, and uses it to prove assertions.Best,SmrutiOn Tuesday, November 17, 2020 at 1:32:02 AM UTC-6 Stephan Merz wrote:Hi Smruti,glad that you found my answer helpful. My replies are below.On 16 Nov 2020, at 20:38, Smruti Padhy <smruti...@xxxxxxxxx> wrote:Hi Stephan,Thank you so much for the detailed reply. It actually helped me a lot with the understanding of the proof. I have some follow up questions as well. I have added me comments and questions in-line with your reply message below:On Saturday, November 14, 2020 at 5:32:39 AM UTC-6 Stephan Merz wrote:Hello,apologies for the late reply – I tried to reconstruct your spec from what you pasted in the message but it may be a bit out of sync with the spec you are actually working on.Yes, I have attached the latest spec with the proofs.The first issue that I noticed was that your invariant mentions both constants MaxBufferLen and MaxTotalNumberOfItemsProduced but you only have an assumption for the first constant. So I added the conjunct/\ MaxTotalNumberOfItemsProduced \in Nat

to your constant assumption. Also, that assumption must of course be used in the proof but this is not shown in the proof that you reported being able to finish. Note that TLC will not help find you problems involving missing assumptions about constants because constants have fixed values in your model.Thanks for pointing that out. I completely missed that point. I have added that now.The second issue concerns the Consume action: it increments the variable num_of_items_consumed while leaving num_of_items_produced unchanged. Therefore you will not be able to conclude that the inequalitynum_of_items_consumed <= num_of_items_produced(which is your SafetyProperty) is preserved. This should have been discovered when you used TLC to check if your invariant was inductive. A minute of reflection indicates that the invariant that you really need isnum_of_items_consumed + Len(buffer) <= num_of_items_producedYes, while checking my previous SafetyProperty, TLC gave me an invariant violation error with a counter example. After some thought, I corrected my inductive invariant toSafetyProperty == num_of_items_produced = num_of_items_consumed + Len(buffer)

Is there a specific reason to use '<=' instead '=' ?

TLAPS is able to prove the inductive invariant with '='. Also as a system property, it seems num_of_items_consumed + Len(buffer) should always be equal to num_of_items_produced. Am I missing any counterexample?

Just after posting my reply, it occurred to me that I could have written '=' instead of '<=', and of course the version with equality is a stronger and more precise invariant, so it should be preferred. Both imply the original property that you stated.Now we can start the formal proof of the invariant, based on the general schema for invariant proofs. The only non-obvious step is the one that shows that [Next]_vars preserves the invariant, so I used the "decompose proof" command to split it into individual proof steps corresponding to the sub-actions of [Next]_vars. The cases corresponding to Produce and UNCHANGED vars are again simple, leaving us with the Consume action, which unfortunately isn't proved automatically. I now guessed that the prover needed to know that the length of the buffer decreases in this step and therefore asserted<3>. Len(buffer') = Len(buffer)-1Thank you so much. This was the key. I was stuck at trying to proof Consume action. This also clarifies some of the doubts I had.With this knowledge, the prover indeed managed to prove the step corresponding to the Consume action. (I could have split the conclusion IInv' into its individual conjuncts to find out which ones go through and which ones don't, further narrowing down the source of the problem.)For understanding how the TLAPS decompose proof works, I have decomposed the steps of the proof into several ways that TLAPS provides. In the updated spec attached, one can find the different decomposition and its proofs. As you have mentioned, I tried the proof decomposition by splitting IInv' to TypeInvariant' and SafetyProperty' (Proof Decomposition 3 in the spec). It is interesting to observe that TypeInvariant' and SafetyInvariant' could further be decomposed into CASE Produce, CASE Consume, CASE UNCHANGED vars. The step <2>1.<3>2 (CASE Consume) does not require the assert Len(buffer') = Len(buffer)-1 to prove TypeInvariant' while step <2>2.<3><2> requires it to prove SafetyProperty'.In Proof Decomposition 3', I tried to decompose proof for step <2>2.<3><2>, i.e CASE Consume, to proof SafetyProperty' without directly using Len(buffer') = Len(buffer)-1. The TLAPS decomposes it to further to CASE Produce, Consume, UNCHANGED vars. The same proof follows. It was like a cycle if we try to decompose Case Consume, it keeps decomposing it. I am not sure if that is the intended behaviour of TLAPS or some bug that I am seeing.When you use "decompose proof", the interface usually (depending on the shape of the formulas) offers you to work on either the hypotheses or the consequence of an assertion. I believe the reason for the behavior that you observed is that the assumption [Next]_vars is still present among the hypotheses, and since it is a disjunction, it can be decomposed. In contrast, the Consume action is a conjunction, and it doesn't make sense to decompose a conjunction in a hypothesis.For proving the auxiliary level-3 step, I use the lemma HeadTailProperties from the library module SequenceTheorems. (These modules are by default installed in /usr/local/lib/tlaps/, just like TLAPS.tla, it is worth looking at the theorems they provide if you are doing any non-trivial proof. You may also look at the proofs of these lemmas in SequenceTheorems_proofs.tla if you are stuck in some proof about sequences.)Thank you for letting me know about the Library modules. I tried the proof you had in the spec. TLAPS is able to proof auxiliary level-3 step with or without HeadTailProperties. Decomposition 1 in my updated spec (attached) is the exact proof that you had with HeadTailProperties and Decomposition 1' in the updated proof in the latest spec that is exactly the same proof as yours without HeadTailProperties. Am I missing something here?Indeed, the SMT backend knows enough about sequences to understand that the length of the tail is one less than the length of the original sequence, so appealing to lemma HeadTailProperties was not necessary here. Unfortunately, although the backend can prove that assertion when it is presented with it, it is not clever enough to replace Len(buffer') with Len(buffer)-1 on its own, and so the intermediate assertion has to be stated ...Happy proving,StephanI also looked into the proof of HeadTailProperties. I am not sure if I understand it correctly, the proof looks like it is stating the property of a sequence with its operators as the last step of the proof is OBVIOUS.----------------------------------------

THEOREM HeadTailProperties ==

ASSUME NEW S,

NEW s \in Seq(S), s # << >>

PROVE /\ Head(s) \in S

/\ Tail(s) \in Seq(S)

/\ Len(Tail(s)) = Len(s)-1

/\ \A i \in 1 .. Len(Tail(s)) : Tail(s)[i] = s[i+1]

OBVIOUS-----------------The overall module with the full proof is attached.Thank you again for the time and the detailed explanation and proof. It helped me a lot.Hope this helps,StephanP.S.: In a first approximation, you should not have to care about which backend (SMT, Zenon or Isabelle) proves any given step since TLAPS will call all of them. Adding "BY SMT" etc. to a step simply documents which backend succeeds in proving a step and avoids unnecessary calls to the other backends. -sThanks for the clarification.Best,Smrutips: When I attached the spec, I was getting error in posting. Also copying pasting here:. You can find the spec in our github repo: https://github.com/tapis-project/specifications/blob/master/generic-patterns/producer_consumer.tla-------------------------

MODULEproducer_consumer -------------------------

EXTENDSNaturals, Sequences, SequenceTheorems, TLAPS

CONSTANTSMaxTotalNumberOfItemsProduced, (* max number of items that can be produced by a producer *)MaxBufferLen (* max buffer capacity for produced items *)

ASSUMEAssumption ==/\ MaxTotalNumberOfItemsProduced \in Nat

/\ MaxBufferLen \in (Nat \ {0}) (* MaxbufferLen should be atleast 1 *)

-----------------------------------------------------------------------------

VARIABLESbuffer, num_of_items_produced, num_of_items_consumedvars == <<buffer, num_of_items_produced, num_of_items_consumed>>

Item == [type: {"item"}]

-----------------------------------------------------------------------------

(* Temporarl property: Any item that is produced gets eventually consumed *)

AllItemsConsumed == <>[](Len(buffer) = 0 /\ num_of_items_produced = num_of_items_consumed)

(* Type Correctness *)

TypeInvariant == /\ buffer \in Seq(Item)

/\ Len(buffer) \in 0..MaxBufferLen

/\ num_of_items_produced \in 0..MaxTotalNumberOfItemsProduced

/\ num_of_items_consumed \in 0..MaxTotalNumberOfItemsProduced

(* An Invariant: num of items consumed is always less than or equal to the total number of items produced *)

SafetyProperty == num_of_items_produced = num_of_items_consumed + Len(buffer)

------------------------------------------------------------------------------

(* Specification *)

Init == /\ buffer = <<>>

/\ num_of_items_produced = 0

/\ num_of_items_consumed = 0

Produce(item) == /\ Len(buffer) < MaxBufferLen

/\ num_of_items_produced < MaxTotalNumberOfItemsProduced

/\ buffer'= Append(buffer, item)

/\ num_of_items_produced' = num_of_items_produced + 1

/\

UNCHANGED<<num_of_items_consumed >>Consume == /\ Len(buffer) > 0

/\ buffer'= Tail(buffer)

/\ num_of_items_consumed' = num_of_items_consumed + 1

/\

UNCHANGED<<num_of_items_produced>>Next ==

\/ \E item \in Item: Produce(item)

\/ Consume

Spec == Init /\ [][Next]_vars

FairSpec == Spec

/\ WF_vars(\E item \in Item: Produce(item))

/\ WF_vars(Consume)

-------------------------------------------------------------------------------

(* Proof *)

(* ---- Proof structure ---- *)

(* ----

Correct = ... \* The invariant you really want to prove

IInv = ... /\ Correct \* the inductive invariant

THEOREM Spec=>[]Correct

<1>1. Init => IInv

<1>2. IInv /\ [Next]_vars => IInv'

<1>3. IInv => Correct

<1>4. QED

BY <1>1, <1>2, <1>3

------------------------ *)

(*---- Inductive Invariant -------*)

IInv == /\ TypeInvariant

/\ SafetyProperty

(* While checking for the inductive invariant in TLC , Seq operator needs to be redefine as MySeq. *)

MySeq(P) ==

UNION{[1..n -> P] : n \in 0..MaxBufferLen}

(* ---- Dr.Stephen's proof decomposition 1 ------- *)

THEOREMSpec => []IInv<1>1. Init => IInv

BYAssumptionDEFInit, IInv, TypeInvariant, SafetyProperty<1>2. IInv /\ [Next]_vars => IInv'

<2>

SUFFICESASSUMEIInv,[Next]_vars

PROVEIInv'

OBVIOUS<2>.

USEAssumptionDEFIInv, TypeInvariant, SafetyProperty<2>1.

ASSUMENEWitem \in Item,Produce(item)

PROVEIInv'

BY<2>1, AssumptionDEFProduce<2>2.

CASEConsume<3>. Len(buffer') = Len(buffer)-1

BY<2>2, HeadTailPropertiesDEFConsume<3>.

QEDBY<2>2DEFConsume<2>3.

CASEUNCHANGEDvars

BY<2>3DEFvars<2>4.

QED

BY<2>1, <2>2, <2>3DEFNext<1>.

QEDBY<1>1, <1>2, PTLDEFSpec

(*------ Decomposition 1' ------ *)

(* Removed HeadTailProperties from the proof step <3>. in decomposition 1. TLAPS still able o prove it *)

THEOREMSpec => []IInv<1>1. Init => IInv

BYAssumptionDEFInit, IInv, TypeInvariant, SafetyProperty<1>2. IInv /\ [Next]_vars => IInv'

<2>

SUFFICESASSUMEIInv,[Next]_vars

PROVEIInv'

OBVIOUS<2>.

USEAssumptionDEFIInv, TypeInvariant, SafetyProperty<2>1.

ASSUMENEWitem \in Item,Produce(item)

PROVEIInv'

BY<2>1, AssumptionDEFProduce<2>2.

CASEConsume<3>. Len(buffer') = Len(buffer)-1

BY<2>2DEFConsume<3>.

QEDBY<2>2DEFConsume<2>3.

CASEUNCHANGEDvars

BY<2>3DEFvars<2>4.

QED

BY<2>1, <2>2, <2>3DEFNext<1>.

QEDBY<1>1, <1>2, PTLDEFSpec

(* ----- Proof Decomposition 2 ------- *)

(* Separately proved step 1 and step 2 of the proof as LEMMA. Then proved the fonal THEOREM. *)

LEMMATypeCorrect == Init => IInv<1>

SUFFICESASSUMEInit

PROVEIInv

OBVIOUS<1>1. TypeInvariant

BYAssumptionDEFInit, IInv, TypeInvariant<1>2. SafetyProperty

BYDEFInit, IInv, SafetyProperty<1>3.

QED

BY<1>1, <1>2DEFIInv

(* Decompose proof into CASE Next, UNCHANGED vars. CASE Next is further decomposed into Produce, Consume, UNCHANGED *)

LEMMASecondStep== IInv /\[Next]_vars => IInv'<1>

SUFFICESASSUMEIInv,[Next]_vars

PROVEIInv'

OBVIOUS<1>1.

CASENext<2>.

USEAssumptionDEFIInv, TypeInvariant, SafetyProperty<2>1.

ASSUMENEWitem \in Item,Produce(item)

PROVEIInv'

BY<2>1, AssumptionDEFProduce<2>2.

CASEConsume<3>. Len(buffer') = Len(buffer)-1

BY<2>2DEFConsume<3>.

QEDBY<2>2DEFConsume<2>3.

QED

BY<1>1, <2>1, <2>2DEFNext<1>2.

CASEUNCHANGEDvars

BYAssumption, <1>2DEFvars, IInv, TypeInvariant, SafetyProperty<1>3.

QED

BY<1>1, <1>2

THEOREMSpec =>[]IInv

BYTypeCorrect, SecondStep, PTLDEFSpec(* ----- Proof decomposition 3 ------- *)

(* Decomposed proof of <1>2 into individual conjunct of IInv', that is TypeInvariant' and SafetyProperty' *)

(* TypeInvariant' and SafetyInvariant' further decomposed into CASE Produce, CASE Consume, CASE UNCHANGED vars respectively.*)

(* It is interesting to see step <2>1.<3>2 does not require assert Len(buffer') = Len(buffer)-1 to prove TypeInvariant' *)

(* while step <2>2.<3><2> requires it to prove SafetyProperty'*)

THEOREMSpec => []IInv<1>1. Init => IInv

BYAssumptionDEFInit, IInv, TypeInvariant, SafetyProperty<1>2. IInv /\ [Next]_vars => IInv'

<2>

SUFFICESASSUMEIInv, [Next]_vars

PROVEIInv'

OBVIOUS<2>1. TypeInvariant'

<3>1.

ASSUMENEWitem \in Item,Produce(item)

PROVETypeInvariant'

BY<3>1, AssumptionDEFProduce, IInv, TypeInvariant, SafetyProperty<3>2.

CASEConsume

BY<3>2, AssumptionDEFConsume, IInv, TypeInvariant, SafetyProperty<3>3.

CASEUNCHANGEDvars

BYAssumption, <3>3DEFvars, IInv, TypeInvariant, SafetyProperty<3>4.

QED

BY<3>1, <3>2, <3>3DEFNext<2>2. SafetyProperty'

<3>1.

ASSUMENEWitem \in Item,Produce(item)

PROVESafetyProperty'

BY<3>1, AssumptionDEFProduce, IInv, TypeInvariant, SafetyProperty<3>2.

CASEConsume<4>. Len(buffer') = Len(buffer)-1

BY<3>2DEFConsume, IInv, TypeInvariant, SafetyProperty<4>.

QEDBY<3>2DEFConsume, IInv, TypeInvariant, SafetyProperty<3>3.

CASEUNCHANGEDvars

BYAssumption, <3>3DEFvars, IInv, TypeInvariant, SafetyProperty<3>4.

QED

BY<3>1, <3>2, <3>3DEFNext<2>3.

QED

BY<2>1, <2>2DEFIInv<1>.

QEDBY<1>1, <1>2, PTLDEFSpec

(* ---- Proof Decomposition 3' --- Modification to the above proof decomposition 3 *)

(* When tried to decompose proof for the step <2>2.<3><2>, i.e CASE Consume to proof SafetyProperty', it decompose it to further to CASE Produce, Consume, UNCHANGED vars*)

THEOREMSpec => []IInv<1>1. Init => IInv

BYAssumptionDEFInit, IInv, TypeInvariant, SafetyProperty<1>2. IInv /\ [Next]_vars => IInv'

<2>

SUFFICESASSUMEIInv, [Next]_vars

PROVEIInv'

OBVIOUS<2>1. TypeInvariant'

<3>1.

ASSUMENEWitem \in Item,Produce(item)

PROVETypeInvariant'

BY<3>1, AssumptionDEFProduce, IInv, TypeInvariant, SafetyProperty<3>2.

CASEConsume

BY<3>2, AssumptionDEFConsume, IInv, TypeInvariant, SafetyProperty<3>3.

CASEUNCHANGEDvars

BYAssumption, <3>3DEFvars, IInv, TypeInvariant, SafetyProperty<3>4.

QED

BY<3>1, <3>2, <3>3DEFNext<2>2. SafetyProperty'

<3>1.

ASSUMENEWitem \in Item,Produce(item)

PROVESafetyProperty'

BY<3>1, AssumptionDEFProduce, IInv, TypeInvariant, SafetyProperty<3>2.

CASEConsume<4>1.

ASSUMENEWitem \in Item,Produce(item)

PROVESafetyProperty'

BY<4>1, AssumptionDEFProduce, IInv, TypeInvariant, SafetyProperty<4>2.

CASEConsume<5>. Len(buffer') = Len(buffer)-1

BY<3>2, AssumptionDEFConsume, IInv, TypeInvariant, SafetyProperty<5>.

QEDBY<4>2DEFConsume, IInv, TypeInvariant, SafetyProperty<4>3.

CASEUNCHANGEDvars

BY<4>3DEFvars, IInv, TypeInvariant, SafetyProperty<4>4.

QED

BY<4>1, <4>2, <4>3DEFNext<3>3.

CASEUNCHANGEDvars

BYAssumption, <3>3DEFvars, IInv, TypeInvariant, SafetyProperty<3>4.

QED

BY<3>1, <3>2, <3>3DEFNext<2>3.

QED

BY<2>1, <2>2DEFIInv<1>.

QEDBY<1>1, <1>2, PTLDEFSpec

=============================================================================

\* Modification History

\* Last modified Mon Nov 16 12:21:06 CST 2020 by spadhy

\* Created Mon Oct 26 10:27:47 CDT 2020 by spadhy

--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/13d52375-2f27-4120-831e-867de5fae8a1n%40googlegroups.com.

--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2c130114-1919-4a45-abf9-4690252a34e6n%40googlegroups.com.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2641981b-8366-4a13-b3b1-908a5174d4ebn%40googlegroups.com.

**References**:**[tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Markus Kuppe

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Markus Kuppe

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Stephan Merz

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Stephan Merz

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Smruti Padhy

**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Understanding Diameter in TLC** - Next by Date:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Previous by thread:
**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS** - Next by thread:
**[tlaplus] Bizzare TLC error on checking liveness with weak fairness** - Index(es):