You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
* 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>
Copy file name to clipboardExpand all lines: docs/VERIFICATION_STATUS.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -158,7 +158,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
158
158
159
159
**Proof-Only Properties (22 exclusions)**: Internal proof machinery that cannot be tested in Foundry.
160
160
161
-
52`sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules.
161
+
46`sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules.
162
162
These are concentrated in the Layer 2 proof modules (`Compiler/Proofs/IRGeneration/`) due to a definition refactor (PR #1639) that added helper-aware interpreter targets. The theorem statements are structurally sound; the tactic proofs are being repaired. Layer 3 proofs and all contract-level specification proofs are fully discharged.
163
163
164
164
1 documented Lean axiom remains. The Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is tracked as an explicit theorem hypothesis rather than a Lean axiom.
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&size=40){kind=avatar}
0 commit comments