fix(edsl): include immutable slots and modifier order - #2332
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_78f47544-db44-406d-8fe6-c959be636e70) |
![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: 9ebab73596
ℹ️ 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".
| pure { | ||
| own with | ||
| functions := functions | ||
| includes := includeIdents | ||
| resolvedIncludes := mixins.map (·.1) |
There was a problem hiding this comment.
When an include host uses a local modifier that calls a qualified helper such as Library.check(), returning own.functions without the previously inlined modifier body hides that call from mkSpecCommand, whose qualified-call discovery scans only function and constructor bodies (Verity/Macro/Translate.lean:2843-2848). The modifier is later translated into an internalCall, but the corresponding qualified helper FunctionSpec is never added, so validation/lowering encounters an unresolved internal callee. Scan modifier bodies as well, or retain an expanded function representation for dependency discovery.
Useful? React with 👍 / 👎.
| pure fn | ||
| else | ||
| let arr ← inlineModifierPrefixes mixinModifiers #[fn] | ||
| let arr ← inlineModifierPrefixes allModifiers #[fn] |
There was a problem hiding this comment.
For an include host whose local modifier contains safeAdd, safeSub, safeMul, or a panic arithmetic helper, this inlines the operation only into modelFn, while localObligationTerms is still computed from the original fn at line 4486. Consequently the generated checked-arithmetic obligation disappears from the function metadata and trust/strict-obligation reports even though the compiled model body performs the operation. Compute obligations from the expanded function or explicitly include applied modifier bodies.
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_9fce43db-46ae-4b88-a110-6e3348a36056) |
![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 + 0/1 paquet(s) reviewés sémantiquement. 3 finding(s) (3 low); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Compiler/TypedIRCompilerCorrectness.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 4 Lean file(s), 164 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 3/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 3 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 5 supported / 5 total; Lean 4, trust docs 0, workflow/scripts 0, contracts 0, docs 1
- Changed lines: 164 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 3; files 1; tokens 0; tool calls 0; warnings 1; duration 829s
- Largest changed files: Verity/Macro/Translate.lean (+59/-40), Contracts/Smoke/Include.lean (+38/-1), Compiler/TypedIRCompilerCorrectness.lean (+9/-9), docs/MODIFIERS_AND_INHERITANCE.md (+4/-2), Verity/Macro/Elaborate.lean (+1/-1)
Packet coverage
- Packet review: enabled; selected 3/8 packet(s)
- Scout: configured; status success; 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: Triaged top 3 scout-ranked packet(s); remaining changed hunks/files require Codex or human proof review, and selected packets still need strong reviewer analysis.
- 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.
- Covered packets:
- Compiler/TypedIRCompilerCorrectness.lean:1130 score 25 [lenses: verification-independence, proof-soundness] — hotspot path/churn; ask: Trace both sides of
compile_setStorage_literal_semantics: isexecSourceSetStorageLiteralan independently specified source transition, or does it reuse compiler/TypedIR evaluator definitions or equivalent shared storage-update code such thatsimpproves both sides reduce to the same producer implementation? - Compiler/TypedIRCompilerCorrectness.lean:1313 score 25 [lenses: verification-independence, proof-soundness] — hotspot path/churn; ask: Expand
execCompiledReturnStorage,execSourceReturnStorage, andcompileStmts_single_return_storage_run; do the source and compiled paths have genuinely separate semantics up to an explicitly trusted common state model, or is the result obtained by replaying shared producer/evaluator code on both sides? - Compiler/TypedIRCompilerCorrectness.lean:1955 score 25 [lenses: proof-soundness] — hotspot path/churn; ask: Why are
ContractState.readSlotandwriteSlotneeded for a literal-return theorem, and does inspecting the post-simp goal reveal an unintended state update, weakened observable semantics, or shared-definition tautology?
- Compiler/TypedIRCompilerCorrectness.lean:1130 score 25 [lenses: verification-independence, proof-soundness] — hotspot path/churn; ask: Trace both sides of
Pilot mode: advisory only. Codex Review remains the merge gate.
| simp [execCompiledLetAssignAddSetStorageLocalLiteral, execSourceSetStorageLiteral, | ||
| compileStmts_let_assign_add_literal_setStorage_local_run, hfind, evalTStmts, defaultEvalFuel] | ||
| simp [evalTStmtsFuel, evalTStmtFuel] | ||
| simp [evalTStmtsFuel, evalTStmtFuel, Verity.ContractState.readSlot, Verity.ContractState.writeSlot] |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| compileStmts_single_return_mapping_caller_run, hSlot, | ||
| evalTStmts, defaultEvalFuel] | ||
| simp [evalTStmtsFuel, evalTStmtFuel] | ||
| simp [evalTStmtsFuel, evalTStmtFuel, Verity.ContractState.readSlot, Verity.ContractState.writeSlot] |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| simp [execCompiledLetReturnLocalLiteral, execSourceLetReturnLocalLiteral, | ||
| compileStmts_let_return_local_literal_run, evalTStmts, defaultEvalFuel] | ||
| simp [evalTStmtsFuel, evalTStmtFuel] | ||
| simp [evalTStmtsFuel, evalTStmtFuel, Verity.ContractState.readSlot, Verity.ContractState.writeSlot] |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
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.
3a3823c to
f784f75
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_de8b7380-5cc6-4506-ab24-3886b4cd71b0) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f784f75433
ℹ️ 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".
| pure fn | ||
| else | ||
| let arr ← inlineModifierPrefixes mixinModifiers #[fn] | ||
| let arr ← inlineModifierPrefixes allModifiers #[fn] |
There was a problem hiding this comment.
When an include-host function has an enum parameter and any modifier, inlineModifierPrefixes places the modifier blocks before the enum guards already present in fn.body. translateBodyToStmtTerms then assumes the first enumGuardCount statements are those guards, so it instead moves one or more modifiers ahead of the initializer/role preludes and leaves the actual enum check later. Invalid enum calldata can therefore execute a modifier or produce its revert reason before the required enum panic in the compilation model, while the executable path explicitly prepends the enum guard before modifiers. Preserve/extract the enum guards before inlining, or inline modifiers after the leading guards.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage + 0/1 paquet(s) reviewés sémantiquement. 4 finding(s) (4 low); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Verity/Macro/Translate.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 3 Lean file(s), 146 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 4/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 4 supported / 4 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 1
- Changed lines: 146 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 1; tokens 0; tool calls 0; warnings 1; duration 834s
- Largest changed files: Verity/Macro/Translate.lean (+59/-40), Contracts/Smoke/Include.lean (+38/-1), docs/MODIFIERS_AND_INHERITANCE.md (+4/-2), Verity/Macro/Elaborate.lean (+1/-1)
Packet coverage
- Packet review: enabled; selected 4/8 packet(s)
- Scout: configured; status success; 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: Triaged top 4 scout-ranked packet(s); remaining changed hunks/files require Codex or human proof review, and selected packets still need strong reviewer analysis.
- 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.
- Covered packets:
- Verity/Macro/Translate.lean:3726 score 13 [lenses: proof-soundness] — hotspot path/churn; ask: Trace an included function with both host and mixin modifiers through include resolution: are all modifiers preserved exactly once, in declared order, and represented identically in executable statements and generated specifications?
- Verity/Macro/Translate.lean:4445 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Compare the generated executable body, CompilationModel statements, and theorem/specification commands for functions using inherited and host modifiers; do they apply the same modifiers exactly once and in the same order, without turning modifier conditions into unearned proof hypotheses?
- Verity/Macro/Translate.lean:3658 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Verify that immutableStorageFieldDecl computes precisely the slot used by code generation for each mixin immutable, including offsets from ordinary fields and earlier mixins, and that clash checking covers both names and every occupied storage slot.
- Verity/Macro/Translate.lean:3606 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Check that the synthesized host immutable fields use the same slot allocation algorithm as translation and that seenFieldNames plus slot-overlap checks account for multi-slot fields, explicit slots, nested declarations, and all host/mixin ordering cases.
Pilot mode: advisory only. Codex Review remains the merge gate.
| -- applied in that order later (executable calls mixin defs; the model | ||
| -- inlines every modifier body). Splitting the list would prefix mixin | ||
| -- guards around already-inlined locals and reverse source order. | ||
| for fn in own.functions do |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [low]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: This changes how host-local versus mixin modifiers are retained or inlined during include resolution. If a modifier is dropped, duplicated, or applied in the wrong order, generated function bodies/specifications may silently lose guards or invariants, making downstream Lean proofs establish a weaker semantics than the source contract declares.
Ask the reviewer: Trace an included function with both host and mixin modifiers through include resolution: are all modifiers preserved exactly once, in declared order, and represented identically in executable statements and generated specifications?
Why flagged: hotspot path/churn; 24 changed line(s) near Verity/Macro/Translate.lean:3726. Signals: hotspot path/churn.
Added-line sample:
- L3726:
-- Keep the declared modifier sequence. Locals and mixin modifiers are - L3727:
-- applied in that order later (executable calls mixin defs; the model - L3728:
-- inlines every modifier body). Splitting the list would prefix mixin - L3729:
-- guards around already-inlined locals and reverse source order. - L3730:
for fn in own.functions do
| pure fn | ||
| else | ||
| let arr ← inlineModifierPrefixes mixinModifiers #[fn] | ||
| let arr ← inlineModifierPrefixes allModifiers #[fn] |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [low]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: The new hostModifiers parameter affects public function command generation and apparently reconciles modifier ordering between translated bodies and generated models/specifications. A mismatch can make proofs reason about guards or effects that execution does not enforce, or omit assumptions required by execution.
Ask the reviewer: Compare the generated executable body, CompilationModel statements, and theorem/specification commands for functions using inherited and host modifiers; do they apply the same modifiers exactly once and in the same order, without turning modifier conditions into unearned proof hypotheses?
Why flagged: hotspot path/churn; 19 changed line(s) near Verity/Macro/Translate.lean:4445. Signals: hotspot path/churn.
Added-line sample:
- L4445:
(boundImmutableDecls : Array ImmutableDecl := immutableDecls) - L4446:
(hostModifiers : Array ModifierDecl := #[]) : CommandElabM (Array Cmd) := do - L4451:
let fnBodyWithMixin ← prefixMixinModifierExecutableBody resolvedIncludes fn fn.body hostModifiers - L4468:
-- CompilationModel inlines every modifier in declared ′with′ order so - L4469:
-- ′modifies(...)′ sees the write set. The executable path still binds
| ("include clash: slot " ++ toString sl ++ " from mixin '" ++ | ||
| toString mixinName ++ "' immutable '" ++ imm.name ++ | ||
| "' overlaps a host or earlier mixin slot") | ||
| seenPersistSlots := seenPersistSlots.push sl |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [low]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: This alters inclusion clash checking for immutable declarations by synthesizing storage fields from immutable indices. Incorrect index or slot derivation could permit immutable/storage aliasing, so generated state semantics and any proofs over distinct fields would be unsound relative to actual storage behavior.
Ask the reviewer: Verify that immutableStorageFieldDecl computes precisely the slot used by code generation for each mixin immutable, including offsets from ordinary fields and earlier mixins, and that clash checking covers both names and every occupied storage slot.
Why flagged: hotspot path/churn; 16 changed line(s) near Verity/Macro/Translate.lean:3658. Signals: hotspot path/churn.
Added-line sample:
- L3658:
for (imm, idx) in mixin.immutableDecls.zipIdx do - L3660:
let immField := immutableStorageFieldDecl mixin.fields imm idx - L3661:
for n in fieldDeclaredNames immField do - L3662:
if seenFieldNames.contains n then - L3663:
throwError
| let mut seenPersistSlots : Array Nat := | ||
| (host.fields.filter (fun f => !f.isTransient)).flatMap fieldOccupiedSlots | ||
| (host.fields.filter (fun f => !f.isTransient)).flatMap fieldOccupiedSlots ++ | ||
| hostImmFields.flatMap fieldOccupiedSlots |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [low]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Finding: Host immutable declarations are newly folded into the storage-field clash set. This is a trust-boundary calculation between parsed declarations and generated storage semantics; an off-by-one, incomplete flattening, or inconsistent slot model could allow aliased fields while proofs treat them as independent.
Ask the reviewer: Check that the synthesized host immutable fields use the same slot allocation algorithm as translation and that seenFieldNames plus slot-overlap checks account for multi-slot fields, explicit slots, nested declarations, and all host/mixin ordering cases.
Why flagged: hotspot path/churn; 11 changed line(s) near Verity/Macro/Translate.lean:3606. Signals: hotspot path/churn.
Added-line sample:
- L3606:
let hostImmFields := - L3607:
host.immutableDecls.zipIdx.map fun (imm, idx) => - L3608:
immutableStorageFieldDecl host.fields imm idx - L3609:
let mut seenFieldNames : Array String := - L3610:
host.fields.flatMap fieldDeclaredNames ++ hostImmFields.flatMap fieldDeclaredNames
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
IncludeImmutableHostfixture putcounton the same slot as mixinversion.withorder when a host mixes local and mixin modifiers.Test Plan
lake build Contracts.Smoke.Include#check_contractIncludeImmutableHost (slot 1) and IncludeModifierOrderHost#guard_msgsIncludeImmutableSlotClashRejectedRelated
Follow-up to #2327 Codex P1s after merge.
Note
Medium Risk
Changes EDSL elaboration for storage layout validation and modifier wrapping on include hosts; incorrect behavior could skew generated models or executable bodies, but scope is narrow with new smoke coverage.
Overview
Include clash checks now treat executable immutables as reserving hidden persistent slots (after the declaring contract’s user fields), for both the host and each included mixin. Overlapping a host field with a mixin immutable slot fails at elaboration with a dedicated error; the smoke fixture moves
countoff mixinversion’s slot.withmodifier composition onincludehosts no longer splits locals vs mixin modifiers or pre-inlines host modifiers during parsing. Locals and mixin modifiers run in source order: the executable path still calls imported mixin modifier defs but inlines host-local modifier bodies in sequence; the CompilationModel path inlines every listed modifier (host + mixin) in that same order somodifies(...)matches runtime behavior.Docs and smoke tests cover immutable slot rejection and
localGuard, mixinGuardordering.Reviewed by Cursor Bugbot for commit f784f75. Bugbot is set up for automated code reviews on this repo. Configure here.