diff --git a/docs/chl-spec.md b/docs/chl-spec.md
index 08272bc8..8f905ece 100644
--- a/docs/chl-spec.md
+++ b/docs/chl-spec.md
@@ -1111,7 +1111,7 @@ A CHL **program** is its top-level block (§2.1): a sequence of
 statements. Each non-terminal statement either introduces a binding
 visible to the remainder of the block, or performs an effect (a feed
 into a deferred output). The block's *value* is the value of its final
-expression statement; if the program mutable variables any sinks (e.g.
+expression statement; if the program registers any sinks (e.g.
 `http_serve`), the program value is implicitly a record of those sinks
 instead.
 
@@ -2572,10 +2572,12 @@ around `reserve` + `quote` + the feed).
 - **Trailing induction read** — after a `for` loop, a bare reference to an
   induction accumulator is its final value (or the pre-loop value if the
   source was empty). The loop has ended, so "latest" is unambiguous.
-- **A `Txn` mutable variable is read only inside a `with begin():` block.** A bare
-  read outside one is an error. Reading inside a block pins a
-  **snapshot-consistent** view: several mutable variable reads in one block see
-  one commit snapshot — the reason the block is required.
+- **A `Txn` mutable variable is read only inside a `with begin():` block
+  [Decided].** A bare read outside one is an error, and stays one: the block is
+  what pins a **snapshot-consistent** view, so that several mutable variable
+  reads in one block see one commit snapshot. A read that wants no snapshot has
+  the two terms below instead — an as-of read fed out of a block, or
+  `await_final`.
 - **As-of read.** A mutable variable read fed *out* of a block that does not
   itself write that mutable variable is an **as-of read at an arbitrary commit
   position** — the mutable variable's value as of wherever the reading transaction
diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs
index 765b602b..5c0994ef 100644
--- a/src/ccl/ccl_utils.rs
+++ b/src/ccl/ccl_utils.rs
@@ -991,7 +991,7 @@ pub fn free_names_in_value(expr: &Expr) -> HashSet<Name> {
                     out.insert(n.clone());
                 }
             }
