Specs failing proof validation

[ahelwer]

I whipped up a quick script then downloaded & ran TLAPS 1.4.5 on macOS against all the modules containing proofs, and the following failed validation (no additional solvers installed, no additional command-line parameters given other than -I for include directory):

specifications/LoopInvariance/BinarySearch.tla
specifications/LoopInvariance/SumSequence.tla
specifications/Paxos/Consensus.tla
specifications/Paxos/Voting.tla
specifications/PaxosHowToWinATuringAward/Consensus.tla
specifications/PaxosHowToWinATuringAward/Voting.tla
specifications/ewd998/AsyncTerminationDetection_proof.tla
specifications/ewd998/EWD998_proof.tla
specifications/lamport_mutex/LamportMutex_proofs.tla

@muenchnerkindl I'd be interested in knowing how many of these are real proof failures and how many are due to wrong options or lack of installed solvers. My script was very simple, it just ran tlapm against each file and printed out the path if it returned a nonzero error code.

[ahelwer]

I re-ran the script using the 202210041448 1.5.0 pre-release and these are the list of failures instead:

Succeeded in 1.4.5 but fail in 1.5.0:

specifications/Bakery-Boulangerie/Bakery.tla
specifications/Bakery-Boulangerie/Boulanger.tla

Fail in both 1.4.5 and 1.5.0:

specifications/LoopInvariance/BinarySearch.tla
specifications/Paxos/Consensus.tla
specifications/Paxos/Voting.tla
specifications/PaxosHowToWinATuringAward/Consensus.tla
specifications/PaxosHowToWinATuringAward/Voting.tla
specifications/ewd998/EWD998_proof.tla
specifications/lamport_mutex/LamportMutex_proofs.tla

Upgrading to 1.5.0 fixed these proofs:

specifications/LoopInvariance/SumSequence.tla
specifications/ewd998/AsyncTerminationDetection_proof.tla

[will62794]

@ahelwer If it might be of any help, I wrote a small Python script a bit ago to parse the command line output of the TLAPS proof manager into a slightly more structured format. Just wanted to mention it in case it might be helpful to build on at any point e.g. to improve proof checking diagnostics in future.

[ahelwer]

@will62794 that's very cool, and a neat project! Is the python script published as a module on pypi?

[muenchnerkindl]

Thanks for checking the proofs in the examples repository. I fixed most of the broken proofs, except for the ones in LamportMutex_proofs that I'm still working on: we had to dumb down the SMT backend because it was getting a little too smart, and this broke a number of legitimate proofs.

I think the lesson for us is that we should consider the proofs in this repository, as we do for the examples in the prover distribution. For an interactive proof system, it doesn't make sense to promise backward compatibility. Some changes may be considered beneficial overall but still break existing proofs. But we should do a best-effort attempt at fixing proofs that we break.

The detail of what I found is below.

specifications/LoopInvariance/BinarySearch.tla
fixed (UNCHANGED not taken into account)

specifications/LoopInvariance/SumSequence.tla
works for me

specifications/MisraReachability/ParReachProofs.tla
works for me (this was mentioned in the original list but has since disappeared)

specifications/MisraReachability/ReachabilityProofs.tla
idem

specifications/MisraReachability/ReachableProofs.tla
idem

specifications/Paxos/Consensus.tla
fixed (in fact, added the proof: the existing proof was only a sketch of what we believed that temporal proofs could look like before we had support for temporal logic in the prover)

specifications/Paxos/Voting.tla
fixed (but didn't add the proof, it's available in the TLAPS distribution and should eventually be copied here)

specifications/PaxosHowToWinATuringAward/Consensus.tla
as above

specifications/PaxosHowToWinATuringAward/Voting.tla
as above

specifications/TwoPhase/TwoPhase.tla
works for me (again, this one no longer appears above)

specifications/ewd840/EWD840_proof.tla
works for me

specifications/ewd998/AsyncTerminationDetection_proof.tla
as noted at the top of the module, it requires using the development version of TLAPS for checking the liveness proofs

specifications/ewd998/EWD998_proof.tla
idem

