Model keccak256 opcode, unaligned calldata, and SHA-256 engine in executable semantics

AXIOMS.md

@@ -118,6 +118,34 @@ structurally via `Compiler/Keccak/SpongeProperties.lean`.
 - End-to-end regression suites that exercise mapping reads/writes.
 - CI cross-checks kernel Keccak output against FFI Keccak output.
 
+### Kernel-computable source-semantics `keccak256(offset, size)`
+
+**Location**: `Compiler/Proofs/IRGeneration/SourceSemantics.lean`
+(`keccakMemorySlice`, `memorySliceBytesBE`, and the `.keccak256` arms of
+`evalExpr` / `evalExprWithHelpers`).
+
+**Role**:
+The executable source semantics evaluates `Expr.keccak256 offset size` by reading
+the `RuntimeState` memory as 256-bit words at `offset, offset+32, …`,
+concatenating them big-endian, truncating the result to `size` bytes, and hashing
+with the in-tree `KeccakEngine.keccak256`. Previously this expression evaluated to
+`none` (modeled as a revert), so any contract performing a native `keccak256` fell
+outside the modeled fragment; it is now executably modeled.
+
+**What we trust** (`keccak256_memory_slice_matches_evm`):
+Verity's compiled output writes scratch memory in whole 32-byte words (`mstore`),
+so reading whole words and truncating the big-endian concatenation to `size` bytes
+reproduces the EVM's byte-addressed `keccak256(offset, size)` preimage exactly. The
+`RuntimeState` memory is word-keyed, so sub-word / byte-granular aliasing is not
+modeled; this is faithful for the word-aligned access shape Verity emits and is the
+same assumption already surfaced in `--trust-report` for `Expr.keccak256`.
+
+**Soundness controls**:
+- Reuses the same kernel-computable `KeccakEngine.keccak256` that CI cross-checks
+  against FFI/EVM keccak; no new hash implementation is introduced.
+- `keccakMemorySlice` is an ordinary computable definition, not an axiom: it adds
+  no `axiom`/`sorry` to the trust surface.
+
 ## EVMYulLean Runtime Semantics (Non-Axiom)
 
 **Location**:

Compiler.lean

@@ -8,6 +8,8 @@ import Compiler.Codegen
 import Compiler.Linker
 import Compiler.Selector
 import Compiler.Selectors
+import Compiler.Sha256.Engine
+import Compiler.Sha256.EngineTest
 import Compiler.ParityPacks
 import Compiler.RandomGen
 import Compiler.CompilationModel

Compiler/CompilationModel/LogicalPurity.lean

@@ -259,6 +259,13 @@ def stmtContainsUnsafeLogicalCallLike : Stmt → Bool
   | Stmt.ecm _ args =>
       exprListAnyUnsafeLogicalCallLike args
   | Stmt.unsafeYul _ =>
+      -- Raw Yul is emitted verbatim, so the expression compiler never duplicates
+      -- its operands — the logicalAnd/logicalOr/ite operand-duplication hazard this
+      -- predicate guards against cannot arise for a raw fragment, so `false` is
+      -- correct. External calls inside a fragment are still caught for CEI /
+      -- no_external_calls by `stmtContainsExternalCall` / `stmtMayContainExternalCall`
+      -- in Validation; folding that detection in here instead produced a misleading
+      -- "move call-like expressions into Stmt.letVar" diagnostic.
       false
 termination_by s => sizeOf s
 decreasing_by all_goals simp_wf; all_goals omega

Compiler/CompilationModel/Types.lean

@@ -507,6 +507,53 @@ partial def yulStmtListScopeEffects : List YulStmt → StmtScopeEffects
       StmtScopeEffects.merge (yulStmtScopeEffects stmt) (yulStmtListScopeEffects rest)
 end
 
