feat(edsl): verifiable mixin include for proof reuse - #2327
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_f81c16a2-8de8-4bbe-ad84-f4615802e90f) |
![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: 29 Lean file(s), 1261 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: 36 supported / 42 total; Lean 29, trust docs 0, workflow/scripts 5, contracts 0, docs 2
- Changed lines: 1261 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 (+277/-9), Verity/Specs/Composition.lean (+128/-0), Contracts/Smoke/Include.lean (+95/-0), Verity/Macro/Translate/Parsing.lean (+62/-20), Contracts/OwnedCounterComposed/Proofs/Basic.lean (+81/-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.
![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: 52f340711b
ℹ️ 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".
| some { | ||
| h with | ||
| body := ms.flatMap (·.body) ++ h.body | ||
| localObligations := ms.flatMap (·.localObligations) ++ h.localObligations |
There was a problem hiding this comment.
When a host initializes a mixin with a differently named parameter or an expression such as M(add x 1), the executable constructor calls the mixin with that argument, but this merge copies the mixin's model body unchanged and retains only the host parameter list. Consequently the compilation model either fails scope validation on the mixin parameter name or, when names happen to match, silently compiles the wrong value; substitute each initializer's arguments into its constructor body before concatenating it.
Useful? React with 👍 / 👎.
| let fnExecutableBody ← prependEnumGuards fn.params fnExecutableBody | ||
| let fnExecutableBody ← prefixMixinModifierExecutableBody resolvedIncludes fn fnExecutableBody |
There was a problem hiding this comment.
For a host function that combines an included modifier with requires(...) or an initializer guard, this late prefix makes the executable run the modifier before those generated guards. The model path instead passes the original function to translateBodyToStmtTerms, which places its role/init preludes before the inlined modifier, so executable behavior and the verified/compiled model can disagree on whether a call succeeds and which revert is returned.
Useful? React with 👍 / 👎.
| let initNames := inits.map fun (id, _) => toString id.getId | ||
| for (mixinName, mixin) in mixins do | ||
| if mixin.ctor.isSome then | ||
| let shortName := mixinShortName mixinName | ||
| unless initNames.any (fun n => namesMixin n mixinName) do |
There was a problem hiding this comment.
A host initializer list such as M(x) M(add x 1) passes this validation because it only checks that each name is known and that every required mixin appears. mkHostConstructorDefCommandPublic then executes both occurrences, while mergeIncludedSpecs incorporates M's constructor exactly once, producing a silent executable/model mismatch; require exactly one initializer per included mixin.
Useful? React with 👍 / 👎.
| \n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
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_e0dbab4f-9353-4ac2-bfd1-6058972a01f2) |
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: 29 Lean file(s), 1417 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: 36 supported / 42 total; Lean 29, trust docs 0, workflow/scripts 5, contracts 0, docs 2
- Changed lines: 1417 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), Verity/Specs/Composition.lean (+128/-0), Contracts/Smoke/Include.lean (+126/-0), Verity/Macro/Translate/Parsing.lean (+62/-20), Contracts/OwnedCounterComposed/Proofs/Basic.lean (+81/-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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: dbe1ad5ab2
ℹ️ 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".
| validateFunctionDeclsPublic (mixinFields ++ fields) errorDecls eventDecls constDecls immutableDecls | ||
| externalDecls ctor (mixinModifiers ++ modifiers) functions |
There was a problem hiding this comment.
When an included mixin modifier references a custom error declared by that mixin, this call validates the collected mixinModifiers using only the host's errorDecls (and likewise only host events, constants, immutables, externals, and functions). A mixin that elaborates successfully on its own therefore fails every host include with an “unknown custom error” during validateDoElemsExprTypes; accumulate the corresponding mixin declarations or retain each modifier's original validation context.
Useful? React with 👍 / 👎.
| adtTypes := mixins.flatMap (·.adtTypes) ++ host.adtTypes | ||
| reservedSlotRanges := mixins.flatMap (·.reservedSlotRanges) ++ host.reservedSlotRanges | ||
| slotAliasRanges := mixins.flatMap (·.slotAliasRanges) ++ host.slotAliasRanges | ||
| constructor := host.constructor |
There was a problem hiding this comment.
When a mixin declares an immutable, the merged model retains that immutable but this assignment discards the mixin constructor that contains its generated setImmutable statement. expandMixinConstructorForModel only copies the mixin's user-written constructor body, while host spec generation emits initializer statements only for host immutables, so validateImmutableInitialization rejects the composed contract as declaring an immutable that is never initialized. Splice each mixin's generated immutable initialization into the host constructor before retaining only host.constructor.
Useful? React with 👍 / 👎.
| for fn in mixin.functions do | ||
| unless fn.isInternal do | ||
| if seenFnNames.contains fn.name then | ||
| throwError s!"include clash: function '{fn.name}' from mixin '{mixinName}' duplicates a host or earlier mixin entrypoint" |
There was a problem hiding this comment.
When two included mixins use the same internal helper name, or a mixin helper matches a host helper, this loop deliberately skips the collision check even though mergeIncludedSpecs later concatenates all internal function specs unchanged. validateCompilationModel then rejects the result with “duplicate internal function name” because Yul definitions are keyed by that name; include internal/shadow names in collision validation or namespace them per mixin.
Useful? React with 👍 / 👎.
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.
dbe1ad5 to
e41b80f
Compare
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_bc7404e6-d4bd-4a55-9061-9d5308e0302c) |
|
Re-reviewed the latest Codex findings and pushed Fixed
The first three Codex P1s (ctor arg substitution, guard order, duplicate mixin ctor inits) were already closed in the previous commit. Not a silent model rewrite |
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: 29 Lean file(s), 1606 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: 36 supported / 42 total; Lean 29, trust docs 0, workflow/scripts 5, contracts 0, docs 2
- Changed lines: 1606 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 (+471/-19), Contracts/Smoke/Include.lean (+209/-0), Verity/Specs/Composition.lean (+128/-0), Verity/Macro/Elaborate.lean (+91/-6), Verity/Macro/Translate/Parsing.lean (+62/-20)
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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e41b80f1d3
ℹ️ 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".
| let mut seenPersistSlots : Array Nat := | ||
| (host.fields.filter (fun f => !f.isTransient)).flatMap fieldOccupiedSlots | ||
| let mut seenTransientSlots : Array Nat := | ||
| (host.fields.filter (·.isTransient)).flatMap fieldOccupiedSlots |
There was a problem hiding this comment.
When a mixin has an immutable, this check reserves only its declared fields and ignores the hidden field produced by immutableStorageFieldDecl; a host field or another mixin immutable can therefore reuse that slot. For example, the new no-field IncludeImmutableMixin assigns its executable version binding to slot 0 while IncludeImmutableHost.count also occupies slot 0, so the imported getter observes count, whereas the merged compilation model uses the independent bytecode immutable. Include these generated immutable fields in the collision check so executable proofs cannot diverge from the compiled contract.
Useful? React with 👍 / 👎.
| let localUsed := fn.modifiers.filter fun id => | ||
| localModifiers.any (fun m => m.name == toString id.getId) | ||
| let mixinUsed := fn.modifiers.filter fun id => | ||
| mixinModNames.contains (toString id.getId) |
There was a problem hiding this comment.
When a host function interleaves modifier kinds, such as with localGuard, mixinGuard, partitioning the list here causes localGuard to be inlined into the body while every retained mixin modifier is later prefixed around that body. Both executable and model lowering therefore run mixinGuard before localGuard, reversing the source order and potentially changing which guard reverts or which side effects occur; inline the combined modifier sequence without separating its ordering.
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.
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_fd04d610-043d-4825-be00-475a76c66168) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
⚪ OCR did not run — this diff has no OCR-supported files. Not a review outcome.
No changed files matched OCR include rules.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: no-supported (router-v10)
- Changed files: 0 supported / 0 total; Lean 0, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 0 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status no-supported; comments 0; files 0; tokens 0; tool calls 0; warnings 0; duration 0s
Pilot mode: advisory only. Codex Review remains the merge gate.
#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).
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.
1 participant
Summary
Adds
verity_mixinandverity_contract Host include M1, M2so a host imports mixin Lean definitions and proofs instead of flattening a copied tree (is Parent).with onlyOwnerbinds the mixin’sonlyOwner(sameStorageSlot).M1(args) M2(args)run mixinconstructorvalues, then the host body.is Parentflatten is unchanged.Acceptance example:
Contracts.Ownable+Contracts.OwnedCounterComposed. Hostincrement_reverts_when_not_ownerreusesonlyOwner_reverts;increment_preserves_ownerisWritesOnly+ disjoint footprints.Ownedspecs now useowner.slot.OwnedCounterremains the Yul / Foundry twin.Test plan
lake build Contracts.Ownedlake build Contracts.Smoke(#check_contract+#guard_msgsfor slot/name/missing-ctor)lake build Contracts.OwnedCounterComposedContract.runeval: owner increment writes count, not-owner reverts, owner slot unchangedmake checkNote
Medium Risk
Large macro and elaboration surface (include merge, constructors, modifiers) affects how every host contract compiles, though clash checks and smoke tests constrain regressions.
Overview
Adds
verity_mixinandverity_contract Host include M1, M2so hosts import mixin Lean defs and proofs instead of flattening withis Parent. Elaboration mergesCompilationModelviamergeIncludedSpecs, emitshost_specplus mergedspec, bindswith onlyOwnerto the mixin modifier, runsMixin(args)constructor inits, and fails closed on slot/name/role/modifier/function clashes. Mixin slots are not remapped.Introduces
Verity.Specs.Composition(Footprint,WritesOnly,writesOnly_preserves_other_inv) so host proofs reuse mixin guard and invariant theorems when footprints are disjoint.Ships
Contracts.OwnableandOwnedCounterComposedas the acceptance path;Ownedspecs/proofs switch from literal slot0toowner.slot. Docs, CONTRIBUTING mixin guidance,PrintAxioms, and verification manifests are updated. Compiler correctness proofs drop redundant storagesimplemmas; smokeInclude.leanadds#guard_msgsfor include errors.Reviewed by Cursor Bugbot for commit afd6501. Bugbot is set up for automated code reviews on this repo. Configure here.