[tlaplus] Re: Help understanding why this proof validates

This is strange. If I change my proof to:

THEOREM Spec => []TypeOK
PROOF
<1>a. Init => TypeOK
BY DEF Init, TypeOK
<1>b. TypeOK /\ UNCHANGED vars => TypeOK'
BY DEF TypeOK, vars
<1>c. TypeOK /\ Next => TypeOK'
<2>a. TypeOK /\ lb => TypeOK'
<2>b. TypeOK /\ Terminating => TypeOK'
<2> QED BY <2>a, <2>b DEF Next
<1> QED BY PTL, <1>a, <1>b, <1>c DEF Spec

then tlapm will report all 10 obligations proved and return with error code 0. But then if I run tlapm with the --summary flag, I get:

---- summary of module "TLAPS" ----
obligations_count = 0
====
(* loading fingerprints in ".tlacache/FindHighest.tlaps/fingerprints" *)
---- summary of module "FindHighest" ----
obligations_count = 10
missing_proofs_count = 2
---- incomplete proof of theorem at line 67, character 1 ----
missing_proofs_count = 2
missing_proof_1 at line 74, characters 5-33
missing_proof_2 at line 75, characters 5-42
====
====

So we see we indeed are missing proofs. Why is tlapm reporting that the missing proofs were successfully proved?

Andrew

On Mon, Mar 27, 2023 at 3:14 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> 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 -2

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

Next == lb
\/ Terminating

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

Termination == <>(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 => []TypeOK
PROOF
<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 -2

under 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