Language design axes: full implementation (25 steps across 6 axes)#1731
Conversation
Planning document for the 5 axes of language design improvements that go beyond Solidity parity (#1726): - Axis 1: Type system enrichment (newtypes, ADTs, Result types) #1727 - Axis 2: Compile-time safety enforcement (CEI, access control, unsafe) #1728 - Axis 3: Effect system & auto-theorem generation #1729 - Axis 4: Storage safety (EIP-7201 namespaces) #1730 Includes suggested implementation order (Axis 3 first — lowest friction, highest proof payoff, builds theorem generation infra reused by Axis 2), effort estimates, file-level impact analysis, and integration mapping to #1724 parity waves. No code changes — planning only. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ctions Phase 1 of the Language Design Axes plan (#1729, Axis 3). For every `view` function in a `verity_contract`, the macro now auto-generates a `@[simp]` theorem `<fn>_is_view` stating: FunctionSpec.isView (<fn>_model) = true This is provable by `rfl` because the macro already sets the flag. The `stmtWritesState` validation in `Validation.lean` guarantees the body contains no state-writing statements, so the flag accurately reflects the function's behavior. Changes: - Specs/Common.lean: add `viewPreservesState` predicate (full state unchanged frame condition, covering all storage + context + events + knownAddresses) with `@[simp]` reflexivity theorem - Macro/Bridge.lean: add `mkViewTheoremCommand` that generates the `_is_view` simp lemma for a view function - Macro/Elaborate.lean: call `mkViewTheoremCommand` in the per-function loop for view functions - MacroTranslateInvariantTest.lean: compile-time assertion that the `MutabilitySmoke.currentOwner_is_view` theorem exists Verified: `lake build` succeeds, `make check` passes, all existing contracts (ERC20, Vault, SimpleToken, Ledger, etc.) unaffected. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
![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: b4a13f829a
ℹ️ 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".
| Emits a `@[simp]` lemma stating the model's `isView` flag is `true`, making this | ||
| fact available to downstream proof automation. Only called when `fnDecl.isView`. -/ | ||
| def mkViewTheoremCommand (fnDecl : FunctionDecl) : CommandElabM Cmd := do | ||
| let viewName ← mkSuffixedIdent fnDecl.ident "_is_view" |
There was a problem hiding this comment.
_is_view helper names
Generating $fn_is_view introduces a new declaration name, but the existing collision validator still only reserves _modelBody, _model, _bridge, and _semantic_preservation in validateGeneratedDefNamesPublic (Verity/Macro/Translate.lean). If a contract already declares a symbol like currentOwner_is_view (function/field/constant), elaboration now fails with a duplicate-name error instead of being rejected up front with the normal validation path. Please add _is_view to generated-name conflict checks (at least for view functions) so these contracts don’t regress.
Useful? React with 👍 / 👎.
Implements Phase 1, Step 1b of the language design axes plan (#1729). New `modifies(field1, field2)` annotation for verity_contract functions declares which storage fields a function writes to. The compiler: 1. Validates modifies field names exist in the storage section 2. Validates the function body only writes to declared fields (via new `stmtWrittenFields` / `stmtListWrittenFields` walkers) 3. Auto-generates `_modifies` simp theorem recording the declared set 4. Auto-generates `_frame` definition: conjunction of unchanged predicates for every field NOT in the modifies set plus sameContext 5. Auto-generates `_frame_rfl` simp lemma proving the frame holds reflexively Syntax: `function myFn (...) modifies(field1, field2) : RetTy := body` Files changed: - Macro/Syntax.lean: new `verityModifies` syntax category - Macro/Translate.lean: FunctionDecl.modifies field, parser, validation - CompilationModel/Types.lean: FunctionSpec.modifies field - CompilationModel/Validation.lean: stmtWrittenFields walker + check - Macro/Bridge.lean: mkModifiesTheoremCommand + mkFrameDefCommand - Macro/Elaborate.lean: emit modifies/frame in per-function loop - Contracts/Smoke.lean: ModifiesSmoke test contract - Tests: invariant test + round-trip fuzz coverage Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 405f491f9d
ℹ️ 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".
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
…s theorem Add the `no_external_calls` mutability modifier that rejects external call statements at compile time and auto-generates a `_no_calls` simp theorem. - Syntax: `function no_external_calls foo (...) : T := body` - New `stmtContainsExternalCall` / `exprContainsExternalCall` walkers in Validation.lean detect call/staticcall/delegatecall/externalCall/ecm - `noExternalCalls : Bool` added to FunctionDecl and FunctionSpec - `mkNoCallsTheoremCommand` in Bridge.lean emits `@[simp] theorem _no_calls` - NoExternalCallsSmoke test contract with compile-time theorem assertions - All `make check` CI invariants pass Phase 1 progress: Steps 1a, 1b, 1c done; Step 1d (annotation composition) remaining. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: deca050b4f
ℹ️ 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".
…on theorem When a function has 2+ effect annotations (view, no_external_calls, modifies), auto-generate an _effects theorem that bundles all individual effect facts into a single And proposition, simplifying downstream proof automation. - Add effectAnnotationCount and mkEffectsTheoremCommand in Bridge.lean - Wire _effects emission in Elaborate.lean for functions with ≥2 annotations - Add EffectCompositionSmoke test contract exercising all combinations - Update MacroTranslateInvariantTest with specs, sigs, selectors, theorem checks - Update MacroTranslateRoundTripFuzz with EffectCompositionSmoke.spec Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
verity/Verity/Macro/Translate.lean
Lines 3859 to 3863 in d639daa
Reserve generated _effects helper names
The elaborator now emits <fn>_effects declarations (mkEffectsTheoremCommand), but generated-name validation still only reserves _modelBody, _model, _bridge, and _semantic_preservation. This allows user symbols like transfer_effects to pass early validation and then fail later with duplicate declaration errors when theorem generation runs. Add _effects to the helper-name collision checks so the failure is caught deterministically during validation.
ℹ️ 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".
| syntax "payable" : verityMutability | ||
| syntax "view" : verityMutability | ||
| syntax "no_external_calls" : verityMutability | ||
| syntax "modifies(" sepBy(ident, ",") ")" : verityModifies |
There was a problem hiding this comment.
modifies() clauses
Using sepBy(ident, ",") allows modifies() with zero fields, and downstream validation/theorem generation is gated on !modifies.isEmpty, so this annotation becomes a silent no-op: write-set checks are skipped and no frame artifacts are emitted. That can mislead users into believing writes are constrained when they are not. Either require at least one field (sepBy1) or treat an empty clause as “writes nothing” and enforce it.
Useful? React with 👍 / 👎.
| | .mappingAddressToUint256 | .mappingChain _ | .mappingStruct _ _ => | ||
| -- ∀ k, s'.storageMap slot k = s.storageMap slot k | ||
| `(∀ k, s'.storageMap $slotLit k = s.storageMap $slotLit k) |
There was a problem hiding this comment.
This branch emits frame conjuncts for all mappingStruct fields via storageMap (address-keyed), ignoring whether the struct mapping key type is Uint256. For contracts that use MappingStruct(Uint256, ...), the generated _frame predicate constrains the wrong state component, so frame obligations can be proven without actually preserving the uint-keyed mapping field. The adjacent mappingStruct2 wildcard has the same key-type erasure risk. Split these cases by key types and use the corresponding storage relation.
Useful? React with 👍 / 👎.
…n_writes opt-out Add Checks-Effects-Interactions ordering enforcement as a default-on static analysis pass. Functions that write storage after an external call are rejected at compile time unless annotated with allow_post_interaction_writes. Compliant functions receive an auto-generated @[simp] _cei_compliant theorem. - Add allow_post_interaction_writes syntax modifier and FunctionDecl/FunctionSpec field - Implement stmtIsPersistentWrite, stmtIsDirectExternalCall, and mutual stmtListCEIViolation/stmtInternalCEIViolation walkers in Validation.lean - Wire CEI validation into validateFunctionSpec (runs at compileChecked time) - Generate _cei_compliant theorem in Bridge.lean/Elaborate.lean - Add CEISmoke positive test and CEIViolationRejected negative test (#guard_msgs) - Annotate 5 existing functions with allow_post_interaction_writes - Update invariant test, fuzz coverage exclusion, and property test artifacts Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9fff4b4fba
ℹ️ 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".
| own nested structure. -/ | ||
| def stmtInternalCEIViolation : Stmt → Option String | ||
| | Stmt.ite _ thenBranch elseBranch => | ||
| match stmtListCEIViolation thenBranch false with |
There was a problem hiding this comment.
stmtInternalCEIViolation always checks if branches with seenCall = false, so an earlier interaction is forgotten once control reaches a compound statement. This lets patterns like externalCall ...; if cond then setStorage ... pass CEI validation even though the write is post-interaction on that path; the same reset happens for loop-body checks. The nested CEI walk needs to inherit the caller’s seenCall state.
Useful? React with 👍 / 👎.
| if seenCall && stmtIsPersistentWrite s then | ||
| some "state write after external call" | ||
| else | ||
| let newSeenCall := seenCall || stmtContainsExternalCall s | ||
| stmtListCEIViolation rest newSeenCall |
There was a problem hiding this comment.
The CEI check only errors on writes when seenCall was already true before the current statement. For statements that both contain an external call and perform a persistent write (for example setStorage/setMapping with a call expression on the RHS), newSeenCall is set after the statement and no violation is raised, allowing an interaction-before-effect sequence to slip through.
Useful? React with 👍 / 👎.
…i_safe Complete the four-rung CEI escalation ladder: Rung 1: Safe by default (compiler enforces CEI ordering) [Step 2a] Rung 2: cei_safe (machine-checked proof obligation) [NEW] Rung 3: nonreentrant(field) (known-safe reentrancy guard) [NEW] Rung 4: allow_post_interaction_writes (explicit trust-surface opt-out) [Step 2a] - Add nonreentrant(field) and cei_safe syntax modifiers - Add nonReentrantLock/ceiSafe fields to FunctionDecl and FunctionSpec - Refactor parseMutabilityModifiers to use ParsedMutability record (was 4-tuple) - Update CEI enforcement to bypass for any escalation rung - Validate nonreentrant lock field references and mutual exclusivity - Auto-generate _nonreentrant and _cei_safe @[simp] theorems - Add CEILadderSmoke test contract exercising all ladder rungs - Update invariant, fuzz, and property test infrastructure Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b1fd6e3a44
ℹ️ 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".
| -- Rung 2: cei_safe (machine-checked proof obligation) | ||
| -- Rung 3: nonreentrant(field) (known-safe reentrancy guard) | ||
| -- Rung 4: allow_post_interaction_writes (explicit trust-surface opt-out) | ||
| let ceiExempt := spec.allowPostInteractionWrites || spec.nonReentrantLock.isSome || spec.ceiSafe |
There was a problem hiding this comment.
cei_safe exemption
Including spec.ceiSafe in ceiExempt disables CEI validation outright, but this change set does not generate or verify any proof obligation for that annotation, so cei_safe currently behaves like an unchecked opt-out. A function can mark itself cei_safe and still perform interaction-then-write sequences (as in CEILadderSmoke.callThenStoreProved) without any machine-checked evidence, which defeats the stated safety ladder.
Useful? React with 👍 / 👎.
…ole theorem Add `requires(field)` annotation for functions that auto-injects a `require(caller == roleHolder)` check at the start of the function body. The named field must be an Address-typed storage field. Both source-level (DSL do-block) and IR-level (Stmt prelude) guards are generated. Changes: - Syntax.lean: new `verityRequiresRole` syntax category, `requires(ident)` - Translate.lean: `requiresRole` field on FunctionDecl, `resolveRoleField` validation, `mkRoleGuardedBody` (source-level), `roleGuardPreludeStmtTerms` (IR-level), wired into `translateBodyToStmtTerms` and FunctionSpec construction - Types.lean: `requiresRole : Option String` on FunctionSpec - Bridge.lean: `mkRequiresRoleTheoremCommand` generates `_requires_role` theorem - Elaborate.lean: emits `_requires_role` theorems for annotated functions - Smoke.lean: RolesSmoke test contract with requires(admin) - Integration tests: MacroTranslateInvariantTest, MacroTranslateRoundTripFuzz, PropertyRolesSmoke.t.sol Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d3a5e48d94
ℹ️ 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".
| ← `(Compiler.CompilationModel.Stmt.require | ||
| (Compiler.CompilationModel.Expr.eq | ||
| (Compiler.CompilationModel.Expr.caller) | ||
| (Compiler.CompilationModel.Expr.storage $(strTerm field.name))) |
There was a problem hiding this comment.
The IR prelude generated for requires(...) compares Expr.caller against Expr.storage field, even though resolveRoleField enforces that the role field is Address-typed and the executable body uses getStorageAddr for the same check. In the model semantics this reads the wrong state component (storage vs storageAddr), so proofs/validation over FunctionSpec.body can disagree with the actual guarded function behavior for role-protected entrypoints.
Useful? React with 👍 / 👎.
Add a `types` section to the verity_contract grammar that lets users declare semantic newtypes (e.g. `TokenId : Uint256`). At the language level the types are distinct identifiers; at the EVM/Yul level they are erased to their base types (zero overhead). Changes: - Syntax.lean: declare verityNewtype syntax category, add optional `types` section before `storage` in verityContractCmd - Translate.lean: NewtypeDecl structure, parseNewtype with scalar-only validation, thread newtypes array through all parse* and valueTypeFromSyntax functions, resolve unknown idents against newtypes before erroring - Elaborate.lean: destructure the new newtypes return value - Smoke.lean: NewtypeSmoke test contract (TokenId, Amount, Owner) with #check_contract - MacroTranslateInvariantTest: specs, signatures, selectors, theorems - MacroTranslateRoundTripFuzz: specs - generate_macro_property_tests.py: parse `types` section, resolve newtypes to base types in function params/return types - PropertyNewtypeSmoke.t.sol: auto-generated property tests Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Every contract now emits a `storageNamespace : Nat` definition equal to
`keccak256("{ContractName}.storage.v0")` computed at elaboration time
using the vendored kernel-computable Keccak engine. This hash can serve
as a base offset so different contracts occupy non-overlapping regions of
the 2^256 storage address space (Step 4b will wire the offset).
Changes:
- Translate.lean: import Compiler.Keccak.Sponge, add byteArrayToNatBE
helper, computeStorageNamespace, mkStorageNamespaceCommand
- Elaborate.lean: emit storageNamespace after storage/immutable defs
- Smoke.lean: fix #check_contract ordering for RolesSmoke/NewtypeSmoke
(forward-reference bug from Step 3a), add storageNamespace type
verification examples
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add `storage_namespace` keyword to the `verity_contract` grammar.
When present, all user-declared `slot N` values are offset by
`keccak256("{ContractName}.storage.v0")`, giving each contract a
unique region in the 2^256 storage address space (EIP-7201 pattern).
Existing contracts without `storage_namespace` are unaffected —
the feature is strictly opt-in, merging the original plan's steps
4b (slot offsetting) and 4c (override attributes) into a single
backwards-compatible mechanism.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Thread `storageNamespace : Option Nat` through the CompilationModel so
downstream tooling can consume it:
- Add `storageNamespace` field to `CompilationModel` (default `none`)
- Pass namespace from `parseContractSyntax` → spec generation
- Emit `"storageNamespace"` key in layout report JSON
- Add `emitContractStorageLayoutJson` / `writeContractStorageLayoutFile`
in ABI.lean — writes `{Contract}.storage.json` alongside ABI output
- Smoke tests verify `spec.storageNamespace.isSome` for namespaced
contracts and `.isNone` for regular contracts
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
| \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``` |
Add `unsafe "reason" do` syntax as a transparent wrapper around statement blocks, laying the groundwork for restricted-operation gating (Step 6b) and trust reporting (Step 6c). - New Stmt.unsafeBlock variant with reason string and body - doElem syntax: `unsafe "..." do <doSeq>` - Translate.lean: validation + translation cases - All 16 exhaustive Stmt pattern-match sites updated (transparent recurse-into-body semantics) - UnsafeBlockSmoke test contract with #check_contract - Integration tests updated (invariant, round-trip fuzz, property gen) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add unguarded mechanics collector that skips `unsafe "reason" do` block bodies, so low-level operations (mstore, call, staticcall, etc.) inside unsafe blocks no longer trigger the local_obligations requirement. Functions/constructors using low-level mechanics *outside* an unsafe block must still declare local_obligations or the validation pass rejects them with a clear error referencing Issue #1424. - TrustSurface: collectUnguardedLowLevelStmtMechanics (returns [] for unsafeBlock instead of recursing), plus public API wrappers - Validation: validateFunctionSpec/validateConstructorSpec now use the unguarded collector - Smoke tests: UnsafeGatingAccepted (mstore inside unsafe passes) and UnsafeGatingRejected (#guard_msgs negative test for mstore outside) - Integration: MacroTranslateInvariantTest, MacroTranslateRoundTripFuzz, property tests, fuzz coverage exclusion all updated Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…afe flag Add unsafe block tracking to the trust report infrastructure: - TrustSurface: collectUnsafeBlockReasons extracts reason strings from Stmt.unsafeBlock nodes; UsageSiteSummary gains unsafeBlocks field; JSON trust report and verbose CLI output both include unsafe blocks; emitUnsafeBlockUsageSiteLines provides per-site diagnostic lines - CompileDriverCommon: ensureNoUnsafeBlocks rejects contracts containing unsafe blocks when --deny-unsafe is set; verbose output includes "Unsafe block report" section - MainDriver: --deny-unsafe CLI flag parsed and threaded through - CompileDriverTest: deny-unsafe rejection test, pass-through test for contracts without unsafe blocks, trust report JSON content assertion Phase 6 (Unsafe Blocks) is now complete: 6a (syntax), 6b (gating), 6c (trust report + deny flag). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add `inductive` section to `verity_contract` grammar for declaring algebraic data types (tagged unions) with typed variant fields. ADTs are parsed, validated (no duplicate names, no built-in shadowing), and threaded through the parse pipeline. IR generation deferred to Step 5b. Grammar: `inductive OptionalUint := | Some(value : Uint256) | None` Syntax categories: verityAdtVariant, verityAdtDecl Structures: AdtVariantDecl, AdtDecl (in Translate.lean) Parsers: parseAdtVariant, parseAdtDecl Files: Syntax.lean, Translate.lean, Elaborate.lean, Smoke.lean, MacroTranslateInvariantTest.lean, MacroTranslateRoundTripFuzz.lean Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add IR-level algebraic data type support across the compilation model: - Types.lean: AdtVariant, AdtTypeDef structs; ParamType.adt variant; Expr.adtConstruct/adtTag/adtField; Stmt.matchAdt; adtTypes in spec - Exhaustive pattern match coverage for ParamType.adt across AbiHelpers, AbiTypeLayout, AbiEncoding, EventAbiHelpers, ParamLoading - Exhaustive Expr ADT cases in LogicalPurity, UsageAnalysis, TrustSurface, ExpressionCompile, ValidationHelpers, Validation - Stmt.matchAdt handling with explicit recursive helpers (replacing branches.any/flatMap/all/for patterns that fail Lean termination) in Validation, ValidationCalls, ValidationEvents, ValidationInterop, ValidationHelpers, ScopeValidation, UsageAnalysis, LogicalPurity - Param now derives BEq (needed for ADT field comparison) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Implement tagged-union storage layout for ADTs and wire compilation through to Yul output. Key changes: - New AdtStorageLayout.lean: layout helpers (tag slot, field slots, total footprint), Yul fragment generators for sload/sstore - Expr.adtField now carries pre-resolved fieldIndex + storageField (avoids threading adtTypes through 90+ compileExpr call sites) - compileExpr: adtTag → sload(base) & 0xFF, adtField → sload(base+i+1) - compileStmt: matchAdt → YulStmt.switch on tag with field bindings - compileMatchAdtBranches: explicit recursive helper (avoids for-loop termination issues in mutual blocks) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a64fac3fc4
ℹ️ 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".
| -- ecm, or expressions with call/staticcall/delegatecall/externalCall). | ||
| -- Internal calls are NOT treated as interactions here because each callee | ||
| -- function has its own CEI validation. | ||
| let newSeenCall := seenCall || stmtContainsExternalCall s |
There was a problem hiding this comment.
stmtListCEIViolation advances seenCall with stmtContainsExternalCall, which treats Stmt.internalCall as call-free unless one of its arguments contains an external call. That means a function can internalCall a helper that performs externalCallBind/tryExternalCallBind, then do setStorage in the caller, and CEI still passes because seenCall never flips to true in the caller frame. CEI needs to conservatively treat statement-form internal calls as potential interactions when updating post-call state.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c8da9816eb
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 56daaba7c7
ℹ️ 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".
| -- but are not visible at this scope). This catches the pattern: | ||
| -- externalCallBind(...) -- seenCall becomes true | ||
| -- internalCall(helper, [...]) -- may write storage → flagged | ||
| if !isCompound && newSeenCall && stmtMayPersistentlyWrite s then |
There was a problem hiding this comment.
stmtListCEIViolation updates seenCall before running the write-after-call check, so Stmt.internalCall/Stmt.internalCallAssign are treated as both "call seen" and "may write" in the same step and get rejected even when they are the first statement in the function. In practice this raises state write after external call without any prior interaction, making helper-only functions fail CEI unless they opt out; the post-interaction write check should be evaluated against the incoming call state (or a separate same-statement rule) rather than the already-updated flag.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 14230a258c
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 33bf07f6d6
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f8a2ffd7b9
ℹ️ 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".
| (f.aliasSlots.zipIdx.map (fun (aliasSlot, aliasIdx) => | ||
| (aliasSlot, s!"{f.name}.aliasSlots[{aliasIdx}]"))) |
There was a problem hiding this comment.
fieldOccupiedSlots only appends each alias base slot, but ADT writes are emitted to aliasBase + 1..maxFields as well (compileAdtStorageWrite writes payload/clear stores for every entry in aliasSlots). That means firstReservedSlotWriteConflict/firstFieldWriteSlotConflict can miss real overlaps on alias payload slots, so a contract with slotAliasRanges can pass layout validation while generated code still writes into reserved or conflicting slots.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1c9ab6ad6a
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b7e90f87d4
ℹ️ 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".
| baseSlots.flatMap fun slot => | ||
| argExprs.zipIdx.map fun (argExpr, idx) => | ||
| compileAdtFieldWrite (YulExpr.lit slot) idx argExpr |
There was a problem hiding this comment.
When ADT storage fields have alias slots, this loop emits one sstore per alias using the original payload argExpr each time, so side-effectful payload expressions (for example Expr.externalCall/Expr.internalCall arguments inside adtConstruct) are re-evaluated once per alias instead of once overall. That can trigger duplicate external/internal calls and diverging state updates compared to the source statement semantics. The non-ADT multi-slot path already memoizes via __compat_value; ADT writes need the same single-evaluation treatment for each payload argument.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 2 potential issues.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit b7e90f8. Configure here.
| else if !isCompound && newSeenCall && stmtMayPersistentlyWrite s then | ||
| some "state write after external call" | ||
| else | ||
| stmtListCEIViolation rest newSeenCall |
There was a problem hiding this comment.
CEI check over-flags every internal call statement
Medium Severity
newSeenCall is computed as seenCall || stmtMayContainExternalCall s and then used to check the current statement s for writes. Since stmtMayContainExternalCall returns true for every Stmt.internalCall and stmtMayPersistentlyWrite also returns true for every Stmt.internalCall, the second condition always fires for internal calls — even without any prior external call. This causes every function containing a statement-level internal call to fail CEI validation with a misleading "state write after external call" message. The propagation variable newSeenCall was intended for subsequent statements (per its comment) but is also applied to the current statement's write check, conflating "write after prior call" with "call+write in same callee."
Additional Locations (1)
Reviewed by Cursor Bugbot for commit b7e90f8. Configure here.
| stmtListMayPersistentlyWrite body | ||
| | Stmt.matchAdt _ _ branches => | ||
| matchBranchesMayPersistentlyWrite branches | ||
| | s => stmtIsPersistentWrite s |
There was a problem hiding this comment.
ECM write-state flag ignored in CEI analysis
Low Severity
stmtMayPersistentlyWrite for Stmt.ecm falls through to stmtIsPersistentWrite, which returns false via the catch-all case. This ignores the ECM module's mod.writesState flag. An ECM that writes to the current contract's storage after a prior external call wouldn't be flagged by CEI, even though stmtWritesState (used for view/pure validation) correctly checks mod.writesState for the same statement type.
Additional Locations (1)
Reviewed by Cursor Bugbot for commit b7e90f8. Configure here.
2 participants
Summary
Implements the complete language design improvement plan for Verity's
verity_contractEDSL — 25 steps across 6 axes, taking the language beyond Solidity parity with verified safety properties.63 files changed, +3349 / -235 lines
Axis 1: Effect System (Steps 1a–1d)
@[view]theorem generation (1a): Auto-generates_is_viewtheorems proving functions make no state writesmodifies(...)annotation (1b): Declares which storage fields a function may write; generates_frametheorem proving all other fields are preservedno_external_callsannotation (1c): Forbids external calls; generates_no_callstheorem_effectsconjunction theorem combining all individual guaranteesAxis 2: Safety Enforcement (Steps 2a–2c)
allow_post_interaction_writesnonreentrant(lock)generates reentrancy guard with_nonreentranttheorem;cei_safemarks functions as CEI-compliant by developer assertionrequires(role)access control (2c): Guards function entry onmsg.sender == role_field; generates_requires_roletheoremAxis 3: Newtypes (Steps 3a–3c)
typessection (3a):verityNewtypesyntax for zero-cost semantic wrappers (e.g.,TokenId : Uint256)ParamType.newtypeOfandValueType.newtypepropagate through all 11+ compilation model files; newtypes erase to their base type at every ABI/Yul boundaryAxis 4: Storage Safety (Steps 4a–4d)
computeStorageNamespacehashes the contract name via kernel Keccak at elaboration timestorage_namespacekeyword (4b): Opt-in; when present, allslot Nbecomeslot (namespaceBase + N)storage_namespace "custom.key"overrides the default contract-name hash{contract}.storage.jsonincludesstorageNamespace; layout reports include the namespace baseAxis 5: ADTs + External Calls (Steps 5a–5f)
inductivesection (5a): Grammar for algebraic data types with named variants and typed fieldsParamType.adt,Expr.adtConstruct/adtTag/adtField,Stmt.matchAdtacross ~17 compilation model files(uint8 tag, uint256 fields...);matchcompiles to Yulswitchon tagtryExternalCall(5f): Non-reverting external calls withCall.Resultreturn type;!sugar for force-unwrapadtTypesfield wired from parsed syntax through to specAxis 6: Unsafe Blocks (Steps 6a–6c)
unsafe "reason" dosyntax (6a): Wraps low-level operations requiring explicit justificationunsafewrapper--deny-unsafe(6c): Unsafe blocks appear in the trust report;--deny-unsafeflag rejects any unsafe usageBug Fixes (Post-Review)
Addresses all CI failures and review comments from Codex/Bugbot:
MacroExternal.storeEchoCEI violation fixed withallow_post_interaction_writesseenCallpropagated into branches; same-stmt call+write detection;stmtIsPersistentWritemade recursive for compound statementsexprContainsExternalCall: Added 11 missing Expr variantsExpr.storage→Expr.storageAddrfor address fieldsmappingStructsplit by key type (.address→storageMap,.uint256→storageMapUint)modifies():sepBy→sepBy1to reject empty clausemodifiesfieldTest plan
#check_contractpass in Smoke.lean (including new contracts: EffectAnnotationSmoke, ModifiesSmoke, NoExternalCallsSmoke, EffectCompositionSmoke, CEISmoke, CEILadderSmoke, RolesSmoke, NewtypeSmoke, NamespacedStorageSmoke, CustomNamespacedSmoke, AdtSmoke, UnsafeBlockSmoke, UnsafeGatingAccepted, ExternalCallMultiReturn, TryExternalCallSmoke, CEIViolationRejected)lake buildpasses (full build)make checkpasses (425 tests)🤖 Generated with Claude Code
Note
High Risk
High risk because it adds new IR constructs and modifies core validation/codegen paths (ABI encoding/decoding, storage writes, dispatch, trust reporting) with new safety rules that can change compilation behavior and reject previously-valid programs.
Overview
Implements a broad language/IR expansion: adds
ParamType.adt/FieldType.adtand ADT type definitions, plus new expressions/statements (Expr.adtTag/Expr.adtField,Stmt.matchAdt) with Yul lowering for tagged-union storage reads/writes and tuple-style ABI encoding/decoding (including event and custom-error support).Introduces zero-cost semantic newtypes via
ParamType.newtypeOf, threading erasure through ABI/type layout, param loading, and event normalization so newtypes compile identically to their base types.Adds new control/safety features in the IR and validation pipeline:
Stmt.tryExternalCallBind(non-reverting external calls with required{name}_trywrapper signature checks),Stmt.unsafeBlockwith trust-report integration (unsafe reasons surfaced and unguarded low-level mechanics gated), and effect/safety annotations onFunctionSpec(modifies(...),no_external_calls, and CEI enforcement rejecting state writes after interactions unless opted out).Extends tooling outputs by emitting
{contract}.storage.jsonstorage layout (including optional EIP-7201storageNamespace) and updating layout reports/validation to account for ADT multi-slot footprints and namespace metadata.Reviewed by Cursor Bugbot for commit b7e90f8. Bugbot is set up for automated code reviews on this repo. Configure here.