proof: package legacy compatibility for mapping2word writes

[Th0rgal]

Summary

• Adds a structural legacy-compatible proof for CompilationModel.compileSetMapping2Word over singleton ordinary two-key mapping word writes.
• Packages StmtListCompiledLegacyCompatible for [Stmt.setMapping2Word ...].
• Regenerates PrintAxioms.lean audit entries/counts.

Base / dependencies

• Base/target: paloma/issue-2080-mapping-chain-phase33 (proof: package legacy compatibility for mapping-chain writes #2143), which is open, clean, and green at inspection time.
• Depends on proof: package legacy compatibility for mapping-chain writes #2143 and inherited stack proof: legacy compatibility for storage mapping singletons #2141, proof: discharge legacy compatibility for core statement lists #2134, and proof: reduce whole-contract legacy-bodies premise to per-statement interface #2128.
• Inspected unrelated proof: expose helper IR mapping-write slot-safety seam #2132 for live status; this PR does not depend on it.

Do not merge until predecessor stack is merged/green.

Validation

• git diff --check passed.
• lean-slot lake build Compiler.Proofs.IRGeneration.Function Compiler.Proofs.IRGeneration.Contract PrintAxioms passed.
• python3 scripts/generate_print_axioms.py --check passed: PrintAxioms.lean is up to date.
• python3 scripts/check_proof_length.py passed: 5811 proofs scanned, no new proofs exceed the 50-line hard limit.
• Confirmed no new sorry, admit, or axiom declarations in touched proof files; rg hits were only PrintAxioms comment/header text.

Refs #2080

---

Note

Low Risk
Proof-only additions with no changes to compilation logic or runtime behavior; risk is limited to formal verification maintenance.

Overview
Extends the IR-generation legacy-compatibility story to setMapping2Word (two-key mapping writes at a word offset), mirroring the existing setMapping2 packaging.

Adds compileSetMapping2Word_legacyCompatible, which case-splits on successful compileSetMapping2Word output and shows the emitted Yul is LegacyCompatibleExternalStmtList, including nested mappingSlot keys and an add when wordOffset ≠ 0, with sstore/tstore chosen from field transience. Adds public stmtList_setMapping2WordSingle_compiledLegacyCompatible so a singleton [Stmt.setMapping2Word …] list is StmtListCompiledLegacyCompatible.

PrintAxioms.lean is refreshed to list the new private helper (commented) and public theorem, with theorem counts 5613 → 5615.

^{Reviewed by Cursor Bugbot for commit 03892e9. 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	Jul 10, 2026 2:54pm

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_d01a3613-a3d4-4d4b-bdf7-664d4e742645)

[github-actions]

OpenCodeReview first-pass review

Status: completed_with_errors · Mode: medium-lean · 0 finding(s) · 2 files · 337963 tokens · 34 tool calls

Some files could not be reviewed due to errors.

⚠️ 1 OCR warning(s) reported.

Warnings

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

OCR pilot metrics

• Routing: medium-lean (router-v8)
• Changed files: 2 supported / 2 total; Lean 2, trust docs 0, workflow/scripts 0, contracts 0, docs 0
• Changed lines: 72 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status completed_with_errors; comments 0; files 2; tokens 337963; tool calls 34; warnings 1; duration 1172s
• Largest changed files: Compiler/Proofs/IRGeneration/Function.lean (+68/-0), PrintAxioms.lean (+3/-1)

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

⚠️ OCR did not complete successfully; this run is intentionally retryable for the same commit.

[Th0rgal]

@codex review

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Chef's kiss.

Reviewed commit: 03892e9bb0

ℹ️ 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".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".