Add generic Unlink audit readiness helpers

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

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

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

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