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;
+  }
+}