proof: package legacy compatibility for struct member2 writes

[Th0rgal]

Refs #2080

Base / dependency chain

Stacked on #2145 (paloma/issue-2080-mapping2word-phase34, head 03892e9bb00745c2c93a578c86b63ba1ea2c4dd5). Inherited stack:

#2128 -> #2134 -> #2141 -> #2143 -> #2145 -> this PR

Live preflight before editing found #2145 open and healthy; its remaining foundry shard has since completed successfully.

Slice

Packages the next ordinary supported singleton after setMapping2WordSingle in SupportedStmtList: unpacked setStructMember2Single.

Changes:

• Adds compileSetStructMember2_legacyCompatible for the compiler shape emitted by compileSetStructMember2 when the supported witness resolves an unpacked struct member.
• Adds public stmtList_setStructMember2Single_compiledLegacyCompatible producing StmtListCompiledLegacyCompatible fields scope [Stmt.setStructMember2 ...].
• Regenerates PrintAxioms.lean for the added theorem surface.

Event heads were inspected but not selected for this #2080 no-events slice: event support is on the scalar-events proof tier, while the current #2080 legacy body bridge remains over SupportedSpec with noEvents.

Validation

• git diff --check
• lean-slot lake build Compiler.Proofs.IRGeneration.Function
• lean-slot lake build Compiler.Proofs.IRGeneration.Contract
• lean-slot lake build Compiler.Proofs.IRGeneration.Function Compiler.Proofs.IRGeneration.Contract
• python3 scripts/generate_print_axioms.py --check
• python3 scripts/check_proof_length.py
• Verified no added sorry, admit, or axiom declarations in the diff

Remaining #2080 gate

The whole-contract retarget still consumes per-body StmtListCompiledLegacyCompatible obligations and still ultimately depends on retiring SupportedStmtList.helperSurfaceClosed. This PR only closes one more singleton body-shape obligation.

Recommended next slice

Package the next uncovered ordinary supported singleton in the same no-events storage tier, likely setStructMemberSingle or setMappingPackedWordSingle after inspecting exact constructor order and compiler shape. Keep event heads for the scalar-events roadmap unless the #2080 bridge is explicitly widened beyond SupportedSpec.noEvents.

---

Note

Low Risk
Proof-only changes in IR generation lemmas; no compiler runtime or code generation behavior is modified.

Overview
Extends the #2080 legacy Yul bridge with one more supported singleton: a single Stmt.setStructMember2 whose struct member is unpacked (no packed layout).

Adds compileSetStructMember2_legacyCompatible, showing the IR from compileSetStructMember2 in that shape satisfies LegacyCompatibleExternalStmtList—including nested mappingSlot keys and sstore/tstore choice from field transience, reusing the same block-write helper pattern as setMapping2Word.

Adds public stmtList_setStructMember2Single_compiledLegacyCompatible, yielding StmtListCompiledLegacyCompatible for that one-statement list under the usual compile-core and scope hypotheses.

PrintAxioms.lean is regenerated (private helper listed; public theorem exported). Theorem count +2; no new axioms or sorries.

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

[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_b0cc4c78-854f-47c5-9311-80f7cf103fe3)

[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 4:17pm

[github-actions]

OpenCodeReview first-pass review

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

Some files could not be reviewed due to errors.

⚠️ 1 OCR warning(s) reported.

Warnings

• subtask_error PrintAxioms.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: 82 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status completed_with_errors; comments 0; files 2; tokens 471067; tool calls 37; warnings 1; duration 1240s
• Largest changed files: Compiler/Proofs/IRGeneration/Function.lean (+78/-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.

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```

[Th0rgal]

@codex review

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Already looking forward to the next diff.

Reviewed commit: 3d95803aa2

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