Retire the reg and Recurse names, and pin the out-of-block read rule

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

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 } => {

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` /

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");

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.