Help understanding why this proof validates

[Andrew Helwer]

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

[Andrew Helwer]

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

[Stephan Merz]

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.

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/CABj%3DxUVYE8ZRF%3D8BNj8bDkU9fELtk1UNjVBfDYWC0ebhM8TkFA%40mail.gmail.com.