Record a NodeId-keyed lineage table as a byproduct of each rewrite

[groundlar]

Provenance so far is a log of rewrite steps folded at a boundary. This replaces it with a NodeId-keyed table: one row per node, holding its parents, its blame, and an interned rule tag. Identity is the key; parentage and attribution are columns. Then it extends the recorded domain to refinement predicates, which is where the interesting problems were.

Stacked on #98 (Clone freshens) and #101 (one substitution engine).

The table

A driver brackets each rewrite by node identity — lineage::enter(slot_id, …) returning a #[must_use] guard — and the nodes minted under that bracket row on the slot. Nothing is declared: a pass never names what it destroys, so there is no region to over-claim and no fate to predict. Deaths are a set difference at the boundary, recorded ∖ live, taken over rows and never over the key space.

Copy rather than Transform is what makes adopt-a-live-subtree expressible: a rewrite that keeps a node's id while wrapping one of its children must not declare that node dead.

Predicates enter the recorded domain

collect_tree_ids now reaches refinement predicates — through type slots, user_annotation, and Cast targets — so the fold must explain them. That splits two questions which previously had one answer, and the design doc now leads with the split:

• Explanation — which ids must the fold account for? The main tree and its predicates.
• Uniqueness — may two live nodes share an id? The main tree only. assert_unique_node_ids stays narrow, because a predicate interior legitimately aliases a main-tree id at inline's blind spot.

A refinement predicate is program text the user wrote — [x for x in xs if x > k] puts x > k in one — so it deserves the same attribution as any other node. The "cost, accepted" the design doc used to record, a guard error reporting without a caret because its id was not in the projection, is exactly what this buys back.

Three crossings have to record. Entry and transformation are done here. Raising — planning materializing a predicate back into the main tree — is not, and is deliberately left: those nodes are minted below the last pane, so no boundary gates them. It lands with the planning commit.

What that surfaced