specifications/lamport_mutex/LamportMutex_proofs.tla
still working on those ...

I haven't looked at the proofs in Bakery-Boulangerie yet that were not in the original list.

[will62794]

@helwer No, the script is not published, but feel free to extend/modify it and publish it there if you want.

[ahelwer]

@muenchnerkindl sorry for the false reports! Might have been some interaction of the 1.4.5 fingerprint files with the 1.5.0 fingerprint files. I deleted the .tlacache directory. The updated set of proof failures is:

specifications/Bakery-Boulangerie/Bakery.tla
specifications/Bakery-Boulangerie/Boulanger.tla
specifications/lamport_mutex/LamportMutex_proofs.tla

Finally, specifications/ewd998/EWD998_proof.tla seemingly fails due to #66:

Error: Operator "FoldFunctionOnSet" not found
 tlapm ending abnormally with Failure("Expr.Anon: 4")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from E_anon.anon#expr in file "e_anon.ml", line 226, characters 17-35
Called from E_visit.map#expr in file "e_visit.ml", line 59, characters 20-35
Called from E_anon.anon#expr in file "e_anon.ml", line 226, characters 17-35
Called from E_anon.anon_sg#defn in file "e_anon.ml", line 214, characters 14-30
Called from M_elab.normalize.spin in file "m_elab.ml", line 1368, characters 45-66
Called from M_elab.normalize in file "m_elab.ml", line 1457, characters 12-66
Called from Tlapm.process_module in file "tlapm.ml", line 293, characters 29-68
Called from Tlapm.main.f in file "tlapm.ml", line 503, characters 23-43
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 506, characters 13-40
Called from Tlapm.init in file "tlapm.ml", line 518, characters 8-33

when run with:

./tlapm-install/bin/tlapm specifications/ewd998/EWD998_proof.tla -I specifications/ewd
998 -I CommunityModules -I StandardModules

Can you help me out with caching proof results so that re-checking them is fast? How would I do that?

[muenchnerkindl]

For older versions of tlapm, fingerprints are stored at
/path/to/module/module.tlaps/fingerprints

More recent versions store them at
/path/to/module/.tlacache/module.tlaps/fingerprints

I don't think there is a command line option to change these paths so I'm assuming that if you want to persist the fingerprint files you'll have to do that in a script.

[muenchnerkindl]

I believe that all proofs now work again. Thanks for uncovering these issues!

[ahelwer]

Hi @muenchnerkindl thank you for your work! Unfortunately I am still running into issues with the following proofs, using release https://github.com/tlaplus/tlapm/releases/tag/202210041448 on Linux; click the dropdowns to see associated errors:

specifications/Bakery-Boulangerie/Bakery.tla

