CI: check proofs with --strict

[vasilisnasopoulos]

Follows up on tlaplus/CommunityModules#128, where @lemmy suggested the same change here.

tlapm exits 0 when a proof step carries no proof at all — such steps generate no obligation, so they never appear in the count and the job passes over a proof that did not close. --strict (tlaplus/tlapm#278) reports this as exit 11.

I measured it against current master rather than assuming. Of the 67 proof modules this job runs, 62 are unaffected. Five change:

module	plain	--strict	tlapm summary
Paxos/Voting.tla	0	11	All 7 obligations proved
PaxosHowToWinATuringAward/Voting.tla	0	11	All 9 obligations proved
byzpaxos/PConProof.tla	0	11	All 10 obligations proved
allocator/AllocatorImplementation_proof.tla	0	11	All 195 obligations proved
MultiCarElevator/Elevator_proof.tla	0	11	All 223 obligations proved

(ewd998/EWD998_proof.tla was a sixth until #218.)

Rather than skip those five outright, they are checked in a separate step without the flag, mirroring the existing SumSequence.tla exclusion. That way they are still verified, and the list of proofs with open steps is visible in the workflow rather than implied.

@muenchnerkindl noted on the other thread that most of these omissions are deliberate — teaching material where leaving the interesting step open is the point. Two of them do not obviously read that way to me, though: allocator/AllocatorImplementation_proof.tla (195 obligations) and MultiCarElevator/Elevator_proof.tla (223). If either is unintentional I would be glad to look at it the way #218 went; if they are all deliberate, the split above is simply documentation.

Measurement run, both invocations for all 67 modules: https://github.com/vasilisnasopoulos-stack/vortex-dse-cslot-proofs/actions/runs/30840318792

[muenchnerkindl]

@vasilisnasopoulos-stack Thank you for offering to help with these proofs! The omitted proof in allocator/AllocatorImplementation_proof.tla has to do with a known issue in referring to facts derived in instantiated modules. Getting this to work would be very technical, if at all possible, with the current implementation. This part of the PM is supposed to be reimplemented shortly, and I'd suggest deferring this proof a little: it could serve as a test case for the new implementation.

The omitted proofs in MultiCarElevator/Elevator_proof.tla are all due to a limitation in the PM, which does not handle function definitions of the form [x \in S, y \in T |-> e(x,y)]. As documented in the module, the workaround would be to change the definition to either [xy \in S \X T |-> e(xy[1], xy[2])], [<<x,y>> \in S \X T |-> e(x,y)] or [x \in S |-> [y \in T |-> e(x,y)]]. The author of the proof decided not to touch the original definition, so currently there is simply no way to do these proofs. (Extending the PM implementation to handle such definitions would be welcome, though.)

[vasilisnasopoulos]

Thank you — that is a much better answer than I expected, and it changes how the exclusions should read.

I had assumed the two larger ones might simply be unfinished. They are not: both are blocked on the prover rather than left open by choice. I have annotated the exclusion list accordingly (c8a1f0e), so the workflow now distinguishes "deliberately open" from "currently not expressible", rather than lumping all five together.

Deferring AllocatorImplementation until the instantiation handling is reimplemented makes sense; it is a better test case for the new implementation than for me.

On extending the PM to handle [x \in S, y \in T |-> e(x,y)] — I would be interested, but I have not worked in the tlapm codebase and would rather not overstate what I can do there. If you think it is a reasonable first thing to attempt, I would appreciate a pointer to where that desugaring would live; if it touches enough of the front end that it is really a maintainer job, I would rather know that up front.

[muenchnerkindl]

If you think it is a reasonable first thing to attempt

I'm afraid it requires touching too much, and the code base is quite delicate. That's why the issue has been delayed for so long.

[vasilisnasopoulos]

Understood, and thank you for saying so plainly — that is exactly what I was hoping to find out before starting rather than after.

I have left the exclusion comments as they are, since they now record the reason in the workflow itself: the next person who wonders why those five are excluded will find your explanation rather than guessing.

The PR is otherwise ready from my side.