diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -34,7 +34,7 @@
 
 ```bash
 cabal update
-cabal install --overwrite-policy=always phino-0.0.145
+cabal install --overwrite-policy=always phino-0.0.148
 phino --version
 ```
 
@@ -875,11 +875,11 @@
 run fills the protocol with lines tens of thousands of characters long. The
 `--abridged` option shortens every term the protocol writes, in the text and
 the XML alike: a formation longer than sixty-four characters keeps its `φ`,
-`Δ` and `λ` bindings and folds the rest into a count, and a byte string longer
-than eight bytes keeps its first two bytes and its last two, with the count of
-the bytes cut out between them. The width is a value of the option,
-`--abridged=120`, for a run that can read longer lines. The result the run
-prints stays whole, and the option is refused without `--protocol`:
+`Δ` and `λ` bindings and folds the rest into a count. The width is a value of
+the option, `--abridged=120`, for a run that can read longer lines. The result
+the run prints stays whole, and the option is refused without `--protocol`.
+Every byte string the protocol writes stays whole too, since a reader may need
+the data a firing came down to:
 
 <!-- markdownlint-disable MD013 -->
 
@@ -895,6 +895,23 @@
 ⟧
 $ phino dataize --locator=Q.t --protocol=wide.txt --abridged --quiet \
     --sweet --hide-rho wide.phi
+$ cat wide.txt
+𝔻(Φ.t)
+  formation(⟦ φ ↦ 48-65-6C-6C-6F-2C-20-77-6F-72-6C-64:Δ, +3 ⟧)  # 𝔻(Φ.t)
+```
+
+<!-- markdownlint-enable MD013 -->
+
+The `--abridged-data` option cuts the data too: a byte string longer than eight
+bytes keeps its first two bytes and its last two, with the count of the bytes
+cut out between them. A formation folded into a count loses its data either
+way, and the option is refused without `--abridged`:
+
+<!-- markdownlint-disable MD013 -->
+
+```bash
+$ phino dataize --locator=Q.t --protocol=wide.txt --abridged \
+    --abridged-data --quiet --sweet --hide-rho wide.phi
 $ cat wide.txt
 𝔻(Φ.t)
   formation(⟦ φ ↦ 48-65-..(8b)..-6C-64:Δ, +3 ⟧)  # 𝔻(Φ.t)
diff --git a/benchmark/Main.hs b/benchmark/Main.hs
--- a/benchmark/Main.hs
+++ b/benchmark/Main.hs
@@ -8,6 +8,7 @@
 import Compiled (compiled)
 import Control.Exception (evaluate)
 import Control.Monad (replicateM, replicateM_)
+import Data.IORef (IORef, newIORef)
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Map.Strict as Map
 import Data.Maybe (fromMaybe)
@@ -22,7 +23,7 @@
 import Lining (LineFormat (MULTILINE, SINGLELINE))
 import Margin (defaultMargin)
 import Merge (merge)