File "./specifications/Bakery-Boulangerie/Bakery.tla", line 398, characters 5-6:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  Procs == 1..N,
                  \prec(a, b) == \/ a[1] < b[1]
                                 \/ a[1] = b[1] /\ a[2] < b[2],
                  NEW VARIABLE num,
                  NEW VARIABLE flag,
                  NEW VARIABLE pc,
                  NEW VARIABLE unchecked,
                  NEW VARIABLE max,
                  NEW VARIABLE nxt,
                  ProcSet == Procs,
                  w2(self) ==
                    /\ pc[self] = "w2"
                    /\ \/ num[nxt[self]] = 0
                       \/ <<num[self], self>>
                          \prec <<num[nxt[self]], nxt[self]>>
                    /\ unchecked'
                       = [unchecked EXCEPT
                            ![self] = unchecked[self] \ {nxt[self]}]
                    /\ pc' = [pc EXCEPT !
                                   [self] = "w1"]
                    /\ UNCHANGED <<num, flag, max, nxt>>,
                  TypeOK ==
                    /\ num \in [Procs -> Nat]
                    /\ flag \in [Procs -> BOOLEAN]
                    /\ unchecked \in [Procs -> SUBSET Procs]
                    /\ max \in [Procs -> Nat]
                    /\ nxt \in [Procs -> Procs]
                    /\ pc
                       \in [Procs ->
                              {"ncs", "e1", "e2", "e3", "e4", "w1", "w2",
                               "cs", "exit"}],
                  Before(i, j) ==
                    /\ num[i] > 0
                    /\ \/ pc[j] \in {"ncs", "e1", "exit"}
                       \/ /\ pc[j] = "e2"
                          /\ \/ i \in unchecked[j]
                             \/ max[j] >= num[i]
                       \/ /\ pc[j] = "e3"
                          /\ max[j] >= num[i]
                       \/ /\ pc[j] \in {"e4", "w1", "w2"}
                          /\ <<num[i], i>> \prec <<num[j], j>>
                          /\ pc[j] \in {"w1", "w2"} => i \in unchecked[j],
                  Inv ==
                    /\ TypeOK
                    /\ \A i \in Procs :
                          /\ pc[i] \in {"e4", "w1", "w2", "cs"} => num[i] # 0
                          /\ pc[i] \in {"e2", "e3"} => flag[i]
                          /\ pc[i] = "w2" => nxt[i] # i
                          /\ pc[i] \in {"w1", "w2"} => i \notin unchecked[i]
                          /\ pc[i] \in {"w1", "w2"}
                             => (\A j \in (Procs \ unchecked[i]) \ {i} :
                                   Before(i, j))
                          /\ (/\ pc[i] = "w2"
                              /\ \/ pc[nxt[i]] = "e2"
                                   /\ 
                                   i \notin unchecked[nxt[i]]
                                 \/ pc[nxt[i]] = "e3")
                             => max[nxt[i]] >= num[i]
                          /\ pc[i] = "cs"
                             => (\A j \in Procs \ {i} : Before(i, j)),
                  N \in Nat ,
                  Inv ,
                  [Next]_vars ,
                  NEW CONSTANT self \in Procs,
                  <2>7 ,
                  Z3 
           PROVE  Inv'
File "./specifications/Bakery-Boulangerie/Bakery.tla", line 1, character 1 to line 457, character 77:
[ERROR]: 1/121 obligations failed.

specifications/Bakery-Boulangerie/Boulanger.tla

File "./specifications/Bakery-Boulangerie/Boulanger.tla", line 490, characters 7-8:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  Procs == 1..N,
                  \prec(a, b) == \/ a[1] < b[1]
                                 \/ a[1] = b[1] /\ a[2] < b[2],
                  NEW VARIABLE num,
                  NEW VARIABLE flag,
                  NEW VARIABLE pc,
                  NEW VARIABLE unchecked,
                  NEW VARIABLE max,
                  NEW VARIABLE nxt,
                  NEW VARIABLE previous,
                  ProcSet == Procs,
                  TypeOK ==
                    /\ num \in [Procs -> Nat]
                    /\ flag \in [Procs -> BOOLEAN]
                    /\ unchecked \in [Procs -> SUBSET Procs]
                    /\ max \in [Procs -> Nat]
                    /\ nxt \in [Procs -> Procs]
                    /\ pc
                       \in [Procs ->
                              {"ncs", "e1", "e2", "e3", "e4", "w1", "w2",
                               "cs", "exit"}]
                    /\ previous \in [Procs -> Nat \cup {-1}],
                  Before(i, j) ==
                    /\ num[i] > 0
                    /\ \/ pc[j] \in {"ncs", "e1", "exit"}
                       \/ /\ pc[j] = "e2"
                          /\ \/ i \in unchecked[j]
                             \/ max[j] >= num[i]
                             \/ j > i /\ max[j] + 1 = num[i]
                       \/ /\ pc[j] = "e3"
                          /\ \/ max[j] >= num[i]
                             \/ j > i /\ max[j] + 1 = num[i]
                       \/ /\ pc[j] \in {"e4", "w1", "w2"}
                          /\ <<num[i], i>> \prec <<num[j], j>>
                          /\ pc[j] \in {"w1", "w2"} => i \in unchecked[j]
                       \/ /\ num[i] = 1
                          /\ i < j,
                  Inv ==
                    /\ TypeOK
                    /\ \A i \in Procs :
                          /\ pc[i] \in {"ncs", "e1", "e2"} => num[i] = 0
                          /\ pc[i] \in {"e4", "w1", "w2", "cs"} => num[i] # 0
                          /\ pc[i] \in {"e2", "e3"} => flag[i]
                          /\ pc[i] = "w2" => nxt[i] # i
                          /\ pc[i] \in {"e2", "w1", "w2"}
                             => i \notin unchecked[i]
                          /\ pc[i] \in {"w1", "w2"}
                             => (\A j \in (Procs \ unchecked[i]) \ {i} :
                                   Before(i, j))
                          /\ (/\ pc[i] = "w2"
                              /\ \/ pc[nxt[i]] = "e2"
                                   /\ 
                                   i \notin unchecked[nxt[i]]
                                 \/ pc[nxt[i]] = "e3")
                             => max[nxt[i]] >= num[i]
                          /\ (/\ pc[i] = "w2"
                              /\ previous[i] # -1
                              /\ previous[i] # num[nxt[i]]
                              /\ pc[nxt[i]] \in {"e4", "w1", "w2", "cs"})
                             => Before(i, nxt[i])
                          /\ pc[i] = "cs"
                             => (\A j \in Procs \ {i} : Before(i, j)),
                  N \in Nat ,
                  Inv ,
                  [Next]_vars ,
                  NEW CONSTANT self \in Procs,
                  <3>_a23 ,
                  <3>2 ,
                  Z3 
           PROVE  Inv'
