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

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



Hi Smruti,

glad that you found my answer helpful. My replies are below.

On 16 Nov 2020, at 20:38, Smruti Padhy <smruti.padhy@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 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? 

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

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,

Stephan


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


--
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/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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3E5BF84F-15DC-4087-B7D6-AC914F980EBC%40gmail.com.