diff --git a/Compiler/CompilationModelFeatureTest.lean b/Compiler/CompilationModelFeatureTest.lean index 5d94b9876..ea4fcdb69 100644 --- a/Compiler/CompilationModelFeatureTest.lean +++ b/Compiler/CompilationModelFeatureTest.lean @@ -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 }] @@ -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 := [] @@ -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 := [] @@ -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" diff --git a/Compiler/Modules/Hashing.lean b/Compiler/Modules/Hashing.lean index 87bcd8805..0ffdea2bd 100644 --- a/Compiler/Modules/Hashing.lean +++ b/Compiler/Modules/Hashing.lean @@ -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}" @@ -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