T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgraph gate

src/v4/DECISIONS.md

@@ -50,7 +50,7 @@ authority location(s) and moves to Part 1.
 | **D1** | The structural-delta vocabulary over `Node` (side-session 2026-05-15; **shape refined** per codex P2 REQUEST_CHANGES on PR #3162). An `Edit` replaces the subtree at a `Path` with a `Node` (term-rewriting `t[s]p`). `Path = List<Symbol>`: each step descends the `Named` edge keyed by that opaque `Symbol` — flat & finite, NOT a new recursive type (A1); resolution = `Symbol` equality ⇒ K-1-clean. Name is **`Path`** (the route), not `Position` (operator pick); "position/occurrence" (JSON Pointer, RFC 6901, member-name tokens only) retained as anchor. **No positional/ordinal selector** (P2 finding 1): an `Int` ordinal admits negative/illegal indices = the representable-illegal-state node.dag designed out at `EdgeLabel`; positional-connective children are reached by replacing the enclosing `Named` subtree (the safe over-fire #3157 blesses); surgical positional addressing is a future operator-ratified extension (consumes-nothing root has no ordinal primitive — no kernel `Nat`; recursive Peano = A1 STOP). **`Diff` = ORDERED `List<Edit>` applied SEQUENTIALLY** (P2 finding 2): no set / pairwise-independence / "parallel positions" invariant, no `diff_well_formed`/`paths_independent` — any `List<Edit>` is a valid rewrite program; a non-resolving Edit ⇒ fail-closed Diagnostic at apply time (operational, not a type-level illegal state); `apply_diff` is a fold, all-or-nothing. **DATA TYPES in `std/node.dag`** (B1/`Hash` precedent: a structural delta over `Node` is substrate-tier; corrects the initial "owner = T-21" read). **OPERATIONS** (`subterm_at`/`apply_diff` → `Result<Node, Diagnostic>`) in **`lens/application.dag`**, FORCED: `std/diagnostic.dag` already `Consumes std/node.dag` (`Correction = Suggested(Node)`) so a node.dag op returning `Result<_,Diagnostic>` is a substrate cycle — the node.dag "consumers fail-close" discipline (`node_well_formed` precedent). `apply_diff` consumer = CLI / test harness / user app code. Two refinements of the in-session ratification were encoded via PR #3162 review (the normal confirm/redirect channel — not an open fork): (a) the data/op split (operations in `application.dag`, forced by the diagnostic→node cycle); (b) the P2-driven shape change — no positional selector (Practice-4 dissolved; receipt in `std/node.dag`) and sequential `Diff` (no independence predicate). Operator redirect, if any, is via the PR like any change | this row + `std/node.dag` Path/Edit/Diff declarations + `lens/application.dag` operation contract + `lens/affected_set.dag` cross-ref |
 | **B-4** | affected_set R2 minimality contract (side-session 2026-05-15). For `lens/affected_set.dag` (T-21) to compute a *minimal* re-exec frontier, `compiler/04_infer.dag` resolution must be **NODE-PRECISE**: a use-site name-reference `Atom` binds to the **exact declaration `Node`**, never merely its module/scope (**carrier corrected** per a P2/Practice-3 review finding on #3162). The use→def fact's named forward carrier is the post-resolution opaque **`Symbol`** (K-1) on the name-ref `Atom`, **NOT `resolved_type`** (that is the node's *type* — many declarations share a type, so it is lossy for binding identity; citing it was the P2/Practice-3 error). AUTHORITY = `compiler/03_resolve.dag` (it owns identifier→declaration binding; resolution canonicalizes a use-site `Atom`'s `Symbol` to equal its binder's `Symbol`, so binding = `Symbol` equality — the K-1-granted op, node.dag `name_occurrences`). `04_infer` is **preserve-only** (must not alter/drop the resolved `Symbol`; no 5th `InferredFacts` field — IR-1-safe). `lens/affected_set.dag` **derives** the graph by `Symbol`-equality traversal over the resolved tree (same "derive, don't store" as `content_hash`/D1). Coarse (module/scope) resolution leaves affected_set *correct but maximally over-firing* — so node-precision is a **precision INVARIANT on T-9**, the dominant gate on R2 minimality, not a T-21 concern. Distinct axis from #3157's hash-granularity "over-fire = safe" tolerance (content identity vs dependency-edge granularity). No new type/field; IR-1-safe | this row + `compiler/03_resolve.dag`; `compiler/04_infer.dag` is a boundary index only |
 | **B-5** | affected_set R1 usefulness contract (side-session 2026-05-15). For purity-aware skipping to be *useful* (not merely correct), effect must be a **per-`Arrow`-Node fact** derived from that node's signature (the B3 authority) and **never aggregated to a coarser unit** (one ambient `IO`, per-module effect set) — a coarse aggregate is the parallel taxonomy B3 forbids (P2) *and* degrades R1 to "re-run ~everything" (still correct/fail-closed, useless). A **granularity invariant**, not effect-lens strength (effects are READ off the signature per B3 ⇒ strong by construction; the only risk is coarse modeling — this forbids collapsing the per-effect-KIND distinction the signature already carries). No new field. = #3153 Ex.R1, now encoded. **Corollary (effects-as-parameters, 2026-05-16):** effects are threaded as explicit parameters (DI-by-construction); a mock-injected unit test's B-4 edge points at the mock `Node`, so affected_set skips it and re-runs only real-carrier (integration) tests *automatically* — "affected" is consumer-relative with no unit/integration mode in the lens. Ambient/global effects re-couple the cone = the anti-pattern this forbids. Honest boundary: a re-run test with changed behavior may have a stale expected value; the lens surfaces "re-run", never rewrites the expectation (no-engine) | `lens/effect.dag` B-5 block (+corollary) + `docs/design-affected-set-lens.md` worked examples |
-| **#3153-subsumed** | `v4-affected-set-design` (#3153, no worker) is **superseded by this branch** (operator 2026-05-15): `docs/design-affected-set-lens.md` remains the prose design authority for the affected-set lens (design framing + 5 worked examples + dimension-aware/fail-closed exclusion discipline); `lens/affected_set.dag` owns only the terse machine-readable T-21 carrier/read surface under the strict de-prose rule. The branch-specific Ex.R1/Ex.R2/Ex.R3 labels are not a second prose authority; they are reconciled here to the now-*encoded* reciprocal contracts — Ex.R1→B-5 (`effect.dag`), Ex.R2→B-4 (`04_infer.dag`), Ex.R3→B-3 (the drafted #3157 B1-CANON point-3 correction). Dogfood-reality is tracked by the T-21 scaffold trigger rather than copied into the `.dag` file. IRT reconciliation (operator 2026-05-17): the eventual `AffectedSetRead.read` body must prune at unchanged/pure `content_hash` boundaries, expand the frontier as a pure parallel fold over the DAG, and make TestClaim result reuse the cache-dual keyed by the input subgraph `content_hash`; a whole-program traversal scaffold is rejected. Practice-4 coproduct classification: `ExclusionProof` is 🟡 scaffold; named trigger = promote or dissolve when the T-21 read body and `.dag` TestClaims prove the exclusion evidence cases. `FrontierDecision` is 🟢 terminal: it is the per-`ExclusionKey` outcome coproduct that makes rerun-vs-excluded mutually exclusive while leaving node identity solely on the key path resolved against the input `Dag`. #3153 carried no new file/type; close it as superseded | `docs/design-affected-set-lens.md` + `lens/affected_set.dag` carrier surface |
+| **#3153-subsumed** | `v4-affected-set-design` (#3153, no worker) is **superseded by this branch** (operator 2026-05-15): `docs/design-affected-set-lens.md` remains the prose design authority for the affected-set lens (design framing + 5 worked examples + dimension-aware/fail-closed exclusion discipline); `lens/affected_set.dag` owns only the terse machine-readable T-21 carrier/read surface under the strict de-prose rule. The branch-specific Ex.R1/Ex.R2/Ex.R3 labels are not a second prose authority; they are reconciled here to the now-*encoded* reciprocal contracts — Ex.R1→B-5 (`effect.dag`), Ex.R2→B-4 (`04_infer.dag`), Ex.R3→B-3 (the drafted #3157 B1-CANON point-3 correction). Dogfood-reality is tracked by the T-21 scaffold trigger rather than copied into the `.dag` file. IRT reconciliation (operator 2026-05-17): the decomposed `AffectedSetRead` model (`boundary_hash_receipt`, `changed_dimension_receipt`, `proven_transitive_changed_subgraph_frontier`, `propagation_receipt`) plus top-level `affected_set(read_model, dag, diff)` must prune only at unchanged/pure `content_hash` boundaries, seed every proven changed dimension for each edit, fold an edit-aware proven transitive changed-subgraph frontier over the DAG, and make TestClaim result reuse the cache-dual keyed by the input subgraph `content_hash`; a whole-program traversal scaffold is rejected. Practice-4 coproduct classification: `ExclusionProof` is 🟡 scaffold; named trigger = promote or dissolve when the T-21 `affected_set` fold and `.dag` TestClaims prove the exclusion evidence cases. `HashReceipt` is 🟡 scaffold; named trigger = dissolve into B1 `content_hash` plus B-5 purity/effect receipts when those reads are substrate-produced. `BoundaryReceipt` is 🟡 scaffold; named trigger = dissolve when T-21 `.dag` TestClaims prove boundary prune/expand/unknown cases. `ChangedDimensionReceipt` is 🟡 scaffold; named trigger = dissolve when per-edit dimension deltas are generated from D1 edits and B-5 effect dimensions. `PropagationReceipt` is 🟡 scaffold; named trigger = dissolve when B-4/B-5 edge receipts are generated. `ReExecFrontier` is 🟢 terminal: it is the IRT-1 whole-DAG-vs-changed-subgraph gate, with `WholeDagFailClosed` making conservative all-rerun structurally exclusive from changed-subgraph decisions. `FrontierAcc` is 🟢 terminal internal fold state because it mirrors `ReExecFrontier` authority during ordered `Diff` accumulation and lowers directly through `frontier_from_acc`. `FrontierDecision` is 🟢 terminal: it is the per-`ExclusionKey` outcome coproduct that makes rerun-vs-excluded mutually exclusive while leaving node identity solely on the key path resolved against the input `Dag`; when multiple changed producers hit the same key, `Rerun` absorbs `Excluded` so the aggregate cannot under-rerun. #3153 carried no new file/type; close it as superseded | `docs/design-affected-set-lens.md` + `lens/affected_set.dag` carrier surface |
 | **PROOF-1** | **External trust-discharge for A3** (operator-ratified 2026-05-15; *not the north star — placed & designed early like AGENT-1*). gunbc's structural evidence (A2 termination descent, the algebra-homomorphism epistemic chain, cost, effects) is EMITTED as a machine-checkable proof term in an external prover (Lean/Coq); their small independently-audited KERNEL checks it. Converts A3's named seed-trust axiom into an INTERSUBJECTIVE check against an anchor gunbc does not own. Does NOT make gunbc un-gameable — the external kernel + the evidence→proof-term faithfulness are the NEW named axioms; it MOVES trust to a stronger anchor (same Trusting-Trust honesty A3 observes). Constraints: the lens EXPORTS witnesses gunbc already has, the prover only KERNEL-CHECKS, never searches (no-engine + A2 "checker not discoverer"); discharges only what is structurally GROUNDED (ungroundable ⇒ fail-closed Diagnostic — inherits gunbc's honesty boundary). Realized as (evidence read) ⊕ (B2-OMNI emit to a `lean`/`coq` language model — ordinary targets). The PROOF-1 *framing* (#3158) added **NO new file** — it was framing-only and explicitly DEFERRED the prover model ("realized when a lean/coq model lands"); that model **subsequently lands as `extdeps/languages/lean.dag` per B-2/L-4** (operator-ratified closed-tree extension — see the **L-4** row). No contradiction: framing = no file; the deferred model's later arrival is the L-4 extension | `STRUCTURE.md` §7 (A3 home) + `workflow/bootstrap.dag` A3 block + `TASKS.md` T-15 note; cross-ref A2 / AGENT-1 / B2-OMNI / **L-4** |
 | **C5-2** | **emit-locality** (operator-ratified 2026-05-16) — `emit` is *structurally local*: a subtree's emitted form depends only on that subtree + a bounded declared context, so a D1 `apply_diff` at Path p re-emits ONLY p's subtree; everything outside p is unchanged by construction. **Locality is Node-relative, NOT file-relative** (operator code-as-data steer: the substrate anchors no semantic on the file concept — a "file" is a convenience projection only; stability = content_hash of the emitted *subtree*, never file bytes). Non-local emit decisions are DECLARED normalizations at the smallest *enclosing Node scope* (never "file scope" — there is no file in the model). Load-bearing: AGENT-1/D1 "faithful re-emit" is unprovable from global `ingest∘emit=id_Node` (C5-1) alone — locality is the stronger separate property; the C5↔D1 hinge | this row; `compiler/05_emit.dag` is a boundary index only; cross-ref C5 / C5-fidelity / D1 |
 | **T-9** | **infer keystone contracts** (operator-ratified 2026-05-16). **A — Find decidable by construction** (closes C1): the homomorphism Find recurses structurally on Node (A2 implicit descent ⇒ the inferencer terminates); the per-node candidate set is EXACTLY the closed declared inhabitances in `std/*` (enumerable, never synthesized/open), so "no homomorphism" = "exhausted the finite declared set" = a *decidable* fail-closed Diagnostic, not a non-terminating search. Synthesizing candidates = left the decidable fragment = STOP. **B — single-file discipline is a scope boundary**: v2's 12-file split was env/scope/lookup/method-resolution tangling; in v4 those are 03_resolve's job (B-4: binding = canonical `Symbol`), so `04_infer` owns ONLY {C1 Find + cardinality propagation + diagnostic precision}. A worker writing scope/env/binding/lookup here re-imported the 12-file pressure → STOP (belongs in 03_resolve). The single file holds because the scope is bounded, not willed | this row; `compiler/04_infer.dag` is a boundary index only; cross-ref C1 / IR-1 / A1 / A2 / B-4 |