diff --git a/Compiler/CompilationModelFeatureTest.lean b/Compiler/CompilationModelFeatureTest.lean
index 2f3624b65..a6a05f289 100644
--- a/Compiler/CompilationModelFeatureTest.lean
+++ b/Compiler/CompilationModelFeatureTest.lean
@@ -1,8 +1,10 @@
 import Compiler.CompilationModel
 import Compiler.ABI
 import Compiler.Codegen
+import Compiler.Modules.Calls
 import Compiler.Modules.ERC4626
 import Compiler.Modules.ERC20
+import Compiler.Modules.Hashing
 import Compiler.Modules.Oracle
 import Compiler.Modules.Precompiles
 import Compiler.Yul.PrettyPrint
@@ -2580,6 +2582,26 @@ private def uintArrayElementOnlySpec : CompilationModel := {
   ]
 }
 
+private def uintArrayForEachAccumulatorSpec : CompilationModel := {
+  name := "UintArrayForEachAccumulator"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "sum"
+      params := [{ name := "values", ty := ParamType.array ParamType.uint256 }]
+      returnType := some FieldType.uint256
+      body := [
+        Stmt.letVar "total" (Expr.literal 0),
+        Stmt.forEach "i" (Expr.arrayLength "values") [
+          Stmt.letVar "value" (Expr.arrayElement "values" (Expr.localVar "i")),
+          Stmt.assignVar "total" (Expr.add (Expr.localVar "total") (Expr.localVar "value"))
+        ],
+        Stmt.return (Expr.localVar "total")
+      ]
+    }
+  ]
+}
+
 private def tupleArrayElementWordOnlySpec : CompilationModel := {
   name := "TupleArrayElementWordOnly"
   fields := []
@@ -2694,6 +2716,272 @@ private def ecrecoverSmokeSpec : CompilationModel := {
   ]
 }
 