Monomorphization was recording nothing at all. frame.def.clone() sat 22 lines above the mono.specialize frame. Since Clone freshens (#98), the clone is what fires on_copy, so every pair fell on the floor: 28 unexplained nodes, and Mono absent from the recorded passes entirely. Two pinned expectations move as a result, both in the right direction — the transaction fixture gains Mono, and the boundaries deriving edges go 7 → 16, a strict superset.

A predicate rebuild is a replacement or a derivation depending on the caller's reach. A predicate is an Rc shared across many type slots, so a rewrite cannot mutate through it — every rebuild builds a new Rc and repoints the refinement it was handed. That is a replacement only if the walk reaches every occurrence; otherwise the original survives on a type the walk never visits, and preserving ids puts one id-set on two simultaneously-live terms.

Nothing about predicates is special here — it is the same replace-versus-derive question the main tree has. Sharing is what makes the answer depend on the caller rather than on the operation. So PredMemo carries the intent: PredMemo::replacing() keeps ids and uniquify is the only caller entitled to it, because it walks the whole tree. Everyone else freshens, bracketed on the source predicate's root.

uniquify's entitlement is asserted, not assumed — a tripwire beside the existing id-multiset one censuses distinct predicate terms (deduped by Rc pointer) before and after the walk and requires N in, N out, same ids.

Predicate id collisions: 33 → 0, now asserted rather than pinned.

Nine substitution sites, each decided by one question — does this code create a new node? rewrite_expr_go takes &mut TypedExpr and edits the node already in the tree, so nothing new exists. apply_expr_inner returns a new one, so it is bracketed on the node it derives from. Discharge payloads keep their ids because a payload is a template: it only feeds apply_type, and as_expr clones it afresh at every occurrence it fills.

Preserving shrinks to what it can justify

Every clone_preserving_ids site was audited with the id savings measured, which moved five to recording:

site	preserved	verdict
fan_out_copy keep-first + chained-compare operands	302 ids, subtrees of 1–5	record
register-init stash	20 ids, subtrees of 1–3	record
apply_expr's early returns	—	record: the result is a new node the caller owns while e stays live
try_lift_defer	2484 ids, subtrees to 19	keep

The lowering sites already had a copy_frame for their other arm, so freshening made both arms identical — this deletes the keep-first bookkeeping outright, including the used: &mut bool threaded recursively through float_comp_source_case.

One justification was retired as simply wrong: "freshen it and the later placements row on an id nothing ever recorded" conflates freshening with not recording. A freshened copy made inside a frame is recorded like any other; the requirement is only that a copy is not an unrecorded mint.

re_root deleted

mut_elim's use was a defect rather than churn: Expr::let_in mints, and the re-root then overwrote that id — a phantom birth, the exact thing preserve exists to make unrepresentable. Now Expr::preserve.

subst's use was necessary but wastefully spelled. It carries the occurrence's id onto the replacement root so a user-written read site keeps its span, but clone().re_root(id) minted a root, recorded a Copy for it, and discarded both — one stranded id and row per substituted occurrence. clone_at builds the root at the carried id while node.clone() still freshens the children. Nothing is stranded.

With both converted, re_root had no users. Its doc also claimed "a clone mints nothing", false since Clone began freshening.

State

Every gated leak class is zero on all 22 pane boundaries. Full suite green, clippy clean.

Known and deliberate: planning's predicate work is untouched (it is the largest remaining body — 775 rewrites over 8825 nodes — and belongs with the planning commit), and predicate uniqueness is asserted only by the new test rather than by a boundary check.

---

Rebased onto main (7a9d1201)

Upstream's #91 (commit stores split by connected components of transaction blocks)
and #92 (await_final terminal reads) rewrote most of transact_phase, so the
recording was re-adopted onto the new structure rather than merged textually.

Ported. build_letrec → plan_store (now per store) and splice_letrec →
splice_stores/walk_spine, carrying transact.commit_record,
transact.history, transact.key_rebind and transact.carrier with them.
key_init threads MutVarDecl through upstream's by-reference signatures.
StorePlan::carrier_slot names each store carrier's slot on the same argument the
single carrier used — the outermost key declaration among its keys. A store's
planned bindings are moved out of the borrowed plan with clone_preserving_ids
rather than freshened, so the finer commit_record / history attribution
survives placement instead of being re-parented wholesale onto the carrier.

Newly bracketed, because the rewrites are new: transact.await_final (the
terminal read a marker becomes) and transact.await_final_seed (a writer-free
key's seed, inlined for its await).

Two recording gaps the audit surfaced, both closed. Neither is new to the
rebase; both were invisible before the window change below.

• fold_cross_domain_loops called mut_elim::fold_induction_loop with no frame
  open, so the entire folded letrec __hist — its binding, trailing reads, feed
  hoists, and the per-accumulator views a commit decision reads acc(r) through —
  was an unrecorded mint. That was ~46 unexplained nodes on every program with a
  cross-domain induction loop. Now transact.cross_domain_fold, with
  wrap_cross_domain bracketing each folded loop's carrier on the statement it came
  from (transact.cross_domain_group, via a slots column index-parallel with
  bindings) and the shared body wrappers on the outermost
  (transact.cross_domain_body).
• mut_elim::flatten_spine mints in two of its arms — the writer-body hoist and a
  terminalized value-position write — and runs at the top of mut_elim::run,
  before any frame. Now letrec.hoist_writer_body and letrec.terminalize_write.
  Its other arms already preserved ids deliberately and are untouched.

CAMBRA_LINEAGE_AUDIT=full now ends at the last instrumented pane
(post-inference..post-as-of-read) instead of join-planned. An audit measures
what the brackets explain, so a window running past the last instrumented pass
counts everything the uninstrumented tail mints as a defect — a number that cannot
reach zero however correct the recording is. That made the audit read as a broken
gate rather than a measurement, and it buried both gaps above in planning's noise.
The endpoint is meant to move to post-lambda-elim and then join-planned in
the commits that instrument those passes; provenance.md now says so at the
window, and the glossary entry on windows says why.

Renames following upstream: the post-live-read boundary is
post-as-of-read; the transact.live_read rule is transact.as_of_read.

State, measured on the restacked stack

Full suite green; fmt clean; clippy clean in debug, release, serde and lib-only.

window	Unexplained	ParentUnknown
letrec (post-inference..post-letrec), predicate interiors live	0 / 581	0 / 581
full (post-inference..post-as-of-read), predicate interiors live	6 / 577	6 / 577

The full residue is all channelize — ending the window at post-desugar
instead accounts for every one of the 6. Channelize's adoption here is scoped to
the defer cluster, and closing the rest is not done in this PR.

With the narrow live set (no CAMBRA_LINEAGE_PREDICATES=1) the letrec window
reports ParentUnknown on 166 of 581 windows, which is the predicate-interior
crossing provenance.md already documents: this commit's PredMemo derives and
records rather than preserving, so a rebuilt predicate's parents are
predicate-interior ids the narrow set excludes. Admitting them is what closes it,
as that section predicts.

Numbers carried over and not re-taken: the "33 → 0" predicate-collision count,
the "all 22 pane boundaries" count, and the 1184-ParentUnknown predicate-domain
residue quoted in provenance.md (measured at the old full span — the doc now
says so inline). The pane-boundary leak gate itself
(pane_boundaries_fold_with_no_structural_leaks, Unexplained == 0 and
ParentUnknown == 0 at both boundaries over its corpus) passes on the restacked
stack; it is the count that was not re-counted.

---

Rebased onto main (7e31f0f2), after #98 and #101 merged

Both landed as squashes, so the stack's own hygiene and subst commits are not
ancestors of main; the three subst commits were dropped as redundant (verified
first: free_among, discharge_env_in_place, both arrow tests, and the removal of
subst_var_with/subst_env are all present on main). #114 (refinements and
function-def output types) also landed underneath.

Where upstream's merged version and this stack had both rewritten the same thing,
upstream's won on two counts where it reached the same conclusion more cleanly:
fan_out_copy dropping its keep-first used flag, and the chained-comparison
operand(i) closure. provenance.md's ### The id domain is now ### Walking the ids, following upstream's rename, with the citations retargeted.

Channelize is instrumented

The previous round left 6 windows leaking, all in channelize, and reported them
rather than fixing them. They are fixed. Two rewrite arms in desugar_inner minted
outside any frame — the defer lift (lift_defer splices the outer body into the
inner scope's tail) and the defer-returning-let collapse (which copies the inner
scope out of the borrowed tree). Both replace the let they match, so both are
bracketed on it: channelize.defer_lift and channelize.defer_collapse.

The audit's default live set now matches the gate's

materialize_panes takes every pane's live set with collect_tree_ids, which is
predicate-inclusive; the audit defaulted to the narrow collect_main_tree_ids
and so reported edges the gate does not. A recorded predicate rebuild's parents are
input-tree predicate interiors, which the narrow set omits from the input side, so
those edges dangled as ParentUnknown with nothing unrecorded — ~166 windows of
noise on a plain invocation, which is exactly where real defects hide.
CAMBRA_LINEAGE_PREDICATES is now on by default, =0 to narrow.

CAMBRA_LINEAGE_GATE=1 — the gate's corpus is the suite

The always-on gate (pane_boundaries_fold_with_no_structural_leaks) samples
eleven programs listed in corpus(). That sample is what let two recording
gaps live — transact_phase calling mut_elim::fold_induction_loop with no frame
open, and flatten_spine's value-position writer hoist — because neither shape is
among the eleven. With this flag every compile folds its own pane boundaries and
gates them, so the corpus is whatever the caller compiles. CI turns it on.

It gates gated_boundaries() rather than both, on the same argument as an audit
window's endpoint: the first boundary spans monomorphization and inference, and
inference's predicate producers do not record — specialize_use clones a
definition per instantiation and the predicate copies inside it row against
interior ids no pass produced. That is 5 programs over
tests/compilation_pipeline, all UDF-with-filter or poly-wrapper shapes, and all
of it the crossing "Known prerequisites" already records. Gating it today would
pin a constant, not catch a regression; it joins gated_boundaries() in the commit
that makes inference record.

Cost, debug, alternating runs on a warm build: the pipeline binary goes
0.97 s → 1.07 s (min-of-6; +~0.10 s, ~+9%), and the whole suite 3.21 s → 3.36 s
(min-of-3; +~0.15 s, ~+4%).

State

Full CI green with DEEP_TYPECHECK=1 CAMBRA_LINEAGE_GATE=1. Every instrumented
audit window is zero on a plain invocation, no flags:

window	span	Unexplained	ParentUnknown
letrec	post-inference..post-letrec	0 / 584	0 / 584
mutelim	post-transact..post-letrec	0 / 584	0 / 584
full	post-inference..post-as-of-read	0 / 580	0 / 580

CAMBRA_LINEAGE_AUDIT=planning reports 39 / 48 over 580 — lambda_elim and
planning, which the upstack commits instrument and which the full endpoint
deliberately stops short of.

---

Third commit: the recording vocabulary is plain English now

The docs carried two bespoke words for one idea — a rewrite "bracketed" its
products, and the OpenStep holding them was a "frame". Neither means anything
outside this subsystem, and "frame" was already spoken for four other ways in the
tree (stack frames, solver specialization frames, scope frames, type-morphism
frames). A rewrite now records, what it opens is a recording, and the RAII
value is a guard. Prose, doc comments and assertion strings only — no item is
renamed, so copy_frame, FrameGuard and OpenStep keep their spellings and the
diff stays reviewable. The eight #[test] names spelling it the old way are
renamed too, having no callers and being otherwise the last "bracket" standing.

Mining the abandoned doc pass turned up claims that had rotted into saying the
opposite of the code, which is the part worth reviewing:

• provenance.md said lambda_elim and planning bracket their rewrites.
  Neither does — lambda_elim opens no recording at all, planning only via
  planning/iterate. That is the same false claim this PR has been working
  around.
• It said the predicate domain is unrecorded and PredMemo::rebuild fires no
  hook — directly contradicting the commit immediately below it, which records
  against predicate.rebuild. What actually remains unrecorded is planning
  raising a predicate back into the main tree.
• Nature's doc claimed Expansion had no production producer; there are 16.
• lineage.rs described a SourceKey → NodeId projection. No such type; both
  domains are NodeId.
• Two RewriteLabel doc examples named labels appearing nowhere in the tree.
• The lowering projection was documented as excluding refinement-predicate
  interiors. It uses collect_tree_ids, which includes them.
• Three doc links pointed at deleted items (flush_bracket, freshen_node_id,
  freshen_clone_node_ids) — invisible to rustdoc, the items being pub(crate).
• Drifted counts: simplify's wrapped rules (thirteen, cited two different wrong
  ways), the TODO(preserve) sites, the interned rule triples.

