TLAPS proof of increment and update

[Smruti Padhy]

Hi,

I have been trying different proofs with TLAPS. In the spec attached in this conversation, I tried a simple example of increment and update of two variables. That is, Increment the first variable at a given time and then update the second variable with the incremented value of the first variable at a different time.

This spec has two variables - valX and valY. valX and valY are represented as a record with two fields: val that can take Natural numbers and ts as timestamp associated with it. We use a global clock for time.

valX is incremented by 1 and valY is updated with the new value of valX. This increment and update pattern is an abstraction that can be used during server/worker zero-downtime updates.

I was able to use TLAPS to prove the safety property of the spec.  But it required two extra enabling conditions in the Inc action for the proof to work:  

      /\ valX.ts <= clock \*<-this is required only for proof

      /\ valY.ts <= clock \*<-this is required only for proof

I am not clear as to why we would need these two conditions. It should follow from the induction hypothesis.

I would appreciate it if someone can provide me some more insights into the workings of the TLAPS proof.   

I have attached the spec with this conversation.  

Best,

Smruti

ps: I am unable to post any attached TLA+ spec to this group in my conversation. so renamed the file with .txt.

[Ayush Pandey]

I am not an expert not even intermediate with TLAPS so I might be completely wrong but I found 2 interesting things in this proof. 

1. You do not need the condition /\ valX.ts <= clock \*<-this is required only for proof  for TLAPS to prove your theorems.
2. Clock is the main culprit of the proof not working properly.

I don't know if I can explain this very well but the obligation that fails in the proof is <2>1. If we perform a symbolic execution of the states, we know that Init => SafetyProperty. This is obvious. Now, in any state other than init, we start with an assumption that safety property holds so, (valX.val > valY.val) => valX.ts >= valY.ts  is true. Now if you apply the operations of the Inc state, clock becomes clock+1 and valX becomes [valX.val+1, clock+1].  Now replace these changes in the safety property which should hold true. We get:

(valX.val+1 > valY.val) => clock+1 >= valY.ts 

With any of the assumptions you started with, it is not possible to prove this. This problem goes away when you add valY.ts <= clock because suddenly the proof assistant has another assumption it can use with the Inc state.

[Ayush Pandey]

My statement regarding the clock might be iffy though. I think its really how the Proof assistant works under the shell that decides how the predicates are handled.

[Stephan Merz]

Hello,

the problem is that your safety property is not an inductive invariant (even with respect to the typing invariant). However, it is easy to see that the time stamps of your variables can never exceed the clock value, and so the extra guard that you added to the Inc action is actually an invariant of your specification. It even happens to be an inductive invariant. 

The attached TLA+ module contains a proof of the safety property. Please see the TLAPS tutorial or other examples in the distribution for the concept and the importance of inductive invariants.

Hope this helps,

Stephan

P.S.: The constant MaxNum is (obviously) unnecessary for the prover – better add a state constraint to the model that you use for TLC instead of adding a spurious precondition in your specification. -s

[Smruti Padhy]

Thank you, Ayush for your reply. 

[Smruti Padhy]

Thank you, Stephan for the detailed proof and for pointing the need for the clock invariant for the safety property proof instead of those conditions as enabling conditions. I will go through examples and tutorials again as it seems I might be missing some basic concepts.

Regarding MaxNum, I added it to limit the number of Inc actions and in turn, limit the number of states during TLC model checking. I couldn't think of a better way to do that. I agree that SpecAssumption is spurious.

Thanks again for the help.

Best,

Smruti

[Stephan Merz]

Hello again,

my initial message was perhaps a little cryptic, so let me explain the rationale behind it. You were effectively trying to prove the implication

TypeInvariant /\ SafetyProperty /\ Inc => SafetyProperty'

but this implication doesn't hold. As a concrete counter-example, consider the state

valX = [ val |-> 42, ts |-> 23 ]

valY = [ val |-> 42, ts |-> 70 ]

clock = 27