+mutual
+/-- Conservative scan for EVM external-call builtins inside raw Yul ASTs.
+    Unsafe-Yul fragments also declare mechanics metadata, but validation should
+    not miss a handwritten `call`/`staticcall`/`delegatecall` if the metadata is
+    under-declared. -/
+partial def yulExprContainsExternalCall : YulExpr → Bool
+  | .call func args =>
+      func == "call" ||
+        func == "staticcall" ||
+        func == "delegatecall" ||
+        yulExprListContainsExternalCall args
+  | _ => false
+
+partial def yulExprListContainsExternalCall : List YulExpr → Bool
+  | [] => false
+  | expr :: rest =>
+      yulExprContainsExternalCall expr || yulExprListContainsExternalCall rest
+
+partial def yulStmtContainsExternalCall : YulStmt → Bool
+  | .comment _ | .leave =>
+      false
+  | .let_ _ value | .letMany _ value | .assign _ value | .expr value =>
+      yulExprContainsExternalCall value
+  | .if_ cond body =>
+      yulExprContainsExternalCall cond || yulStmtListContainsExternalCall body
+  | .for_ init cond post body =>
+      yulStmtListContainsExternalCall init ||
+        yulExprContainsExternalCall cond ||
+        yulStmtListContainsExternalCall post ||
+        yulStmtListContainsExternalCall body
+  | .switch discr cases default =>
+      yulExprContainsExternalCall discr ||
+        cases.any (fun (_, body) => yulStmtListContainsExternalCall body) ||
+        match default with
+        | none => false
+        | some body => yulStmtListContainsExternalCall body
+  | .block stmts =>
+      yulStmtListContainsExternalCall stmts
+  | .funcDef _ _ _ body =>
+      yulStmtListContainsExternalCall body
+
+partial def yulStmtListContainsExternalCall : List YulStmt → Bool
+  | [] => false
+  | stmt :: rest =>
+      yulStmtContainsExternalCall stmt || yulStmtListContainsExternalCall rest
+end
+
 /-- Typed trust-report mechanics emitted by low-level statements and raw Yul fragments.
     JSON and human-readable reports still render these through `toReportString`,
     preserving the existing public report format while keeping the model boundary

Compiler/CompilationModel/Validation.lean

@@ -884,7 +884,8 @@ def stmtContainsExternalCall : Stmt → Bool
   | Stmt.unsafeYul fragment =>
       fragment.mechanics.contains .call ||
         fragment.mechanics.contains .staticcall ||
-        fragment.mechanics.contains .delegatecall
+        fragment.mechanics.contains .delegatecall ||
+        yulStmtListContainsExternalCall fragment.stmts
   | _ => false
 termination_by s => sizeOf s
 decreasing_by all_goals simp_wf; all_goals omega
@@ -920,6 +921,11 @@ def stmtMayContainExternalCall : Stmt → Bool
       stmtListMayContainExternalCall body
   | Stmt.matchAdt _ scrutinee branches =>
       exprMayContainExternalCall scrutinee || matchBranchesMayContainExternalCall branches
+  | Stmt.unsafeYul fragment =>
+      fragment.mechanics.contains .call ||
+        fragment.mechanics.contains .staticcall ||
+        fragment.mechanics.contains .delegatecall ||
+        yulStmtListContainsExternalCall fragment.stmts
   | Stmt.letVar _ value | Stmt.assignVar _ value =>
       exprMayContainExternalCall value
   | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setStorageWord _ _ value
@@ -1642,7 +1648,8 @@ def stmtInternalCEIViolation : Stmt → Bool → Option String
       let fragmentCalls :=
         fragment.mechanics.contains .call ||
           fragment.mechanics.contains .staticcall ||
-          fragment.mechanics.contains .delegatecall
+          fragment.mechanics.contains .delegatecall ||
+          yulStmtListContainsExternalCall fragment.stmts
       let fragmentWrites :=
         !fragment.scopeEffects.storageWrites.isEmpty ||
           fragment.mechanics.contains .storageWrite ||

Compiler/CompilationModelFeatureTest.lean

@@ -2814,6 +2814,47 @@ private def unsafeYulScopeObligation (name : String) : LocalObligation :=
     obligation := "Raw Yul scope effects must conservatively describe the Yul payload."
     proofStatus := .assumed }
 