NodeId::as_u64 is deleted — no caller anywhere, the serde wire impl reads
the field directly, and being pub on a pub type nothing warned. The comment
above the wire impl now says why there is no accessor instead of pointing at one.

Pass::Uniquify and Pass::LambdaElim are left in place, documented as not yet
constructed, since they are constructed upstack.

Gates

Every ci.sh target green, including clippy_release, clippy_serde and
clippy_lib (the serde one matters here, since as_u64 sat next to the wire
impl), and DEEP_TYPECHECK=1 CAMBRA_LINEAGE_GATE=1 ./ci.sh test. The audit windows
are unchanged at zero: letrec and mutelim 0/584, full 0/580.

[dpmills]

Sounds like FrameGuard should be RecordingGuard

[dpmills]

How is "slot" different from "parent"?

[dpmills]

Defining "predicate interior" to mean a type of node ID is a confusing definition. Does this really need a term? Just writing "NodeIds inside refinements" when those need to be referenced feels just as good and doesn't involve new terminology

[dpmills]

Looks like this is reverting a bunch of edits you made downstack

[dpmills]

All four of these paragraphs are misplaced. They aren't defining terms, and this is the terms section. Looks like this is stuff about what automated verification we have; it probably belongs in a section at the end, or maybe alongside whichever section introduces the invariant that is being checked.

Also, it looks like the content might be stale. It references exceptions for refinements

[dpmills]

Why are provenance and lineage two separate things? The contents of provenance.rs aren't even "provenance" in the colloquial sense; it's just node identity. Can we drop one of these two terms entirely?

[dpmills]

What happens if you create multiple recording guards against the same nodeID? For example, maybe we create something blamed to a node, then later transform that same node into new nodes? Do we maintain the proper edges?

[dpmills]

If this isn't a leak, why is it in the Leak enum?

[dpmills]

How is ParentUnknown different from Unexplained? Seems like you would hit them the same way: when you see a row in the LineageTable where the parent doesn't exist. Is the difference whether we discovered the node by looking at the LineageTable or by walking the AST and comparing against the LineageMap? That doesn't seem like a particularly important distinction, but if it is, these need better names since that is very non-obvious from either the names or the comments.

If we don't care about the distinction, then this entire Leak enum can be deleted

[dpmills]

If this is an inflight recording, should it be called InflightRecording?