verity#1849 G1: dynamic-member length on struct-array elements#1852
Merged
Conversation
… IR side)
Introduces the new `Expr.arrayElementDynamicMemberLength` IR constructor
that reads the length word of a dynamically-sized member (`Array<T>`,
`bytes`, `string`) nested inside a struct-array element. This is G1 of
the three macro lifts identified in verity#1849 as the remaining
Verity-core gate on the UnlinkPool body translation.
## Semantics
Given a struct-array parameter `name` indexed at `index`, with the
dynamic member's head pointer at `wordOffset` (relative to the
element's head section), the Yul lowering:
1. bounds-checks `index < length`;
2. loads `__element_rel_offset` from the array's offset table;
3. bounds-checks the element offset against `length*32` (offset table size);
4. loads `__member_rel_offset` from the element head at `wordOffset`;
5. bounds-checks the final member-data position against `calldatasize`
(calldata variant only — the memory variant trusts its source);
6. returns the length word at `element_head + __member_rel_offset`.
The dynamic-member head pointer is element-relative per Solidity's
ABI: `__member_data_pos = element_head + __member_rel_offset` where
`element_head = data_offset + __element_rel_offset`.
## Surface coverage
- `Compiler/CompilationModel/Types.lean` — constructor.
- `Compiler/CompilationModel/DynamicData.lean` — `checkedArrayElementDynamicMemberLength{Calldata,Memory}Helper` Yul helpers.
- `Compiler/CompilationModel/ExpressionCompile.lean` — IR-to-Yul lowering.
- `Compiler/CompilationModel/Dispatch.lean` — emit helpers under existing `arrayElementWord` gate (conservative; correctly tracks usage without a new predicate).
- `Compiler/CompilationModel/UsageAnalysis.lean` — 6 sites: `exprUsesArrayElementKind`, `exprUsesArrayElement`, `exprUsesParamDynamicHeadWord`, `exprUsesMulDiv512`, `exprUsesStorageArrayElement`, `exprUsesDynamicBytesEq`.
- `Compiler/CompilationModel/Validation*.lean` — read/write/external-call surfaces (`exprReadsStateOrEnv`, `exprWritesState`, `exprHasUntrackableWrites`, `exprContainsExternalCall`, `exprMayContainExternalCall`, `exprContainsAdtConstruct`, internal-call shapes, external-call targets, interop).
- `Compiler/CompilationModel/ValidationHelpers.lean` — `collectExprNames`.
- `Compiler/CompilationModel/LogicalPurity.lean` — `exprContainsCallLike`, `exprContainsUnsafeLogicalCallLike`.
- `Compiler/CompilationModel/ScopeValidation.lean` — scope/type check for the new constructor (mirrors `arrayElementDynamicWord`).
- `Compiler/CompilationModel/TrustSurface.lean` — 5 collect-* sites.
- `Compiler/Proofs/IRGeneration/ExprCore.lean` — `exprBoundNames`.
- `Compiler/Proofs/IRGeneration/SupportedSpec.lean` — 12 exhaustiveness cases across `exprTouchesUnsupported*Surface` defs and the `exprTouchesUnsupportedCallSurface_eq_featureOr` / `exprTouchesUnsupportedContractSurface_eq_false_of_featureClosed` / `exprTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed` decomposition proofs, plus `exprInternalHelperCallNames`.
The new constructor joins `paramDynamicHeadWord` / `arrayElementDynamicWord` as an unsupported-core surface — contracts that use it are rejected by `SupportedSpec` until the proof framework widens, which is the same posture as the existing dynamic-member shape primitives.
`lake build` is fully green.
Macro-side parser extension (`Verity/Macro/Translate.lean`) plus the
companion smoke test and 5-site registration come in a follow-up
commit; the IR-level infrastructure is the audit-touching half and is
worth a separate commit for review.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Wires the previously added `Expr.arrayElementDynamicMemberLength` IR
constructor into the `verity_contract` DSL by extending `arrayLength`
to accept compound projections of the form
`arrayLength (arrayElement <param> <i>).<dynamicField>` when
`<dynamicField>` is a dynamic member (`Array<T>`, `bytes`, `string`) of
the struct-array element type.
## Changes
- `Verity/Macro/Translate.lean`:
- New `arrayElementDynamicMemberProjection?` helper that mirrors
`arrayElementStructProjection?` but accepts dynamic-leaf field
types (Array / bytes / string) instead of single-word static
leaves.
- Type-check path: extend `arrayLength` to consult the new helper
and accept the compound projection (returning `.uint256`).
- Lowering path: extend `arrayLength` to emit
`Expr.arrayElementDynamicMemberLength` with the resolved
`(paramName, indexExpr, wordOffset)` when the new helper fires.
- `Contracts/Smoke/ArrayElementDynamicMemberLengthSmoke.lean`: new
smoke contract with a `Transaction` struct whose `proof : Array
Uint256` is the first dynamic member. The function
`proofLength (txs, idx)` returns `arrayLength (arrayElement txs idx).proof`.
An `rfl` assertion over `proofLength_modelBody` proves the macro
lowers to `Expr.arrayElementDynamicMemberLength "txs" (param "idx") 0`.
- `Contracts/MacroTranslateInvariantTest.lean`: register the new smoke
in the `macroSpecs` list, `expectedExternalSignatures`
(`proofLength((uint256[],address,uint256)[],uint256)`), and
`expectedExternalSelectors` (`0xfbb81f5b`).
- `Contracts/MacroTranslateRoundTripFuzz.lean`: register in the
round-trip spec list.
- `scripts/check_macro_property_test_generation.py`: add
`ArrayElementDynamicMemberLengthSmoke` to `EXCLUDED_CONTRACTS`
alongside `DynamicStructArraySmoke` — the property generator does
not yet synthesize Solidity examples for struct-array parameters
with nested dynamic members, but Lean macro/invariant/round-trip
coverage exercises the contract.
## Unblocks
This was G1 of verity#1849. Authors of contracts that translate
struct-array entrypoints (e.g. UnlinkPool's `transfer` / `withdraw` /
`emergencyWithdraw`) can now emit shape-check reverts such as
```lean
requireError
(cmp_eq (arrayLength (arrayElement txs i).nullifierHashes) c.inputCount)
PoolInvalidInputShape ()
```
`lake build Contracts.MacroTranslateInvariantTest` is green locally;
`scripts/check_macro_health.py` reports "macro health checks passed".
G2 (element indexing on struct-element dynamic members) and G3
(pass-through to external calls / emit / revertError) plus
verity#1824 (helpers with Array parameters) remain.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 9f515b4. Configure here.
| YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0]) | ||
| ], | ||
| YulStmt.let_ "__element_head_pos" elementHeadPos, | ||
| YulStmt.let_ "__member_rel_offset" (YulExpr.call loadOp [memberHeadSlot]), |
There was a problem hiding this comment.
Missing bounds check on intermediate calldataload position
Medium Severity
The checkedArrayElementDynamicMemberLengthHelper reads __member_rel_offset from memberHeadSlot (line 248) without first bounds-checking that position against calldatasize. The analogous checkedArrayElementDynamicWordHelper does bounds-check its equivalent read position (__element_word_pos) before loading. Since __member_rel_offset is attacker-controlled calldata, a crafted value can cause __element_head_pos + __member_rel_offset to overflow mod 2²⁵⁶, producing a small __member_data_pos that passes the final sizeCheck and reads from an unintended calldata position.
Additional Locations (1)
Reviewed by Cursor Bugbot for commit 9f515b4. Configure here.
Contributor
| \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``` |
4 tasks
Th0rgal
added a commit
that referenced
this pull request
May 13, 2026
…, IR + macro spike) Introduces the new `Expr.arrayElementDynamicMemberElement` IR constructor that reads element `inner_index` of a dynamic word-array member nested inside a struct-array element. This is G2 of verity#1849. ## Semantics Given a struct-array parameter `name` indexed at `index`, with the dynamic member's head pointer at `wordOffset` (relative to the element's head section), the Yul lowering: 1. bounds-checks `index < length` (outer array); 2. loads `__element_rel_offset` from the outer offset table; 3. bounds-checks the element offset against `length*32`; 4. loads `__member_rel_offset` from the element head at `wordOffset`; 5. computes `__member_data_pos = element_head + __member_rel_offset`, which holds the dynamic member's length word followed by its data; 6. loads `__member_length` from `__member_data_pos`; 7. bounds-checks `inner_index < __member_length`; 8. computes `__word_pos = __member_data_pos + 32 + inner_index*32`; 9. bounds-checks `__word_pos` against `calldatasize` (calldata variant only — the memory variant trusts its source); 10. returns `load(__word_pos)`. ## Surface coverage The same 15-file pattern as G1 (#1852) plus an `set_option maxHeartbeats 800000` in `ScopeValidation.lean` to keep the eq_def deriver inside its budget after the new constructor was added to the giant mutual block. Each `Expr → ...` surface def now handles the 2-sub-expression shape (both `index` and `inner_index`) when recursion is appropriate, or treats the new constructor as a leaf alongside `paramDynamicHeadWord` / `arrayElementDynamicWord` / `arrayElementDynamicMemberLength` in the `exprTouchesUnsupported*Surface` family. ## Macro spike `Verity/Macro/Translate.lean` extends `arrayElement`'s `inferPureExprType` and `translatePureExprWithTypes` arms to detect the compound projection `(arrayElement <param> <i>).<dynamicField>` and lower through `Expr.arrayElementDynamicMemberElement`. The detection uses the existing `arrayElementDynamicMemberProjection?` helper from G1. **Known follow-up**: an end-to-end smoke that reaches the new lowering path (e.g. `function f (...) := return arrayElement (arrayElement txs idx).proof k`) currently still errors on the compilation-model gate before the new macro arm fires; the lowering edits are committed as a spike alongside the IR-side infrastructure but a smoke proving the macro path lights up requires a small additional fix to be debugged in a follow-up. `lake build` is fully green; the new IR constructor is callable directly via `Compiler.CompilationModel.Expr.arrayElementDynamicMemberElement` which is enough for hand-built IR tests and Layer-2 proof callers. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Th0rgal
added a commit
that referenced
this pull request
May 13, 2026
…, IR + macro spike) (#1853) Introduces the new `Expr.arrayElementDynamicMemberElement` IR constructor that reads element `inner_index` of a dynamic word-array member nested inside a struct-array element. This is G2 of verity#1849. ## Semantics Given a struct-array parameter `name` indexed at `index`, with the dynamic member's head pointer at `wordOffset` (relative to the element's head section), the Yul lowering: 1. bounds-checks `index < length` (outer array); 2. loads `__element_rel_offset` from the outer offset table; 3. bounds-checks the element offset against `length*32`; 4. loads `__member_rel_offset` from the element head at `wordOffset`; 5. computes `__member_data_pos = element_head + __member_rel_offset`, which holds the dynamic member's length word followed by its data; 6. loads `__member_length` from `__member_data_pos`; 7. bounds-checks `inner_index < __member_length`; 8. computes `__word_pos = __member_data_pos + 32 + inner_index*32`; 9. bounds-checks `__word_pos` against `calldatasize` (calldata variant only — the memory variant trusts its source); 10. returns `load(__word_pos)`. ## Surface coverage The same 15-file pattern as G1 (#1852) plus an `set_option maxHeartbeats 800000` in `ScopeValidation.lean` to keep the eq_def deriver inside its budget after the new constructor was added to the giant mutual block. Each `Expr → ...` surface def now handles the 2-sub-expression shape (both `index` and `inner_index`) when recursion is appropriate, or treats the new constructor as a leaf alongside `paramDynamicHeadWord` / `arrayElementDynamicWord` / `arrayElementDynamicMemberLength` in the `exprTouchesUnsupported*Surface` family. ## Macro spike `Verity/Macro/Translate.lean` extends `arrayElement`'s `inferPureExprType` and `translatePureExprWithTypes` arms to detect the compound projection `(arrayElement <param> <i>).<dynamicField>` and lower through `Expr.arrayElementDynamicMemberElement`. The detection uses the existing `arrayElementDynamicMemberProjection?` helper from G1. **Known follow-up**: an end-to-end smoke that reaches the new lowering path (e.g. `function f (...) := return arrayElement (arrayElement txs idx).proof k`) currently still errors on the compilation-model gate before the new macro arm fires; the lowering edits are committed as a spike alongside the IR-side infrastructure but a smoke proving the macro path lights up requires a small additional fix to be debugged in a follow-up. `lake build` is fully green; the new IR constructor is callable directly via `Compiler.CompilationModel.Expr.arrayElementDynamicMemberElement` which is enough for hand-built IR tests and Layer-2 proof callers. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Implements G1 of verity#1849 — the smallest of the three macro lifts needed to translate the UnlinkPool
transfer/withdraw/emergencyWithdrawbodies. After this lands,verity_contractauthors can writeto read the length of a dynamic-array member nested inside a struct-array element — the macro lowers it to a new
Expr.arrayElementDynamicMemberLengthconstructor with a verified Yul helper.What's covered
Expr.arrayElementDynamicMemberLength (name : String) (index : Expr) (wordOffset : Nat)constructor inCompiler/CompilationModel/Types.lean, with calldata + memory Yul helpers inDynamicData.lean. The helpers bounds-check the index against the array length, the element-relative offset against the offset-table size, and the final member-data position againstcalldatasize(calldata variant only).Expr → ...def that the audit step (post-Fix audit-step exhaustiveness errors after #1761 / #1832 #1848) requires exhaustive —UsageAnalysis.lean(6 sites),Validation.lean(6 sites),ValidationInterop.lean,ValidationCalls.lean(2 sites),ValidationHelpers.lean,LogicalPurity.lean(2 sites),ScopeValidation.lean,TrustSurface.lean(5 sites),ExprCore.lean,SupportedSpec.lean(12 sites including the exhaustiveness cases and thefeatureOr/featureCloseddecomposition proofs), andDispatch.lean(emit the new helpers under the existingarrayElementWordgate).arrayElementDynamicMemberProjection?helper inTranslate.leanthat mirrorsarrayElementStructProjection?but accepts dynamic-leaf field types. ExtendsarrayLengthtype-check + lowering to consult the new helper.Contracts/Smoke/ArrayElementDynamicMemberLengthSmoke.leandefines aTransactionstruct withproof : Array Uint256and a functionproofLengththat exercises the new constructor.rflassertion overproofLength_modelBodyproves the IR shape.Posture
The new constructor joins
paramDynamicHeadWord/arrayElementDynamicWordas an unsupported-core surface — contracts that use it are accepted by the macro but rejected by the strictSupportedSpecuntil the proof framework widens. This is the same posture #1832 / #1843 took for their codegen-only additions and is what lets the audit step pass without a newcontractUsesArrayElementDynamicMemberLength_eq_falseproof chain.Test plan
lake buildis fully green locally.lake build Contracts.MacroTranslateInvariantTestpasses the 8/8 randomized IR↔Yul differential checks and the ABI parity checks.scripts/check_macro_health.pyreports "macro health checks passed".scripts/check_macro_property_test_generation.py --checkis green (the new smoke is inEXCLUDED_CONTRACTSalongsideDynamicStructArraySmokebecause the property generator doesn't yet synthesize Solidity examples for struct-array parameters with nested dynamic members).What's next
This unblocks emitting shape-check reverts (
PoolInvalidInputShape/PoolInvalidOutputShape/PoolCiphertextCountMismatch) inside loops over_transactions. The remaining gaps to writeUnlinkPoolbodies are:txn.nullifierHashes[k]). Same shape as G1 but with one further bounds-checked word read.Array<wordLike>totryExternalCall/emit/revertErrorargument lists.🤖 Generated with Claude Code
Note
Medium Risk
Adds a new IR surface and Yul helper for reading dynamic-member lengths inside ABI-encoded struct-array elements, touching macro translation and multiple validation/proof exhaustiveness sites; mistakes could cause incorrect bounds checks or miscompiled calldata reads.
Overview
Enables
arrayLength (arrayElement <structArrayParam> i).<dynamicField>by introducing a new IR constructorExpr.arrayElementDynamicMemberLengthand lowering it to new calldata/memory Yul helpers that bounds-check the array index, element offset-table access, and (for calldata) the final member-data read.Wires the new expression through expression compilation, scope/purity/usage/validation/trust-surface analyses, and updates helper emission in
Dispatch.lean(reusing the existingarrayElementWordhelper gate). Adds a dedicated smoke contract and includes it in macro invariant + round-trip fuzz test suites, while excluding it from the macro property-test generator.Reviewed by Cursor Bugbot for commit 9f515b4. Bugbot is set up for automated code reviews on this repo. Configure here.