proof: bridge owned resources into frame couplings (#1990)

[Th0rgal]

Short description

Add the smallest reusable bridge that turns one Resource into a supported Coupling, then packages computed footprint disjointness as a SegmentSimWithFields frame theorem.

What changed

• add Coupling.owned, the canonical coupling for one concrete resource observation
• prove Coupling.owned_supported
• add SegmentSimWithFields.frame_owned_writeFootprint, combining coupling support, footprint soundness, and the frame rule without per-consumer support boilerplate
• migrate the existing execStmt_letVar_preserves_selector_calldata proof to the new primitive, providing a concrete existing consumer/regression
• register both public theorems in PrintAxioms.lean

This is proof-only and additive: no interpreter semantics, fragment classification, trust boundary, or gate changes.

Validation

• lake build Compiler.Proofs.Frames — exit 0, Build completed successfully (1207 jobs)
• lean-slot env GIT_CONFIG_GLOBAL=/dev/null lake build — exit 0, Build completed successfully (2476 jobs)
• lean-slot env GIT_CONFIG_GLOBAL=/dev/null lake build PrintAxioms — exit 0, Build completed successfully (2624 jobs)
• make check — exit 0, Ran 666 tests, All checks passed
• python3 scripts/generate_print_axioms.py --check — exit 0
• python3 scripts/generate_trust_surface_report.py --check — exit 0
• git diff --check origin/main...HEAD — exit 0
• changed-Lean forbidden-escape audit plus lean_hygiene — no introduced sorry, admit, axiom, or unsafe; generated registry remains 0 sorry'd

Base: cca73c39a4f49176fc01c570febb31ea891b3898
Head: 09855b85319c451ccc7ccea21e805289017ff8a7

Closes part of #1990.

[vercel]

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

Project	Deployment	Actions	Updated
verity	Ready	Preview	Sep 2, 2026 12:24pm UTC

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-02T12:27:42.838475Z	09855b8	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[github-actions]

OpenCodeReview first-pass review

🔁 Incomplete — this run did not finish and will retry on the same commit. Do not count it as review coverage.

Some files could not be reviewed due to errors.

Warnings

• subtask_error Compiler/Proofs/Frames.lean: LLM completion error: context deadline exceeded

OCR pilot metrics & packet coverage

OCR pilot metrics

• Routing: medium-lean (router-v10)
• Changed files: 2 supported / 2 total; Lean 2, trust docs 0, workflow/scripts 0, contracts 0, docs 0
• Changed lines: 53 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status completed_with_errors; comments 0; files 2; tokens 272707; tool calls 27; warnings 1; duration 1375s
• Largest changed files: Compiler/Proofs/Frames.lean (+40/-9), PrintAxioms.lean (+3/-1)

Pilot mode: advisory only. Codex Review remains the merge gate.