(I'm omitting the variable n because it is unimportant for this discussion.)

Observe that this state satisfies both TypeInvariant and SafetyProperty. In particular, the latter holds trivially because the left-hand side of the implication is false. Now, Inc will lead you to the state

valX = [ val |-> 43, ts |-> 28 ]

valY = [ val |-> 42, ts |-> 70 ]

clock = 28

and SafetyProperty is false for that state. This shows that SafetyProperty is not inductive (relative to TypeInvariant).

However, the first state is actually not reachable in your specification, and one way to rule it out is to observe that time stamps cannot exceed the clock value. This observation leads to asserting the invariant ClockInv, which makes the proof go through. Now, in general there is no guarantee that the additional predicate is an inductive invariant: you may have to iterate the process and successively add more information about reachable states in order to obtain an inductive invariant that you can prove with a proof assistant such as TLAPS.

As for model checking, you are completely right that you need to bound the state space that TLC will explore. One standard way to do this is to add a state constraint where you bound the value of clock.

Stephan

-- 
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d9af2d7a-f150-422f-956a-98b6b69f7843n%40googlegroups.com.

[Smruti Padhy]

Thank you so much, Stephen for the detailed example.  It helped me a lot.

One quick question - Can this inductive invariant can be checked in the TLC model checker to check to get. an idea if it is a candidate inductive invariant? It involves Nat. I tried doing it by setting Nat to a small number but it shows the error : 

Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],

but can't enumerate the value of the `val' field:Nat

I think I am missing some assumptions in the spec or in the TLC settings. 

Best,

Smruti

[Karolis Petrauskas]

You can look at https://lamport.azurewebsites.net/tla/inductive-invariant.pdf for checking inductive invariants using TLC.

Karolis

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/189be644-18f8-40ae-9584-b552fc0c5842n%40googlegroups.com.

[Isaac DeFrain]

Hello Smurti,

Apalache is a great option for checking inductive invariants. The docs are here.

Best,

Isaac DeFrain

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/189be644-18f8-40ae-9584-b552fc0c5842n%40googlegroups.com.

[Stephan Merz]

Hello Smruti,

for checking if an invariant Inv is inductive you model check Inv for the specification

  Inv /\ [][Next]_vars

i.e. you replace the initial condition of your original specification by the invariant.

In order for this to work, the invariant should begin with a typing invariant that contains conjuncts x \in S for each variable, and S must be a set that TLC can enumerate. In particular, Nat cannot be enumerated and you will need to override it by an interval 0 .. N for some value N. 

Then, in order to make sure that values stay within that interval despite incrementation, you need to add a state constraint that ensures that states for which some Nat-valued variable or record component reaches N are discarded. For example, add a constraint "clock < N" so that TLC will never try to increment the clock in a state where clock = N.

By increasing the bound N, you increase your confidence in the result of (bounded) verification.

A corresponding variant of your spec is attached. In order to check that the invariant is inductive, do the following:

- Instantiate the constant largestNat by some value, say 10.

- In the model overview pane, indicate temporal formula CheckInductiveSpec as the behavior spec and InductiveInvariant as the invariant to be checked.

- In the additional spec options, add the predicate StateConstraint as (you guessed it) the state constraint and add a definition override Nat <- 0 .. largestNat.

Now run TLC. You'll see that all states are found when evaluating the initial state predicate (InductiveInvariant) whereas the actions do not generate any new states, confirming that the invariant is indeed inductive.

–––

This technique works for "small" state spaces. The note [1] mentioned by Karolis Petrauskas describes a technique for probabilistic invariant checking when state spaces are too big.

Regards,

Stephan

[1] https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

[Smruti Padhy]

Thanks, Karolis. Yes, I have read the paper. I also found the paper Proving Safety Properties (https://lamport.azurewebsites.net/tla/proving-safety.pdf) very useful.

Best,

Smruti 

[Smruti Padhy]

Thanks, Isaac, I will look into it.

Best,

Smruti

[Smruti Padhy]

Hi Stephan,

Thank you so much for the detailed explanation and the updated spec example. Now I understand how to define and set state constraints options in TLC. I did not see or aware of the state constraint option in TLC additional spec before this conversation. Thanks again for taking the time to explain that to me.

Best,

Smruti