File "./specifications/Bakery-Boulangerie/Boulanger.tla", line 1, character 1 to line 532, character 77:
[ERROR]: 1/125 obligations failed.

specifications/Paxos|PaxosHowToWinATuringAward/Consensus.tla

File "./specifications/Paxos/Consensus.tla", line 44, characters 5-6:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT Value,
                  NEW VARIABLE chosen,
                  TypeOK == /\ chosen \subseteq Value
                            /\ IsFiniteSet(chosen),
                  Next == /\ chosen = {}
                          /\ \E v \in Value : chosen' = {v},
                  Inv == /\ TypeOK
                         /\ Cardinality(chosen) =< 1,
                  FS_Singleton 
           PROVE  Inv /\ Next => Inv'
File "./specifications/Paxos/Consensus.tla", line 1, character 1 to line 58, character 77:
[ERROR]: 1/12 obligations failed.

specifications/lamport_mutex/LamportMutex_proofs.tla

File "./specifications/lamport_mutex/LamportMutex_proofs.tla", line 667, characters 11-12:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  NEW CONSTANT maxClock,
                  NType == N \in Nat,
                  maxClockType == maxClock \in Nat,
                  Clock == Nat \ {0},
                  NEW VARIABLE clock,
                  NEW VARIABLE req,
                  NEW VARIABLE ack,
                  NEW VARIABLE network,
                  NEW VARIABLE crit,
                  TypeOK ==
                    /\ clock \in [Proc -> Clock]
                    /\ req \in [Proc -> [Proc -> Nat]]
                    /\ ack \in [Proc -> SUBSET Proc]
                    /\ network \in [Proc -> [Proc -> Seq(Message)]]
                    /\ crit \in SUBSET Proc,
                  Precedes(s, mt1, mt2) ==
                    \A i, j \in 1..Len(s) :
                       s[i].type = mt1 /\ s[j].type = mt2 => i < j,
                  TypeOK ,
                  BasicInv ,
                  ClockInv ,
                  [Next]_vars ,
                  NEW CONSTANT n \in Proc,
                  NEW CONSTANT k \in 
                  Proc \ {n},
                  m == Head(network[k][n]),
                  <3>_a713 ,
                  NEW CONSTANT p \in Proc,
                  NEW CONSTANT q \in 
                  Proc \ {p},
                  pq == network[p][q],
                  qp == network[q][p],
                  <4>_a714 ,
                  NEW CONSTANT i \in 
                  1..Len(qp'),
                  <3>1 ,
                  <4>1 ,
                  <5>5 
           PROVE  FALSE
File "./specifications/lamport_mutex/LamportMutex_proofs.tla", line 640, characters 7-8:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  NEW CONSTANT maxClock,
                  NType == N \in Nat,
                  maxClockType == maxClock \in Nat,
                  Clock == Nat \ {0},
                  NEW VARIABLE clock,
                  NEW VARIABLE req,
                  NEW VARIABLE ack,
                  NEW VARIABLE network,
                  NEW VARIABLE crit,
                  TypeOK ==
                    /\ clock \in [Proc -> Clock]
                    /\ req \in [Proc -> [Proc -> Nat]]
                    /\ ack \in [Proc -> SUBSET Proc]
                    /\ network \in [Proc -> [Proc -> Seq(Message)]]
                    /\ crit \in SUBSET Proc,
                  Contains(s, mtype) ==
                    \E i \in 1..Len(s) : s[i].type = mtype,
                  ClockInvInner(p, q) ==
                    LET pq == network[p][q]
                        qp == network[q][p]
                    IN  /\ \A i \in 1..Len(pq) :
                              pq[i].type = "req" => pq[i].clock = req[p][p]
                        /\ Contains(qp, "ack") \/ q \in ack[p]
                           => (/\ req[q][p] = req[p][p]
                               /\ clock[q] > req[p][p]
                               /\ Precedes(qp, "ack", "req")
                                  => (
                                  \A i \in 1..Len(qp) :
                                   qp[i].type = "req"
                                   => 
                                   qp[i].clock > req[p][p]))
                        /\ p \in crit => beats(p, q),
                  ClockInv ==
                    \A p \in Proc : \A q \in Proc \ {p} : ClockInvInner(p, q),
                  TypeOK ,
                  BasicInv ,
                  ClockInv ,
                  [Next]_vars ,
                  NEW CONSTANT n \in Proc,
                  NEW CONSTANT k \in 
                  Proc \ {n},
                  m == Head(network[k][n]),
                  <3>1 
           PROVE  m.clock = req[k][k]
File "./specifications/lamport_mutex/LamportMutex_proofs.tla", line 1, character 1 to line 811, character 78:
[ERROR]: 2/654 obligations failed.

One final strange one is specifications/ewd998/EWD998_proof.tla, which will ordinarily fail because it cannot find Randomization.tla. If I extract the standard modules (which include Randomization.tla) from the nightly tla2tools.jar and put them on the tlaps path with the -I flag, nearly all modules with proofs will fail. If I put Randomization.tla on the paths included with -I alone, it fails with this error:

specifications/lamport_mutex/LamportMutex_proofs.tla

File "./specifications/ewd998/EWD998_proof.tla", line 782, characters 9-10:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  NAssumption == N \in Nat \ {0},
                  NEW VARIABLE active,
                  NEW VARIABLE color,
                  NEW VARIABLE counter,
                  NEW VARIABLE pending,
                  NEW VARIABLE token,
                  terminationDetected ==
                    /\ token.pos = 0
                    /\ token.color = "white"
                    /\ token.q + counter[0] = 0
                    /\ color[0] = "white"
                    /\ ~active[0],
                  NAssumption ,
                  NodeIsNode ,
                  TypeOK ,
                  TypeOK' ,
                  Inv ,
                  Inv' ,
                  [Next]_vars ,
                  <3>2 ,
                  <3>4 
           PROVE  /\ (token').pos = 0
                  /\ ~active[0]
                  /\ pending[0] = 0
File "./specifications/ewd998/EWD998_proof.tla", line 666, characters 17-18:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  NAssumption == N \in Nat \ {0},
                  Node == 0..N - 1,
                  Token == [pos : Node, q : Int, color : Color],
                  NEW VARIABLE active,
                  NEW VARIABLE color,
                  NEW VARIABLE counter,
                  NEW VARIABLE pending,
                  NEW VARIABLE token,
                  TypeOK ==
                    /\ active \in [Node -> BOOLEAN]
                    /\ color \in [Node -> Color]
                    /\ counter \in [Node -> Int]
                    /\ pending \in [Node -> Nat]
                    /\ token \in Token,
                  InitiateProbe ==
                    /\ token.pos = 0
                    /\ \/ token.color = "black"
                       \/ color[0] = "black"
                       \/ counter[0] + token.q > 0
                    /\ token' = [pos |-> N - 1, q |-> 0, color |-> "white"]
                    /\ color' = [color EXCEPT !
                                   [0] = "white"]
                    /\ UNCHANGED <<active, counter, pending>>,
                  B == Sum(pending, Node),
                  Termination == /\ \A i \in Node : ~active[i]
                                 /\ B = 0,
                  NAssumption ,
                  atMaster == token.pos = 0,
                  tknWhite == token.color = "white",
                  allWhite == \A i \in Node : color[i] = "white",
                  P(n) ==
                    /\ Termination /\ n \in Node /\ token.pos = n
                    /\ allWhite /\ tknWhite
                    /\ token.q = Sum(counter, Rng(n + 1, N - 1)),
                  Q == P(0),
                  R(n) == BSpec => [](P(n) => <>Q),
                  S == Termination /\ atMaster /\ allWhite,
                  T == P(N - 1),
                  TypeOK ,
                  S ,
                  System ,
                  <4>_a881 ,
                  <3>1 ,
                  SumEmpty 
           PROVE  T'
File "./specifications/ewd998/EWD998_proof.tla", line 519, characters 7-8:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  NAssumption == N \in Nat \ {0},
                  Node == 0..N - 1,
                  Token == [pos : Node, q : Int, color : Color],
                  NEW VARIABLE active,
                  NEW VARIABLE color,
                  NEW VARIABLE counter,
                  NEW VARIABLE pending,
                  NEW VARIABLE token,
                  TypeOK ==
                    /\ active \in [Node -> BOOLEAN]
                    /\ color \in [Node -> Color]
                    /\ counter \in [Node -> Int]
                    /\ pending \in [Node -> Nat]
                    /\ token \in Token,
                  B == Sum(pending, Node),
                  Termination == /\ \A i \in Node : ~active[i]
                                 /\ B = 0,
                  Inv ==
                    /\ P0::(B = Sum(counter, Node))
                    /\ \/ P1::/\ \A i \in Rng(token.pos + 1, N - 1) :
                                   active[i] = FALSE
                              /\ IF token.pos = N - 1
                                   THEN token.q = 0
                                   ELSE 
                                   token.q
                                   = 
                                   Sum(counter, Rng(token.pos + 1, N - 1))
                       \/ P2::(Sum(counter, Rng(0, token.pos)) + token.q > 0)
                       \/ P3::\E i \in Rng(0, token.pos) : color[i] = "black"
                       \/ P4::(token.color = "black"),
                  NAssumption ,
                  TypeOK ,
                  Inv ,
                  Termination ,
                  token.pos = 0 ,
                  ~terminationDetected ,
                  <2>1 ,
                  <3>1 
           PROVE  counter[0] + token.q = 0
File "./specifications/ewd998/EWD998_proof.tla", line 432, characters 9-10:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  NAssumption == N \in Nat \ {0},
                  Node == 0..N - 1,
                  NEW VARIABLE active,
                  NEW VARIABLE color,
                  NEW VARIABLE counter,
                  NEW VARIABLE pending,
                  NEW VARIABLE token,
                  TypeOK ==
                    /\ active \in [Node -> BOOLEAN]
                    /\ color \in [Node -> Color]
                    /\ counter \in [Node -> Int]
                    /\ pending \in [Node -> Nat]
                    /\ token \in Token,
                  Rng(a, b) == {i \in Node : a =< i /\ i =< b},
                  NAssumption ,
                  TypeOK ,
                  Inv ,
                  terminationDetected ,
                  <4>1 ,
                  SumEmpty 
           PROVE  Sum(counter, Rng(0, 0)) = counter[0]
File "./specifications/ewd998/EWD998_proof.tla", line 249, characters 11-12:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT N,
                  NAssumption == N \in Nat \ {0},
                  Token == [pos : Node, q : Int, color : Color],
                  NEW VARIABLE active,
                  NEW VARIABLE color,
                  NEW VARIABLE counter,
                  NEW VARIABLE pending,
                  NEW VARIABLE token,
                  TypeOK ==
                    /\ active \in [Node -> BOOLEAN]
                    /\ color \in [Node -> Color]
                    /\ counter \in [Node -> Int]
                    /\ pending \in [Node -> Nat]
                    /\ token \in Token,
                  NAssumption ,
                  TypeOK ,
                  TypeOK' ,
                  Inv ,
                  [Next]_vars ,
                  NEW CONSTANT i \in 
                  Node \ {0},
                  <5>1 ,
                  <5>2 ,
                  <5>3 ,
                  <5>4 ,
                  <5>5 
           PROVE  Sum(counter, Rng(0, token.pos))' + (token').q
                  = Sum(counter, Rng(0, token.pos)) + token.q
