From f867472ddfef724cbc38d867689c2d379b6d2735 Mon Sep 17 00:00:00 2001
From: Marcin Benke <marcin.benke@argot.org>
Date: Wed, 5 Aug 2026 10:12:37 +0200
Subject: [PATCH] Comptime keccak256 over memory, with a symbolic free memory
 pointer

Let the partial evaluator run memory operations and keccak256 at compile
time, so that hashing idioms such as the EIP-712 domain separator fold to
a literal.

Memory ops (mload/mstore/mstore8/keccak256) are gated on comptime mode:
outside it, hashing memory the compiler cannot see would be unsound, so
the block is abandoned.  Memory is byte-level and sparse; an unwritten
byte reads as unknown rather than zero, since runtime code may have
written it first.

The free memory pointer's value is unknown at compile time, so it is
tracked symbolically as YulVal = Concrete | FreeOffset: mload(0x40)
yields FreeOffset 0, add/sub shift the offset, and every other operation
on it fails.  That address has no MAST form, so evaluating an expression
now yields both what to emit and what the evaluator additionally knows
(EvalResult); emission goes through the former, which makes leaking a
symbolic address into the program impossible by construction.

Absolute and free-relative addresses may alias at run time, so one
evaluation may use only one region, and any write disturbing the pointer
slot aborts the evaluation.

Finally, a call to a '-> comptime' function whose arguments are all known
must have folded by the time the verifier runs; if it survived, the
annotation's promise was not kept and the call site is reported.

Assisted-By: Claude Opus 5 (claude-opus-5)
---
 doc/comptime-asm.md                           | 131 +++++-
 src/Solcore/Backend/ComptimeCheck.hs          |  19 +-
 src/Solcore/Backend/MastEval.hs               | 429 ++++++++++++------
 test/Cases.hs                                 |   3 +
 test/YulEvalTests.hs                          | 413 +++++++++++++++--
 .../comptime/ct_comptime_unfolded.solc        |  17 +
 test/examples/comptime/ct_keccak_domain.solc  |  49 ++
 test/examples/comptime/ct_keccak_mem.solc     |  18 +
 8 files changed, 892 insertions(+), 187 deletions(-)
 create mode 100644 test/examples/comptime/ct_comptime_unfolded.solc
 create mode 100644 test/examples/comptime/ct_keccak_domain.solc
 create mode 100644 test/examples/comptime/ct_keccak_mem.solc

diff --git a/doc/comptime-asm.md b/doc/comptime-asm.md
index 671ce577a..dc8ac131c 100644
--- a/doc/comptime-asm.md
+++ b/doc/comptime-asm.md
@@ -2,8 +2,11 @@
 
 ## Status
 
-The initial Yul arithmetic interpreter is implemented in `src/Solcore/Backend/MastEval.hs`.
-It supports `add` and `mul`, replacing the earlier hardcoded `addWord`/`mulWord` builtins.
+The Yul interpreter lives in `src/Solcore/Backend/MastEval.hs`.  Word arithmetic,
+byte-level memory, `keccak256` and a symbolic free memory pointer are all
+implemented; the sections below record the design in the order it was built, so
+the "extension plan" headings describe work that is now done.  Where the plan and
+the implementation diverged, the later section says so.
 
 ---
 
@@ -12,12 +15,17 @@ It supports `add` and `mul`, replacing the earlier hardcoded `addWord`/`mulWord`
 ### YulState
 
 ```haskell
-type YulState = Map.Map Name Integer  -- variable bindings only (no memory yet)
+type YulState = Map.Map Name YulVal  -- variable bindings; memory lives in EvalM
 ```
 
+(`YulVal` was `Integer` originally; see "Pointers into memory" below.)
+
 ### Supported operations
 
-`evalYulOp` handles: `add`, `mul` (256-bit, wrapping mod 2^256).
+`evalYulOp` handles the 256-bit word ops in `evalWordOp`: `add`, `sub`, `mul`,
+`div`, `mod`, `gt`, `lt`, `eq`, `iszero`, `and`, `or`, `xor`, `not`, `shl`,
+`shr` — plus the memory ops `mload`, `mstore`, `mstore8` and `keccak256`, which
+have their own clauses because they touch `esMem`.
 
 `evalYulStmt` handles: `YAssign [n] e` — single-target assignment.
 
@@ -379,7 +387,7 @@ and the call site is left unevaluated.  In a comptime chain, if `get_free_memory
 called before anything has written to address 64 in `esMem`, `mloadWord` returns
 `Nothing` → inlining fails → the `let x : comptime` binding is not folded.  Correct.
 
-### Future: keccak256 over known memory
+### keccak256 over known memory
 
 The pattern in `hash1`/`hash2` in `std/NumLib.solc`:
 
@@ -389,9 +397,112 @@ result := keccak256(0, 32)
 ```
 
 When `x` is a known comptime value, the 32 bytes at `mem[0..31]` are known, and
-`keccak256` can be evaluated at compile time (the infrastructure already exists
-in `evalPrimitive` for `keccakLit`).  This requires reading a contiguous byte range
-from `esMem` — straightforward with the byte-level representation.
+`keccak256` is evaluated at compile time.  `mloadRange p n` reads a contiguous
+byte range from `esMem` (`Nothing` if any byte is unwritten) and `keccakInteger`
+hashes it — the same helper the `keccakLit` primitive uses.  Like `mload`, the
+op is gated on `envComptimeMode`.
+
+Two further conditions had to hold for the pattern to fold end to end:
+
+- **Statement expressions must be evaluated during inlining.**  `mstore(p, v)`
+  appears as a `MastStmtExp`, which `evalFunBody` used to discard.  Discarding it
+  skipped the memory write, so the following `keccak256` saw empty memory.
+- **`-> comptime` enables comptime mode.**  `withComptimeMode` was only entered
+  for the RHS of a `let x : comptime`.  `tryInline` now also enters it when the
+  callee is annotated `-> comptime`, which is what makes a call like
+  `eip712DomainSeparator(...)` fold at a plain `return`.
+
+### Pointers into memory (`get_free_memory`) — done
+
+Code that borrows scratch space above the free memory pointer —
+
+```
+let ptr = get_free_memory();
+mstore(ptr, ...); mstore(ptr + 32, ...);
+return keccak256(ptr, 160);
+```
+
+— now folds.  `get_free_memory()` is `mload(0x40)`, whose value is not known at
+compile time; seeding `esMem[0x40]` with `0x80` would be unsound, since the free
+pointer depends on the allocations that ran before.  Instead the base is
+**symbolic**: only offsets from it are tracked, never the base itself.
+
+```haskell
+data YulVal   = Concrete Integer | FreeOffset Integer
+data MemRegion = AbsoluteMem | FreeMem
+type MemAddr   = (MemRegion, Integer)
+```
+
+- `mload(0x40)` in comptime mode yields `FreeOffset 0`.
+- `add`/`sub` shift the offset; **every other operation on a `FreeOffset`
+  fails**, so a symbolic address can never become part of a folded word.
+- `esMem` is keyed by `MemAddr`, so `Concrete n` and `FreeOffset k` address
+  distinct regions.
+- Storing a `FreeOffset` *as a value* fails: written to memory it would lose its
+  base and could be read back as a plain word.
+
+Because a `FreeOffset` never materialises as a literal,
+`let p : comptime word = get_free_memory()` is still correctly rejected.
+
+#### The symbolic value crosses the MAST level
+
+The address is produced by a *call* (`get_free_memory()`), not inside a single
+asm block, so it has to survive `evalExp` → `tryInline` → `evalFunBody` and back.
+An interpreter-only change is therefore not enough.  Evaluating a MAST expression
+now yields two channels:
+
+```haskell
+data EvalResult = EvalResult
+  { resExp        :: MastExp          -- what to emit
+  , resFreeOffset :: Maybe Integer    -- what the evaluator additionally knows
+  }
+```
+
+`VEnv` maps variables to `EvalResult`.  Emission always goes through `resExp`, so
+a symbolic address is structurally incapable of leaking into the program: a
+variable bound to one is rebound to *itself* (`MastVar i`), and a call returning
+one keeps the call as its residual expression.  `resIsKnown` (may propagate) and
+`resIsFoldable` (may replace the expression) split apart accordingly.
+
+#### One region per evaluation
+
+`AbsoluteMem` and `FreeMem` may alias at run time — whether `0x80` is above the
+free pointer depends on its value.  Treating them as disjoint would be unsound
+(write `FreeOffset 0`, write `Concrete 128`, read `FreeOffset 0` → stale).  So a
+single comptime evaluation may use only **one** region: `regionUsable` compares
+the requested region against whatever is already in `esMem` and aborts on a mix.
+
+#### The free memory pointer must not move
+
+`FreeOffset` assumes the pointer stays put; reallocation is not modelled.  Any
+write overlapping `[64, 96)` — including `set_free_memory` and any wide `mstore`
+that reaches into the slot — aborts the evaluation (`touchesFreeMemPtr`).
+
+This is why the EIP-712 example writes above the free pointer rather than at
+fixed addresses 0..159: the latter would clobber the pointer slot at 64, in the
+compile-time model as much as at run time.
+
+#### Memory is reset on entering comptime mode
+
+Each comptime evaluation is an independent hypothetical execution and must not
+observe another's writes — otherwise two unrelated folds in one function would
+trip the single-region rule on each other.  `withComptimeMode` clears `esMem`
+when entering from outside, and keeps it on a nested entry (a `-> comptime` call
+inside a comptime let), which is part of the same evaluation.
+
+### Call sites of `-> comptime` functions must fold
+
+`Backend/ComptimeCheck.hs` runs after partial evaluation, so a call to a
+`-> comptime` function whose arguments are all known values (`isKnownValue`)
+should no longer be there.  If it survived, the evaluator could not compute the
+result and the annotation's promise was not kept; `checkCallSite` reports it.
+
+The check is deliberately limited to call sites:
+
+- Not on a `-> comptime` function's own `MastReturn`: inside the definition the
+  parameters are symbolic, so the body legitimately does not fold.
+- Not on `let x : comptime = e`: `evalLoopStmt` never folds comptime lets inside
+  loop bodies, so tightening that path would produce false positives.
 
 ---
 
@@ -469,7 +580,9 @@ Add patterns as described above.  Tests:
 Add `.solc` test in `test/examples/comptime/` with a function wrapping
 `mstore`/`mload` that should be comptime-evaluated.
 
-### Step 8 (later): keccak256 over known memory ranges
+### Step 8: keccak256 over known memory ranges — done
+
+See "keccak256 over known memory" above.
 
 ---
 
