Lean definitions and proofs for Pact processes, inferred types, constructor automata, compatibility, and inferred-type optimality.
For artifact reviewers, Updates since submission summarizes the main updates relative to the submitted paper.
This mechanization is part of the POPL 2027 artifact, archived on Zenodo: 10.5281/zenodo.23301148.
PactSafety proves inference/checking soundness, type-automaton correspondence, process simulation and readiness agreement, log-objective regularity, game reduction, compatibility soundness, and inferred-type optimality. Results and proofs lists their precise statements, explicit premises, and supporting proof chains.
Compatibility soundness requires equal process/type fair-choice and progress IDs. Optimality also requires equal message alphabets componentwise. Complexity and algorithmic decidability claims are not formalized.
| Module | Contents |
|---|---|
| Base, Alphabet | Identifiers, message actions, and alphabets |
| Proc, PactSemantics | Processes, evaluation, transitions, and offers |
| PactTypes | Type semantics, compilation, and correspondence |
| ProofHelpers | Inference, strategies, monitors, refinement, and compatibility |
| PactSafetyStructures | Correspondence witnesses and finite paths |
| PactSafety | Public results |
Use the toolchain pinned in lean-toolchain:
lake build
lake env lean ProofAudit.leanProofAudit checks the public results' axiom dependencies.
They use only propext, Classical.choice, and Quot.sound.
Declaration comments describe their result in one or two lines. Module READMEs
describe the current development; status.md and HANDOFF.md hold work records.