Coupling invariant frame rules (#1990 part 3/3)

[Th0rgal]

Summary

• Adds the coupling-invariant layer on top of the frame rule and write footprints in Compiler/Proofs/Frames.lean: Coupling (with Inv : RuntimeState → Abs → Prop), SegmentSim, and the generalized SegmentSimWithFields.
• Support-based invariant preservation (Coupling.Supported), composition/weakening (SegmentSim.seq, SegmentSim.weaken, Coupling.supported_and), footprint/frame preservation (SegmentSim.frame, SegmentSim.frame_writeFootprint, SegmentSim.and_frame), and loop lifting (Coupling.iterFrom, SegmentSimWithFields.execForEachLoop_sim, SegmentSim.forEach).
• Registers the new theorems in PrintAxioms.lean (zero new axioms).

Stacked on #2007 (part 2/3) → #2005 (part 1/3). Completes the #1990 surface; downstream consumer is Morpho Blue Proofs/Disciplines.lean local-axiom discharge.

Test plan

• lake build Verity Contracts Compiler PrintAxioms → "Build completed successfully."
• generate_print_axioms.py + refresh_verification_artifacts.sh → [refresh] PASS
• make check → "All checks passed."
• CI green

---

Note

Low Risk
Proof-only additions in compiler frames; no runtime, auth, or data-path changes; registered without new axioms.

Overview
Adds a coupling-invariant layer on top of the existing frame/write-footprint machinery in Compiler/Proofs/Frames.lean, so correctness proofs can relate concrete RuntimeState to abstract models through Coupling (Inv : RuntimeState → Abs → Prop) and segment simulation (SegmentSim / SegmentSimWithFields).

New proof infrastructure includes Coupling.Supported (invariant transport when agreed resources match), Coupling.and / supported_and, abstract loop iteration via Coupling.iterFrom, append lemmas for execStmtList, and compositional rules: id, seq, weaken, frame / frame_writeFootprint, and_frame, plus forEach / execForEachLoop_sim for lifting loop bodies. Thin SegmentSim wrappers specialize the field-aware version to empty fields.

PrintAxioms.lean lists the 21 new theorems (theorem count 5212 → 5233); no new axioms.

^{Reviewed by Cursor Bugbot for commit 67b4767. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jun 12, 2026 7:24pm