diff --git a/src/Solcore/Backend/ComptimeCheck.hs b/src/Solcore/Backend/ComptimeCheck.hs
index 04883ec7e..a4c64a69e 100644
--- a/src/Solcore/Backend/ComptimeCheck.hs
+++ b/src/Solcore/Backend/ComptimeCheck.hs
@@ -22,7 +22,7 @@ module Solcore.Backend.ComptimeCheck (checkComptime) where
 import Data.Map qualified as Map
 import Data.Set qualified as Set
 import Solcore.Backend.Mast
-import Solcore.Backend.MastEval (FunTable, buildFunTable, computePureFuns)
+import Solcore.Backend.MastEval (FunTable, buildFunTable, computePureFuns, isKnownValue)
 import Solcore.Frontend.Syntax.Name (Name)
 
 -- | Set of variable names known to be comptime in the current scope.
@@ -125,13 +125,14 @@ checkExp ft pure_ env (MastCond c t e) =
   mapM_ (checkExp ft pure_ env) [c, t, e]
 checkExp _ _ _ _ = Right ()
 
--- | Verify that comptime-annotated parameters receive comptime arguments.
+-- | Verify the annotations of the callee against this call site.
 checkCallSite :: FunTable -> Set.Set Name -> ComptimeEnv -> MastId -> [MastExp] -> Either String ()
 checkCallSite ft pure_ env f args =
   case Map.lookup (mastIdName f) ft of
     Nothing -> Right () -- builtin or unknown; no annotation to check
-    Just fd ->
+    Just fd -> do
       mapM_ checkArg (zip (mastFunParams fd) args)
+      checkFolded fd
   where
     checkArg (param, arg) =
       when_ (mastParamComptime param && not (isComptime ft pure_ env arg)) $
@@ -141,6 +142,18 @@ checkCallSite ft pure_ env f args =
           ++ show (mastIdName f)
           ++ "'"
 
+    -- Partial evaluation runs before this pass, and it folds a '-> comptime'
+    -- call whose arguments are all known values.  A surviving call means the
+    -- evaluator could not compute the result, so the annotation's promise was
+    -- not kept — most often because the body reads state the compiler cannot
+    -- know, or because it ran out of fuel.
+    checkFolded fd =
+      when_ (mastFunRetComptime fd && all isKnownValue args) $
+        "call to '"
+          ++ show (mastIdName f)
+          ++ "' annotated '-> comptime' was not evaluated at compile time, "
+          ++ "although all its arguments are known"
+
 -- | Classify an expression as comptime (True) or runtime (False).
 --
 -- A value is comptime if it is:
diff --git a/src/Solcore/Backend/MastEval.hs b/src/Solcore/Backend/MastEval.hs
index 7ab0c47a4..da817a2e0 100644
--- a/src/Solcore/Backend/MastEval.hs
+++ b/src/Solcore/Backend/MastEval.hs
@@ -5,12 +5,17 @@ module Solcore.Backend.MastEval
     FunTable,
     buildFunTable,
     computePureFuns,
+    isKnownValue,
     -- Evaluation monad (exported for testing)
     EvalEnv (..),
     EvalState (..),
     EvalM,
     runEvalM,
     -- Yul interpreter (exported for testing)
+    YulVal (..),
+    MemRegion (..),
+    MemAddr,
+    memAddr,
     YulState,
     evalYulExp,
     evalYulOp,
@@ -20,6 +25,7 @@ module Solcore.Backend.MastEval
     maskWord,
     mstoreBytes,
     mloadWord,
+    mloadRange,
     -- Primitive evaluator (exported for testing)
     evalPrimitive,
   )
@@ -42,7 +48,7 @@ import Data.Bits (complement, shiftL, shiftR, xor, (.&.), (.|.))
 import Data.ByteArray qualified as BA
 import Data.ByteString qualified as BS
 import Data.Map.Strict qualified as Map
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, isJust, isNothing)
 import Data.Set qualified as Set
 import Data.Text qualified as T
 import Data.Text.Encoding qualified as TE
