proof: discharge legacy compatibility for core statement lists by Th0rgal · Pull Request #2134 · lfglabs-dev/verity

Th0rgal · 2026-07-09T18:45:27Z

Summary

Discharges StmtListCompiledLegacyCompatible for the generic StmtListCompileCore grammar.
Adds terminal-core coverage via stmtListTerminalCore_compiledLegacyCompatible, including terminal ite bodies by reusing the proof: reduce whole-contract legacy-bodies premise to per-statement interface #2128 list bridge on compiled branches.
Packages function-level entrypoints for compile-core and terminal-core bodies: compileFunctionSpec_body_legacyCompatible_of_compileCore and compileFunctionSpec_body_legacyCompatible_of_terminalCore.
Regenerates PrintAxioms.lean and documents the two mechanical structural witnesses in the proof-length allowlist.

Stack / dependency

Base/target: paloma/parallel-fallback-fragment-helper (#2128).

Do not merge until predecessor stack is merged/green.

Validation

git diff --check PASS
lean-slot lake build Compiler.Proofs.IRGeneration.Function PASS (local fallback after Spark offload 403 for this isolated worktree path)
lean-slot lake build Compiler.Proofs.IRGeneration.Contract PASS (local fallback after Spark offload 403 for this isolated worktree path)
python3 scripts/generate_print_axioms.py --check PASS
python3 scripts/check_proof_length.py PASS
rg -n "\\b(sorry|admit|axiom)\\b" Compiler/Proofs/IRGeneration/Function.lean PASS (no matches)

Refs #2080

Note

Low Risk
Changes are confined to Lean proofs and axiom inventory; no compiler runtime or security-sensitive execution paths are modified.

Overview
Advances #2080 by proving that bodies in the StmtListCompileCore and StmtListTerminalCore grammars satisfy StmtListCompiledLegacyCompatible, so compiled Yul stays in the legacy-compatible external subset without hand-written per-statement witnesses.

Adds structural lemmas (legacyCompatibleExternalStmtList_map_exprStmt, revertWithMessage_legacyCompatible) and large inductive theorems stmtListCompileCore_compiledLegacyCompatible and stmtListTerminalCore_compiledLegacyCompatible (per-constructor cases aligned with compilation, including terminal ite via the existing list bridge). Two function-level corollaries—compileFunctionSpec_body_legacyCompatible_of_compileCore and ..._of_terminalCore—compose param loads with those list proofs.

PrintAxioms.lean is regenerated to export the new public theorems; check_proof_length.py allowlists the two mechanical structural witnesses.

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

Add the missing legacy-compatibility analog of the proven disjoint composition: - compileStmtList_legacyCompatible_of_interface: lift the per-statement StmtListCompiledLegacyCompatible interface to a whole-list LegacyCompatibleExternalStmtList witness for the emitted Yul body. - compileFunctionSpec_body_legacyCompatible_of_interface: per-function bridge composing genParamLoads_scalar_legacy with the body lemma. These lift the remaining per-statement #2080 legacy obligations toward the whole-contract LegacyCompatibleExternalBodies target.

…om per-statement interface

… interface

vercel · 2026-07-09T18:45:33Z

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:25pm

cursor · 2026-07-09T18:45:40Z

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_669a7391-2266-4231-bad9-5ef8e1a43062)

github-actions · 2026-07-09T19:08:10Z

OpenCodeReview first-pass review

Status: completed_with_errors · 0 finding(s) · 3 files · 1245669 tokens · 70 tool calls

Some files could not be reviewed due to errors.

⚠️ 2 OCR warning(s) reported.

Warnings

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

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 · 2026-07-10T16:15:27Z

@codex review

chatgpt-codex-connector · 2026-07-10T16:18:22Z

Codex Review: Didn't find any major issues. 🎉

Reviewed commit: 3ecf90daa0

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

# Conflicts: # Compiler/Proofs/IRGeneration/Function.lean # PrintAxioms.lean

cursor · 2026-07-10T16:25:42Z

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_ccff9e95-42b4-4895-94b9-d1dfa7c22f40)

Th0rgal · 2026-07-10T16:25:47Z

@codex review

