Split transactional commit stores by connected components of transaction blocks

docs/chl-spec.md

@@ -2636,6 +2636,12 @@ interleaved (or parallel) otherwise. The events:
 
 Consequences a program may rely on:
 
+- **Commit order is not global.** Two `with begin():` blocks are ordered
+  relative to each other only if they mention a mutable variable in common —
+  a shared variable is what makes one block's commit visible to the other.
+  Blocks with no variable in common are **unordered**: nothing in the
+  language imposes an order between them, and their transactions interleave
+  freely. Two independent `for` loops relate their accumulators the same way.
 - **Commit order is not lexical order.** Two `with begin():` blocks do
   **not** commit in the order they appear in source; each block's position
   is fixed by its trigger event (a source arrival, or the loop index for a

src/ccl/design/mutability.md

@@ -503,6 +503,73 @@ mutable variables and channels they target. Generators survive inlining because
 leaves nothing to lose — a generator body is `For` + `Feed` nodes against an implicit result feed,
 substituted wholesale.
 
+### How many commit stores a program has
+
+**One per set of mutable variables a `with begin():` block relates** — not one per program, and
+not one per mutable variable. `transact_phase::partition_keys` computes the partition; each part
+becomes its own `LetRec`, its own `Transact{domain: Txn}`, and its own `CommitOperator`. The
+induction path partitions the same way: `mut_elim::transform_loop` emits one letrec per loop.
+
+A block is what forces mutable variables together, for two reasons that coincide on the block's
+footprint. The store is not a user-facing concept: the
+[CHL spec's ordering model](../../../docs/chl-spec.md#85-ordering-and-concurrency) says only that
+two blocks are ordered when they mention a mutable variable in common, and that blocks sharing no
+variable are unordered. The partition is how that is realized — a program never has to reason
+about it.
+
+- **Atomicity.** A writing block produces one commit record, so every key it *writes*
+  advances at one tick, and every key it *reads* is read at that tick's snapshot.
+  `{reads ∪ writes}` is therefore one store — which is why the `limit` a guard consults is
+  in the same store as the `total` it guards, though nothing writes `limit`.
+- **Snapshot consistency.** A read-only block's reads are latched at one frontier, which
+  `rewrite_live_reads`'s `build_snapshot` realizes by handing `AsOf` a single mutable variable
+  record. Keys read together must be in that record. Such a block is *unwrapped* onto the
+  spine and leaves no `WriterSite`, so `strip` keeps its footprint explicitly
+  (`Stripped::read_only_footprints`).
+
+Nothing else forces sharing. Two consequences are observable:
+
+- **Completion.** A store reports terminal only once all of its writers have drained,
+  and a fed-out read is an `AsOf`, non-terminal until its store is. So a finite mutable
+  variable's trailing read settles even while an unrelated mutable variable has a live-source
+  writer (`a_finite_mut_var_completes_despite_a_live_unrelated_writer`).
+- **Commit clocks.** Unrelated mutable variables share no commit order, so nothing imposes an
+  interleaving between transactions that never interact.
+
+A mutable variable **no block writes at all** is not a key of any store, and relates nothing by
+being read. Nothing can advance it — the lowering write gate admits a mutable variable write only
+inside a block, and a block write would put it in a write set — so its history is constant at its
+seed and every read of it is that seed. It keeps its introduction on the spine. Only a read-only
+footprint reaches this case: `limit` above is unwritten too, but a *writing* block reads it, which
+makes its value a question about a commit snapshot rather than about a constant.
+
+**Placement.** `plan_store` plans each store (its keys' history bindings, its writers'
+commit records, its taps) and `splice_stores` places them in one spine walk. A store's
+letrec sits below everything its bindings need — a writer's iteration source, chiefly —
+and above everything that reads its keys. Each spine statement gets a **level**: 0 if it
+reads no store, else one past the last store it reads, transitively through statements
+already carried. Level 0 keeps its place above every letrec; the rest ride inside the
+store they read. A statement cannot read two stores at once, which is what makes the
+level well-defined — reading two mutable variables together is a block, and the partition put
+those keys in one store so the read has one snapshot to come from.
+
+"Reads a store" means *names anything that store's body binds*: a key, a history binding, or a
+**defer fed inside the store** — either an in-block feed, whose tap the store's body binds, or
+the feed of a read-only block, carried in as an effect statement. The defer has no fallback: a
+key left above the letrec would still find its seed introduction, whereas a defer fed only inside
+the store exists nowhere else. That is also why an effect statement counts for the transitive
+step — it binds no name, but it contributes to one.
+
+The folded cross-domain induction loops (`CrossDomain`) wrap the **whole** nest: an
+accumulator a commit decision reads must be bound outside any store that reads it, and
+outermost satisfies that for all of them at once (`a_cross_domain_read_coexists_with_a_second_store`
+pins the nesting).
+
+Both paths close a group through one shared routine, `mut_elim::close_recurrence_group`
+— trailing reads, then feed hoists, then the causality assert, then the `LetRec`. The two
+differ in how they *find* their bindings and where the group is spliced, not in how a group
+is closed.
+
 ### mut_elim: eliminating overwrite mutability
 
 Input: a typed, inlined, surface-CCL tree. Output: pure CCL (`let`/`letrec` algebra) with every

src/ccl/lower/stmts.rs

@@ -745,8 +745,8 @@ pub(super) fn lower_middle_stmt(
             Ok(ctx.tag_machinery(Expr::expr_stmt(effect, body), stmt.span, "lower.stmt_seq"))
         }
         // A standalone `with begin():` transaction — one commit over a
-        // synthesized singleton source, `transact_phase` folds it into the
-        // shared commit store (see src/ccl/design/mutability.md).
+        // synthesized singleton source, which `transact_phase` folds into the commit
+        // store holding the mutable variables it touches (see src/ccl/design/mutability.md).
         ChlStmt::With { .. } => lower_standalone_transaction(stmt, body, ctx),
         // Parse-recovery placeholder: silently drop the broken statement and
         // pass the continuation through. See `ChlExpr::Error`.

src/ccl/mut_elim.rs

@@ -582,6 +582,50 @@ fn hist_field_view(
     comp
 }
 
+/// Close a recurrence group: wrap `cont` in `letrec { bindings } in <feed hoists>
+/// in <trailing reads> in cont`.
+///
+/// Both mutability paths end at this shape, which is why it lives here rather than in
+/// either: an induction loop and a transaction store differ in how they *find* their
+/// bindings (one loop's accumulators, versus every writer site's footprint) and in where
+/// the group is spliced, not in how a group is closed. Both supply:
+///
+/// - `bindings` — the guarded history bindings (plus, for a transaction, its
+///   commit-record and tap bindings), whose causality is asserted here so neither
+///   caller can forget to;
+/// - `reads` — one `let x = final_or_default(⟨history⟩, init)` per key, the trailing
+///   read that reduces a history to the value the continuation names. Prepended in
+///   reverse so the first is outermost;
+/// - `feeds` — the in-group feeds to route ([`hoist_feeds`], whose source-order
+///   invariant this preserves by hoisting *outside* the reads).
+///
+/// The nesting order is load-bearing and shared: feeds outermost, then reads, then
+/// the continuation. A read may not be hoisted over a feed — `channelize` collects
+/// feeds outermost-first — and a feed's view names only group bindings, never a read.
+pub(crate) fn close_recurrence_group(
+    bindings: Vec<(TypedBinding, Expr)>,
+    reads: Vec<(TypedBinding, Expr)>,
+    feeds: Vec<(Name, Expr)>,
+    cont: Expr,
+) -> Expr {
+    let mut body = cont;
+    for (b, def) in reads.into_iter().rev() {
+        body = Expr::let_in(b, def, body);
+    }
+    let body = hoist_feeds(body, feeds);
+    debug_assert!(
+        check_letrec_causal(&bindings).is_ok(),
+        "mutability phase emitted a non-causal group: {:?}",
+        check_letrec_causal(&bindings)
+    );
+    let ty = body.ty.clone();
+    Expr::new(TypedExprNode::LetRec {
+        bindings,
+        body: Box::new(body),
+    })
+    .with_ty(ty)
+}
+
 /// Wrap `body` in one `Feed(defer, view)` per collected in-body feed, so
 /// `channelize` routes each per-position value stream to its channel. Each
 /// `view` is the feed's value stream over its contributing domain — for an
@@ -696,22 +740,12 @@ fn transform_loop(target: TypedBinding, iter: Expr, loop_body: Expr, cont: Expr)
     for (acc, x_final) in &fold.renames {
         rename_uses(&mut cont, acc, x_final);
     }
-    let mut body_out = rewrite(cont);
-    for (b, def) in fold.reads.into_iter().rev() {
-        body_out = Expr::let_in(b, def, body_out);
-    }
-    body_out = hoist_feeds(body_out, fold.feed_views);
-    let bindings = vec![fold.binding];
-    debug_assert!(
-        check_letrec_causal(&bindings).is_ok(),
-        "letrec phase emitted a non-causal group"
-    );
-    let ty = body_out.ty.clone();
-    Expr::new(TypedExprNode::LetRec {
-        bindings,
-        body: Box::new(body_out),
-    })
-    .with_ty(ty)
+    close_recurrence_group(
+        vec![fold.binding],
+        fold.reads,
+        fold.feed_views,
+        rewrite(cont),
+    )
 }
 
 /// An induction loop folded into a single decision-factored history binding,