+private def sha256MemorySmokeSpec : CompilationModel := {
+  name := "Sha256MemorySmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "hash"
+      params := [
+        { name := "inputOffset", ty := ParamType.uint256 }
+        , { name := "inputSize", ty := ParamType.uint256 }
+        , { name := "outputOffset", ty := ParamType.uint256 }
+      ]
+      returnType := none
+      returns := [ParamType.bytes32]
+      body := [
+        Compiler.Modules.Precompiles.sha256
+          "digest"
+          (Expr.param "inputOffset")
+          (Expr.param "inputSize")
+          (Expr.param "outputOffset"),
+        Stmt.returnValues [Expr.localVar "digest"]
+      ]
+    }
+  ]
+}
+
+private def sha256MemoryTwiceSmokeSpec : CompilationModel := {
+  name := "Sha256MemoryTwiceSmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "hashBoth"
+      params := [
+        { name := "inputOffset", ty := ParamType.uint256 }
+        , { name := "inputSize", ty := ParamType.uint256 }
+        , { name := "firstOutputOffset", ty := ParamType.uint256 }
+        , { name := "secondOutputOffset", ty := ParamType.uint256 }
+      ]
+      returnType := none
+      returns := [ParamType.bytes32, ParamType.bytes32]
+      body := [
+        Compiler.Modules.Precompiles.sha256
+          "firstDigest"
+          (Expr.param "inputOffset")
+          (Expr.param "inputSize")
+          (Expr.param "firstOutputOffset"),
+        Compiler.Modules.Precompiles.sha256
+          "secondDigest"
+          (Expr.param "inputOffset")
+          (Expr.param "inputSize")
+          (Expr.param "secondOutputOffset"),
+        Stmt.returnValues [Expr.localVar "firstDigest", Expr.localVar "secondDigest"]
+      ]
+    }
+  ]
+}
+
+private def abiEncodePackedWordsSmokeSpec : CompilationModel := {
+  name := "AbiEncodePackedWordsSmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "hash"
+      params := [
+        { name := "a", ty := ParamType.bytes32 }
+        , { name := "b", ty := ParamType.bytes32 }
+        , { name := "c", ty := ParamType.bytes32 }
+      ]
+      returnType := none
+      returns := [ParamType.bytes32]
+      body := [
+        Compiler.Modules.Hashing.abiEncodePacked
+          "digest"
+          [Expr.param "a", Expr.param "b", Expr.param "c"],
+        Stmt.returnValues [Expr.localVar "digest"]
+      ]
+    }
+  ]
+}
+
+private def sha256PackedWordsSmokeSpec : CompilationModel := {
+  name := "Sha256PackedWordsSmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "hash"
+      params := [
+        { name := "root", ty := ParamType.bytes32 }
+        , { name := "context", ty := ParamType.bytes32 }
+      ]
+      returnType := none
+      returns := [ParamType.bytes32]
+      body := [
+        Compiler.Modules.Hashing.sha256Packed
+          "digest"
+          [Expr.param "root", Expr.param "context"],
+        Stmt.returnValues [Expr.localVar "digest"]
+      ]
+    }
+  ]
+}
+
+private def abiEncodePackedStaticSegmentsSmokeSpec : CompilationModel := {
+  name := "AbiEncodePackedStaticSegmentsSmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "hash"
+      params := [
+        { name := "who", ty := ParamType.address }
+        , { name := "amount", ty := ParamType.bytes32 }
+      ]
+      returnType := none
+      returns := [ParamType.bytes32]
+      body := [
+        Compiler.Modules.Hashing.abiEncodePackedStaticSegments
+          "digest"
+          [(Expr.param "who", 20), (Expr.param "amount", 32)],
+        Stmt.returnValues [Expr.localVar "digest"]
+      ]
+    }
+  ]
+}
+
+private def sha256PackedStaticSegmentsSmokeSpec : CompilationModel := {
+  name := "Sha256PackedStaticSegmentsSmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "hash"
+      params := [
+        { name := "who", ty := ParamType.address }
+        , { name := "context", ty := ParamType.bytes32 }
+      ]
+      returnType := none
+      returns := [ParamType.bytes32]
+      body := [
+        Compiler.Modules.Hashing.sha256PackedStaticSegments
+          "digest"
+          [(Expr.param "who", 20), (Expr.param "context", 32)],
+        Stmt.returnValues [Expr.localVar "digest"]
+      ]
+    }
+  ]
+}
+
+private def sha256MemoryBadAritySpec : CompilationModel := {
+  name := "Sha256MemoryBadArity"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [{ name := "inputOffset", ty := ParamType.uint256 }]
+      returnType := none
+      body := [
+        Stmt.ecm (Compiler.Modules.Precompiles.sha256MemoryModule "digest")
+          [Expr.param "inputOffset"],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def abiEncodePackedWordsBadAritySpec : CompilationModel := {
+  name := "AbiEncodePackedWordsBadArity"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [{ name := "a", ty := ParamType.bytes32 }]
+      returnType := none
+      body := [
+        Stmt.ecm (Compiler.Modules.Hashing.abiEncodePackedWordsModule "digest" 2)
+          [Expr.param "a"],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def sha256PackedWordsBadAritySpec : CompilationModel := {
+  name := "Sha256PackedWordsBadArity"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [{ name := "root", ty := ParamType.bytes32 }]
+      returnType := none
+      body := [
+        Stmt.ecm (Compiler.Modules.Hashing.sha256PackedWordsModule "digest" 2)
+          [Expr.param "root"],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def abiEncodePackedStaticSegmentsBadWidthSpec : CompilationModel := {
+  name := "AbiEncodePackedStaticSegmentsBadWidth"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [{ name := "who", ty := ParamType.address }]
+      returnType := none
+      body := [
+        Compiler.Modules.Hashing.abiEncodePackedStaticSegments
+          "digest"
+          [(Expr.param "who", 33)],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def sha256PackedStaticSegmentsBadWidthSpec : CompilationModel := {
+  name := "Sha256PackedStaticSegmentsBadWidth"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [{ name := "who", ty := ParamType.address }]
+      returnType := none
+      body := [
+        Compiler.Modules.Hashing.sha256PackedStaticSegments
+          "digest"
+          [(Expr.param "who", 0)],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def abiEncodePackedStaticSegmentsBadAritySpec : CompilationModel := {
+  name := "AbiEncodePackedStaticSegmentsBadArity"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [{ name := "who", ty := ParamType.address }]
+      returnType := none
+      body := [
+        Stmt.ecm (Compiler.Modules.Hashing.abiEncodePackedStaticSegmentsModule "digest" [20, 32])
+          [Expr.param "who"],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def sha256PackedStaticSegmentsBadAritySpec : CompilationModel := {
+  name := "Sha256PackedStaticSegmentsBadArity"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [{ name := "who", ty := ParamType.address }]
+      returnType := none
+      body := [
+        Stmt.ecm (Compiler.Modules.Hashing.sha256PackedStaticSegmentsModule "digest" [20, 32])
+          [Expr.param "who"],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
 private def oracleReadSmokeSpec : CompilationModel := {
   name := "OracleReadSmoke"
   fields := []
@@ -2718,6 +3006,160 @@ private def oracleReadSmokeSpec : CompilationModel := {
   ]
 }
 
+private def bubblingValueCallSmokeSpec : CompilationModel := {
+  name := "BubblingValueCallSmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "forward"
+      params := [
+        { name := "target", ty := ParamType.address }
+        , { name := "ethValue", ty := ParamType.uint256 }
+        , { name := "inputOffset", ty := ParamType.uint256 }
+        , { name := "inputSize", ty := ParamType.uint256 }
+        , { name := "outputOffset", ty := ParamType.uint256 }
+        , { name := "outputSize", ty := ParamType.uint256 }
+      ]
+      returnType := none
+      body := [
+        Compiler.Modules.Calls.bubblingValueCall
+          (Expr.param "target")
+          (Expr.param "ethValue")
+          (Expr.param "inputOffset")
+          (Expr.param "inputSize")
+          (Expr.param "outputOffset")
+          (Expr.param "outputSize"),
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def bubblingValueCallBadAritySpec : CompilationModel := {
+  name := "BubblingValueCallBadArity"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [
+        { name := "target", ty := ParamType.address }
+        , { name := "ethValue", ty := ParamType.uint256 }
+      ]
+      returnType := none
+      body := [
+        Stmt.ecm Compiler.Modules.Calls.bubblingValueCallModule [
+          Expr.param "target",
+          Expr.param "ethValue"
+        ],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def bubblingValueCallViewRejectedSpec : CompilationModel := {
+  name := "BubblingValueCallViewRejected"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "forward"
+      params := [
+        { name := "target", ty := ParamType.address }
+        , { name := "ethValue", ty := ParamType.uint256 }
+        , { name := "inputOffset", ty := ParamType.uint256 }
+        , { name := "inputSize", ty := ParamType.uint256 }
+        , { name := "outputOffset", ty := ParamType.uint256 }
+        , { name := "outputSize", ty := ParamType.uint256 }
+      ]
+      returnType := none
+      isView := true
+      body := [
+        Compiler.Modules.Calls.bubblingValueCall
+          (Expr.param "target")
+          (Expr.param "ethValue")
+          (Expr.param "inputOffset")
+          (Expr.param "inputSize")
+          (Expr.param "outputOffset")
+          (Expr.param "outputSize"),
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def bubblingValueCallNoOutputSmokeSpec : CompilationModel := {
+  name := "BubblingValueCallNoOutputSmoke"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "forward"
+      params := [
+        { name := "target", ty := ParamType.address }
+        , { name := "ethValue", ty := ParamType.uint256 }
+        , { name := "inputOffset", ty := ParamType.uint256 }
+        , { name := "inputSize", ty := ParamType.uint256 }
+      ]
+      returnType := none
+      body := [
+        Compiler.Modules.Calls.bubblingValueCallNoOutput
+          (Expr.param "target")
+          (Expr.param "ethValue")
+          (Expr.param "inputOffset")
+          (Expr.param "inputSize"),
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def bubblingValueCallNoOutputViewRejectedSpec : CompilationModel := {
+  name := "BubblingValueCallNoOutputViewRejected"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "forward"
+      params := [
+        { name := "target", ty := ParamType.address }
+        , { name := "ethValue", ty := ParamType.uint256 }
+        , { name := "inputOffset", ty := ParamType.uint256 }
+        , { name := "inputSize", ty := ParamType.uint256 }
+      ]
+      returnType := none
+      isView := true
+      body := [
+        Compiler.Modules.Calls.bubblingValueCallNoOutput
+          (Expr.param "target")
+          (Expr.param "ethValue")
+          (Expr.param "inputOffset")
+          (Expr.param "inputSize"),
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
+private def bubblingValueCallNoOutputBadAritySpec : CompilationModel := {
+  name := "BubblingValueCallNoOutputBadArity"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := [
+        { name := "target", ty := ParamType.address }
+        , { name := "ethValue", ty := ParamType.uint256 }
+      ]
+      returnType := none
+      body := [
+        Stmt.ecm Compiler.Modules.Calls.bubblingValueCallNoOutputModule [
+          Expr.param "target",
+          Expr.param "ethValue"
+        ],
+        Stmt.stop
+      ]
+    }
+  ]
+}
+
 private def erc20BalanceOfSmokeSpec : CompilationModel := {
   name := "ERC20BalanceOfSmoke"
   fields := []
@@ -3367,6 +3809,11 @@ set_option maxRecDepth 4096 in
   expectTrue "arrayElement-only specs do not emit word-array helpers"
     (!(contains uintArrayElementOnlyYul checkedArrayElementWordCalldataHelperName) &&
       !(contains uintArrayElementOnlyYul checkedArrayElementWordMemoryHelperName))
+  let uintArrayForEachAccumulatorYul ←
+    expectCompileToYul "uint256[] forEach accumulator smoke spec" uintArrayForEachAccumulatorSpec
+  expectTrue "forEach accumulator specs assign outer locals inside the loop body"
+    (contains uintArrayForEachAccumulatorYul "let i := 0" &&
+      contains uintArrayForEachAccumulatorYul "total := add(total, value)")
   let tupleArrayElementWordOnlyYul ←
     expectCompileToYul "tuple[] arrayElementWord-only smoke spec" tupleArrayElementWordOnlySpec
   expectTrue "arrayElementWord-only specs emit the word-array helpers"
@@ -3436,6 +3883,127 @@ set_option maxRecDepth 4096 in
     (contains ecrecoverYul "if iszero(returndatasize()) {")
   expectTrue "ecrecover ECM masks recovered address to 160 bits"
     (contains ecrecoverYul "let signer := and(mload(0), 0xffffffffffffffffffffffffffffffffffffffff)")
+  let sha256MemoryYul ←
+    expectCompileToYul "sha256 memory smoke spec" sha256MemorySmokeSpec
+  expectTrue "sha256Memory ECM binds output offset once before the precompile call"
+    (contains sha256MemoryYul "let __sha256_output_offset := outputOffset")
+  expectTrue "sha256Memory ECM lowers to precompile 0x02 staticcall"
+    (contains sha256MemoryYul "staticcall(gas(), 2, inputOffset, inputSize, __sha256_output_offset, 32)")
+  expectTrue "sha256Memory ECM reverts when the precompile call fails"
+    (contains sha256MemoryYul "if iszero(__sha256_success) {")
+  expectTrue "sha256Memory ECM returns the digest word from output memory"
+    (contains sha256MemoryYul "let digest := 0" &&
+      contains sha256MemoryYul "digest := mload(__sha256_output_offset)")
+  let sha256MemoryTwiceYul ←
+    expectCompileToYul "sha256 memory twice smoke spec" sha256MemoryTwiceSmokeSpec
+  expectTrue "sha256Memory ECM scopes internal temporaries across repeated uses"
+    (countOccurrences sha256MemoryTwiceYul "let __sha256_output_offset :=" == 2 &&
+      countOccurrences sha256MemoryTwiceYul "let __sha256_success :=" == 2 &&
+      contains sha256MemoryTwiceYul "let firstDigest := 0" &&
+      contains sha256MemoryTwiceYul "firstDigest := mload(__sha256_output_offset)" &&
+      contains sha256MemoryTwiceYul "let secondDigest := 0" &&
+      contains sha256MemoryTwiceYul "secondDigest := mload(__sha256_output_offset)")
+  expectCompileErrorContains
+    "sha256Memory ECM rejects invalid argument counts"
+    sha256MemoryBadAritySpec
+    "uses ECM 'sha256Memory' with 1 arguments but it expects 3"
+  let sha256MemoryTrustReport := emitTrustReportJson [sha256MemorySmokeSpec]
+  expectTrue "sha256Memory trust report surfaces the SHA-256 precompile assumption"
+    (contains sha256MemoryTrustReport "\"module\":\"sha256Memory\"" &&
+      contains sha256MemoryTrustReport "\"assumption\":\"evm_sha256_precompile\"" &&
+      contains sha256MemoryTrustReport "\"status\":\"assumed\"")
+  let abiEncodePackedWordsYul ←
+    expectCompileToYul "abiEncodePackedWords smoke spec" abiEncodePackedWordsSmokeSpec
+  expectTrue "abiEncodePackedWords evaluates source words before clobbering scratch memory"
+    (contains abiEncodePackedWordsYul "let __packed_word_0 := a" &&
+      contains abiEncodePackedWordsYul "let __packed_word_1 := b" &&
+      contains abiEncodePackedWordsYul "let __packed_word_2 := c")
+  expectTrue "abiEncodePackedWords stores static words contiguously"
+    (contains abiEncodePackedWordsYul "mstore(0, __packed_word_0)" &&
+      contains abiEncodePackedWordsYul "mstore(32, __packed_word_1)" &&
+      contains abiEncodePackedWordsYul "mstore(64, __packed_word_2)")
+  expectTrue "abiEncodePackedWords hashes the exact packed byte length"
+    (contains abiEncodePackedWordsYul "let digest := keccak256(0, 96)")
+  let sha256PackedWordsYul ←
+    expectCompileToYul "sha256PackedWords smoke spec" sha256PackedWordsSmokeSpec
+  expectTrue "sha256PackedWords evaluates source words before clobbering scratch memory"
+    (contains sha256PackedWordsYul "let __packed_word_0 := root" &&
+      contains sha256PackedWordsYul "let __packed_word_1 := context")
+  expectTrue "sha256PackedWords stores static words contiguously"
+    (contains sha256PackedWordsYul "mstore(0, __packed_word_0)" &&
+      contains sha256PackedWordsYul "mstore(32, __packed_word_1)")
+  expectTrue "sha256PackedWords hashes the exact packed byte length through precompile 0x02"
+    (contains sha256PackedWordsYul "staticcall(gas(), 2, 0, 64, 64, 32)")
+  expectTrue "sha256PackedWords reverts when the precompile call fails"
+    (contains sha256PackedWordsYul "if iszero(__sha256_packed_success) {")
+  expectTrue "sha256PackedWords returns the digest word from non-overlapping output memory"
+    (contains sha256PackedWordsYul "let digest := mload(64)")
+  expectCompileErrorContains
+    "sha256PackedWords ECM rejects invalid argument counts"
+    sha256PackedWordsBadAritySpec
+    "uses ECM 'sha256PackedWords' with 1 arguments but it expects 2"
+  let sha256PackedWordsTrustReport := emitTrustReportJson [sha256PackedWordsSmokeSpec]
+  expectTrue "sha256PackedWords trust report surfaces packed-layout and SHA-256 assumptions"
+    (contains sha256PackedWordsTrustReport "\"module\":\"sha256PackedWords\"" &&
+      contains sha256PackedWordsTrustReport "\"assumption\":\"abi_packed_static_word_layout\"" &&
+      contains sha256PackedWordsTrustReport "\"assumption\":\"evm_sha256_precompile\"" &&
+      contains sha256PackedWordsTrustReport "\"status\":\"assumed\"")
+  let abiEncodePackedStaticSegmentsYul ←
+    expectCompileToYul "abiEncodePackedStaticSegments smoke spec" abiEncodePackedStaticSegmentsSmokeSpec
+  expectTrue "abiEncodePackedStaticSegments masks and left-aligns sub-word static values"
+    (contains abiEncodePackedStaticSegmentsYul
+      "mstore(0, shl(96, and(__packed_word_0, 0xffffffffffffffffffffffffffffffffffffffff)))")
+  expectTrue "abiEncodePackedStaticSegments places the next segment at the byte-precise offset"
+    (contains abiEncodePackedStaticSegmentsYul "mstore(20, __packed_word_1)")
+  expectTrue "abiEncodePackedStaticSegments hashes the exact byte length"
+    (contains abiEncodePackedStaticSegmentsYul "let digest := keccak256(0, 52)")
+  expectCompileErrorContains
+    "abiEncodePackedStaticSegments rejects invalid segment widths"
+    abiEncodePackedStaticSegmentsBadWidthSpec
+    "abiEncodePackedStaticSegments segment widths must be between 1 and 32 bytes"
+  expectCompileErrorContains
+    "abiEncodePackedStaticSegments ECM rejects invalid argument counts"
+    abiEncodePackedStaticSegmentsBadAritySpec
+    "uses ECM 'abiEncodePackedStaticSegments' with 1 arguments but it expects 2"
+  let abiEncodePackedStaticSegmentsTrustReport :=
+    emitTrustReportJson [abiEncodePackedStaticSegmentsSmokeSpec]
+  expectTrue "abiEncodePackedStaticSegments trust report surfaces segment-layout and keccak assumptions"
+    (contains abiEncodePackedStaticSegmentsTrustReport "\"module\":\"abiEncodePackedStaticSegments\"" &&
+      contains abiEncodePackedStaticSegmentsTrustReport "\"assumption\":\"abi_packed_static_segment_layout\"" &&
+      contains abiEncodePackedStaticSegmentsTrustReport "\"assumption\":\"keccak256_memory_slice_matches_evm\"")
+  let sha256PackedStaticSegmentsYul ←
+    expectCompileToYul "sha256PackedStaticSegments smoke spec" sha256PackedStaticSegmentsSmokeSpec
+  expectTrue "sha256PackedStaticSegments masks and left-aligns sub-word static values"
+    (contains sha256PackedStaticSegmentsYul
+      "mstore(0, shl(96, and(__packed_word_0, 0xffffffffffffffffffffffffffffffffffffffff)))")
+  expectTrue "sha256PackedStaticSegments hashes the exact byte length through precompile 0x02"
+    (contains sha256PackedStaticSegmentsYul "staticcall(gas(), 2, 0, 52, 64, 32)")
+  expectTrue "sha256PackedStaticSegments returns the digest from aligned non-overlapping output memory"
+    (contains sha256PackedStaticSegmentsYul "let digest := mload(64)")
+  expectCompileErrorContains
+    "sha256PackedStaticSegments rejects invalid segment widths"
+    sha256PackedStaticSegmentsBadWidthSpec
+    "sha256PackedStaticSegments segment widths must be between 1 and 32 bytes"
+  expectCompileErrorContains
+    "sha256PackedStaticSegments ECM rejects invalid argument counts"
+    sha256PackedStaticSegmentsBadAritySpec
+    "uses ECM 'sha256PackedStaticSegments' with 1 arguments but it expects 2"
+  let sha256PackedStaticSegmentsTrustReport :=
+    emitTrustReportJson [sha256PackedStaticSegmentsSmokeSpec]
+  expectTrue "sha256PackedStaticSegments trust report surfaces segment-layout and SHA-256 assumptions"
+    (contains sha256PackedStaticSegmentsTrustReport "\"module\":\"sha256PackedStaticSegments\"" &&
+      contains sha256PackedStaticSegmentsTrustReport "\"assumption\":\"abi_packed_static_segment_layout\"" &&
+      contains sha256PackedStaticSegmentsTrustReport "\"assumption\":\"evm_sha256_precompile\"" &&
+      contains sha256PackedStaticSegmentsTrustReport "\"status\":\"assumed\"")
+  expectCompileErrorContains
+    "abiEncodePackedWords ECM rejects invalid argument counts"
+    abiEncodePackedWordsBadAritySpec
+    "uses ECM 'abiEncodePackedWords' with 1 arguments but it expects 2"
+  let abiEncodePackedWordsTrustReport := emitTrustReportJson [abiEncodePackedWordsSmokeSpec]
+  expectTrue "abiEncodePackedWords trust report surfaces packed-layout and keccak assumptions"
+    (contains abiEncodePackedWordsTrustReport "\"module\":\"abiEncodePackedWords\"" &&
+      contains abiEncodePackedWordsTrustReport "\"assumption\":\"abi_packed_static_word_layout\"" &&
+      contains abiEncodePackedWordsTrustReport "\"assumption\":\"keccak256_memory_slice_matches_evm\"")
   let oracleReadYul ←
     expectCompileToYul "oracle read smoke spec" oracleReadSmokeSpec
   expectTrue "oracle read ECM lowers to staticcall"
@@ -3446,6 +4014,49 @@ set_option maxRecDepth 4096 in
     (contains oracleReadYul "if iszero(eq(returndatasize(), 32)) {")
   expectTrue "oracle read ECM ABI-encodes the selector"
     (contains oracleReadYul "mstore(0, shl(224, 0xfeaf968c))")
+  let bubblingValueCallYul ←
+    expectCompileToYul "bubbling value call smoke spec" bubblingValueCallSmokeSpec
+  expectTrue "bubbling value call ECM lowers to call, not staticcall"
+    (contains bubblingValueCallYul
+      "call(gas(), target, ethValue, inputOffset, inputSize, outputOffset, outputSize)" &&
+      !(contains bubblingValueCallYul "staticcall("))
+  expectTrue "bubbling value call ECM forwards revert returndata"
+    (contains bubblingValueCallYul "let __bvc_rds := returndatasize()" &&
+      contains bubblingValueCallYul "returndatacopy(0, 0, __bvc_rds)" &&
+      contains bubblingValueCallYul "revert(0, __bvc_rds)")
+  expectCompileErrorContains
+    "bubbling value call ECM rejects invalid argument counts"
+    bubblingValueCallBadAritySpec
+    "uses ECM 'bubblingValueCall' with 2 arguments but it expects 6"
+  expectCompileErrorContains
+    "bubbling value call ECM remains rejected from view functions"
+    bubblingValueCallViewRejectedSpec
+    "function 'forward' is marked view but writes state"
+  let bubblingValueCallTrustReport := emitTrustReportJson [bubblingValueCallSmokeSpec]
+  expectTrue "bubbling value call trust report surfaces the generic call assumption"
+    (contains bubblingValueCallTrustReport "\"module\":\"bubblingValueCall\"" &&
+      contains bubblingValueCallTrustReport "\"assumption\":\"generic_low_level_value_call_interface\"" &&
+      contains bubblingValueCallTrustReport "\"status\":\"assumed\"")
+  let bubblingValueCallNoOutputYul ←
+    expectCompileToYul "bubbling value call no-output smoke spec" bubblingValueCallNoOutputSmokeSpec
+  expectTrue "bubbling value call no-output helper fixes output slice to zero"
+    (contains bubblingValueCallNoOutputYul
+      "call(gas(), target, ethValue, inputOffset, inputSize, 0, 0)")
+  expectCompileErrorContains
+    "bubbling value call no-output helper remains rejected from view functions"
+    bubblingValueCallNoOutputViewRejectedSpec
+    "function 'forward' is marked view but writes state"
+  expectCompileErrorContains
+    "bubbling value call no-output ECM rejects invalid argument counts"
+    bubblingValueCallNoOutputBadAritySpec
+    "uses ECM 'bubblingValueCallNoOutput' with 2 arguments but it expects 4"
+  let bubblingValueCallNoOutputTrustReport :=
+    emitTrustReportJson [bubblingValueCallNoOutputSmokeSpec]
+  expectTrue "bubbling value call no-output helper preserves the generic call assumption"
+    (contains bubblingValueCallNoOutputTrustReport "\"module\":\"bubblingValueCallNoOutput\"" &&
+      contains bubblingValueCallNoOutputTrustReport
+        "\"assumption\":\"generic_low_level_value_call_interface\"" &&
+      contains bubblingValueCallNoOutputTrustReport "\"status\":\"assumed\"")
   let erc20BalanceOfYul ←
     expectCompileToYul "erc20 balanceOf smoke spec" erc20BalanceOfSmokeSpec
   expectTrue "erc20 balanceOf ECM lowers to staticcall"
diff --git a/Compiler/Modules.lean b/Compiler/Modules.lean
index 176648c26..62910313b 100644
--- a/Compiler/Modules.lean
+++ b/Compiler/Modules.lean
@@ -2,5 +2,6 @@ import Compiler.Modules.Calls
 import Compiler.Modules.Callbacks
 import Compiler.Modules.ERC4626
 import Compiler.Modules.ERC20
+import Compiler.Modules.Hashing
 import Compiler.Modules.Oracle
 import Compiler.Modules.Precompiles
diff --git a/Compiler/Modules/Calls.lean b/Compiler/Modules/Calls.lean
index 7d4d0206e..a42a43b78 100644
--- a/Compiler/Modules/Calls.lean
+++ b/Compiler/Modules/Calls.lean
@@ -4,9 +4,13 @@
   Standard ECM for ABI-encoded external calls with a single uint256 return:
   - `withReturn`: call/staticcall with selector + args, revert-forward on failure,
     validate return data, bind result variable
+  - `bubblingValueCall`: arbitrary low-level call with caller-provided ETH value,
+    caller-provided input/output memory slices, and exact revert-data bubbling
 
   Trust assumption: the target contract's function matches the declared
-  selector and ABI encoding.
+  selector and ABI encoding. For arbitrary low-level calls, the target contract
+  behavior and calldata ABI are deliberately outside Verity core and are surfaced
+  as an explicit ECM assumption.
 -/
 
 import Compiler.ECM
@@ -18,6 +22,29 @@ open Compiler.Yul
 open Compiler.ECM
 open Compiler.CompilationModel (Stmt Expr)
 
+private def bubblingValueCallYul
+    (targetExpr valueExpr inputOffsetExpr inputSizeExpr outputOffsetExpr outputSizeExpr : YulExpr) :
+    List YulStmt :=
+  let callExpr := YulExpr.call "call" [
+    YulExpr.call "gas" [],
+    targetExpr,
+    valueExpr,
+    inputOffsetExpr,
+    inputSizeExpr,
+    outputOffsetExpr,
+    outputSizeExpr
+  ]
+  [YulStmt.block [
+    YulStmt.let_ "__bvc_success" callExpr,
+    YulStmt.if_ (YulExpr.call "iszero" [YulExpr.ident "__bvc_success"]) [
+      YulStmt.let_ "__bvc_rds" (YulExpr.call "returndatasize" []),
+      YulStmt.expr (YulExpr.call "returndatacopy" [
+        YulExpr.lit 0, YulExpr.lit 0, YulExpr.ident "__bvc_rds"
+      ]),
+      YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.ident "__bvc_rds"])
+    ]
+  ]]
+
 /-- Generic external call with single uint256 return.
     ABI-encodes `selector(args...)`, calls/staticcalls target, reverts on failure,
     validates returndatasize >= 32, and binds the result.
@@ -82,4 +109,72 @@ def withReturn (resultVar : String) (target : Expr) (selector : Nat)
     (args : List Expr) (isStatic : Bool := false) : Stmt :=
   .ecm (withReturnModule resultVar selector args.length isStatic) ([target] ++ args)
 
+/-- Generic Solidity-style low-level value call with revert-data bubbling.
+
+    This models the common wrapper:
+
+    ```
+    let success := call(gas(), target, value, inputOffset, inputSize, outputOffset, outputSize)
+    if iszero(success) {
+      returndatacopy(0, 0, returndatasize())
+      revert(0, returndatasize())
+    }
+    ```
+
+    Arguments passed to compile:
+    `[target, value, inputOffset, inputSize, outputOffset, outputSize]`.
+
+    The module intentionally does not interpret the calldata or returndata
+    payload. Protocol-specific meaning belongs in packages that use this generic
+    Verity-core mechanism and document their own assumptions. -/
+def bubblingValueCallModule : ExternalCallModule where
+  name := "bubblingValueCall"
+  numArgs := 6
+  resultVars := []
+  writesState := true
+  readsState := true
+  axioms := ["generic_low_level_value_call_interface"]
+  compile := fun _ctx args => do
+    let (targetExpr, valueExpr, inputOffsetExpr, inputSizeExpr, outputOffsetExpr, outputSizeExpr) ←
+      match args with
+      | [target, value, inputOffset, inputSize, outputOffset, outputSize] =>
+          pure (target, value, inputOffset, inputSize, outputOffset, outputSize)
+      | _ =>
+          throw "bubblingValueCall expects 6 arguments (target, value, inputOffset, inputSize, outputOffset, outputSize)"
+    pure <| bubblingValueCallYul
+      targetExpr valueExpr inputOffsetExpr inputSizeExpr outputOffsetExpr outputSizeExpr
+
+/-- Four-argument no-output variant of `bubblingValueCallModule`.
+
+    This is useful for `verity_contract` `ecmDo` call sites and for adapter or
+    router calls where successful returndata is intentionally ignored. Failure
+    returndata is still bubbled exactly. -/
+def bubblingValueCallNoOutputModule : ExternalCallModule where
+  name := "bubblingValueCallNoOutput"
+  numArgs := 4
+  resultVars := []
+  writesState := true
+  readsState := true
+  axioms := ["generic_low_level_value_call_interface"]
+  compile := fun _ctx args => do
+    let (targetExpr, valueExpr, inputOffsetExpr, inputSizeExpr) ←
+      match args with
+      | [target, value, inputOffset, inputSize] =>
+          pure (target, value, inputOffset, inputSize)
+      | _ =>
+          throw "bubblingValueCallNoOutput expects 4 arguments (target, value, inputOffset, inputSize)"
+    pure <| bubblingValueCallYul
+      targetExpr valueExpr inputOffsetExpr inputSizeExpr (YulExpr.lit 0) (YulExpr.lit 0)
+
+/-- Convenience constructor for `bubblingValueCallModule`. -/
+def bubblingValueCall
+    (target value inputOffset inputSize outputOffset outputSize : Expr) : Stmt :=
+  .ecm bubblingValueCallModule [target, value, inputOffset, inputSize, outputOffset, outputSize]
+
+/-- Convenience constructor for the common adapter/router shape that ignores
+    successful returndata while still bubbling failure returndata exactly. -/
+def bubblingValueCallNoOutput
+    (target value inputOffset inputSize : Expr) : Stmt :=
+  .ecm bubblingValueCallNoOutputModule [target, value, inputOffset, inputSize]
+
 end Compiler.Modules.Calls
diff --git a/Compiler/Modules/Hashing.lean b/Compiler/Modules/Hashing.lean
new file mode 100644
index 000000000..87bcd8805
--- /dev/null
+++ b/Compiler/Modules/Hashing.lean
@@ -0,0 +1,205 @@
+/-
+  Compiler.Modules.Hashing: packed static hash helpers
+
+  These helpers cover common audit-modeling hash preimages:
+  - static 32-byte words
+  - static byte-width segments from 1 to 32 bytes
+
+  They intentionally do not model dynamic Solidity packed encoding for bytes or
+  strings yet.
+-/
+
+import Compiler.ECM
+import Compiler.CompilationModel
+
+namespace Compiler.Modules.Hashing
+
+open Compiler.Yul
+open Compiler.ECM
+open Compiler.CompilationModel (Stmt Expr)
+
+private def packedWordTempName (idx : Nat) : String :=
+  s!"__packed_word_{idx}"
+
+private def packedWordBindings (words : List YulExpr) : List YulStmt :=
+  words.zipIdx.map fun (word, idx) =>
+    YulStmt.let_ (packedWordTempName idx) word
+
+private def packedWordTempStores (wordCount : Nat) : List YulStmt :=
+  (List.range wordCount).map fun idx =>
+    YulStmt.expr (YulExpr.call "mstore" [
+      YulExpr.lit (idx * 32),
+      YulExpr.ident (packedWordTempName idx)
+    ])
+
+private def alignUp32 (n : Nat) : Nat :=
+  ((n + 31) / 32) * 32
+
+private def packedSegmentMask (width : Nat) : Nat :=
+  2 ^ (width * 8) - 1
+
+private def packedSegmentTempStore (offset width idx : Nat) : YulStmt :=
+  let value := YulExpr.ident (packedWordTempName idx)
+  let stored :=
+    if width == 32 then
+      value
+    else
+      YulExpr.call "shl" [
+        YulExpr.lit ((32 - width) * 8),
+        YulExpr.call "and" [value, YulExpr.hex (packedSegmentMask width)]
+      ]
+  YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit offset, stored])
+
+private def packedSegmentTempStoresAux (offset : Nat) : List Nat → Nat → List YulStmt
+  | [], _ => []
+  | width :: widths, idx =>
+      packedSegmentTempStore offset width idx ::
+        packedSegmentTempStoresAux (offset + width) widths (idx + 1)
+
+private def packedSegmentTempStores (widths : List Nat) : List YulStmt :=
+  packedSegmentTempStoresAux 0 widths 0
+
+private def validatePackedSegmentWidths (moduleName : String) (widths : List Nat) : Except String Unit :=
+  widths.forM fun width =>
+    if width == 0 || width > 32 then
+      throw s!"{moduleName} segment widths must be between 1 and 32 bytes"
+    else
+      pure ()
+
+/-- Keccak-256 over packed static 32-byte words stored at scratch memory offset 0.
+    This is the static-word subset of Solidity `abi.encodePacked(...)` followed
+    by `keccak256`. -/
+def abiEncodePackedWordsModule (resultVar : String) (wordCount : Nat) : ExternalCallModule where
+  name := "abiEncodePackedWords"
+  numArgs := wordCount
+  resultVars := [resultVar]
+  writesState := false
+  readsState := false
+  axioms := ["keccak256_memory_slice_matches_evm", "abi_packed_static_word_layout"]
+  compile := fun _ctx args => do
+    if args.length != wordCount then
+      throw s!"abiEncodePackedWords expects {wordCount} static word argument(s)"
+    let size := wordCount * 32
+    pure [
+      YulStmt.block (packedWordBindings args ++ packedWordTempStores wordCount),
+      YulStmt.let_ resultVar (YulExpr.call "keccak256" [YulExpr.lit 0, YulExpr.lit size])
+    ]
+
+/-- Convenience constructor for static-word packed Keccak hashing. -/
+def abiEncodePackedWords (resultVar : String) (words : List Expr) : Stmt :=
+  .ecm (abiEncodePackedWordsModule resultVar words.length) words
+
+/-- Short alias for the static 32-byte-word subset of `abi.encodePacked`.
+    Use `abiEncodePackedWords` when the narrower semantics should be explicit at
+    the call site. -/
+def abiEncodePacked (resultVar : String) (words : List Expr) : Stmt :=
+  abiEncodePackedWords resultVar words
+
+/-- 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
+    values. Sub-word values are masked to their requested width before being
+    shifted into position. Widths must be between 1 and 32 bytes. -/
+def abiEncodePackedStaticSegmentsModule (resultVar : String) (widths : List Nat) : ExternalCallModule where
+  name := "abiEncodePackedStaticSegments"
+  numArgs := widths.length
+  resultVars := [resultVar]
+  writesState := false
+  readsState := false
+  axioms := ["keccak256_memory_slice_matches_evm", "abi_packed_static_segment_layout"]
+  compile := fun _ctx args => do
+    if args.length != widths.length then
+      throw s!"abiEncodePackedStaticSegments expects {widths.length} static segment argument(s)"
+    validatePackedSegmentWidths "abiEncodePackedStaticSegments" widths
+    let size := widths.foldl (· + ·) 0
+    pure [
+      YulStmt.block (packedWordBindings args ++ packedSegmentTempStores widths),
+      YulStmt.let_ resultVar (YulExpr.call "keccak256" [YulExpr.lit 0, YulExpr.lit size])
+    ]
+
+/-- Convenience constructor for static byte-width packed Keccak hashing. -/
+def abiEncodePackedStaticSegments (resultVar : String) (segments : List (Expr × Nat)) : Stmt :=
+  .ecm (abiEncodePackedStaticSegmentsModule resultVar (segments.map Prod.snd))
+    (segments.map Prod.fst)
+
+/-- SHA-256 over packed static 32-byte words stored at scratch memory offset 0.
+    The digest is written after the packed input words and then bound from
+    memory, avoiding overlap with the preimage. -/
+def sha256PackedWordsModule (resultVar : String) (wordCount : Nat) : ExternalCallModule where
+  name := "sha256PackedWords"
+  numArgs := wordCount
+  resultVars := [resultVar]
+  writesState := false
+  readsState := true
+  axioms := ["evm_sha256_precompile", "abi_packed_static_word_layout"]
+  compile := fun _ctx args => do
+    if args.length != wordCount then
+      throw s!"sha256PackedWords expects {wordCount} static word argument(s)"
+    let size := wordCount * 32
+    let outputOffset := size
+    let callExpr := YulExpr.call "staticcall" [
+      YulExpr.call "gas" [],
+      YulExpr.lit 2,
+      YulExpr.lit 0, YulExpr.lit size,
+      YulExpr.lit outputOffset, YulExpr.lit 32
+    ]
+    let revertBlock := YulStmt.if_ (YulExpr.call "iszero" [YulExpr.ident "__sha256_packed_success"]) [
+      YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
+    ]
+    pure [
+      YulStmt.block (packedWordBindings args ++ packedWordTempStores wordCount ++ [
+        YulStmt.let_ "__sha256_packed_success" callExpr,
+        revertBlock
+      ]),
+      YulStmt.let_ resultVar (YulExpr.call "mload" [YulExpr.lit outputOffset])
+    ]
+
+/-- Convenience constructor for static-word packed SHA-256 hashing. -/
+def sha256PackedWords (resultVar : String) (words : List Expr) : Stmt :=
+  .ecm (sha256PackedWordsModule resultVar words.length) words
+
+/-- Short alias for static 32-byte-word packed SHA-256 preimages. -/
+def sha256Packed (resultVar : String) (words : List Expr) : Stmt :=
+  sha256PackedWords resultVar words
+
+/-- SHA-256 over packed static byte-width segments.
+    The digest is written at the next 32-byte-aligned offset after the preimage
+    to avoid overlapping with non-word-sized packed input bytes. Sub-word
+    values are masked to their requested width before being shifted into
+    position. -/
+def sha256PackedStaticSegmentsModule (resultVar : String) (widths : List Nat) : ExternalCallModule where
+  name := "sha256PackedStaticSegments"
+  numArgs := widths.length
+  resultVars := [resultVar]
+  writesState := false
+  readsState := true
+  axioms := ["evm_sha256_precompile", "abi_packed_static_segment_layout"]
+  compile := fun _ctx args => do
+    if args.length != widths.length then
+      throw s!"sha256PackedStaticSegments expects {widths.length} static segment argument(s)"
+    validatePackedSegmentWidths "sha256PackedStaticSegments" widths
+    let size := widths.foldl (· + ·) 0
+    let outputOffset := alignUp32 size
+    let callExpr := YulExpr.call "staticcall" [
+      YulExpr.call "gas" [],
+      YulExpr.lit 2,
+      YulExpr.lit 0, YulExpr.lit size,
+      YulExpr.lit outputOffset, YulExpr.lit 32
+    ]
+    let revertBlock := YulStmt.if_ (YulExpr.call "iszero" [YulExpr.ident "__sha256_packed_segments_success"]) [
+      YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
+    ]
+    pure [
+      YulStmt.block (packedWordBindings args ++ packedSegmentTempStores widths ++ [
+        YulStmt.let_ "__sha256_packed_segments_success" callExpr,
+        revertBlock
+      ]),
+      YulStmt.let_ resultVar (YulExpr.call "mload" [YulExpr.lit outputOffset])
+    ]
+
+/-- Convenience constructor for static byte-width packed SHA-256 hashing. -/
+def sha256PackedStaticSegments (resultVar : String) (segments : List (Expr × Nat)) : Stmt :=
+  .ecm (sha256PackedStaticSegmentsModule resultVar (segments.map Prod.snd))
+    (segments.map Prod.fst)
+
+end Compiler.Modules.Hashing
diff --git a/Compiler/Modules/Precompiles.lean b/Compiler/Modules/Precompiles.lean
index 728bef5fb..132360903 100644
--- a/Compiler/Modules/Precompiles.lean
+++ b/Compiler/Modules/Precompiles.lean
@@ -3,6 +3,7 @@
 
   Standard ECMs for EVM precompile calls:
   - `ecrecover`: ECDSA signature recovery via precompile at address 0x01
+  - `sha256Memory`: SHA-256 over an existing memory slice via precompile 0x02
 
   Trust assumption: EVM precompiles behave according to the Ethereum
   Yellow Paper specification.
@@ -63,4 +64,49 @@ def ecrecoverModule (resultVar : String) : ExternalCallModule where
 def ecrecover (resultVar : String) (hash v r s : Expr) : Stmt :=
   .ecm (ecrecoverModule resultVar) [hash, v, r, s]
 
+/-- SHA-256 precompile over an existing memory slice.
+    Arguments: [inputOffset, inputSize, outputOffset]
+    Binds one result variable to `mload(outputOffset)`.
+    Reverts if precompile 0x02 reports failure. -/
+def sha256MemoryModule (resultVar : String) : ExternalCallModule where
+  name := "sha256Memory"
+  numArgs := 3
+  resultVars := [resultVar]
+  writesState := false
+  readsState := true
+  axioms := ["evm_sha256_precompile"]
+  compile := fun _ctx args => do
+    let (inputOffset, inputSize, outputOffset) ← match args with
+      | [inputOffset, inputSize, outputOffset] => pure (inputOffset, inputSize, outputOffset)
+      | _ => throw "sha256Memory expects 3 arguments (inputOffset, inputSize, outputOffset)"
+    let outputOffsetTemp := YulExpr.ident "__sha256_output_offset"
+    let callExpr := YulExpr.call "staticcall" [
+      YulExpr.call "gas" [],
+      YulExpr.lit 2,
+      inputOffset, inputSize,
+      outputOffsetTemp, YulExpr.lit 32
+    ]
+    let revertBlock := YulStmt.if_ (YulExpr.call "iszero" [YulExpr.ident "__sha256_success"]) [
+      YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])
+    ]
+    let bindResult := YulStmt.let_ resultVar (YulExpr.lit 0)
+    let assignResult := YulStmt.assign resultVar (YulExpr.call "mload" [outputOffsetTemp])
+    pure [
+      bindResult,
+      YulStmt.block [
+        YulStmt.let_ "__sha256_output_offset" outputOffset,
+        YulStmt.let_ "__sha256_success" callExpr,
+        revertBlock,
+        assignResult
+      ]
+    ]
+
+/-- Convenience: create a `Stmt.ecm` for SHA-256 over memory. -/
+def sha256Memory (resultVar : String) (inputOffset inputSize outputOffset : Expr) : Stmt :=
+  .ecm (sha256MemoryModule resultVar) [inputOffset, inputSize, outputOffset]
+
+/-- Short alias for SHA-256 over an existing memory slice. -/
+def sha256 (resultVar : String) (inputOffset inputSize outputOffset : Expr) : Stmt :=
+  sha256Memory resultVar inputOffset inputSize outputOffset
+
 end Compiler.Modules.Precompiles
diff --git a/Compiler/Modules/README.md b/Compiler/Modules/README.md
index 10120ea4c..d75688334 100644
--- a/Compiler/Modules/README.md
+++ b/Compiler/Modules/README.md
@@ -10,10 +10,11 @@ structure that the compiler can plug in without modification.
 |------|---------|----------|
 | `ERC20.lean` | `safeTransfer`, `safeTransferFrom`, `safeApprove`, `balanceOf`, `allowance`, `totalSupply` | `Stmt.safeTransfer`, `Stmt.safeTransferFrom`, canonical ERC-20 read wrappers |
 | `ERC4626.lean` | `previewDeposit`, `previewMint`, `previewWithdraw`, `previewRedeem`, `convertToAssets`, `convertToShares`, `totalAssets`, `asset`, `maxDeposit`, `maxMint`, `maxWithdraw`, `maxRedeem`, `deposit` | canonical vault preview/conversion wrappers plus a standard deposit wrapper |
+| `Hashing.lean` | `abiEncodePackedWords` / `abiEncodePacked`, `sha256PackedWords` / `sha256Packed`, `abiEncodePackedStaticSegments`, `sha256PackedStaticSegments` | handwritten static packed hash preimage `mstore` choreography |
 | `Oracle.lean` | `oracleReadUint256` | canonical oracle read wrappers |
-| `Precompiles.lean` | `ecrecover` | `Stmt.ecrecover` |
+| `Precompiles.lean` | `ecrecover`, `sha256Memory` / `sha256` | `Stmt.ecrecover`, handwritten SHA-256 precompile calls |
 | `Callbacks.lean` | `callback` | `Stmt.callback` |
-| `Calls.lean` | `withReturn` | `Stmt.externalCallWithReturn` |
+| `Calls.lean` | `withReturn`, `bubblingValueCall`, `bubblingValueCallNoOutput` | `Stmt.externalCallWithReturn`, handwritten low-level `call{value: ...}` wrappers |
 
 ## Usage
 
@@ -30,6 +31,40 @@ body := [
 ]
 ```
 
+Static-word packed hashing helpers are available for ZK/audit preimages whose
+items are already 32-byte words:
+
+```lean
+Modules.Hashing.abiEncodePackedWords
+  "digest"
+  [Expr.param "root", Expr.param "contextHash", Expr.param "nullifier"]
+
+Modules.Hashing.sha256PackedWords
+  "publicSignalDigest"
+  [Expr.param "root", Expr.param "contextHash"]
+```
+
+The shorter `Modules.Hashing.abiEncodePacked` and
+`Modules.Hashing.sha256Packed` aliases are available for the same static-word
+semantics. These helpers write words contiguously at scratch memory offset zero.
+For static packed preimages with byte-width segments such as address-sized
+values, use the segment helpers:
+
+```lean
+Modules.Hashing.abiEncodePackedStaticSegments
+  "digest"
+  [(Expr.param "who", 20), (Expr.param "amount", 32)]
+
+Modules.Hashing.sha256PackedStaticSegments
+  "publicSignalDigest"
+  [(Expr.param "who", 20), (Expr.param "contextHash", 32)]
+```
+
+Segment widths are explicit byte counts from 1 to 32. Sub-word values are
+masked to their requested width and left-aligned before `mstore`, and subsequent
+segments are placed at byte-precise offsets. These helpers still do not
+implement dynamic Solidity packed encoding for `bytes` or `string`.
+
 ## Writing a New Standard Module
 
 1. Create `Compiler/Modules/YourModule.lean`.
diff --git a/Contracts/MacroTranslateInvariantTest.lean b/Contracts/MacroTranslateInvariantTest.lean
index 45b5f9889..b423d5f56 100644
--- a/Contracts/MacroTranslateInvariantTest.lean
+++ b/Contracts/MacroTranslateInvariantTest.lean
@@ -5,6 +5,7 @@ import Compiler.Selector
 import Compiler.Hex
 import Contracts
 import Contracts.Smoke
+import Contracts.Smoke.PackedHashECMSmoke
 import Contracts.Smoke.SelfBalanceSmoke
 import Contracts.ProxyUpgradeabilityMacroSmoke
 import Contracts.ProxyUpgradeabilityLayoutCompatibleSmoke
@@ -304,6 +305,7 @@ private def macroSpecs : List CompilationModel :=
   , Contracts.Smoke.SpecialEntrypointSmoke.spec
   , Contracts.Smoke.LeanDefHelperSmoke.spec
   , Contracts.Smoke.DirectHelperCallSmoke.spec
+  , Contracts.Smoke.MultiReturnHelperSmoke.spec
   , Contracts.Smoke.InitializerSmoke.spec
   , Contracts.Smoke.ConstantSmoke.spec
   , Contracts.Smoke.ImmutableSmoke.spec
@@ -333,6 +335,8 @@ private def macroSpecs : List CompilationModel :=
   , Contracts.Smoke.ERC20HelperSmoke.spec
   , Contracts.Smoke.GenericECMReadSmoke.spec
   , Contracts.Smoke.GenericECMWriteSmoke.spec
+  , Contracts.Smoke.BubblingValueCallECMSmoke.spec
+  , Contracts.Smoke.PackedHashECMSmoke.spec
   , Contracts.Smoke.LowLevelTryCatchSmoke.spec
   , Contracts.Smoke.LocalObligationRequiredForUnsafeFunctionBoundary.spec
   , Contracts.Smoke.LocalObligationRequiredForUnsafeConstructorBoundary.spec
@@ -414,6 +418,7 @@ private def expectedExternalSignatures : List (String × List String) :=
   , ("LeanDefHelperSmoke", ["addOffset(uint256,int256)", "sameWord(uint256,uint256)"])
   , ("DirectHelperCallSmoke", ["addToTotal(uint256)", "readTotalPlus(uint256)", "pairWithTotal(uint256)",
       "runHelpers(uint256,uint256,uint256)", "snapshot()"])
+  , ("MultiReturnHelperSmoke", ["summarize(uint256)", "useSummary(uint256)"])
   , ("InitializerSmoke", ["initOwner(address)", "upgradeToV2()"])
   , ("ConstantSmoke", ["feeOn(uint256)", "treasuryAddr()"])
   , ("ImmutableSmoke", ["supplyCap()", "treasuryAddr()", "shadowed(uint256)"])
@@ -457,6 +462,9 @@ private def expectedExternalSignatures : List (String × List String) :=
       "snapshotAllowance(address,address,address)", "snapshotSupply(address)"])
   , ("GenericECMReadSmoke", ["snapshotQuote(address,address)"])
   , ("GenericECMWriteSmoke", ["runEffect(uint256,uint256)"])
+  , ("BubblingValueCallECMSmoke", ["forwardNoOutput(address,uint256,uint256,uint256)"])
+  , ("PackedHashECMSmoke", ["hashAddressAmount(address,uint256)", "hashLowByteAmount(uint256,uint256)",
+      "sha256AddressAmount(address,uint256)"])
   , ("LowLevelTryCatchSmoke", ["catchFailure()", "skipCatchOnSuccess()", "catchFailureWithShadowedParam(uint256)"])
   , ("LocalObligationRequiredForUnsafeFunctionBoundary", ["preview()"])
   , ("LocalObligationRequiredForUnsafeConstructorBoundary", ["noop()"])
@@ -530,6 +538,7 @@ private def expectedExternalSelectors : List (String × List String) :=
   , ("SpecialEntrypointSmoke", ["0x931999fb", "0x74b204a4"])
   , ("LeanDefHelperSmoke", ["0x42dbad08", "0x9ca603a4"])
   , ("DirectHelperCallSmoke", ["0x623f577a", "0xe9696d56", "0xe176587e", "0xa392867e", "0x9711715a"])
+  , ("MultiReturnHelperSmoke", ["0x9c9c9cd5", "0xbe1e29cd"])
   , ("InitializerSmoke", ["0x0d009297", "0xcc01053e"])
   , ("ConstantSmoke", ["0x9c421eb5", "0x30d9a62a"])
   , ("ImmutableSmoke", ["0x8f770ad0", "0x30d9a62a", "0x655b96ec"])
@@ -563,6 +572,8 @@ private def expectedExternalSelectors : List (String × List String) :=
       "0x7247c4a5"])
   , ("GenericECMReadSmoke", ["0x78f2e50f"])
   , ("GenericECMWriteSmoke", ["0xc1192eb1"])
+  , ("BubblingValueCallECMSmoke", ["0x7ba1ade4"])
+  , ("PackedHashECMSmoke", ["0xffba6b66", "0xb70f2d26", "0x9c3e158c"])
   , ("LowLevelTryCatchSmoke", ["0x42d9c6d1", "0xdaf546c4", "0xa4660933"])
   , ("LocalObligationRequiredForUnsafeFunctionBoundary", ["0xefae2305"])
   , ("LocalObligationRequiredForUnsafeConstructorBoundary", ["0x5dfc2e4a"])
@@ -893,6 +904,15 @@ private def checkDirectHelperCallSmoke : IO Unit := do
     (contains (reprStr runHelpers.body) "Stmt.internalCallAssign" &&
       contains (reprStr runHelpers.body) "\"internal_pairWithTotal\"")
 
+private def checkMultiReturnHelperSmoke : IO Unit := do
+  expectTrue
+    "MultiReturnHelperSmoke: tuple-return helper binds lower to internalCallAssign"
+    (match Contracts.Smoke.MultiReturnHelperSmoke.useSummary_modelBody with
+    | [Stmt.internalCallAssign ["head", "tail"] helperName [Expr.param "seed"],
+        Stmt.return (Expr.add (Expr.localVar "head") (Expr.localVar "tail"))] =>
+        helperName == "internal_summarize"
+    | _ => false)
+
 private def checkNamedStructParamSmoke : IO Unit := do
   expectTrue
     "NamedStructParamSmoke: nested struct leaf projection uses recursive tuple binding"
@@ -1085,6 +1105,7 @@ private def checkSpec (spec : CompilationModel) : IO Unit := do
   checkLowLevelTryCatchSmoke
   checkSpecialEntrypointSmoke
   checkDirectHelperCallSmoke
+  checkMultiReturnHelperSmoke
   checkNamedStructParamSmoke
   checkCurveCutArraySmoke
   checkDynamicStructArraySmoke
diff --git a/Contracts/MacroTranslateRoundTripFuzz.lean b/Contracts/MacroTranslateRoundTripFuzz.lean
index 00648d7e4..4164e7e00 100644
--- a/Contracts/MacroTranslateRoundTripFuzz.lean
+++ b/Contracts/MacroTranslateRoundTripFuzz.lean
@@ -6,6 +6,7 @@ import Contracts.ProxyUpgradeabilityMacroSmoke
 import Contracts.ProxyUpgradeabilityLayoutCompatibleSmoke
 import Contracts.ProxyUpgradeabilityLayoutIncompatibleSmoke
 import Contracts.Smoke
+import Contracts.Smoke.PackedHashECMSmoke
 import Contracts.Smoke.SelfBalanceSmoke
 
 namespace Compiler.MacroTranslateRoundTripFuzz
@@ -64,6 +65,7 @@ private def macroSpecs : List CompilationModel :=
   , Contracts.Smoke.SpecialEntrypointSmoke.spec
   , Contracts.Smoke.LeanDefHelperSmoke.spec
   , Contracts.Smoke.DirectHelperCallSmoke.spec
+  , Contracts.Smoke.MultiReturnHelperSmoke.spec
   , Contracts.Smoke.InitializerSmoke.spec
   , Contracts.Smoke.ConstantSmoke.spec
   , Contracts.Smoke.ImmutableSmoke.spec
@@ -90,6 +92,8 @@ private def macroSpecs : List CompilationModel :=
   , Contracts.Smoke.ERC20HelperSmoke.spec
   , Contracts.Smoke.GenericECMReadSmoke.spec
   , Contracts.Smoke.GenericECMWriteSmoke.spec
+  , Contracts.Smoke.BubblingValueCallECMSmoke.spec
+  , Contracts.Smoke.PackedHashECMSmoke.spec
   , Contracts.Smoke.LowLevelTryCatchSmoke.spec
   , Contracts.Smoke.ModifiesSmoke.spec
   , Contracts.Smoke.NoExternalCallsSmoke.spec
diff --git a/Contracts/Smoke.lean b/Contracts/Smoke.lean
index e7f2ecc93..f6f90d8b0 100644
--- a/Contracts/Smoke.lean
+++ b/Contracts/Smoke.lean
@@ -11,6 +11,7 @@ import Contracts.SimpleToken.SimpleToken
 import Contracts.ERC20.ERC20
 import Contracts.ERC721.ERC721
 import Compiler.Modules.ERC20
+import Compiler.Modules.Calls
 import Compiler.Modules.Oracle
 
 namespace Contracts.Smoke
@@ -1226,6 +1227,34 @@ verity_contract DirectHelperCallSmoke where
     let right ← getStorage lastRight
     return (current, left, right)
 
+verity_contract MultiReturnHelperSmoke where
+  storage
+    lastTotal : Uint256 := slot 0
+    lastHead : Uint256 := slot 1
+
+  function summarize (seed : Uint256) : Tuple [Uint256, Uint256] := do
+    let head := add seed 1
+    let tail := add seed 2
+    return (head, tail)
+
+  function useSummary (seed : Uint256) : Uint256 := do
+    let (head, tail) ← summarize seed
+    return (add head tail)
+
+/--
+error: `total` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `total`, consider using `let total` instead
+-/
+#guard_msgs in
+verity_contract ForEachMutableLocalMacroRejected where
+  storage
+
+  function sumValues (values : Array Uint256) : Uint256 := do
+    let mut total := 0
+    forEach "i" (arrayLength values) (do
+      let value := arrayElement values i
+      total := add total value)
+    return total
+
 /--
 error: helper call 'consumePayload' uses a parameter or return type that direct macro helper lowering does not support yet; only static non-fallback/non-receive helpers can be lowered to internal specs
 -/
@@ -1471,6 +1500,13 @@ verity_contract GenericECMWriteSmoke where
   function runEffect (lhs : Uint256, rhs : Uint256) : Unit := do
     ecmDo genericECMEffectDemoModule [lhs, rhs]
 
+verity_contract BubblingValueCallECMSmoke where
+  storage
+
+  function forwardNoOutput (target : Address, ethValue : Uint256, inputOffset : Uint256, inputSize : Uint256) : Unit := do
+    ecmDo Compiler.Modules.Calls.bubblingValueCallNoOutputModule
+      [addressToWord target, ethValue, inputOffset, inputSize]
+
 set_option linter.unusedVariables false in
 verity_contract LowLevelTryCatchSmoke where
   storage
@@ -1800,6 +1836,7 @@ end SpecGenSmoke
 #check_contract DynamicStructArraySmoke
 #check_contract PackedStorageWriteSmoke
 #check_contract DirectHelperCallSmoke
+#check_contract MultiReturnHelperSmoke
 #check_contract Uint8Smoke
 #check_contract AddressHelpersSmoke
 #check_contract ZeroAddressShadowSmoke
@@ -2084,6 +2121,24 @@ example :
       , Compiler.CompilationModel.Stmt.stop
       ] := rfl
 
+example :
+    (Compiler.CompilationModel.FunctionSpec.body
+      (BubblingValueCallECMSmoke.forwardNoOutput_model : Compiler.CompilationModel.FunctionSpec)) =
+    BubblingValueCallECMSmoke.forwardNoOutput_modelBody := by
+  simpa using BubblingValueCallECMSmoke.forwardNoOutput_semantic_preservation
+
+example :
+    BubblingValueCallECMSmoke.forwardNoOutput_modelBody =
+      [ Compiler.CompilationModel.Stmt.ecm
+          Compiler.Modules.Calls.bubblingValueCallNoOutputModule
+          [ Compiler.CompilationModel.Expr.param "target"
+          , Compiler.CompilationModel.Expr.param "ethValue"
+          , Compiler.CompilationModel.Expr.param "inputOffset"
+          , Compiler.CompilationModel.Expr.param "inputSize"
+          ]
+      , Compiler.CompilationModel.Stmt.stop
+      ] := rfl
+
 example :
     (LowLevelTryCatchSmoke.catchFailure.run Verity.defaultState).getValue? = some 0 := by
   decide
diff --git a/Contracts/Smoke/PackedHashECMSmoke.lean b/Contracts/Smoke/PackedHashECMSmoke.lean
new file mode 100644
index 000000000..eb8d24fc1
--- /dev/null
+++ b/Contracts/Smoke/PackedHashECMSmoke.lean
@@ -0,0 +1,62 @@
+import Contracts.Common
+import Compiler.Modules.Hashing
+
+namespace Contracts.Smoke
+
+open Verity hiding pure bind
+
+verity_contract PackedHashECMSmoke where
+  storage
+
+  function hashAddressAmount (who : Address, amount : Uint256) : Bytes32 := do
+    let digest ← ecmCall
+      (fun resultVar => Compiler.Modules.Hashing.abiEncodePackedStaticSegmentsModule resultVar [20, 32])
+      [addressToWord who, amount]
+    return digest
+
+  function hashLowByteAmount (value : Uint256, amount : Uint256) : Bytes32 := do
+    let digest ← ecmCall
+      (fun resultVar => Compiler.Modules.Hashing.abiEncodePackedStaticSegmentsModule resultVar [1, 32])
+      [value, amount]
+    return digest
+
+  function sha256AddressAmount (who : Address, amount : Uint256) : Bytes32 := do
+    let digest ← ecmCall
+      (fun resultVar => Compiler.Modules.Hashing.sha256PackedStaticSegmentsModule resultVar [20, 32])
+      [addressToWord who, amount]
+    return digest
+
+example :
+    PackedHashECMSmoke.hashAddressAmount_modelBody =
+      [ Compiler.CompilationModel.Stmt.ecm
+          (Compiler.Modules.Hashing.abiEncodePackedStaticSegmentsModule "digest" [20, 32])
+          [ Compiler.CompilationModel.Expr.param "who"
+          , Compiler.CompilationModel.Expr.param "amount"
+          ]
+      , Compiler.CompilationModel.Stmt.return
+          (Compiler.CompilationModel.Expr.localVar "digest")
+      ] := rfl
+
+example :
+    PackedHashECMSmoke.hashLowByteAmount_modelBody =
+      [ Compiler.CompilationModel.Stmt.ecm
+          (Compiler.Modules.Hashing.abiEncodePackedStaticSegmentsModule "digest" [1, 32])
+          [ Compiler.CompilationModel.Expr.param "value"
+          , Compiler.CompilationModel.Expr.param "amount"
+          ]
+      , Compiler.CompilationModel.Stmt.return
+          (Compiler.CompilationModel.Expr.localVar "digest")
+      ] := rfl
+
+example :
+    PackedHashECMSmoke.sha256AddressAmount_modelBody =
+      [ Compiler.CompilationModel.Stmt.ecm
+          (Compiler.Modules.Hashing.sha256PackedStaticSegmentsModule "digest" [20, 32])
+          [ Compiler.CompilationModel.Expr.param "who"
+          , Compiler.CompilationModel.Expr.param "amount"
+          ]
+      , Compiler.CompilationModel.Stmt.return
+          (Compiler.CompilationModel.Expr.localVar "digest")
+      ] := rfl
+
+end Contracts.Smoke
diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 345f3d798..dcb33f5e2 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -574,6 +574,18 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 #print axioms Verity.Proofs.Stdlib.MappingAutomation.setMapping2_preserves_events
 
 -- Verity/Proofs/Stdlib/Math.lean
+#print axioms Verity.Proofs.Stdlib.Math.SNARK_SCALAR_FIELD_ne_zero
+#print axioms Verity.Proofs.Stdlib.Math.SNARK_SCALAR_FIELD_lt_modulus
+#print axioms Verity.Proofs.Stdlib.Math.modField_nat_eq
+#print axioms Verity.Proofs.Stdlib.Math.modField_lt
+#print axioms Verity.Proofs.Stdlib.Math.modField_eq_self_of_lt
+#print axioms Verity.Proofs.Stdlib.Math.modField_zero
+#print axioms Verity.Proofs.Stdlib.Math.modField_SNARK_SCALAR_FIELD
+#print axioms Verity.Proofs.Stdlib.Math.modField_eq_zero_iff
+#print axioms Verity.Proofs.Stdlib.Math.modField_eq_of_nat_mod_eq
+#print axioms Verity.Proofs.Stdlib.Math.modField_eq_iff_nat_mod_eq
+#print axioms Verity.Proofs.Stdlib.Math.modField_nat_mod_eq
+#print axioms Verity.Proofs.Stdlib.Math.modField_idempotent
 -- #print axioms Verity.Proofs.Stdlib.Math.modulus_eq_max_succ  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.lt_modulus_of_le_max  -- private
 -- #print axioms Verity.Proofs.Stdlib.Math.max_uint256_lt_modulus  -- private
@@ -3896,4 +3908,4 @@ import Compiler.Proofs.YulGeneration.ReferenceOracle.Semantics
 -- Compiler/Proofs/YulGeneration/ReferenceOracle/Semantics.lean
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_sender
 #print axioms Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
--- Total: 3720 theorems/lemmas (2770 public, 950 private, 0 sorry'd)
+-- Total: 3732 theorems/lemmas (2782 public, 950 private, 0 sorry'd)
diff --git a/Verity/Proofs/Stdlib/Math.lean b/Verity/Proofs/Stdlib/Math.lean
index 2add4cfb0..97fa381ee 100644
--- a/Verity/Proofs/Stdlib/Math.lean
+++ b/Verity/Proofs/Stdlib/Math.lean
@@ -13,6 +13,103 @@ namespace Verity.Proofs.Stdlib.Math
 open Verity
 open Verity.Stdlib.Math
 
+/-! ## BN254 Field Helpers -/
+
+theorem SNARK_SCALAR_FIELD_ne_zero : SNARK_SCALAR_FIELD ≠ 0 := by
+  intro h
+  have hVal : (SNARK_SCALAR_FIELD : Nat) = 0 := by
+    simpa using congrArg (fun x : Uint256 => (x : Nat)) h
+  rw [SNARK_SCALAR_FIELD_val] at hVal
+  exact (by decide : (21888242871839275222246405745257275088548364400416034343698204186575808495617 : Nat) ≠ 0) hVal
+
+theorem SNARK_SCALAR_FIELD_lt_modulus :
+    (SNARK_SCALAR_FIELD : Nat) < Verity.Core.Uint256.modulus := by
+  rw [SNARK_SCALAR_FIELD_val]
+  decide
+
+theorem modField_nat_eq (x : Uint256) :
+    (modField x : Nat) = (x : Nat) % (SNARK_SCALAR_FIELD : Nat) := by
+  have hFieldNonzero : (SNARK_SCALAR_FIELD : Nat) ≠ 0 := by
+    intro h
+    exact SNARK_SCALAR_FIELD_ne_zero (Verity.Core.Uint256.ext (by simpa using h.symm))
+  have hModLt :
+      (x : Nat) % (SNARK_SCALAR_FIELD : Nat) < Verity.Core.Uint256.modulus := by
+    exact Nat.lt_trans
+      (Nat.mod_lt _ (Nat.pos_of_ne_zero hFieldNonzero))
+      SNARK_SCALAR_FIELD_lt_modulus
+  simp only [modField, Verity.Core.Uint256.mod, hFieldNonzero, ↓reduceIte,
+    Verity.Core.Uint256.val_ofNat]
+  exact Nat.mod_eq_of_lt hModLt
+
+theorem modField_lt (x : Uint256) :
+    (modField x : Nat) < (SNARK_SCALAR_FIELD : Nat) := by
+  rw [modField_nat_eq]
+  have hFieldNonzero : (SNARK_SCALAR_FIELD : Nat) ≠ 0 := by
+    intro h
+    exact SNARK_SCALAR_FIELD_ne_zero (Verity.Core.Uint256.ext (by simpa using h.symm))
+  exact Nat.mod_lt _ (Nat.pos_of_ne_zero hFieldNonzero)
+
+theorem modField_eq_self_of_lt (x : Uint256)
+    (h : (x : Nat) < (SNARK_SCALAR_FIELD : Nat)) :
+    modField x = x := by
+  apply Verity.Core.Uint256.ext
+  rw [modField_nat_eq]
+  exact Nat.mod_eq_of_lt h
+
+theorem modField_zero :
+    modField 0 = 0 := by
+  apply Verity.Core.Uint256.ext
+  rw [modField_nat_eq]
+  simp
+
+theorem modField_SNARK_SCALAR_FIELD :
+    modField SNARK_SCALAR_FIELD = 0 := by
+  apply Verity.Core.Uint256.ext
+  rw [modField_nat_eq]
+  exact Nat.mod_self _
+
+theorem modField_eq_zero_iff (x : Uint256) :
+    modField x = 0 ↔ (x : Nat) % (SNARK_SCALAR_FIELD : Nat) = 0 := by
+  constructor
+  · intro h
+    have hNat := congrArg (fun y : Uint256 => (y : Nat)) h
+    have hNat' : (modField x : Nat) = 0 := by
+      simpa using hNat
+    rw [modField_nat_eq] at hNat'
+    exact hNat'
+  · intro h
+    apply Verity.Core.Uint256.ext
+    rw [modField_nat_eq]
+    exact h
+
+theorem modField_eq_of_nat_mod_eq {x y : Uint256}
+    (h : (x : Nat) % (SNARK_SCALAR_FIELD : Nat) =
+      (y : Nat) % (SNARK_SCALAR_FIELD : Nat)) :
+    modField x = modField y := by
+  apply Verity.Core.Uint256.ext
+  rw [modField_nat_eq, modField_nat_eq]
+  exact h
+
+theorem modField_eq_iff_nat_mod_eq (x y : Uint256) :
+    modField x = modField y ↔
+      (x : Nat) % (SNARK_SCALAR_FIELD : Nat) =
+        (y : Nat) % (SNARK_SCALAR_FIELD : Nat) := by
+  constructor
+  · intro h
+    have hNat : (modField x : Nat) = (modField y : Nat) := by
+      simpa using congrArg (fun z : Uint256 => (z : Nat)) h
+    rw [modField_nat_eq, modField_nat_eq] at hNat
+    exact hNat
+  · exact modField_eq_of_nat_mod_eq
+
+theorem modField_nat_mod_eq (x : Uint256) :
+    (modField x : Nat) % (SNARK_SCALAR_FIELD : Nat) = (modField x : Nat) := by
+  exact Nat.mod_eq_of_lt (modField_lt x)
+
+theorem modField_idempotent (x : Uint256) :
+    modField (modField x) = modField x := by
+  exact modField_eq_self_of_lt (modField x) (modField_lt x)
+
 /-! ## mulDiv / wad Helpers -/
 
 private theorem modulus_eq_max_succ :
diff --git a/Verity/Stdlib/Math.lean b/Verity/Stdlib/Math.lean
index c99d2aa7f..391d54bea 100644
--- a/Verity/Stdlib/Math.lean
+++ b/Verity/Stdlib/Math.lean
@@ -52,6 +52,14 @@ def safeDiv (a b : Uint256) : Option Uint256 :=
 /-- Fixed-point scaling factor used by `wMulDown` and `wDivUp`. -/
 def WAD : Uint256 := 1000000000000000000
 
+/-- BN254 scalar field modulus used by Groth16/BN254 circuit public inputs. -/
+def SNARK_SCALAR_FIELD : Uint256 :=
+  21888242871839275222246405745257275088548364400416034343698204186575808495617
+
+/-- Reduce a word modulo the BN254 scalar field. -/
+def modField (x : Uint256) : Uint256 :=
+  Verity.Core.Uint256.mod x SNARK_SCALAR_FIELD
+
 /-- `mulDivDown(a, b, c)` = `floor(a * b / c)` under the EVM's `div` semantics. -/
 def mulDivDown (a b c : Uint256) : Uint256 :=
   (a * b) / c
@@ -127,6 +135,14 @@ def requireSomeUint (opt : Option Uint256) (message : String) : Contract Uint256
 @[simp] theorem WAD_val : (WAD : Nat) = 1000000000000000000 := by
   rfl
 
+@[simp] theorem SNARK_SCALAR_FIELD_val :
+    (SNARK_SCALAR_FIELD : Nat) =
+      21888242871839275222246405745257275088548364400416034343698204186575808495617 := by
+  rfl
+
+@[simp] theorem modField_def (x : Uint256) :
+    modField x = Verity.Core.Uint256.mod x SNARK_SCALAR_FIELD := rfl
+
 theorem WAD_ne_zero : WAD ≠ 0 := by
   intro h
   have : ((WAD : Uint256) : Nat) = 0 := by
diff --git a/artifacts/macro_property_tests/PropertyMultiReturnHelperSmoke.t.sol b/artifacts/macro_property_tests/PropertyMultiReturnHelperSmoke.t.sol
new file mode 100644
index 000000000..4048bbc7e
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyMultiReturnHelperSmoke.t.sol
@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyMultiReturnHelperSmokeTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke.lean
+ */
+contract PropertyMultiReturnHelperSmokeTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("MultiReturnHelperSmoke");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: TODO decode and assert `summarize` result
+    function testTODO_Summarize_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("summarize(uint256)", uint256(1)));
+        require(ok, "summarize reverted unexpectedly");
+        require(ret.length >= 64, "summarize ABI tuple return payload unexpectedly short");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 2: TODO decode and assert `useSummary` result
+    function testTODO_UseSummary_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("useSummary(uint256)", uint256(1)));
+        require(ok, "useSummary reverted unexpectedly");
+        assertEq(ret.length, 32, "useSummary ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+}
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index 2d7b66ceb..8aa1934ff 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -223,6 +223,13 @@ forEach "i" count (do
 )
 ```
 
+The compilation model supports accumulator-style loops by placing `Stmt.assignVar`
+inside `Stmt.forEach`; generated Yul preserves assignment to the outer local.
+The `verity_contract` source fallback currently rejects mutating a Lean
+`let mut` local from inside the nested `forEach` body term, so macro-authored
+contracts should use explicit memory scratch space for loop accumulators until
+that executable-path limitation is removed.
+
 Reference points:
 
 - `Stmt.forEach` in `Compiler/CompilationModel.lean`
@@ -315,11 +322,17 @@ def mulDivUp (a b c : Uint256) : Uint256
 def wMulDown (a b : Uint256) : Uint256
 
 def wDivUp (a b : Uint256) : Uint256
+
+def SNARK_SCALAR_FIELD : Uint256
+
+def modField (x : Uint256) : Uint256
 ```
 
 **Proof lemmas**
 
 - `mulDivDown_nat_eq`, `mulDivUp_nat_eq`, `mulDivDown_le_mulDivUp`, `mulDivDown_antitone_divisor`, `mulDivUp_antitone_divisor`, `mulDivDown_comm`, `mulDivUp_comm`, `wMulDown_comm` (`Verity/Proofs/Stdlib/Math.lean`)
+- `SNARK_SCALAR_FIELD_val`, `modField_def` (`Verity/Stdlib/Math.lean`)
+- BN254 field lemmas: `SNARK_SCALAR_FIELD_ne_zero`, `SNARK_SCALAR_FIELD_lt_modulus`, `modField_nat_eq`, `modField_lt`, `modField_zero`, `modField_SNARK_SCALAR_FIELD`, `modField_eq_zero_iff`, `modField_eq_of_nat_mod_eq`, `modField_eq_iff_nat_mod_eq`, `modField_eq_self_of_lt`, `modField_nat_mod_eq`, `modField_idempotent` (`Verity/Proofs/Stdlib/Math.lean`)
 - Rounding-gap lemmas: `mulDivUp_le_mulDivDown_add_one`, `mulDivUp_eq_mulDivDown_or_succ`, `mulDivUp_eq_mulDivDown_of_dvd`, `mulDivUp_eq_mulDivDown_add_one_of_not_dvd` (`Verity/Proofs/Stdlib/Math.lean`)
 - Positivity lemmas: `mulDivDown_pos`, `mulDivUp_pos`, `wMulDown_pos`, `wDivUp_pos` (`Verity/Proofs/Stdlib/Math.lean`)
 - Zero-case lemmas: `mulDivDown_zero_left/right`, `mulDivUp_zero_left/right`, `wMulDown_zero_left/right`, `wDivUp_zero` (`Verity/Proofs/Stdlib/Math.lean`)
@@ -643,6 +656,26 @@ def Compiler.Modules.ERC4626.deposit
 def Compiler.Modules.Oracle.oracleReadUint256
   (resultVar : String) (target : Expr) (selector : Nat)
   (staticArgs : List Expr) : Stmt
+def Compiler.Modules.Precompiles.sha256Memory
+  (resultVar : String) (inputOffset inputSize outputOffset : Expr) : Stmt
+def Compiler.Modules.Precompiles.sha256
+  (resultVar : String) (inputOffset inputSize outputOffset : Expr) : Stmt
+def Compiler.Modules.Calls.bubblingValueCall
+  (target value inputOffset inputSize outputOffset outputSize : Expr) : Stmt
+def Compiler.Modules.Calls.bubblingValueCallNoOutput
+  (target value inputOffset inputSize : Expr) : Stmt
+def Compiler.Modules.Hashing.abiEncodePackedWords
+  (resultVar : String) (words : List Expr) : Stmt
+def Compiler.Modules.Hashing.abiEncodePacked
+  (resultVar : String) (words : List Expr) : Stmt
+def Compiler.Modules.Hashing.sha256PackedWords
+  (resultVar : String) (words : List Expr) : Stmt
+def Compiler.Modules.Hashing.sha256Packed
+  (resultVar : String) (words : List Expr) : Stmt
+def Compiler.Modules.Hashing.abiEncodePackedStaticSegments
+  (resultVar : String) (segments : List (Expr × Nat)) : Stmt
+def Compiler.Modules.Hashing.sha256PackedStaticSegments
+  (resultVar : String) (segments : List (Expr × Nat)) : Stmt
 ```
 
 These are emitted as `Stmt.ecm ...` with explicit module metadata and trust assumptions.
@@ -694,6 +727,43 @@ This elaborates to `Compiler.CompilationModel.Expr.keccak256` and lowers to the
 
 `Expr.keccak256` also remains an explicit proof boundary today: the compiler supports it directly, but the current proof stack still treats it as an axiomatized primitive instead of a fully modeled operation. When it appears, archive `--trust-report` and use `--deny-axiomatized-primitives` for proof-strict runs (see issue `#1411`).
 
+### Static-word packed hashing
+
+For packed preimages where each item is already a full 32-byte word, use the
+standard hashing ECMs instead of open-coded offset arithmetic:
+
+```lean
+Compiler.Modules.Hashing.abiEncodePackedWords
+  "digest"
+  [Expr.param "root", Expr.param "contextHash", Expr.param "nullifier"]
+
+Compiler.Modules.Hashing.sha256PackedWords
+  "publicSignalDigest"
+  [Expr.param "root", Expr.param "contextHash"]
+```
+
+These helpers lower to contiguous `mstore` calls starting at scratch memory
+offset zero. The shorter `abiEncodePacked` and `sha256Packed` names are aliases
+for the same static-word semantics. `abiEncodePackedWords` binds
+`keccak256(0, wordCount * 32)`; `sha256PackedWords` calls precompile `0x02`,
+reverts on precompile failure, and binds the digest word.
+
+For static mixed-width preimages, use explicit byte-width segment helpers:
+
+```lean
+Compiler.Modules.Hashing.abiEncodePackedStaticSegments
+  "digest"
+  [(Expr.param "who", 20), (Expr.param "amount", 32)]
+
+Compiler.Modules.Hashing.sha256PackedStaticSegments
+  "publicSignalDigest"
+  [(Expr.param "who", 20), (Expr.param "contextHash", 32)]
+```
+
+Segment widths must be between 1 and 32 bytes. Sub-word values are left-aligned
+before `mstore`, and later segments are placed at byte-precise offsets. Dynamic
+`bytes` and `string` packed encoding remains outside this core helper surface.
+
 ### `ecrecover` precompile
 
 `verity_contract` can bind the standard `ecrecover` precompile directly:
@@ -704,6 +774,12 @@ let signer <- ecrecover digest v r s
 
 This elaborates to `Compiler.Modules.Precompiles.ecrecoverModule` and the trust report records the explicit assumption `evm_ecrecover_precompile`.
 
+`Compiler.Modules.Precompiles.sha256Memory` covers SHA-256 over an existing
+memory slice. The shorter `Compiler.Modules.Precompiles.sha256` name is an
+alias for the same ECM. It emits precompile `0x02`, reverts on precompile
+failure, binds `mload(outputOffset)`, and records the explicit assumption
+`evm_sha256_precompile`.
+
 `Compiler.Modules.Oracle.oracleReadUint256` covers the common read-only oracle case: it ABI-encodes the selector plus static arguments, performs a `staticcall`, requires exactly one 32-byte return word, and binds that word to a local result variable. The trust report records the explicit ECM assumption `oracle_read_uint256_interface`.
 
 `Compiler.Modules.ERC20.balanceOf` covers the common token-balance read case: it ABI-encodes `balanceOf(address)`, performs a `staticcall`, requires exactly one 32-byte return word, and binds the returned balance word to a local result variable. The trust report records the explicit ECM assumption `erc20_balanceOf_interface`.
diff --git a/docs/ARITHMETIC_PROFILE.md b/docs/ARITHMETIC_PROFILE.md
index bd2b4f911..cd01683da 100644
--- a/docs/ARITHMETIC_PROFILE.md
+++ b/docs/ARITHMETIC_PROFILE.md
@@ -130,6 +130,13 @@ side conditions without importing the full arithmetic proof module directly.
 | Ceil sandwich bounds | `mulDivUp_mul_ge`, `mulDivUp_mul_lt_add` | `wDivUp_mul_ge`, `wDivUp_mul_lt_add` |
 
 The sandwich bounds are especially useful for AMM reserve/share proofs.
+For BN254/Groth16 public-input proofs, `modField_nat_eq`, `modField_lt`,
+`modField_zero`, `modField_SNARK_SCALAR_FIELD`,
+`modField_eq_zero_iff`, `modField_eq_of_nat_mod_eq`,
+`modField_eq_iff_nat_mod_eq`, `modField_eq_self_of_lt`,
+`modField_nat_mod_eq`, and
+`modField_idempotent` expose the exact
+`SNARK_SCALAR_FIELD` reduction semantics used by `Stdlib.Math.modField`.
 
 **Example**: See `Contracts/SafeCounter/SafeCounter.lean` and `Contracts/SafeCounter/Proofs/Basic.lean` for a contract using checked arithmetic with proven overflow/underflow behavior.
 
diff --git a/docs/EXTERNAL_CALL_MODULES.md b/docs/EXTERNAL_CALL_MODULES.md
index 9b8afd15e..6fb2c5cac 100644
--- a/docs/EXTERNAL_CALL_MODULES.md
+++ b/docs/EXTERNAL_CALL_MODULES.md
@@ -73,12 +73,83 @@ Standard modules ship in `Compiler/Modules/`:
 | `ERC20.safeTransfer` | `transfer(to, amount)` | ERC-20 transfer with optional-bool-return handling | `erc20_transfer_interface` |
 | `ERC20.safeTransferFrom` | `transferFrom(from, to, amount)` | ERC-20 transferFrom with optional-bool-return handling | `erc20_transferFrom_interface` |
 | `ERC20.safeApprove` | `approve(spender, amount)` | ERC-20 approve with optional-bool-return handling | `erc20_approve_interface` |
+| `Hashing.abiEncodePackedWords` / `Hashing.abiEncodePacked` | Static-word packed Keccak | Writes 32-byte words contiguously and binds `keccak256(0, wordCount * 32)` | `keccak256_memory_slice_matches_evm`, `abi_packed_static_word_layout` |
+| `Hashing.sha256PackedWords` / `Hashing.sha256Packed` | Static-word packed SHA-256 | Writes 32-byte words contiguously, calls precompile 0x02, and binds digest word | `evm_sha256_precompile`, `abi_packed_static_word_layout` |
+| `Hashing.abiEncodePackedStaticSegments` | Static byte-width packed Keccak | Writes 1- to 32-byte static segments at byte-precise offsets and binds `keccak256(0, totalBytes)` | `keccak256_memory_slice_matches_evm`, `abi_packed_static_segment_layout` |
+| `Hashing.sha256PackedStaticSegments` | Static byte-width packed SHA-256 | Writes 1- to 32-byte static segments, calls precompile 0x02 over the exact byte length, and binds digest word | `evm_sha256_precompile`, `abi_packed_static_segment_layout` |
 | `Precompiles.ecrecover` | Precompile 0x01 | ECDSA recovery, binds result address | `evm_ecrecover_precompile` |
+| `Precompiles.sha256Memory` / `Precompiles.sha256` | Precompile 0x02 | SHA-256 over an existing memory slice, binds digest word | `evm_sha256_precompile` |
 | `Callbacks.callback` | Parameterized | ABI-encode selector + static args + bytes, call target | `callback_target_interface` |
 | `Calls.withReturn` | Parameterized | Generic call/staticcall with single uint256 return | `external_call_abi_interface` |
+| `Calls.bubblingValueCall` / `Calls.bubblingValueCallNoOutput` | `call{value: v}(data)` shape | Generic low-level value call over caller-provided memory slices; bubbles exact revert returndata on failure | `generic_low_level_value_call_interface` |
 
 See `Compiler/Modules/README.md` for the full checklist on adding new standard modules.
 
+### Generic Value Calls
+
+`Compiler.Modules.Calls.bubblingValueCall` is the standard Verity-core surface
+for Solidity-style arbitrary low-level calls:
+
+```lean
+Compiler.Modules.Calls.bubblingValueCall
+  (Expr.param "target")
+  (Expr.param "ethValue")
+  (Expr.param "inputOffset")
+  (Expr.param "inputSize")
+  (Expr.param "outputOffset")
+  (Expr.param "outputSize")
+```
+
+It lowers to `call(gas(), target, ethValue, inputOffset, inputSize,
+outputOffset, outputSize)`. On failure, it copies `returndatasize()` bytes from
+offset zero into memory offset zero and reverts with that exact payload. The
+module is marked state-writing and state-reading, so normal mutability and CEI
+checks still apply; in particular, it is rejected from `view` / `pure`
+entrypoints rather than being treated as a read-only interface.
+
+This module models only generic EVM call mechanics. The meaning of the calldata,
+the callee's behavior, and protocol-specific postconditions remain assumptions
+of the package that uses the call.
+
+For adapter/router calls that intentionally ignore successful returndata, use
+`Compiler.Modules.Calls.bubblingValueCallNoOutput target value inputOffset
+inputSize`. It is backed by the four-argument
+`bubblingValueCallNoOutputModule`, which is suitable for `verity_contract`
+`ecmDo` call sites. Trust reports surface the distinct
+`bubblingValueCallNoOutput` module name with the same
+`generic_low_level_value_call_interface` assumption.
+
+### Packed Hashing Helpers
+
+`Compiler.Modules.Hashing.abiEncodePackedWords` and
+`Compiler.Modules.Hashing.sha256PackedWords` cover the audit-critical static
+word subset of packed preimage construction. The shorter
+`Compiler.Modules.Hashing.abiEncodePacked` and
+`Compiler.Modules.Hashing.sha256Packed` aliases expose the same semantics. They
+are intended for values that already occupy complete ABI words, such as
+`uint256`, `bytes32`, and address values after the model has chosen its
+word-level representation.
+
+The current helpers deliberately do not claim full Solidity
+`abi.encodePacked` parity for dynamic bytes/strings. For static mixed-width
+preimages, `Compiler.Modules.Hashing.abiEncodePackedStaticSegments` and
+`Compiler.Modules.Hashing.sha256PackedStaticSegments` accept explicit byte
+widths from 1 to 32:
+
+```lean
+Compiler.Modules.Hashing.abiEncodePackedStaticSegments
+  "digest"
+  [(Expr.param "who", 20), (Expr.param "amount", 32)]
+```
+
+Sub-word segments are masked to their requested width and left-aligned before
+`mstore`, then subsequent segments are placed at byte-precise offsets so later
+writes overwrite the unused tail bytes from earlier sub-word stores. These
+segment helpers expose
+`abi_packed_static_segment_layout` separately from the word-only layout
+assumption. Dynamic packed inputs should still be spelled out explicitly or
+added through a focused helper with its own tests and trust-report assumption.
+
 ## Writing Your Own ECM
 
 ### Minimal Example
@@ -195,5 +266,10 @@ For a machine-readable version, run `verity-compiler --trust-report <path>`. The
 - Standard modules in `Compiler/Modules/` are maintained and audited alongside
   the compiler.
 - Third-party modules are outside the Verity team's trust boundary.
+- Verity core owns generic Solidity/EVM mechanics such as low-level call
+  lowering, returndata bubbling, mutability flags, CEI tracking, and trust
+  reporting. Protocol-specific assumptions, including Unlink's Permit2,
+  Poseidon, Lazy-IMT, and Groth16 verifier boundaries, should live in the
+  dependent package as linked externals or package-local ECMs.
 
 See `TRUST_ASSUMPTIONS.md` section 7 and `AXIOMS.md` for details.
diff --git a/docs/INTERPRETER_FEATURE_MATRIX.md b/docs/INTERPRETER_FEATURE_MATRIX.md
index 9617dee50..2aa38df37 100644
--- a/docs/INTERPRETER_FEATURE_MATRIX.md
+++ b/docs/INTERPRETER_FEATURE_MATRIX.md
@@ -111,6 +111,25 @@ Legend: **ok** = supported, **0** = returns 0 (not modeled), **del** = delegated
 
 Legend: **ok** = supported, **rev** = reverts (not modeled), **nop** = no-op (codegen concern), **--** = not applicable, **n/m** = not modeled.
 
+ECMs include standard Verity-core modules for generic external-call mechanics,
+including `Compiler.Modules.Calls.bubblingValueCall`, which lowers
+Solidity-style `call{value: v}(data)` wrappers to Yul `call` and forwards exact
+revert returndata on failure. `bubblingValueCallNoOutputModule` exposes the
+same no-output adapter/router shape directly to `verity_contract` `ecmDo` call
+sites. These mechanics remain explicit trust-report surfaces: Verity models the
+generic call choreography, while package-specific callee behavior and protocol
+assumptions belong in dependent packages.
+
+The standard ECM library also includes static-word packed hashing helpers:
+`Compiler.Modules.Hashing.abiEncodePackedWords` and
+`Compiler.Modules.Hashing.sha256PackedWords`. These model contiguous 32-byte
+word preimages. For static mixed-width preimages, such as an address-sized
+segment followed by a 32-byte value, use
+`Compiler.Modules.Hashing.abiEncodePackedStaticSegments` or
+`Compiler.Modules.Hashing.sha256PackedStaticSegments` with explicit 1- to
+32-byte widths. Dynamic `bytes` / `string` packed encoding remains outside the
+current core surface.
+
 ---
 
 ## Builtin Bridge (Verity vs EVMYulLean)
diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md
index 6e9002423..e6c143392 100644
--- a/docs/ROADMAP.md
+++ b/docs/ROADMAP.md
@@ -117,6 +117,44 @@ Delivery policy for unsupported features:
 2. Error text must suggest the nearest currently-supported pattern.
 3. Error text must include the tracking issue reference.
 
+### Unlink Audit Readiness: Verity-Core Scope
+
+The Unlink audit should keep Verity focused on generic Solidity-modeling
+capabilities and move Unlink-specific cryptographic or protocol assumptions to
+a separate `unlink-verity` package. Verity should not grow built-in Poseidon,
+Permit2, Lazy-IMT, or Groth16 verifier semantics. Instead, Verity should provide
+the generic call, ABI, loop, helper-return, and trust-report surfaces needed for
+a clean line-by-line model, while `unlink-verity` declares the protocol-specific
+assumed boundaries with explicit axiom names and proof-status tags.
+
+Priority work for Verity core:
+
+| Priority | Work item | Scope | Exit criteria |
+|---|---|---|---|
+| P0 | ETH-aware generic external call ECM | Add a reusable ECM for Solidity-style arbitrary `call{value: v}(data)` with explicit target, ETH value, input offset/size or bytes-like calldata source, returndata bubbling on failure, and configurable output/returndata handling. | `Compiler/Modules/Calls.lean` exposes `bubblingValueCall` for explicit memory-slice calls and `bubblingValueCallNoOutput` / `bubblingValueCallNoOutputModule` for adapter/router calls that ignore successful returndata, including `verity_contract` `ecmDo` usage; generated Yul forwards revert returndata exactly; CEI/mutability/trust-report metadata are covered by compile-time tests for call lowering, value forwarding, revert bubbling, argument validation, and assumption reporting. |
+| P0 | ECM and trust-boundary documentation | Make the Verity-core vs `unlink-verity` package split explicit. | `docs/EXTERNAL_CALL_MODULES.md`, `docs/INTERPRETER_FEATURE_MATRIX.md`, and this roadmap document which generic surfaces are modeled by Verity and which Unlink-specific dependencies should be package-local assumptions. |
+| P1 | `forEach` mutable-local verification/docs | Confirm accumulator-style loop bodies can update local variables via `Stmt.assignVar`, and document the current macro-source limitation. | A feature test demonstrates `Stmt.letVar ...; Stmt.forEach ... [Stmt.assignVar ...]` lowering to Yul assignment inside the loop; macro docs state that `let mut` reassignment from inside a `verity_contract` `forEach` body is still rejected by the executable fallback, so source authors should use scratch memory until that limitation is removed. |
+| P1 | Multi-value internal return verification/docs | Confirm helper functions can return multiple values and callers can bind them cleanly from macro syntax. | A smoke or feature test demonstrates `_buildPublicSignals`-style helper returns, including `Stmt.internalCallAssign` or equivalent macro syntax; docs point users to the pattern. |
+| P1 | `abiEncodePacked` helper | Reduce hash-preimage offset mistakes in ZK/audit models. | `Compiler.Modules.Hashing.abiEncodePackedWords` covers the static 32-byte word subset, with `abiEncodePacked` as a short alias for the same semantics; `Compiler.Modules.Hashing.abiEncodePackedStaticSegments` covers static 1- to 32-byte segments such as address-sized values. Both lower to contiguous memory writes plus exact-length `keccak256` and have generated-Yul/trust-report tests. Dynamic Solidity packed encoding remains future work. |
+| P1 | `sha256` / `sha256Packed` helper | Avoid hand-rolled SHA-256 precompile calls in public-signal construction. | `Compiler.Modules.Precompiles.sha256Memory` covers existing memory slices, with `sha256` as a short alias; `Compiler.Modules.Hashing.sha256PackedWords` covers static-word packed preimages, with `sha256Packed` as a short alias; `Compiler.Modules.Hashing.sha256PackedStaticSegments` covers static 1- to 32-byte segments. SHA-256 helpers route through precompile 0x02 with failure reverts and generated-Yul/trust-report tests. |
+| P2 | BN254 scalar field helper | Improve readability of circuit-facing reductions. | `Verity.Stdlib.Math` exposes documented `SNARK_SCALAR_FIELD` and `modField` helpers with basic simp lemmas. |
+
+Already-supported items that should not become new roadmap work:
+
+- Named struct field access for calldata array elements is already available
+  through `struct` declarations and `arrayElement` field projection, lowering to
+  `Expr.arrayElementDynamicWord` where needed.
+- ERC-20 `balanceOf`, `allowance`, and `totalSupply` ECMs already exist under
+  `Compiler/Modules/ERC20.lean` alongside the safe token write modules.
+
+Package-boundary rule for the Unlink audit:
+
+- Keep Permit2, Poseidon, Lazy-IMT, and Groth16 verifier assumptions in
+  `unlink-verity` as external declarations or package-local ECMs with precise
+  axiom names, proof-status tags, and a trust manifest.
+- Keep Verity-core additions protocol-agnostic. A feature belongs in Verity core
+  only if it models ordinary Solidity/EVM behavior or reusable audit ergonomics.
+
 ---
 
 ## Lessons from UnlinkPool (#185)
diff --git a/docs/UNLINK_AUDIT_VERITY_CORE_PROMPT.md b/docs/UNLINK_AUDIT_VERITY_CORE_PROMPT.md
new file mode 100644
index 000000000..0781ff90c
--- /dev/null
+++ b/docs/UNLINK_AUDIT_VERITY_CORE_PROMPT.md
@@ -0,0 +1,239 @@
+# Prompt: Unlink Audit Readiness In Verity Core
+
+You are working in the `lfglabs-dev/verity` repository. The priority is to make
+the Verity-core language/compiler surface clean enough for a line-by-line Unlink
+audit model, while keeping Unlink-specific cryptographic and protocol
+assumptions out of Verity core.
+
+Do not implement an Unlink model in this repository. Do not add built-in
+Poseidon, Permit2, Lazy-IMT, or Groth16 verifier semantics to Verity core. Those
+belong in a separate `unlink-verity` package as external declarations or
+package-local ECMs with explicit axiom names and proof-status tags.
+
+## Goal
+
+Implement and document the generic Verity-core features needed to express
+Unlink cleanly:
+
+1. ETH-aware generic external call ECM.
+2. ECM/trust-boundary documentation sync.
+3. Verification/docs for mutable accumulators in `forEach`.
+4. Verification/docs for multi-value internal helper returns.
+5. `abiEncodePacked` helper.
+6. `sha256` / `sha256Packed` helper.
+7. BN254 scalar field constant and `modField` helper.
+
+## Current Status Checkpoint
+
+Before starting new work, inspect the current repository state and avoid
+reimplementing items that are already present. As of this checkpoint, the
+expected Verity-core surface is:
+
+- `Compiler.Modules.Calls.bubblingValueCall` for generic
+  `call{value: v}(data)` over explicit memory slices, with revert-returndata
+  bubbling and trust-report metadata. Use
+  `Compiler.Modules.Calls.bubblingValueCallNoOutput` for the common adapter
+  path that ignores successful returndata, or
+  `Compiler.Modules.Calls.bubblingValueCallNoOutputModule` from
+  `verity_contract` `ecmDo` call sites.
+- `Compiler.Modules.Precompiles.sha256Memory` and the shorter
+  `Compiler.Modules.Precompiles.sha256` alias for SHA-256 precompile 0x02 over
+  caller-provided memory slices.
+- `Compiler.Modules.Hashing.abiEncodePackedWords` /
+  `Compiler.Modules.Hashing.abiEncodePacked` and
+  `Compiler.Modules.Hashing.sha256PackedWords` /
+  `Compiler.Modules.Hashing.sha256Packed` for static 32-byte-word packed
+  preimages.
+- `Compiler.Modules.Hashing.abiEncodePackedStaticSegments` and
+  `Compiler.Modules.Hashing.sha256PackedStaticSegments` for explicit 1- to
+  32-byte static segments such as address-sized preimages.
+- `Verity.Stdlib.Math.SNARK_SCALAR_FIELD` and
+  `Verity.Stdlib.Math.modField`.
+- Compilation-model tests for mutable `Stmt.assignVar` inside `Stmt.forEach`
+  and macro smoke coverage for tuple-return helper bindings lowering to
+  `Stmt.internalCallAssign`.
+
+Known remaining limitation: `verity_contract` executable fallback source still
+rejects mutating a Lean `let mut` local from inside a nested `forEach` body.
+The compilation model supports the desired accumulator shape directly via
+`Stmt.assignVar`; macro-authored contracts that need executable fallback tests
+should use explicit scratch storage/memory until the fallback limitation is
+removed.
+
+Good follow-up work should either remove that fallback limitation cleanly, add
+tests/docs around a genuinely missing edge case, or tighten trust-boundary
+documentation. Do not keep adding parallel helper names for already-covered
+static packed hashing semantics.
+
+## Required Implementation Order
+
+### 1. ETH-aware generic external call ECM
+
+Add a reusable module under `Compiler/Modules/Calls.lean` for Solidity-style
+arbitrary external calls equivalent to:
+
+```solidity
+(bool ok, bytes memory returndata) = target.call{value: value}(data);
+if (!ok) {
+    assembly {
+        revert(add(returndata, 32), mload(returndata))
+    }
+}
+```
+
+The API should be protocol-agnostic and usable by UnlinkAdapter-style execution
+of arbitrary call data. It should support:
+
+- target address
+- ETH value
+- calldata/input offset and size, or the closest existing bytes-like Verity
+  surface if one already exists
+- configurable output handling if the existing ECM design supports it
+- exact revert-data bubbling on failed calls
+- correct `writesState`, `readsState`, `axioms`, and `proofStatus` metadata
+- clear validation errors for unsupported argument shapes
+
+Do not weaken CEI or mutability checks. If the module writes state, it must be
+marked accordingly.
+
+Add compile-time tests in `Compiler/CompilationModelFeatureTest.lean` covering:
+
+- lowering uses `call`, not `staticcall`
+- the call value operand is wired from the user argument
+- failure path copies `returndatasize()` bytes and reverts with that payload
+- invalid argument counts fail closed
+- trust-report / ECM metadata remains visible through existing reporting paths
+  if there is an existing test pattern for that
+
+### 2. Documentation sync
+
+Update:
+
+- `docs/EXTERNAL_CALL_MODULES.md`
+- `docs/INTERPRETER_FEATURE_MATRIX.md`
+- `docs/ROADMAP.md`
+
+The docs must state the package split:
+
+- Verity core owns generic Solidity/EVM modeling surfaces such as low-level call
+  mechanics, returndata bubbling, ABI helper ergonomics, loop/mutable-local
+  syntax, multi-value helper return syntax, and trust reporting.
+- `unlink-verity` owns Unlink-specific assumptions for Poseidon, Permit2,
+  Lazy-IMT, and Groth16 verifier behavior.
+
+Avoid wording that implies the full Unlink model or Unlink-specific assumptions
+should live in Verity core.
+
+### 3. Mutable accumulators inside `forEach`
+
+Check whether macro syntax already supports this pattern:
+
+```lean
+let mut total := 0
+forEach "i" (arrayLength notes) (do
+  let amount := (arrayElement notes i).amount
+  total := add total amount)
+return total
+```
+
+If it already works, add a focused smoke/feature test and docs example. If it
+does not work, first preserve the current boundary with a regression test and
+docs. Then implement the smallest macro/EDSL change needed so assignment to a
+mutable local inside `forEach` lowers to `Stmt.assignVar`, including whatever
+executable fallback adjustment is needed for `verity_contract` source terms.
+
+Do not introduce a separate `forEachAccum` unless the existing assignment syntax
+cannot be made to work cleanly.
+
+### 4. Multi-value internal helper returns
+
+Check whether macro syntax already supports `_buildPublicSignals`-style helper
+returns. Prefer a syntax that maps to existing `Stmt.internalCallAssign`, for
+example a tuple binding if that is already supported by local conventions.
+
+Add a smoke/feature test and docs example. If macro support is missing, add the
+smallest syntax extension that reuses the existing compilation-model
+`Stmt.internalCallAssign` machinery.
+
+### 5. `abiEncodePacked` helper
+
+Add helpers for static packed encoding used in hash preimages. The first version
+may support only a list of word-sized `Expr` values; a higher-ROI follow-up is a
+static segment helper with explicit 1- to 32-byte widths for address-sized and
+other sub-word preimages.
+
+Expected behavior:
+
+- writes each word at consecutive 32-byte offsets
+- for segment helpers, left-aligns sub-word values and places subsequent
+  segments at byte-precise offsets
+- computes the correct total byte length
+- returns `keccak256(offset, length)` or expands to existing `Expr.keccak256`
+  support
+- avoids ad hoc offset arithmetic in user contracts
+
+Add tests that inspect generated Yul or compilation-model output for correct
+offsets and length.
+
+### 6. `sha256` / `sha256Packed` helper
+
+Add a helper for SHA-256 precompile 0x02:
+
+- emits `staticcall(gas(), 2, inputOffset, inputSize, outputOffset, 32)`
+- reverts on precompile failure
+- returns `mload(outputOffset)` as the digest word
+
+If `sha256Packed` is added, it should reuse the same packed memory layout as
+`abiEncodePacked` but route to the SHA-256 precompile instead of `keccak256`.
+
+Add generated-Yul tests for precompile address, input size, output size, and
+failure handling.
+
+### 7. BN254 scalar helper
+
+Add a generic, documented helper for circuit-facing field reductions:
+
+```lean
+SNARK_SCALAR_FIELD =
+21888242871839275222246405745257275088548364400416034343698204186575808495617
+
+modField x = mod x SNARK_SCALAR_FIELD
+```
+
+Place it in a generic arithmetic/ZK helper location consistent with the repo's
+existing module layout. Add a small test or compile-time check.
+
+## Already Done: Do Not Reimplement
+
+- `address(this).balance` / `selfbalance()` support has already landed.
+- Named struct field access on calldata array elements is already supported via
+  `struct` declarations and `(arrayElement xs i).field`.
+- ERC-20 `balanceOf`, `allowance`, and `totalSupply` ECMs already exist in
+  `Compiler/Modules/ERC20.lean`.
+- Low-level primitives such as `mstore`, `keccak256`, `staticcall`, `call`,
+  `returndataSize`, `returndataCopy`, and `revertReturndata` already exist at
+  the macro or compilation-model level.
+
+## Verification
+
+Before opening a PR, run as much local validation as practical:
+
+```bash
+lake build Contracts Compiler PrintAxioms
+python3 scripts/generate_print_axioms.py --check
+make check
+```
+
+If a narrower test is added for a specific feature, run it directly as well.
+Report any tests that could not be run and why.
+
+## PR Expectations
+
+Keep the PR Verity-core only. The final PR description should include:
+
+- summary of implemented generic features
+- tests run
+- exact docs changed
+- explicit statement that Poseidon, Permit2, Lazy-IMT, Groth16, and the full
+  Unlink model remain in `unlink-verity`
+- trust-boundary notes for every new ECM or helper that emits low-level calls
diff --git a/scripts/check_macro_property_test_generation.py b/scripts/check_macro_property_test_generation.py
index 6575c3071..34d582389 100644
--- a/scripts/check_macro_property_test_generation.py
+++ b/scripts/check_macro_property_test_generation.py
@@ -23,6 +23,14 @@
     # arrays of tuple/struct values with nested dynamic members. This smoke is
     # covered by Lean macro invariant and round-trip tests instead.
     "DynamicStructArraySmoke",
+    # The generator does not fund the deployed contract before calling value
+    # forwarding ECM smoke entrypoints. Lean macro/model tests cover this
+    # low-level surface; a generated no-revert Foundry stub would be invalid.
+    "BubblingValueCallECMSmoke",
+    # External-call-module specs with hashing compile closures are covered by
+    # Lean macro/model tests; the standalone compiler artifact path does not
+    # materialize these ECM smoke contracts for generated no-revert stubs.
+    "PackedHashECMSmoke",
 }