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

@@ -1046,6 +1046,69 @@ example : storeHelperPairTailNameCollisionExecutablePreservesParam = true := by
 
 end MacroTupleDestructuringSmoke
 
+namespace MacroHigherOrderInternalCallSmoke
+
+open Contracts
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+
+-- #1747: higher-order internal helpers (function-pointer parameters) are
+-- eliminated by a compile-time monomorphization pre-pass.  `applyTwice` takes a
+-- function pointer `op` and applies it twice; `runDouble` calls it with the
+-- statically-known helper `double`.  After the pre-pass the contract contains
+-- only first-order helpers: a synthesized clone `applyTwice_mono_double` (with
+-- `op` removed and every `op` call replaced by `double`) plus the rewritten
+-- call site.  Nothing downstream — model, IR, Yul — ever sees a function
+-- pointer, so the existing machinery applies unchanged.
+verity_contract HigherOrderDemo where
+  storage
+    result : Uint256 := slot 0
+
+  function double (x : Uint256) : Uint256 := do
+    return add x x
+
+  function applyTwice (op : Uint256 → Uint256, x : Uint256) : Uint256 := do
+    let once ← op x
+    let twice ← op once
+    return twice
+
+  function runDouble (seed : Uint256) : Uint256 := do
+    let out ← applyTwice double seed
+    return out
+
+-- The higher-order call `applyTwice double seed` is rewritten to a first-order
+-- call to the synthesized clone; the model never sees a function pointer.
+def runDoubleModelMonomorphizesHigherOrderCall : Bool :=
+  match HigherOrderDemo.runDouble_modelBody with
+  | [Stmt.letVar "out" (Expr.internalCall helperName [Expr.param "seed"]),
+      Stmt.return (Expr.localVar "out")] =>
+      helperName == "internal_applyTwice_mono_double"
+  | _ => false
+
+example : runDoubleModelMonomorphizesHigherOrderCall = true := by native_decide
+
+-- The synthesized clone is an ordinary first-order helper whose body calls the
+-- concrete helper `double` directly (the function pointer `op` is gone).
+def applyTwiceCloneModelCallsConcreteHelper : Bool :=
+  match HigherOrderDemo.applyTwice_mono_double_modelBody with
+  | [Stmt.letVar "once" (Expr.internalCall op1 [Expr.param "x"]),
+      Stmt.letVar "twice" (Expr.internalCall op2 [Expr.localVar "once"]),
+      Stmt.return (Expr.localVar "twice")] =>
+      op1 == "internal_double" && op2 == "internal_double"
+  | _ => false
+
+example : applyTwiceCloneModelCallsConcreteHelper = true := by native_decide
+
+-- End-to-end: the monomorphized contract still computes double (double seed).
+def runDoubleExecutableComputesDoubleApplication : Bool :=
+  match HigherOrderDemo.runDouble 5 Verity.defaultState with
+  | .success out _ => out == 20
+  | .revert _ _ => false
+
+example : runDoubleExecutableComputesDoubleApplication = true := by native_decide
+
+end MacroHigherOrderInternalCallSmoke
+
 namespace MacroQualifiedLibraryCallSmoke
 
 open Contracts
@@ -2814,6 +2877,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 +5396,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/Contract.lean

@@ -1466,10 +1466,14 @@ theorem compileFunctionSpec_correct_generic_except_mapping_writes_stmtSafety
     (hSupported := hSupported) hfn tx initialWorld] using hcorrect
 
 /-- Helper-proof-carrying function-level generic theorem.
-This is the proof-ready theorem surface for the next helper-composition step.
-Today the additional helper-proof argument is compatibility-redundant because
-the body proof still closes helpers through the helper-excluding
-`SupportedStmtList` fragment. -/
+This is the proof-ready theorem surface for the helper-composition step (#1630).
+The `hHelperProofs` argument is now backed by a first-class *source-level* reuse
+interface: `SourceSemantics.SupportedSpecHelperProofs.helperCallSummarySound` (and
+its `eval`/`exec` call-site corollaries) thread the once-proved helper catalog
+through to every selector-dispatched caller and call site. This compiled-side
+function proof still reduces through the helper-excluding `SupportedStmtList`
+fragment, so consuming that reuse interface here — retargeting the body proof —
+is the tracked next step; the trusted boundary is unchanged. -/
 theorem compileFunctionSpec_correct_generic_with_helper_proofs
     (model : CompilationModel)
     (selectors : List Nat)
@@ -1942,12 +1946,15 @@ theorem compile_preserves_semantics_except_mapping_writes_and_helper_ir_supporte
         (FunctionBody.initialIRStateForTx model tx initialWorld))
 
 /-- Helper-proof-carrying whole-contract Layer 2 theorem.
-This theorem family is the intended stable public interface for the helper
-composition step tracked by `#1630`: callers can already pass explicit
-summary-soundness evidence today, and once the body proof consumes it this
-theorem can strengthen without another theorem-shape rewrite. The current proof
-still reduces through the legacy helper-closed path, so the trusted boundary is
-unchanged. -/
+This theorem family is the stable public interface for the helper-composition
+step tracked by `#1630`. Callers pass explicit summary-soundness evidence
+(`hHelperProofs`), which is now reusable across callers through the source-level
+interface `SourceSemantics.SupportedSpecHelperProofs.helperCallSummarySound` (and
+its `eval`/`exec` call-site corollaries): one helper proof in the shared catalog
+discharges every call site of every selector-dispatched function. This
+whole-contract proof still reduces through the helper-closed path on the compiled
+side, so retargeting the body proof to consume that reuse is the remaining step;
+the trusted boundary is unchanged. -/
 theorem compile_preserves_semantics_with_helper_proofs
     (model : CompilationModel)
     (selectors : List Nat)

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