proof: expose helper IR mapping-write slot-safety seam#2132
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot 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_54329f69-ac41-447d-af02-96160069b791) |
# Conflicts: # PrintAxioms.lean
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot 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_2e9f6f59-d03d-48c4-acd0-6d2ac3152c4a) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 4 finding(s) · 3 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 3 Lean file(s), 129 changed supported line(s). Scout model ranked 4/6 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
Warnings
OCR pilot metrics
Packet coverage
Pilot mode: advisory only. Codex Review remains the merge gate. Inline findings that could not be posted
|
|
Codex Review: Didn't find any major issues. Swish! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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: # PrintAxioms.lean
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot 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_83c6d31e-66ed-47a6-a8aa-046e37c63d49) |
|
Codex Review: Didn't find any major issues. You're on a roll. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: success · Mode: medium-lean · 0 finding(s) · 4 files · 175482 tokens · 25 tool calls
No comments generated. Looks good to me.
OCR pilot metrics
- Routing: medium-lean (router-v8)
- Changed files: 4 supported / 4 total; Lean 2, trust docs 0, workflow/scripts 2, contracts 0, docs 0
- Changed lines: 49 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 4; tokens 175482; tool calls 25; warnings 0; duration 272s
- Largest changed files: Compiler/Proofs/IRGeneration/Contract.lean (+36/-0), scripts/generate_layer2_boundary_catalog.py (+8/-0), PrintAxioms.lean (+2/-1), artifacts/layer2_boundary_catalog.json (+2/-0)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
@codex review |
|
Codex Review: Didn't find any major issues. Can't wait for the next one! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
| \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``` |
# Conflicts: # PrintAxioms.lean
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot 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_4b59e1e2-7e98-4dfd-afba-acb5c617c610) |
|
@codex review |
|
Codex Review: Didn't find any major issues. 👍 Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: success · Mode: medium-lean · 0 finding(s) · 4 files · 146004 tokens · 23 tool calls
No comments generated. Looks good to me.
OCR pilot metrics
- Routing: medium-lean (router-v8)
- Changed files: 4 supported / 4 total; Lean 2, trust docs 0, workflow/scripts 2, contracts 0, docs 0
- Changed lines: 49 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 4; tokens 146004; tool calls 23; warnings 0; duration 303s
- Largest changed files: Compiler/Proofs/IRGeneration/Contract.lean (+36/-0), scripts/generate_layer2_boundary_catalog.py (+8/-0), PrintAxioms.lean (+2/-1), artifacts/layer2_boundary_catalog.json (+2/-0)
Pilot mode: advisory only. Codex Review remains the merge gate.
1 participant
Summary
compile_preserves_semantics_except_mapping_writes_and_helper_ir_globalSlotSafety, a helper-IR mapping-write whole-contract seam using the existing global slot-safety hypotheses.PrintAxioms.leanand records both mapping-write helper-IR variants in the Layer 2 boundary catalog.Base
origin/mainafter proof: retarget whole-contract helper IR from core output #2126 was merged.Validation
lean-slot lake env lean Compiler/Proofs/IRGeneration/Contract.leanlean-slotfell back to local validation and passed.python3 scripts/generate_layer2_boundary_catalog.py --checkpython3 scripts/generate_print_axioms.py --checkpython3 scripts/lean_lint.py --only axiomsgit diff --checkNotes
sorry,admit, or project-levelaxiom.Note
Low Risk
Lean proof and catalog/axiom inventory updates only; no runtime compiler behavior or trusted axioms added.
Overview
Adds
compile_preserves_semantics_except_mapping_writes_and_helper_ir_globalSlotSafety, a whole-contract Tier 2 wrapper that matches the existing mapping-write semantics theorem but usesSupportedStmtListMappingWriteSlotSafety(global slot safety) and concludes overinterpretIRWithInternalswhen a conservative-extension equality tointerpretIRis assumed.The proof is a thin
simpaovercompile_preserves_semantics_except_mapping_writes, parallel to the per-statement..._and_helper_irvariant that still uses per-functionStmtMappingWriteSlotSafeobligations.PrintAxioms.leanlists the new theorem (public count 3888→3889). The Layer 2 boundary catalog generator andartifacts/layer2_boundary_catalog.jsonnow name both mapping-write helper-IR theorem variants for tooling and reviewers.Reviewed by Cursor Bugbot for commit fc860c4. Bugbot is set up for automated code reviews on this repo. Configure here.