+private def unsafeYulRawCallExpr : Compiler.Yul.YulExpr :=
+  Compiler.Yul.YulExpr.call "call" [
+    Compiler.Yul.YulExpr.lit 5000,
+    Compiler.Yul.YulExpr.lit 0,
+    Compiler.Yul.YulExpr.lit 0,
+    Compiler.Yul.YulExpr.lit 0,
+    Compiler.Yul.YulExpr.lit 0,
+    Compiler.Yul.YulExpr.lit 0,
+    Compiler.Yul.YulExpr.lit 0
+  ]
+
+private def unsafeYulRawCallStmt : Stmt :=
+  Stmt.unsafeYul {
+    label := "raw_yul_call"
+    stmts := [Compiler.Yul.YulStmt.expr unsafeYulRawCallExpr]
+    obligations := [unsafeYulScopeObligation "raw_yul_call_obligation"]
+  }
+
+private def unsafeYulRawCallAllowedSpec : CompilationModel := {
+  name := "UnsafeYulRawCallAllowed"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "bad"
+      params := []
+      returnType := none
+      body := [unsafeYulRawCallStmt, Stmt.stop]
+    }
+  ]
+}
+
+def unsafeYulRawCallPropagatesCEI : Bool :=
+  match stmtListCEIViolation [
+      unsafeYulRawCallStmt,
+      Stmt.setStorage "value" (Expr.literal 1)
+    ] false with
+  | some msg => contains msg "state write after external call"
+  | none => false
+
+example : unsafeYulRawCallPropagatesCEI = true := by native_decide
+
 private def unsafeYulUnderDeclaredBindSpec : CompilationModel := {
   name := "UnsafeYulUnderDeclaredBind"
   fields := []
@@ -5292,6 +5333,12 @@ set_option maxRecDepth 4096 in
     "unsafeYul tstore mechanic is rejected from view functions"
     unsafeYulTstoreMechanicViewRejectedSpec
     "function 'bad' is marked view but writes state"
+  discard <| expectCompile
+    "unsafeYul raw call AST is allowed by logical-purity validation"
+    unsafeYulRawCallAllowedSpec
+  expectTrue
+    "unsafeYul raw call AST propagates CEI seen-call state"
+    unsafeYulRawCallPropagatesCEI
   discard <| expectCompile
     "matchAdt with terminating branches"
     matchAdtAllBranchesTerminateSpec

Compiler/Proofs/IRGeneration/FunctionBody.lean

@@ -1966,9 +1966,9 @@ private theorem calldataloadWord_lt_evmModulus
     · -- offset ≥ 4: let binding then conditional
       dsimp only []
       split
-      · -- unaligned: returns 0
-        norm_num [Compiler.Constants.evmModulus]
-      · -- aligned: returns calldata.getD idx 0 % evmModulus
+      · -- aligned (r = 0): calldata.getD q 0 % evmModulus
+        exact Nat.mod_lt _ (by norm_num [Compiler.Constants.evmModulus])
+      · -- unaligned (r ≠ 0): composed hi/lo window reduced mod evmModulus
         exact Nat.mod_lt _ (by norm_num [Compiler.Constants.evmModulus])
 
 theorem compileExpr_calldataload_ok

Compiler/Proofs/IRGeneration/SourceSemantics.lean

@@ -2,6 +2,7 @@ import Compiler.Proofs.IRGeneration.SupportedSpec
 import Compiler.Proofs.IRGeneration.IRInterpreter
 import Compiler.Proofs.MappingSlot
 import Compiler.CompilationModel.LayoutValidation
+import Compiler.Keccak.Sponge
 
 set_option linter.unnecessarySimpa false
 set_option linter.unusedSimpArgs false
@@ -29,6 +30,32 @@ def addressModulus : Nat := 2 ^ 160
 def boolWord (b : Bool) : Nat :=
   if b then 1 else 0
 
+/-- Big-endian 32-byte encoding of a 256-bit word (byte 0 most significant). -/
+def wordToBytesBE (w : Nat) : ByteArray :=
+  ⟨((List.range 32).map (fun i => UInt8.ofNat ((w / (256 ^ (31 - i))) % 256))).toArray⟩
+
+/-- Concatenate the big-endian bytes of the word-aligned memory cells covering
+`[offset, offset + size)` and keep the first `size` bytes.
+
+This is faithful to EVM `keccak256(offset, size)` for the word-aligned access
+pattern Verity's compiler emits: one 32-byte cell per slot at `offset + 32*i`,
+matching how `mload`/`mstore` are modelled here (memory is keyed by byte offset
+and returns the full word stored at that key). -/
+def memorySliceBytesBE (memory : Nat → Verity.Core.Uint256) (offset size : Nat) :
+    ByteArray :=
+  let nWords := (size + 31) / 32
+  let full := (List.range nWords).foldl
+    (fun acc i => acc ++ wordToBytesBE (memory (offset + 32 * i)).val) ByteArray.empty
+  full.extract 0 size
+
+/-- Source-semantics model of `keccak256(offset, size)`: the in-tree pure Keccak
+engine applied to the word-aligned memory slice, returned as a big-endian word.
+Uses the real `KeccakEngine.keccak256`, so the modelled digest is the genuine
+Keccak-256 of the slice (no abstract placeholder). -/
+def keccakMemorySlice (memory : Nat → Verity.Core.Uint256) (offset size : Nat) : Nat :=
+  wordNormalize (KeccakEngine.byteArrayToNatBE
+    (KeccakEngine.keccak256 (memorySliceBytesBE memory offset size)))
+
 /-- Low-level proof encoding of an emitted event.
 
 Source execution stores the same log payload shape as proof IR `log*`
@@ -1040,6 +1067,10 @@ def evalExpr (fields : List Field) (state : RuntimeState) : Expr → Option Nat
   | .calldataload offset => do
       let resolvedOffset ← evalExpr fields state offset
       some (Compiler.Proofs.YulGeneration.calldataloadWord state.selector state.world.calldata resolvedOffset)
+  | .keccak256 offExpr sizeExpr => do
+      let off ← evalExpr fields state offExpr
+      let size ← evalExpr fields state sizeExpr
+      some (keccakMemorySlice state.world.memory off size)
   | .constructorArg idx =>
       lookupBinding? state.bindings s!"arg{idx}"
   | _ => none
@@ -1218,7 +1249,10 @@ private theorem evalExpr_keccak256
     (fields : List Field)
     (state : RuntimeState)
     (a b : Expr) :
-    evalExpr fields state (.keccak256 a b) = none := rfl
+    evalExpr fields state (.keccak256 a b) = (do
+      let off ← evalExpr fields state a
+      let size ← evalExpr fields state b
+      some (keccakMemorySlice state.world.memory off size)) := rfl
 
 private theorem evalExpr_mulDiv512Down
     (fields : List Field)
@@ -3016,6 +3050,12 @@ mutual
     | .calldataload offset => do
         let resolvedOffset ← evalExprWithHelpers spec fields fuel state offset
         some (Compiler.Proofs.YulGeneration.calldataloadWord state.selector state.world.calldata resolvedOffset)
+    | .keccak256 offExpr sizeExpr => do
+        -- Keep this in sync with the helper/call surface scans, which recurse
+        -- into the offset and size expressions.
+        let off ← evalExprWithHelpers spec fields fuel state offExpr
+        let size ← evalExprWithHelpers spec fields fuel state sizeExpr
+        some (keccakMemorySlice state.world.memory off size)
     -- Unmodeled / codegen-only constructors (no helper-aware semantics yet).
     -- Listed explicitly rather than via `| _ => none` so the
     -- `_mutual.eq_def` deriver does not enumerate the complement and trip
@@ -3033,7 +3073,6 @@ mutual
     | .arrayElementDynamicMemberDataOffset _ _ _
     | .arrayElementDynamicMemberElement _ _ _ _
     | .extcodesize _ | .returndataSize | .returndataOptionalBoolAt _
-    | .keccak256 _ _
     | .call _ _ _ _ _ _ _ | .staticcall _ _ _ _ _ _ | .delegatecall _ _ _ _ _ _
     | .externalCall _ _ | .mappingChain _ _ | .intrinsic _ _ _ _
     | .forkIfAtLeast _ _ _
@@ -3985,7 +4024,12 @@ mutual
         simp [evalExprWithHelpers, evalExpr_extcodesize,
           evalExpr_returndataOptionalBoolAt]
     | keccak256 a b =>
-        simpa [evalExprWithHelpers, evalExpr_keccak256]
+        simp only [exprTouchesUnsupportedHelperSurface, Bool.or_eq_false_iff] at hsurface
+        have ha :=
+          evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state a hsurface.1
+        have hb :=
+          evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state b hsurface.2
+        simpa [evalExprWithHelpers, evalExpr_keccak256, ha, hb]
     | call g t v io is oo os =>
         simpa [evalExprWithHelpers, evalExpr_call]
     | staticcall g t io is oo os =>

Compiler/Proofs/IRGeneration/SourceSemanticsFeatureTest.lean

@@ -92,6 +92,33 @@ private def storageWordSpec : CompilationModel :=
 private def storageWordState : SourceSemantics.RuntimeState :=
   { world := Verity.defaultState, bindings := [] }
 
+private def helperKeccakOffset : FunctionSpec :=
+  { name := "hashOffset"
+    params := []
+    returnType := some .uint256
+    isInternal := true
+    body := [Stmt.return (.literal 64)] }
+
+private def helperKeccakSize : FunctionSpec :=
+  { name := "hashSize"
+    params := []
+    returnType := some .uint256
+    isInternal := true
+    body := [Stmt.return (.literal 32)] }
+
+private def helperKeccakSpec : CompilationModel :=
+  { name := "HelperKeccak"
+    fields := []
+    constructor := none
+    functions := [helperKeccakOffset, helperKeccakSize] }
+
+private def helperKeccakWorld : Verity.ContractState :=
+  { Verity.defaultState with
+    memory := fun offset => if offset = 64 then 0x1234 else 0 }
+
+private def helperKeccakState : SourceSemantics.RuntimeState :=
+  { world := helperKeccakWorld, bindings := [] }
+
 private def resultStorageAt? (slot : Nat) : SourceSemantics.StmtResult → Option Nat
   | .continue st => some (st.world.storage slot).val
   | .stop st => some (st.world.storage slot).val
@@ -202,6 +229,14 @@ example :
                Verity.Core.Uint256.ofNat (11 % Compiler.Constants.evmModulus)] }] := by
   native_decide
 
+example :
+    SourceSemantics.evalExprWithHelpers helperKeccakSpec [] 1 helperKeccakState
+      (Expr.keccak256
+        (Expr.internalCall "hashOffset" [])
+        (Expr.internalCall "hashSize" [])) =
+      some (SourceSemantics.keccakMemorySlice helperKeccakWorld.memory 64 32) := by
+  native_decide
+
 example :
     resultStorageAt? 12
       (SourceSemantics.execStmtWithEvents storageWordFields [] storageWordState