Re: [tlaplus] Help understanding why this proof validates

• From: Stephan Merz <stephan.merz@xxxxxxxxx>
• Date: Tue, 28 Mar 2023 08:35:37 +0200
• References: <CABj=xUVYE8ZRF=8BNj8bDkU9fELtk1UNjVBfDYWC0ebhM8TkFA@mail.gmail.com>

 Hi Andrew,TLAPS behaves as expected: all proofs that you wrote are successfully checked by the prover, and they are all valid. However, the level-2 QED step has no proof, and it is therefore not checked. Were you using the Toolbox, you'd see that step (and the assertion of the theorem) colored yellow, indicating that proofs are missing.Should the command-line version display information about missing proofs more prominently by default? Perhaps, but that's not the way it is programmed today, and as you found out, you can obtain that information using the --summary command-line option.StephanOn 27 Mar 2023, at 21:14, Andrew Helwer wrote:Hello, I am writing a proof of a very simple PlusCal algorithm that iterates over a sequence and records its largest element. Currently I am just proving the type invariant, TypeOK:---------------------------- MODULE FindHighest -----------------------------EXTENDS Sequences, Naturals, Integers, TLAPS(****************************************************************************--algorithm Highest {  variables    f \in Seq(Nat);    h = -1;    i = 1;  define {    max(a, b) == IF a > b THEN a ELSE b  } {lb: while (i <= Len(f)) {      h := max(h, f[i]);      i := i + 1;    }  }}****************************************************************************)\* BEGIN TRANSLATION (chksum(pcal) = "c908a386" /\ chksum(tla) = "36657a9f")VARIABLES f, h, i, pc(* define statement *)max(a, b) == IF a > b THEN a ELSE -2vars == << f, h, i, pc >>Init == (* Global variables *)        /\ f \in Seq(Nat)        /\ h = -1        /\ i = 1        /\ pc = "lb"lb == /\ pc = "lb"      /\ IF i <= Len(f)            THEN /\ h' = max(h, f[i])                 /\ i' = i + 1                 /\ pc' = "lb"            ELSE /\ pc' = "Done"                 /\ UNCHANGED << h, i >>      /\ f' = f(* Allow infinite stuttering to prevent deadlock on termination. *)Terminating == pc = "Done" /\ UNCHANGED varsNext == lb           \/ TerminatingSpec == Init /\ [][Next]_varsTermination == <>(pc = "Done")\* END TRANSLATION TypeOK ==  IF f = <<>>  THEN    /\ f = <<>>    /\ h = -1    /\ i = 1  ELSE    /\ f \in Seq(Nat)    /\ h \in Nat \cup {-1}    /\ i \in 1..Len(f)THEOREM Spec => []TypeOKPROOF  <1>a. Init => TypeOK    BY DEF Init, TypeOK  <1>b. TypeOK /\ UNCHANGED vars => TypeOK'    BY DEF TypeOK, vars  <1>c. TypeOK /\ Next => TypeOK'    <2> SUFFICES  /\ TypeOK /\ lb => TypeOK'                  /\ TypeOK /\ Terminating => TypeOK'        BY DEF Next    <2> QED  <1> QED BY PTL, <1>a, <1>b, <1>c DEF Spec=============================================================================Surprisingly, this proof checks out. I am using the 202210041448 1.5.0 pre-release of tlapm. I would assume the subproof of TypeOK /\ Next => TypeOK' would have to be greatly expanded in order to check properly. Also, doing simple modifications like changing the definition of max to:max(a, b) == IF a > b THEN a ELSE -2under which TypeOK should not hold results in tlapm still validating the proof:tlapm FindHighest.tla(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)File "/home/ahelwer/.local/lib/tlaps/TLAPS.tla", line 1, character 1 to line 362, character 77:[INFO]: All 0 obligation proved.fgrep: warning: fgrep is obsolescent; using grep -F** Unexpanded symbols: ---** Unexpanded symbols: ---** Unexpanded symbols: ACTION_lb_, ACTION_Terminating_, STATE_TypeOK_(* created new ".tlacache/FindHighest.tlaps/FindHighest.thy" *)(* fingerprints written in ".tlacache/FindHighest.tlaps/fingerprints" *)File "./FindHighest.tla", line 1, character 1 to line 79, character 77:[INFO]: All 8 obligations proved.Why is this proof validating? Am I accidentally typing something with SUFFICES that is interpreted as an OMITTED proof? Thanks,Andrew Helwer -- 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/CABj%3DxUVYE8ZRF%3D8BNj8bDkU9fELtk1UNjVBfDYWC0ebhM8TkFA%40mail.gmail.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/BB10F913-6529-4B04-ABC6-B2BE7200445A%40gmail.com.