Skip to content

Support ABI hashing for static dynamic arrays #1863

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
+148 −9
Merged

Support ABI hashing for static dynamic arrays #1863

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
88 changes: 80 additions & 8 deletions Compiler/CompilationModelFeatureTest.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2536,14 +2536,6 @@ private def adtAliasPayloadMemoizesExprSpec : CompilationModel := {
{ name := "choice", ty := FieldType.adt "Choice" 1, «slot» := some 10, aliasSlots := [100] }
]
«constructor» := none
externals := [
{ name := "echo"
params := [ParamType.uint256]
returnType := some ParamType.uint256
returns := [ParamType.uint256]
axiomNames := []
}
]
functions := [
{ name := "store"
params := [{ name := "input", ty := ParamType.uint256 }]
Expand Down Expand Up @@ -3086,6 +3078,27 @@ private def sha256PackedWordsSmokeSpec : CompilationModel := {
]
}

private def abiEncodeStaticArraySmokeSpec : CompilationModel := {
name := "AbiEncodeStaticArraySmoke"
fields := []
«constructor» := none
functions := [
{ name := "hash"
params := [
{ name := "items", ty := ParamType.array (ParamType.tuple [
ParamType.uint256, ParamType.fixedArray ParamType.uint256 3
]) }
]
returnType := none
returns := [ParamType.bytes32]
body := [
Compiler.Modules.Hashing.abiEncodeStaticArray "digest" "items" 4,
Stmt.returnValues [Expr.localVar "digest"]
]
}
]
}

private def abiEncodePackedStaticSegmentsSmokeSpec : CompilationModel := {
name := "AbiEncodePackedStaticSegmentsSmoke"
fields := []
Expand Down Expand Up @@ -3164,6 +3177,39 @@ private def abiEncodePackedWordsBadAritySpec : CompilationModel := {
]
}

private def abiEncodeStaticArrayBadAritySpec : CompilationModel := {
name := "AbiEncodeStaticArrayBadArity"
fields := []
«constructor» := none
functions := [
{ name := "bad"
params := [{ name := "items", ty := ParamType.array ParamType.uint256 }]
returnType := none
body := [
Stmt.ecm (Compiler.Modules.Hashing.abiEncodeStaticArrayModule "digest" "items" 1)
[Expr.param "items"],
Stmt.stop
]
}
]
}

private def abiEncodeStaticArrayBadWidthSpec : CompilationModel := {
name := "AbiEncodeStaticArrayBadWidth"
fields := []
«constructor» := none
functions := [
{ name := "bad"
params := [{ name := "items", ty := ParamType.array ParamType.uint256 }]
returnType := none
body := [
Compiler.Modules.Hashing.abiEncodeStaticArray "digest" "items" 0,
Stmt.stop
]
}
]
}

private def sha256PackedWordsBadAritySpec : CompilationModel := {
name := "Sha256PackedWordsBadArity"
fields := []
Expand Down Expand Up @@ -4365,6 +4411,32 @@ set_option maxRecDepth 4096 in
contains abiEncodePackedWordsYul "mstore(64, __packed_word_2)")
expectTrue "abiEncodePackedWords hashes the exact packed byte length"
(contains abiEncodePackedWordsYul "let digest := keccak256(0, 96)")
let abiEncodeStaticArrayYul ←
expectCompileToYul "abiEncodeStaticArray smoke spec" abiEncodeStaticArraySmokeSpec
expectTrue "abiEncodeStaticArray writes the single dynamic argument head and length"
(contains abiEncodeStaticArrayYul "mstore(__digest_abi_array_ptr, 32)" &&
contains abiEncodeStaticArrayYul "mstore(add(__digest_abi_array_ptr, 32), items_length)")
expectTrue "abiEncodeStaticArray copies the fixed-width element payload"
(contains abiEncodeStaticArrayYul
"let __digest_abi_array_data_bytes := mul(items_length, 128)" &&
contains abiEncodeStaticArrayYul
"calldatacopy(add(__digest_abi_array_ptr, 64), items_data_offset, __digest_abi_array_data_bytes)")
expectTrue "abiEncodeStaticArray hashes the ABI-encoded dynamic array byte length"
(contains abiEncodeStaticArrayYul
"let digest := keccak256(__digest_abi_array_ptr, __digest_abi_array_total_bytes)")
expectCompileErrorContains
"abiEncodeStaticArray ECM rejects invalid argument counts"
abiEncodeStaticArrayBadAritySpec
"uses ECM 'abiEncodeStaticArray' with 1 arguments but it expects 0"
expectCompileErrorContains
"abiEncodeStaticArray rejects zero-width elements"
abiEncodeStaticArrayBadWidthSpec
"abiEncodeStaticArray requires elementWords > 0"
let abiEncodeStaticArrayTrustReport := emitTrustReportJson [abiEncodeStaticArraySmokeSpec]
expectTrue "abiEncodeStaticArray trust report surfaces array layout and keccak assumptions"
(contains abiEncodeStaticArrayTrustReport "\"module\":\"abiEncodeStaticArray\"" &&
contains abiEncodeStaticArrayTrustReport "\"assumption\":\"abi_standard_dynamic_array_static_element_layout\"" &&
contains abiEncodeStaticArrayTrustReport "\"assumption\":\"keccak256_memory_slice_matches_evm\"")
let sha256PackedWordsYul ←
expectCompileToYul "sha256PackedWords smoke spec" sha256PackedWordsSmokeSpec
expectTrue "sha256PackedWords evaluates source words before clobbering scratch memory"
Expand Down
69 changes: 68 additions & 1 deletion Compiler/Modules/Hashing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ namespace Compiler.Modules.Hashing

open Compiler.Yul
open Compiler.ECM
open Compiler.CompilationModel (Stmt Expr)
open Compiler.CompilationModel (Stmt Expr freeMemoryPointer)

private def packedWordTempName (idx : Nat) : String :=
s!"__packed_word_{idx}"
Expand Down Expand Up @@ -95,6 +95,73 @@ def abiEncodePackedWords (resultVar : String) (words : List Expr) : Stmt :=
def abiEncodePacked (resultVar : String) (words : List Expr) : Stmt :=
abiEncodePackedWords resultVar words

/-- 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:

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

This covers arrays such as `uint256[]`, `address[]`, and arrays of static
tuples/structs when the caller supplies the element word width. -/
def abiEncodeStaticArrayModule
(resultVar arrayParam : String) (elementWords : Nat) : ExternalCallModule where
name := "abiEncodeStaticArray"
numArgs := 0
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}"
if arrayParam.isEmpty then
throw "abiEncodeStaticArray requires a non-empty array parameter name"
if elementWords == 0 then
throw "abiEncodeStaticArray requires elementWords > 0"
let ptrName := s!"__{resultVar}_abi_array_ptr"
let dataBytesName := s!"__{resultVar}_abi_array_data_bytes"
let totalBytesName := s!"__{resultVar}_abi_array_total_bytes"
let paddedTotalName := s!"__{resultVar}_abi_array_padded_total"
let ptr := YulExpr.ident ptrName
let dataBytes := YulExpr.ident dataBytesName
let totalBytes := YulExpr.ident totalBytesName
pure [
YulStmt.block ([
YulStmt.let_ ptrName (YulExpr.call "mload" [YulExpr.lit freeMemoryPointer]),
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"
]),
YulStmt.let_ dataBytesName (YulExpr.call "mul" [
YulExpr.ident s!"{arrayParam}_length",
YulExpr.lit (elementWords * 32)
])
] ++ ECM.dynamicCopyData ctx
(YulExpr.call "add" [ptr, YulExpr.lit 64])
(YulExpr.ident s!"{arrayParam}_data_offset")
dataBytes ++ [
YulStmt.let_ totalBytesName (YulExpr.call "add" [YulExpr.lit 64, dataBytes]),
YulStmt.let_ paddedTotalName (YulExpr.call "and" [
YulExpr.call "add" [totalBytes, YulExpr.lit 31],
YulExpr.call "not" [YulExpr.lit 31]
]),
YulStmt.expr (YulExpr.call "mstore" [
YulExpr.lit freeMemoryPointer,
YulExpr.call "add" [ptr, YulExpr.ident paddedTotalName]
]),
YulStmt.let_ resultVar (YulExpr.call "keccak256" [ptr, totalBytes])
])
]

/-- 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) []

/-- Keccak-256 over packed static byte-width segments.
Each argument is encoded as exactly the matching byte width from `widths`,
using Solidity's left-aligned memory representation for sub-word static
Expand Down