Skip to content

Thread length into static array ABI hashing #1864

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Th0rgal merged 1 commit into from
May 14, 2026
+19 −14
Merged

Thread length into static array ABI hashing #1864

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions Compiler/CompilationModelFeatureTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3092,7 +3092,8 @@ private def abiEncodeStaticArraySmokeSpec : CompilationModel := {
returnType := none
returns := [ParamType.bytes32]
body := [
Compiler.Modules.Hashing.abiEncodeStaticArray "digest" "items" 4,
Compiler.Modules.Hashing.abiEncodeStaticArray
"digest" "items" 4 (Expr.arrayLength "items"),
Stmt.returnValues [Expr.localVar "digest"]
]
}
Expand Down Expand Up @@ -3187,7 +3188,7 @@ private def abiEncodeStaticArrayBadAritySpec : CompilationModel := {
returnType := none
body := [
Stmt.ecm (Compiler.Modules.Hashing.abiEncodeStaticArrayModule "digest" "items" 1)
[Expr.param "items"],
[Expr.arrayLength "items", Expr.literal 0],
Stmt.stop
]
}
Expand All @@ -3203,7 +3204,8 @@ private def abiEncodeStaticArrayBadWidthSpec : CompilationModel := {
params := [{ name := "items", ty := ParamType.array ParamType.uint256 }]
returnType := none
body := [
Compiler.Modules.Hashing.abiEncodeStaticArray "digest" "items" 0,
Compiler.Modules.Hashing.abiEncodeStaticArray
"digest" "items" 0 (Expr.arrayLength "items"),
Stmt.stop
]
}
Expand Down Expand Up @@ -4427,7 +4429,7 @@ set_option maxRecDepth 4096 in
expectCompileErrorContains
"abiEncodeStaticArray ECM rejects invalid argument counts"
abiEncodeStaticArrayBadAritySpec
"uses ECM 'abiEncodeStaticArray' with 1 arguments but it expects 0"
"uses ECM 'abiEncodeStaticArray' with 2 arguments but it expects 1"
expectCompileErrorContains
"abiEncodeStaticArray rejects zero-width elements"
abiEncodeStaticArrayBadWidthSpec
Expand Down
23 changes: 13 additions & 10 deletions Compiler/Modules/Hashing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,9 +98,9 @@ def abiEncodePacked (resultVar : String) (words : List Expr) : Stmt :=
/-- Keccak-256 over Solidity `abi.encode(array)` for a direct dynamic-array
parameter whose elements have a fixed static word width.

The module references `{arrayParam}_length` and `{arrayParam}_data_offset`
emitted by the calldata/internal dynamic-array lowering. It encodes the
single dynamic-array argument as:
The module takes the array length as its single expression argument and
references `{arrayParam}_data_offset` emitted by the calldata/internal
dynamic-array lowering. It encodes the single dynamic-array argument as:

head offset (32), array length, contiguous static element words

Expand All @@ -109,14 +109,16 @@ def abiEncodePacked (resultVar : String) (words : List Expr) : Stmt :=
def abiEncodeStaticArrayModule
(resultVar arrayParam : String) (elementWords : Nat) : ExternalCallModule where
name := "abiEncodeStaticArray"
numArgs := 0
numArgs := 1
resultVars := [resultVar]
writesState := false
readsState := false
axioms := ["keccak256_memory_slice_matches_evm", "abi_standard_dynamic_array_static_element_layout"]
compile := fun ctx args => do
if !args.isEmpty then
throw s!"abiEncodeStaticArray expects 0 expression argument(s), got {args.length}"
let arrayLengthExpr ←
match args with
| [arrayLengthExpr] => pure arrayLengthExpr
| _ => throw s!"abiEncodeStaticArray expects 1 expression argument, got {args.length}"
if arrayParam.isEmpty then
throw "abiEncodeStaticArray requires a non-empty array parameter name"
if elementWords == 0 then
Expand All @@ -134,10 +136,10 @@ def abiEncodeStaticArrayModule
YulStmt.expr (YulExpr.call "mstore" [ptr, YulExpr.lit 32]),
YulStmt.expr (YulExpr.call "mstore" [
YulExpr.call "add" [ptr, YulExpr.lit 32],
YulExpr.ident s!"{arrayParam}_length"
arrayLengthExpr
]),
YulStmt.let_ dataBytesName (YulExpr.call "mul" [
YulExpr.ident s!"{arrayParam}_length",
arrayLengthExpr,
Copy link
Copy Markdown

@cursor cursor Bot May 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Array length expression inlined twice without binding

Low Severity

arrayLengthExpr is used twice in the generated Yul block (in mstore at the first use and mul at the second) without being bound to a Yul let variable first. The old code was inherently safe because it hardcoded YulExpr.ident s!"{arrayParam}_length", always a simple variable reference. The new code accepts an arbitrary compiled YulExpr, which gets duplicated in the AST. Other modules in the same file (e.g., abiEncodePackedWordsModule) use packedWordBindings to bind each argument expression to a local before use. Introducing a let binding for the length expression would match the established convention and prevent double evaluation if a non-trivial expression is ever supplied.

Fix in Cursor Fix in Web

Reviewed by Cursor Bugbot for commit b511cec. Configure here.

YulExpr.lit (elementWords * 32)
])
] ++ ECM.dynamicCopyData ctx
Expand All @@ -159,8 +161,9 @@ def abiEncodeStaticArrayModule

/-- Convenience constructor for `keccak256(abi.encode(array))` over static-width
dynamic-array parameters. -/
def abiEncodeStaticArray (resultVar arrayParam : String) (elementWords : Nat) : Stmt :=
.ecm (abiEncodeStaticArrayModule resultVar arrayParam elementWords) []
def abiEncodeStaticArray
(resultVar arrayParam : String) (elementWords : Nat) (arrayLength : Expr) : Stmt :=
.ecm (abiEncodeStaticArrayModule resultVar arrayParam elementWords) [arrayLength]

/-- Keccak-256 over packed static byte-width segments.
Each argument is encoded as exactly the matching byte width from `widths`,
Expand Down
Loading