File "./specifications/ewd998/EWD998_proof.tla", line 1, character 1 to line 860, character 77:
[ERROR]: 5/758 obligations failed.

You can also see these errors occurring in this CI run: https://github.com/tlaplus/Examples/actions/runs/4347799514/jobs/7595536785

[ahelwer]

I am also seeing strange behavior with fingerprint caching. Only some proofs seem to benefit from it; if I delete the .tlacache directory (which is output in the working directory from which I run TLAPS) then I see:

[ahelwer@node examples]$ python .github/scripts/check_proofs.py 
specifications/LoopInvariance/BinarySearch.tla
Checked proofs in 6.2s
specifications/MisraReachability/ParReachProofs.tla
Checked proofs in 1.4s
specifications/MisraReachability/ReachabilityProofs.tla
Checked proofs in 5.7s
specifications/MisraReachability/ReachableProofs.tla
Checked proofs in 5.4s
specifications/Paxos/Voting.tla
Checked proofs in 0.7s
specifications/PaxosHowToWinATuringAward/Voting.tla
Checked proofs in 0.7s
specifications/TeachingConcurrency/Simple.tla
Checked proofs in 0.2s
specifications/TeachingConcurrency/SimpleRegular.tla
Checked proofs in 5.3s
specifications/TwoPhase/TwoPhase.tla
Checked proofs in 0.2s
specifications/ewd840/EWD840_proof.tla
Checked proofs in 0.5s
specifications/ewd998/AsyncTerminationDetection_proof.tla
Checked proofs in 0.8s
specifications/ewd998/EWD998_proof.tla
Checked proofs in 0.2s

