Split transactional commit stores by connected components of transaction blocks

[dpmills]

Two for loops over := accumulators have always compiled to two induction stores, one letrec each. Two with begin(): loops over unrelated Mut(_, Txn) variables compiled to one commit store, because transact_phase unioned every writer site's footprint into a single key set. That coupled two things that should be independent: their commit clocks, and their completion. The second is observable — a store is terminal only when every writer has drained, and a fed-out read is an AsOf, non-terminal until its store is — so a finite variable's trailing read could not settle if any unrelated variable had a live-source writer. This partitions the keys, giving the transaction path one store per set of variables some block actually relates.

Planning and placement come apart

build_letrec becomes plan_store plus splice_stores. A store sits below everything its bindings need and above everything reading its keys; each spine statement gets a level — 0 if it reads no store, else one past the last store it reads, transitively — and rides inside that store. A statement cannot read two stores at once, which is what makes the level well-defined: reading two variables together is a block, and the partition put those keys in one store precisely so the read has one snapshot. CrossDomain wraps the whole nest, since an accumulator a decision reads must be outside every store reading it.

Both mutability paths ended in the same four steps — trailing reads, feed hoists, causality assert, LetRec — now mut_elim::close_recurrence_group. It puts the assert where neither caller can forget it, and states as load-bearing an ordering both had right by coincidence: a read hoisted over a feed would break channelize's outermost-first collection silently.

Tests

Nine, four of them asserting the planned graph rather than only values — two programs can agree on every number and differ in store count. a_finite_mut_var_completes_despite_a_live_unrelated_writer is the payoff, checked against the base rather than assumed: there the read yields empty forever. Recognition and op-conversion needed no changes.

[dpmills]

This change is part of the following stack:

• Freshening asks a different question than type_level, so it needs its own #71
  • SharedHole: let lowering state that two type positions are the same #72
    • Traits: state what an operator requires of its operands, not that they are the same #73
      • Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
        • Annotations stop standing in for binder structure, and stop outliving inference #60
          • Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63
            • A mutable variable read is an explicit operation, not a subtyping rule #64
              • Split transactional commit stores by connected components of transaction blocks #91 ◀
                • Build the await_final terminal read as a completion-point sample, and give the as-of read its own term #92
                  • Feed both writers' decision bodies through tiles, retiring WriterBuffer #93
                  • Add an end-to-end walkthrough of mutability, from CHL source to operators #97
                  • Close a commit store's keys individually, so an await waits only for its own variable's writers #102
                  • Retire the reg and Recurse names, and pin the out-of-block read rule #106

_{Change managed by git-spice.}