diff --git a/Compiler/CompilationModelFeatureTest.lean b/Compiler/CompilationModelFeatureTest.lean
index ea4fcdb69..439440340 100644
--- a/Compiler/CompilationModelFeatureTest.lean
+++ b/Compiler/CompilationModelFeatureTest.lean
@@ -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"]
       ]
     }
@@ -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
       ]
     }
@@ -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
       ]
     }
@@ -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
diff --git a/Compiler/Modules/Hashing.lean b/Compiler/Modules/Hashing.lean
index 0ffdea2bd..8e17a5f11 100644
--- a/Compiler/Modules/Hashing.lean
+++ b/Compiler/Modules/Hashing.lean
@@ -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
 
@@ -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
@@ -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,
           YulExpr.lit (elementWords * 32)
         ])
       ] ++ ECM.dynamicCopyData ctx
@@ -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`,