feat(core): storage-lens burn-down — C5 step 2.5 (pre-flip) - #2329
Conversation
Add verity_mixin and verity_contract include so a host imports mixin Lean defs and theorems instead of flattening a copied tree. with and constructor inits bind the mixin Contract values; slot/name clashes fail closed. Ownable + OwnedCounterComposed is the acceptance example. Owned specs now name owner.slot. is Parent flatten is unchanged.
Codex P1s plus storage clash holes: - Expand mixin constructor inits into the host CompilationModel with hygienic argument bindings; merge no longer concatenates mixin ctor bodies (wrong param names / expressions). - Reject duplicate mixin constructor calls and wrong arities. - Run mixin modifiers after ABI/init/role guards so executable order matches the model. - Treat transient and persistent slots as distinct; occupy ADT payload slots; clash on field aliases; merge reserved/alias ranges.
Migrates the raw ContractState storage-channel record-update sites to the lens API: 304 baselined sites -> 63 (39 of which are the lens/bulk-lens/ ofChannels implementations in Verity/Core.lean, the permanent residue the step-3 flip swaps in place). - New Core lenses: writeSlots/modifySlots/writeTransientSlots/ modifyTransientSlots/writeAddrSlots (bulk, shapes definitionally equal to the historical multi-slot raw updates), withStorageChannel (channel transformer for denotational flat-view rebuilds), and the ContractState.ofChannels constructor for harness/fixture full states. - Denote/SourceSemantics write helpers now route through lenses (defeq swaps where the guard shapes matched; withStorageChannel + map lenses for the flat-view mapping writes). - Contract proof suites: post-state record literals in _unfold lemma statements restated as lens chains; verity_frame macro extended with lens unfolds; fixtures rebuilt over defaultState + lens chains. - Gate BASELINE shrunk to 5 files with per-entry justification (Owned/* belongs to the concurrent composition lane; IRState fixture and let-binding false positives documented; the =-guarded dual-channel SourceSemantics writers stay for the step-3 burn-down). No theorem statements changed except lens-form restatements that are definitionally equal to the previous raw-record form.
|
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_12758b22-8a83-4c32-ac73-8d71cc343c41) |
![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
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 54 Lean file(s), 2636 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 62 supported / 68 total; Lean 54, trust docs 0, workflow/scripts 6, contracts 0, docs 2
- Changed lines: 2636 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Verity/Macro/Translate.lean (+400/-12), Contracts/TypedIRTests.lean (+53/-180), Contracts/Ledger/Proofs/Basic.lean (+29/-116), Verity/Specs/Composition.lean (+128/-0), Contracts/Smoke/Include.lean (+126/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
Add verity_mixin and verity_contract include so a host imports mixin Lean defs and theorems instead of flattening a copied tree. with and constructor inits bind the mixin Contract values; slot/name clashes fail closed. Ownable + OwnedCounterComposed is the acceptance example. Owned specs now name owner.slot. is Parent flatten is unchanged.
Codex P1s plus storage clash holes: - Expand mixin constructor inits into the host CompilationModel with hygienic argument bindings; merge no longer concatenates mixin ctor bodies (wrong param names / expressions). - Reject duplicate mixin constructor calls and wrong arities. - Run mixin modifiers after ABI/init/role guards so executable order matches the model. - Treat transient and persistent slots as distinct; occupy ADT payload slots; clash on field aliases; merge reserved/alias ranges.
Validate included modifiers against mixin errors and other mixin declarations. Emit substituted mixin setImmutable statements in the host constructor model so merged immutables initialize. Reject colliding internal helper names at include time instead of failing later in compilation-model validation.
![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: eb46f61204
ℹ️ 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".
| reservedSlotRanges := mixins.flatMap (·.reservedSlotRanges) ++ host.reservedSlotRanges | ||
| slotAliasRanges := mixins.flatMap (·.slotAliasRanges) ++ host.slotAliasRanges | ||
| constructor := host.constructor |
There was a problem hiding this comment.
When an included mixin declares an immutable, this merges the ImmutableSpec but replaces all mixin constructors with host.constructor; the host constructor expansion copies explicit mixin bodies but not the synthesized Stmt.setImmutable statements created for the mixin spec. Consequently validateImmutableInitialization rejects the merged model (and a mixin with an immutable but no explicit constructor leaves the host with no constructor at all). Preserve each mixin's immutable initialization when constructing the host constructor.
Useful? React with 👍 / 👎.
| match field.ty with | ||
| | .scalar (.adt _ maxFields) => maxFields | ||
| | _ => 0 |
There was a problem hiding this comment.
When a mixin or host declares a fixed Uint128 array of at least three elements, this returns only its base slot because .fixedArray falls through to extra := 0. Fixed-array lowering reads and writes baseSlot + index / 2, so a host field at baseSlot + 1 is accepted even though it overlaps the included array; accesses can then silently corrupt each other's compiled EVM storage. Compute the fixed-array span here as well.
Useful? React with 👍 / 👎.
| let translationFields := mixinFields ++ fields | ||
| for fn in functions do | ||
| let fnCmds ← mkFunctionCommandsPublic fields roleDecls errorDecls constDecls immutableDecls externalDecls functions fn | ||
| let fnCmds ← mkFunctionCommandsPublic translationFields roleDecls errorDecls constDecls immutableDecls externalDecls functions fn resolvedIncludes |
There was a problem hiding this comment.
When an included modifier references a custom error, constant, immutable, external, role, or helper function declared by its mixin, the modifier body is later inlined but this call supplies only the host's declaration arrays; only mixin fields were added to translationFields. The standalone mixin is valid, yet model elaboration for a host using the modifier fails with an unknown declaration or cannot translate the expression. Aggregate the relevant mixin declarations or translate the modifier in its original environment.
Useful? React with 👍 / 👎.
| "codebase": { | ||
| "core_lines": 1070, | ||
| "example_contracts": 16 | ||
| "core_lines": 1098, |
There was a problem hiding this comment.
After the 80 added lines in Verity/Core.lean, python3 scripts/generate_verification_status.py --check fails: regeneration changes core_lines from the committed 1098 to 1178. This leaves the published metric stale and causes the repository's freshness check to fail.
Useful? React with 👍 / 👎.
Rebase onto main rebuilt TypedIRCompilerCorrectness against lenses-off default simp. The explicit readSlot/writeSlot simp arguments are now unused and fail the warning baseline.
feat(edsl): verifiable mixin include for proof reuse
|
Note de clôture de session : la validation locale complète n'a pas pu aboutir parce qu'une session concurrente (branche |
First slice of the forEach fragment-admission arc (#2330), building on the - prefix-discrimination toolkit (pickFreshName_startsWith, ne_of_startsWith_of_not_startsWith) in the kernel-friendly String.startsWith style of ReservedScratchNames; - loopFreeCheck: executable mirror of LoopFree with mutual soundness (spliceSimCheck style); - forEachCompiledBodyChecks: the per-contract decidable gate - compile the body in forEachBodyScope and require loop-free + counters never bound or assigned. Discharged by decide on concrete contracts; a generic name-discipline theorem (#2330 PR-C) can later eliminate the counter checks. Next (#2330 PR-A remainder): forEach_loop_coupling + compiledStmtStep_forEach_literal consuming these gates. Artifacts regenerated (PrintAxioms, verification_status, trust_surface_report).
#2327 (verity-mixin-include) landed proofs relying on the pre-#2326 storage-lens simp set; four compile_*_semantics theorems no longer fold the raw storage record into writeSlot. Unfold ContractState.writeSlot in their closing simp sets (only the four affected sites; the other occurrences stay untouched to keep the zero-warning baseline).
feat(proofs): decidable admission gates for literal-bound forEach bodies
Hidden executable immutable slots are part of the include clash set, so a host field cannot silently alias a mixin immutable. Local and mixin modifiers stay in declared `with` order instead of prefixing mixin guards around already-inlined locals.
…and-modifier-order fix(edsl): include immutable slots and modifier order
Migrates the raw ContractState storage-channel record-update sites to the lens API: 304 baselined sites -> 63 (39 of which are the lens/bulk-lens/ ofChannels implementations in Verity/Core.lean, the permanent residue the step-3 flip swaps in place). - New Core lenses: writeSlots/modifySlots/writeTransientSlots/ modifyTransientSlots/writeAddrSlots (bulk, shapes definitionally equal to the historical multi-slot raw updates), withStorageChannel (channel transformer for denotational flat-view rebuilds), and the ContractState.ofChannels constructor for harness/fixture full states. - Denote/SourceSemantics write helpers now route through lenses (defeq swaps where the guard shapes matched; withStorageChannel + map lenses for the flat-view mapping writes). - Contract proof suites: post-state record literals in _unfold lemma statements restated as lens chains; verity_frame macro extended with lens unfolds; fixtures rebuilt over defaultState + lens chains. - Gate BASELINE shrunk to 5 files with per-entry justification (Owned/* belongs to the concurrent composition lane; IRState fixture and let-binding false positives documented; the =-guarded dual-channel SourceSemantics writers stay for the step-3 burn-down). No theorem statements changed except lens-form restatements that are definitionally equal to the previous raw-record form.
Rebasing the storage-lens burn-down onto main replayed cleanly at the text level but not semantically: main's C5 flip dropped the storage-lens simp args, so the lens chains this PR introduces no longer reduce on their own. - StructArrayStorage: unfold writeArray/writeSlot alongside arrayBridgeState at the sites that previously relied on the ambient simp set; add arrayBridgeField so the field match reduces, and close the length goal with hlen now that simp discharges the mod step. - OwnedCounter/SafeCounter: drop lens unfolds that the migration left unused (zero-warning baseline is fail-closed). - OwnedCounter.Correctness: unfold writeAddrSlot so the post-transfer owner guard reduces. - SimpleToken: merge a split intro flagged by the linter. - Regenerate verification_status.json (core_lines 1098 -> 1178) to match the +80 lines this PR adds to Verity/Core.lean. No theorem statements changed; tactic arguments only. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Reconciles the pre-rebase public head of PR #2329 with the branch as replayed onto main 0fd1c2f. Uses -s ours deliberately: the tree is taken entirely from the replayed side, which already contains this work. Nothing is discarded by this strategy: - eb46f61 (the genuine C5 step 2.5 payload) was replayed as b84d0fa with an identical patch-id (66a10d9a). - 52f3407, dbe1ad5 and 3d65643 had already landed on main via #2327 and #2332; main carries the later reviewed fixes on top (e41b80f, f784f75), so main's version supersedes them. This junction preserves both histories and keeps the push fast-forward, so the branch is updated without rewriting published history.
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_dd485e1f-b7e9-45dc-be80-81ac29d77c6c) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 26 Lean file(s), 1259 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 28 supported / 28 total; Lean 26, trust docs 0, workflow/scripts 2, contracts 0, docs 0
- Changed lines: 1259 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/TypedIRTests.lean (+53/-180), Contracts/Ledger/Proofs/Basic.lean (+29/-116), Contracts/OwnedCounter/Proofs/Basic.lean (+18/-81), Verity/Core/Model/Denote.lean (+27/-70), Verity/Core.lean (+80/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
| \n### CI Failure Hints\n\nFailed jobs: `build-compiler-binaries`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
writeUintSlots/writeAddressSlots/writeTransientTargets now delegate to the ContractState bulk lenses (writeSlots/writeAddrSlots/writeTransientSlots), which are plain defs. The frame lemmas unfolded only the SourceSemantics wrappers, so the `targets.contains` guard stayed buried and `rw [hcontains]` found no pattern. Adds the lens unfolds to the existing simp/rw sets. Tactic arguments only: no theorem statements changed, no new sorry/admit/axiom/unsafe.
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_32b4ab6c-c9c1-4ad7-a9d3-c633101962ce) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 27 Lean file(s), 1280 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 29 supported / 29 total; Lean 27, trust docs 0, workflow/scripts 2, contracts 0, docs 0
- Changed lines: 1280 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/TypedIRTests.lean (+53/-180), Contracts/Ledger/Proofs/Basic.lean (+29/-116), Contracts/OwnedCounter/Proofs/Basic.lean (+18/-81), Verity/Core/Model/Denote.lean (+27/-70), Verity/Core.lean (+80/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
…mple The C5 bulk-lens migration replaced the raw ContractState record literal in vulnerable_attack_exists with ContractState.ofChannels, so simp no longer reduced the .storage/.storageMap projections and the first three bullets were left with unsolved goals.
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_046cf8ae-1d55-4254-ac63-10750bd7d4ec) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 27 Lean file(s), 1286 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 29 supported / 29 total; Lean 27, trust docs 0, workflow/scripts 2, contracts 0, docs 0
- Changed lines: 1286 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/TypedIRTests.lean (+53/-180), Contracts/Ledger/Proofs/Basic.lean (+29/-116), Contracts/OwnedCounter/Proofs/Basic.lean (+18/-81), Verity/Core/Model/Denote.lean (+27/-70), Verity/Core.lean (+80/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
1 participant
Migrates the raw
ContractStatestorage-channel record-update sites to the lens API: 304 baselined sites → 63 (39 = the lens implementations inVerity/Core.lean, the permanent residue the step-3 flip swaps in place).writeSlots/modifySlots/writeTransientSlots/modifyTransientSlots/writeAddrSlots— definitionally equal to the historical multi-slot raw shapes),withStorageChannel(channel transformer for the denotational flat-view mapping writes),ofChannels(canonical full-state constructor for harnesses/fixtures).Denote/SourceSemanticswrite helpers route through lenses (defeq swaps where guards matched; the=-guarded dual-channel writers stay baselined — re-guarding them reshapes the GenericInduction unfold surface, deferred to step 3)._unfoldstatement literals restated as lens chains (definitionally equal);verity_frameextended with lens unfolds; fixtures rebuilt overdefaultState.BASELINEshrunk to 5 justified entries (net −241 sites).make checkdu gate vert). Voir l'issue de suivi C5.Note
Medium Risk
Wide refactor across core storage semantics, compiler proofs, and contract verification paths; changes are mostly definitional but any lens mismatch could break soundness proofs or interpreter agreement.
Overview
Burns down raw
ContractStatestorage-channel record updates in favor of the lens API (writeSlot,writeMap,writeSlots,writeArray,ofChannels, etc.), shrinking the raw-update baseline from hundreds of sites to a small permanent residue inVerity/Core.lean.Compiler and semantics layers now route slot/mapping/transient writes through lenses:
SourceSemanticshelpers delegate towriteSlots/writeAddrSlots/writeTransientSlots; denotation agreement and frame/storage-bridge proofs gain matchingsimpunfolds. Contract/runtime code (Contracts/Common, interpreter initial state) and typed-IR correctness specs use the same helpers instead of inline{ world with storage := … }literals.Contract proofs and fixtures restate
_unfoldlemmas as lens chains (definitionally equal) and rebuild test worlds viadefaultState.writeArray/ofChannels.Adds reusable ownership composition: a
verity_mixin Ownablefacet with specs, footprint, and proofs;OwnedCounterComposedhosts it viaincludeand proves count writes preserve the mixin invariant.Contracts/Smoke/Include.leanexercises mixininclude(namespaces, errors, immutables, clash rejection). CONTRIBUTING documents the mixin workflow.New IR proof scaffolding:
CompiledNameDiscipline.leanintroducesloopFreeCheck,forEachCompiledBodyChecks, and prefix lemmas for literal-boundforEachbodies.Reviewed by Cursor Bugbot for commit bdb1906. Bugbot is set up for automated code reviews on this repo. Configure here.