ci: pass --strict when verifying TLAPS proofs

[vasilisnasopoulos]

The TLAPS job runs

tlapm --cleanfp "$proof" || status=1

but tlapm exits 0 even when obligations fail, so || status=1 never fires and the job reports success over a proof that did not close. Context in tlaplus/tlapm#287; --strict was added in tlaplus/tlapm#278 and gives distinct non-zero codes for failed obligations (10), incomplete proofs (11), and empty targets (12).

This is not a latent failure here. I ran all six _proofs.tla modules against tlapm 1.6.0-pre (096df83), with and without the flag:

module	exit with --strict	result
FiniteSetsExtTheorems_proofs.tla	0	All 431 obligations proved
FoldsTheorems_proofs.tla	0	All 244 obligations proved
FunctionTheorems_proofs.tla	0	All 771 obligations proved
GraphTheorems_proofs.tla	0	All 506 obligations proved
QuorumTheorems_proofs.tla	0	All 7 obligations proved
SequencesExtTheorems_proofs.tla	0	All 930 obligations proved

Aggregate status is 0 both with and without --strict, so this changes nothing today. It makes the job fail if a future change breaks one of those 2,889 obligations, which it currently would not.

Run: https://github.com/vasilisnasopoulos-stack/vortex-dse-cslot-proofs/actions/runs/30570917693

[lemmy]

I suppose a similar change should be made at tlaplus/examples. ;-)

[vasilisnasopoulos]

Happy to. Before sending a patch there I would rather measure it: Examples runs 68 proof modules from many contributors, and --strict also flags incomplete proofs, not just failed ones — so unlike here, I cannot assume the outcome is unchanged. The CI already carries a manual exclusion for LoopInvariance/SumSequence.tla ("Failing on Linux"), which suggests there may be more to find.

I will run the full set both ways and report what actually changes. If it is clean, the PR is the same one-word change. If it is not, that seems worth knowing regardless of whether the flag lands.

[vasilisnasopoulos]

Reporting back on tlaplus/Examples, as promised. I am not opening a PR there, because the flag would not be a no-op the way it was here.

I ran the same selection the CI makes — modules with a proof entry, excluding LoopInvariance/SumSequence.tla, maxRuntimeMinutes <= 5 — against tlapm 1.6.0-pre (096df83), twice: once exactly as CI invokes it, once with --strict added. 67 modules.

60 are unaffected. Six change:

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

Exit 11 is the incomplete-proof case from #278 — steps carrying no proof, which generate no obligation and so do not show up in the count. Paxos/Voting.tla is the smallest illustration:

THEOREM Invariance == Spec => []Inv

THEOREM Spec => C!Spec
<1>1. Inv /\ Init => C!Init
<1>2. Inv /\ [Next]_<<votes, maxBal>> => [C!Next]_chosen
<1>3. QED
  BY <1>1, <1>2, Invariance, PTL DEF Spec, C!Spec

<1>1 and <1>2 are stated, used by the QED step, and never proved. tlapm reports "All 7 obligations proved" and exits 0.

I have no opinion on whether these should be closed. Several are teaching material where leaving the interesting steps open is presumably the point, and that is a reasonable thing for a specification to do. The observation is narrower: as things stand the CI cannot distinguish a proof that closed from one that was asserted, so if any of those six is unintentional, nothing will say so.

If it is useful, the options I can see are to add --strict together with an explicit skip list for the deliberate cases, mirroring the existing SumSequence.tla exclusion; or to leave the flag off and treat this purely as information. Happy to prepare either, or neither.

One caveat I cannot resolve from here: specifications/ewd687a/EWD687a_proof.tla exits 3 in my runs, with and without the flag, so it is unrelated to --strict — but it does mean my environment differs from yours somewhere, since your CI is green. Worth a glance in case it is not just me.

Full run, including the per-module table: https://github.com/vasilisnasopoulos-stack/vortex-dse-cslot-proofs/actions/runs/30656083825

[muenchnerkindl]

Thank you for this analysis. I believe that indeed most of the omitted proofs are left open deliberately, although I agree that this is somewhat inconsistent (for example, I believe that Paxos/Voting.tla has a proof in the examples directory of the PM distribution). Instead of introducing "library" lemmas without proofs in EWD998_proof.tla, one should now be able to use the relevant lemmas about fold from the Community Modules.

EWD687a_proof is recent, it passes both locally for me and in the CI. What environment do you use?

[vasilisnasopoulos]

Environment was the problem, and it was mine — apologies for the noise.

I fetched CommunityModules-deps.jar but never unzipped it, so -I pointed at a directory containing only the jar. EWD687a_proof.tla extends Graphs and GraphTheorems, hence:

Error: Unknown module "GraphTheorems"
Error: Unknown module "Graphs"

Your linux-setup.sh does unzip "$DEPS_DIR/community/modules.jar" -d "$DEPS_DIR/community", which I had skipped. With that added, on ubuntu-latest with tlapm 1.6.0-pre (096df83):

	exit
plain	0	All 407 obligations proved
--strict	0	All 407 obligations proved

So EWD687a_proof is fine and unaffected by the flag. The six modules in the table above are unchanged by this — none of them extend community modules, and they were run the same way you would.

On EWD998: agreed, and that seems like the more interesting thread — replacing the unproved local lemmas with the proved fold lemmas from CommunityModules would close the gap rather than just excluding it. Happy to look at that if it would help.

[muenchnerkindl]

If you want to have a stab at EWD998, that would be very welcome. Happy to help if necessary. Otherwise I may do it when I have some time.

[vasilisnasopoulos]

I'll take a stab at it — thanks for the offer of help, I may well take you up on it.

Scope as I read it: nine lemmas in EWD998_proof.tla are stated without proof. Six are the FoldFunctionOnSet* family, which look like they map onto the proved theorems in FunctionTheorems almost name-for-name. The remaining three (SumIterate, SumUnion, SumEqual) are EWD998-specific and would need proving on top of those, since Sum is defined locally.

Plan is to replace the six with the community versions first and check nothing downstream breaks, then work on the three. I'll open a PR against tlaplus/Examples when it holds together, or come back here if I get stuck on the Sum lemmas.

[muenchnerkindl]

There are some lemmas about sums in FiniteSetsExtTheorems, they may help.

[vasilisnasopoulos]

FiniteSetsExtTheorems was exactly the missing piece — thank you.

The FoldFunctionOnSet* family imports cleanly from FunctionTheorems, but the two Sum lemmas that iterate and split (SumIterate, SumUnion) would not go through: TLAPS could not instantiate the second-order op(_,_) against the LAMBDA x1, x2 : x1 + x2 in Sum. MapThenSumSet takes a unary op(_), which sidesteps that entirely, and unfolding the definitions makes Sum(f, S) and MapThenSumSet(LAMBDA i : f[i], S) the same term. MapThenSumSetAddElement and MapThenSumSetDisjointUnion then apply directly.

Result on EWD998_proof.tla, with tlapm 1.6.0-pre:

	before	after
lemmas stated without proof	9	0
--strict exit	11	0
obligations	807	851, all proved

One thing worth flagging: the module's local copy of Functions.tla predates SumFunctionOnSet, which FunctionTheorems needs, so it has to be refreshed from the community version. The community copy is a strict superset — nothing defined locally is missing from it — but it does mean the PR touches that file too.

AsyncTerminationDetection_proof is unaffected (exit 0, 30 obligations). EWD998PCal_proof fails for me with Unknown module "BagsExt" both before and after the change, so that looks like my include path rather than anything I touched.

Opening a PR against tlaplus/Examples now.