Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS

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 inequality

num_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 is

num_of_items_consumed + Len(buffer) <= num_of_items_produced

Yes, while checking my previous SafetyProperty, TLC gave me an invariant violation error with a counter example. After some thought, I corrected my inductive invariant to

SafetyProperty == 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?

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)-1

Thank 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.

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?

I 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,
Stephan

P.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. -s

Thanks for the clarification.

Best,

Smruti

ps: 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

------------------------- MODULE producer_consumer -------------------------

EXTENDS Naturals, Sequences, SequenceTheorems, TLAPS

CONSTANTS MaxTotalNumberOfItemsProduced, (* max number of items that can be produced by a producer *)

MaxBufferLen (* max buffer capacity for produced items *)

ASSUME Assumption ==

/\ MaxTotalNumberOfItemsProduced \in Nat

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

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

VARIABLES buffer, num_of_items_produced, num_of_items_consumed

vars == <<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 ------- *)

THEOREM Spec => []IInv

<1>1. Init => IInv

BY Assumption DEF Init, IInv, TypeInvariant, SafetyProperty

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

<2> SUFFICES ASSUME IInv,

[Next]_vars

PROVE IInv'

OBVIOUS

<2>. USE Assumption DEF IInv, TypeInvariant, SafetyProperty

<2>1. ASSUME NEW item \in Item,

Produce(item)

PROVE IInv'

BY <2>1, Assumption DEF Produce

<2>2. CASE Consume

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

BY <2>2, HeadTailProperties DEF Consume

<3>. QED BY <2>2 DEF Consume

<2>3. CASE UNCHANGED vars

BY <2>3 DEF vars

<2>4. QED

BY <2>1, <2>2, <2>3 DEF Next

<1>. QED BY <1>1, <1>2, PTL DEF Spec

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

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

THEOREM Spec => []IInv

<1>1. Init => IInv

BY Assumption DEF Init, IInv, TypeInvariant, SafetyProperty

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

<2> SUFFICES ASSUME IInv,

[Next]_vars

PROVE IInv'

OBVIOUS

<2>. USE Assumption DEF IInv, TypeInvariant, SafetyProperty

<2>1. ASSUME NEW item \in Item,

Produce(item)

PROVE IInv'

BY <2>1, Assumption DEF Produce

<2>2. CASE Consume

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

BY <2>2 DEF Consume

<3>. QED BY <2>2 DEF Consume

<2>3. CASE UNCHANGED vars

BY <2>3 DEF vars

<2>4. QED

BY <2>1, <2>2, <2>3 DEF Next

<1>. QED BY <1>1, <1>2, PTL DEF Spec

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

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

LEMMA TypeCorrect == Init => IInv

<1> SUFFICES ASSUME Init

PROVE IInv

OBVIOUS

<1>1. TypeInvariant

BY Assumption DEF Init, IInv, TypeInvariant

<1>2. SafetyProperty

BY DEF Init, IInv, SafetyProperty

<1>3. QED

BY <1>1, <1>2 DEF IInv

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

LEMMA SecondStep== IInv /\[Next]_vars => IInv'

<1> SUFFICES ASSUME IInv,

[Next]_vars

PROVE IInv'

OBVIOUS

<1>1. CASE Next

<2>. USE Assumption DEF IInv, TypeInvariant, SafetyProperty

<2>1. ASSUME NEW item \in Item,

Produce(item)

PROVE IInv'

BY <2>1, Assumption DEF Produce

<2>2. CASE Consume

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

BY <2>2 DEF Consume

<3>. QED BY <2>2 DEF Consume

<2>3. QED

BY <1>1, <2>1, <2>2 DEF Next

<1>2. CASE UNCHANGED vars

BY Assumption, <1>2 DEF vars, IInv, TypeInvariant, SafetyProperty

<1>3. QED

BY <1>1, <1>2

THEOREM Spec =>[]IInv

BY TypeCorrect, SecondStep, PTL DEF Spec

(* ----- 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'*)

THEOREM Spec => []IInv

<1>1. Init => IInv

BY Assumption DEF Init, IInv, TypeInvariant, SafetyProperty

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

<2> SUFFICES ASSUME IInv, [Next]_vars

PROVE IInv'

OBVIOUS

<2>1. TypeInvariant'

<3>1. ASSUME NEW item \in Item,

Produce(item)

PROVE TypeInvariant'

BY <3>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty

<3>2. CASE Consume

BY <3>2, Assumption DEF Consume, IInv, TypeInvariant, SafetyProperty

<3>3. CASE UNCHANGED vars

BY Assumption, <3>3 DEF vars, IInv, TypeInvariant, SafetyProperty

<3>4. QED

BY <3>1, <3>2, <3>3 DEF Next

<2>2. SafetyProperty'

<3>1. ASSUME NEW item \in Item,

Produce(item)

PROVE SafetyProperty'

BY <3>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty

<3>2. CASE Consume

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

BY <3>2 DEF Consume, IInv, TypeInvariant, SafetyProperty

<4>. QED BY <3>2 DEF Consume, IInv, TypeInvariant, SafetyProperty

<3>3. CASE UNCHANGED vars

BY Assumption, <3>3 DEF vars, IInv, TypeInvariant, SafetyProperty

<3>4. QED

BY <3>1, <3>2, <3>3 DEF Next

<2>3. QED

BY <2>1, <2>2 DEF IInv

<1>. QED BY <1>1, <1>2, PTL DEF Spec

(* ---- 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*)

THEOREM Spec => []IInv

<1>1. Init => IInv

BY Assumption DEF Init, IInv, TypeInvariant, SafetyProperty

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

<2> SUFFICES ASSUME IInv, [Next]_vars

PROVE IInv'

OBVIOUS

<2>1. TypeInvariant'

<3>1. ASSUME NEW item \in Item,

Produce(item)

PROVE TypeInvariant'

BY <3>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty

<3>2. CASE Consume

BY <3>2, Assumption DEF Consume, IInv, TypeInvariant, SafetyProperty

<3>3. CASE UNCHANGED vars

BY Assumption, <3>3 DEF vars, IInv, TypeInvariant, SafetyProperty

<3>4. QED

BY <3>1, <3>2, <3>3 DEF Next

<2>2. SafetyProperty'

<3>1. ASSUME NEW item \in Item,

Produce(item)

PROVE SafetyProperty'

BY <3>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty

<3>2. CASE Consume

<4>1. ASSUME NEW item \in Item,

Produce(item)

PROVE SafetyProperty'

BY <4>1, Assumption DEF Produce, IInv, TypeInvariant, SafetyProperty

<4>2. CASE Consume

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

BY <3>2, Assumption DEF Consume, IInv, TypeInvariant, SafetyProperty

<5>. QED BY <4>2 DEF Consume, IInv, TypeInvariant, SafetyProperty

<4>3. CASE UNCHANGED vars

BY <4>3 DEF vars, IInv, TypeInvariant, SafetyProperty

<4>4. QED

BY <4>1, <4>2, <4>3 DEF Next

<3>3. CASE UNCHANGED vars

BY Assumption, <3>3 DEF vars, IInv, TypeInvariant, SafetyProperty

<3>4. QED

BY <3>1, <3>2, <3>3 DEF Next

<2>3. QED

BY <2>1, <2>2 DEF IInv

<1>. QED BY <1>1, <1>2, PTL DEF Spec

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

\* 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