@@ -58,9 +64,43 @@ import Solcore.Primitives.Primitives (integerPrimNames, memStringFromLitName, st
 -- Data structures
 -----------------------------------------------------------------------
 
+-- | The outcome of partially evaluating a MAST expression: the expression to
+-- emit, plus its offset from the free memory pointer when the value is a
+-- compile-time address.  Such an address has no MAST form — its base is only
+-- known at run time — so it travels beside 'resExp' rather than inside it.
+-- That way it can drive the comptime memory model without any risk of being
+-- folded into the emitted program.
+data EvalResult = EvalResult
+  { resExp :: MastExp,
+    resFreeOffset :: Maybe Integer
+  }
+
+plainResult :: MastExp -> EvalResult
+plainResult e = EvalResult {resExp = e, resFreeOffset = Nothing}
+
+-- | True if the value may be propagated through the environment: a literal,
+-- a constructor of such, or a symbolic address.
+resIsKnown :: EvalResult -> Bool
+resIsKnown r = isJust (resFreeOffset r) || isKnownValue (resExp r)
+
+-- | True if the value may replace its expression in the emitted program.
+-- A symbolic address may not: there is no MAST expression denoting it.
+resIsFoldable :: EvalResult -> Bool
+resIsFoldable r = isNothing (resFreeOffset r) && isKnownValue (resExp r)
+
 -- Variable environment: variable id (name + type) -> known value
 -- Uses full MastId to distinguish variables with same name but different types
-type VEnv = Map.Map MastId MastExp
+type VEnv = Map.Map MastId EvalResult
+
+-- | Record a variable's value, or forget it if the value is not known.
+-- A symbolic address is rebound to the variable itself, so that later uses emit
+-- the variable rather than re-running the expression that produced the address.
+bindResult :: MastId -> EvalResult -> VEnv -> VEnv
+bindResult i r env = case resFreeOffset r of
+  Just k -> Map.insert i (EvalResult (MastVar i) (Just k)) env
+  Nothing
+    | isKnownValue (resExp r) -> Map.insert i r env
+    | otherwise -> Map.delete i env
 
 -- Function table: function name -> definition
 type FunTable = Map.Map Name MastFunDef
@@ -72,9 +112,31 @@ type Fuel = Int
 -- Pre-scanned from the whole function body so it survives no-init let deletions.
 type TypeReg = Map.Map Name MastId
 
--- | State for Yul arithmetic interpretation.
--- Currently tracks only variable values; may be extended to include memory.
-type YulState = Map.Map Name Integer
+-- | A value in the Yul interpreter.  Most values are concrete 256-bit words,
+-- but reading the free memory pointer yields an address whose base is unknown
+-- at compile time.  Tracking it symbolically, as an offset from that base, lets
+-- comptime code borrow scratch space above the free pointer.
+data YulVal
+  = Concrete Integer
+  | FreeOffset Integer
+  deriving (Eq, Show)
+
+-- | Comptime memory is split into two regions: absolute addresses, and
+-- addresses relative to the free memory pointer.  Whether they overlap depends
+-- on the run-time value of that pointer, so a single comptime evaluation may
+-- only use one of them (see 'regionUsable').
+data MemRegion = AbsoluteMem | FreeMem
+  deriving (Eq, Ord, Show)
+
+type MemAddr = (MemRegion, Integer)
+
+-- | The memory address denoted by a Yul value.
+memAddr :: YulVal -> MemAddr
+memAddr (Concrete n) = (AbsoluteMem, n)
+memAddr (FreeOffset k) = (FreeMem, k)
+
+-- | State for Yul arithmetic interpretation: local Yul variable bindings.
+type YulState = Map.Map Name YulVal
 
 defaultFuel :: Fuel
 defaultFuel = 100
@@ -96,7 +158,7 @@ type CloneKey = (Name, [(Name, Literal)])
 
 data EvalState = EvalState
   { esFuel :: !Fuel,
-    esMem :: !(Map.Map Integer Word8),
+    esMem :: !(Map.Map MemAddr Word8),
     -- clones created so far, for reuse across call sites
     esCloneNames :: !(Map.Map CloneKey Name),
     -- clone definitions, by clone name; kept for clone-of-clone lookups
@@ -132,8 +194,15 @@ askComptimeMode :: EvalM Bool
 askComptimeMode = asks envComptimeMode
 
 -- Run an action with comptime mode enabled (memory ops become active).
+-- Entering comptime mode starts from fresh memory: each comptime evaluation is
+-- an independent hypothetical execution and must not observe another's writes.
+-- A nested entry (a '-> comptime' call inside a comptime let) keeps the memory,
+-- since it is part of the same evaluation.
 withComptimeMode :: EvalM a -> EvalM a
-withComptimeMode = local (\e -> e {envComptimeMode = True})
+withComptimeMode m = do
+  nested <- askComptimeMode
+  if nested then pure () else modifyMem (const Map.empty)
+  local (\e -> e {envComptimeMode = True}) m
 
 getFuel :: EvalM Fuel
 getFuel = lift $ gets esFuel
@@ -152,12 +221,23 @@ useFuel = do
 restoreFuel :: EvalM ()
 restoreFuel = lift $ modify (\s -> s {esFuel = esFuel s + 1})
 
-getsMem :: EvalM (Map.Map Integer Word8)
+getsMem :: EvalM (Map.Map MemAddr Word8)
 getsMem = lift $ gets esMem
 
-modifyMem :: (Map.Map Integer Word8 -> Map.Map Integer Word8) -> EvalM ()
+modifyMem :: (Map.Map MemAddr Word8 -> Map.Map MemAddr Word8) -> EvalM ()
 modifyMem f = lift $ modify (\s -> s {esMem = f (esMem s)})
 
+-- | True if a memory access in this region is compatible with what the current
+-- comptime evaluation has already written.  Absolute and free-pointer-relative
+-- addresses may alias at run time, so mixing the two regions within one
+-- evaluation could silently produce a wrong answer; the evaluator gives up.
+regionUsable :: MemRegion -> EvalM Bool
+regionUsable r = do
+  mem <- getsMem
+  pure $ case Map.lookupMin mem of
+    Nothing -> True
+    Just ((r', _), _) -> r' == r
+
 -----------------------------------------------------------------------
 -- Main entry point
 -----------------------------------------------------------------------
@@ -291,32 +371,28 @@ evalStmt tyReg env stmt = case stmt of
   MastLet ct i ty mInit -> do
     mInit' <- traverse (if ct then withComptimeMode . evalExp env else evalExp env) mInit
     let env' = case mInit' of
-          Just e | isKnownValue e -> Map.insert i e env
-          _ -> Map.delete i env -- Shadow/remove any existing binding
+          Just r -> bindResult i r env
+          Nothing -> Map.delete i env -- Shadow/remove any existing binding
           -- Comptime lets with known values are dead after evaluation: all uses will be
           -- substituted from VEnv, and EmitHull cannot handle string-typed variables.
     let stmts = case mInit' of
-          Just e | ct && isKnownValue e -> []
-          _ -> [MastLet ct i ty mInit']
+          Just r | ct && resIsFoldable r -> []
+          _ -> [MastLet ct i ty (resExp <$> mInit')]
     pure (env', stmts)
   MastAssign i e -> do
-    e' <- evalExp env e
-    let env' =
-          if isKnownValue e'
-            then Map.insert i e' env
-            else Map.delete i env -- Value no longer known
-            -- Always emit the assignment: the variable may be referenced by opaque asm blocks
-    pure (env', [MastAssign i e'])
+    r <- evalExp env e
+    -- Always emit the assignment: the variable may be referenced by opaque asm blocks
+    pure (bindResult i r env, [MastAssign i (resExp r)])
   MastStmtExp e -> do
-    e' <- evalExp env e
-    if isKnownValue e'
+    r <- evalExp env e
+    if resIsFoldable r
       then pure (env, [])
-      else pure (env, [MastStmtExp e'])
+      else pure (env, [MastStmtExp (resExp r)])
   MastReturn e -> do
-    e' <- evalExp env e
-    pure (env, [MastReturn e'])
+    r <- evalExp env e
+    pure (env, [MastReturn (resExp r)])
   MastMatch e alts -> do
-    e' <- evalExp env e
+    e' <- resExp <$> evalExp env e
     alts' <- mapM (evalAlt tyReg env) alts
     -- Any variable assigned in any alt may be updated; remove from env
     -- so downstream code doesn't see the pre-match value.
@@ -355,7 +431,7 @@ evalStmt tyReg env stmt = case stmt of
             `Set.union` foldMap assignedInStmt body
         loopEnv = foldr Map.delete env (Set.toList assigned)
     (_, initStmt') <- evalLoopStmt loopEnv initStmt
-    cond' <- evalExp loopEnv cond
+    cond' <- resExp <$> evalExp loopEnv cond
     (_, post') <- evalLoopStmt loopEnv post
     (_, bodies') <- mapAccumM evalLoopStmt loopEnv body
     pure (Map.empty, [MastFor initStmt' cond' post' bodies'])
@@ -367,24 +443,20 @@ evalLoopStmt env st = case st of
   MastLet ct i ty mInit -> do
     mInit' <- traverse (evalExp env) mInit
     let env' = case mInit' of
-          Just e | isKnownValue e -> Map.insert i e env
-          _ -> Map.delete i env
-    pure (env', MastLet ct i ty mInit')
+          Just r -> bindResult i r env
+          Nothing -> Map.delete i env
+    pure (env', MastLet ct i ty (resExp <$> mInit'))
   MastAssign i e -> do
-    e' <- evalExp env e
-    let env' =
-          if isKnownValue e'
-            then Map.insert i e' env
-            else Map.delete i env
-    pure (env', MastAssign i e')
+    r <- evalExp env e
+    pure (bindResult i r env, MastAssign i (resExp r))
   MastStmtExp e -> do
-    e' <- evalExp env e
+    e' <- resExp <$> evalExp env e
     pure (env, MastStmtExp e')
   MastReturn e -> do
-    e' <- evalExp env e
+    e' <- resExp <$> evalExp env e
     pure (env, MastReturn e')
   MastMatch e alts -> do
-    e' <- evalExp env e
+    e' <- resExp <$> evalExp env e
     -- No tyReg in loop context; asm in loop bodies is treated as opaque.
     alts' <- mapM (evalAlt Map.empty env) alts
     let mutated = foldMap (assignedInStmts . snd) alts
@@ -392,7 +464,7 @@ evalLoopStmt env st = case st of
     pure (env', MastMatch e' alts')
   MastFor initStmt cond post body -> do
     (_, initStmt') <- evalLoopStmt env initStmt
-    cond' <- evalExp env cond
+    cond' <- resExp <$> evalExp env cond
     (_, post') <- evalLoopStmt env post
     bodies' <- mapM (fmap snd . evalLoopStmt env) body
     pure (Map.empty, MastFor initStmt' cond' post' bodies')
@@ -415,7 +487,7 @@ evalAlt tyReg env (pat, body) = do
 -- MastPExp must reduce to a literal; any other form is a compile-time error.
 evalPat :: VEnv -> MastPat -> EvalM MastPat
 evalPat env (MastPExp e) = do
-  e' <- evalExp env e
+  e' <- resExp <$> evalExp env e
   case e' of
     MastLit l -> pure (MastPLit l)
     _ -> error $ "comptime expression in match label could not be evaluated to a literal: " ++ show e'
@@ -440,17 +512,18 @@ assignedInStmt _ = Set.empty
 -- Evaluate expressions
 -----------------------------------------------------------------------
 
-evalExp :: VEnv -> MastExp -> EvalM MastExp
-evalExp _ expr@(MastLit _) = pure expr
+evalExp :: VEnv -> MastExp -> EvalM EvalResult
+evalExp _ expr@(MastLit _) = pure (plainResult expr)
 evalExp env expr@(MastVar i) =
   pure $ case Map.lookup i env of
-    Just lit -> lit
-    Nothing -> expr
+    Just r -> r
+    Nothing -> plainResult expr
 evalExp env (MastCall i args) = do
   args' <- mapM (evalExp env) args
   let fname = mastIdName i
-  case evalPrimitive fname args' of
-    Just result -> pure result
+      residual = MastCall i (map resExp args')
+  case evalPrimitive fname (map resExp args') of
+    Just result -> pure (plainResult result)
     Nothing -> do
       -- Try inlining if we have fuel
       hasFuel <- useFuel
@@ -459,21 +532,26 @@ evalExp env (MastCall i args) = do
           result <- tryInline fname args'
           restoreFuel -- Restore fuel: it acts purely as recursion depth limit
           case result of
+            -- A symbolic address keeps the call as its residual expression:
+            -- the value itself cannot be written in MAST.
+            Just r | Just k <- resFreeOffset r -> pure (EvalResult residual (Just k))
             Just r -> pure r
             -- Not foldable to a value: the call stays, but it may still carry
             -- comptime-only arguments that have to be erased from the callee.
-            Nothing -> fromMaybe (MastCall i args') <$> tryCloneComptime i args'
-        else pure $ MastCall i args'
+            Nothing ->
+              plainResult . fromMaybe residual
+                <$> tryCloneComptime i (map resExp args')
+        else pure (plainResult residual)
 evalExp env (MastCon i es) = do
   es' <- mapM (evalExp env) es
-  pure $ MastCon i es'
+  pure $ plainResult (MastCon i (map resExp es'))
 evalExp env (MastCond e1 e2 e3) = do
   -- Evaluate all branches (conservative approach)
   -- Could potentially simplify if condition is known literal
-  e1' <- evalExp env e1
-  e2' <- evalExp env e2
-  e3' <- evalExp env e3
-  pure $ MastCond e1' e2' e3'
+  e1' <- resExp <$> evalExp env e1
+  e2' <- resExp <$> evalExp env e2
+  e3' <- resExp <$> evalExp env e3
+  pure $ plainResult (MastCond e1' e2' e3')
 
 -----------------------------------------------------------------------
 -- Primitive evaluation (named-function fast paths)
@@ -502,12 +580,7 @@ evalPrimitive (Name "strlenLit") [MastLit (StrLit s)] =
   let bs = TE.encodeUtf8 (T.pack s)
    in Just (MastLit (IntLit (toInteger (BS.length bs))))
 evalPrimitive (Name "keccakLit") [MastLit (StrLit s)] =
-  let bs = TE.encodeUtf8 (T.pack s)
-      digest :: Digest Keccak_256
-      digest = hash bs
-      digestBytes :: BS.ByteString
-      digestBytes = BA.convert digest
-   in Just (MastLit (IntLit (bsToIntegerBE digestBytes)))
+  Just (MastLit (IntLit (keccakInteger (TE.encodeUtf8 (T.pack s)))))
 -- Integer (comptime-only, unlimited precision) primitives:
 evalPrimitive (Name "wordToInteger") [MastLit (IntLit n)] =
   Just (MastLit (IntLit n)) -- value-level identity
@@ -527,6 +600,13 @@ evalPrimitive (QualName (Name "Int") "fromInteger") [x] = Just x -- identity for
 evalPrimitive (QualName (Name "Str") "fromString") [x] = Just x -- identity for string -> string
 evalPrimitive _ _ = Nothing
 
+-- | keccak256 of a byte sequence, as the 256-bit big-endian word EVM produces.
+keccakInteger :: BS.ByteString -> Integer
+keccakInteger bs = bsToIntegerBE (BA.convert digest)
+  where
+    digest :: Digest Keccak_256
+    digest = hash bs
+
 bsToIntegerBE :: BS.ByteString -> Integer
 bsToIntegerBE = BS.foldl' step 0
   where
@@ -557,11 +637,22 @@ wordMod = 2 ^ (256 :: Integer)
 maskWord :: Integer -> Integer
 maskWord n = n `mod` wordMod
 
+-- | The address at which the free memory pointer is kept.
+freeMemPtrSlot :: Integer
+freeMemPtrSlot = 64
+
+-- | True if writing n bytes at this address would disturb the free memory
+-- pointer.  The evaluator does not model reallocation — 'FreeOffset' assumes
+-- the pointer stays put — so such a write aborts the evaluation.
+touchesFreeMemPtr :: YulVal -> Integer -> Bool
+touchesFreeMemPtr (Concrete p) n = p < freeMemPtrSlot + 32 && freeMemPtrSlot < p + n
+touchesFreeMemPtr (FreeOffset _) _ = False
+
 -- | Write a 256-bit value to memory at byte address p (big-endian, 32 bytes).
-mstoreBytes :: Integer -> Integer -> Map.Map Integer Word8 -> Map.Map Integer Word8
-mstoreBytes p v mem =
+mstoreBytes :: MemAddr -> Integer -> Map.Map MemAddr Word8 -> Map.Map MemAddr Word8
+mstoreBytes (r, p) v mem =
   foldl'
-    (\m i -> Map.insert (p + i) (fromIntegral ((v `shiftR` (8 * (31 - fromIntegral i))) .&. 0xff)) m)
+    (\m i -> Map.insert (r, p + i) (fromIntegral ((v `shiftR` (8 * (31 - fromIntegral i))) .&. 0xff)) m)
     mem
     [0 .. 31]
 
@@ -570,12 +661,14 @@ mstoreBytes p v mem =
 -- evaluation. We cannot assume unwritten bytes are 0: runtime code may have
 -- written to memory before this function executes (e.g. the free memory pointer
 -- at slot 64 is set by initialization code before any user function runs).
-mloadWord :: Integer -> Map.Map Integer Word8 -> Maybe Integer
-mloadWord p mem =
-  foldl'
-    (\mAcc i -> do acc <- mAcc; b <- Map.lookup (p + i) mem; pure (acc * 256 + fromIntegral b))
-    (Just 0)
-    [0 .. 31]
+mloadWord :: MemAddr -> Map.Map MemAddr Word8 -> Maybe Integer
+mloadWord a mem = bsToIntegerBE <$> mloadRange a 32 mem
+
+-- | Read n bytes from memory starting at byte address p.
+-- Like 'mloadWord', returns Nothing unless every byte in the range was written
+-- during this comptime evaluation.
+mloadRange :: MemAddr -> Integer -> Map.Map MemAddr Word8 -> Maybe BS.ByteString
+mloadRange (r, p) n mem = BS.pack <$> traverse (\i -> Map.lookup (r, p + i) mem) [0 .. n - 1]
 
 -----------------------------------------------------------------------
 -- Yul interpreter: expression and statement evaluator (in EvalM)
@@ -584,11 +677,11 @@ mloadWord p mem =
 -- | Evaluate a Yul expression given the current Yul state.
 -- Returns Nothing if any operand is unknown or the operation is unsupported.
 -- Clause order matters: mload must precede the general YCall catch-all.
-evalYulExp :: YulState -> YulExp -> EvalM (Maybe Integer)
+evalYulExp :: YulState -> YulExp -> EvalM (Maybe YulVal)
 evalYulExp env (YIdent n) = pure (Map.lookup n env)
-evalYulExp _ (YLit (YulNumber n)) = pure (Just n)
-evalYulExp _ (YLit YulTrue) = pure (Just 1)
-evalYulExp _ (YLit YulFalse) = pure (Just 0)
+evalYulExp _ (YLit (YulNumber n)) = pure (Just (Concrete n))
+evalYulExp _ (YLit YulTrue) = pure (Just (Concrete 1))
+evalYulExp _ (YLit YulFalse) = pure (Just (Concrete 0))
 evalYulExp env (YCall (Name "mload") [pExp]) = do
   compt <- askComptimeMode
   if not compt
@@ -596,8 +689,22 @@ evalYulExp env (YCall (Name "mload") [pExp]) = do
     else do
       mp <- evalYulExp env pExp
       case mp of
-        Just p -> mloadWord p <$> getsMem -- Nothing if any byte unwritten
+        -- Reading the free memory pointer yields the symbolic base itself.
+        Just (Concrete p) | p == freeMemPtrSlot -> pure (Just (FreeOffset 0))
+        Just a -> withRegionOf a $ \addr mem -> Concrete <$> mloadWord addr mem
         Nothing -> pure Nothing
+evalYulExp env (YCall (Name "keccak256") [pExp, nExp]) = do
+  compt <- askComptimeMode
+  if not compt
+    then pure Nothing -- hashing memory is only meaningful in comptime context
+    else do
+      mp <- evalYulExp env pExp
+      mn <- evalYulExp env nExp
+      case (mp, mn) of
+        -- A length is always a plain word; only the address may be symbolic.
+        (Just a, Just (Concrete n)) ->
+          withRegionOf a $ \addr mem -> Concrete . keccakInteger <$> mloadRange addr n mem
+        _ -> pure Nothing
 evalYulExp env (YCall op args) = do
   mvals <- mapM (evalYulExp env) args
   case sequence mvals of
@@ -605,26 +712,53 @@ evalYulExp env (YCall op args) = do
     Just vals -> evalYulOp op vals
 evalYulExp _ _ = pure Nothing
 
--- | Evaluate a Yul built-in operation on known integer values.
+-- | Read comptime memory at the address denoted by a Yul value, provided that
+-- address lies in the region this evaluation is already using.
+withRegionOf :: YulVal -> (MemAddr -> Map.Map MemAddr Word8 -> Maybe a) -> EvalM (Maybe a)
+withRegionOf a k = do
+  let addr = memAddr a
+  ok <- regionUsable (fst addr)
+  if not ok
+    then pure Nothing
+    else do
+      mem <- getsMem
+      pure (k addr mem)
+
+-- | Evaluate a Yul built-in operation on known values.
 -- Returns Nothing for unsupported or unknown operations.
 -- All operations use EVM semantics: unsigned 256-bit arithmetic, no exceptions.
-evalYulOp :: Name -> [Integer] -> EvalM (Maybe Integer)
-evalYulOp (Name "add") [a, b] = pure (Just (maskWord (a + b)))
-evalYulOp (Name "sub") [a, b] = pure (Just (maskWord (a - b)))
-evalYulOp (Name "mul") [a, b] = pure (Just (maskWord (a * b)))
-evalYulOp (Name "div") [a, b] = pure (Just (if b == 0 then 0 else a `div` b))
-evalYulOp (Name "mod") [a, b] = pure (Just (if b == 0 then 0 else a `mod` b))
-evalYulOp (Name "gt") [a, b] = pure (Just (if a > b then 1 else 0))
-evalYulOp (Name "lt") [a, b] = pure (Just (if a < b then 1 else 0))
-evalYulOp (Name "eq") [a, b] = pure (Just (if a == b then 1 else 0))
-evalYulOp (Name "iszero") [a] = pure (Just (if a == 0 then 1 else 0))
-evalYulOp (Name "and") [a, b] = pure (Just (a .&. b))
-evalYulOp (Name "or") [a, b] = pure (Just (a .|. b))
-evalYulOp (Name "xor") [a, b] = pure (Just (a `xor` b))
-evalYulOp (Name "not") [a] = pure (Just (maskWord (complement a)))
-evalYulOp (Name "shl") [sh, v] = pure (Just (maskWord (v `shiftL` fromIntegral sh)))
-evalYulOp (Name "shr") [sh, v] = pure (Just (v `shiftR` fromIntegral sh))
-evalYulOp _ _ = pure Nothing
+-- Only add/sub accept the symbolic free-memory base, so it can be used as an
+-- address but can never end up in a folded word.
+evalYulOp :: Name -> [YulVal] -> EvalM (Maybe YulVal)
+evalYulOp (Name "add") [FreeOffset k, Concrete n] = pure (Just (FreeOffset (k + n)))
+evalYulOp (Name "add") [Concrete n, FreeOffset k] = pure (Just (FreeOffset (k + n)))
+evalYulOp (Name "sub") [FreeOffset k, Concrete n] = pure (Just (FreeOffset (k - n)))
+evalYulOp op args = pure $ do
+  ns <- traverse concreteVal args
+  Concrete <$> evalWordOp op ns
+
+concreteVal :: YulVal -> Maybe Integer
+concreteVal (Concrete n) = Just n
+concreteVal (FreeOffset _) = Nothing
+
+-- | The 256-bit word semantics of the supported Yul built-ins.
+evalWordOp :: Name -> [Integer] -> Maybe Integer
+evalWordOp (Name "add") [a, b] = Just (maskWord (a + b))
+evalWordOp (Name "sub") [a, b] = Just (maskWord (a - b))
+evalWordOp (Name "mul") [a, b] = Just (maskWord (a * b))
+evalWordOp (Name "div") [a, b] = Just (if b == 0 then 0 else a `div` b)
+evalWordOp (Name "mod") [a, b] = Just (if b == 0 then 0 else a `mod` b)
+evalWordOp (Name "gt") [a, b] = Just (if a > b then 1 else 0)
+evalWordOp (Name "lt") [a, b] = Just (if a < b then 1 else 0)
+evalWordOp (Name "eq") [a, b] = Just (if a == b then 1 else 0)
+evalWordOp (Name "iszero") [a] = Just (if a == 0 then 1 else 0)
+evalWordOp (Name "and") [a, b] = Just (a .&. b)
+evalWordOp (Name "or") [a, b] = Just (a .|. b)
+evalWordOp (Name "xor") [a, b] = Just (a `xor` b)
+evalWordOp (Name "not") [a] = Just (maskWord (complement a))
+evalWordOp (Name "shl") [sh, v] = Just (maskWord (v `shiftL` fromIntegral sh))
+evalWordOp (Name "shr") [sh, v] = Just (v `shiftR` fromIntegral sh)
+evalWordOp _ _ = Nothing
 
 -- | Evaluate one Yul statement, updating the Yul state.
 -- mstore/mstore8 update EvalM memory; assignments update YulState.
@@ -633,31 +767,44 @@ evalYulStmt :: YulState -> YulStmt -> EvalM (Maybe YulState)
 evalYulStmt env (YAssign [n] e) = do
   mv <- evalYulExp env e
   pure (fmap (\v -> Map.insert n v env) mv)
-evalYulStmt env (YExp (YCall (Name "mstore") [pExp, vExp])) = do
-  compt <- askComptimeMode
-  if not compt
-    then pure Nothing -- mstore only in comptime context; fail block so callers aren't inlined
-    else do
-      mp <- evalYulExp env pExp
-      mv <- evalYulExp env vExp
-      case (mp, mv) of
-        (Just p, Just v) -> do
-          modifyMem (mstoreBytes p v)
-          pure (Just env) -- YulState unchanged; memory updated in EvalM
-        _ -> pure Nothing
-evalYulStmt env (YExp (YCall (Name "mstore8") [pExp, vExp])) = do
+evalYulStmt env (YExp (YCall (Name "mstore") [pExp, vExp])) =
+  evalMemWrite env pExp vExp 32 $ \addr v -> mstoreBytes addr v
+evalYulStmt env (YExp (YCall (Name "mstore8") [pExp, vExp])) =
+  evalMemWrite env pExp vExp 1 $ \addr v -> Map.insert addr (fromIntegral (v .&. 0xff))
+evalYulStmt _ _ = pure Nothing
+
+-- | Common shape of mstore and mstore8: evaluate address and value, check that
+-- the write is one the comptime memory model can represent, then apply it.
+-- Returns Nothing (aborting the block) whenever it cannot, so that a function
+-- whose body writes memory is never inlined on the strength of a skipped write.
+evalMemWrite ::
+  YulState ->
+  YulExp ->
+  YulExp ->
+  Integer ->
+  (MemAddr -> Integer -> Map.Map MemAddr Word8 -> Map.Map MemAddr Word8) ->
+  EvalM (Maybe YulState)
+evalMemWrite env pExp vExp width write = do
   compt <- askComptimeMode
   if not compt
-    then pure Nothing -- mstore8 only in comptime context
+    then pure Nothing -- memory writes only in comptime context
     else do
       mp <- evalYulExp env pExp
       mv <- evalYulExp env vExp
       case (mp, mv) of
-        (Just p, Just v) -> do
-          modifyMem (Map.insert p (fromIntegral (v .&. 0xff)))
-          pure (Just env)
+        -- Moving the free memory pointer would invalidate the symbolic base.
+        (Just a, _) | touchesFreeMemPtr a width -> pure Nothing
+        -- Only concrete words are stored: a symbolic address written to memory
+        -- would lose its base and could later be read back as a plain word.
+        (Just a, Just (Concrete v)) -> do
+          let addr = memAddr a
+          ok <- regionUsable (fst addr)
+          if not ok
+            then pure Nothing
+            else do
+              modifyMem (write addr v)
+              pure (Just env) -- YulState unchanged; memory updated in EvalM
         _ -> pure Nothing
-evalYulStmt _ _ = pure Nothing
 
 -- | Evaluate a Yul block, threading the Yul state through each statement.
 -- Returns Nothing if any statement cannot be evaluated.
@@ -675,10 +822,13 @@ evalYulBlock env (s : ss) = do
 -- VEnv / YulState / TypeReg helpers
 -----------------------------------------------------------------------
 
--- | Extract known integer values from a VEnv into a YulState.
+-- | Extract known values from a VEnv into a YulState.
 venvToYulState :: VEnv -> YulState
-venvToYulState env =
-  Map.fromList [(mastIdName k, v) | (k, MastLit (IntLit v)) <- Map.toList env]
+venvToYulState env = Map.fromList (concatMap entry (Map.toList env))
+  where
+    entry (k, EvalResult _ (Just off)) = [(mastIdName k, FreeOffset off)]
+    entry (k, EvalResult (MastLit (IntLit v)) Nothing) = [(mastIdName k, Concrete v)]
+    entry _ = []
 
 -- | Build a name→YulExp substitution map from all known literal values in VEnv.
 -- Used to inline comptime values into asm blocks so that eliminated 'let' bindings
@@ -687,7 +837,7 @@ venvToSubst :: VEnv -> Map.Map Name YulExp
 venvToSubst env =
   Map.fromList
     [ (mastIdName k, yulLit l)
-    | (k, MastLit l) <- Map.toList env
+    | (k, EvalResult (MastLit l) Nothing) <- Map.toList env
     ]
   where
     yulLit (IntLit v) = YLit (YulNumber v)
@@ -732,8 +882,12 @@ mergeYulStateToVEnv tyReg yulState venv =
   where
     update acc n v =
       case Map.lookup n tyReg of
-        Just mastId -> Map.insert mastId (MastLit (IntLit v)) acc
         Nothing -> acc
+        Just mastId -> case v of
+          Concrete w -> Map.insert mastId (plainResult (MastLit (IntLit w))) acc
+          -- A symbolic address is known to the evaluator but has no MAST form,
+          -- so the variable itself stands for it in the emitted program.
+          FreeOffset off -> Map.insert mastId (EvalResult (MastVar mastId) (Just off)) acc
 
 -----------------------------------------------------------------------
 -- Comptime-only parameter erasure
@@ -809,7 +963,7 @@ cloneWith fd binds args = do
     cloneTy = foldr (MastArrow . mastParamType) (mastFunReturn fd) keptParams
     env0 =
       Map.fromList
-        [ (MastId (mastParamName p) (mastParamType p), MastLit l)
+        [ (MastId (mastParamName p) (mastParamType p), plainResult (MastLit l))
         | (p, l) <- binds
         ]
     -- Each new clone costs fuel, permanently.  A recursive callee that derives
@@ -850,7 +1004,7 @@ suffixName (QualName q s) suffix = QualName q (s ++ suffix)
 -- Works when: (1) all arguments are known values, or
 --             (2) function is "constant" (ignores its arguments)
 -- Only pure functions (no non-interpretable asm, no impure calls) are eligible.
-tryInline :: Name -> [MastExp] -> EvalM (Maybe MastExp)
+tryInline :: Name -> [EvalResult] -> EvalM (Maybe EvalResult)
 tryInline fname args = do
   pureFuns <- askPureFuns
   if fname `Set.notMember` pureFuns
@@ -866,31 +1020,34 @@ tryInline fname args = do
                   paramToId p = MastId (mastParamName p) (mastParamType p)
                   env = Map.fromList $ zip (map paramToId params) args
                   tyReg = buildTypeReg params (mastFunBody fd)
-              evalFunBody tyReg env (mastFunBody fd)
+                  -- '-> comptime' asserts the body is a compile-time computation,
+                  -- so its memory operations may run even outside a comptime let.
+                  inComptime = if mastFunRetComptime fd then withComptimeMode else id
+              inComptime $ evalFunBody tyReg env (mastFunBody fd)
 
 -- Evaluate a function body and extract the return value
-evalFunBody :: TypeReg -> VEnv -> [MastStmt] -> EvalM (Maybe MastExp)
+evalFunBody :: TypeReg -> VEnv -> [MastStmt] -> EvalM (Maybe EvalResult)
 evalFunBody _ _ [] = pure Nothing -- No return statement found
 evalFunBody tyReg env (stmt : rest) = case stmt of
   MastLet _ i _ mInit -> do
     mInit' <- traverse (evalExp env) mInit
     let env' = case mInit' of
-          Just e | isKnownValue e -> Map.insert i e env
-          _ -> Map.delete i env
+          Just r -> bindResult i r env
+          Nothing -> Map.delete i env
     evalFunBody tyReg env' rest
   MastAssign i e -> do
-    e' <- evalExp env e
-    let env' =
-          if isKnownValue e'
-            then Map.insert i e' env
-            else Map.delete i env
-    evalFunBody tyReg env' rest
-  MastStmtExp _ -> evalFunBody tyReg env rest
+    r <- evalExp env e
+    evalFunBody tyReg (bindResult i r env) rest
+  -- Evaluate for effect: a void call such as `mstore(p, v)` contributes
+  -- nothing to the environment but does write comptime memory.
+  MastStmtExp e -> do
+    _ <- evalExp env e
+    evalFunBody tyReg env rest
   MastReturn e -> do
-    e' <- evalExp env e
-    pure $ if isKnownValue e' then Just e' else Nothing
+    r <- evalExp env e
+    pure $ if resIsKnown r then Just r else Nothing
   MastMatch scrut alts -> do
-    scrut' <- evalExp env scrut
+    scrut' <- resExp <$> evalExp env scrut
     alts' <- mapM (\(p, b) -> (,b) <$> evalPat env p) alts
     case matchAlts env scrut' alts' of
       Just (env', body) -> evalFunBody tyReg env' body
@@ -928,7 +1085,7 @@ findConMatch env conName args ((pat, body) : rest) =
             Just env' -> Just (env', body)
             Nothing -> findConMatch env conName args rest
     MastPVar varId ->
-      let env' = Map.insert varId (MastCon (MastId conName (mastIdType varId)) args) env
+      let env' = Map.insert varId (plainResult (MastCon (MastId conName (mastIdType varId)) args)) env
        in Just (env', body)
     MastPWildcard -> Just (env, body)
     _ -> findConMatch env conName args rest
@@ -940,7 +1097,7 @@ findLitMatch env lit ((pat, body) : rest) =
   case pat of
     MastPLit patLit | patLit == lit -> Just (env, body)
     MastPVar varId ->
-      let env' = Map.insert varId (MastLit lit) env
+      let env' = Map.insert varId (plainResult (MastLit lit)) env
        in Just (env', body)
     MastPWildcard -> Just (env, body)
     MastPExp _ -> error "PANIC: MastPExp reached findLitMatch — evalAlt failed to evaluate it"
@@ -956,7 +1113,7 @@ bindPatterns env (pat : pats) (arg : args) =
     MastPVar varId ->
       let env' =
             if isKnownValue arg
-              then Map.insert varId arg env
+              then Map.insert varId (plainResult arg) env
               else Map.delete varId env
        in bindPatterns env' pats args
     MastPWildcard -> bindPatterns env pats args
@@ -1083,12 +1240,14 @@ asmIsInterpretable = all interpretableStmt
     interpretableStmt (YExp (YCall (Name "mstore8") [p, v])) = interpretableExp p && interpretableExp v
     interpretableStmt _ = False
 
-    -- mload has its own clause (reads memory); general YCall delegates to interpretableOp
+    -- mload and keccak256 have their own clauses (they read memory);
+    -- general YCall delegates to interpretableOp
     interpretableExp (YIdent _) = True
     interpretableExp (YLit (YulNumber _)) = True
     interpretableExp (YLit YulTrue) = True
     interpretableExp (YLit YulFalse) = True
     interpretableExp (YCall (Name "mload") [p]) = interpretableExp p
+    interpretableExp (YCall (Name "keccak256") [p, n]) = interpretableExp p && interpretableExp n
     interpretableExp (YCall op args) =
       interpretableOp op (length args) && all interpretableExp args
     interpretableExp _ = False
diff --git a/test/Cases.hs b/test/Cases.hs
index 8049c63a5..b0c66f7f2 100644
--- a/test/Cases.hs
+++ b/test/Cases.hs
@@ -44,6 +44,8 @@ comptime =
       runTestForFile "fib2.solc" comptimeFolder,
       runTestForFile "fib3.solc" comptimeFolder,
       runTestForFile "ct_asm_mem.solc" comptimeFolder,
+      runTestForFile "ct_keccak_mem.solc" comptimeFolder,
+      runTestForFile "ct_keccak_domain.solc" comptimeFolder,
       runTestForFile "integer-basic.solc" comptimeFolder,
       runTestForFile "integer-fib.solc" comptimeFolder,
       runTestForFile "integer-from-integer.solc" comptimeFolder,
@@ -69,6 +71,7 @@ comptime =
       runTestExpectingFailure "ct_runtime_arg.solc" comptimeFolder,
       runTestExpectingFailure "ct_let_runtime.solc" comptimeFolder,
       runTestExpectingFailure "ct_asm_ret.solc" comptimeFolder,
+      runTestExpectingFailure "ct_comptime_unfolded.solc" comptimeFolder,
       runTestExpectingFailure "ct_overloaded_bad.solc" comptimeFolder,
       runTestExpectingFailure "string-mem-runtime-fail.solc" comptimeFolder
     ]
diff --git a/test/YulEvalTests.hs b/test/YulEvalTests.hs
index a4f28f4cb..68bea7821 100644
--- a/test/YulEvalTests.hs
+++ b/test/YulEvalTests.hs
@@ -1,10 +1,11 @@
 module YulEvalTests (yulEvalTests) where
 
+import Data.ByteString qualified as BS
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Data.Word (Word8)
 import Language.Yul (YLiteral (..), YulExp (..), YulStmt (..))
-import Solcore.Backend.Mast (MastExp (..), MastId (..), MastTy (..), mastIdName)
+import Solcore.Backend.Mast
 import Solcore.Backend.MastEval
 import Solcore.Frontend.Syntax.Name
 import Solcore.Frontend.Syntax.Stmt (Literal (..))
@@ -27,8 +28,25 @@ yAssign n e = YAssign [Name n] e
 yExp :: String -> [YulExp] -> YulStmt
 yExp op args = YExp (YCall (Name op) args)
 
+-- A Yul state of concrete words
 st :: [(String, Integer)] -> YulState
-st = Map.fromList . map (\(n, v) -> (Name n, v))
+st = Map.fromList . map (\(n, v) -> (Name n, Concrete v))
+
+-- An absolute comptime memory address
+at :: Integer -> MemAddr
+at n = (AbsoluteMem, n)
+
+-- A comptime memory address at an offset above the free memory pointer
+above :: Integer -> MemAddr
+above k = (FreeMem, k)
+
+-- Apply a Yul built-in to concrete words, keeping only a concrete result
+wordOp :: String -> [Integer] -> Maybe Integer
+wordOp op args = runPure (evalYulOp (Name op) (map Concrete args)) >>= asWord
+
+asWord :: YulVal -> Maybe Integer
+asWord (Concrete n) = Just n
+asWord (FreeOffset _) = Nothing
 
 -- Run an EvalM action in non-comptime mode (memory ops inactive).
 runPure :: EvalM a -> a
@@ -58,6 +76,9 @@ yulEvalTests =
       evalYulBlockTests,
       memoryHelperTests,
       memoryEvalTests,
+      freeMemoryTests,
+      keccakEvalTests,
+      comptimeFoldingTests,
       asmIsInterpretableTests
     ]
 
@@ -125,48 +146,48 @@ evalYulOpTests =
   testGroup
     "evalYulOp"
     [ testCase "add: 3 + 5 = 8" $
-        runPure (evalYulOp (Name "add") [3, 5]) @?= Just 8,
+        wordOp "add" [3, 5] @?= Just 8,
       testCase "add: 0 + 0 = 0" $
-        runPure (evalYulOp (Name "add") [0, 0]) @?= Just 0,
+        wordOp "add" [0, 0] @?= Just 0,
       testCase "add: identity with 0" $
-        runPure (evalYulOp (Name "add") [42, 0]) @?= Just 42,
+        wordOp "add" [42, 0] @?= Just 42,
       testCase "add: wraps at 2^256" $
-        runPure (evalYulOp (Name "add") [maskWord (-1), 1]) @?= Just 0,
+        wordOp "add" [maskWord (-1), 1] @?= Just 0,
       testCase "add: large numbers stay within 256 bits" $
-        runPure (evalYulOp (Name "add") [maskWord (-1), maskWord (-1)])
+        wordOp "add" [maskWord (-1), maskWord (-1)]
           @?= Just (maskWord (-2)),
       testCase "mul: 3 * 5 = 15" $
-        runPure (evalYulOp (Name "mul") [3, 5]) @?= Just 15,
+        wordOp "mul" [3, 5] @?= Just 15,
       testCase "mul: 0 * anything = 0" $
-        runPure (evalYulOp (Name "mul") [0, 99]) @?= Just 0,
+        wordOp "mul" [0, 99] @?= Just 0,
       testCase "mul: 1 * anything = anything" $
-        runPure (evalYulOp (Name "mul") [1, 7]) @?= Just 7,
+        wordOp "mul" [1, 7] @?= Just 7,
       testCase "mul: wraps at 2^256" $
-        runPure (evalYulOp (Name "mul") [2 ^ (128 :: Integer), 2 ^ (128 :: Integer)]) @?= Just 0,
+        wordOp "mul" [2 ^ (128 :: Integer), 2 ^ (128 :: Integer)] @?= Just 0,
       testCase "sload: unsupported → Nothing" $
-        runPure (evalYulOp (Name "sload") [0]) @?= Nothing,
+        wordOp "sload" [0] @?= Nothing,
       testCase "sub: 10 - 3 = 7" $
-        runPure (evalYulOp (Name "sub") [10, 3]) @?= Just 7,
+        wordOp "sub" [10, 3] @?= Just 7,
       testCase "sub: wraps at 2^256" $
-        runPure (evalYulOp (Name "sub") [0, 1]) @?= Just (2 ^ (256 :: Integer) - 1),
+        wordOp "sub" [0, 1] @?= Just (2 ^ (256 :: Integer) - 1),
       testCase "gt: 5 > 3 = 1" $
-        runPure (evalYulOp (Name "gt") [5, 3]) @?= Just 1,
+        wordOp "gt" [5, 3] @?= Just 1,
       testCase "gt: 3 > 5 = 0" $
-        runPure (evalYulOp (Name "gt") [3, 5]) @?= Just 0,
+        wordOp "gt" [3, 5] @?= Just 0,
       testCase "lt: 3 < 5 = 1" $
-        runPure (evalYulOp (Name "lt") [3, 5]) @?= Just 1,
+        wordOp "lt" [3, 5] @?= Just 1,
       testCase "eq: 4 == 4 = 1" $
-        runPure (evalYulOp (Name "eq") [4, 4]) @?= Just 1,
+        wordOp "eq" [4, 4] @?= Just 1,
       testCase "eq: 4 == 5 = 0" $
-        runPure (evalYulOp (Name "eq") [4, 5]) @?= Just 0,
+        wordOp "eq" [4, 5] @?= Just 0,
       testCase "iszero: 0 = 1" $
-        runPure (evalYulOp (Name "iszero") [0]) @?= Just 1,
+        wordOp "iszero" [0] @?= Just 1,
       testCase "iszero: 1 = 0" $
-        runPure (evalYulOp (Name "iszero") [1]) @?= Just 0,
+        wordOp "iszero" [1] @?= Just 0,
       testCase "add with wrong arity → Nothing" $
-        runPure (evalYulOp (Name "add") [1, 2, 3]) @?= Nothing,
+        wordOp "add" [1, 2, 3] @?= Nothing,
       testCase "unknown op → Nothing" $
-        runPure (evalYulOp (Name "frobnicate") [1, 2]) @?= Nothing
+        wordOp "frobnicate" [1, 2] @?= Nothing
     ]
 
 -----------------------------------------------------------------------
@@ -178,30 +199,30 @@ evalYulExpTests =
   testGroup
     "evalYulExp"
     [ testCase "YLit number → its value" $
-        runPure (evalYulExp Map.empty (yNum 42)) @?= Just 42,
+        runPure (evalYulExp Map.empty (yNum 42)) @?= Just (Concrete 42),
       testCase "YLit true → 1" $
-        runPure (evalYulExp Map.empty (YLit YulTrue)) @?= Just 1,
+        runPure (evalYulExp Map.empty (YLit YulTrue)) @?= Just (Concrete 1),
       testCase "YLit false → 0" $
-        runPure (evalYulExp Map.empty (YLit YulFalse)) @?= Just 0,
+        runPure (evalYulExp Map.empty (YLit YulFalse)) @?= Just (Concrete 0),
       testCase "YIdent: known variable → its value" $
-        runPure (evalYulExp (st [("x", 5)]) (yIdent "x")) @?= Just 5,
+        runPure (evalYulExp (st [("x", 5)]) (yIdent "x")) @?= Just (Concrete 5),
       testCase "YIdent: unknown variable → Nothing" $
         runPure (evalYulExp Map.empty (yIdent "x")) @?= Nothing,
       testCase "YCall add with two literals" $
-        runPure (evalYulExp Map.empty (yCall "add" [yNum 3, yNum 5])) @?= Just 8,
+        runPure (evalYulExp Map.empty (yCall "add" [yNum 3, yNum 5])) @?= Just (Concrete 8),
       testCase "YCall add with variable and literal" $
-        runPure (evalYulExp (st [("x", 3)]) (yCall "add" [yIdent "x", yNum 5])) @?= Just 8,
+        runPure (evalYulExp (st [("x", 3)]) (yCall "add" [yIdent "x", yNum 5])) @?= Just (Concrete 8),
       testCase "YCall add with two variables" $
         runPure (evalYulExp (st [("x", 4), ("y", 6)]) (yCall "add" [yIdent "x", yIdent "y"]))
-          @?= Just 10,
+          @?= Just (Concrete 10),
       testCase "YCall add: one unknown variable → Nothing" $
         runPure (evalYulExp (st [("x", 4)]) (yCall "add" [yIdent "x", yIdent "y"]))
           @?= Nothing,
       testCase "YCall mul with literals" $
-        runPure (evalYulExp Map.empty (yCall "mul" [yNum 6, yNum 7])) @?= Just 42,
+        runPure (evalYulExp Map.empty (yCall "mul" [yNum 6, yNum 7])) @?= Just (Concrete 42),
       testCase "YCall nested: mul(add(2,3), 4)" $
         runPure (evalYulExp Map.empty (yCall "mul" [yCall "add" [yNum 2, yNum 3], yNum 4]))
-          @?= Just 20,
+          @?= Just (Concrete 20),
       testCase "YCall sload: unsupported → Nothing" $
         runPure (evalYulExp Map.empty (yCall "sload" [yNum 0])) @?= Nothing,
       testCase "YCall with unknown arg makes whole call Nothing" $
@@ -279,28 +300,28 @@ memoryHelperTests =
   testGroup
     "Memory helpers (mstoreBytes / mloadWord)"
     [ testCase "round-trip: store then load recovers value" $
-        mloadWord 0 (mstoreBytes 0 42 Map.empty) @?= Just 42,
+        mloadWord (at 0) (mstoreBytes (at 0) 42 Map.empty) @?= Just 42,
       testCase "round-trip: non-zero address" $
-        mloadWord 64 (mstoreBytes 64 999 Map.empty) @?= Just 999,
+        mloadWord (at 64) (mstoreBytes (at 64) 999 Map.empty) @?= Just 999,
       testCase "round-trip: max word value" $
-        mloadWord 0 (mstoreBytes 0 (maskWord (-1)) Map.empty) @?= Just (maskWord (-1)),
+        mloadWord (at 0) (mstoreBytes (at 0) (maskWord (-1)) Map.empty) @?= Just (maskWord (-1)),
       testCase "load from unwritten address returns Nothing" $
         -- Cannot assume unwritten bytes are 0: runtime code may have written to memory
-        mloadWord 0 Map.empty @?= Nothing,
+        mloadWord (at 0) Map.empty @?= Nothing,
       testCase "overlapping stores: all 32 bytes covered, value is computable" $ do
         -- mstore(0, x) writes bytes 0..31; mstore(1, y) writes bytes 1..32.
         -- mload(0) reads bytes 0..31: all present (byte 0 from first, 1..31 from second).
         let x = 0x0102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f20 :: Integer
             y = 0xaabbccdd00000000000000000000000000000000000000000000000000000001 :: Integer
-            mem = mstoreBytes 1 y (mstoreBytes 0 x Map.empty)
-            result = mloadWord 0 mem
+            mem = mstoreBytes (at 1) y (mstoreBytes (at 0) x Map.empty)
+            result = mloadWord (at 0) mem
             -- byte 0: from mstore(0,x) → 0x01; bytes 1..31: from mstore(1,y) → 0xaa,0xbb,...
             expected = 0x01aabbccdd000000000000000000000000000000000000000000000000000000
         result @?= Just expected,
       testCase "partial write (mstore8 only): mloadWord returns Nothing" $ do
         -- Only one byte written; the other 31 are unknown → Nothing
-        let mem = Map.insert 31 (0x34 :: Word8) Map.empty
-        mloadWord 0 mem @?= Nothing
+        let mem = Map.insert (at 31) (0x34 :: Word8) Map.empty
+        mloadWord (at 0) mem @?= Nothing
     ]
 
 -----------------------------------------------------------------------
@@ -409,6 +430,315 @@ memoryEvalTests =
           @?= Nothing
     ]
 
+-----------------------------------------------------------------------
+-- The symbolic free memory pointer
+-----------------------------------------------------------------------
+
+freeMemoryTests :: TestTree
+freeMemoryTests =
+  testGroup
+    "Symbolic free memory pointer"
+    [ testCase "mload(0x40) yields the symbolic base" $
+        runComptime (evalYulExp Map.empty (yCall "mload" [yNum 64]))
+          @?= Just (FreeOffset 0),
+      testCase "mload(0x40) outside comptime mode → Nothing" $
+        runPure (evalYulExp Map.empty (yCall "mload" [yNum 64])) @?= Nothing,
+      testCase "add shifts the symbolic offset" $
+        runComptime (evalYulOp (Name "add") [FreeOffset 0, Concrete 32])
+          @?= Just (FreeOffset 32),
+      testCase "add shifts the symbolic offset from either side" $
+        runComptime (evalYulOp (Name "add") [Concrete 32, FreeOffset 64])
+          @?= Just (FreeOffset 96),
+      testCase "sub shifts the symbolic offset" $
+        runComptime (evalYulOp (Name "sub") [FreeOffset 64, Concrete 32])
+          @?= Just (FreeOffset 32),
+      testCase "arithmetic on two symbolic addresses → Nothing" $
+        runComptime (evalYulOp (Name "add") [FreeOffset 0, FreeOffset 32]) @?= Nothing,
+      testCase "multiplying a symbolic address → Nothing" $
+        runComptime (evalYulOp (Name "mul") [FreeOffset 0, Concrete 2]) @?= Nothing,
+      testCase "comparing a symbolic address → Nothing" $
+        -- Its run-time value is unknown, so no comparison can be decided
+        runComptime (evalYulOp (Name "eq") [FreeOffset 0, Concrete 0]) @?= Nothing,
+      testCase "scratch space above the free pointer: store then load" $
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yAssign "p" (yCall "mload" [yNum 64]),
+                yExp "mstore" [yCall "add" [yIdent "p", yNum 32], yNum 7],
+                yAssign "r" (yCall "mload" [yCall "add" [yIdent "p", yNum 32]])
+              ]
+          )
+          @?= Just (Map.fromList [(Name "p", FreeOffset 0), (Name "r", Concrete 7)]),
+      testCase "scratch space above the free pointer: keccak256 over it" $
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yAssign "p" (yCall "mload" [yNum 64]),
+                yExp "mstore" [yIdent "p", yNum 42],
+                yAssign "h" (yCall "keccak256" [yIdent "p", yNum 32])
+              ]
+          )
+          @?= Just (Map.fromList [(Name "p", FreeOffset 0), (Name "h", Concrete keccak42)]),
+      testCase "a symbolic address is never stored as a value" $
+        -- Stored, it would be read back as a plain word, losing its unknown base
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yAssign "p" (yCall "mload" [yNum 64]),
+                yExp "mstore" [yIdent "p", yIdent "p"]
+              ]
+          )
+          @?= Nothing,
+      testCase "moving the free memory pointer aborts the evaluation" $
+        -- FreeOffset assumes the pointer stays put; reallocation is not modelled
+        runComptime (evalYulBlock Map.empty [yExp "mstore" [yNum 64, yNum 0x80]])
+          @?= Nothing,
+      testCase "a write merely overlapping the pointer slot also aborts" $
+        runComptime (evalYulBlock Map.empty [yExp "mstore" [yNum 33, yNum 1]])
+          @?= Nothing,
+      testCase "mstore8 into the pointer slot aborts too" $
+        runComptime (evalYulBlock Map.empty [yExp "mstore8" [yNum 64, yNum 1]])
+          @?= Nothing,
+      testCase "a write below the pointer slot is unaffected" $
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yExp "mstore" [yNum 32, yNum 1],
+                yAssign "r" (yCall "mload" [yNum 32])
+              ]
+          )
+          @?= Just (st [("r", 1)]),
+      testCase "mixing absolute and free-relative memory → Nothing" $
+        -- The two may alias at run time, so one evaluation may use only one region
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yExp "mstore" [yNum 0, yNum 1],
+                yAssign "p" (yCall "mload" [yNum 64]),
+                yExp "mstore" [yIdent "p", yNum 2]
+              ]
+          )
+          @?= Nothing,
+      testCase "reading absolute memory after writing free-relative → Nothing" $
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yAssign "p" (yCall "mload" [yNum 64]),
+                yExp "mstore" [yIdent "p", yNum 1],
+                yAssign "r" (yCall "mload" [yNum 0])
+              ]
+          )
+          @?= Nothing,
+      testCase "the memory helpers keep the two regions apart" $
+        mloadWord (at 0) (mstoreBytes (above 0) 42 Map.empty) @?= Nothing
+    ]
+
+-----------------------------------------------------------------------
+-- keccak256 over comptime-known memory
+-----------------------------------------------------------------------
+
+-- keccak256 of the 32-byte big-endian encoding of 42
+keccak42 :: Integer
+keccak42 = 0xbeced09521047d05b8960b7e7bcc1d1292cf3e4b2a6b63f48335cbde5f7545d2
+
+-- keccak256 of the empty byte string
+keccakEmpty :: Integer
+keccakEmpty = 0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470
+
+keccakEvalTests :: TestTree
+keccakEvalTests =
+  testGroup
+    "keccak256 in Yul evaluator"
+    [ testCase "mloadRange: reads a written byte range" $
+        mloadRange (at 0) 2 (Map.fromList [(at 0, 0xde), (at 1, 0xad)]) @?= Just (BS.pack [0xde, 0xad]),
+      testCase "mloadRange: zero length is the empty string" $
+        mloadRange (at 100) 0 Map.empty @?= Just BS.empty,
+      testCase "mloadRange: any missing byte yields Nothing" $
+        mloadRange (at 0) 2 (Map.fromList [(at 0, 0xde)]) @?= Nothing,
+      testCase "mstore then keccak256 over the stored word" $
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yExp "mstore" [yNum 0, yNum 42],
+                yAssign "h" (yCall "keccak256" [yNum 0, yNum 32])
+              ]
+          )
+          @?= Just (st [("h", keccak42)]),
+      testCase "keccak256 over a zero-length range needs no memory" $
+        runComptime (evalYulBlock Map.empty [yAssign "h" (yCall "keccak256" [yNum 0, yNum 0])])
+          @?= Just (st [("h", keccakEmpty)]),
+      testCase "keccak256 over unwritten memory → Nothing" $
+        runComptime (evalYulBlock Map.empty [yAssign "h" (yCall "keccak256" [yNum 0, yNum 32])])
+          @?= Nothing,
+      testCase "keccak256 over a partially written range → Nothing" $
+        -- 32 bytes written at 0, but the hash covers 64 bytes
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yExp "mstore" [yNum 0, yNum 42],
+                yAssign "h" (yCall "keccak256" [yNum 0, yNum 64])
+              ]
+          )
+          @?= Nothing,
+      testCase "keccak256 with unknown address → Nothing" $
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [yAssign "h" (yCall "keccak256" [yIdent "p", yNum 32])]
+          )
+          @?= Nothing,
+      testCase "keccak256 with unknown length → Nothing" $
+        runComptime
+          ( evalYulBlock
+              Map.empty
+              [ yExp "mstore" [yNum 0, yNum 42],
+                yAssign "h" (yCall "keccak256" [yNum 0, yIdent "n"])
+              ]
+          )
+          @?= Nothing,
+      testCase "keccak256 in non-comptime mode → Nothing" $
+        runPure (evalYulBlock Map.empty [yAssign "h" (yCall "keccak256" [yNum 0, yNum 0])])
+          @?= Nothing
+    ]
+
+-----------------------------------------------------------------------
+-- Whole-unit folding of comptime hashing (evalCompUnit)
+-----------------------------------------------------------------------
+
+-- These build the MAST that `mstore(0, x); keccak256(0, 32)` specialises to,
+-- and check that partial evaluation replaces the call with the hash literal.
+-- The .solc-level comptime tests only assert that compilation succeeds, so
+-- they cannot tell folding apart from a call left in the output.
+
+wordTy :: MastTy
+wordTy = MastTyCon (Name "word") []
+
+unitTy :: MastTy
+unitTy = MastTyCon (Name "unit") []
+
+funId :: String -> [MastTy] -> MastTy -> MastId
+funId n argTys ret = MastId (Name n) (foldr MastArrow ret argTys)
+
+varId :: String -> MastId
+varId n = MastId (Name n) wordTy
+
+param :: String -> MastParam
+param n = MastParam (Name n) False wordTy
+
+-- function mstore(a, b) -> () { assembly { mstore(a, b) } }
+mstoreDef :: MastFunDef
+mstoreDef =
+  MastFunDef (Name "mstore") [param "a", param "b"] False unitTy $
+    [MastAsm [yExp "mstore" [yIdent "a", yIdent "b"]]]
+
+-- function keccak256(a, b) -> word { let res; assembly { res := keccak256(a, b) } return res; }
+keccakDef :: MastFunDef
+keccakDef =
+  MastFunDef (Name "keccak256") [param "a", param "b"] False wordTy $
+    [ MastLet False (varId "res") (Just wordTy) Nothing,
+      MastAsm [yAssign "res" (yCall "keccak256" [yIdent "a", yIdent "b"])],
+      MastReturn (MastVar (varId "res"))
+    ]
+
+-- function hashOne(x) -> <retComptime> word { mstore(0, x); return keccak256(0, 32); }
+hashOneDef :: Bool -> MastFunDef
+hashOneDef retComptime =
+  MastFunDef (Name "hashOne") [param "x"] retComptime wordTy $
+    [ MastStmtExp (MastCall (funId "mstore" [wordTy, wordTy] unitTy) [intLit 0, MastVar (varId "x")]),
+      MastReturn (MastCall (funId "keccak256" [wordTy, wordTy] wordTy) [intLit 0, intLit 32])
+    ]
+
+-- function get_free_memory() -> word { let fp; assembly { fp := mload(0x40) } return fp; }
+getFreeMemoryDef :: MastFunDef
+getFreeMemoryDef =
+  MastFunDef (Name "get_free_memory") [] False wordTy $
+    [ MastLet False (varId "fp") (Just wordTy) Nothing,
+      MastAsm [yAssign "fp" (yCall "mload" [yNum 64])],
+      MastReturn (MastVar (varId "fp"))
+    ]
+
+getFreeMemoryCall :: MastExp
+getFreeMemoryCall = MastCall (funId "get_free_memory" [] wordTy) []
+
+-- function hashScratch(x) -> comptime word {
+--   let p = get_free_memory(); mstore(p, x); return keccak256(p, 32);
+-- }
+hashScratchDef :: MastFunDef
+hashScratchDef =
+  MastFunDef (Name "hashScratch") [param "x"] True wordTy $
+    [ MastLet False (varId "p") (Just wordTy) (Just getFreeMemoryCall),
+      MastStmtExp
+        ( MastCall
+            (funId "mstore" [wordTy, wordTy] unitTy)
+            [MastVar (varId "p"), MastVar (varId "x")]
+        ),
+      MastReturn
+        ( MastCall
+            (funId "keccak256" [wordTy, wordTy] wordTy)
+            [MastVar (varId "p"), intLit 32]
+        )
+    ]
+
+-- The body of `main` after partially evaluating a unit made of the given
+-- helper definitions plus a `main` with the given body.
+foldedMainWith :: [MastFunDef] -> [MastStmt] -> [MastStmt]
+foldedMainWith defs mainBody =
+  concat [mastFunBody fd | MastCFunDecl fd <- decls', mastFunName fd == Name "main"]
+  where
+    mainDef = MastFunDef (Name "main") [] False wordTy mainBody
+    unit =
+      MastCompUnit [] $
+        [ MastTContr . MastContract (Name "C") $
+            map MastCFunDecl (defs ++ [mainDef])
+        ]
+    (unit', _) = evalCompUnit defaultFuel unit
+    decls' = concat [mastContrDecls c | MastTContr c <- mastTopDecls unit']
+
+-- The body of `main` for a unit whose `hashOne` has the given comptime-return
+-- flag and whose `main` has the given body.
+foldedMain :: Bool -> [MastStmt] -> [MastStmt]
+foldedMain retComptime = foldedMainWith [mstoreDef, keccakDef, hashOneDef retComptime]
+
+comptimeFoldingTests :: TestTree
+comptimeFoldingTests =
+  testGroup
+    "evalCompUnit: comptime hashing"
+    [ testCase "comptime let folds a memory hash to its literal" $
+        -- let r : comptime word = hashOne(42);  ==>  the let disappears, r is known
+        foldedMain
+          False
+          [ MastLet True (varId "r") (Just wordTy) (Just (MastCall (funId "hashOne" [wordTy] wordTy) [intLit 42])),
+            MastReturn (MastVar (varId "r"))
+          ]
+          @?= [MastReturn (intLit keccak42)],
+      testCase "'-> comptime' function folds at its call site without a comptime let" $
+        -- return hashOne(42);  where hashOne is annotated '-> comptime word'
+        foldedMain True [MastReturn (MastCall (funId "hashOne" [wordTy] wordTy) [intLit 42])]
+          @?= [MastReturn (intLit keccak42)],
+      testCase "without '-> comptime' and without a comptime let, the call is left alone" $
+        -- Memory ops must not run outside comptime context: hashing runtime
+        -- memory at compile time would be unsound.
+        foldedMain False [MastReturn (MastCall (funId "hashOne" [wordTy] wordTy) [intLit 42])]
+          @?= [MastReturn (MastCall (funId "hashOne" [wordTy] wordTy) [intLit 42])],
+      testCase "scratch space above the free memory pointer folds" $
+        -- The address is unknown, but the offsets from it are enough to lay out
+        -- and hash the bytes.
+        foldedMainWith
+          [mstoreDef, keccakDef, getFreeMemoryDef, hashScratchDef]
+          [MastReturn (MastCall (funId "hashScratch" [wordTy] wordTy) [intLit 42])]
+          @?= [MastReturn (intLit keccak42)],
+      testCase "the free memory pointer itself is not a comptime value" $
+        -- Only offsets from the base are tracked; the base has no literal form
+        foldedMainWith
+          [getFreeMemoryDef]
+          [ MastLet True (varId "p") (Just wordTy) (Just getFreeMemoryCall),
+            MastReturn (MastVar (varId "p"))
+          ]
+          @?= [ MastLet True (varId "p") (Just wordTy) (Just getFreeMemoryCall),
+                MastReturn (MastVar (varId "p"))
+              ]
+    ]
+
 -----------------------------------------------------------------------
 -- asmIsInterpretable
 -----------------------------------------------------------------------
@@ -440,6 +770,9 @@ asmIsInterpretableTests =
       testCase "mload in assignment → True" $
         asmIsInterpretable [yAssign "r" (yCall "mload" [yNum 0])]
           @?= True,
+      testCase "keccak256 in assignment → True" $
+        asmIsInterpretable [yAssign "r" (yCall "keccak256" [yIdent "a", yIdent "b"])]
+          @?= True,
       testCase "sload-assign → False" $
         asmIsInterpretable [yAssign "rw" (yCall "sload" [yNum 0])]
           @?= False,
diff --git a/test/examples/comptime/ct_comptime_unfolded.solc b/test/examples/comptime/ct_comptime_unfolded.solc
new file mode 100644
index 000000000..2040609d3
--- /dev/null
+++ b/test/examples/comptime/ct_comptime_unfolded.solc
@@ -0,0 +1,17 @@
+/* Negative: a '-> comptime' function called with known arguments must actually
+   fold.  Here it reads memory it never wrote, so the partial evaluator cannot
+   produce a value and the call survives — the annotation promised a
+   compile-time result that the compiler cannot deliver.
+*/
+import std.{*};
+import std.opcodes.{mload};
+
+function readScratch(a : word) -> comptime word {
+    return mload(a);
+}
+
+contract ComptimeUnfolded {
+  function main() -> word {
+    return readScratch(0);
+  }
+}
diff --git a/test/examples/comptime/ct_keccak_domain.solc b/test/examples/comptime/ct_keccak_domain.solc
new file mode 100644
index 000000000..6e82b9721
--- /dev/null
+++ b/test/examples/comptime/ct_keccak_domain.solc
@@ -0,0 +1,49 @@
+/* Positive: the EIP-712 domain separator is a compile-time constant.
+
+   Five words are laid out contiguously above the free memory pointer and
+   hashed.  The pointer's run-time value is unknown, but the evaluator tracks
+   the scratch addresses symbolically as offsets from it, which is enough to
+   know which bytes the hash covers.
+
+   The function is annotated '-> comptime', which lets the partial evaluator
+   run the memory operations at its call sites even though there is no
+   'comptime' let: with literal arguments the whole call folds to the domain
+   separator literal.
+*/
+import std.{*};
+import std.opcodes.{mstore, keccak256};
+
+function eip712DomainSeparator(
+    nameHash: bytes32,
+    versionHash: bytes32,
+    chainId: uint256,
+    verifyingContract: address
+) -> comptime bytes32 {
+    let typeHash = keccakLit("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)");
+    // Borrow the area above the free memory pointer as scratch (as `ecrecover`
+    // does): the preimage is consumed immediately by keccak256 and never needs
+    // to persist, so there is no need to bump the free pointer.
+    let ptr = get_free_memory();
+    mstore(ptr,       typeHash);
+    mstore(ptr + 32,  Typedef.rep(nameHash));
+    mstore(ptr + 64,  Typedef.rep(versionHash));
+    mstore(ptr + 96,  Typedef.rep(chainId));
+    mstore(ptr + 128, Typedef.rep(verifyingContract));
+    return bytes32(keccak256(ptr, 160));
+}
+
+// Domain separator for name "Ether Mail", version "1", chainId 1 and the
+// verifying contract from the EIP-712 specification example.  The expected
+// value is 0xf2cee375fa42b42143804025fc449deafd50cc031ca257e0b194a650a912090f.
+function mailDomainSeparator() -> bytes32 {
+    return eip712DomainSeparator(
+        bytes32(keccakLit("Ether Mail")),
+        bytes32(keccakLit("1")),
+        uint256(1),
+        address(0xCcCCccccCCCCcCCCCCCcCcCccCcCCCcCcccccccC)
+    );
+}
+
+contract EIP712Domain {
+  function main() -> bytes32 { mailDomainSeparator() }
+}
diff --git a/test/examples/comptime/ct_keccak_mem.solc b/test/examples/comptime/ct_keccak_mem.solc
new file mode 100644
index 000000000..d746d6381
--- /dev/null
+++ b/test/examples/comptime/ct_keccak_mem.solc
@@ -0,0 +1,18 @@
+/* Positive: keccak256 over a memory range written in the same comptime
+   evaluation folds to a literal.  Memory ops only run in comptime context,
+   so the hash is computed over bytes this evaluation wrote itself.
+*/
+import std.{*};
+import std.opcodes.{mstore, keccak256};
+
+function hashOne(x : word) -> word {
+    mstore(0, x);
+    return keccak256(0, 32);
+}
+
+contract ComptimeKeccakMem {
+  function main() -> word {
+    let res : comptime word = hashOne(42);
+    return res;
+  }
+}