-import Morph (Memo, ReduceContext (ReduceContext), Steps (Steps), memoized, morph)
+import Morph (Memo, ReduceContext (ReduceContext), Steps (Steps), emptyState, memoized, morph)
 import Must (Must (MtDisabled))
 import Parser (parseExpressionThrows)
 import Printer (printExpression')
@@ -60,8 +61,8 @@
     Nothing
     dontSaveStep
 
-symbolicCtx :: Acyclic -> Maybe Memo -> Lambdas -> Expression -> ReduceContext
-symbolicCtx acyclic memo lambdas locator =
+symbolicCtx :: Acyclic -> Maybe Memo -> IORef Int -> Lambdas -> Expression -> ReduceContext
+symbolicCtx acyclic memo minted lambdas locator =
   ReduceContext
     locator
     locator
@@ -70,6 +71,7 @@
     25
     (Steps 1000 0)
     Nothing
+    minted
     Nothing
     memo
     1
@@ -192,5 +194,8 @@
     symbolic acyclic universe lambdas locator = do
       seedTaus universe
       memo <- memoized (Just acyclic)
-      (answer, _, _) <- morph universe (started universe) (symbolicCtx acyclic memo lambdas locator)
+      minted <- newIORef 0
+      let ctx = symbolicCtx acyclic memo minted lambdas locator
+      started universe ctx
+      (answer, _, _) <- morph universe emptyState ctx
       pure (hashExpression answer)
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.148
+version: 0.0.149
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/src/Abridge.hs b/src/Abridge.hs
--- a/src/Abridge.hs
+++ b/src/Abridge.hs
@@ -10,8 +10,8 @@
 import Lining (toSingleLine)
 import Render (render)
 
-abridged :: Int -> EXPRESSION -> EXPRESSION
-abridged width = goExpr
+abridged :: Bool -> Int -> EXPRESSION -> EXPRESSION
+abridged cut width = goExpr
   where
     goExpr :: EXPRESSION -> EXPRESSION
     goExpr expr@EX_FORMATION{..}
@@ -68,7 +68,7 @@
     goAppArgs AAS_EMPTY = AAS_EMPTY
     goBytes :: BYTES -> BYTES
     goBytes (BT_MANY bts)
-      | length bts > 8 = BT_CUT (take 2 bts) (length bts - 4) (drop (length bts - 2) bts)
+      | cut && length bts > 8 = BT_CUT (take 2 bts) (length bts - 4) (drop (length bts - 2) bts)
     goBytes bts = bts
     short :: EXPRESSION -> Bool
     short expr = T.length (render (toSingleLine expr)) <= width
diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs
--- a/src/CLI/Helpers.hs
+++ b/src/CLI/Helpers.hs
@@ -23,7 +23,7 @@
 import qualified Data.Map.Strict as M
 import Data.Maybe
 import qualified Data.Text as T
-import Deps (Evaluation (EvRun), Judgment, SaveEvalFunc, SaveStepFunc, State (..), dontSaveEval, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, progressed, saveEval, saveEvalXml, saveStep)
+import Deps (Evaluation (EvRun), Judgment, SaveEvalFunc, SaveStepFunc, dontSaveEval, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, progressed, saveEval, saveEvalXml, saveStep)
 import Encoding
 import Engine (Engine, fresh, yaml)
 import Files (ensuredFile, overwrite)
@@ -35,7 +35,7 @@
 import Lining (LineFormat (SINGLELINE))
 import Locator (locatedExpression)
 import Logger
-import Morph (ReduceContext, emptyState, insideUniverse)
+import Morph (ReduceContext (..), insideUniverse)
 import Parser (parseExpressionThrows)
 import qualified Printer as P
 import qualified Random as R
@@ -63,8 +63,8 @@
         | _outputFormat == LATEX = "tex"
         | otherwise = show _outputFormat
       render expr = do
-        shown <- F.include' expr included
-        printInFormat ctx ((if _canonize then canonizeExpr else id) (F.exclude' shown excluded))
+        shown <- F.include' expr included >>= (`F.exclude'` excluded)
+        printInFormat ctx ((if _canonize then canonizeExpr else id) shown)
       save :: SaveStepFunc
       save expr = do
         step <- atomicModifyIORef' counter (\value -> (value + 1, value + 1))
@@ -118,8 +118,8 @@
   logDebug (printf "The option '--symbolic' is specified, reading the λ functions from '%s'" file)
   ensuredFile file >>= readLambdas
 
-started :: Expression -> State
-started expr = emptyState{_minted = taken expr}
+started :: Expression -> ReduceContext -> IO ()
+started expr ctx = writeIORef ctx._minted (taken expr)
 
 heading :: SaveEvalFunc -> PrintContext -> Judgment -> Expression -> IO ()
 heading record ctx judgment locator =
@@ -130,7 +130,7 @@
   pure (P.printExpressionWith shaped expr (_sugar, UNICODE, SINGLELINE, _margin))
   where
     shaped :: SugarType -> EXPRESSION -> EXPRESSION
-    shaped sugar = maybe id abridged _abridged . hidden ctx sugar
+    shaped sugar = maybe id (abridged _abridgedData) _abridged . hidden ctx sugar
 
 salted :: PrintContext -> Expression -> IO String
 salted ctx = flattened ctx{_sugar = SALTY}
diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs
--- a/src/CLI/Parsers.hs
+++ b/src/CLI/Parsers.hs
@@ -290,13 +290,21 @@
         ( long "abridged"
             <> help
               "Shorten every 𝜑-expression written to the --protocol file: a formation longer than the width \
-              \keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', and a byte string \
-              \longer than eight bytes keeps its first two bytes and its last two with the count of the bytes \
-              \between them, as '00-00-..(45b)..-FF-EE'; the width is 64 characters unless given as --abridged=WIDTH"
+              \keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', while every byte string \
+              \it writes stays whole; the width is 64 characters unless given as --abridged=WIDTH"
         )
         <|> option auto (long "abridged" <> metavar "WIDTH" <> internal)
     )
 
+optAbridgedData :: Parser Bool
+optAbridgedData =
+  switch
+    ( long "abridged-data"
+        <> help
+          "Cut every byte string longer than eight bytes that the --abridged protocol writes to its first \
+          \two bytes and its last two with the count of the bytes between them, as '00-00-..(45b)..-FF-EE'"
+    )
+
 optShuffle :: Parser Bool
 optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying")
 
@@ -408,6 +416,7 @@
             <*> optStepsDir
             <*> optProtocol
             <*> optAbridged
+            <*> optAbridgedData
             <*> optSymbolic
             <*> argInputFile
         )
@@ -457,6 +466,7 @@
             <*> optStepsDir
             <*> optProtocol
             <*> optAbridged
+            <*> optAbridgedData
             <*> optSymbolic
             <*> argInputFile
         )
diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs
--- a/src/CLI/Runners.hs
+++ b/src/CLI/Runners.hs
@@ -16,6 +16,7 @@
 import Control.Exception
 import Control.Monad (unless, when)
 import Data.Foldable (traverse_)
+import Data.IORef (newIORef)
 import Data.List (intercalate)
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Map.Strict as Map
@@ -76,7 +77,7 @@
   save <- saveStepFunc _stepsDir printCtx included excluded
   let steps = map (stepOf linked) rules
   (rewrittens, exceeded) <- rewrite expr steps (RewriteContext loc _maxDepth _maxCycles _depthSensitive Nothing (building linked) linked._normal (every steps) _must _breakpoint save)
-  rewrittens' <- exclude <$> include (if _sequence then NE.toList rewrittens else [NE.last rewrittens])
+  rewrittens' <- include (if _sequence then NE.toList rewrittens else [NE.last rewrittens]) >>= exclude
   logDebug (printf "Printing rewritten 𝜑-expression as %s" (show _outputFormat))
   exprs <- printRewrittens printCtx (rewrittens', exceeded)
   output _targetFile exprs
@@ -138,6 +139,7 @@
         _sugarType
         _hideRho
         Nothing
+        False
         _flat
         _margin
         xmirCtx
@@ -173,6 +175,7 @@
       include = (`F.include` included)
   save <- saveStepFunc _stepsDir printCtx included excluded
   tally <- tallied _maxFirings
+  minted <- newIORef 0
   memo <- memoized _acyclic
   linked <- engine
   (outcome, chain, _) <-
@@ -180,13 +183,14 @@
       _protocol
       printCtx
       ( \record -> do
-          let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally deadline memo 1 _depthSensitive _shuffle _partial False 1 _acyclic Dataization [] Map.empty lambdas (building linked) reduction evaluation fired save record linked
+          let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 _depthSensitive _shuffle _partial False 1 _acyclic Dataization [] Map.empty lambdas (building linked) reduction evaluation fired save record linked
           (universe, aiming) <- aimed _inside expr ctx
           heading record printCtx Dataization aiming._locator
-          dataize universe (started universe) aiming
+          started universe aiming
+          dataize universe emptyState aiming
       )
-  when _sequence (include chain >>= \shown -> printRewrittens printCtx (exclude shown, False) >>= putStrLn)
-  unless _quiet (printOutcome printCtx (\residue -> (`F.exclude'` excluded) <$> F.include' residue included) outcome >>= putStrLn)
+  when _sequence (include chain >>= exclude >>= \shown -> printRewrittens printCtx (shown, False) >>= putStrLn)
+  unless _quiet (printOutcome printCtx (\residue -> F.include' residue included >>= (`F.exclude'` excluded)) outcome >>= putStrLn)
   where
     printOutcome :: PrintContext -> (Expression -> IO Expression) -> Outcome -> IO String
     printOutcome _ _ (Dataized bytes) = pure (P.printBytes bytes)
@@ -205,6 +209,7 @@
       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus
       when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")
       when (isJust _abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged")
+      when (_abridgedData && isNothing _abridged) (invalidCLIArguments "The option --abridged-data requires --abridged, since only an abridged protocol cuts its data")
       when
         (isJust _inside && _locator /= "Q")
         (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")
@@ -214,6 +219,7 @@
         _sugarType
         _hideRho
         _abridged
+        _abridgedData
         _flat
         _margin
         (XmirContext _omitListing _omitComments _hideRho listing atoms)
@@ -252,6 +258,7 @@
       include = (`F.include` included)
   save <- saveStepFunc _stepsDir printCtx included excluded
   tally <- tallied _maxFirings
+  minted <- newIORef 0
   memo <- memoized _acyclic
   linked <- engine
   (morphed, chain, _) <-
@@ -259,19 +266,20 @@
       _protocol
       printCtx
       ( \record -> do
-          let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally deadline memo 1 _depthSensitive _shuffle _partial _deep _jobs _acyclic Morphing [] Map.empty lambdas (building linked) reduction evaluation fired save record linked
+          let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 _depthSensitive _shuffle _partial _deep _jobs _acyclic Morphing [] Map.empty lambdas (building linked) reduction evaluation fired save record linked
           (universe, aiming) <- aimed _inside expr ctx
           heading record printCtx Morphing aiming._locator
-          morph universe (started universe) aiming
+          started universe aiming
+          morph universe emptyState aiming
       )
   printed <-
     if _quiet
       then pure Nothing
       else do
-        answer <- (`F.exclude'` excluded) <$> F.include' (if foc == ExRoot then morphed else maybe morphed fst (lastMaybe chain)) included
+        answer <- F.include' (if foc == ExRoot then morphed else maybe morphed fst (lastMaybe chain)) included >>= (`F.exclude'` excluded)
         validateXmirTopLevel _outputFormat answer
         Just <$> printAnswer printCtx answer
-  when _sequence (include chain >>= \shown -> printRewrittens printCtx (exclude shown, False) >>= putStrLn)
+  when _sequence (include chain >>= exclude >>= \shown -> printRewrittens printCtx (shown, False) >>= putStrLn)
   mapM_ putStrLn printed
   where
     lastMaybe :: [a] -> Maybe a
@@ -287,6 +295,7 @@
       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus
       when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")
       when (isJust _abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged")
+      when (_abridgedData && isNothing _abridged) (invalidCLIArguments "The option --abridged-data requires --abridged, since only an abridged protocol cuts its data")
       when (_jobs > 1 && not _deep) (invalidCLIArguments "The option --jobs requires --deep, since only the deep walk runs on several workers")
       when
         (isJust _inside && _locator /= "Q")
@@ -297,6 +306,7 @@
         _sugarType
         _hideRho
         _abridged
+        _abridgedData
         _flat
         _margin
         (XmirContext _omitListing _omitComments _hideRho listing atoms)
@@ -363,6 +373,7 @@
         _sugarType
         False
         Nothing
+        False
         _flat
         _margin
         xmirCtx
diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs
--- a/src/CLI/Types.hs
+++ b/src/CLI/Types.hs
@@ -20,6 +20,7 @@
   { _sugar :: SugarType
   , _hideRho :: Bool
   , _abridged :: Maybe Int
+  , _abridgedData :: Bool
   , _line :: LineFormat
   , _margin :: Int
   , _xmirCtx :: XmirContext
@@ -126,6 +127,7 @@
   , _stepsDir :: Maybe FilePath
   , _protocol :: Maybe FilePath
   , _abridged :: Maybe Int
+  , _abridgedData :: Bool
   , _symbolic :: Maybe FilePath
   , _inputFile :: Maybe FilePath
   }
@@ -172,6 +174,7 @@
   , _stepsDir :: Maybe FilePath
   , _protocol :: Maybe FilePath
   , _abridged :: Maybe Int
+  , _abridgedData :: Bool
   , _symbolic :: Maybe FilePath
   , _inputFile :: Maybe FilePath
   }
diff --git a/src/Deps.hs b/src/Deps.hs
--- a/src/Deps.hs
+++ b/src/Deps.hs
@@ -35,8 +35,7 @@
 type BuildTermMethod = [ExtraArgument] -> Subst -> IO Term
 
 data State = State
-  { _minted :: Int
-  , _manufactured :: Maybe Int
+  { _manufactured :: Maybe Int
   , _stuck :: Maybe T.Text
   }
 
diff --git a/src/Evaluate.hs b/src/Evaluate.hs
--- a/src/Evaluate.hs
+++ b/src/Evaluate.hs
@@ -11,6 +11,7 @@
 import Builder (buildExpressionThrows)
 import Control.Exception (catch, throwIO, try)
 import Control.Monad (foldM, unless)
+import Data.IORef (readIORef, writeIORef)
 import Data.List (partition)
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.Maybe (fromMaybe, isNothing, listToMaybe)
@@ -85,9 +86,9 @@
     worked :: ReduceContext -> Lambda -> Firing -> Subst -> State -> IO (Answer, State)
     worked ctx entry firing@(Firing _ operands _) bound state' = do
       rewrote <- foldM (reshaped ctx) bound entry._rewritten
-      (bound', stood) <- foldM (masked ctx) (rewrote, state') entry._symbolized
-      (bound'', forked) <- foldM (paired ctx (listToMaybe operands)) (bound', stood) entry._paired
-      (answer, state'') <- answered ctx entry operands bound'' forked
+      stood <- foldM (masked ctx) rewrote entry._symbolized
+      forked <- foldM (paired ctx (listToMaybe operands)) stood entry._paired
+      (answer, state'') <- answered ctx entry operands forked state'
       remember caller._memo firing answer
       pure (answer, state'')
     shown :: Int -> Answer -> IO ()
@@ -144,19 +145,19 @@
       shaped <- rewritten rules (RuleContext ctx._buildTerm Nothing ctx._engine._normal) term
       ctx._saveEval (EvSymbolize ctx._nesting meta._spelling (ExMeta source._name) shaped)
       bind meta (MvExpression shaped) bound
-    masked :: ReduceContext -> (Subst, State) -> (Meta, Expression) -> IO (Subst, State)
-    masked ctx (bound, state') (meta, term) = do
+    masked :: ReduceContext -> Subst -> (Meta, Expression) -> IO Subst
+    masked ctx bound (meta, term) = do
       reduced <- buildExpressionThrows term bound
-      let (stood, known, spent) = symbolized reduced state'._minted
+      (stood, known, spent) <- symbolized reduced <$> readIORef ctx._minted
+      writeIORef ctx._minted spent
       mapM_ (ctx._saveEval . fact) known
       ctx._saveEval (EvSymbolize ctx._nesting meta._spelling term stood)
-      bound' <- bind meta (MvExpression stood) bound
-      pure (bound', state'{_minted = spent})
+      bind meta (MvExpression stood) bound
       where
         fact :: (Int, Bytes) -> Evaluation
         fact (fresh, bytes) = EvKnown ctx._nesting fresh bytes
-    paired :: ReduceContext -> Maybe (Either Int Bytes) -> (Subst, State) -> (Meta, (Meta, Meta)) -> IO (Subst, State)
-    paired ctx condition (bound, state') (meta, (left, right)) = do
+    paired :: ReduceContext -> Maybe (Either Int Bytes) -> Subst -> (Meta, (Meta, Meta)) -> IO Subst
+    paired ctx condition bound (meta, (left, right)) = do
       one <- branch left
       two <- branch right
       case (one, two) of
@@ -165,32 +166,34 @@
         (_, ExTermination) -> terminating "right" right one
         _ -> both one two
       where
-        both :: Expression -> Expression -> IO (Subst, State)
-        both one two = case joined one two state'._minted of
-          Nothing -> throwIO (Stuck func)
-          Just (term, made, spent) -> do
-            mapM_ (ctx._saveEval . fact) made
-            ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
-            bound' <- bind meta (MvExpression term) bound
-            pure (bound', state'{_minted = spent})
-        terminating :: T.Text -> Meta -> Expression -> IO (Subst, State)
+        both :: Expression -> Expression -> IO Subst
+        both one two = do
+          outcome <- joined one two <$> readIORef ctx._minted
+          case outcome of
+            Nothing -> throwIO (Stuck func)
+            Just (term, made, spent) -> do
+              writeIORef ctx._minted spent
+              mapM_ (ctx._saveEval . fact) made
+              ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
+              bind meta (MvExpression term) bound
+        terminating :: T.Text -> Meta -> Expression -> IO Subst
         terminating side raised term = do
           ctx._saveEval (EvTerminate ctx._nesting condition side raised._spelling)
           ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
-          bound' <- bind meta (MvExpression term) bound
-          pure (bound', state')
+          bind meta (MvExpression term) bound
         branch :: Meta -> IO Expression
         branch named = buildExpressionThrows (ExMeta named._name) bound
         fact :: (Int, (Int, Int)) -> Evaluation
         fact (fresh, pair) = EvJoined ctx._nesting fresh pair
     answered :: ReduceContext -> Lambda -> [Either Int Bytes] -> Subst -> State -> IO (Answer, State)
     answered ctx entry operands bound state' = do
-      let (fresh, spent) = minted entry._answer state'._minted
+      (fresh, spent) <- minted entry._answer <$> readIORef ctx._minted
+      writeIORef ctx._minted spent
       mapM_ (\idx -> ctx._saveEval (EvMinted ctx._nesting idx operands)) [idx | (_, FnSymbol idx) <- fresh]
       symbolic <- foldM mint bound fresh
       built <- buildExpressionThrows entry._answer symbolic
       ctx._saveEval (EvBuilt ctx._nesting built)
-      (normal, state'') <- settled built univ state'{_minted = spent} ctx
+      (normal, state'') <- settled built univ state' ctx
       ctx._saveEval (EvAnswer ctx._nesting normal)
       pure ((built, normal), state'')
     mint :: Subst -> (Slot, Function) -> IO Subst
diff --git a/src/Filter.hs b/src/Filter.hs
--- a/src/Filter.hs
+++ b/src/Filter.hs
@@ -11,29 +11,25 @@
 import Misc
 import Rewriter
 
-exclude' :: Expression -> [Expression] -> Expression
-exclude' expr [] = expr
-exclude' expr@(ExFormation _) (fqn : remaining) = case fqnToAttrs fqn of
-  Just fqn' -> exclude' (excludedFormation expr fqn') remaining
-  _ -> expr
+exclude' :: Expression -> [Expression] -> IO Expression
+exclude' expr [] = pure expr
+exclude' expr (fqn : remaining) = case fqnToAttrs fqn of
+  Just attrs@(_ : _) -> maybe (throwIO (CanNotFindObjectByLocator fqn)) (`exclude'` remaining) (excludedFormation expr attrs)
+  _ -> throwIO (InvalidLocatorProvided fqn)
   where
-    excludedFormation :: Expression -> [Attribute] -> Expression
-    excludedFormation (ExFormation bindings) [at] = ExFormation [bd | bd <- bindings, attributeFromBinding bd /= Just at]
-    excludedFormation (ExFormation bindings) atts = ExFormation (excludedBindings bindings atts)
-      where
-        excludedBindings :: [Binding] -> [Attribute] -> [Binding]
-        excludedBindings [] _ = []
-        excludedBindings (bd@(BiTau at' form@(ExFormation _)) : bs) as@(at'' : rs)
-          | at' == at'' = BiTau at' (excludedFormation form rs) : bs
-          | otherwise = bd : excludedBindings bs as
-        excludedBindings (bd : bs) as = bd : excludedBindings bs as
-    excludedFormation e _ = e
-exclude' expr _ = expr
+    excludedFormation :: Expression -> [Attribute] -> Maybe Expression
+    excludedFormation (ExFormation bindings) [at]
+      | any ((== Just at) . attributeFromBinding) bindings = Just (ExFormation [bd | bd <- bindings, attributeFromBinding bd /= Just at])
+    excludedFormation (ExFormation bindings) (at : rest) = case break (nested at) bindings of
+      (before, BiTau at' form : after) -> (\form' -> ExFormation (before ++ BiTau at' form' : after)) <$> excludedFormation form rest
+      _ -> Nothing
+    excludedFormation _ _ = Nothing
+    nested :: Attribute -> Binding -> Bool
+    nested at (BiTau at' (ExFormation _)) = at == at'
+    nested _ _ = False
 
-exclude :: [Rewritten] -> [Expression] -> [Rewritten]
-exclude [] _ = []
-exclude rs [] = rs
-exclude ((expr, maybeRule) : rest) exprs = (exclude' expr exprs, maybeRule) : exclude rest exprs
+exclude :: [Rewritten] -> [Expression] -> IO [Rewritten]
+exclude rs exprs = traverse (\(expr, maybeRule) -> (,maybeRule) <$> exclude' expr exprs) rs
 
 include' :: Expression -> [Expression] -> IO Expression
 include' expr [] = pure expr
diff --git a/src/Functions.hs b/src/Functions.hs
--- a/src/Functions.hs
+++ b/src/Functions.hs
@@ -213,6 +213,7 @@
 _number _ _ = throwIO (userError "Function number() requires exactly 1 argument as 'Φ.string'")
 
 _sum :: BuildTermMethod
+_sum [] _ = throwIO (userError "Function sum() requires at least 1 argument")
 _sum args subst = do
   nums <- traverse (`argToNumber` subst) args
   pure (TeExpression (DataNumber (numToBts (sum nums))))
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -155,7 +155,7 @@
         ( \idx comment (item, rule) reached ->
             let item' = toLatex (baseTab idx) item
                 opening = if idx == 0 then item' else printf "  %s %s" (relation reached) item'
-             in comment ++ maybe opening (\(judgment, name) -> printf "%s %s[\\nameref{r:%s}]" opening (relation judgment) name) rule
+             in comment ++ maybe opening (\(judgment, name) -> printf "%s %s[\\nameref{r:%s}]" opening (relation judgment) (escaped name)) rule
         )
         [0 ..]
         comments
@@ -468,12 +468,15 @@
 inference :: String -> String -> Maybe String -> Maybe Y.Condition -> [String] -> String -> String
 inference env name label cond premises conclusion =
   intercalate "\n" $
-    ["\\begin{" ++ env ++ "}", "  \\phinoName{" ++ name ++ "}"]
+    ["\\begin{" ++ env ++ "}", "  \\phinoName{" ++ escaped name ++ "}"]
       ++ maybe [] (\symbol -> ["  \\phinoLabel{" ++ symbol ++ "}"]) label
       ++ maybe [] (\rendered -> ["  \\phinoCondition{ " ++ rendered ++ " }"]) (conditionInLatex cond)
       ++ map (\premise -> "  \\phinoPremise{ " ++ premise ++ " }") premises
       ++ ["  \\phinoConclusion{ " ++ conclusion ++ " }", "\\end{" ++ env ++ "}"]
 
+escaped :: String -> String
+escaped = T.unpack . toLaTeX . T.pack
+
 renderExpr :: Expression -> String
 renderExpr expr = renderToLatex (expressionToCST expr) defaultLatexContext
 
@@ -484,7 +487,7 @@
 trrule macro label name lhs rhs cond extras =
   intercalate
     "\n  "
-    [ macro ++ labelArg ++ "{" ++ name ++ "}"
+    [ macro ++ labelArg ++ "{" ++ escaped name ++ "}"
     , braced lhs
     , braced rhs
     , conditionToLatex cond
diff --git a/src/Morph.hs b/src/Morph.hs
--- a/src/Morph.hs
+++ b/src/Morph.hs
@@ -19,7 +19,7 @@
 import Control.Exception (Exception, SomeException, catch, evaluate, throwIO, try)
 import Control.Monad (unless, when)
 import Data.Bifunctor (first)
-import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef)
+import Data.IORef (IORef, atomicModifyIORef', modifyIORef', newIORef, readIORef, writeIORef)
 import Data.List (find, partition)
 import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
@@ -54,7 +54,7 @@
 type FiringFunc = Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Maybe Expression, State)
 
 emptyState :: State
-emptyState = State 0 Nothing Nothing
+emptyState = State Nothing Nothing
 
 data Steps = Steps
   { _limit :: Int
@@ -95,6 +95,7 @@
   , _maxCycles :: Int
   , _steps :: Steps
   , _tally :: Maybe Tally
+  , _minted :: IORef Int
   , _deadline :: Maybe Deadline
   , _memo :: Maybe Memo
   , _nesting :: Int
@@ -440,12 +441,10 @@
       form <- held path store
       if copied form
         then do
+          fresh <- coined caller
           looped caller mode before (Just (fresh, called form))
-          throwIO (Severed (ExFormation [BiLambda (FnSymbol fresh)]) reached{_minted = fresh})
+          throwIO (Severed (ExFormation [BiLambda (FnSymbol fresh)]) reached)
         else refused caller refusal
-      where
-        fresh :: Int
-        fresh = reached._minted + 1
     cut _ _ caller refusal = refused caller refusal
     copied :: Expression -> Bool
     copied (ExFormation bds) = boxed bds && not (any abstract bds) && any code bds
@@ -488,11 +487,11 @@
         }
     deferred :: Expression -> State -> ReduceContext -> IO (Expression, State)
     deferred copy state' caller = do
+      fresh <- coined caller
       caller._saveEval (EvDeferred caller._nesting fresh caller._judgment copy (called copy) caller._site)
-      pure (ExFormation [BiLambda (FnSymbol fresh)], state'{_minted = fresh})
-      where
-        fresh :: Int
-        fresh = state'._minted + 1
+      pure (ExFormation [BiLambda (FnSymbol fresh)], state')
+    coined :: ReduceContext -> IO Int
+    coined caller = atomicModifyIORef' caller._minted (\count -> (count + 1, count + 1))
     called :: Expression -> Maybe Expression
     called copy@(ExFormation bds) = do
       (path, declared) <- origin copy
@@ -552,45 +551,44 @@
     spread :: Maybe Expression -> Frame -> Expression -> State -> ReduceContext -> IO (Expression, State)
     spread standing (Frame world _ _ _) form@(ExFormation bds) state' caller
       | not (any abstract bds) = do
-          jobs <- mapM (planned (synonym caller._universe form)) (zip [1 ..] bds)
-          (entered, _, state'') <- pooled caller._jobs jobs gathered ([], 0, state')
+          floor' <- readIORef caller._minted
+          jobs <- mapM (planned floor' (synonym caller._universe form)) (zip [1 ..] bds)
+          (entered, state'') <- pooled caller._jobs jobs (gathered floor') ([], state')
           pure (ExFormation (reverse entered), state'')
       where
-        floor' :: Int
-        floor' = state'._minted
-        planned :: Maybe (Expression, [Attribute]) -> (Int, Binding) -> IO (IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State))))
-        planned alias (idx, BiTau attr body)
+        planned :: Int -> Maybe (Expression, [Attribute]) -> (Int, Binding) -> IO (IO ([Evaluation], Int, Either SomeException (Int -> IO (Binding, Maybe State))))
+        planned floor' alias (idx, BiTau attr body)
           | attr /= AtRho = do
               new <- if closed body then fresh alias attr caller else pure True
-              pure (if new then worker idx attr body else kept (BiTau attr body))
-        planned _ (_, bd) = pure (kept bd)
-        kept :: Binding -> IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State)))
-        kept bd = pure ([], Right (const (pure (bd, Nothing))))
-        worker :: Int -> Attribute -> Expression -> IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State)))
-        worker idx attr body = do
+              pure (if new then worker floor' idx attr body else kept (BiTau attr body))
+        planned _ _ (_, bd) = pure (kept bd)
+        kept :: Binding -> IO ([Evaluation], Int, Either SomeException (Int -> IO (Binding, Maybe State)))
+        kept bd = pure ([], 0, Right (const (pure (bd, Nothing))))
+        worker :: Int -> Int -> Attribute -> Expression -> IO ([Evaluation], Int, Either SomeException (Int -> IO (Binding, Maybe State)))
+        worker floor' idx attr body = do
           buffer <- newIORef []
           tau <- tausOf idx
           tally <- tallied (fmap (\(Tally cap _) -> cap) caller._tally)
+          minted <- newIORef floor'
           memo <- memoized caller._acyclic
           copy <- newIORef =<< readIORef world
           (store, path) <- home standing copy form
-          let own = caller{_jobs = 1, _tally = tally, _memo = memo, _saveEval = modifyIORef' buffer . (:), _buildTerm = minting tau caller._buildTerm}
+          let own = caller{_jobs = 1, _tally = tally, _minted = minted, _memo = memo, _saveEval = modifyIORef' buffer . (:), _buildTerm = minting tau caller._buildTerm}
           outcome <- try (try (go (fmap (`ExDispatch` attr) standing) Nothing (Frame copy store path (Just attr)) body state' own))
           records <- reverse <$> readIORef buffer
-          pure (records, fmap (either severed (\(term, walked) offset -> pure (BiTau attr (lifted floor' offset term), Just (moved offset walked)))) outcome)
-        severed :: Severed -> Int -> IO (Binding, Maybe State)
-        severed (Severed answer reached) offset = throwIO (Severed (lifted floor' offset answer) (moved offset reached))
-        moved :: Int -> State -> State
-        moved offset walked =
-          walked
-            { _minted = walked._minted + offset
-            , _manufactured = fmap (\sym -> if sym > floor' then sym + offset else sym) walked._manufactured
-            }
-        gathered :: ([Binding], Int, State) -> ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State))) -> IO ([Binding], Int, State)
-        gathered (done, offset, current) (records, outcome) = do
+          spent <- subtract floor' <$> readIORef minted
+          pure (records, spent, fmap (either (severed floor') (\(term, walked) offset -> pure (BiTau attr (lifted floor' offset term), Just (moved floor' offset walked)))) outcome)
+        severed :: Int -> Severed -> Int -> IO (Binding, Maybe State)
+        severed floor' (Severed answer reached) offset = throwIO (Severed (lifted floor' offset answer) (moved floor' offset reached))
+        moved :: Int -> Int -> State -> State
+        moved floor' offset walked = walked{_manufactured = fmap (\sym -> if sym > floor' then sym + offset else sym) walked._manufactured}
+        gathered :: Int -> ([Binding], State) -> ([Evaluation], Int, Either SomeException (Int -> IO (Binding, Maybe State))) -> IO ([Binding], State)
+        gathered floor' (done, current) (records, spent, outcome) = do
+          offset <- subtract floor' <$> readIORef caller._minted
           mapM_ (caller._saveEval . renumbered floor' offset) records
+          modifyIORef' caller._minted (+ spent)
           (bd, walked) <- either throwIO ($ offset) outcome
-          pure (bd : done, maybe offset (\after -> after._minted - floor') walked, fromMaybe current walked)
+          pure (bd : done, fromMaybe current walked)
     spread standing frame term state' caller = parts standing frame term state' caller
     minting :: IO T.Text -> BuildTermFunc -> BuildTermFunc
     minting tau build func
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -25,7 +25,7 @@
 import Control.Exception (Exception)
 import Control.Monad (guard, when)
 import Data.Char (isAsciiLower, isAsciiUpper, isDigit)
-import Data.Scientific (toRealFloat)
+import Data.Scientific (scientific, toRealFloat)
 import qualified Data.Set as Set
 import qualified Data.Text as T
 import Data.Void
@@ -74,7 +74,7 @@
 label' :: Parser T.Text
 label' = lexeme $ do
   first <- oneOf ['a' .. 'z']
-  rest <- many (satisfy (`notElem` " \r\n\t,.|':;!?][}{)(⟧⟦") <?> "allowed character")
+  rest <- many (choice [try (char '-' <* notFollowedBy (char '>')), satisfy (`notElem` " \r\n\t,.|':;!?][}{)(⟧⟦-↦⤍>\"ξΦ⊥")] <?> "allowed character")
   return (T.pack (first : rest))
 
 function :: Parser String
@@ -186,16 +186,29 @@
 number :: Parser Expression
 number = do
   sign <- optional (choice [char '-', char '+'])
-  unsigned <- lexeme L.scientific
+  unsigned <- lexeme magnitude
   return
     ( DataNumber
         ( numToBts
             ( case sign of
-                Just '-' -> negate (toRealFloat unsigned)
-                _ -> toRealFloat unsigned
+                Just '-' -> negate unsigned
+                _ -> unsigned
             )
         )
     )
+  where
+    magnitude :: Parser Double
+    magnitude = do
+      whole <- some digitChar
+      fraction <- option "" (try (char '.' >> some digitChar))
+      power <- option 0 (try (oneOf ['e', 'E'] >> L.signed (pure ()) L.decimal))
+      pure (scaled (read (whole ++ fraction)) (power - toInteger (length fraction)) (toInteger (length (whole ++ fraction))))
+    scaled :: Integer -> Integer -> Integer -> Double
+    scaled coefficient power digits
+      | coefficient == 0 = 0
+      | power > 400 = 1 / 0
+      | power < negate (400 + digits) = 0
+      | otherwise = toRealFloat (scientific coefficient (fromInteger power))
 
 root :: Parser Expression
 root = do
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -200,7 +200,7 @@
               _applied rule (RuleContext _buildTerm _universe _normal) expression >>= \case
                 Nothing -> do
                   logDebug (printf "Rule '%s' does not match, rewriting is stopped" ruleName)
-                  if _breakpoint == Just ruleName
+                  if _breakpoint == Just ruleName && ruleName `notElem` [fired | (_, Just (_, fired)) <- NE.toList _rewrittens]
                     then do
                       logDebug (printf "Rule '%s' is a breakpoint, dropping down all the previous rewritings..." ruleName)
                       pure (_rewrittens, expression, _unique, True, _found)
diff --git a/src/Sugar.hs b/src/Sugar.hs
--- a/src/Sugar.hs
+++ b/src/Sugar.hs
@@ -62,8 +62,19 @@
       | otherwise = Just (AA_TAU (APP_BINDING (goPair pair)))
     goArgument (AA_TAUS binding) = case goArgBinding binding of
       BI_EMPTY{} -> Nothing
-      binding' -> Just (AA_TAUS binding')
+      binding'
+        | sugar == SWEET, Just args <- positional binding' -> Just (AA_EXPRS args)
+        | otherwise -> Just (AA_TAUS binding')
     goArgument (AA_EXPRS args) = Just (AA_EXPRS (goAppArg args))
+    positional :: BINDING -> Maybe APP_ARG
+    positional (BI_PAIR (PA_ALPHA (AL_IDX _ 0) _ first) rest _) = APP_ARG first <$> following 1 rest
+      where
+        following :: Int -> BINDINGS -> Maybe APP_ARGS
+        following _ BDS_EMPTY{} = Just AAS_EMPTY
+        following next (BDS_PAIR eol' tab' (PA_ALPHA (AL_IDX _ index) _ arg) more)
+          | index == next = AAS_EXPR eol' tab' arg <$> following (next + 1) more
+        following _ _ = Nothing
+    positional _ = Nothing
     goArgBinding :: BINDING -> BINDING
     goArgBinding empty@BI_EMPTY{} = empty
     goArgBinding BI_META{..} = BI_META meta (goArgBindings bindings) tab
diff --git a/src/XMIR.hs b/src/XMIR.hs
--- a/src/XMIR.hs
+++ b/src/XMIR.hs
@@ -618,7 +618,9 @@
             | not (hasAttr "base" arg) && hasText arg = do
                 key <- asToKey arg idx
                 bytes <- getText arg
-                pure (ExApplication expr (mkArg key (ExFormation [BiDelta (bytesToBts bytes)])))
+                bds <- mapM (\node -> xmirToFormationBinding derived node fqn) (arg C.$/ C.element (toName "o"))
+                let delta = BiDelta (bytesToBts (T.unpack (T.strip (T.pack bytes))))
+                pure (ExApplication expr (mkArg key (ExFormation (delta : bds))))
             | otherwise = do
                 key <- asToKey arg idx
                 arg' <- xmirToExpression derived arg fqn
@@ -662,7 +664,7 @@
         at : _ ->
           let attr = T.unpack at
            in if null attr
-                then throwIO (InvalidXMIRFormat (printf "The attribute '%s' is not expected to be empty" attr) cur)
+                then throwIO (InvalidXMIRFormat (printf "The attribute '%s' is not expected to be empty" key) cur)
                 else pure attr
 
 hasText :: C.Cursor -> Bool
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -21,6 +21,7 @@
 import Data.Maybe (fromMaybe)
 import Data.Scientific (isInteger)
 import Data.Text (Text, unpack)
+import qualified Data.Text as T
 import Data.Yaml (Parser)
 import qualified Data.Yaml as Yaml
 import GHC.Generics (Generic)
@@ -197,6 +198,7 @@
     referenceless rule.name "where" rule.where_
     referenceless rule.name "having" rule.having
     targets rule (metas rule.pattern) (fromMaybe [] rule.where_)
+    steps rule (named (metas rule.pattern)) (fromMaybe [] rule.where_)
     pure rule
     where
       targets :: Rule -> [Text] -> [Extra] -> Parser ()
@@ -211,6 +213,27 @@
       fresh rule known bound
         | bound `elem` known = fail (printf "The rule '%s' has a 'where' step that binds the meta '%s' again, while it is already bound" rule.name (unpack bound))
         | otherwise = pure ()
+      named :: [Text] -> [Text]
+      named = filter ((> 1) . T.length)
+      steps :: Rule -> [Text] -> [Extra] -> Parser ()
+      steps rule known [] = do
+        unread rule known "result" (metas rule.result)
+        unread rule known "when" (metas rule.when)
+        unread rule known "having" (metas rule.having)
+      steps rule known (extra : rest) = do
+        unread rule known "where" (metas extra.args)
+        steps rule (known ++ named (metas extra.meta)) rest
+      unread :: Rule -> [Text] -> String -> [Text] -> Parser ()
+      unread rule known field used = case filter (`notElem` known) (named used) of
+        [] -> pure ()
+        missing : _ ->
+          fail
+            ( printf
+                "The rule '%s' reads the meta '%s' it never binds, in '%s', since neither its pattern nor an earlier 'where' step binds it"
+                rule.name
+                (unpack missing)
+                field
+            )
 
 data Number
   = MetaIndex Text
diff --git a/test/AbridgeSpec.hs b/test/AbridgeSpec.hs
--- a/test/AbridgeSpec.hs
+++ b/test/AbridgeSpec.hs
@@ -21,25 +21,25 @@
   describe "abridged" $ do
     it "leaves a formation no longer than the width as it is" $
       printExpressionWith
-        (const (abridged 64))
+        (const (abridged True 64))
         (ExFormation [BiTau (AtLabel "kübel") (ExDispatch ExXi (AtLabel "wand")), BiVoid (AtLabel "zaun")])
         (SWEET, UNICODE, SINGLELINE, defaultMargin)
         `shouldBe` "⟦ kübel ↦ wand, zaun ↦ ∅ ⟧"
     it "keeps a formation exactly as wide as the width" $
       printExpressionWith
-        (const (abridged 68))
+        (const (abridged True 68))
         (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("ort-" <> show idx))) ExRoot) [1 .. 6 :: Int]))
         (SWEET, UNICODE, SINGLELINE, defaultMargin)
         `shouldBe` "⟦ ort-1 ↦ Φ, ort-2 ↦ Φ, ort-3 ↦ Φ, ort-4 ↦ Φ, ort-5 ↦ Φ, ort-6 ↦ Φ ⟧"
     it "folds a formation one character wider than the width" $
       printExpressionWith
-        (const (abridged 67))
+        (const (abridged True 67))
         (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("ort-" <> show idx))) ExRoot) [1 .. 6 :: Int]))
         (SWEET, UNICODE, SINGLELINE, defaultMargin)
         `shouldBe` "⟦ +6 ⟧"
     it "keeps the data and the λ of a long formation and folds the rest into a count" $
       printExpressionWith
-        (const (abridged 64))
+        (const (abridged True 64))
         ( ExFormation
             ( BiDelta (BtMany ["00", "77", "66"])
                 : BiLambda (Function "L_xxx")
@@ -50,7 +50,7 @@
         `shouldBe` "⟦ Δ ⤍ 00-77-66, λ ⤍ L_xxx, +34 ⟧"
     it "keeps the φ of a long formation and folds the formation it holds" $
       printExpressionWith
-        (const (abridged 64))
+        (const (abridged True 64))
         ( ExFormation
             [ BiTau (AtLabel "hund") ExRoot
             , BiTau AtPhi (ExFormation (map (\idx -> BiTau (AtLabel (T.pack ("pfote-" <> show idx))) ExRoot) [1 .. 9 :: Int]))
@@ -61,25 +61,37 @@
         `shouldBe` "⟦ φ ↦ ⟦ +9 ⟧, +2 ⟧"
     it "cuts a long byte string to its first bytes, its last bytes and the count of the bytes between them" $
       printExpressionWith
-        (const (abridged 64))
+        (const (abridged True 64))
         (ExFormation [BiDelta (BtMany (map (printf "%02X") [7 .. 51 :: Int]))])
         (SWEET, UNICODE, SINGLELINE, defaultMargin)
         `shouldBe` "07-08-..(41b)..-32-33:Δ"
     it "cuts a long byte string inside a formation too short to fold" $
       printExpressionWith
-        (const (abridged 64))
+        (const (abridged True 64))
         (ExFormation [BiTau (AtLabel "k") (ExFormation [BiDelta (BtMany ["01", "02", "03", "04", "05", "06", "07", "08", "09", "0A"])])])
         (SWEET, UNICODE, SINGLELINE, defaultMargin)
         `shouldBe` "01-02-..(6b)..-09-0A:Δ:k"
+    it "keeps a long byte string whole unless told to cut the data" $
+      printExpressionWith
+        (const (abridged False 64))
+        (ExFormation [BiDelta (BtMany (map (printf "%02X") [3 .. 19 :: Int]))])
+        (SWEET, UNICODE, SINGLELINE, defaultMargin)
+        `shouldBe` "03-04-05-06-07-08-09-0A-0B-0C-0D-0E-0F-10-11-12-13:Δ"
+    it "folds a long formation and keeps its long byte string whole unless told to cut the data" $
+      printExpressionWith
+        (const (abridged False 64))
+        (ExFormation (BiDelta (BtMany ["30", "31", "32", "33", "34", "35", "36", "37", "38", "39", "41", "42"]) : map (\idx -> BiVoid (AtLabel (T.pack ("fenster-" <> show idx)))) [1 .. 7 :: Int]))
+        (SWEET, UNICODE, SINGLELINE, defaultMargin)
+        `shouldBe` "⟦ Δ ⤍ 30-31-32-33-34-35-36-37-38-39-41-42, +7 ⟧"
     it "keeps a byte string of eight bytes whole" $
       printExpressionWith
-        (const (abridged 64))
+        (const (abridged True 64))
         (ExFormation (BiDelta (BtMany ["40", "60", "E0", "00", "00", "00", "00", "01"]) : map (\idx -> BiVoid (AtLabel (T.pack ("ränder-" <> show idx)))) [1 .. 5 :: Int]))
         (SWEET, UNICODE, SINGLELINE, defaultMargin)
         `shouldBe` "⟦ Δ ⤍ 40-60-E0-00-00-00-00-01, +5 ⟧"
     it "spells a folded formation the same way in ASCII" $
       printExpressionWith
-        (const (abridged 64))
+        (const (abridged True 64))
         (ExFormation (BiLambda (Function "F") : map (\idx -> BiVoid (AtLabel (T.pack ("sehr-langes-" <> show idx)))) [1 .. 5 :: Int]))
         (SWEET, ASCII, SINGLELINE, defaultMargin)
         `shouldBe` "[[ L> F, +5 ]]"
diff --git a/test/CLIHelpersSpec.hs b/test/CLIHelpersSpec.hs
--- a/test/CLIHelpersSpec.hs
+++ b/test/CLIHelpersSpec.hs
@@ -22,7 +22,7 @@
 {-# ANN testPrintContext ("HLint: ignore Eta reduce" :: String) #-}
 testPrintContext :: IOFormat -> PrintContext
 testPrintContext format =
-  PrintCtx SWEET False Nothing MULTILINE 2 defaultXmirContext False False False False False 1 1 ExRoot Nothing Nothing Nothing format
+  PrintCtx SWEET False Nothing False MULTILINE 2 defaultXmirContext False False False False False 1 1 ExRoot Nothing Nothing Nothing format
 
 spec :: Spec
 spec = do
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -238,6 +238,12 @@
         , ["rewrite", "--sweet", "--hide-rho", "--margin=3"]
         , ["⟦\n  b(c) ↦ ⟦⟧\n⟧:x:a"]
         )
+      ,
+        ( "prints positional arguments as such once the rho is gone"
+        , "⟦ a ↦ ξ.b(ρ ↦ ξ, α0 ↦ ξ.c, α1 ↦ ξ.d) ⟧"
+        , ["rewrite", "--flat", "--sweet", "--hide-rho"]
+        , ["b( c, d ):a"]
+        )
       ]
       (\(desc, input, args, expected) -> it desc (withStdin input (testCLISucceeded args expected)))
 
@@ -1168,6 +1174,12 @@
         withStdin "[[ x -> $ ]]" $
           testCLISucceeded ["rewrite", "--rule=" ++ fix, "--max-depth=1", "--depth-sensitive", "--flat"] ["⟦ x ↦ Φ ⟧"]
 
+    it "keeps the rewritten expression when the --breakpoint rule fired" $
+      withStdin "⟦ a ↦ ⟦ b ↦ Φ ⟧.b ⟧" $
+        testCLISucceeded
+          ["rewrite", "--flat", "--normalize", "--breakpoint=dot"]
+          ["⟦ a ↦ Φ( ρ ↦ ⟦ b ↦ Φ ⟧ ) ⟧"]
+
   describe "morph --focus under --locator" $ do
     it "finds the same object for the steps and for the answer" $
       withStdin "⟦ t ↦ ⟦ a ↦ ⟦ Δ ⤍ 01- ⟧ ⟧, a ↦ ⟦ Δ ⤍ 02- ⟧ ⟧" $ do
@@ -1181,6 +1193,10 @@
         (out, _) <- withStdout (try (runCLI ["morph", "--locator=Q.t", "--focus=Q.nope", "--flat", "--sequence"]) :: IO (Either ExitCode ()))
         out `shouldNotContain` "⟦ t ↦"
 
+  it "fails on a --hide locator that matches nothing, as --show does" $
+    withStdin "[[ x -> Q.y ]]" $
+      testCLIFailed ["rewrite", "--hide=Q.nope"] ["Can't find object by locator: 'Φ.nope'"]
+
   describe "dataize" $ do
     it "prints help" $
       testCLISucceeded ["dataize", "--help"] ["Dataize the 𝜑-expression"]
@@ -1379,15 +1395,29 @@
         , ("XMLXXXXXX.xml", "    <bind meta=\"𝛿1.1\">01-02-..(8b)..-0B-0C</bind>")
         ]
         ( \(template, line) ->
-            it ("cuts a long datum a firing came down to, as " ++ line) $
+            it ("cuts a long datum a firing came down to under --abridged-data, as " ++ line) $
               withTempFile template $ \(path, stream) -> do
                 hClose stream
                 withLambdasOf (T.pack "- λ: L_outer\n  dataize:\n    𝛿1: ξ.arg\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \outer ->
                   withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ Δ ⤍ 01-02-03-04-05-06-07-08-09-0A-0B-0C ⟧, λ ⤍ L_outer ⟧ ⟧" $
-                    testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []
+                    testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--abridged-data", "--sweet", "--hide-rho", "--quiet"] []
                 records <- readProtocol path
                 lines records `shouldContain` [line]
         )
+      forM_
+        [ ("textXXXXXX.txt", "    𝛿1.1 := 30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46  # 𝔻(ξ.arg)")
+        , ("XMLXXXXXX.xml", "    <bind meta=\"𝛿1.1\">30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46</bind>")
+        ]
+        ( \(template, line) ->
+            it ("keeps a long datum a firing came down to whole without --abridged-data, as " ++ line) $
+              withTempFile template $ \(path, stream) -> do
+                hClose stream
+                withLambdasOf (T.pack "- λ: L_hex\n  dataize:\n    𝛿1: ξ.arg\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \hex ->
+                  withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ Δ ⤍ 30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46 ⟧, λ ⤍ L_hex ⟧ ⟧" $
+                    testCLISucceeded ["dataize", "--symbolic=" ++ hex, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []
+                records <- readProtocol path
+                lines records `shouldContain` [line]
+        )
       it "folds a long formation under the width given as the value" $
         withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
           hClose stream
@@ -1413,6 +1443,12 @@
       it "refuses the flag without a protocol" $
         withStdin wide $
           testCLIFailed ["dataize", "--locator=Q.t", "--abridged"] ["The option --abridged requires --protocol"]
+      it "refuses to cut the data in dataize without --abridged" $
+        withStdin wide $
+          testCLIFailed ["dataize", "--locator=Q.t", "--protocol=daten.txt", "--abridged-data"] ["The option --abridged-data requires --abridged"]
+      it "refuses to cut the data in morph without --abridged" $
+        withStdin wide $
+          testCLIFailed ["morph", "--locator=Q.t", "--protocol=daten.xml", "--abridged-data"] ["The option --abridged-data requires --abridged"]
 
     describe "--protocol" $ do
       let sum' = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
diff --git a/test/CompiledSpec.hs b/test/CompiledSpec.hs
--- a/test/CompiledSpec.hs
+++ b/test/CompiledSpec.hs
@@ -87,11 +87,11 @@
     matched :: Expression -> IO (Set.Set Int)
     matched expr = Set.fromList . map fst <$> filterM (\(_, rule) -> not . null <$> matchExpressionWithRule expr rule (RuleContext (building yaml) Nothing (_normal yaml))) (zip [0 ..] Y.normalizationRules)
     morphed :: Lambdas -> Engine -> Expression -> IO (Either String String)
-    morphed lambdas engine world = settled (show . fst <$> morph' (ExDispatch ExRoot (AtLabel "x"), (world, Nothing) :| []) world emptyState (reducing lambdas engine))
+    morphed lambdas engine world = settled (show . fst <$> (morph' (ExDispatch ExRoot (AtLabel "x"), (world, Nothing) :| []) world emptyState =<< reducing lambdas engine))
     dataized :: Lambdas -> Engine -> Expression -> IO (Either String String)
-    dataized lambdas engine world = settled (show . fst <$> dataize' (ExDispatch ExRoot (AtLabel "x"), (world, Nothing) :| []) world emptyState (reducing lambdas engine))
-    reducing :: Lambdas -> Engine -> ReduceContext
-    reducing lambdas engine = (defaultReduceContext ExRoot){_engine = engine, _buildTerm = building engine, _shuffle = False, _steps = Steps 40 0, _symbolic = lambdas}
+    dataized lambdas engine world = settled (show . fst <$> (dataize' (ExDispatch ExRoot (AtLabel "x"), (world, Nothing) :| []) world emptyState =<< reducing lambdas engine))
+    reducing :: Lambdas -> Engine -> IO ReduceContext
+    reducing lambdas engine = (\ctx -> ctx{_engine = engine, _buildTerm = building engine, _shuffle = False, _steps = Steps 40 0, _symbolic = lambdas}) <$> defaultReduceContext ExRoot
     program :: Int -> Expression
     program seed = fst (formation False 4 (mkStdGen seed))
     contextualized :: Engine -> Expression -> Expression -> IO (Either String String)
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -13,6 +13,7 @@
 import Control.Exception (SomeException)
 import Control.Monad
 import Data.Aeson (FromJSON)
+import Data.IORef (newIORef)
 import Data.List (find, isInfixOf, nub)
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.Map.Strict qualified as Map
@@ -39,7 +40,7 @@
 test func useCases =
   forM_ useCases $ \(desc, input, expr, output) ->
     it desc $ do
-      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultReduceContext ExRoot)
+      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState =<< defaultReduceContext ExRoot
       res `shouldBe` output
 
 data DataizePack = DataizePack
@@ -57,7 +58,8 @@
   DataizePack{..} <- Decode.decodeFileThrow pth
   expr <- parseExpressionThrows (if model == Just True then primitives input else input)
   loc <- parseExpressionThrows (fromMaybe "Q" location)
-  let ctx = (defaultReduceContext loc){_symbolic = if symbolic == Just True then known else emptyLambdas}
+  base <- defaultReduceContext loc
+  let ctx = base{_symbolic = if symbolic == Just True then known else emptyLambdas}
   case (result, fails) of
     (Just res, Nothing) -> do
       bts <- either (fail . ("cannot read the expected bytes: " ++)) pure (parseBytes res)
@@ -71,7 +73,8 @@
 partially known src = do
   expr <- parseExpressionThrows (primitives src)
   recorded $ \record -> do
-    let ctx = (withLambdas known (defaultReduceContext ExRoot)){_partial = True, _saveEval = record}
+    base <- defaultReduceContext ExRoot
+    let ctx = (withLambdas known base){_partial = True, _saveEval = record}
     (outcome, chain, _) <- dataize expr emptyState ctx
     pure (outcome, chain)
 
@@ -84,11 +87,12 @@
 
   describe "dataize' fails when no dataization rule matches the term" $
     it "throws instead of treating the unmatched meta as ⊥" $
-      dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)
+      (dataize' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot)
         `shouldThrow` (\e -> "no dataization rule matched" `isInfixOf` show (e :: SomeException))
 
   describe "dataization 'norm' is disjoint from the specific clauses" $ do
-    let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot)) Nothing (_normal linked)
+    ctx <- runIO (defaultReduceContext ExRoot)
+    let rctx = RuleContext (execBuildTerm ExRoot ctx) Nothing (_normal linked)
         dataizeRule :: String -> Yaml.DataizeRule
         dataizeRule nm = fromMaybe (error ("no dataization rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.dataizationRules)
         asRule :: Yaml.DataizeRule -> Yaml.Rule
@@ -156,7 +160,7 @@
   describe "fails to dataize the terminator" $ do
     let failsOn desc input =
           it desc $
-            dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)
+            (dataize' (input, (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot)
               `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
     failsOn "throws on ⊥ instead of mapping it to empty bytes" ExTermination
     failsOn "throws on a data-less formation, which dataizes ⊥" (ExFormation [])
@@ -168,13 +172,15 @@
     it "fails on the step limit instead of morphing forever" $
       looping $ \endless -> do
         expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧"
-        dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+        minted <- newIORef 0
+        dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
           `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))
 
     it "parks the step limit as a residual with --partial" $
       looping $ \endless -> do
         expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧"
-        (outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing Nothing Nothing 1 False True True False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+        minted <- newIORef 0
+        (outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 False True True False 1 Nothing Dataization [] Map.empty endless (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
         case outcome of
           Residual _ -> pure ()
           Dataized bts -> expectationFailure ("expected a residual, dataized to " ++ show bts)
@@ -183,14 +189,15 @@
     it "fails a partial dataization once the deadline has passed" $ do
       expr <- parseExpressionThrows "[[ @ -> [[ D> 7E- ]] ]]"
       deadline <- overdue 29
-      dataize expr emptyState (defaultReduceContext ExRoot){_deadline = Just deadline, _partial = True}
+      ctx <- defaultReduceContext ExRoot
+      dataize expr emptyState ctx{_deadline = Just deadline, _partial = True}
         `shouldThrow` (\e -> "--max-seconds=29" `isInfixOf` show (e :: SomeException))
 
   describe "partially evaluates around a λ function that cannot fire (--partial)" $ do
     let placeholder = ExFormation [BiLambda (Function "Sym_arg_0")]
     it "fails on it without the flag, naming the λ function" $ do
       expr <- parseExpressionThrows (primitives "2.times(3).nope")
-      dataize expr emptyState (withLambdas known (defaultReduceContext ExRoot))
+      (dataize expr emptyState . withLambdas known =<< defaultReduceContext ExRoot)
         `shouldThrow` (\e -> "No entry of --symbolic answers the λ function 'L_number_nope'" `isInfixOf` show (e :: SomeException))
     it "leaves the application of the unanswered λ function in place" $ do
       ((outcome, _), _) <- partially known "2.times(3).nope"
@@ -241,27 +248,30 @@
     forM_
       [
         ( "--max-cycles"
-        , ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing Nothing Nothing 1 True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
+        , \minted -> ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
         , "--max-cycles=0"
         )
       ,
         ( "--max-depth"
-        , ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing Nothing Nothing 1 True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
+        , \minted -> ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing minted Nothing Nothing 1 True True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
         , "--max-depth=0"
         )
       ]
-      ( \(flag, ctx, message) ->
+      ( \(flag, reducing, message) ->
           it ("throws once " ++ flag ++ " is exhausted with --depth-sensitive") $ do
             expr <- parseExpressionThrows "[[ @ -> [[ x -> [[ D> 00- ]] ]].x ]]"
+            ctx <- reducing <$> newIORef 0
             dataize expr emptyState ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))
       )
     it "does not throw without --depth-sensitive even once --max-depth is exhausted" $ do
       expr <- parseExpressionThrows boxed
-      (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+      minted <- newIORef 0
+      (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing minted Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
       value `shouldBe` Dataized (BtOne "00")
     it "throws once --max-cycles is exhausted even without --depth-sensitive" $ do
       expr <- parseExpressionThrows boxed
-      dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
+      minted <- newIORef 0
+      dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 False True False False 1 Nothing Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
         `shouldThrow` (\e -> "--max-cycles=0" `isInfixOf` show (e :: SomeException))
 
   describe "labels every step with a defined rule or operation" $ do
@@ -280,7 +290,7 @@
     it "uses no step label without a defining rule or operation" $ do
       expr <- parseExpressionThrows (primitives "5.plus(6)")
       loc <- parseExpressionThrows "Q"
-      (_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc))
+      (_, chain, _) <- dataize expr emptyState . withLambdas known =<< defaultReduceContext loc
       let orphans = nub [label | (_, Just (_, label)) <- chain, label `notElem` allowed, label /= "symbol"]
       unless
         (null orphans)
@@ -288,15 +298,15 @@
     it "takes the step of a firing by evaluation" $ do
       expr <- parseExpressionThrows (primitives "5.plus(6)")
       loc <- parseExpressionThrows "Q"
-      (_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc))
+      (_, chain, _) <- dataize expr emptyState . withLambdas known =<< defaultReduceContext loc
       map snd chain `shouldContain` [Just (Evaluation, "evaluate")]
     it "takes the step of a box by contextualization" $ do
       expr <- parseExpressionThrows "[[ @ -> [[ D> 0A- ]] ]]"
-      (_, chain, _) <- dataize expr emptyState (defaultReduceContext ExRoot)
+      (_, chain, _) <- dataize expr emptyState =<< defaultReduceContext ExRoot
       map snd chain `shouldContain` [Just (Contextualization, "contextualize")]
     it "takes the step of a delta by dataization" $ do
       expr <- parseExpressionThrows "[[ D> 3C- ]]"
-      (_, chain, _) <- dataize expr emptyState (defaultReduceContext ExRoot)
+      (_, chain, _) <- dataize expr emptyState =<< defaultReduceContext ExRoot
       map snd chain `shouldBe` [Just (Dataization, "delta"), Nothing]
 
   describe "names every rule uniquely across rule sets" $
@@ -313,7 +323,7 @@
     let labelsOf loc src = do
           expr <- parseExpressionThrows src
           loc' <- parseExpressionThrows loc
-          (_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext loc'))
+          (_, chain, _) <- dataize expr emptyState . withLambdas known =<< defaultReduceContext loc'
           pure [label | (_, Just (_, label)) <- chain]
     it "dataizes 5.plus(6) through the expected rules" $ do
       labels <-
@@ -335,7 +345,7 @@
       labels `shouldBe` ["contextualize", "md", "dot", "skip", "mf", "delta"]
     it "takes every step of 5.plus(6) by the judgment of its rule" $ do
       expr <- parseExpressionThrows "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
-      (_, chain, _) <- dataize expr emptyState (withLambdas known (defaultReduceContext ExRoot))
+      (_, chain, _) <- dataize expr emptyState . withLambdas known =<< defaultReduceContext ExRoot
       [judgment | (_, Just (judgment, _)) <- chain]
         `shouldBe` [ Contextualization
                    , Morphing
diff --git a/test/EvaluateSpec.hs b/test/EvaluateSpec.hs
--- a/test/EvaluateSpec.hs
+++ b/test/EvaluateSpec.hs
@@ -26,7 +26,7 @@
 import Lining (LineFormat (SINGLELINE))
 import Margin (defaultMargin)
 import Matcher (substEmpty)
-import Morph (ReduceContext (..), Steps (..), execBuildTerm, memoized, morph)
+import Morph (ReduceContext (..), Steps (..), emptyState, execBuildTerm, memoized, morph)
 import Parser (parseExpressionThrows)
 import Printer (printExpression, printExpression', printExpressionHidingRho')
 import Sugar (SugarType (SWEET))
@@ -65,8 +65,9 @@
     (_, written) <- recorded' hidden $ \record -> do
       let mode = named <$> acyclic
       cells <- memoized mode
+      base <- defaultReduceContext loc
       let ctx =
-            (defaultReduceContext loc)
+            base
               { _deep = deep == Just True
               , _partial = partial == Just True
               , _acyclic = mode
@@ -76,11 +77,12 @@
               , _saveEval = record
               }
       record (EvRun Morphing (T.pack (printExpression loc)))
+      started expr ctx
       case fails of
         Just message ->
-          morph expr (started expr) ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))
+          morph expr emptyState ctx `shouldThrow` (\err -> message `isInfixOf` show (err :: SomeException))
         Nothing -> do
-          (morphed, _, _) <- morph expr (started expr) ctx
+          (morphed, _, _) <- morph expr emptyState ctx
           forM_ result $ \res -> do
             expected <- parseExpressionThrows res
             spelled hidden morphed `shouldBe` spelled False expected
@@ -103,8 +105,9 @@
 
   describe "execBuildTerm 'evaluate'" $ do
     let univ = ExFormation []
-        ctx = withLambdas known (defaultReduceContext ExRoot)
-        runEvaluate args = execBuildTerm univ ctx "evaluate" args substEmpty
+        runEvaluate args = do
+          ctx <- withLambdas known <$> defaultReduceContext ExRoot
+          execBuildTerm univ ctx "evaluate" args substEmpty
     forM_
       [
         ( "the first argument is not a formation"
@@ -124,7 +127,8 @@
 
     it "gets stuck on a λ naming a symbol, instead of refusing the formation" $ do
       (_, written) <- recorded $ \record -> do
-        let stuck = (withLambdas known (defaultReduceContext ExRoot)){_saveEval = record}
+        ctx <- withLambdas known <$> defaultReduceContext ExRoot
+        let stuck = ctx{_saveEval = record}
             fire = execBuildTerm univ stuck "evaluate" [ArgExpression (ExFormation [BiLambda (FnSymbol 1)]), ArgExpression univ] substEmpty
         fire `shouldThrow` (\e -> "No entry of --symbolic answers the λ function '𝜎1'" `isInfixOf` show (e :: SomeException))
       written `shouldBe` "  unanswered(𝜎1)  # 𝕄(𝜎1:λ)\n"
@@ -147,7 +151,8 @@
     it "evaluates a λ-bearing formation to the answer of its entry, normalized" $ do
       let form = ExFormation [BiLambda (Function "L_answer"), BiTau AtRho (ExFormation [BiDelta (BtOne "00")])]
       answered <- withLambdasOf "- λ: L_answer\n  𝑛: ⟦ Δ ⤍ FF- ⟧\n" readLambdas
-      result <- execBuildTerm univ (withLambdas answered ctx) "evaluate" [ArgExpression form, ArgExpression univ] substEmpty
+      ctx <- withLambdas answered <$> defaultReduceContext ExRoot
+      result <- execBuildTerm univ ctx "evaluate" [ArgExpression form, ArgExpression univ] substEmpty
       case result of
         TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "FF")]
         _ -> expectationFailure "expected TeExpression"
diff --git a/test/FilterSpec.hs b/test/FilterSpec.hs
--- a/test/FilterSpec.hs
+++ b/test/FilterSpec.hs
@@ -44,30 +44,33 @@
           included <- traverse parseExpressionThrows shown
           excluded <- traverse parseExpressionThrows hidden
           res <- parseExpressionThrows result
-          [(expr', _)] <- (`F.exclude` excluded) <$> F.include [(expr, Nothing)] included
+          [(expr', _)] <- F.include [(expr, Nothing)] included >>= (`F.exclude` excluded)
           expr' `shouldBe` res
       )
 
   describe "direct unit tests" $ do
     describe "exclude" $ do
-      it "leaves the expression untouched when the fqn is not a Q-dispatch chain" $ do
-        expr <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"
-        badFqn <- parseExpressionThrows "$.x"
-        let [(expr', _)] = F.exclude [(expr, Nothing)] [badFqn]
-        expr' `shouldBe` expr
-
-      it "leaves a non-formation expression untouched" $ do
-        expr <- parseExpressionThrows "Q.x"
-        fqn <- parseExpressionThrows "Q.y"
-        let [(expr', _)] = F.exclude [(expr, Nothing)] [fqn]
-        expr' `shouldBe` expr
+      forM_
+        [ ("fails when the fqn is not a Q-dispatch chain", "[[ x -> ?, y -> ? ]]", "$.x")
+        , ("fails when the fqn is the whole program", "[[ x -> ?, y -> ? ]]", "Q")
+        , ("fails when nothing matches the fqn", "[[ x -> ? ]]", "Q.nope")
+        , ("fails when a nested fqn stops short of its last attribute", "[[ x -> [[ y -> ? ]] ]]", "Q.x.nope")
+        , ("fails for a non-formation expression", "Q.x", "Q.y")
+        , ("fails when the fqn walks into something that is not a formation", "[[ org -> [[ eolang -> Q.x ]] ]]", "Q.org.eolang.number")
+        ]
+        ( \(desc, phi, locator) ->
+            it desc $ do
+              expr <- parseExpressionThrows phi
+              fqn <- parseExpressionThrows locator
+              F.exclude [(expr, Nothing)] [fqn] `shouldThrow` anyException
+        )
 
       it "recurses over a multi-element rewrite list, preserving each rule label" $ do
         first' <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"
         second' <- parseExpressionThrows "[[ x -> ?, y -> ? ]]"
         fqn <- parseExpressionThrows "Q.x"
         expected <- parseExpressionThrows "[[ y -> ? ]]"
-        let excluded = F.exclude [(first', Just (Normalization, "rule-a")), (second', Just (Evaluation, "rule-b"))] [fqn]
+        excluded <- F.exclude [(first', Just (Normalization, "rule-a")), (second', Just (Evaluation, "rule-b"))] [fqn]
         map fst excluded `shouldBe` [expected, expected]
         map snd excluded `shouldBe` [Just (Normalization, "rule-a"), Just (Evaluation, "rule-b")]
 
diff --git a/test/Fixtures.hs b/test/Fixtures.hs
--- a/test/Fixtures.hs
+++ b/test/Fixtures.hs
@@ -30,6 +30,7 @@
 import Data.Aeson (FromJSON (parseJSON), withObject, (.:))
 import Data.ByteString qualified as BS
 import Data.Char (toLower)
+import Data.IORef (newIORef)
 import Data.List (isPrefixOf, stripPrefix)
 import Data.Map.Strict qualified as Map
 import Data.Maybe (fromMaybe)
@@ -50,8 +51,10 @@
 import System.IO (Handle, IOMode (ReadMode), hClose, hGetContents, hSetEncoding, openBinaryTempFile, utf8, withFile)
 import XMIR (defaultXmirContext)
 
-defaultReduceContext :: Expression -> ReduceContext
-defaultReduceContext loc = ReduceContext loc loc Nothing 25 25 (Steps 250 0) Nothing Nothing Nothing 1 False True False False 1 Nothing Morphing [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked
+defaultReduceContext :: Expression -> IO ReduceContext
+defaultReduceContext loc = do
+  minted <- newIORef 0
+  pure (ReduceContext loc loc Nothing 25 25 (Steps 250 0) Nothing minted Nothing Nothing 1 False True False False 1 Nothing Morphing [] Map.empty emptyLambdas (building linked) reduction evaluation fired dontSaveStep dontSaveEval linked)
 
 linked :: Engine
 linked = fromMaybe yaml compiled
@@ -117,6 +120,7 @@
         SWEET
         hidden
         Nothing
+        False
         MULTILINE
         2
         defaultXmirContext
diff --git a/test/FunctionsSpec.hs b/test/FunctionsSpec.hs
--- a/test/FunctionsSpec.hs
+++ b/test/FunctionsSpec.hs
@@ -187,6 +187,18 @@
         , [ArgExpression (DataNumber (numToBts 2)), ArgExpression (DataNumber (numToBts 3))]
         , \term -> expectExpression term (DataNumber (numToBts 5))
         )
+      ,
+        ( "sum keeps a single numeric argument as is"
+        , "sum"
+        , [ArgExpression (DataNumber (numToBts 7))]
+        , \term -> expectExpression term (DataNumber (numToBts 7))
+        )
+      ,
+        ( "sum of operands that cancel out is still zero"
+        , "sum"
+        , [ArgExpression (DataNumber (numToBts 4)), ArgExpression (DataNumber (numToBts (-4)))]
+        , \term -> expectExpression term (DataNumber (numToBts 0))
+        )
       ]
 
     failureCases :: [(String, String, [ExtraArgument], String)]
@@ -226,6 +238,7 @@
         , [ArgExpression (DataNumber (BtMany ["68", "65", "6C", "6C", "6F"]))]
         , "Expected 8 bytes for a number, got 5"
         )
+      , ("sum fails on an empty argument list", "sum", [], "sum() requires at least 1 argument")
       ,
         ( "an unsupported function name fails with a descriptive message"
         , "no-such-function"
diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs
--- a/test/LaTeXSpec.hs
+++ b/test/LaTeXSpec.hs
@@ -248,6 +248,17 @@
       explainRules [Y.Rule "rt" Nothing Nothing ptn ptn Nothing (Just [Y.Extra (Y.ArgAttribute (AtMeta "t1")) "random-tau" []]) Nothing]
         `shouldContain` "\\randomTau{"
 
+    it "escapes the name of the rule it refers to" $ do
+      step1 <- parseExpressionThrows "[[ x -> Q.y ]]"
+      step2 <- parseExpressionThrows "[[ x -> Q.z ]]"
+      latex <- rewrittensToLatex ([(step1, Nothing), (step2, Just (Normalization, "my_rule%1"))], False) defaultLatexContext
+      latex `shouldContain` "\\nameref{r:my\\char95{}rule\\char37{}1}"
+
+    it "escapes the name of the rule it explains" $ do
+      ptn <- parseExpressionThrows "Q.x"
+      explainRules [Y.Rule "my_rule%1" Nothing Nothing ptn ptn Nothing Nothing Nothing]
+        `shouldContain` "\\phinoNormalizationRule{my\\char95{}rule\\char37{}1}"
+
     it "prefixes each step with a '% === Step' header when '_headers' is set" $ do
       step1 <- parseExpressionThrows "[[ x -> Q.y ]]"
       step2 <- parseExpressionThrows "[[ x -> Q.z ]]"
diff --git a/test/MorphSpec.hs b/test/MorphSpec.hs
--- a/test/MorphSpec.hs
+++ b/test/MorphSpec.hs
@@ -44,7 +44,7 @@
 test' func useCases =
   forM_ useCases $ \(desc, input, expr, output) ->
     it desc $ do
-      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState (defaultReduceContext ExRoot)
+      ((res, _), _) <- func (input, (expr, Nothing) :| []) expr emptyState =<< defaultReduceContext ExRoot
       res `shouldBe` output
 
 data MorphPack = MorphPack
@@ -64,8 +64,9 @@
   expr <- parseExpressionThrows (if model == Just True then primitives input else input)
   seedTaus expr
   loc <- parseExpressionThrows (fromMaybe "Q" location)
+  base <- defaultReduceContext loc
   let ctx =
-        (defaultReduceContext loc)
+        base
           { _deep = deep
           , _partial = partial == Just True
           , _symbolic = if symbolic == Just True then known else emptyLambdas
@@ -90,7 +91,7 @@
 
     it "reports the chain of steps oldest first" $ do
       expr <- parseExpressionThrows "[[ D> 00- ]]"
-      (morphed, chain, _) <- morph expr emptyState (defaultReduceContext ExRoot)
+      (morphed, chain, _) <- morph expr emptyState =<< defaultReduceContext ExRoot
       morphed `shouldBe` expr
       map snd chain `shouldBe` [Just (Morphing, "mf"), Nothing]
       map fst chain `shouldBe` [expr, expr]
@@ -99,7 +100,8 @@
       expr <- parseExpressionThrows "[[ w -> [[ k -> [[ ]] ]].k, y -> Q.w ]]"
       loc <- parseExpressionThrows "Q.y"
       saved <- newIORef (0 :: Int)
-      _ <- morph expr emptyState (defaultReduceContext loc){_saveStep = const (modifyIORef' saved (+ 1))}
+      ctx <- defaultReduceContext loc
+      _ <- morph expr emptyState ctx{_saveStep = const (modifyIORef' saved (+ 1))}
       readIORef saved `shouldReturn` 2
 
   describe "morph with '_deep'" $ do
@@ -112,7 +114,8 @@
         withLambdasOf "- λ: L_answer\n  𝑛: ⟦ Δ ⤍ FF- ⟧\n" $ \file -> do
           box <- readLambdas file
           world <- parseExpressionThrows "[[ foo -> [[ f -> [[ a -> ?, @ -> $.a, L> L_answer ]] ]], x -> Q.foo.f( a -> [[ D> 01- ]] ).@ ]]"
-          (morphed, _, _) <- morph world emptyState (withLambdas box (defaultReduceContext ExRoot)){_deep = True}
+          ctx <- withLambdas box <$> defaultReduceContext ExRoot
+          (morphed, _, _) <- morph world emptyState ctx{_deep = True}
           morphed `shouldBe` world
 
   describe "morph'" $
@@ -157,27 +160,29 @@
   describe "inferred" $
     it "morphs a premise in the universe it names, not in the one the frame is in" $ do
       world <- parseExpressionThrows "[[ x -> [[ ]] ]]"
+      ctx <- defaultReduceContext ExRoot
       Just (Answered _ answer, _) <-
         inferred
           ExRoot
           ExRoot
           emptyState
-          (defaultReduceContext ExRoot)
+          ctx
           [direct (\_ _ -> [Morphs ExRoot world (pure . Concludes . Answered (Morphing, "premise"))])]
       answer `shouldBe` world
 
   describe "morph' fails when no morphing rule matches the term" $
     it "throws instead of looping when handed a bare, unmatched meta" $
-      morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)
+      (morph' (ExMeta "unbound", (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot)
         `shouldThrow` (\e -> "Morphing expects a normal form" `isInfixOf` show (e :: SomeException))
 
   describe "execBuildTerm 'morph'" $ do
     let univ = ExFormation []
-        ctx = defaultReduceContext ExRoot
-    it "throws when not given exactly one expression argument" $
+    it "throws when not given exactly one expression argument" $ do
+      ctx <- defaultReduceContext ExRoot
       execBuildTerm univ ctx "morph" [] substEmpty
         `shouldThrow` (\e -> "requires exactly 1 expression argument" `isInfixOf` show (e :: SomeException))
     it "morphs a single expression argument to its already-normal form" $ do
+      ctx <- defaultReduceContext ExRoot
       result <- execBuildTerm univ ctx "morph" [ArgExpression (ExFormation [BiDelta (BtOne "00")])] substEmpty
       case result of
         TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")]
@@ -188,7 +193,7 @@
         reduced src = do
           univ <- parseExpressionThrows universe
           target <- parseExpressionThrows src
-          (extended, ctx) <- insideUniverse target univ (defaultReduceContext ExRoot)
+          (extended, ctx) <- insideUniverse target univ =<< defaultReduceContext ExRoot
           (outcome, _, _) <- dataize extended emptyState ctx
           pure outcome
     it "reduces an expression the program does not contain" $ do
@@ -199,7 +204,7 @@
       value `shouldBe` Dataized (BtOne "01")
     it "refuses a universe which is not a formation" $ do
       target <- parseExpressionThrows "Q.y"
-      insideUniverse target ExRoot (defaultReduceContext ExRoot)
+      (insideUniverse target ExRoot =<< defaultReduceContext ExRoot)
         `shouldThrow` (\e -> "not a formation" `isInfixOf` show (e :: SomeException))
 
   describe "morphing is order-independent under --shuffle" $ do
@@ -217,11 +222,12 @@
           ]
     forM_ cases $ \(desc, input, univ, expected) ->
       it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do
-        results <- replicateM 100 (fst . fst <$> morph' (input, (univ, Nothing) :| []) univ emptyState (defaultReduceContext ExRoot))
+        results <- replicateM 100 (fst . fst <$> (morph' (input, (univ, Nothing) :| []) univ emptyState =<< defaultReduceContext ExRoot))
         nub results `shouldBe` [expected]
 
   describe "morphing 'md' is disjoint from 'ml'" $ do
-    let rctx = RuleContext (execBuildTerm ExRoot (defaultReduceContext ExRoot)) Nothing (_normal linked)
+    ctx <- runIO (defaultReduceContext ExRoot)
+    let rctx = RuleContext (execBuildTerm ExRoot ctx) Nothing (_normal linked)
         morphRule :: String -> Yaml.MorphRule
         morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules)
         asRule :: Yaml.MorphRule -> Yaml.Rule
@@ -236,19 +242,21 @@
     it "drills a chained λ-formation dispatch down to the base 'ml'" $ do
       let base = ExFormation [BiLambda (Function "F")]
           chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")
-      morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultReduceContext ExRoot)
+      (morph' (chain, (ExRoot, Nothing) :| []) ExRoot emptyState =<< defaultReduceContext ExRoot)
         `shouldThrow` (\e -> "No entry of --symbolic answers the λ function 'F'" `isInfixOf` show (e :: SomeException))
 
   describe "stops by the clock of --max-seconds" $ do
     it "fails a morphing that fires nothing once the deadline has passed" $ do
       expr <- parseExpressionThrows "[[ k -> [[ D> 3F- ]] ]]"
       deadline <- overdue 17
-      morph expr emptyState (defaultReduceContext ExRoot){_deadline = Just deadline}
+      ctx <- defaultReduceContext ExRoot
+      morph expr emptyState ctx{_deadline = Just deadline}
         `shouldThrow` (\e -> "--max-seconds=17" `isInfixOf` show (e :: SomeException))
     it "fails a partial morphing once the deadline has passed" $ do
       expr <- parseExpressionThrows "[[ q -> [[ D> 5A- ]] ]]"
       deadline <- overdue 23
-      morph expr emptyState (defaultReduceContext ExRoot){_deadline = Just deadline, _partial = True}
+      ctx <- defaultReduceContext ExRoot
+      morph expr emptyState ctx{_deadline = Just deadline, _partial = True}
         `shouldThrow` (\e -> "--max-seconds=23" `isInfixOf` show (e :: SomeException))
 
   describe "stops an entrance by the clock of --max-seconds" $
@@ -256,6 +264,7 @@
       due <- (+ 0.2) <$> getMonotonicTime
       let formation :: Expression -> Int -> Expression
           formation base depth = ExFormation [BiTau (AtLabel "x") (iterate (`ExDispatch` AtLabel "w") base !! depth), BiLambda (Function "L_q")]
-      ctx <- enter (formation ExRoot 1300) (defaultReduceContext ExRoot){_acyclic = Just Plausible, _deadline = Just (Deadline 31 due)}
+      base <- defaultReduceContext ExRoot
+      ctx <- enter (formation ExRoot 1300) base{_acyclic = Just Plausible, _deadline = Just (Deadline 31 due)}
       timeout 10000000 (enter (formation ExXi 1700) ctx)
         `shouldThrow` (\e -> "--max-seconds=31" `isInfixOf` show (e :: SomeException))
diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs
--- a/test/ParserSpec.hs
+++ b/test/ParserSpec.hs
@@ -413,6 +413,16 @@
     fromLeft "" (parseExpression "⟦\n  a ↦ ξ,\n  b ↦ ξ,\n  b ↦ Φ\n⟧\n\n\n")
       `shouldSatisfy` isInfixOf "expression:4:3:"
 
+  describe "an arrow ends an attribute name" $
+    forM_
+      [ ("⟦ a ↦ ξ.b(c↦ξ) ⟧", "⟦ a ↦ ξ.b(c ↦ ξ) ⟧")
+      , ("[[ a -> $.b(c->$) ]]", "[[ a -> $.b(c -> $) ]]")
+      , ("⟦ a ↦ ξ.as-bytes(x-y↦ξ) ⟧", "⟦ a ↦ ξ.as-bytes(x-y ↦ ξ) ⟧")
+      ]
+      ( \(tight, spaced) ->
+          it tight (parseExpression tight `shouldBe` parseExpression spaced)
+      )
+
   describe "parse number" $
     test
       parseNumber
@@ -433,6 +443,10 @@
       , ("1.5e2", Just (DataNumber (BtMany ["40", "62", "C0", "00", "00", "00", "00", "00"])))
       , ("2e-3", Just (DataNumber (BtMany ["3F", "60", "62", "4D", "D2", "F1", "A9", "FC"])))
       , ("-1e10", Just (DataNumber (BtMany ["C2", "02", "A0", "5F", "20", "00", "00", "00"])))
+      , ("1e18446744073709551617", Just (DataNumber (BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"])))
+      , ("-1e18446744073709551617", Just (DataNumber (BtMany ["FF", "F0", "00", "00", "00", "00", "00", "00"])))
+      , ("1e9223372036854775808", Just (DataNumber (BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"])))
+      , ("5e-18446744073709551615", Just (DataNumber (BtMany ["00", "00", "00", "00", "00", "00", "00", "00"])))
       , ("abc", Nothing)
       , ("", Nothing)
       ]
diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs
--- a/test/XMIRSpec.hs
+++ b/test/XMIRSpec.hs
@@ -304,6 +304,7 @@
       , ("keeps Δ data between sibling bindings", "[[ top -> [[ a -> [[]], D> 01-02, b -> [[]] ]] ]]")
       , ("keeps a bare 'Q' bound to a named attribute", "[[ x -> Q ]]")
       , ("keeps a formation bound to φ", "[[ k -> [[ @ -> [[ L> S8 ]] ]] ]]")
+      , ("keeps byte data and sibling bindings in an application argument", "[[ x -> Q.y(a -> [[ D> 01-02, b -> Q.z ]]) ]]")
       ]
       ( \(desc, source) -> it desc $ do
           expr <- parseExpressionThrows source
@@ -341,6 +342,11 @@
             expr <- parseExpressionThrows "[[ x -> [[ a -> ? ]](a -> Q.y) ]]"
             try (void (expressionToXMIR expr defaultXmirContext)) :: IO (Either SomeException ())
         , ["XMIR does not support such expression", "a ↦ Φ.y"]
+        )
+      ,
+        ( "names the attribute that is empty"
+        , try (void (parseXMIRThrows "<object><o name=\"a\" base=\"\"/></object>" >>= xmirToPhi)) :: IO (Either SomeException ())
+        , ["The attribute 'base' is not expected to be empty"]
         )
       ,
         ( "explains an unsupported binding"
diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs
--- a/test/YamlSpec.hs
+++ b/test/YamlSpec.hs
@@ -9,7 +9,7 @@
 import AST (Alpha, Attribute, Binding, Bytes, Expression (ExMeta, ExRoot))
 import Control.Exception (Exception (displayException), SomeException)
 import Control.Monad
-import Data.Either (isLeft)
+import Data.Either (isLeft, isRight)
 import Data.List (isInfixOf, nub, sort, (\\))
 import Data.Maybe (fromMaybe)
 import Data.Text qualified as T
@@ -85,6 +85,20 @@
   it "rejects a 'where' step whose meta is not a meta" $
     (decodeYaml' "name: nometa\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ x ↦ 𝑒1 ⟧'\nwhere:\n  - meta: 'z'\n    function: concat\n    args: ['\"a\"']" :: Either Yaml.ParseException Rule)
       `shouldSatisfy` failsWith "whose 'meta' is not a meta"
+
+  describe "rejects a meta that nothing binds" $
+    forM_
+      [ ("in 'when'", "name: w\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ y ↦ 𝑒1 ⟧'\nwhen:\n  not:\n    eq: ['𝑒9', '𝑒1']", "'e9'")
+      , ("in 'result'", "name: r\npattern: '⟦ x ↦ 𝑒1, 𝐵1 ⟧'\nresult: '⟦ y ↦ 𝑒9, 𝐵1 ⟧'", "'e9'")
+      , ("in a 'where' argument", "name: a\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ x ↦ 𝑒2 ⟧'\nwhere:\n  - meta: '𝑒2'\n    function: concat\n    args: ['𝑒7']", "'e7'")
+      ]
+      ( \(desc, yaml, meta) ->
+          it desc ((decodeYaml' yaml :: Either Yaml.ParseException Rule) `shouldSatisfy` failsWith ("reads the meta " ++ meta))
+      )
+
+  it "accepts a meta that an earlier 'where' step binds" $
+    (decodeYaml' "name: ok\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ x ↦ 𝑒3 ⟧'\nwhere:\n  - meta: '𝑒2'\n    function: concat\n    args: ['𝑒1']\n  - meta: '𝑒3'\n    function: concat\n    args: ['𝑒2']" :: Either Yaml.ParseException Rule)
+      `shouldSatisfy` isRight
 
   it "rejects an 'e-match' in a rewriting rule" $
     (decodeYaml' "name: kvz\npattern: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\ne-match: '𝑒2'\nresult: '𝑒2'" :: Either Yaml.ParseException Rule)