If I then run it again without deleting the fingerprints, I get:

[ahelwer@node examples]$ python .github/scripts/check_proofs.py 
specifications/LoopInvariance/BinarySearch.tla
Checked proofs in 0.7s
specifications/MisraReachability/ParReachProofs.tla
Checked proofs in 0.6s
specifications/MisraReachability/ReachabilityProofs.tla
Checked proofs in 5.7s
specifications/MisraReachability/ReachableProofs.tla
Checked proofs in 0.6s
specifications/Paxos/Voting.tla
Checked proofs in 0.7s
specifications/PaxosHowToWinATuringAward/Voting.tla
Checked proofs in 0.7s
specifications/TeachingConcurrency/Simple.tla
Checked proofs in 0.1s
specifications/TeachingConcurrency/SimpleRegular.tla
Checked proofs in 0.1s
specifications/TwoPhase/TwoPhase.tla
Checked proofs in 0.1s
specifications/ewd840/EWD840_proof.tla
Checked proofs in 0.3s
specifications/ewd998/AsyncTerminationDetection_proof.tla
Checked proofs in 0.2s
specifications/sums_even/sums_even.tla
Checked proofs in 0.1s

So for some reason specifications/MisraReachability/ReachabilityProofs.tla (and possibly Voting.tla) is not hitting the fingerprint cache and seems to be checking all proofs from scratch.

[damiendoligez]

I compiled and installed from a fresh checkout of 202210041448 and couldn't reproduce any of the failures you reported. Could you run tlapm --config and post the output here?

[damiendoligez]

OK I managed to reproduce the problem under Ubuntu.

[damiendoligez]

specifications/Bakery-Boulangerie/Bakery.tla

This one is easy, it's a timeout. Z3 is given 5 seconds to solve the proof obligation, but (on my machine) it takes about 11 seconds. I've submitted #73 to increase the timeout to 30 seconds.