chatgpt-codex-connector · 2026-07-10T16:29:33Z

Codex Review: Didn't find any major issues. What shall we delve into next?

Reviewed commit: 2e54ef9906

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

github-actions · 2026-07-10T17:06:11Z

OpenCodeReview first-pass review

Status: completed_with_errors · Mode: medium-lean · 0 finding(s) · 3 files · 761103 tokens · 57 tool calls

Some files could not be reviewed due to errors.

⚠️ 2 OCR warning(s) reported.

Warnings

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

OCR pilot metrics

Routing: medium-lean (router-v8)
Changed files: 3 supported / 3 total; Lean 2, trust docs 0, workflow/scripts 1, contracts 0, docs 0
Changed lines: 289 supported; thresholds large Lean >=3 files or >800 lines
OCR: status completed_with_errors; comments 0; files 3; tokens 761103; tool calls 57; warnings 2; duration 1520s
Largest changed files: Compiler/Proofs/IRGeneration/Function.lean (+275/-0), PrintAxioms.lean (+7/-1), scripts/check_proof_length.py (+6/-0)

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 and others added 5 commits July 9, 2026 11:50

proof: bridge compiled contract bodies to legacy-compatible subset fr…

4c01aa0

…om per-statement interface

proof: whole-contract retarget theorem stated on per-statement legacy…

1bea5de

… interface

chore: auto-refresh derived artifacts

64a61de

proof: discharge legacy compatibility for core statement lists

3ecf90d

This was referenced Jul 10, 2026

proof: legacy compatibility for storage mapping singletons #2141

Merged

proof: package legacy compatibility for mapping-chain writes #2143

Merged

proof: package legacy compatibility for mapping2word writes #2145

Merged

Th0rgal mentioned this pull request Jul 10, 2026

proof: package legacy compatibility for struct member2 writes #2146

Merged

Th0rgal changed the base branch from paloma/parallel-fallback-fragment-helper to main July 10, 2026 16:19

Merge remote-tracking branch 'origin/main' into HEAD

2e54ef9

# Conflicts: # Compiler/Proofs/IRGeneration/Function.lean # PrintAxioms.lean

vercel Bot deployed to Preview July 10, 2026 16:25 View deployment

Th0rgal merged commit 54e98c0 into main Jul 10, 2026
22 checks passed

Th0rgal mentioned this pull request Jul 10, 2026

proof: package direct helper statement context bridge #2147

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

proof: discharge legacy compatibility for core statement lists - #2134

proof: discharge legacy compatibility for core statement lists#2134
Th0rgal merged 6 commits into
mainfrom
paloma/issue-2080-legacy-compatible-stmt-phase31

Th0rgal commented Jul 9, 2026 •

edited by cursor Bot

Loading

Uh oh!

vercel Bot commented Jul 9, 2026 •

edited

Loading

Uh oh!

cursor Bot commented Jul 9, 2026

Uh oh!

github-actions Bot commented Jul 9, 2026

Uh oh!

Th0rgal commented Jul 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Jul 10, 2026

Uh oh!

cursor Bot commented Jul 10, 2026

Uh oh!

Th0rgal commented Jul 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Jul 10, 2026

Uh oh!

github-actions Bot commented Jul 10, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

Th0rgal commented Jul 9, 2026 • edited by cursor Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Stack / dependency

Validation

Uh oh!

vercel Bot commented Jul 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

cursor Bot commented Jul 9, 2026

Bugbot couldn't run - usage limit reached

Uh oh!

github-actions Bot commented Jul 9, 2026

OpenCodeReview first-pass review

Warnings

Uh oh!

Th0rgal commented Jul 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Jul 10, 2026

Uh oh!

cursor Bot commented Jul 10, 2026

Bugbot couldn't run - usage limit reached

Uh oh!

Th0rgal commented Jul 10, 2026

Uh oh!

chatgpt-codex-connector Bot commented Jul 10, 2026

Uh oh!

github-actions Bot commented Jul 10, 2026

OpenCodeReview first-pass review

Warnings

OCR pilot metrics

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Th0rgal commented Jul 9, 2026 •

edited by cursor Bot

Loading

vercel Bot commented Jul 9, 2026 •

edited

Loading