proofs: continue reducing sorry cleanly (next pass 3)#1659
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: af2329d7b0
ℹ️ 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".
| "SimpleToken": 61 | ||
| }, | ||
| "proven": 154, | ||
| "proven": 155, |
There was a problem hiding this comment.
This generated artifact is still stale after the proof reduction. scripts/verification_metrics.py derives theorems.proven as total - sorry_count, so with total = 277 and proofs.sorry = 121 the value here should be 156, not 155. As committed, python3 scripts/generate_verification_status.py --check exits with Stale verification artifact, so the repository no longer passes the verification-metrics sync check.
Useful? React with 👍 / 👎.
| #print axioms Compiler.Proofs.IRGeneration.FunctionBody.eval_compileExpr_logicalNot_of_compiled | ||
| -- #print axioms Compiler.Proofs.IRGeneration.FunctionBody.eval_compileExpr_logicalAnd_of_compiled -- sorry'd | ||
| #print axioms Compiler.Proofs.IRGeneration.FunctionBody.eval_compileExpr_logicalAnd_of_compiled | ||
| -- #print axioms Compiler.Proofs.IRGeneration.FunctionBody.eval_compileExpr_logicalOr_of_compiled -- sorry'd |
There was a problem hiding this comment.
After this commit, Compiler.Proofs.IRGeneration.FunctionBody.eval_compileExpr_logicalOr_of_compiled is no longer sorry'd, but PrintAxioms.lean still leaves it commented out here as -- sorry'd. That makes the generated axiom audit stale: python3 scripts/generate_print_axioms.py --check now fails, and #print axioms is skipped for the newly discharged theorem until this file is regenerated.
Useful? React with 👍 / 👎.
| \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``` |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 595eae5a45
ℹ️ 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".
| "SimpleToken": 61 | ||
| }, | ||
| "proven": 154, | ||
| "proven": 156, |
There was a problem hiding this comment.
Fresh evidence on this revision: Compiler/Proofs/IRGeneration/FunctionBody.lean:1663-1691 also discharges eval_compileExpr_ge_of_compiled, so scripts/verification_metrics.py now computes theorems.proven = 157. Leaving this artifact at 156 makes python3 scripts/generate_verification_status.py --check fail on the commit, so the verification-metrics sync check is still broken.
Useful? React with 👍 / 👎.
| #print axioms Compiler.Proofs.YulGeneration.ir_yul_function_equiv_from_state_of_stmt_equiv_and_adequacy | ||
| #print axioms Compiler.Proofs.YulGeneration.ir_yul_function_equiv_from_state_of_stmt_equiv | ||
| -- Total: 1723 theorems/lemmas (1130 public, 545 private, 48 sorry'd) | ||
| -- Total: 1723 theorems/lemmas (1132 public, 545 private, 46 sorry'd) |
There was a problem hiding this comment.
Fresh evidence on this revision: eval_compileExpr_ge_of_compiled is no longer sorry'd in Compiler/Proofs/IRGeneration/FunctionBody.lean:1663-1691, but this generated footer still counts only 1132 public / 46 sorry'd. python3 scripts/generate_print_axioms.py --check fails because PrintAxioms.lean still omits #print axioms Compiler.Proofs.IRGeneration.FunctionBody.eval_compileExpr_ge_of_compiled and the totals are one theorem short.
Useful? React with 👍 / 👎.
…ss 3 The ge/le/div/sub/mod compiled-expression proofs follow the same mechanical case-split pattern as the already-allowlisted logicalAnd and logicalOr proofs. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace the sorry in the mutual-block theorem evalExpr_lt_evmModulus_core_onExpr with a complete proof by induction on ExprCompileCore. Each case unfolds evalExpr via `show (do ...)` and dispatches with Uint256.isLt (arithmetic ops), boolWord_lt_evmModulus (comparisons/booleans), or Nat.lt_trans for Address fields. Uses @-pattern matching to bind implicit expression sub-terms in the mutual induction. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: bd4dfad9ec
ℹ️ 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".
| {fn : FunctionSpec} | ||
| (hBody : SupportedBodyInterface spec fn) | ||
| (hnoConflict : firstFieldWriteSlotConflict spec.fields = none) : | ||
| StmtListHelperFreeStepInterface spec.fields (fn.params.map (·.name)) fn.body := by sorry | ||
| StmtListHelperFreeStepInterface spec.fields (fn.params.map (·.name)) fn.body := by |
There was a problem hiding this comment.
This commit turns SupportedBodyInterface.helperFreeStepInterface into a concrete proof, but python3 scripts/check_proof_length.py now fails with SupportedBodyInterface (54 lines, limit 50) because the theorem exceeds the hard limit and is not in the allowlist. I verified the parent commit (be667d0cdecb901bb51f7c1a9b81c683e2ff6cb5) passes the same check, so this is a new regression introduced here and will keep proof-length-gated verification runs red until the proof is decomposed or explicitly allowlisted.
Useful? React with 👍 / 👎.
…ricInduction case exhaustiveness - Replace broken `duper [hlist]` with `exact hlist` in SupportedSpec.lean (the hypothesis already proves the goal directly) - Fix `| stmt =>` catch-all in GenericInduction.lean that became invalid after new Stmt constructors were added (ecm, setMappingChain, etc.) - Enumerate all Stmt constructors explicitly in the cases tactic - Add bind/Except.bind simplification for do-notation desugaring in setMapping and setMappingUint branches - Sorry 6 mapping-related constructor cases (setMappingWord, setMappingPackedWord, setMapping2Word, setMappingChain, setStructMember, setStructMember2) that need specialized proofs Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Prove the setMappingWord constructor case in legacyCompatibleExternalStmtList_of_compileStmt_ok_on_supportedContractSurface_exceptMappingWrites using the same do-notation desugaring strategy as setMapping/setMappingUint. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add legacyCompatibleExternalStmtList_of_mapping2WordCompatBlock and legacyCompatibleExternalStmtList_of_compileSetMapping2Word_ok helper theorems, then prove the setMapping2Word constructor case in the except-mapping-writes legacy compatibility theorem. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…s in legacy compatibility theorem Adds helper theorems for the remaining mapping-write constructors: - legacyCompatibleExternalStmtList_of_mapLetStmts: general helper for mapped let_ stmts - legacyCompatibleExternalStmtList_of_compileSetMappingChain_ok: chain mapping writes - legacyCompatibleExternalStmtList_of_compileMappingPackedSlotWrite_ok: packed slot writes - legacyCompatibleExternalStmtList_of_compileSetStructMember_ok: struct member writes Reduces sorry count by 3 in the main legacy compatibility theorem. Only setStructMember2 remains as sorry in this section. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0c7fc56757
ℹ️ 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".
| {fn : FunctionSpec} | ||
| (hBody : SupportedBodyInterface spec fn) | ||
| (hnoConflict : firstFieldWriteSlotConflict spec.fields = none) : |
There was a problem hiding this comment.
This theorem now spans 54 lines, exceeding the 50-line hard limit enforced by scripts/check_proof_length.py; running that checker on this commit reports SupportedBodyInterface (54 lines, limit 50) and exits non-zero. Because the proof-length gate is part of verification, this change introduces a CI failure until the proof is decomposed or this theorem is explicitly added to ALLOWLIST with justification.
Useful? React with 👍 / 👎.
Make compilePackedStorageWrite and compileCompatPackedStorageWrites non-private so they can be referenced in proofs from other modules. Add helper theorems for mapped expr/block statements and complete all four sub-cases (single/multi × packed/unpacked) of the setStructMember2 compilation proof. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d93c2a3d34
ℹ️ 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".
| · simp [hkey, hvalue] at hcompile | ||
| exact legacyCompatibleExternalStmtList_of_compileMappingPackedSlotWrite_ok hcompile | ||
|
|
||
| private theorem legacyCompatibleExternalStmtList_of_compileSetStructMember2_ok |
There was a problem hiding this comment.
Running python3 scripts/check_proof_length.py on this commit fails with legacyCompatibleExternalStmtList_of_compileSetStructMember2_ok (89 lines, limit 50) because this newly added theorem exceeds HARD_LIMIT and has no ALLOWLIST entry. The parent commit (be667d0) passes the same check, so this commit introduces a new proof-length gate failure; the proof should be decomposed or explicitly allowlisted with justification.
Useful? React with 👍 / 👎.
Uncomment and fix proofs for compiledStmtStepWithHelpersAndHelperIR_internalCallAssign and compiledStmtStepWithHelpersAndHelperIR_internalCall. Fix variable naming after subst (argExprs -> argExprs'), remove extraneous omega, and use direct rw+exact approach for existential witnesses. Reduces sorry count from 54 to 52. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Uncomment and restore proven proofs for: - stmtTouchesUnsupportedContractSurface_of_stmtListTouchesUnsupportedContractSurface_append_cons - stmtListScopeDiscipline_of_validateFunctionIdentifierReferences_prefix - stmtListTouchesUnsupportedContractSurface_append - stmtListGenericCore_append These were previously commented out with TYPESIG_SORRY markers. The stmtListGenericCore_append theorem is particularly important as it unblocks the require clause family of theorems. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Restore both TYPESIG_SORRY'd theorems with complete proofs using the proven FunctionBody helpers (execIRStmts_compiled_stop/return). Key technique: structural sizeOf decomposition for fuel bounds with free variables, eval_compileExpr_core_of_scope for evalExpr totality. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f898232e0d
ℹ️ 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".
| -- SORRY'D: (FunctionBody.execIRStmts_compiled_stop_core_append_wholeFuel | ||
| -- SORRY'D: (state := state) (tailIR := []) (extraFuel := wholeExtraFuel)) | ||
| -- SORRY'D: · simpa [stmtStepMatchesIRExec, stmtNextScope, collectStmtNames] using hruntime | ||
| theorem compiledStmtStep_return |
There was a problem hiding this comment.
compiledStmtStep_return is newly expanded to 62 lines, but scripts/check_proof_length.py does not add it to ALLOWLIST, so the proof-length gate now fails on this commit (... compiledStmtStep_return (62 lines, limit 50)). I validated this is introduced here by running the checker on the parent commit (be667d0), which passes, while this commit fails. Because .github/workflows/verify.yml runs this checker in the Generate proof length report step, CI will stay red until this theorem is decomposed or explicitly allowlisted with justification.
Useful? React with 👍 / 👎.
These were TYPESIG_SORRY'd due to the Option Nat migration in evalExpr. Proved directly in GenericInduction.lean by using eval_compileExpr_core_of_scope to extract the Nat value, then establishing all post-state invariants. Still 52 sorry warnings (these theorems weren't in the warning count). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5fa3508e86
ℹ️ 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".
| · left; right; right; exact hassign | ||
| · right; exact hfield | ||
|
|
||
| theorem compiledStmtStep_letVar |
There was a problem hiding this comment.
This theorem now spans 93 lines, exceeding the 50-line hard limit enforced by scripts/check_proof_length.py; running that checker on 56806cd reports compiledStmtStep_letVar (93 lines, limit 50) and exits non-zero. I also checked the parent commit (be667d0), where the same checker passes, so this regression is introduced here and will keep verification red because .github/workflows/verify.yml runs the proof-length check in the Generate proof length report step.
Useful? React with 👍 / 👎.
| · simp [stmtStepMatchesIRExec] | ||
| exact ⟨hruntime', hexact', hbounded', hscope'⟩ | ||
|
|
||
| theorem compiledStmtStep_assignVar |
There was a problem hiding this comment.
This proof is 147 lines long, so python3 scripts/check_proof_length.py fails on this commit with compiledStmtStep_assignVar (147 lines, limit 50) because there is no allowlist entry for it. The parent commit (be667d0) passes the same check, which makes this a new CI-breaking regression introduced by this change; the workflow executes this gate in .github/workflows/verify.yml under Generate proof length report.
Useful? React with 👍 / 👎.
Uncomment two TYPESIG_SORRY theorems in FunctionBody.lean with corrected type signatures (split Option Nat condition into explicit evalExpr=some and Nat!=0 hypotheses to fix OfNat (Option Nat) 0 synthesis failure from the Option migration). Both proofs use the already-proven execStmtList_terminal_core_not_continue lemma. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e9665356cb
ℹ️ 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".
| -- SORRY'D: (scope := scope) | ||
| -- SORRY'D: (stmts := elseBranch) | ||
| -- SORRY'D: helse next helseExec | ||
| theorem execStmtList_terminal_core_ite_else_eq |
There was a problem hiding this comment.
This commit introduces execStmtList_terminal_core_ite_else_eq as a 356-line proof, but scripts/check_proof_length.py still enforces a 50-line hard limit for non-allowlisted theorems, so the proof-length gate now fails on this revision (python3 scripts/check_proof_length.py reports this theorem as over limit; parent commit be667d0 passes). Because .github/workflows/verify.yml runs this checker in the Generate proof length report step, CI remains red until this proof is decomposed or explicitly added to ALLOWLIST with justification.
Useful? React with 👍 / 👎.
The sorry-reduction pass 3 (PR #1659) introduced several newly proven theorems that exceed the 50-line proof-length limit but were not added to the ALLOWLIST in check_proof_length.py, breaking CI after merge. Theorems added: - compiledStmtStep_letVar (93 lines) - compiledStmtStep_assignVar (147 lines) - compiledStmtStep_return (62 lines) - execStmtList_terminal_core_ite_else_eq (356 lines) - SupportedBodyInterface (54 lines) - legacyCompatibleExternalStmtList_of_compileSetStructMember2_ok (89 lines) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
* fix: allowlist 6 proof-length violations from PR #1659 The sorry-reduction pass 3 (PR #1659) introduced several newly proven theorems that exceed the 50-line proof-length limit but were not added to the ALLOWLIST in check_proof_length.py, breaking CI after merge. Theorems added: - compiledStmtStep_letVar (93 lines) - compiledStmtStep_assignVar (147 lines) - compiledStmtStep_return (62 lines) - execStmtList_terminal_core_ite_else_eq (356 lines) - SupportedBodyInterface (54 lines) - legacyCompatibleExternalStmtList_of_compileSetStructMember2_ok (89 lines) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Prove stmtResultMatchesIRExec_compiled_terminal_ite_then and _else Write corrected versions of these theorems that split the condition hypothesis into separate hcondEval/hcondTrue (or hcondFalse) parts, avoiding the OfNat (Option Nat) 0 type error. The proofs use the already-proven execStmtList_terminal_core_ite_{then,else}_eq, stmtResultMatchesIRExec_ir_not_continue_of_terminal_core, and execIRStmts_compiled_terminal_ite_{then,else}_of_irExec helpers. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * chore: auto-refresh derived artifacts * Prove eval_compileRequireFailCond_core_onExpr Proves that compileRequireFailCond produces correct IR for all ExprCompileCore cases. For ge/le expressions, the compilation produces lt/gt IR ops respectively, with correctness shown via case analysis on the comparison predicate. For all other expression types, the proof uses iszero(compileExpr) via a shared helper. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Prove exec_compileStmtList_core with proper Option Nat handling Replaces the sorry in exec_compileStmtList_core with a complete proof handling all 6 StmtListCompileCore cases (nil, letVar, assignVar, require_, return_, stop). The key change from the previously sorry'd code is proper handling of evalExpr returning Option Nat: each case that uses evalExpr first establishes the result is some via eval_compileExpr_core, then case-splits to extract the Nat value. The require_ case uses eval_compileRequireFailCond_core_onExpr (proven in the previous commit) instead of the broken eval_compileRequireFailCond_core whose type signature had = 0 instead of = some 0 for Option Nat. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Prove eval_compileRequireFailCond_core_of_scope (corrected) Adds the scope-based variant of eval_compileRequireFailCond that uses the corrected = some 0 conclusion (instead of the broken = 0 in the TYPESIG_SORRY). Delegates to eval_compileRequireFailCond_core_onExpr via bindingsExactlyMatchIRVarsOnScope_implies_onExpr, following the same pattern as eval_compileExpr_core_of_scope. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Prove exec_compileStmtList_core_extraFuel (remove sorry) Adapts the exec_compileStmtList_core proof to the extraFuel variant by threading extraFuel through all fuel arithmetic. Uses the Option-Nat-correct patterns (rcases on evalIRExpr, eval_compileRequireFailCond_core_onExpr) and the _extraFuel helper lemmas for execIRStmts cons/revert/return. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * fix: disambiguate allowlist entries by capturing dotted theorem names Update THEOREM_RE regex to capture full dot-separated Lean theorem names (e.g. SupportedBodyInterface.helperFreeStepInterface) instead of only the prefix before the first dot. Replace ambiguous allowlist entries with their specific dotted names so each entry targets exactly one proof. Addresses Codex review comment on PR #1668. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Prove exec_compileStmtList_terminal_core_sizeOf_extraFuel (remove last sorry in FunctionBody.lean) Complete proof of the terminal statement list compilation theorem covering all StmtListTerminalCore cases: letVar, assignVar, require_ (pass/fail), return_, stop, and ite (then/else branches). The ITE case required careful fuel arithmetic using sizeOf_spec lemmas with an intermediate subtraction elimination technique to work around omega's limitations with Nat subtraction over many variables. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Prove compiledStmtStep_ite: terminal ITE statement compilation correctness Eliminates one sorry from GenericInduction.lean (49 → 48 sorry warnings). Proves that compiling an ITE statement with terminal branches produces correct IR by bridging source-level execStmt with IR-level block execution via stmtResultMatchesIRExec_compiled_terminal_ite_{then,else}. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove compiledStmtStep_require (was TYPESIG_SORRY) Prove the compilation-step theorem for `require` statements by following the pattern from `compiledStmtStep_letVar`. The key insight is that for `ExprCompileCore` conditions, `collectExprNames` only contains variable names (not storage field names), so `scopeNamesPresent (stmtNextScope ...)` can be proved via `scopeNamesPresent_of_included`. Also make `execIRStmts_revertWithMessage_revert` non-private so it can be used cross-file. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * prove stmtListGenericCore_of_{CompileCore,TerminalCore}_of_scopeNamesIncluded Prove both scope-weakening conversion theorems that convert StmtListCompileCore/StmtListTerminalCore proofs into StmtListGenericCore. This eliminates 2 active sorries (48 → 46). Key additions: - scopeNamesIncluded_cons: scope inclusion lifts through cons - stmtListCompileCore_of_scopeNamesIncluded: CompileCore scope weakening - stmtListTerminalCore_of_scopeNamesIncluded: TerminalCore scope weakening These were blocked on compiledStmtStep_require (proven in previous commit) and compiledStmtStep_ite (proven earlier). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * chore: regenerate PrintAxioms.lean and derived artifacts - Regenerate PrintAxioms.lean to reflect visibility/sorry changes: execIRStmts_revertWithMessage_revert (private -> public), exec_compileStmtList_core and _extraFuel (sorry -> proven), exec_compileStmtList_terminal_core_sizeOf_extraFuel (sorry -> proven), compiledStmtStep_ite (sorry -> proven), plus new public theorems. - Update verification_status.json, VERIFICATION_STATUS.md, and check_lean_hygiene.py sorry count (52 -> 46). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude <claude@anthropic.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
2 participants
Summary
next pass 2branchVerification
Note
Low Risk
Primarily proof refactors and sorry-elimination around
Option-valued expression evaluation; core compilation/runtime behavior is unchanged, aside from making two storage-write helpers public and tightening a transient-storage lemma precondition.Overview
Continues the Option-migration proof cleanup by replacing multiple
sorryblocks inCompiler/Proofs/IRGeneration/FunctionBody.leanwith explicit case splits onSourceSemantics.evalExpr/evalIRExprand new helper lemmas, covering comparisons, boolean ops, arithmetic, statement execution (letVar/assignVar/return), terminal statement lists, and source-vs-IR result matching.Adds a set of stepping/bridge lemmas in
CompilationModel/Types.lean(including standalone “CopyFrom” versions) andLayoutValidation.leanto make recursive field/slot search and slot-conflict detection usable from other proof modules. Also exposescompilePackedStorageWriteandcompileCompatPackedStorageWrites(previouslyprivate) for reuse in proofs/compilation code.Written by Cursor Bugbot for commit 4009f02. This will update automatically on new commits. Configure here.