-            // A key label names a field of the mutable variable record the node denotes, not a
+            // A key label names a field of the history record the node denotes, not a
             // variable use — the same exclusion `count_free_in_value` makes.
             ScopedItem::KeyRef(_) => {}
             ScopedItem::Child { expr, binders } => {
diff --git a/src/ccl/channelize.rs b/src/ccl/channelize.rs
index e57b766b..4d776a3b 100644
--- a/src/ccl/channelize.rs
+++ b/src/ccl/channelize.rs
@@ -2107,7 +2107,7 @@ fn extract_for_defer_impl(
                 // is bound (a generator body inlined out) needs it carried
                 // along; a channel that doesn't mention it must *not* be
                 // wrapped, or every channel drags in an unused binding — a whole
-                // mutable variable record, in the worst case (each `http_serve` reply re-emitting
+                // history record, in the worst case (each `http_serve` reply re-emitting
                 // a mutable variable it never reads). The reference test is
                 // `collect_free_vars` rather than `count_free` because the
                 // binding may be referenced only through a `user_annotation` /
diff --git a/src/ccl/context.rs b/src/ccl/context.rs
index f32d1b5f..a7bca64d 100644
--- a/src/ccl/context.rs
+++ b/src/ccl/context.rs
@@ -948,8 +948,8 @@ pub fn compile_program(
     // inlining (so cross-function writers land at their call sites) and
     // *before* channelize, so a per-iteration feed inside a loop is
     // hoisted to an ordinary feed of the loop's history for desugar to route.
-    // The tree still carries Defer/Feed here, so the walls are the relaxed
-    // pre-desugar check.
+    // The tree still carries Defer/Feed here, so the check is the relaxed
+    // pre-desugar one.
     let phase_out = mut_elim::run(expr);
     debug!("Letrec phase CCL:\n{}", symbolic(&phase_out));
     check_pre_desugar(&phase_out).expect("letrec phase produced an inconsistent tree");
diff --git a/src/ccl/design/ir.md b/src/ccl/design/ir.md
index 9672a2f5..1d58bc3d 100644
--- a/src/ccl/design/ir.md
+++ b/src/ccl/design/ir.md
@@ -61,7 +61,7 @@ The rules themselves:
 - `For` — `target` scopes over `body`; `iter` is outside.
 - `Case` — each branch's `pattern.binding` scopes over that branch's `guard` and `body`, and nothing else.
 - `Feed` / `Define` / `MutWrite` — the `name` field is a *use* of the binder it names, not a binder.
-- `Transact` — introduces no binder; its keys are labels of the mutable variable record the node denotes, so they are surfaced as a distinct occurrence kind that free-*variable* analyses skip while an identity-sensitive consumer still folds them in.
+- `Transact` — introduces no binder; its keys are labels of the history record the node denotes, so they are surfaced as a distinct occurrence kind that free-*variable* analyses skip while an identity-sensitive consumer still folds them in.
 
 Every `match` that decides one of these rules is exhaustive with **no wildcard arm**, deliberately: before this existed, the walkers ended in `_ => walk_children(..)`, so a new binding form compiled clean in all of them and silently got the wrong scope in every one. Now it is a compile error until the new form declares its scope. That covers three matches, each closing the same failure mode at a different layer:
 
@@ -141,7 +141,7 @@ Op-conversion accordingly compiles a fed union as a flat merge — a disjoint jo
 
 CHL mutation-accumulation `for` loops **and** `with begin():` transactions share one carrier node, `Transact`, rather than recursive `Lambda`/`Let` combinations or a dedicated fold node. (For the lowering mechanics and the operator-graph realization, see [lowering.md](lowering.md#mutation-accumulation-loops) and [mutability.md](mutability.md).)
 
-`Transact { keys, writers, domain }` denotes a **transactional mutable variable**: a set of scalar-variable `keys` sharing one sequencing `domain`, driven by concurrent `writers` that read the shared mutable variables and propose per-position writes. It denotes a *pure value* — the mutable variable record `{key: Fun(domain, V)}`, each field a key's history — so a variable read is the projection `__reg.key`; the mutable variable↔writer cycle is the operator's runtime behaviour, not the node's denotation (exactly as the induction/commit store realizes a recurrence). Each key carries its position-0 `init` (evaluated once outside every writer's parameter scope); an induction-domain carrier has exactly one writer (a `mut` loop, whose footprint is all its accumulators).
+`Transact { keys, writers, domain }` denotes a **transactional mutable variable**: a set of scalar-variable `keys` sharing one sequencing `domain`, driven by concurrent `writers` that read the shared mutable variables and propose per-position writes. It denotes a *pure value* — the history record `{key: Fun(domain, V)}`, each field a key's history — so a variable read is the projection `__hist.key`; the mutable variable↔writer cycle is the operator's runtime behaviour, not the node's denotation (exactly as the induction/commit store realizes a recurrence). Each key carries its position-0 `init` (evaluated once outside every writer's parameter scope); an induction-domain carrier has exactly one writer (a `mut` loop, whose footprint is all its accumulators).
 
 `Transact` is **born in `planning::plan_loops`** (from the causal `LetRec` the mutability phase emits — see below) and consumed at operator conversion, which **dispatches on `domain`**: a concrete iteration domain → the position-driven `InductionStore` changelog (the induction case — one always-commit or commit-gated writer, whose footprint is all its accumulators); `Type::Txn` → the concurrent commit operator (the transactional slice — multiple writers, serialize + retry). Loop planning runs **after `lambda_elim`**, on the group's point-free normal form — it anchors on the causal accessors (`get_prev_seq` / `get_prev_txn` / `begin_<site>`), which survive elimination, so one `LetRec` travels from the mutability phase through `channelize` and `lambda_elim` and is planned point-free; `Transact` is then loop planning's *output* carrier from there to op-conversion (op-conversion is lambda-free, and planning stages the carrier's writer sources). There is no `Jump` node: `while` loops with explicit restart/break are future work.
 
diff --git a/src/ccl/design/mutability.md b/src/ccl/design/mutability.md
index aaade6b9..36e38191 100644
--- a/src/ccl/design/mutability.md
+++ b/src/ccl/design/mutability.md
@@ -8,13 +8,13 @@ feeds one idea, the surface syntax, and how the compiler realizes them.
 
 ## The idea in one line
 
-A mutable variable **is** a function from a **sequencing domain** (a time axis) to a value.
+A mutable variable is a function from a **sequencing domain** (a time axis) to a value.
 "Mutation" is the incremental revelation of that function's values as the domain advances;
 "reading the variable" is looking up a value at a position. Sequential rebinding, loop
-accumulation, and concurrent transactions are then *one* model over three domains, not three
+accumulation, and concurrent transactions are then one model over three domains, not three
 mechanisms.
 
-A **feed** (a reply or yield, written `<<`) is the *same* object — a function over the same
+A **feed** (a reply or yield, written `<<`) is the same object — a function over the same
 kind of domain — and is therefore **the second form of mutability**, not a separate concept:
 `o << e` is surface-impure exactly as `x := e` is (action-at-a-distance on a channel bound
 elsewhere; both break referential transparency). The two forms differ only in their
@@ -79,10 +79,10 @@ the failure `:=` exists to make impossible.
 The structural difference between the two causal accessors mirrors a difference between the two
 kinds of variable:
 
-- An **induction variable** has exactly one writer (its loop), and its domain *is* that writer's
+- An **induction variable** has exactly one writer (its loop), and its domain is that writer's
   domain. Its history binding is directly the recurrence:
   `cnt = λ 𝑟 → get_prev_seq(cnt, 𝑟, init) + 1`.
-- A **transactional variable**'s domain (`Txn`) is *not* any writer's domain — writers iterate
+- A **transactional variable**'s domain (`Txn`) is no writer's domain — writers iterate
   request streams, and an oracle assigns each transaction a commit time. So its history is defined
   *indirectly*, through **commit records**: each writing site produces one `{time, write}` record
   per iteration, and the variable's history searches those records by time. The commit-time oracle
@@ -118,7 +118,7 @@ about to constrain is a handle position.
   off the head of the spine — and lowering resolves the operand by name as it does a write
   target, so the mention never becomes a value position at all.
 
-A lambda's result is deliberately *not* dereffed: that is where rule 2 catches a function
+A lambda's result is not dereffed, which is where rule 2 catches a function
 returning a `Mut`, and dereffing would silently accept the escape by turning it into a
 read.
 
@@ -128,8 +128,8 @@ introduction's body** report their continuation's *value* — they emit it as a
 operand — so a program ending in a read of its accumulator has that accumulator's value
 rather than a handle. Their coalesce-time lifted type derefs for the same reason
 (`solve.rs`): a lift that copied the continuation's type verbatim would re-stamp the node
-with the handle the read just looked through, leaving the node's recorded type
-contradicting the rule that typed it. A **`Let` body** is the one tail that does *not*
+with the handle the read looked through, leaving the node's recorded type
+contradicting the rule that typed it. A **`Let` body** is the one tail that does not
 deref: a `Let` owns nothing — it cannot even bind a mutable variable — so it reports whatever its
 body reports, handle included, which is what leaves rule 2 an escape to catch. The same
 deref would hide an escape one line away from the boundary: reading the
@@ -174,7 +174,7 @@ Two surface facts are load-bearing for the realization and worth restating here:
   [as-of-read rewrite](#replies-live-cross-endpoint-reads-and-commit-ordered-taps) and the
   [`AsOf` engine](#the-runtime-engines) below.
 
-> **Design commitment — transactional mutability is deliberately *unordered*.** There is no
+> **Design commitment — transactional mutability is unordered.** There is no
 > ordering guarantee between transactions on the same `Txn` variable beyond the existence of *a*
 > commit order the runtime picks; a program may not assume one transaction serializes before
 > another, and nothing in the compiler or engine should impose such an order. The arbitrary-position
@@ -198,8 +198,8 @@ these markers; `mut_elim` + `channelize` rewrite it into **pure CCL** — the ma
 the rest of the pipeline runs on. This is the concrete input→output contract of the mutability
 eliminator, stated by content rather than by a "mirrors CHL" adjective.)
 
-- `For { target, iter, body }` — **every** statement `for` loop, generator / side-effecting /
-  mutation alike (comprehensions keep their expression lowering). Lowering does *not* distinguish
+- `For { target, iter, body }` — every statement `for` loop, generator / side-effecting /
+  mutation alike (comprehensions keep their expression lowering). Lowering does not distinguish
   the loop kinds — that classification is the phase's, post-inference (see
   [Mutability is the type](#mutability-is-the-type-no-lowering-registry)). Value `Unit`;
   `iter : 𝐼 ⇒ 𝑇`, `target : 𝑇` bound in `body`.
@@ -207,13 +207,13 @@ eliminator, stated by content rather than by a "mirrors CHL" adjective.)
   binding `x` as a mutable variable over `body`. The declaring half of `:=`, paired with
   `MutWrite` for its writing half; before it existed the introduction was a `Let`
   carrying a `Mut` annotation, and every pass that had to recognize one consulted
-  that annotation as a proxy for the declaration. It is the **only** node that binds
+  that annotation as a proxy for the declaration. It is the only node that binds
   a mutable variable (a pass-by-reference `Mut` parameter aside), which is what makes
   "is this binder mutable?" a question about the node rather than about a type that
   happened to survive inference.
-- `MutWrite { name, value }` — one write to a variable. Value `Unit`. Its target **must** be
+- `MutWrite { name, value }` — one write to a variable. Value `Unit`. Its target must be
   `Mut`-typed: inference peels the target's `Mut(𝑉, 𝐷)` and requires `value ⊑ 𝑉`; a write whose
-  target is *not* `Mut` is a **type error**, never a shadowing rebind (`x += e` on a plain `x` is
+  target is not `Mut` is a **type error**, never a shadowing rebind (`x += e` on a plain `x` is
   rejected, not silently turned into `x = x + e`). `x += e` lowers to `MutWrite(x, x + e)`, the
   embedded read being the in-context read.
 - `Begin { body }` — one `with begin():` transaction block, made a *single* `Unit`-valued statement
@@ -232,7 +232,7 @@ residue, and planning/op-conversion never see them.
 
 ### Mutability is the type (no lowering registry)
 
-Whether a name denotes a mutable variable is carried **only** by the mutable-variable type
+Whether a name denotes a mutable variable is carried by the mutable-variable type alone
 `Type::History { kind: Overwrite }` (displayed `Mut(𝑉, 𝐷)`), and is therefore known
 only after inference. Lowering never tracks it — there is no lowering-side mutable-variable registry. This is
 what keeps lowering a pure representation change: it emits the markers above by *shape and scope
@@ -240,9 +240,9 @@ alone*, and every decision that needs mutability happens later, keyed on the typ
 
 Lowering's two choices, both scope-only:
 
-- **Introduction vs. write.** `x := e` where `x` is *not* in scope is an introduction — a
+- **Introduction vs. write.** `x := e` where `x` is out of scope is an introduction — a
   `let x = e` whose binding is stamped `Mut(𝑉, 𝐷)` (`𝐷 = Txn` iff annotated `Mut(𝑉, Txn)`, else a
-  `Hole` the phase resolves). `x := e` / `x += e` where `x` *is* in scope is a write — a bare
+  `Hole` the phase resolves). `x := e` / `x += e` where `x` is in scope is a write — a bare
   `MutWrite(x, e)`. The choice is membership in the ambient scope set (which lowering already
   threads for other reasons); it consults no mutability record.
 - **Loop shape.** Every `for` becomes a `For` marker (above). Lowering does not decide
@@ -267,7 +267,7 @@ Everything mutability-dependent is then a post-inference decision on the `Type::
 
 The payoff: lowering has one loop path and one write path, no `is_mutable`/`with_shadowed`
 book-keeping, and no base-name scoping scaffolding — a shadowing parameter spelled like an outer
-mutable variable is just a different binding with its own (non-`Mut`) type, handled by ordinary inference.
+mutable variable is a different binding with its own (non-`Mut`) type, handled by ordinary inference.
 
 ### `Mut` is a CCL type
 
@@ -297,7 +297,7 @@ Typing:
 - **Reads deref at the rule that emits them**: `cnt + 1`, `f(cnt)` for an `Int` parameter, and a
   trailing `cnt` all read, and each reads because the rule typing that position asks for a value
   operand (`emit::emit_value_read`). Only a position that *expects* `Mut` — a pass-by-reference
-  argument, a write's target — receives the handle. `Mut(𝑉) <: 𝑉` is deliberately not a subtyping
+  argument, a write's target — receives the handle. `Mut(𝑉) <: 𝑉` is not a subtyping
   fact; see [A mutable variable read is an explicit operation](#a-mutable-variable-read-is-an-explicit-operation)
   for why putting it in the relation could not distinguish a read from a handle passed along.
   After inlining, no `Mut`-expecting positions remain, so the phase's rewrite is purely structural
@@ -333,7 +333,7 @@ introduction every write targets. The discipline:
 3. A plain `=` off a mutable **reads** it: `b = a` binds `b` at `a`'s value — a
    snapshot, exactly as any other value position reads a mutable variable. This is not a
    rule but a consequence: `emit_let` reads through an initializer that is a mutable variable, so a
-   `Let` *cannot* bind a register and the alias is unrepresentable rather than
+   `Let` cannot bind a mutable variable, so the alias is unrepresentable rather than
    rejected. Writing through the copy (`b += 1`) is then the ordinary
    write-to-a-non-mutable error, which blames the write instead of the binding.
    The only mutable variable binders are `MutDecl` (a `:=` introduction) and a
@@ -343,7 +343,7 @@ introduction every write targets. The discipline:
 One structural check after inference enforces the two rules. The real fault line is the **merge law**,
 not `Feed`-vs-`Mut`. *Append-only* mutability merges commutatively — a feed by `++`, and (at
 runtime) a `Txn` mutable variable by the commit operator's timestamped merge — so multiple writers are
-already the semantics and aliasing is benign; that is why `Feed` deliberately stays first-class (it
+already the semantics and aliasing is benign; that is why `Feed` stays first-class (it
 is returned in `http_serve`'s tuple). *Last-write-wins* mutability instead needs a **resolvable
 writer set** — but that requirement is fundamental only for an **induction** accumulator, which
 compiles to a single-writer `InductionStore` changelog. A `Txn` mutable variable already tolerates an open writer set (its
@@ -399,7 +399,7 @@ commit record for time `𝑡`). Every cycle must contain a causal edge — equiv
 non-causal-reference subgraph is acyclic. A structural check enforces this; op-conversion treats an
 unrecognized non-causal cycle as a compile error rather than attempting fixpoint iteration.
 
-`LetRec` is deliberately more general than mutability needs: `while` loops (recursion over a
+`LetRec` is more general than mutability needs: `while` loops (recursion over a
 condition-bounded prefix of `Nat`), recursively-defined collections, and general structural
 recursion all target the same node.
 
@@ -439,7 +439,7 @@ A decision is a **choice**, and the two things it chooses between carry differen
 carries a write set, a denial carries nothing. Today that is encoded as a record with a `commit:
 Bool` beside a `writes` field that is meaningless when `commit` is false — a product standing in for
 a sum, so nothing stops a reader consulting `writes` on a denied decision. The direction is the sum
-itself, `` `commit(writes) `` / `` `abort(unit) ``, which makes the write set reachable *only* on the
+itself, `` `commit(writes) `` / `` `abort(unit) ``, which makes the write set reachable on the
 granting path.
 
 What exists today is the algebra that shape needs, in both directions:
@@ -464,7 +464,7 @@ are, so the mutable variable's value space is their **join**: a `` `none `` seed
 the two-tag sum `` {`none | `some{Int}} `` with the arm that did not occur left empty, and every
 emission is built at that declared space rather than at the width of whichever alternative occurred.
 ``acc := `some(𝑖)`` under a `` `none `` seed, and a conditional write choosing between tags, are both
-just that.
+instances of it.
 
 ## Compilation pipeline
 
@@ -482,7 +482,7 @@ CHL source
                         by substitution; eliminates Feed / Defer)
   → as-of-read rewrite (bare history reads fed out of read-only blocks → AsOf)
   → lambda_elim        (the LetRec travels through — bodies point-freed, group intact)
-  → typecheck          (strict wall)
+  → typecheck          (strict, no relaxations)
   → plan_loops         (planning/loops.rs: point-free letrec patterns → the Transact carrier;
                         causality re-checked by the point-free matcher)
   → planning           (stages the carrier's writer sources) → simplify
@@ -504,7 +504,7 @@ and `plan_loops` splits scaffold from body structurally, lifting the body
 **verbatim**. The `Transact` carrier is born at loop planning and spans only
 `plan_loops` → planning → op-conversion.
 
-Inlining runs **before** `mut_elim`: a UDF that writes a `Mut` parameter or feeds a `Feed` parameter
+Inlining runs before `mut_elim`: a UDF that writes a `Mut` parameter or feeds a `Feed` parameter
 is beta-reduced to its call site, where `mut_elim` sees its writes and feeds in the scope of the
 mutable variables and channels they target. Generators survive inlining because surface-CCL lowering
 leaves nothing to lose — a generator body is `For` + `Feed` nodes against an implicit result feed,
@@ -703,11 +703,11 @@ Reading it off:
   indexed by the GET request loop. This is the **same store-level-timestamp mechanism** the `AsOf`
   sections describe as "a sample at an arbitrary observation-time position": the read takes a timestamp
   at its observation point and returns the committed prefix as of that time — described uniformly here
-  and there, not as rival semantics. `read_at_get` is deliberately *not* a `begin_<site>` oracle: a
+  and there, not as rival semantics. `read_at_get` is not a `begin_<site>` oracle: a
   read-only block mints none — it commits nothing, produces no `{time, write}` record, and takes no
   commit slot (`begin_<site>`/`BeginTxn` is the *writer* oracle only). It is pure composition, no
   commit record, no write set. **External consistency** is a real property of this same mechanism (not
-  a competing guarantee): a GET issued *after* a POST's `ok`-reply lands at an observation time ≥ that
+  a competing guarantee): a GET issued once a POST's `ok`-reply has landed reads at an observation time ≥ that
   POST's commit (arrival-order monotonicity), so a client that sees `ok 2` then GETs observes `≥ 2`;
   a read with no such causal ordering samples an *arbitrary* position among concurrent commits — which
   is all the "arbitrary as-of" of the `AsOf` sections means.
@@ -734,12 +734,9 @@ this section states how the letrec model *delivers* them.
   rejects — see the caveat there); only `Txn`-domain variables participate in the atomic commit. A
   program that needs the counter transactionally consistent with the mutable variable declares it
   `Mut(Int, Txn)`.
-- **Liveness.** Induction domains are finite or stream-complete; `Txn` histories complete when all
-  writer sources do. A fed-out `Txn` mutable variable read reads as-of its own position in the commit
-  clock and does not wait for completeness. The one term that waits for a mutable variable's
-  completeness is [`await_final`](#await_final), and it is well-defined because it closes the writer
-  set: the mutable variable is unreferenceable afterward, so no later writer can extend the history it
-  just declared complete.
+- **Liveness.** Induction domains are finite or stream-complete; a `Txn` history completes when the
+  writers of its key do. Only [`await_final`](#await_final) waits for that completion; every other
+  read is an as-of sample.
 
 ## Ordering and concurrency
 
@@ -754,7 +751,7 @@ remain open in the model.
 is why dispatch on the sequencing domain is load-bearing (not an optimization):
 
 - **Induction (`InductionStore`)** reads position `𝑖-1`, so it is a *strict total-order data-dependence
-  chain*: necessarily sequential, independent iterations **not** reordered.
+  chain*: necessarily sequential, with independent iterations left in order.
 - **`Txn` (commit operator)** has a *serial denotation* (a total commit order, each transaction reading
   the prefix strictly before its time) but a *concurrent engine* (optimistic concurrency), correct iff
   observationally equivalent to that denotation. Disjoint footprints commit concurrently.
@@ -808,12 +805,12 @@ causal matcher (`letrec::check_letrec_causal`).
 - **The commit operator** — the concurrent generalization of the induction accumulator, for the `Txn` domain. The
   store is an MVCC commit log `Txn ⇀ (Key ⇀ Value)`. A writer reads a snapshot of its footprint,
   runs its pure body, and proposes `{reads, writes}`; the operator validates the read set against
-  the current store (backward / optimistic concurrency) *before* allocating a timestamp — a valid
+  the current store (backward / optimistic concurrency) ahead of allocating a timestamp — a valid
   proposal commits and consumes a tick, a stale one is skipped and retries against the advanced
   snapshot. Disjoint footprints commit concurrently; overlapping ones serialize. `release` is the
   commit acknowledgment (the retry signal rides the existing producer/consumer channel). The store
   compacts by the MVCC law and GCs the released prefix.
-- **`AsOf`** — the as-of (temporal) join: **every** fed-out `Txn` mutable variable read, regardless of the
+- **`AsOf`** — the as-of (temporal) join: every fed-out `Txn` mutable variable read, regardless of the
   reading loop's domain. Given a *trigger* (the reading loop — the positions to sample at) and a
   *source* (the store), it latches, for each trigger position, the store's value as of the moment
   that position is first observed. The output is indexed by the **trigger** (the outer reading loop),
@@ -842,15 +839,15 @@ Dispatch on the sequencing domain is load-bearing, not an optimization.
 
 A consumer reading "as of `𝑡`" must know no further commits will land at `≤ 𝑡`. The runtime already
 carries this: function tiles hold a `domain_predicate` marking the complete region of the domain. A
-watermark *is* a `domain_predicate` advancing over `Txn`. Conflict validation — which depends on
-which value combinations were observed — is deliberately engine-level, above the tiling algebra,
+watermark is a `domain_predicate` advancing over `Txn`. Conflict validation — which depends on
+which value combinations were observed — is engine-level, above the tiling algebra,
 because that is exactly what domain predicates cannot express.
 
 ## Concurrency and distribution
 
 The transactional case is the concurrent sequencing domain, and most of it falls out of the
 algebra: out-of-order commits are fine (`⊕` is commutative; writes at distinct timestamps are
-compatible tiles), and watermarks are `domain_predicate`s over `Txn`. What is *not* in the algebra
+compatible tiles), and watermarks are `domain_predicate`s over `Txn`. What the algebra lacks
 is conflict validation (read-set dependence), which is the engine's job. The design generalizes to
 distributed execution with no model change: the compiler knows the full set of writes a transaction
 *could* perform, so distributed commit can be decided from complete local knowledge rather than a
@@ -864,7 +861,7 @@ affordable by that complete compile-time knowledge.
 - **Nested `for` loops** — lexicographic product domains; data-dependent bounds meet the
   refinement-types work as dependent sums.
 - **Mutable collections** — sigma types (`List[𝑇] = Σ 𝐼 . 𝐼 ⤇ 𝑇`) as letrec bindings; the
-  append-only `Appendable` case first, as a commit stream whose history *is* the collection. This
+  append-only `Appendable` case first, as a commit stream whose history is the collection. This
   is also what first-class `Mut` (returning or storing references) needs: carrying mutable variable identity in
   types is a sigma/index-types question. Until then the second-class discipline is the aliasing
   firewall.
@@ -933,7 +930,7 @@ standalone read), which demand-drives this convergence: each committed reply pul
 advances the sibling loop, exactly as an in-block reply drives the writer in the co-indexed case. The
 co-indexed and non-cross paths are untouched.
 
-(Note the asymmetry: the broadcast **source** — the sibling induction loop's accumulator — *does*
+(The asymmetry: the broadcast **source** — the sibling induction loop's accumulator — does
 have a final, read via `ExtractFinal`, because an induction loop terminates and its final value is
 denotable. The result **mutable variable** does not: a `Txn` mutable variable has no final-value term, so reads of it
 are `AsOf`, never `ExtractFinal`.)
@@ -1101,7 +1098,7 @@ guard-rejected position. See `../../interpreter/design-operators.md`.
 
 Both a **finite** loop and an **async** (streaming) source drive an induction accumulator — the
 model treats a finite domain as a stream that terminates (§Liveness) — and every induction accumulator
-uses *one* realization: the changelog `InductionStore`. Plain, conditional, and feed-carrying loops
+uses one realization: the changelog `InductionStore`. Plain, conditional, and feed-carrying loops
 over finite or async extents all route through it. The
 drive reads its source by absolute domain position (async domains arrive unordered), reclaims the
 consumed prefix as it advances, and carries reply feeds as `__fire`-gated taps — see *Induction
@@ -1173,7 +1170,7 @@ mutually exclusive and, taken together with the implicit empty arm of a guard th
 exhaustive: exactly one path runs per transaction.
 
 Paths are a *compile-time* enumeration, not a runtime branch: the walk visits every path and emits
-**one** decision variant, whose `` `commit ``/`` `abort `` tag and per-tap fire fields are path conditions
+one decision variant, whose `` `commit ``/`` `abort `` tag and per-tap fire fields are path conditions
 and whose per-key writes are `Case`s over the local branch guards — so every path is evaluated in
 one straight-line writer body and one transaction is still one decision. Walking a block threads
 `(path, env)` (read-your-writes) and the block denotes
@@ -1208,7 +1205,7 @@ transaction appends the tap only where its fire gate holds. A single-guard feed
 path == commit) and a spine feed omit the field and fire with their transaction — so unconditional
 programs keep their fire-field-free shape.
 
-A write key written *only* conditionally (an absolute `k := 𝑒` inside a `Case` arm, never read) is
+A write key written conditionally and never read (an absolute `k := 𝑒` inside a `Case` arm) is
 finalized into the *read* set by `collect_footprint`, so it has a snapshot to **carry** on the paths
 its arm does not fire; a read-modify-write already reads the key, and a purely spine (unconditional)
 write needs no carry and stays write-only.
@@ -1267,22 +1264,23 @@ zero-or-one times.
 
 **Why this is sound where per-path writer sites *inside* one block are not** (contrast the "one
 decision record per transaction" verdict above): the guard `𝑝` is a **source-domain** predicate —
-evaluated on the request element *before* the transaction, not on its snapshot — so it may
+evaluated on the request element ahead of the transaction, not on its snapshot — so it may
 legitimately restrict the source; each branch's block is a **distinct transaction** with its own
 `begin_<site>`, so distinct serialization points are correct rather than a violation; and atomicity
 is intact — still one snapshot, one commit, one write-set per transaction. The whole difference is
 "two transactions" vs. "one transaction, two paths".
 
-**Footgun — a variable-reading guard is not an atomic check.** These are *not* equivalent:
+**A guard reading the variable is rejected, so the non-atomic check is unwritable.** Of these two,
+only (B) is a program:
 
 ```text
-if balance > 0: with begin(): balance -= req      # (A) non-atomic pre-check
+if balance > 0: with begin(): balance -= req      # (A) rejected: `balance` is read outside a block
 with begin(): if balance > 0: balance -= req       # (B) atomic — checked in the snapshot
 ```
 
-In (A) `balance > 0` is a **live/as-of read outside the transaction** — a TOCTOU pre-check that can
-go stale between the read and the commit. It is faithfully compilable (the guard becomes a gating
-as-of read deciding whether the transaction fires), but it is not an atomic guard, and a user who
-wrote (A) most likely meant (B), the in-block deny guard. This form should at least be documented,
-ideally linted (a variable-reading guard on a conditional transaction) with a pointer at (B).
+(A) would be a TOCTOU pre-check, stale between the read and the commit. It does not compile, and not
+because conditional transactions are unbuilt: a `Txn` variable is read only inside a `with begin():`
+block, permanently (the CHL spec, [reads](../../../docs/chl-spec.md#83-reads)), so the guard is
+rejected at lowering whatever becomes of the conditional around it. That leaves (B) as the only way
+to write the check, which is the atomic one, so there is no footgun here to lint.
 
diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md
index 37d5b6f5..04da23b1 100644
--- a/src/ccl/design/type-inference.md
+++ b/src/ccl/design/type-inference.md
@@ -318,7 +318,7 @@ the re-entrant clone walk truncates the scope stack, which a depth cannot surviv
 **Deadness is the absence of a demand, not of a specialization.** The two come apart
 in both directions — a use whose instantiation fails to resolve reports and returns
 before minting anything, and a use inside a discarded subtree deliberately does not
-mutable variable — so `specs.is_empty()` cannot decide this. `SpecializeFrame::demanded`,
+register — so `specs.is_empty()` cannot decide this. `SpecializeFrame::demanded`,
 set on entry to `specialize_use`, is what does. Reading the memo instead re-walks the
 definition of a binding whose uses merely *failed*, which reports that body's conflict
 a second time from its own nodes: one defect, four diagnostics.
@@ -335,9 +335,9 @@ nothing calls — so the specialization blowup documented under
 `SpecializeFrame::specs`, "The remaining gap" (one clone per distinct argument
 tuple, compounding through a call chain) is now reachable from code no one calls,
 where before dead code cost nothing. Two things keep that bounded rather than
-multiplied. A use inside the discarded subtree still *mutable variables* its
+multiplied. A use inside the discarded subtree still *registers* its
 specialization, so the memo shares clones exactly as a live use does — declining to
-mutable variable instead made every dead use re-clone its callee, which measured ~5× the
+register instead made every dead use re-clone its callee, which measured ~5× the
 shared cost at a call-chain depth of six; splice-liveness is decided separately, at
 the rebuild (`Specialization::referenced`). And a dead definition nested inside a
 *live* generalized one is walked once per clone of its enclosing binding — which is
@@ -777,7 +777,7 @@ The shared variant keeps the overwrite/feed operator discipline **on the type**:
 
 Invariance has no MLsub-blessed polar story, so the two polarity-sensitive mechanisms treat it specially:
 
-* **Extrusion** (`extrude_invariant`): a history's `value`/`domain` variables crossing a level boundary each get a *single* fresh proxy linked to the original by **both** a lower and an upper bound (an equality link through the standard lower×upper closure), instead of the polar one-way link. The proxy mutable variables under both `ExtrudeCache` polarity keys.
+* **Extrusion** (`extrude_invariant`): a history's `value`/`domain` variables crossing a level boundary each get a *single* fresh proxy linked to the original by **both** a lower and an upper bound (an equality link through the standard lower×upper closure), instead of the polar one-way link. The proxy registers under both `ExtrudeCache` polarity keys.
 * **Compaction/coalesce**: the two children occupy a dedicated `CompactType::history_slot` (carrying the `kind`), recursing at the **same polarity** — by compaction time the constraint-level invariance has already propagated both directions, so this is materialization only, not a second polarity analysis. `simplify_type` walks the slot at the same polarity; refinement/co-occurrence behavior is unchanged.
 * **Transparent read at joins** (`dissolve_read_feeds`): rule 2 covers a feed handle meeting a concrete consumer *directly*, but a read can also meet other contributions through a shared join variable (`x + 1` flows `Feed(Int)` and `Int` into the binop's `∀α.(α,α)→α`). At coalesce, a position carrying a `Feed`-kind `history_slot` **alongside** non-feed contributions dissolves the handle into its channel before the contribution count; a feed handle alone (or two handles merged) keeps its constructor. Feeding-then-scalar-reading still errors correctly: the dissolved channel is `Fun(?, T)`, which genuinely collides with a scalar.
 
diff --git a/src/ccl/expr.rs b/src/ccl/expr.rs
index 43bdd69a..635c151a 100644
--- a/src/ccl/expr.rs
+++ b/src/ccl/expr.rs
@@ -356,8 +356,8 @@ pub enum TypedExprNode {
     /// [`crate::ccl::planning::plan_loops`] and consumed at operator
     /// conversion. It denotes a pure value — the mutable variable **record** `{key:
     /// ⟦key⟧}`, each field a key's history `Fun(domain, V)` — so a variable
-    /// read is the record projection `__reg.key` (an `Apply` of `Proj(field)`
-    /// to the `__reg` binder). Serialization and the mutable variable↔writer cycle are
+    /// read is the record projection `__hist.key` (an `Apply` of `Proj(field)`
+    /// to the `__hist` binder). Serialization and the mutable variable↔writer cycle are
     /// the *operator's* runtime behaviour (a cyclic `FanOut`), not the node's
     /// denotation — exactly as the induction/commit store realizes the recurrence.
     ///
@@ -371,7 +371,7 @@ pub enum TypedExprNode {
         /// sequencing domain. Each carries its position-0 `init` (the seed,
         /// evaluated once outside every writer's parameter scope). The node
         /// denotes the mutable variable **record** `{key.field_key(): Fun(domain, V)}`; a
-        /// variable read is a projection `__reg.key`. A single-key carrier is
+        /// variable read is a projection `__hist.key`. A single-key carrier is
         /// the one-accumulator case.
         keys: Vec<TransactKey>,
         /// The writers, in declaration order. Each reads/writes a footprint of
@@ -1907,7 +1907,7 @@ impl Default for TypedExpr {
 #[derive(Debug, Clone, PartialEq)]
 pub struct TransactKey {
     /// The key — the (α-uniquified) `Name` of the mutable variable. A read of the
-    /// variable projects [`Name::field_key`] of the mutable variable record (`__reg.k`).
+    /// variable projects [`Name::field_key`] of the history record (`__hist.k`).
     pub name: Name,
     /// The position-0 initial value (the scalar seed), evaluated once outside
     /// every writer's scope. The key's history is `Fun(domain, V)`; a read is
diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs
index 48422c29..f7a05fa7 100644
--- a/src/ccl/infer/api.rs
+++ b/src/ccl/infer/api.rs
@@ -1416,7 +1416,7 @@ pub fn check_mut_discipline(expr: &Expr) -> Result<(), Vec<InferError>> {
 /// [`TypedExprNode::MutDecl`] (a `:=` introduction) and a pass-by-reference
 /// `Lambda` param — both declarations by construction. Checked rather than argued,
 /// because the failure is silent: a mutable variable reaching a `Let` binder is an alias,
-/// and an alias means a register with an unknown writer set.
+/// and an alias means a mutable variable with an unknown writer set.
 ///
 /// A **feed** handle on a `Let` is legal and common (`let d = Defer in …`), which is
 /// why this keys on `mut_value_type` (`Overwrite` only) and not `is_handle`.
diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs
index ca771371..cd20019c 100644
--- a/src/ccl/infer/emit.rs
+++ b/src/ccl/infer/emit.rs
@@ -1311,11 +1311,11 @@ pub(super) fn emit_let<C: Typing>(
         // minting a second variable here would leave the one the binder is bound at
         // unrelated to the one the initializer flowed into.
         //
-        // There is no register arm and no deref-copy case. A mutable variable introduction
-        // is a `MutDecl` (see `emit_mut_decl`), and a mutable-variable-typed initializer was
-        // already deref'd above — so `y: Int = x` off a mutable variable needs no special
-        // handling, and `y: _ = x` completes from the *value* rather than the
-        // history, which is what makes it mean exactly `y = x`.
+        // There is no mutable-variable arm and no deref-copy case. A mutable variable
+        // introduction is a `MutDecl` (see `emit_mut_decl`), and a mutable-variable-typed
+        // initializer was already deref'd above — so `y: Int = x` off a mutable variable
+        // needs no special handling, and `y: _ = x` completes from the *value* rather
+        // than the history, which is what makes it mean exactly `y = x`.
         Some(ann) => {
             let declared = match ann {
                 Type::BoundedHole(_) => ann.clone(),
@@ -1415,17 +1415,17 @@ pub(super) fn emit_letrec<C: Typing>(
 ///
 /// The binder is bound at the history `Mut(V, D)`, so references to `x` carry
 /// `Mut` and a read derefs to `V` at the rule that emits it ([`emit_value_read`], not
-/// the subtyping relation — see `src/ccl/design/mutability.md`, "A mutable variable read is
-/// an explicit operation"). `normalize`
-/// mints the declared type's `Hole` value/domain as fresh variables in Emit — so
-/// `?V` receives the seed and every write — and is the identity in Check.
+/// the subtyping relation — see `src/ccl/design/mutability.md`, "A mutable variable
+/// read is an explicit operation"). `normalize` mints the declared type's `Hole`
+/// value/domain as fresh variables in Emit — so `?V` receives the seed and every
+/// write — and is the identity in Check.
 ///
 /// The seed is one **contribution** to `V`, not its definition, and flows in
 /// verbatim: the join with the mutable variable's writes is what keeps `x := 0` from
-/// pinning the mutable variable to `{Int | __elem == 0}`. A register with *no* writes keeps
-/// its seed's refinement, and that is correct — it really does hold that value at
-/// every position. The constraint is skipped when `V` is still a `Hole` (Check's
-/// identity-normalize), which the already-resolved tree validates on its own.
+/// pinning the mutable variable to `{Int | __elem == 0}`. A mutable variable with *no*
+/// writes keeps its seed's refinement, and that is correct — it really does hold that
+/// value at every position. The constraint is skipped when `V` is still a `Hole`
+/// (Check's identity-normalize), which the already-resolved tree validates on its own.
 ///
 /// The node's own type is its body's: a mutable variable introduction scopes a mutable variable
 /// over `body` and yields whatever `body` yields, exactly as a `let` does.
@@ -1828,7 +1828,7 @@ fn accumulator_body_domain(slots: impl IntoIterator<Item = Type>, item: Type) ->
 
 /// The per-position `to_<defer>` output fields a writer's decision carries beyond
 /// `writes`, read off the writer body's codomain — `(field, value_ty)`. Each
-/// becomes a virtual variable-record key `to_<defer>: Fun(domain, value_ty)` (the
+/// becomes a virtual history-record key `to_<defer>: Fun(domain, value_ty)` (the
 /// per-position feed output stream). The decision codomain is the variant
 /// `` {`commit{𝑃} | `abort} ``; the taps live inside the (dense) `commit` payload
 /// record `𝑃`, so peel `commit` and drop the `writes` field.
@@ -1929,7 +1929,7 @@ fn emit_transact_writer<C: Typing>(
 ///
 /// The node denotes the mutable variable **record** `{key: ⟦key⟧}` — each key's read type
 /// `Fun(domain, α)` (the value's history over the mutable variable's sequencing domain),
-/// what a variable projection `__reg.key` yields; a read reduces it to the
+/// what a variable projection `__hist.key` yields; a read reduces it to the
 /// latest `α` via `final_or_default(history, init)`. The init is the position-0
 /// value, so it bounds the codomain `α` (`init <: α`), not the whole stream.
 /// There is no recurrence *fixpoint* over a step type — the mutable variable↔writer cycle
@@ -1951,7 +1951,7 @@ pub(super) fn emit_transact<C: Typing>(
     // bound) — the codomain of the key's history.
     let mut key_types: HashMap<Name, Type> = HashMap::with_capacity(keys.len());
     for k in keys.iter_mut() {
-        // The variable-record field is the value's history `Fun(domain, α)` over
+        // The history-record field is the value's history `Fun(domain, α)` over
         // the mutable variable's sequencing domain; `final_or_default` reads it back to the
         // latest `α`.
         let value_ty = ctx.fresh();
@@ -1969,7 +1969,7 @@ pub(super) fn emit_transact<C: Typing>(
     for w in writers.iter_mut() {
         emit_transact_writer(w, &key_types, ctx)?;
         // A `to_<defer>` field on the writer's decision record becomes a
-        // virtual mutable variable key the consumer reads as `__reg.to_…`. Its stream
+        // virtual mutable variable key the consumer reads as `__hist.to_…`. Its stream
         // is **site-domained** — one tap value per iteration of *this
         // writer's* source (the channel unions channelize assembled reference
         // it at that type) — unlike the key histories, which live over the
diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs
index 5d540c7e..40ac3403 100644
--- a/src/ccl/infer/solver/constrain.rs
+++ b/src/ccl/infer/solver/constrain.rs
@@ -1616,7 +1616,7 @@ mod tests {
         // Setup: α has upper Int. Then β <: α.
         //
         // Note: the solver's constrain_subtype rule, when both sides are
-        // variables, fires the Var-on-lhs branch first and mutable variables
+        // variables, fires the Var-on-lhs branch first and registers
         // rhs (α) directly in lhs (β)'s upper bounds. α's existing
         // uppers are NOT eagerly transferred to β — that transitive
         // chain (β <: Int) is recovered at simplification time by
diff --git a/src/ccl/infer/solver/traits.rs b/src/ccl/infer/solver/traits.rs
index 9122f8a8..8f906843 100644
--- a/src/ccl/infer/solver/traits.rs
+++ b/src/ccl/infer/solver/traits.rs
@@ -963,7 +963,7 @@ fn places_under(root: &Rc<InferVar>) -> std::collections::BTreeMap<StepPath, Pla
                     codomain,
                     ..
                 } => descend(codomain, &path, Step::Result, &mut frontier),
-                // The value a register or channel carries is a component of it in the
+                // The value a mutable variable or channel carries is a component of it in the
                 // same sense a field is; the domain beside it is an index, not a value
                 // this place holds.
                 Type::History { value, .. } => {
diff --git a/src/ccl/lower/exprs.rs b/src/ccl/lower/exprs.rs
index c25a24e7..40b369ed 100644
--- a/src/ccl/lower/exprs.rs
+++ b/src/ccl/lower/exprs.rs
@@ -162,13 +162,13 @@ pub(super) fn lower_call(
                     "await_final takes a transactional mutable variable by name",
                 ));
             };
-            let reg = id.as_str();
-            if !ctx.is_transactional_mut_var(reg) || ctx.is_shadowed(reg) {
+            let name = id.as_str();
+            if !ctx.is_transactional_mut_var(name) || ctx.is_shadowed(name) {
                 return Err(LoweringError::unsupported(
                     arg.span,
                     format!(
-                        "`{reg}` is not a transactional mutable variable, so it has no commit history to \
-                         await. `await_final` applies to a `{reg}: Mut(V, Txn) := …` mutable variable; an \
+                        "`{name}` is not a transactional mutable variable, so it has no commit history to \
+                         await. `await_final` applies to a `{name}: Mut(V, Txn) := …` mutable variable; an \
                          induction accumulator's final value is read by naming it after its loop"
                     ),
                 ));
@@ -180,22 +180,22 @@ pub(super) fn lower_call(
                 return Err(LoweringError::unsupported(
                     func.span,
                     format!(
-                        "await_final(`{reg}`) inside a `with begin():` block would wait on the \
-                         commit history that block extends; a block reads `{reg}` bare, as a \
+                        "await_final(`{name}`) inside a `with begin():` block would wait on the \
+                         commit history that block extends; a block reads `{name}` bare, as a \
                          snapshot"
                     ),
                 ));
             }
-            // The *linearity* rule — the await consumes the mutable variable, so no later read
-            // or write may name it, and no mutable variable may be awaited twice — is not
-            // checkable here: `lower_stmts_inner` builds its statement chain
-            // right-to-left, so lowering visits the tail before the statements it
-            // follows. It is `transact_phase::check_await_final_linearity`, on the
-            // typed tree whose continuation spine runs in source order and where mutable variable
-            // identity is exact. A later `with begin():` block is only rejected by it
-            // if that block names the awaited mutable variable; blocks over other mutable variables
-            // are ordinary.
-            let mut_var = ctx.tag_image(Expr::var(reg.to_string()), arg.span);
+            // The *linearity* rule — the await consumes the mutable variable, so no
+            // later read or write may name it, and no mutable variable may be awaited
+            // twice — is not checkable here: `lower_stmts_inner` builds its statement
+            // chain right-to-left, so lowering visits the tail before the statements
+            // it follows. It is `transact_phase::check_await_final_linearity`, on the
+            // typed tree whose continuation spine runs in source order and where
+            // mutable variable identity is exact. A later `with begin():` block is
+            // only rejected by it if that block names the awaited mutable variable;
+            // blocks over other mutable variables are ordinary.
+            let mut_var = ctx.tag_image(Expr::var(name.to_string()), arg.span);
             let await_fn = ctx.tag_image(Expr::builtin(Builtin::AwaitFinal), func.span);
             Ok(Expr::apply(mut_var, await_fn))
         }
diff --git a/src/ccl/lower/stmts.rs b/src/ccl/lower/stmts.rs
index 06860d70..4373750f 100644
--- a/src/ccl/lower/stmts.rs
+++ b/src/ccl/lower/stmts.rs
@@ -431,7 +431,7 @@ pub(super) fn lower_middle_stmt(
             }
             let (req_name, resp_name) = extract_http_serve_names(target)?;
             let (port, method, path) = extract_http_serve_args(value)?;
-            // Create and mutable variable the source now; the caller drains new_sources
+            // Create and register the source now; the caller drains new_sources
             // via take_new_sources() after lower_stmts returns, before type inference.
             let port_u16: u16 = port.parse().map_err(|_| {
                 LoweringError::unsupported(
@@ -596,7 +596,7 @@ pub(super) fn lower_middle_stmt(
             };
             // Stamp the binding `Mut(V, D)` (so inference binds `x` at `Mut` and
             // its references deref to `V`). `D = Txn` for a transactional mutable variable
-            // (fixed here, never inferred), which also mutable variables `x` so its
+            // (fixed here, never inferred), which also registers `x` so its
             // `with begin():` writes lower to `MutWrite` and its bare reads are
             // gated. An induction accumulator gets `D = Hole` and carries *no* lowering
             // registry — its mutability is this `Mut` type, checked
@@ -1009,7 +1009,7 @@ pub(super) fn pre_register_txn_decls(stmts: &[Spanned<ChlStmt>], ctx: &mut Lower
             // A `def` with a pass-by-reference `Mut` parameter is lowered and
             // applied curried. Blocks lower right-to-left, so a call site is
             // lowered *before* the `def` preceding it textually — pre-register
-            // the name here so [`lower_call`] picks the curried shape. Mutable variable
+            // the name here so [`lower_call`] picks the curried shape. Register
             // or unregister per the definition's mut-ness so the last `def` of a
             // name in the block wins (a non-`Mut` redefinition clears an earlier
             // `Mut` one, so its calls lower tupled).
diff --git a/src/ccl/lower/transactions.rs b/src/ccl/lower/transactions.rs
index 3d979e7a..1fd49019 100644
--- a/src/ccl/lower/transactions.rs
+++ b/src/ccl/lower/transactions.rs
@@ -6,7 +6,7 @@
 //! (`ExprStmt(For{target, iter, block}, continuation)`); the *only* structural
 //! difference is that its `MutWrite`s target `Mut(V, Txn)` stores, which
 //! `transact_phase` recognizes (by the mutable variable's registered base name) and routes
-//! to the commit engine rather than the induction `Recurse`. A standalone
+//! to the commit engine rather than the induction store. A standalone
 //! transaction is one commit over a synthesized singleton source. Writes and
 //! reads inside the block run with `in_tx_body = true`, so a bare mutable variable read is
 //! a snapshot (a bare mutable variable read *outside* a block is the rejected out-of-block
@@ -245,7 +245,7 @@ fn lower_tx_block_inner(
             // the read-your-writes snapshot at this point (a bare mutable variable read
             // resolves to the just-written value); `transact_phase` collects it
             // as a `to_<defer>` tap on the writer decision and hoists a
-            // `Feed(defer, __reg ▷ .to_<defer>)` into the mutable variable body, so each
+            // `Feed(defer, __hist ▷ .to_<defer>)` into the mutable variable body, so each
             // emission carries *its own* commit's value. Mirrors the induction
             // phase's in-loop feeds (see `src/ccl/mut_elim.rs`).
             ChlStmt::Expr(value) if matches!(&value.node, ChlExpr::Feed { .. }) => {
diff --git a/src/ccl/mut_elim.rs b/src/ccl/mut_elim.rs
index 68a65f7d..c7066c27 100644
--- a/src/ccl/mut_elim.rs
+++ b/src/ccl/mut_elim.rs
@@ -20,9 +20,9 @@
 //!
 //! [`crate::ccl::planning::plan_loops`] runs **after `lambda_elim`**, on the group's point-free
 //! normal form, and lowers each group onto the domain-parameterized
-//! [`TypedExprNode::Transact`] carrier (`let __reg = Transact{…} in …`),
-//! whose induction domain op-conversion compiles to the `Recurse` recurrence
-//! (the `Txn` domain, to the commit operator).
+//! [`TypedExprNode::Transact`] carrier (`let __hist = Transact{…} in …`),
+//! whose induction domain op-conversion compiles to the changelog induction
+//! store (the `Txn` domain, to the commit operator).
 //!
 //! **Why one `LetRec` travels post-elim, and why `Transact` still exists.**
 //! Recognition anchors on the guard builtins (`get_prev_seq` / `get_prev_txn`
@@ -680,10 +680,10 @@ fn transform_loop(target: TypedBinding, iter: Expr, loop_body: Expr, cont: Expr)
     // Every reference to an accumulator is either in the loop (a read-your-writes
     // read) or downstream of it (the trailing final read), so these two trees
     // carry every `Mut(V, D)` this loop's mutable variables have.
-    let reg_vtys = mut_var_value_tys([&loop_body, &cont]);
+    let value_tys = mut_var_value_tys([&loop_body, &cont]);
     // Accumulators in first-write order, with their value types.
     let mut accs: Vec<(Name, Type)> = Vec::new();
-    collect_writes(&loop_body, &reg_vtys, &mut accs);
+    collect_writes(&loop_body, &value_tys, &mut accs);
     if accs.is_empty() {
         // A loop with no accumulator. If its body feeds — a stateless generator,
         // or a `with begin():` read-only transaction (`for r in iter: with
@@ -735,7 +735,7 @@ fn transform_loop(target: TypedBinding, iter: Expr, loop_body: Expr, cont: Expr)
     // Fold the accumulators into a decision-factored history binding, then wrap it
     // in a nested `LetRec`: re-point the continuation's trailing reads at the
     // extracted finals, recurse into it, prepend the reads, and hoist the feeds.
-    let fold = fold_induction_loop(&target, &iter, loop_body, &reg_vtys);
+    let fold = fold_induction_loop(&target, &iter, loop_body, &value_tys);
     let mut cont = cont;
     for (acc, x_final) in &fold.renames {
         rename_uses(&mut cont, acc, x_final);
@@ -800,17 +800,17 @@ impl InductionFold {
 /// See [`InductionFold`]. Caller must guard on a non-empty accumulator set
 /// (an accumulator-free loop is a feed-only/no-op loop, handled separately).
 ///
-/// `reg_vtys` supplies each accumulator's value type ([`mut_var_value_tys`]);
+/// `value_tys` supplies each accumulator's value type ([`mut_var_value_tys`]);
 /// the caller builds it over the widest tree it holds, so that a mutable variable read
 /// only *downstream* of the loop still contributes its `Mut(V, D)`.
 pub(crate) fn fold_induction_loop(
     target: &TypedBinding,
     iter: &Expr,
     loop_body: Expr,
-    reg_vtys: &HashMap<Name, Type>,
+    value_tys: &HashMap<Name, Type>,
 ) -> InductionFold {
     let mut accs: Vec<(Name, Type)> = Vec::new();
-    collect_writes(&loop_body, reg_vtys, &mut accs);
+    collect_writes(&loop_body, value_tys, &mut accs);
     assert!(
         !accs.is_empty(),
         "fold_induction_loop: caller must guard on a non-empty accumulator set"
@@ -982,7 +982,7 @@ pub(crate) fn fold_induction_loop(
 /// no history binding and no letrec.
 ///
 /// When `value` is a read of a transactional mutable variable (a `Var` `transact_phase`
-/// rebound to `as_of_read(__reg.k)`, constant in `target`), the map broadcasts that
+/// rebound to `as_of_read(__hist.k)`, constant in `target`), the map broadcasts that
 /// as-of read to every loop position; `transact_phase::rewrite_as_of_reads`
 /// (post-`channelize`, pre-lambda-elim) then pairs it with this loop as its trigger,
 /// which is where the outer-indexed as-of join gets the position it reads at.
@@ -1085,7 +1085,7 @@ pub(crate) fn mut_var_value_tys<'a>(
 }
 
 /// Collect `MutWrite` targets in first-write order with their value types, taken
-/// from `reg_vtys` — the join inference recorded on the mutable variable's `Mut(V, D)`.
+/// from `value_tys` — the join inference recorded on the mutable variable's `Mut(V, D)`.
 ///
 /// A mutable variable with no entry is one no reference types as a `Mut`: either nothing
 /// reads it (only writes mention it, so its value type is unobservable), or the
@@ -1094,17 +1094,17 @@ pub(crate) fn mut_var_value_tys<'a>(
 /// mutable variable takes no refinement from any single contribution, and an unstripped
 /// one would be a refinement acquired by erasure rather than by `cast`
 /// (`src/ccl/design/type-inference.md`, "Refinements on the lattice").
-fn collect_writes(expr: &Expr, reg_vtys: &HashMap<Name, Type>, out: &mut Vec<(Name, Type)>) {
+fn collect_writes(expr: &Expr, value_tys: &HashMap<Name, Type>, out: &mut Vec<(Name, Type)>) {
     if let TypedExprNode::MutWrite { name, value } = &expr.node
         && !out.iter().any(|(n, _)| n == name)
     {
-        let vty = reg_vtys
+        let vty = value_tys
             .get(name)
             .cloned()
             .unwrap_or_else(|| strip_refinements(&value.ty));
         out.push((name.clone(), vty));
     }
-    expr.walk_children(|c| collect_writes(c, reg_vtys, out));
+    expr.walk_children(|c| collect_writes(c, value_tys, out));
 }
 
 /// Whether `expr` contains a `Feed` marker (backs the no-op-loop invariant
@@ -1240,8 +1240,8 @@ fn transform_chain(
         // unchanged value is a no-op — the conditional change rides the *values*
         // (each value-`Case` compiles via the C-form at `lambda_elim`), not a
         // per-position commit gate. One writer over the full source, so no
-        // restricted per-leg sources and no cyclic desync — the changelog
-        // (`InductionStore`) realization the dense multi-leg `Recurse` replaced.
+        // restricted per-leg sources and no cyclic desync, which a multi-leg
+        // realization over per-leg restricted sources could not avoid.
         TypedExprNode::ExprStmt { expr: effect, body }
             if matches!(
                 &effect.node,
@@ -1467,10 +1467,10 @@ fn decision_writes(dec: &Expr) -> Vec<Expr> {
 ///   (`⧺ⱼ wⱼᵢ ↾ π̂ⱼ`), so a **partial op** (`//`, `%`) in a write value is only
 ///   evaluated at the positions its guard admits — never at a carried position.
 ///
-/// Carry-completeness is also what makes the dense `Recurse` path correct for an
-/// **async source**: that path cycles on `.writes` (not `` `commit ``), and `writes`
-/// now carries `snapshotᵢ` (the previous accumulator) wherever no guard fires, so
-/// the guard is honored by the value rather than silently dropped.
+/// Carry-completeness is also what makes a **`.writes`-cycling** realization correct
+/// for an **async source**: `writes` carries `snapshotᵢ` (the previous accumulator)
+/// wherever no guard fires, so the guard is honored by the value rather than
+/// silently dropped.
 fn conditional_decision(
     writing: Vec<(Expr, Vec<Expr>)>,
     carry: Vec<Expr>,
@@ -1795,10 +1795,10 @@ mod tests {
     }
 
     /// Recognition lowers the group onto the domain-parameterized `Transact`
-    /// carrier: `let __reg = transact (x = x) { [x]⇒[x] over … do λ __p → …
-    /// `commit(⟨writes: (x)⟩) | `abort } in (__reg.x, x) ▷ final_or_default``, with
+    /// carrier: `let __hist = transact (x = x) { [x]⇒[x] over … do λ __p → …
+    /// `commit(⟨writes: (x)⟩) | `abort } in (__hist.x, x) ▷ final_or_default``, with
     /// the key `init` read from the pre-loop binding and each accumulator read
-    /// rewritten to a variable-record projection.
+    /// rewritten to a history-record projection.
     #[test]
     fn recognition_builds_the_transact_carrier() {
         let (tree, _, _) = direct_mirror_sum();
@@ -1820,8 +1820,8 @@ mod tests {
             "writer body must terminate in a `` `commit(⟨writes⟩) | `abort `` decision: {s}"
         );
         assert!(
-            s.contains("__reg.") && s.contains("final_or_default"),
-            "trailing read must project the mutable variable record and reduce it: {s}"
+            s.contains("__hist.") && s.contains("final_or_default"),
+            "trailing read must project the history record and reduce it: {s}"
         );
     }
 
diff --git a/src/ccl/names.rs b/src/ccl/names.rs
index 23777b12..891d5823 100644
--- a/src/ccl/names.rs
+++ b/src/ccl/names.rs
@@ -218,7 +218,7 @@ impl Name {
     /// Unlike [`base`](Self::base) it folds the `uid` in, so two distinct
     /// binders sharing a spelling (e.g. accumulators in sibling loops) get
     /// distinct keys. A variable read of a mutable variable key projects this field of
-    /// the mutable variable record (`__reg.field_key`).
+    /// the history record (`__hist.field_key`).
     pub fn field_key(&self) -> String {
         match self {
             Name::Raw(s) => s.clone(),
diff --git a/src/ccl/ops.rs b/src/ccl/ops.rs
index e6e6a8f2..7bfcb3c8 100644
--- a/src/ccl/ops.rs
+++ b/src/ccl/ops.rs
@@ -393,7 +393,7 @@ pub enum Builtin {
     /// "Builtins", and [`crate::ccl::letrec::check_letrec_causal`]).
     ///
     /// Op-conversion never compiles this builtin directly: letrec pattern
-    /// recognition consumes it (the causal self-cycle becomes the `Recurse`
+    /// recognition consumes it (the causal self-cycle becomes the induction-store
     /// engine), so its op-conversion arm is a deliberate error, like
     /// `LetRec`'s.
     GetPrevSeq,
@@ -455,7 +455,7 @@ pub enum Builtin {
     /// *completeness*; every other fed-out mutable variable read is an arbitrary as-of
     /// sample ([`Self::AsOf`]). It is a surface marker in the sense the `For` /
     /// `Begin` / `MutWrite` nodes are: [`crate::ccl::transact_phase`] consumes it,
-    /// replacing each occurrence with `final_or_default(reg_x, init)` over the
+    /// replacing each occurrence with `final_or_default(hist_x, init)` over the
     /// mutable variable's history binding — the single sanctioned application of
     /// [`Self::FinalOrDefault`] to a commit history. So it never reaches
     /// op-conversion, and its arm there is a deliberate error like
diff --git a/src/ccl/planning/iterate.rs b/src/ccl/planning/iterate.rs
index dfead343..7482c2be 100644
--- a/src/ccl/planning/iterate.rs
+++ b/src/ccl/planning/iterate.rs
@@ -159,7 +159,7 @@ pub(super) fn insert_iterate_recurse(expr: &mut Expr) {
         }
         // `as_of` takes `Tuple([trigger, source])` — the `trigger` is the
         // iteration site (op-conversion compiles it with `input=None`), so wrap
-        // it; the `source` is a mutable variable read (`__reg.k`), not an iteration source,
+        // it; the `source` is a mutable variable read (`__hist.k`), not an iteration source,
         // and is left alone. A `Var` trigger is already iterate-wrapped at its
         // let-site, so `wrap_with_iterate`'s `is_iteration_bearing` check makes
         // this a no-op there; a raw `[unit]` singleton (the standalone terminal
@@ -225,7 +225,7 @@ pub(super) fn insert_iterate_recurse(expr: &mut Expr) {
             }
         }
         // Each transaction writer's source is iterated internally by the
-        // mutable variable engine (`Recurse` for an induction accumulator); op-conversion
+        // mutable variable engine (the induction store for an accumulator); op-conversion
         // compiles it with `input=None`, so wrap it like a loop source.
         TypedExprNode::Transact { writers, .. } => {
             for w in writers.iter_mut() {
@@ -1143,7 +1143,7 @@ mod tests {
         // previous-accumulator read.  The exact body shape doesn't matter for
         // this test — we only check the writer `source` gets iterate-wrapped.
         let body = Expr::var("acc").with_ty(int.clone());
-        let reg_ty = Type::Record(vec![(
+        let hist_ty = Type::Record(vec![(
             "acc".to_string(),
             fun_ty(Type::UIntRange(3), int.clone()),
         )]);
@@ -1160,7 +1160,7 @@ mod tests {
             }],
             domain: Type::UIntRange(3),
         })
-        .with_ty(reg_ty);
+        .with_ty(hist_ty);
 
         insert_iterate_recurse(&mut expr);
 
diff --git a/src/ccl/planning/loops.rs b/src/ccl/planning/loops.rs
index 20a807b3..01fa1f3b 100644
--- a/src/ccl/planning/loops.rs
+++ b/src/ccl/planning/loops.rs
@@ -27,7 +27,7 @@ use crate::ccl::{
 
 /// Lower every phase-emitted `LetRec` — **after `lambda_elim`**, on its
 /// point-free normal form — onto the [`TypedExprNode::Transact`] carrier:
-/// `let __reg = Transact{…} in <reads off __reg.field>`. An unrecognized
+/// `let __hist = Transact{…} in <reads off __hist.field>`. An unrecognized
 /// group is a compile-time panic (no silent fallback) — the phases and this
 /// recognizer are co-designed against the point-free normal forms, exercised
 /// end-to-end by the induction suite (`tests/compilation_pipeline/mutability.rs`),
@@ -53,7 +53,7 @@ pub(crate) fn plan_loops(expr: Expr) -> Expr {
             unreachable!("causal above")
         };
         // The point-free guard matcher backs this in all builds — recognition
-        // is the wall between "phase emitted" and "engine consumed", with
+        // is the boundary between "phase emitted" and "engine consumed", with
         // channelize and lambda_elim in between.
         if let Err(errs) = check_letrec_causal(&bindings) {
             panic!(
@@ -163,7 +163,7 @@ fn unwrap_const(e: Expr) -> Expr {
 /// `(⟨view⟩ ▷ const, ⟨pos⟩, ⟨default⟩ ▷ const) ▷ zip ≫ get_prev_*`,
 /// returning `(default, which-guard)`. The view slot (the causal history
 /// read) is validated by `check_letrec_causal` and discarded here — the
-/// engine reconstructs every read from the reg itself.
+/// engine reconstructs every read from the history record itself.
 fn split_causal_compose(guard: Expr) -> (Expr, Builtin) {
     let TypedExprNode::Compose(mut elts) = guard.node else {
         panic!("letrec recognition: guard is not a compose");
@@ -248,7 +248,7 @@ fn split_decision_compose(decision: Expr, decision_ty: &Type) -> (Vec<Expr>, Exp
 /// Which binding a transaction `LetRec` binding is (dispatched on its body\'s
 /// post-elim shape — see [`recognize_txn_group`]).
 enum TxnBinding {
-    /// `reg_k : Txn ⇒ V = (⟨view⟩ ▷ const, id, ⟨init⟩ ▷ const) ▷ zip ≫ get_prev_txn`.
+    /// `hist_k : Txn ⇒ V = (⟨view⟩ ▷ const, id, ⟨init⟩ ▷ const) ▷ zip ≫ get_prev_txn`.
     History,
     /// `commits_j : 𝐼 ⇒ {time, write_targets, decision} = let __t = begin in ⟨record⟩ ▷ zip`.
     Commit,
@@ -280,7 +280,7 @@ fn classify_txn_binding(def: &Expr) -> TxnBinding {
 /// (k…) ▷ const, decision: (⟨reads…⟩, ⟨source⟩) ▷ zip ≫ ⟨body⟩) ▷ zip`.
 /// The writer body is lifted verbatim; `write_keys` come off the
 /// `write_targets` tuple\'s history vars, `read_keys` off each snapshot
-/// read\'s trailing history var (`__t ≫ reg_k`).
+/// read\'s trailing history var (`__t ≫ hist_k`).
 fn recover_writer(site_dom: &Type, def: Expr) -> WriterSite {
     let TypedExprNode::Let {
         bound_expr, body, ..
@@ -363,7 +363,7 @@ fn recover_writer(site_dom: &Type, def: Expr) -> WriterSite {
         };
     }
     let (reads, source, body) = split_decision_compose(decision, &decision_ty);
-    // Each snapshot read is `__t ≫ reg_k` — the key is the trailing
+    // Each snapshot read is `__t ≫ hist_k` — the key is the trailing
     // history var.
     let read_keys: Vec<Name> = reads
         .into_iter()
@@ -374,7 +374,7 @@ fn recover_writer(site_dom: &Type, def: Expr) -> WriterSite {
                     "letrec recognition: snapshot read does not end in a mutable variable key var"
                 ),
             },
-            _ => panic!("letrec recognition: snapshot read is not `__t ≫ reg_k`"),
+            _ => panic!("letrec recognition: snapshot read is not `__t ≫ hist_k`"),
         })
         .collect();
 
@@ -386,7 +386,7 @@ fn recover_writer(site_dom: &Type, def: Expr) -> WriterSite {
     }
 }
 
-/// The variable-record tap field a tap binding `commits_j ≫ .decision ≫ .field`
+/// The history-record tap field a tap binding `commits_j ≫ .decision ≫ .field`
 /// projects — its trailing field projection.
 fn tap_field(def: &Expr) -> String {
     let TypedExprNode::Compose(elts) = &def.node else {
@@ -404,13 +404,13 @@ fn tap_field(def: &Expr) -> String {
 /// key (its `init` off the guard\'s default slot), one **commit-record** per
 /// `with begin():` site ([`recover_writer`] — writer body verbatim), one
 /// **tap** per in-block feed. A read of a history / tap binding in the
-/// continuation becomes a variable-record projection `__reg.field`.
+/// continuation becomes a history-record projection `__hist.field`.
 fn recognize_txn_group(bindings: Vec<(TypedBinding, Expr)>, body: Expr) -> Expr {
     let mut keys: Vec<TransactKey> = Vec::new();
-    // Key history-binding name → value type (for the mutable variable record + read types).
+    // Key history-binding name → value type (for the history record + read types).
     let mut key_ty: Vec<(Name, Type)> = Vec::new();
     let mut writers: Vec<WriterSite> = Vec::new();
-    // Tap binding name → (variable-record field, value type).
+    // Tap binding name → (history-record field, value type).
     let mut taps: Vec<(Name, String, Type)> = Vec::new();
     // Every binding name, to assert the continuation has no dangling references.
     let mut binding_names: Vec<Name> = Vec::with_capacity(bindings.len());
@@ -447,24 +447,24 @@ fn recognize_txn_group(bindings: Vec<(TypedBinding, Expr)>, body: Expr) -> Expr
     // Variable record `{key.field_key(): Fun(Txn, V), …, to_<defer>: Fun(Txn, V)}`
     // — mutable variable keys (key order) then tap virtual keys (feed order), the exact
     // field order op-conversion\'s `emit_transact`/`build_commit_store` produce.
-    let mut reg_field_tys: Vec<(String, Type)> = key_ty
+    let mut hist_field_tys: Vec<(String, Type)> = key_ty
         .iter()
         .map(|(n, v)| (n.field_key(), Type::fun(Type::Txn, v.clone())))
         .collect();
     for (_, field, stream_ty) in &taps {
-        reg_field_tys.push((field.clone(), stream_ty.clone()));
+        hist_field_tys.push((field.clone(), stream_ty.clone()));
     }
-    let reg_ty = Type::Record(reg_field_tys);
+    let hist_ty = Type::Record(hist_field_tys);
 
     let mut transact = Expr::new(TypedExprNode::Transact {
         keys,
         writers,
         domain: Type::Txn,
     });
-    transact.ty = reg_ty.clone();
+    transact.ty = hist_ty.clone();
 
     // Continuation reads: each history / tap binding reference is a
-    // variable-record projection `__reg.field : Fun(Txn, V)`.
+    // history-record projection `__hist.field : Fun(Txn, V)`.
     let mut read_map: HashMap<Name, (String, Type)> = HashMap::new();
     for (n, v) in &key_ty {
         read_map.insert(n.clone(), (n.field_key(), Type::fun(Type::Txn, v.clone())));
@@ -473,10 +473,10 @@ fn recognize_txn_group(bindings: Vec<(TypedBinding, Expr)>, body: Expr) -> Expr
         read_map.insert(n.clone(), (field.clone(), stream_ty.clone()));
     }
 
-    let reg = Name::fresh("__reg");
+    let hist = Name::fresh("__hist");
     let mut body = body;
-    rewrite_txn_reads(&mut body, &reg, &reg_ty, &read_map);
-    collapse_snapshot_sources(&mut body, &reg, &reg_ty);
+    rewrite_txn_reads(&mut body, &hist, &hist_ty, &read_map);
+    collapse_snapshot_sources(&mut body, &hist, &hist_ty);
     for n in &binding_names {
         assert_eq!(
             count_free(n, &body),
@@ -486,35 +486,35 @@ fn recognize_txn_group(bindings: Vec<(TypedBinding, Expr)>, body: Expr) -> Expr
         );
     }
 
-    Expr::let_in(binding(reg, reg_ty), transact, body)
+    Expr::let_in(binding(hist, hist_ty), transact, body)
 }
 
 /// Rewrite every history / tap binding reference in the continuation to a
-/// variable-record projection `__reg.field`, then drop the letrec (its bindings
+/// history-record projection `__hist.field`, then drop the letrec (its bindings
 /// are now carried by the `Transact`). Mirrors [`rewrite_hist_reads`].
 fn rewrite_txn_reads(
     e: &mut Expr,
-    reg: &Name,
-    reg_ty: &Type,
+    hist: &Name,
+    hist_ty: &Type,
     read_map: &HashMap<Name, (String, Type)>,
 ) {
     if let TypedExprNode::Var(n) = &e.node
         && let Some((field, field_ty)) = read_map.get(n)
     {
-        *e = reg_field_read(reg, reg_ty, field.clone(), field_ty.clone());
+        *e = hist_field_read(hist, hist_ty, field.clone(), field_ty.clone());
         return;
     }
-    e.walk_children_mut(|c| rewrite_txn_reads(c, reg, reg_ty, read_map));
+    e.walk_children_mut(|c| rewrite_txn_reads(c, hist, hist_ty, read_map));
 }
 
 /// Collapse a multi-variable as-of read\'s snapshot source: the pre-elim
 /// as-of-read rewrite emits `as_of((trigger, (f_a: ⟨a-hist⟩, f_b: ⟨b-hist⟩)))`
-/// with a *record literal* of history reads (the mutable variable record does not exist
-/// yet). After [`rewrite_txn_reads`] every field is `__reg.f`; replace the
+/// with a *record literal* of history reads (the history record does not exist
+/// yet). After [`rewrite_txn_reads`] every field is `__hist.f`; replace the
 /// literal with the mutable variable itself, so op-conversion latches ONE
 /// whole-variable snapshot per request (§I-c atomicity) instead of per-field
 /// reads.
-fn collapse_snapshot_sources(e: &mut Expr, reg: &Name, reg_ty: &Type) {
+fn collapse_snapshot_sources(e: &mut Expr, hist: &Name, hist_ty: &Type) {
     if let TypedExprNode::Apply { argument, function } = &mut e.node
         && matches!(&function.node, TypedExprNode::Builtin(Builtin::AsOf))
         && let TypedExprNode::Tuple(elts) = &mut argument.node
@@ -523,14 +523,14 @@ fn collapse_snapshot_sources(e: &mut Expr, reg: &Name, reg_ty: &Type) {
         && fields.iter().all(|(f, v)| {
             matches!(&v.node,
                 TypedExprNode::Apply { argument: sv, function: proj }
-                    if matches!(&sv.node, TypedExprNode::Var(n) if n == reg)
+                    if matches!(&sv.node, TypedExprNode::Var(n) if n == hist)
                         && matches!(&proj.node, TypedExprNode::Proj(ProjKey::Field(pf)) if pf == f))
         })
     {
         // Stamp the source with the mutable variable's *own* type (all keys + taps), not
-        // just the read subset — the `Var(__reg)` must agree with its binder,
+        // just the read subset — the `Var(__hist)` must agree with its binder,
         // and op-conversion's snapshot read projects the fields it needs by name.
-        *source = tvar(reg, reg_ty.clone());
+        *source = tvar(hist, hist_ty.clone());
         // The argument tuple\'s recorded type keeps its shape; re-stamp the
         // source slot.
         if let Type::Tuple(tys) = &mut argument.ty
@@ -539,7 +539,7 @@ fn collapse_snapshot_sources(e: &mut Expr, reg: &Name, reg_ty: &Type) {
             tys[1] = source.ty.clone();
         }
     }
-    e.walk_children_mut(|c| collapse_snapshot_sources(c, reg, reg_ty));
+    e.walk_children_mut(|c| collapse_snapshot_sources(c, hist, hist_ty));
 }
 
 /// Destructure the phase\'s decision-factored induction binding (post-elim)
@@ -553,7 +553,7 @@ fn collapse_snapshot_sources(e: &mut Expr, reg: &Name, reg_ty: &Type) {
 /// The writer `body` is lifted verbatim; keys\' inits come off the guard\'s
 /// defaults tuple; the source off the snapshot\'s trailing slot. Reads of
 /// `__hist` in the letrec body (`__hist ≫ .writes ≫ .i` extracts and
-/// `__hist ≫ .to_<feed>` taps) become variable-record projections.
+/// `__hist ≫ .to_<feed>` taps) become history-record projections.
 fn recognize_group(h: TypedBinding, def: Expr, letrec_body: Expr) -> Expr {
     let (domain_ty, decision_ty) = fun_parts(&h.ty);
     // The decision codomain is the variant `` {`commit{𝑃} | `abort} ``; the feed taps
@@ -614,7 +614,7 @@ fn recognize_group(h: TypedBinding, def: Expr, letrec_body: Expr) -> Expr {
         .collect();
     let key_names: Vec<Name> = keys.iter().map(|k| k.name.clone()).collect();
 
-    let mut reg_field_tys: Vec<(String, Type)> = keys
+    let mut hist_field_tys: Vec<(String, Type)> = keys
         .iter()
         .zip(&acc_tys)
         .map(|(k, vty)| {
@@ -625,9 +625,9 @@ fn recognize_group(h: TypedBinding, def: Expr, letrec_body: Expr) -> Expr {
         })
         .collect();
     for (f, vty) in &feed_fields {
-        reg_field_tys.push((f.clone(), Type::fun(domain_ty.clone(), vty.clone())));
+        hist_field_tys.push((f.clone(), Type::fun(domain_ty.clone(), vty.clone())));
     }
-    let reg_ty = Type::Record(reg_field_tys);
+    let hist_ty = Type::Record(hist_field_tys);
 
     let writer = WriterSite {
         read_keys: key_names.clone(),
@@ -641,15 +641,15 @@ fn recognize_group(h: TypedBinding, def: Expr, letrec_body: Expr) -> Expr {
         writers: vec![writer],
         domain: domain_ty.clone(),
     });
-    transact.ty = reg_ty.clone();
+    transact.ty = hist_ty.clone();
 
-    let reg = Name::fresh("__reg");
+    let hist = Name::fresh("__hist");
     let mut body = letrec_body;
     rewrite_hist_reads(
         &mut body,
         &h.name,
-        &reg,
-        &reg_ty,
+        &hist,
+        &hist_ty,
         &keys_for_reads,
         &acc_tys,
         &domain_ty,
@@ -661,29 +661,29 @@ fn recognize_group(h: TypedBinding, def: Expr, letrec_body: Expr) -> Expr {
         h.name
     );
 
-    Expr::let_in(binding(reg, reg_ty), transact, body)
+    Expr::let_in(binding(hist, hist_ty), transact, body)
 }
 
-/// `__reg.field = Apply(Var(__reg), Proj(Field(field)))` — a variable-record
+/// `__hist.field = Apply(Var(__hist), Proj(Field(field)))` — a history-record
 /// projection reading key `field`\'s history `Fun(D, V)`.
-fn reg_field_read(reg: &Name, reg_ty: &Type, field: String, field_ty: Type) -> Expr {
+fn hist_field_read(hist: &Name, hist_ty: &Type, field: String, field_ty: Type) -> Expr {
     let mut proj = Expr::proj_field(field);
-    proj.ty = Type::fun(reg_ty.clone(), field_ty.clone());
-    let mut app = Expr::apply(tvar(reg, reg_ty.clone()), proj);
+    proj.ty = Type::fun(hist_ty.clone(), field_ty.clone());
+    let mut app = Expr::apply(tvar(hist, hist_ty.clone()), proj);
     app.ty = field_ty;
     app
 }
 
-/// Rewrite every `__hist` view in the letrec body to a variable-record
-/// projection `__reg.field`. The phase builds accumulator reads as the flat
+/// Rewrite every `__hist` view in the letrec body to a history-record
+/// projection `__hist.field`. The phase builds accumulator reads as the flat
 /// compose `__hist ≫ .writes ≫ .i` and feed reads as `__hist ≫ .to_<feed>`;
 /// downstream normalization may extend those composes (`__hist ≫ .to ≫ f`),
 /// so the match is on the *prefix*, keeping any tail elements.
 fn rewrite_hist_reads(
     e: &mut Expr,
     h: &Name,
-    reg: &Name,
-    reg_ty: &Type,
+    hist: &Name,
+    hist_ty: &Type,
     keys: &[TransactKey],
     acc_tys: &[Type],
     domain_ty: &Type,
@@ -699,7 +699,7 @@ fn rewrite_hist_reads(
             Some(TypedExprNode::Builtin(Builtin::VariantProject(_)))
         )
     {
-        // The reg read replacing the matched prefix, plus how many compose
+        // The history-record read replacing the matched prefix, plus how many compose
         // elements the prefix covered (the `variant_project` step included).
         let replacement: Option<(Expr, usize)> =
             match (elts.get(2).map(|x| &x.node), elts.get(3).map(|x| &x.node)) {
@@ -709,14 +709,14 @@ fn rewrite_hist_reads(
                 ) if f == F_WRITES => {
                     let field = keys[*i].name.field_key();
                     let field_ty = Type::fun(domain_ty.clone(), acc_tys[*i].clone());
-                    Some((reg_field_read(reg, reg_ty, field, field_ty), 4))
+                    Some((hist_field_read(hist, hist_ty, field, field_ty), 4))
                 }
                 (Some(TypedExprNode::Proj(ProjKey::Field(f))), _) if f != F_WRITES => {
                     // A tap read ``__hist ≫ variant_project(`commit) ≫ .to_<feed>``:
-                    // its stream type is the mutable variable record\'s field type.
+                    // its stream type is the history record\'s field type.
                     let field = f.clone();
-                    let field_ty = reg_ty_field(reg_ty, &field);
-                    Some((reg_field_read(reg, reg_ty, field, field_ty), 3))
+                    let field_ty = hist_ty_field(hist_ty, &field);
+                    Some((hist_field_read(hist, hist_ty, field, field_ty), 3))
                 }
                 _ => None,
             };
@@ -736,19 +736,17 @@ fn rewrite_hist_reads(
             return;
         }
     }
-    e.walk_children_mut(|c| rewrite_hist_reads(c, h, reg, reg_ty, keys, acc_tys, domain_ty));
+    e.walk_children_mut(|c| rewrite_hist_reads(c, h, hist, hist_ty, keys, acc_tys, domain_ty));
 }
 
-/// The declared type of `field` on the mutable variable record.
-fn reg_ty_field(reg_ty: &Type, field: &str) -> Type {
-    let Type::Record(fs) = reg_ty else {
-        panic!("letrec recognition: reg type is not a record");
+/// The declared type of `field` on the history record.
+fn hist_ty_field(hist_ty: &Type, field: &str) -> Type {
+    let Type::Record(fs) = hist_ty else {
+        panic!("letrec recognition: history-record type is not a record");
     };
     fs.iter()
         .find(|(n, _)| n == field)
-        .unwrap_or_else(|| {
-            panic!("letrec recognition: mutable variable record lacks field `{field}`")
-        })
+        .unwrap_or_else(|| panic!("letrec recognition: history record lacks field `{field}`"))
         .1
         .clone()
 }
diff --git a/src/ccl/scope.rs b/src/ccl/scope.rs
index 53fc5653..0e8a4610 100644
--- a/src/ccl/scope.rs
+++ b/src/ccl/scope.rs
@@ -170,7 +170,7 @@ pub enum ScopedItem<'a> {
     VarRef(&'a Name),
     /// A variable-key *label* occurrence — a [`Transact`](TypedExprNode::Transact)
     /// key or writer footprint entry. Not a variable use: it names a field of
-    /// the mutable variable record the node denotes, so free-variable analyses skip it
+    /// the history record the node denotes, so free-variable analyses skip it
     /// while a consumer that cares about every name a node mentions folds it in.
     KeyRef(&'a Name),
 }
@@ -269,7 +269,7 @@ where
         }
 
         // A mutable variable introduction scopes exactly like a `let`: `init` sits outside
-        // the binder — a seed cannot reference the register it seeds — and
+        // the binder — a seed cannot reference the variable it seeds — and
         // `binding` scopes over `body`, which is where its writes and reads live.
         N::MutDecl {
             binding,
@@ -548,14 +548,14 @@ mod tests {
             }),
             TypedExpr::let_bind("l", var("bound"), var("l")),
             TypedExpr::mut_decl(
-                "reg",
+                "md",
                 Type::History {
                     value: Box::new(Type::Hole),
                     domain: Box::new(Type::Hole),
                     kind: crate::ccl::HistoryKind::Overwrite,
                 },
                 var("seed"),
-                var("reg"),
+                var("md"),
             ),
             node(N::List(vec![var("e0"), var("e1")])),
             case_with_two_branches(),
diff --git a/src/ccl/symbolic.rs b/src/ccl/symbolic.rs
index febb5625..3ad3c7d0 100644
--- a/src/ccl/symbolic.rs
+++ b/src/ccl/symbolic.rs
@@ -366,7 +366,7 @@ fn fmt_inner(expr: &Expr, opts: &SymbolicOpts) -> (Precedence, String) {
         // `transact (k = init, …) { [reads]⇒[writes] over <source> do <body>;
         // … }` — the shared keys with their seeds, then one writer clause per
         // concurrent writer. Reads of a key are the record projection
-        // `__reg.k` elsewhere in the tree, not shown here.
+        // `__hist.k` elsewhere in the tree, not shown here.
         TypedExprNode::Transact { keys, writers, .. } => {
             let key_strs: Vec<_> = keys
                 .iter()
diff --git a/src/ccl/transact_phase.rs b/src/ccl/transact_phase.rs
index b9f08197..def0adbb 100644
--- a/src/ccl/transact_phase.rs
+++ b/src/ccl/transact_phase.rs
@@ -29,15 +29,15 @@
 //!    building the direct fold used; only the assembly below differs.
 //! 2. **partitions** the keys into commit stores ([`partition_keys`]) and
 //!    **assembles** one `LetRec` per store (see [`plan_store`]): one **history** binding
-//!    `reg_k : Txn ⇒ V = λ t → get_prev_txn(view, t, init)` per key — reading
+//!    `hist_k : Txn ⇒ V = λ t → get_prev_txn(view, t, init)` per key — reading
 //!    its writing site's commit stream (or self-guarded for a read-only key) —
 //!    and one **commit-record** binding `commits_j : 𝐼 ⇒ {time, write_targets,
 //!    decision}` per site, whose `decision` is the writer body applied to the
-//!    snapshot `(reg_rk(begin(r)) …, source(r))` of the variables it reads, at commit
-//!    time `begin(r)` (the [`Builtin::BeginTxn`] oracle). The `reg_k ↔
+//!    snapshot `(hist_rk(begin(r)) …, source(r))` of the variables it reads, at commit
+//!    time `begin(r)` (the [`Builtin::BeginTxn`] oracle). The `hist_k ↔
 //!    commits_j` cycle crosses `get_prev_txn` once, so it is guarded.
 //! 3. **places** the stores ([`splice_stores`]), rebinding each key variable still
-//!    named in the continuation from `let x = init` to `let x = as_of_read(reg_x)` over
+//!    named in the continuation from `let x = init` to `let x = as_of_read(hist_x)` over
 //!    its history binding — an as-of read of it, at a position nothing has supplied yet.
 //!    A read fed out of a block that does not write `x` is broadcast over the reading
 //!    loop and, after `channelize`, joined with that loop into an `AsOf` by
@@ -199,12 +199,12 @@ fn first_unpaired_as_of_read(e: &Expr) -> Option<Name> {
 
 /// One as-of read in a reply chain: its `let` binder, the history-binding
 /// reference (the as-of source for a single-variable read — recognition later
-/// rewrites it to a variable-record projection), the variable-record field its
+/// rewrites it to a history-record projection), the history-record field its
 /// history will occupy (`hist.field_key()`, matching recognition's read map),
 /// and the mutable variable's value type.
 struct BoundRead {
     name: Name,
-    reg_read: Expr,
+    hist_read: Expr,
     field: String,
     value_ty: Type,
 }
@@ -215,7 +215,7 @@ struct BoundRead {
 fn as_of_join(expr: &Expr) -> Option<Expr> {
     // Walk consecutive `let kᵢ = final_or_default((⟨histᵢ⟩, _))` bindings —
     // each a bare reference to a live history binding — down to the broadcast
-    // body. Pre-recognition there is no shared mutable variable record: several
+    // body. Pre-recognition there is no shared history record: several
     // mutable variables are several history bindings; the snapshot case rebuilds
     // their record below and recognition collapses it onto the mutable variable.
     let mut reads: Vec<BoundRead> = Vec::new();
@@ -226,14 +226,14 @@ fn as_of_join(expr: &Expr) -> Option<Expr> {
         body,
     } = &cur.node
     {
-        let Some((reg_read, field)) = as_of_read_source(bound_expr) else {
+        let Some((hist_read, field)) = as_of_read_source(bound_expr) else {
             break;
         };
         reads.push(BoundRead {
             name: binding.name.clone(),
-            reg_read: reg_read.clone(),
+            hist_read: hist_read.clone(),
             field,
-            value_ty: reg_read.ty.codomain()?,
+            value_ty: hist_read.ty.codomain()?,
         });
         cur = body;
     }
@@ -301,7 +301,7 @@ fn build_zip_read(
     // The as-of source and the variable-snapshot value type: one mutable variable reads bare,
     // several fold into a record (as in `build_snapshot`).
     let (source, snap_ty) = if used.len() == 1 {
-        (used[0].reg_read.clone(), used[0].value_ty.clone())
+        (used[0].hist_read.clone(), used[0].value_ty.clone())
     } else {
         let record_ty = Type::Record(
             used.iter()
@@ -310,12 +310,12 @@ fn build_zip_read(
         );
         let source_ty = Type::Record(
             used.iter()
-                .map(|r| (r.field.clone(), r.reg_read.ty.clone()))
+                .map(|r| (r.field.clone(), r.hist_read.ty.clone()))
                 .collect(),
         );
         let source = Expr::new(TypedExprNode::Record(
             used.iter()
-                .map(|r| (r.field.clone(), r.reg_read.clone()))
+                .map(|r| (r.field.clone(), r.hist_read.clone()))
                 .collect(),
         ))
         .with_ty(source_ty);
@@ -372,7 +372,7 @@ fn subst_var_with(e: &mut Expr, name: &Name, replacement: &Expr) {
 }
 
 /// Match `as_of_read(⟨hist⟩)` over a **commit-log** history — a bare reference to a
-/// `Txn`-domained letrec history binding — returning the read and the variable-record
+/// `Txn`-domained letrec history binding — returning the read and the history-record
 /// field its history will occupy. `None` for any other bound expression.
 ///
 /// The domain test is the exact `Type::Txn` commit-sequencing domain, not a derived
@@ -383,7 +383,7 @@ fn subst_var_with(e: &mut Expr, name: &Name, replacement: &Expr) {
 fn as_of_read_source(bound_expr: &Expr) -> Option<(&Expr, String)> {
     let TypedExprNode::Apply {
         function: sample_fn,
-        argument: reg_read,
+        argument: hist_read,
     } = &bound_expr.node
     else {
         return None;
@@ -391,13 +391,13 @@ fn as_of_read_source(bound_expr: &Expr) -> Option<(&Expr, String)> {
     if !matches!(&sample_fn.node, TypedExprNode::Builtin(Builtin::AsOfRead)) {
         return None;
     }
-    if !matches!(reg_read.ty.domain(), Some(Type::Txn)) {
+    if !matches!(hist_read.ty.domain(), Some(Type::Txn)) {
         return None;
     }
-    let TypedExprNode::Var(hist) = &reg_read.node else {
+    let TypedExprNode::Var(hist) = &hist_read.node else {
         return None;
     };
-    Some((reg_read, hist.field_key()))
+    Some((hist_read, hist.field_key()))
 }
 
 /// `as_of((trigger, source)) : Fun(B, codomain)`.
@@ -414,7 +414,7 @@ fn build_as_of(trigger: &Expr, source: &Expr, codomain: Type) -> Option<Expr> {
 /// A single-variable as-of read: `as_of((trigger, balance.f))`, bare when the reply
 /// is the identity `read`, else `≫ (λ read → e)`.
 fn build_single(trigger: &Expr, read: &BoundRead, lam_body: &Expr, out_ty: Type) -> Option<Expr> {
-    let as_of = build_as_of(trigger, &read.reg_read, read.value_ty.clone())?;
+    let as_of = build_as_of(trigger, &read.hist_read, read.value_ty.clone())?;
     if matches!(&lam_body.node, TypedExprNode::Var(n) if *n == read.name) {
         return Some(as_of);
     }
@@ -425,9 +425,9 @@ fn build_single(trigger: &Expr, read: &BoundRead, lam_body: &Expr, out_ty: Type)
 /// A multi-variable as-of read: `as_of((trigger, (f_a: ⟨a-hist⟩, f_b:
 /// ⟨b-hist⟩))) ≫ (λ snap → e[kᵢ ↦ snap.fᵢ])` — one snapshot record per
 /// request (§I-c), the reply projecting each mutable variable off it. The source is a
-/// record *literal* of the history-binding reads (the shared mutable variable record
+/// record *literal* of the history-binding reads (the shared history record
 /// does not exist pre-recognition); recognition rewrites each field to
-/// `__reg.f` and then collapses the literal onto the mutable variable itself,
+/// `__hist.f` and then collapses the literal onto the mutable variable itself,
 /// so the engine latches one whole-variable snapshot per request.
 fn build_snapshot(
     trigger: &Expr,
@@ -442,12 +442,12 @@ fn build_snapshot(
     );
     let source_ty = Type::Record(
         used.iter()
-            .map(|r| (r.field.clone(), r.reg_read.ty.clone()))
+            .map(|r| (r.field.clone(), r.hist_read.ty.clone()))
             .collect(),
     );
     let source = Expr::new(TypedExprNode::Record(
         used.iter()
-            .map(|r| (r.field.clone(), r.reg_read.clone()))
+            .map(|r| (r.field.clone(), r.hist_read.clone()))
             .collect(),
     ))
     .with_ty(source_ty);
@@ -578,7 +578,7 @@ struct RawSite {
 /// the target defer, the fresh `to_<defer>` tap field the writer decision's
 /// `` `commit `` payload carries beside `writes`, and the tap value's type. The writer
 /// decision computes the tap value alongside the write set (read-your-writes at
-/// the feed's position); the phase hoists `Feed(defer, __reg ▷ .to_<defer>)`
+/// the feed's position); the phase hoists `Feed(defer, __hist ▷ .to_<defer>)`
 /// into the mutable variable body so `channelize` routes it as an ordinary channel
 /// contribution — mirroring `mut_elim`'s in-loop induction feeds. The tap
 /// commits with the transaction (a denied `` `abort `` contributes no reply, since
@@ -932,8 +932,8 @@ fn fold_cross_domain_loops(expr: Expr, cross_reads: &HashSet<Name>, out: &mut Cr
         // The loop body and the continuation between them carry every reference to
         // this loop's accumulators, so their `Mut(V, D)`s give each one the value
         // type inference joined for it.
-        let reg_vtys = mut_var_value_tys([&*body, &*cont]);
-        let fold = fold_induction_loop(&target, &iter, *body, &reg_vtys);
+        let value_tys = mut_var_value_tys([&*body, &*cont]);
+        let fold = fold_induction_loop(&target, &iter, *body, &value_tys);
         for (i, (acc, vty)) in fold.accs.iter().enumerate() {
             if cross_reads.contains(acc) {
                 let final_var = fold
@@ -1445,16 +1445,16 @@ pub fn check_no_guarded_induction_write_in_block(
 /// continuation spine here supplies ([`Expr::walk_children`] visits `bound_expr` before `body`
 /// for every spine node) and lowering's right-to-left statement chain is not.
 pub fn check_await_final_linearity(expr: &Expr) -> Result<(), String> {
-    fn used_up(reg: &Name) -> String {
+    fn used_up(var: &Name) -> String {
         format!(
-            "`{reg}` is unreferenceable after `await_final({reg})`: the await consumes the \
+            "`{var}` is unreferenceable after `await_final({var})`: the await consumes the \
              mutable variable, declaring its commit history complete",
-            reg = reg.base()
+            var = var.base()
         )
     }
     fn go(e: &Expr, awaited: &mut HashSet<Name>) -> Result<(), String> {
         match &e.node {
-            TypedExprNode::Var(reg) if awaited.contains(reg) => return Err(used_up(reg)),
+            TypedExprNode::Var(var) if awaited.contains(var) => return Err(used_up(var)),
             TypedExprNode::MutWrite { name, .. } if awaited.contains(name) => {
                 return Err(used_up(name));
             }
@@ -1463,14 +1463,14 @@ pub fn check_await_final_linearity(expr: &Expr) -> Result<(), String> {
             TypedExprNode::Apply { argument, function }
                 if matches!(&function.node, TypedExprNode::Builtin(Builtin::AwaitFinal)) =>
             {
-                let TypedExprNode::Var(reg) = &argument.node else {
+                let TypedExprNode::Var(var) = &argument.node else {
                     return Err(
                         "await_final's operand must be a bare mutable variable reference"
                             .to_string(),
                     );
                 };
-                if !awaited.insert(reg.clone()) {
-                    return Err(used_up(reg));
+                if !awaited.insert(var.clone()) {
+                    return Err(used_up(var));
                 }
                 return Ok(());
             }
@@ -1548,9 +1548,9 @@ fn check_store_acyclicity(
         fn direct(e: &Expr, out: &mut Vec<Name>) {
             if let TypedExprNode::Apply { argument, function } = &e.node
                 && matches!(&function.node, TypedExprNode::Builtin(Builtin::AwaitFinal))
-                && let TypedExprNode::Var(reg) = &argument.node
+                && let TypedExprNode::Var(var) = &argument.node
             {
-                out.push(reg.clone());
+                out.push(var.clone());
             }
             e.walk_children(|c| direct(c, out));
         }
@@ -1660,11 +1660,11 @@ fn resolve_writer_free_awaits(e: &mut Expr, written_keys: &[Name]) {
     fn collect(e: &Expr, written_keys: &[Name], out: &mut Vec<Name>) {
         if let TypedExprNode::Apply { argument, function } = &e.node
             && matches!(&function.node, TypedExprNode::Builtin(Builtin::AwaitFinal))
-            && let TypedExprNode::Var(reg) = &argument.node
-            && !written_keys.contains(reg)
-            && !out.contains(reg)
+            && let TypedExprNode::Var(var) = &argument.node
+            && !written_keys.contains(var)
+            && !out.contains(var)
         {
-            out.push(reg.clone());
+            out.push(var.clone());
         }
         e.walk_children(|c| collect(c, written_keys, out));
     }
@@ -1677,8 +1677,8 @@ fn resolve_writer_free_awaits(e: &mut Expr, written_keys: &[Name]) {
     fn rewrite(e: &mut Expr, seeds: &HashMap<Name, Expr>) {
         if let TypedExprNode::Apply { argument, function } = &e.node
             && matches!(&function.node, TypedExprNode::Builtin(Builtin::AwaitFinal))
-            && let TypedExprNode::Var(reg) = &argument.node
-            && let Some(seed) = seeds.get(reg)
+            && let TypedExprNode::Var(var) = &argument.node
+            && let Some(seed) = seeds.get(var)
         {
             *e = seed.clone();
             return;
@@ -2116,7 +2116,7 @@ fn walk_block(
         }
         // Unreachable, as in `splice_block` / `partition_spine`. The rule it would
         // implement is known — the seed enters the read-your-writes environment
-        // exactly as a `Let`'s bound value does — but a block-local register also
+        // exactly as a `Let`'s bound value does — but a block-local mutable variable also
         // needs a decision this pass cannot make alone: whether its writes join the
         // enclosing commit or are private to the block.
         TypedExprNode::MutDecl { .. } => todo!(
@@ -2441,7 +2441,7 @@ fn fun_parts(ty: &Type) -> (Type, Type) {
 ///
 /// Built point-free (a `zip` of two `commits_j` views) rather than as a one-arm
 /// `match` lambda: a `match` covering only `commit` over a two-tag scrutinee is a
-/// width-subtyping error at the strict wall (`` {`commit | `abort} ≮: {`commit} ``),
+/// width-subtyping error at the strict `typecheck` (`` {`commit | `abort} ≮: {`commit} ``),
 /// whereas `variant_project` carries its own stamped type and reads the payload
 /// off the stream directly. The views are pointwise reads of the (guarded) commit
 /// stream, so the references to `commits_j` stay guarded
@@ -2521,7 +2521,7 @@ fn record_field_ty(ty: &Type, field: &str) -> Type {
 
 /// A hoisted in-block feed: the target defer and the tap binding (`Fun(𝐼, V)`
 /// over its site's commit-record stream) whose per-commit values feed it.
-/// `recognize` maps a read of `tap` to the mutable variable record's tap field.
+/// `recognize` maps a read of `tap` to the history record's tap field.
 struct HoistedFeed {
     defer: Name,
     tap: Name,
@@ -2531,19 +2531,19 @@ struct HoistedFeed {
 /// Assemble the transaction `letrec` from the built writers/keys/feeds and
 /// splice it in at the outermost key `let`. Emits, in mutual scope:
 ///
-/// - one **history** binding per key — `reg_k : Txn ⇒ V = λ t →
+/// - one **history** binding per key — `hist_k : Txn ⇒ V = λ t →
 ///   get_prev_txn((view, t, init))`, `view` its writing site's commit stream
-///   (guarded — the `reg_k ↔ commits_j` cycle crosses `get_prev_txn`) or
-///   `reg_k` itself for a read-only key (a self-guarded constant);
+///   (guarded — the `hist_k ↔ commits_j` cycle crosses `get_prev_txn`) or
+///   `hist_k` itself for a read-only key (a self-guarded constant);
 /// - one **commit-record** binding per `with begin():` site — `commits_j : 𝐼 ⇒
 ///   {time, write_targets, decision}`, whose `decision` is the writer body
-///   (verbatim) applied to the mutable variable snapshot `(reg_rk(begin(r)) …,
+///   (verbatim) applied to the mutable variable snapshot `(hist_rk(begin(r)) …,
 ///   source(r))` at the site's commit time, and whose `write_targets` names the
 ///   write-set keys' histories so recognition recovers the writer's write-set;
 /// - one **tap** binding per in-block feed — `commits_j ≫ .decision ≫ .field`.
 ///
 /// The continuation rebinds each key variable's `let x = init` to a
-/// `final_or_default(reg_x, init)` read over its history and hoists each
+/// `final_or_default(hist_x, init)` read over its history and hoists each
 /// in-block feed to `Feed(defer, tap)`. `recognize` inverts this straight into
 /// the `Transact{keys, writers, domain: Txn}` carrier.
 ///
@@ -2676,7 +2676,7 @@ fn plan_store(
         // `commits_j ≫ .decision ≫ variant_project(`commit) ≫ .field`, the
         // per-commit tap stream — the tap rides the (dense) `commit` payload, so
         // eliminate the `` {`commit{𝑃} | `abort} `` decision before the field read.
-        // recognition maps its ref to the mutable variable record's `field` tap. Emitted in
+        // recognition maps its ref to the history record's `field` tap. Emitted in
         // feed (source) order across sites.
         let payload_ty = crate::ccl::ccl_utils::commit_payload_ty(&decision_ty);
         for f in feeds {
@@ -2716,7 +2716,7 @@ fn plan_store(
     let mut hist_bindings: Vec<(TypedBinding, Expr)> = Vec::with_capacity(key_names.len());
     for k in &key_names {
         let v = value_ty(k);
-        let reg_k = hist[k].clone();
+        let hist_k = hist[k].clone();
         let t = Name::fresh("__t");
         let init = key_init.get(k).cloned().expect("key init present");
         // The `get_prev_txn` history slot — the design's denotation: the
@@ -2732,7 +2732,7 @@ fn plan_store(
         // history. The pointwise maps and the union are guarded shapes
         // (`letrec::is_guarded_history_slot` — they change what is read at each
         // position, never which positions the accessor consults), so the
-        // `reg_k ↔ commits_j` cycles still cross the guard.
+        // `hist_k ↔ commits_j` cycles still cross the guard.
         let view_rec_ty = Type::Record(vec![
             (F_TIME.to_string(), Type::Txn),
             (F_WRITE.to_string(), v.clone()),
@@ -2777,7 +2777,7 @@ fn plan_store(
             }
             None => {
                 let ty = history_ty(&v);
-                (tvar(&reg_k, ty.clone()), ty)
+                (tvar(&hist_k, ty.clone()), ty)
             }
         };
         let arg_ty = Type::Tuple(vec![view_ty, Type::Txn, v.clone()]);
@@ -2790,7 +2790,7 @@ fn plan_store(
         );
         let mut lam = Expr::lambda(t, Type::Txn, gpt);
         lam.ty = history_ty(&v);
-        hist_bindings.push((binding(reg_k, history_ty(&v)), lam));
+        hist_bindings.push((binding(hist_k, history_ty(&v)), lam));
     }
 
     // History bindings first, then commit records, then tap views — order is
@@ -3145,16 +3145,16 @@ fn relink_spine_body(mut node: Expr, inner: Expr) -> Expr {
 fn resolve_await_finals(e: &mut Expr, hist: &HashMap<Name, Name>, key_init: &HashMap<Name, Expr>) {
     if let TypedExprNode::Apply { argument, function } = &e.node
         && matches!(&function.node, TypedExprNode::Builtin(Builtin::AwaitFinal))
-        && let TypedExprNode::Var(reg) = &argument.node
-        && hist.contains_key(reg)
+        && let TypedExprNode::Var(var) = &argument.node
+        && hist.contains_key(var)
     {
-        *e = final_key(reg, hist, key_init);
+        *e = final_key(var, hist, key_init);
         return;
     }
     e.walk_children_mut(|c| resolve_await_finals(c, hist, key_init));
 }
 
-/// `final_read(reg_k)` — key `k`'s **terminal read**: its value at the position its own
+/// `final_read(hist_k)` — key `k`'s **terminal read**: its value at the position its own
 /// writers finish. Minted only for a [`Builtin::AwaitFinal`] marker.
 ///
 /// No seed operand, for the same reason [`as_of_read`] has none: this samples the carried
@@ -3168,7 +3168,7 @@ fn final_key(k: &Name, hist: &HashMap<Name, Name>, key_init: &HashMap<Name, Expr
     sampling_read(&hist[k], v, Builtin::FinalRead)
 }
 
-/// `as_of_read(reg_k)` — a key's **as-of read**, awaiting the reading loop
+/// `as_of_read(hist_k)` — a key's **as-of read**, awaiting the reading loop
 /// [`rewrite_as_of_reads`] pairs it with. No seed operand: the sampled position always
 /// has a value, because tick 0 of every store is its keys' seeds.
 fn as_of_read(hist: &Name, value_ty: Type) -> Expr {
diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs
index 90086ac4..760ca45b 100644
--- a/src/ccl/ty.rs
+++ b/src/ccl/ty.rs
@@ -750,7 +750,7 @@ pub enum Type {
     /// reference) and the passes that erase it — the unified phase
     /// (`transact_phase` / `mut_elim`) for `Overwrite` histories, `channelize`
     /// for `Feed` ones. Both erase it to a bare `Type::Fun`; no pass downstream
-    /// may observe a `History` (a survivor at the strict wall is a compiler bug —
+    /// may observe a `History` (a survivor at the strict `typecheck` is a compiler bug —
     /// see `collect_type_errors`). See src/ccl/design/mutability.md.
     History {
         /// The type of the history's value (a position's cell / element). Read
diff --git a/src/interpreter/commit_operator.rs b/src/interpreter/commit_operator.rs
index 623bda98..b102c94e 100644
--- a/src/interpreter/commit_operator.rs
+++ b/src/interpreter/commit_operator.rs
@@ -15,7 +15,7 @@
 //!   *writer input* (a stream of proposals), drains it into the engine on each
 //!   `get`, and renders the store tile. The writer input is wired through a
 //!   `writer_input_setter` so that, in a cyclic graph, the writer can read the
-//!   store back (the operator's own output) before proposing — the `Recurse`
+//!   store back (the operator's own output) before proposing — the cyclic-`FanOut`
 //!   feedback idiom. The store the writer reads carries a watermark, and the
 //!   writer reports the timestamp it observed as its proposal's snapshot.
 //!
@@ -1402,7 +1402,7 @@ impl TileProducer for InductionStoreProducer {
                 // the commit gate), so a fired tap always rides an appended change.
                 // Layout invariant (as on the transaction side): `write_keys` =
                 // carry keys ++ tap keys, so the subtraction never underflows —
-                // a break would wrap `n_reg` to a huge value in release and
+                // a break would wrap `n_carry` to a huge value in release and
                 // mis-index `tap_fired`.
                 debug_assert!(
                     self.write_keys.len() >= self.tap_fields.len(),
@@ -1410,14 +1410,14 @@ impl TileProducer for InductionStoreProducer {
                     self.tap_fields.len(),
                     self.write_keys.len()
                 );
-                let n_reg = self.write_keys.len() - self.tap_fields.len();
+                let n_carry = self.write_keys.len() - self.tap_fields.len();
                 Some(
                     self.write_keys
                         .iter()
                         .cloned()
                         .zip(writes)
                         .enumerate()
-                        .filter(|(i, _)| *i < n_reg || tap_fired[*i - n_reg])
+                        .filter(|(i, _)| *i < n_carry || tap_fired[*i - n_carry])
                         .map(|(_, kv)| kv)
                         .collect(),
                 )
@@ -2179,9 +2179,9 @@ impl TileProducer for StoreDenseReadProducer {
 /// it never changes; later commits only affect *later* trigger positions. The
 /// different-value-per-request behaviour comes from `B` being a multi-position
 /// domain — each position an immutable snapshot — not from a scalar that mutates
-/// (which the immutability invariant forbids). It is the dual of the commit
-/// `Recurse`: `Recurse` latches a private accumulator per *source* step; `AsOf`
-/// latches the store's current value per *trigger* step.
+/// (which the immutability invariant forbids). It is the dual of a store's own
+/// drive: a drive latches an accumulator per *source* step; `AsOf` latches the
+/// store's current value per *trigger* step.
 /// One field of a multi-variable [`AsOf`] snapshot: the record field the reply
 /// projects (`snap.field`), the store's runtime key it samples, and its value
 /// extent.
@@ -2503,8 +2503,8 @@ impl TileProducer for AsOfProducer {
                     Predicate::LessThanEq(Value::UInt(f - 1)),
                 )));
         }
-        // Terminality gate. With the producer-side drive-to-fixpoint retired, this
-        // reader samples one watermark per pull and relies on being re-pulled (via the
+        // Terminality gate. This reader samples one watermark per pull — it does not
+        // drive the store to a fixpoint itself — and relies on being re-pulled (via the
         // writer's wakeup fanning through the cyclic `FanOut`) to converge. So it must stay
         // **non-terminal** until the store itself is terminal, or it could report "done"
         // while the store is still committing and freeze a store no other consumer drives.
@@ -3851,21 +3851,21 @@ impl TileProducer for TransactWriterProducer {
                     // over-fire on a sibling route's commit.
                     // Layout invariant: `write_keys` = carry keys ++ tap keys, so
                     // the subtraction never underflows. Assert it — a break would wrap
-                    // `n_reg` to a huge value in release and mis-index `tap_fired`.
+                    // `n_carry` to a huge value in release and mis-index `tap_fired`.
                     debug_assert!(
                         self.write_keys.len() >= self.tap_fields.len(),
                         "commit operator: tap fields ({}) exceed write keys ({})",
                         self.tap_fields.len(),
                         self.write_keys.len()
                     );
-                    let n_reg = self.write_keys.len() - self.tap_fields.len();
+                    let n_carry = self.write_keys.len() - self.tap_fields.len();
                     let writes: HashMap<Value, Value> = self
                         .write_keys
                         .iter()
                         .cloned()
                         .zip(new)
                         .enumerate()
-                        .filter(|(i, _)| *i < n_reg || tap_fired[*i - n_reg])
+                        .filter(|(i, _)| *i < n_carry || tap_fired[*i - n_carry])
                         .map(|(_, kv)| kv)
                         .collect();
                     // Re-proposing this item at a new frontier supersedes its
@@ -3909,7 +3909,7 @@ impl TileProducer for TransactWriterProducer {
                     }
                     // Otherwise the decision is **not ready**: it reads a broadcast
                     // cross-loop accumulator final still converging — its
-                    // `ExtractFinal` is empty until the sibling loop's `Recurse`
+                    // `ExtractFinal` is empty until the sibling loop's own cycle
                     // drains, one position per body pull. Leaving `last_decided_pos`
                     // unset is the whole handling: this position stays undecided, so
                     // nothing acks the drive row, so the drive's item cursor does not
@@ -4439,8 +4439,7 @@ mod tests {
 
     /// The dense read of a plain (unconditional) accumulator: every position
     /// writes, so `acc := 10; acc += i` over `[1,2,3]` reads `[11, 13, 16]` — a
-    /// dense function with no carries, exactly as the retired `.writes.(index)`
-    /// projection produced.
+    /// dense function with no carries.
     #[test]
     fn dense_read_unconditional_accumulator() {
         assert_eq!(dense_read(&[1, 2, 3], i64::MIN, 10), vec![11, 13, 16]);
@@ -4753,7 +4752,9 @@ mod tests {
     }
 
     /// Repeated writes to one key, each reading the prior commit: every attempt
-    /// commits, the timestamp domain stays dense (the `Recurse` degeneration).
+    /// commits, so the timestamp domain stays dense — the uncontended degeneration
+    /// of allocate-on-commit, where the tick sequence has no gaps because nothing
+    /// ever goes stale.
     #[test]
     fn repeated_writes_to_one_key_are_dense() {
         let mut e = CommitEngine::new(balances(&[("n", 0)]));
diff --git a/src/interpreter/design-operators.md b/src/interpreter/design-operators.md
index efb5e6fc..a5aaf82a 100644
--- a/src/interpreter/design-operators.md
+++ b/src/interpreter/design-operators.md
@@ -366,7 +366,7 @@ Three arms share an input across multiple downstream consumers:
   each tuple / record element; the elements get `Some(fan_out_branch)` and
   combine via [`fan_in`] (function-tiled arms) or [`ScalarFanIn`] (scalar arms).
   The 2-arm Zip-with-const fast path skips the fan-out and emits a single
-  `MapResultToConst` instead. A **store-read arm** (`__reg.k`) is a *leaf*
+  `MapResultToConst` instead. A **store-read arm** (`__hist.k`) is a *leaf*
   source over its own domain, so it is converted with **no** input (rather than
   the fanned branch, which it would reject); `fan_in` co-aligns it with the
   input-driven arms by domain position. This is the cross-domain co-iteration a
@@ -493,7 +493,7 @@ There is one writer over the *full* source: a conditional write's carry position
 change rather than a synthesized same-value write on a complement leg, which is what keeps a
 restricted-source multi-leg realization's cyclic-convergence desync from arising.
 
-**`StoreDenseRead` — the dense changelog read.** A `__reg.k` read folds the changelog at
+**`StoreDenseRead` — the dense changelog read.** A `__hist.k` read folds the changelog at
 *every* position of the loop extent → `Fun(D, V)`: an `IterateExtent(D)` trigger supplies
 the domain positions (a live enumeration — over a `DataSource` it re-reads the arrived keys
 each pull, so it spans live arrivals — and it aligns via `fan_in` with any co-iterated
@@ -529,8 +529,9 @@ position it reads the tap **only if that position's delta actually wrote it**
 **conditional feed** (`if p: out << e`) is the same shape — the letrec phase gives it a
 `to_<defer>__fire` gate (its guard path) and folds that path into the `commit` gate so a
 feed-only position still appends a change carrying the tap. Because the drive is
-position-sorted, the tap stream is position-ordered even over an async source (the dense
-`Recurse` path scrambled it by arrival order — the bug this replaces).
+position-sorted, the tap stream is position-ordered even over an async source — which is the
+property that matters, since an async domain arrives in arbitrary order and a tap read off
+arrival order would scramble the feed.
 
 <a id="remaining-the-never-terminating-bound"></a>
 **Bounding a never-terminating loop (keep-latest changelog GC).** The changelog is bounded
diff --git a/src/interpreter/operator_conversion.rs b/src/interpreter/operator_conversion.rs
index d1c6f2a6..e57505c3 100644
--- a/src/interpreter/operator_conversion.rs
+++ b/src/interpreter/operator_conversion.rs
@@ -106,8 +106,8 @@ pub fn convert_record_fields_to_operators(
             bound_expr,
             body,
         } => {
-            // `let __reg = Transact{…}`: build the shared store and register it
-            // (the reads `__reg.k` in the fields project off it), the same as
+            // `let __hist = Transact{…}`: build the shared store and register it
+            // (the reads `__hist.k` in the fields project off it), the same as
             // the `convert_impl` `Let` arm. Multi-sink programs (a trailing
             // `Record`) reach the store binding through here.
             if let TypedExprNode::Transact {
@@ -246,7 +246,7 @@ struct KeyReadInfo {
     /// The per-commit value extent for [`StoreValueStream`] (`commit` stores
     /// only; the accumulator value extent for induction stores).
     value_extent: Extent,
-    /// The key's position in the writer's `writes` tuple: `__reg.k` projects
+    /// The key's position in the writer's `writes` tuple: `__hist.k` projects
     /// `.writes.(index)` off the store body stream (`Induction` stores).
     index: usize,
     /// Whether the key's value carries forward across commit ticks that don't
@@ -256,8 +256,8 @@ struct KeyReadInfo {
     carry_forward: bool,
 }
 
-/// A built transactional store, registered under its `__reg` binder so each
-/// per-variable read (`__reg.k`) can branch the shared fan and project key
+/// A built transactional store, registered under its `__hist` binder so each
+/// per-variable read (`__hist.k`) can branch the shared fan and project key
 /// `k`. The scalar-read reduction (`final_or_default` → `ExtractFinal`) is
 /// expressed in the CCL, not here.
 struct StoreReadInfo {
@@ -287,9 +287,9 @@ pub struct OpConversionContext {
     scopes: ScopeStack<Name, (Rc<FanOut>, BindingKind)>,
     /// Maps source names to their runtime [`DataSourceDomainExtentImpl`].
     sources: HashMap<String, Rc<RefCell<dyn DataSourceDomainExtentImpl>>>,
-    /// Transactional stores in scope, keyed by their `__reg` binder. A
-    /// `let __reg = Transact{…}` builds the shared store once and mutable variables
-    /// it here; each variable read `__reg.k` projects key `k` off the shared
+    /// Transactional stores in scope, keyed by their `__hist` binder. A
+    /// `let __hist = Transact{…}` builds the shared store once and registers
+    /// it here; each variable read `__hist.k` projects key `k` off the shared
     /// store fan (see [`StoreReadInfo`]). Names are α-unique, so a flat
     /// (unscoped) map suffices.
     transactional_stores: HashMap<Name, StoreReadInfo>,
@@ -377,12 +377,12 @@ impl OpConversionContext {
         self.scopes.lookup(name)
     }
 
-    /// Register a built transactional store under its `__reg` binder.
+    /// Register a built transactional store under its `__hist` binder.
     fn register_store(&mut self, name: Name, info: StoreReadInfo) {
         self.transactional_stores.insert(name, info);
     }
 
-    /// Look up a transactional store by its `__reg` binder.
+    /// Look up a transactional store by its `__hist` binder.
     fn lookup_store(&self, name: &Name) -> Option<&StoreReadInfo> {
         self.transactional_stores.get(name)
     }
@@ -501,8 +501,8 @@ fn convert_impl_inner(
             panic!("Expected no lambdas, got {}", symbolic(expr));
         }
 
-        // `__reg.k` — a read of variable `k` off a transactional store. The
-        // shared store fan was built at `let __reg = Transact{…}`; this
+        // `__hist.k` — a read of variable `k` off a transactional store. The
+        // shared store fan was built at `let __hist = Transact{…}`; this
         // branches it and projects key `k`'s carry-forward stream. A store read
         // is a leaf source (no upstream input).
         TypedExprNode::Apply { argument, function }
@@ -520,10 +520,10 @@ fn convert_impl_inner(
         }
 
         // A bare `Transact` never reaches here: `plan_loops` always binds it as
-        // `let __reg = Transact{…}`, which the `Let` arm intercepts (building
+        // `let __hist = Transact{…}`, which the `Let` arm intercepts (building
         // the shared store and registering it) before compiling `bound_expr`.
         TypedExprNode::Transact { .. } => Err(ConversionError::Unsupported(
-            "Transact must be bound by a `let __reg = …` (recognition invariant), \
+            "Transact must be bound by a `let __hist = …` (recognition invariant), \
              never compiled as a bare value"
                 .into(),
         )),
@@ -546,9 +546,9 @@ fn convert_impl_inner(
             bound_expr,
             body,
         } => {
-            // `let __reg = Transact{…} in body`: build the shared store once
-            // and register it under `__reg`; the variable reads (`__reg.k`)
-            // in `body` project keys off it. `__reg` is never a plain `Var`
+            // `let __hist = Transact{…} in body`: build the shared store once
+            // and register it under `__hist`; the variable reads (`__hist.k`)
+            // in `body` project keys off it. `__hist` is never a plain `Var`
             // use, so it needs no scope binding.
             if let TypedExprNode::Transact {
                 keys,
@@ -639,7 +639,7 @@ fn convert_impl_inner(
                     // arms, function upstream produces function arms.  `fan_in`
                     // picks the matching combinator.
                     //
-                    // A **store-read arm** (`__reg.k`) is a *leaf* source over
+                    // A **store-read arm** (`__hist.k`) is a *leaf* source over
                     // its own domain (empty input), not an iteration-driven
                     // morphism — it must not take the fanned input (it would
                     // reject it). This is the cross-domain co-iteration shape: a
@@ -775,8 +775,8 @@ fn convert_impl_inner(
         // `transact_phase::rewrite_as_of_reads`. `AsOf` folds the raw `Tile::Store`
         // fan directly (via `store_current`), so no `StoreValueStream`
         // intermediary. Two source shapes:
-        //   - `__reg.k` (a bare mutable variable read) → a scalar `AsOf` sampling key `k`;
-        //   - `__reg` (the whole store) → a snapshot `AsOf` sampling every field
+        //   - `__hist.k` (a bare mutable variable read) → a scalar `AsOf` sampling key `k`;
+        //   - `__hist` (the whole store) → a snapshot `AsOf` sampling every field
         //     of the reply's record type at one commit frontier (§I-c), which the
         //     reply then projects.
         TypedExprNode::Apply { argument, function }
@@ -796,7 +796,7 @@ fn convert_impl_inner(
                 )));
             };
             let trigger_op = convert_impl(trigger, None, ctx)?;
-            // A whole-store source (`Var(__reg)`) → snapshot read: the as_of's
+            // A whole-store source (`Var(__hist)`) → snapshot read: the as_of's
             // output codomain is the record of sampled fields.
             if let TypedExprNode::Var(store_name) = &source.node
                 && ctx.lookup_store(store_name).is_some()
@@ -960,7 +960,7 @@ fn convert_impl_inner(
 
         // `GetPrevSeq` is a letrec guard accessor, never compiled directly:
         // pattern recognition (a `get_prev_seq`-causal self-cycle → the
-        // `Recurse` engine) consumes it before op-conversion. Reaching this
+        // induction-store engine) consumes it before op-conversion. Reaching this
         // arm means a `LetRec` group escaped recognition — a compiler bug,
         // reported explicitly rather than falling through to the generic
         // Apply arm. Recognition lands with the unified phase
@@ -1299,7 +1299,7 @@ fn convert_impl_inner(
 
         // A raw `LetRec` never compiles directly: op-conversion *recognizes
         // patterns* in the group (a `get_prev_seq`-causal self-cycle → the
-        // `Recurse` engine, commit-record shapes → the commit operator) and
+        // induction-store engine, commit-record shapes → the commit operator) and
         // an unrecognized group is a compile error, never a silent fallback.
         // Recognition lands with the unified phase
         // (`src/ccl/design/mutability.md`).
@@ -1435,9 +1435,9 @@ fn compile_lit(lit: &Lit) -> Result<Box<dyn TileOperator>, ConversionError> {
     Ok(Box::new(Constant::new(value, extent)))
 }
 
-/// Build the operator graph for a `let __reg = Transact{…}` and return the
-/// [`StoreReadInfo`] registered under the `__reg` binder so each per-variable
-/// read `__reg.k` ([`convert_store_read`]) branches the fan and projects it.
+/// Build the operator graph for a `let __hist = Transact{…}` and return the
+/// [`StoreReadInfo`] registered under the `__hist` binder so each per-variable
+/// read `__hist.k` ([`convert_store_read`]) branches the fan and projects it.
 ///
 /// Op-conversion dispatches on the store's sequencing `domain`: a concrete
 /// iteration extent → the position-driven [`InductionStore`] changelog (an
@@ -1704,7 +1704,7 @@ fn build_induction_store(
 /// `(prev…, item)` input. Mirrors [`build_commit_store`]'s writer setup, but
 /// driven by iteration position — one writer, no conflict, no retry. Reads
 /// register as [`StoreReadKind::InductionChangelog`]:
-/// each `__reg.k` folds the changelog densely over the loop extent via
+/// each `__hist.k` folds the changelog densely over the loop extent via
 /// [`StoreDenseRead`], serving both a scalar-final read (`ExtractFinal` over it)
 /// and a co-iterated read (the dense `Fun(D, V)` itself).
 fn build_induction_store_single(
@@ -1813,7 +1813,7 @@ fn build_induction_store_single(
     let set_body = store.body_input_setter();
     // Cyclic: the drive reads this store's changelog back to recover each
     // position's previous accumulator, so one fan branch feeds the cycle and the
-    // rest serve the downstream `__reg.k` dense reads.
+    // rest serve the downstream `__hist.k` dense reads.
     let fan = Rc::new(FanOut::new_cyclic(Box::new(store)));
     let drive = InductionDrive::new(
         fan.branch(),
@@ -1831,7 +1831,7 @@ fn build_induction_store_single(
     })
 }
 
-/// Resolve an `as_of` read's `source` — a bare mutable variable read `__reg.k`
+/// Resolve an `as_of` read's `source` — a bare mutable variable read `__hist.k`
 /// off a registered commit store — to the raw store fan branch, its runtime key,
 /// and the key's value extent. `AsOf` folds the [`Tile::Store`] fan directly (via
 /// `store_current`), so the as-of path takes the fan + key rather than
@@ -1842,7 +1842,7 @@ fn as_of_store_source(
 ) -> Result<(Box<dyn TileOperator>, Value, Extent), ConversionError> {
     let bad = || {
         ConversionError::Unsupported(format!(
-            "as_of source must be a bare store mutable variable read `__reg.k`, got {:?}",
+            "as_of source must be a bare store mutable variable read `__hist.k`, got {:?}",
             source.node
         ))
     };
@@ -1907,7 +1907,7 @@ fn as_of_snapshot_fields(
         .collect()
 }
 
-/// The `(store, field)` of a `__reg.field` read on a registered store, if `e` is one.
+/// The `(store, field)` of a `__hist.field` read on a registered store, if `e` is one.
 /// The same shape the generic `Apply`/`Proj` arm matches, factored out so the
 /// `FinalRead` arm can recognise its own operand.
 fn as_store_read(e: &Expr, ctx: &OpConversionContext) -> Option<(Name, String)> {
@@ -1955,7 +1955,7 @@ fn convert_store_final_read(
     )))
 }
 
-/// Compile a per-variable read `__reg.field` off a registered transactional
+/// Compile a per-variable read `__hist.field` off a registered transactional
 /// store. `plan_loops` wraps a scalar accumulator read in `final_or_default(stream,
 /// init)`, so the current/final value (via [`ExtractFinal`]) is selected
 /// downstream, not here. A surface `await_final` is not this read — it is
@@ -2344,7 +2344,7 @@ fn field_extent_of(record_extent: &Extent, field_name: &str) -> Result<Extent, C
 // `scalar_tile_to_column_value` later in the pipeline.  Filtering here
 // keeps that caller from ever seeing a function-typed argument.
 /// Whether a `zip` arm is a **leaf source** over its own domain — a store read
-/// `__reg.k` or an `as_of((trigger, store))` read — rather than an
+/// `__hist.k` or an `as_of((trigger, store))` read — rather than an
 /// iteration-driven morphism. Such an arm is converted with *no* input (it would
 /// reject the fanned iteration input); `fan_in` co-aligns it with the
 /// input-driven arms by domain position. This is the cross-domain co-iteration
@@ -2352,7 +2352,7 @@ fn field_extent_of(record_extent: &Extent, field_name: &str) -> Result<Extent, C
 /// combining the request with a store read (`zip((trigger, as_of(store)))`).
 fn is_leaf_zip_arm(expr: &Expr, ctx: &OpConversionContext) -> bool {
     match &expr.node {
-        // `__reg.k` — a store read.
+        // `__hist.k` — a store read.
         TypedExprNode::Apply { argument, function }
             if matches!(&function.node, TypedExprNode::Proj(ProjKey::Field(_))) =>
         {
diff --git a/src/interpreter/tile_operators/fanout.rs b/src/interpreter/tile_operators/fanout.rs
index 631f22a3..bf7d6dca 100644
--- a/src/interpreter/tile_operators/fanout.rs
+++ b/src/interpreter/tile_operators/fanout.rs
@@ -31,7 +31,8 @@ struct FanOutReentrancy {
     cached_tile: Tile,
     /// Re-entrancy guard for the inner subscribe path.  `FanOutBranch::subscribe`
     /// of one branch can transitively trigger `subscribe` on a sibling
-    /// (e.g. the loop body's `acc_var` reads close back through `Recurse`).
+    /// (e.g. an induction loop's drive subscribes to its store branch while
+    /// the store is subscribing the body that reads the drive).
     /// The re-entrant call sees this set, skips the inner subscribe (the
     /// outer call is doing it), and just returns a `FanOutProducer`.
     subscribing_inner: bool,
diff --git a/src/interpreter/tile_operators/union.rs b/src/interpreter/tile_operators/union.rs
index 85a96ffa..72890553 100644
--- a/src/interpreter/tile_operators/union.rs
+++ b/src/interpreter/tile_operators/union.rs
@@ -75,7 +75,7 @@ impl UnionOperator {
             codomains[0].clone()
         } else {
             // Differing arms get merged into one column, so each must fit in one:
-            // a `Scalar`, or a `Record` of them — a compound register's arms are
+            // a `Scalar`, or a `Record` of them — a compound mutable variable's arms are
             // the latter and disagree on *layout* (a constructed tuple arrives as
             // a record of columns, the carried snapshot as one column of record
             // values), which `flat_merge` reconciles by rebuilding the column at
diff --git a/tests/cli_driver_convergence.rs b/tests/cli_driver_convergence.rs
index ceb0b5a0..7fa2af5e 100644
--- a/tests/cli_driver_convergence.rs
+++ b/tests/cli_driver_convergence.rs
@@ -1,5 +1,5 @@
 //! The CLI driver contract: a notification-gated drive loop (as in
-//! `src/main.rs`) must converge a mutation-loop accumulator, whose `Recurse`
+//! `src/main.rs`) must converge a mutation-loop accumulator, whose store/drive
 //! cycle advances one position per pull and requests its own re-pull through the
 //! scheduler's deferred-wakeup queue.
 //!
@@ -88,8 +88,9 @@ fn drive_scalar_int(code: &str) -> i64 {
 }
 
 /// The reported bug: a finite induction accumulator must converge through the
-/// notification-gated driver. Its `Recurse` cycle self-requests re-pulls until
-/// terminal; before the wakeup queue this spun forever.
+/// notification-gated driver. Its store/drive cycle self-requests re-pulls until
+/// terminal — without the wakeup queue nothing would re-pull it, since a
+/// non-terminal tile alone does not make the driver come back.
 #[test]
 fn accumulator_converges_via_notification_gated_driver() {
     assert_eq!(
diff --git a/tests/compilation_pipeline/generators_udf_poly.rs b/tests/compilation_pipeline/generators_udf_poly.rs
index 20d7bdd2..d14e8ae9 100644
--- a/tests/compilation_pipeline/generators_udf_poly.rs
+++ b/tests/compilation_pipeline/generators_udf_poly.rs
@@ -165,7 +165,7 @@ fn test_generator_function(#[case] code: &str, #[case] expected: Tile) {
 // mutates a pre-loop variable (`total += item`) and yields its updated
 // value each iteration, producing a running-total stream.  This routes
 // through the causal `LetRec` the unified phase emits (recognized onto the
-// `Transact` carrier, then `Recurse`), with the yield-defer hoisted out as a
+// `Transact` carrier, then the induction store), with the yield-defer hoisted out as a
 // `to_*` feed field on the history record.
 #[rstest]
 #[timeout(Duration::from_secs(10))]
diff --git a/tests/compilation_pipeline/helpers.rs b/tests/compilation_pipeline/helpers.rs
index 2eb45088..75610073 100644
--- a/tests/compilation_pipeline/helpers.rs
+++ b/tests/compilation_pipeline/helpers.rs
@@ -64,8 +64,8 @@ pub(crate) fn run_pipeline_with_ctx(ctx: &mut GlobalContext, code: &str) -> (Exp
         .expect("pipeline test expects a `main` output");
     // A single `get` is not always enough to fully drain a producer.  Some
     // tile operators advance their internal state by one step per pull
-    // (notably the mutation-loop `Recurse` cycle, where each pull of the
-    // body op records one more position into the recurrence cache).
+    // (notably a mutation loop's store/drive cycle, where each pull decides one
+    // more position of the recurrence).
     // Loop until the producer reports a terminal tile, with a generous
     // iteration cap to catch the regression where the cycle stops making
     // progress without converging.
diff --git a/tests/compilation_pipeline/mutability.rs b/tests/compilation_pipeline/mutability.rs
index 26a51b79..9e070428 100644
--- a/tests/compilation_pipeline/mutability.rs
+++ b/tests/compilation_pipeline/mutability.rs
@@ -1376,7 +1376,7 @@ fn non_mut_redef_shadows_mut_param_fn_lowers_tupled() {
 /// Regression: a `Mut`-param `def` local to a nested scope (here a function
 /// body) must not leak its curried call shape to a same-named top-level `def`.
 /// Statement blocks lower right-to-left, so the top-level `bump(3, 4)` call is
-/// lowered *after* `outer`'s body mutable variables a nested `Mut`-param `bump`; without
+/// lowered *after* `outer`'s body registers a nested `Mut`-param `bump`; without
 /// block-scoping the leak made that call lower curried against the 2-tuple
 /// top-level `bump`. `r = bump(3,4) = 7`; `outer(100)` bumps `y` once then adds
 /// 100 → 101; total 108.
diff --git a/tests/compilation_pipeline/sources_incremental.rs b/tests/compilation_pipeline/sources_incremental.rs
index 1e9ba6bc..727380a7 100644
--- a/tests/compilation_pipeline/sources_incremental.rs
+++ b/tests/compilation_pipeline/sources_incremental.rs
@@ -503,11 +503,9 @@ fn test_incremental_global_aggregate() {
     );
 }
 
-/// Mutation loop summing values from an incremental source, semantically
-/// equivalent to `sum(source1())` but exercising `Recurse` instead of
 /// A *conditional* induction write over an async source: `if i > 15: x := x + i`.
-/// An async (`DataSourceDomain`) extent routes to the dense `Recurse` path, which
-/// cycles on `.writes` (not `.commit`). The writer decision is *carry-complete*
+/// An async (`DataSourceDomain`) extent routes to the changelog induction store.
+/// The writer decision is *carry-complete*
 /// (`writes.x = Case[i > 15 → x + i; true → x]`), so a rejected position carries the
 /// previous accumulator rather than accumulating unconditionally — the guard is
 /// honored by the value, not silently dropped. Source `[10, 20, 30]`, guard `> 15`:
@@ -562,7 +560,7 @@ x";
 /// `InductionStore` drives the source by *absolute position* (an async domain
 /// arrives unordered), so the feed's per-position stream is position-ordered —
 /// loop position `p` sees `cnt = p + 1`, not a value scrambled by arrival order
-/// (the dense `Recurse` path's bug this replaces). Source `[10, 20, 30]` → the
+/// rather than by arrival. Source `[10, 20, 30]` → the
 /// feed maps `{0 ↦ 1, 1 ↦ 2, 2 ↦ 3}`.
 #[test_log::test]
 fn test_incremental_tap_loop() {
@@ -613,7 +611,7 @@ o";
     );
 }
 
-/// `MapAggregate`.  Verifies that `Recurse` correctly:
+/// `MapAggregate`.  Verifies that the induction cycle correctly:
 /// - Re-reads its `domain` input as the source grows in batches.
 /// - Holds back the final emission until the source signals it's done.
 /// - Fires notifications when each batch arrives and again on terminal.
diff --git a/tests/compilation_pipeline/transactions.rs b/tests/compilation_pipeline/transactions.rs
index fb09b05f..a8e82550 100644
--- a/tests/compilation_pipeline/transactions.rs
+++ b/tests/compilation_pipeline/transactions.rs
@@ -1024,7 +1024,7 @@ fn await_final_bound_then_read_in_a_feed_loop_stays_final() {
 
 /// Bound to a name and used downstream: the await need not be the program's tail.
 /// The letrec splice moves above the `let` that reads the history binding, which is
-/// what keeps `reg_pool` in scope there.
+/// what keeps `hist_pool` in scope there.
 #[test]
 fn await_final_bound_then_computed_with() {
     check_tile(
@@ -1274,8 +1274,8 @@ fn await_final_of_an_induction_accumulator_rejected() {
 /// The shape a single program-wide store made impossible: `b`'s seed names `a`'s
 /// completion, so with one store `b`'s tick-0 value would await the store `b` itself
 /// writes. No block mentions `a` and `b` together, so they partition into two stores
-/// and the dependency is an ordinary one-way edge between two letrecs — `reg_a` bound
-/// outside, `reg_b`'s seed reading it. `a` reaches 1 + 1 = 2, seeding `b`, which
+/// and the dependency is an ordinary one-way edge between two letrecs — `hist_a` bound
+/// outside, `hist_b`'s seed reading it. `a` reaches 1 + 1 = 2, seeding `b`, which
 /// reaches 3.
 #[test]
 fn a_mut_var_seeded_from_another_store_s_final_value() {
@@ -1502,7 +1502,7 @@ fn registers_written_in_one_block_share_a_store() {
 
 /// **Snapshot consistency** holds a store together too, and writes alone do not show it:
 /// nothing writes both mutable variables, but one block reads both, latching them at a
-/// single frontier, so they must come from one mutable variable record. The writers are
+/// single frontier, so they must come from one history record. The writers are
 /// exactly those of `unrelated_mut_vars_get_separate_stores` — only this read is added.
 ///
 /// The read stays a `with begin():` block because it *is* the subject; what is dropped is
@@ -1528,7 +1528,7 @@ fn mut_vars_read_together_share_a_store() {
     assert_eq!(commit_stores(code), vec!["Txn[a,b]"]);
 }
 
-/// A register a *writing* block reads to decide its commit is read at that commit's
+/// A mutable variable a *writing* block reads to decide its commit is read at that commit's
 /// snapshot, so the read alone pulls it into the store — no write to `limit` is
 /// needed. (`limit` is never written, so it is a read-only key of the store. The key
 /// order is the block's footprint order, which is where the guard reads them, not the
@@ -1886,8 +1886,9 @@ fn a_read_only_mentioned_key_completes_while_a_live_writer_runs() {
 // Read rules and rejected shapes
 // ---------------------------------------------------------------------------
 
-/// A transactional mutable variable may be read only inside a `with begin():` block; a
-/// bare read outside one is rejected with a hint to wrap it in a block.
+/// A transactional mutable variable may be read only inside a `with begin():` block, and
+/// that is permanent rather than a current limitation (the CHL spec, "8.3 Reads"). The
+/// diagnostic names both legal reads: wrap it in a block, or `await_final` it.
 #[test]
 fn bare_txn_read_outside_tx_rejected() {
     check_compile_error(
@@ -1901,6 +1902,27 @@ fn bare_txn_read_outside_tx_rejected() {
     );
 }
 
+/// The gate follows a `Mut(_, Txn)` **parameter** into the callee: a by-reference pass is
+/// the one mention lowering lets through, and it hands the callee a mutable variable in
+/// its own right, so a read of it there obeys the same rule. Reading only inside a block
+/// is permanent (the CHL spec, "8.3 Reads"), so it holds through a function boundary as
+/// well as at the top level.
+#[test]
+fn bare_read_of_a_mut_param_outside_a_block_rejected() {
+    check_compile_error(
+        indoc! {r#"
+            def draw(p: Mut(Int, Txn), amt):
+                before = p
+                with begin():
+                    p := p - amt
+            pool: Mut(Int, Txn) := 100
+            draw(pool, 10)
+            await_final(pool)
+        "#},
+        "read transactional variable `p` inside a `with begin():` block",
+    );
+}
+
 /// A *computed* live cross-endpoint read (`resp << latest + 1`) compiles: the
 /// pre-lambda-elim as-of-read rewrite turns it into `as_of(…) ≫ (λ x → x + 1)`,
 /// whose reply lambda the elim pass point-frees. Running the rewrite before
@@ -2198,18 +2220,18 @@ fn induction_write_inside_begin_block_rejected() {
 
 /// A *guarded* induction write in a **mixed** block — one that *does* commit a
 /// transactional mutable variable — is rejected. `check_no_induction_only_transactions`
-/// passes (the block commits `reg`), but the guarded `cnt += 1` is not liftable
+/// passes (the block commits `total`), but the guarded `cnt += 1` is not liftable
 /// by `partition_spine` and would be silently dropped from the decision record.
 /// A dedicated pre-check (`check_no_guarded_induction_write_in_block`) catches it.
 #[test]
 fn guarded_induction_write_in_mixed_block_rejected() {
     check_compile_error(
         indoc! {r#"
-            reg: Mut(Int, Txn) := 0
+            total: Mut(Int, Txn) := 0
             cnt: Mut(Int) := 0
             for x in [1, 2, 3]:
                 with begin():
-                    reg := reg + x
+                    total := total + x
                     if x >= 2:
                         cnt := cnt + 1
             cnt
@@ -2277,17 +2299,17 @@ fn txn_writer_called_inside_block_rejected() {
 /// PR-2 registry leak (same class as PR-1's mutable-registry leak): a
 /// `Mut(_, Txn)` mutable variable declared *inside* a `def` body must not leak into the
 /// transactional registry and falsely gate a like-spelled top-level local. The
-/// def-body scope snapshots and restores *both* mutable variable registries, so `reg`
+/// def-body scope snapshots and restores *both* mutable variable registries, so `v`
 /// outside `f` is an ordinary local (assignable, readable).
 #[test]
 fn txn_mut_var_in_def_body_does_not_leak_to_outer_local() {
     check_scalar(
         indoc! {r#"
             def f(x):
-                reg: Mut(Int, Txn) := 0
+                v: Mut(Int, Txn) := 0
                 x
-            reg = 5
-            reg
+            v = 5
+            v
         "#},
         cambra::interpreter::Value::Int(5),
     );
@@ -2491,7 +2513,7 @@ fn commit_decision_reads_induction_accumulator() {
 /// trailing read, which is an arbitrary as-of sample — so the committed values
 /// are deterministic: `pool` draws down `100 → 97 → 94` over commit ticks 1, 2.
 /// Exercises the writer's deferred-wakeup convergence: the broadcast `cnt`'s
-/// `ExtractFinal` is empty until its loop's `Recurse` drains, so the writer
+/// `ExtractFinal` is empty until its loop's own cycle drains, so the writer
 /// re-arms itself on the wakeup queue each not-ready pull rather than deadlocking
 /// on the stalled commit frontier; the in-block reply demands each commit and
 /// drives that convergence.
@@ -2546,7 +2568,7 @@ fn broadcast_read_races_a_second_writer() {
 }
 
 /// Broadcast off a finite **async** (data-source) sibling loop. `cnt` counts a
-/// `TestDataSource`'s three elements — a loop whose `Recurse` converges only as
+/// `TestDataSource`'s three elements — a loop that converges only as
 /// the source's data arrives (via scheduler notifications), not synchronously.
 /// The txn decision reads `cnt`'s value (broadcast, 3), observed via an in-block
 /// reply — one commit, `pool = 100 − 3 = 97` at commit tick 1. This is the case
diff --git a/tests/compilation_pipeline/variants.rs b/tests/compilation_pipeline/variants.rs
index 22b475bf..84b984b9 100644
--- a/tests/compilation_pipeline/variants.rs
+++ b/tests/compilation_pipeline/variants.rs
@@ -979,15 +979,15 @@ fn test_pipe_is_still_logical_or(#[case] code: &str, #[case] expected: Value) {
     check_scalar(code, expected);
 }
 
-/// A **variant-valued mutable register**.
+/// A **variant-valued mutable variable**.
 ///
-/// A register's seed and its writes are *alternatives at one position*, exactly as a
-/// conditional's arms are, so the register's value space is their **join** — and
-/// every emission has to be built at that joined space rather than at the width of
-/// whichever alternative occurred. A `` `none `` seed with `` `some `` writes is the two-tag
-/// sum with the arm that did not occur left empty; building a column from the
-/// surviving value alone would carry only its own tag and fail to conform to the
-/// register's own tiling.
+/// A mutable variable's seed and its writes are *alternatives at one position*,
+/// exactly as a conditional's arms are, so the variable's value space is their
+/// **join** — and every emission has to be built at that joined space rather than at
+/// the width of whichever alternative occurred. A `` `none `` seed with `` `some ``
+/// writes is the two-tag sum with the arm that did not occur left empty; building a
+/// column from the surviving value alone would carry only its own tag and fail to
+/// conform to the variable's own tiling.
 ///
 /// The variant elimination stack covers that law at the `ExtractFinal` boundary (its
 /// two emission paths *are* the seed and the writes). These are the surface
@@ -1034,7 +1034,7 @@ for i in [1, 2, 3]:
 acc",
     union("none", Value::Unit)
 )]
-// No annotation: the register's variant type is inferred from seed and writes.
+// No annotation: the variable's variant type is inferred from seed and writes.
 #[case(
     r"
 acc := `some(0)
@@ -1052,7 +1052,7 @@ for i in [1, 2, 3]:
 acc",
     union("some", Value::Int(3))
 )]
-fn test_variant_valued_register(#[case] code: &str, #[case] expected: Value) {
+fn test_variant_valued_mut_var(#[case] code: &str, #[case] expected: Value) {
     check_scalar(code, expected);
 }
 
diff --git a/tests/programs/http_counter/mod.rs b/tests/programs/http_counter/mod.rs
index a56a7c36..2db0fc17 100644
--- a/tests/programs/http_counter/mod.rs
+++ b/tests/programs/http_counter/mod.rs
@@ -70,7 +70,7 @@ fn http_computed_live_read() {
 /// A *multi-variable* live cross-endpoint read: `GET /get` replies `a + b`,
 /// reading **two** live mutable variables in one block. Snapshot consistency (§I-c)
 /// requires both reads to come from one commit snapshot — served by a single
-/// bundled `as_of((trigger, __reg))` folding the whole store at one frontier,
+/// bundled `as_of((trigger, __hist))` folding the whole store at one frontier,
 /// the reply projecting each mutable variable off the latched snapshot record. A `POST
 /// /set` writes both mutable variables, so `a + b` reflects the latest committed values.
 #[test]
diff --git a/tests/type_check.rs b/tests/type_check.rs
index bc0e5391..67c7c9ac 100644
--- a/tests/type_check.rs
+++ b/tests/type_check.rs
@@ -996,7 +996,7 @@ fn a_never_called_function_over_a_source_is_typechecked(
 }
 
 /// Deadness is the absence of a *demand*, not of a specialization: a use can be
-/// reached and still mutable variable nothing. Registering nothing is what the memo records,
+/// reached and still register nothing. Registering nothing is what the memo records,
 /// so reading deadness off the memo walks the definition of a binding that is very
 /// much used — reporting its body's defect a second time, from its own nodes.
 ///
@@ -2629,7 +2629,7 @@ mod binder_slot_records_the_bound_at_type {
     /// A bare `_` declares nothing, so `b: _ = a` binds exactly where `b = a`
     /// does: at the mutable variable's *value*. Such an initializer reads through before
     /// any annotation is consulted, so `_` needs no special handling — and a `Let`
-    /// cannot bind a register at all.
+    /// cannot bind a mutable variable at all.
     #[test]
     fn a_let_never_binds_a_mut_var() {
         for code in [