fix: allowlist proof-length violations + reduce sorries pass 4#1668
Conversation
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>
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>
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>
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>
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>
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>
![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: c35078017b
ℹ️ 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".
| "compiledStmtStep_assignVar", | ||
| "compiledStmtStep_return", | ||
| "execStmtList_terminal_core_ite_else_eq", | ||
| "SupportedBodyInterface", |
There was a problem hiding this comment.
check_proof_length.py matches allowlist entries against unqualified theorem names (if name in ALLOWLIST), so adding "SupportedBodyInterface" here allowlists all declarations with that identifier, not just the long one in GenericInduction.lean. There are already two other SupportedBodyInterface theorems in Compiler/Proofs/IRGeneration/SupportedSpec.lean; if either grows past 50 lines, CI will now miss that regression. This weakens the hard-limit guard beyond the intended scope of this PR.
Useful? React with 👍 / 👎.
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>
…t 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>
…tness
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 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>
…Included 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>
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
- 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>
Resolve PrintAxioms.lean conflict by regenerating from source. All make check passes. 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: ca0cd4d095
ℹ️ 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".
| THEOREM_RE = re.compile( | ||
| r"^\s*(?P<attrs>(?:@\[[^\]]*\]\s*)*)(?P<visibility>(?:(?:private|protected)\s+)*)" | ||
| r"(?P<kind>theorem|lemma)\s+(?P<name>[A-Za-z_][A-Za-z0-9_']*)\b" | ||
| r"(?P<kind>theorem|lemma)\s+(?P<name>[A-Za-z_][A-Za-z0-9_.']*)\b" |
There was a problem hiding this comment.
Allowing . in theorem identifiers here means manifest extraction can now produce names like Foo.bar, but extract_property_names still relies on PROPERTY_WITH_NUM_RE / PROPERTY_SIMPLE_RE, which only accept [A-Za-z0-9_']+. In that scenario, a test annotation such as /// Property: Foo.bar is ignored, so coverage checks (check_property_coverage.py and verification metrics) will report the theorem as uncovered even when the test exists. Please update the property-tag regexes to accept dotted identifiers so manifest and coverage parsing stay aligned.
Useful? React with 👍 / 👎.
2 participants
Summary
scripts/check_proof_length.pyCI Fix Details
Theorems added to allowlist:
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)Test plan
make checkpasseslake build PrintAxiomspassespython3 scripts/check_proof_length.pypassespython3 scripts/generate_print_axioms.py --checkpassespython3 scripts/generate_verification_status.py --checkpasses🤖 Generated with Claude Code
Note
Low Risk
Mostly proof-only Lean changes plus CI script baseline updates; low runtime risk, but moderate chance of proof-check or tooling regressions if fuel/Option-migration reasoning is incomplete.
Overview
Replaces multiple
sorryplaceholders in Layer-2 IR-generation proofs with full constructive proofs, includingeval_compileRequireFailCond_core_onExpr,exec_compileStmtList_core(_extraFuel), and terminalitebranch-matching lemmas; also exposesexecIRStmts_revertWithMessage_revertfor downstream use.Updates GenericInduction to prove
compiledStmtStep_requireandcompiledStmtStep_ite, adds scope-inclusion helper lemmas, and adjustsPrintAxioms/verification artifacts to reflect fewer remainingsorrys.Fixes CI hygiene tooling by expanding the long-proof allowlist, lowering the expected
sorrybaseline (52→46), and allowing dotted theorem names inproperty_utils.pyregexes.Written by Cursor Bugbot for commit ca0cd4d. This will update automatically on new commits. Configure here.