From cc9d2ca8775f4e2652feafd6c11634e9a33047c8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 3 Jul 2026 02:29:23 +0000 Subject: [PATCH 1/4] =?UTF-8?q?docs(body-lowering):=20DESIGN=20+=20staged?= =?UTF-8?q?=20plan=20=E2=80=94=20make=20v2=20inferred=20tree=20faithfully?= =?UTF-8?q?=20represent=20runtime=20iteration?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Design-first milestone deliverable (no load-bearing edits). Fixes the gap from receipts: a Loop node carries its cycle as an acyclic encoding (measure ^loop_bound_edge + iteration-fold body, §4), but the inferred tree drops both loop facts: 1. behavior_multiplicity(Loop) decides termination TAG-ONLY — the Node, and thus the measure, is not in scope — so every raw loop is Violates regardless of its descent evidence (cardinality.dag:219-228). 2. LoopBound{measure,termination}, the carrier that would bind measure→proof, is a DEAD SCAFFOLD (loop_bound_witness_for_node has zero callers) and even it computes termination without reading the measure. 3. 04_infer has NO Loop arm — the body is typed as an opaque conjunction with no per-iteration τ→τ relation (Branch/Match get real arm-typing; Loop doesn't). Thesis: derive termination FROM the measure (fail-closed to DescentUnknown) + type the body as a repeated transform — both as Loop sugar readers, so For/While/Retry/recursion type at once. Blocked-on: a DescentEvidence §3 fork (cardinality.dag:108 bare vs dag/std/termination.dag lattice) consolidates first. Staged plan (5 separately-signed PRs) + 3 open flags for operator sign. Registers the milestone as a DESIGN.md open thread. Co-Authored-By: Claude Opus 4.8 --- DESIGN.md | 1 + docs/plans/body-lowering-design.md | 200 +++++++++++++++++++++++++++++ 2 files changed, 201 insertions(+) create mode 100644 docs/plans/body-lowering-design.md diff --git a/DESIGN.md b/DESIGN.md index 688a40e51ee..25c8f4ff60f 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -86,6 +86,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/` - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.) - floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction (M1: within-walk resolve memo ~105s; M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md) +- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** The substrate models a `Loop` faithfully (measure `^loop_bound_edge` + iteration-fold body, §4), but the inferred tree drops both loop facts: `behavior_multiplicity(Loop)` decides termination **tag-only** (never reading the measure) so every raw loop is `Violates` regardless of its descent evidence (`cardinality.dag:219-228`), the `LoopBound{measure,termination}` carrier that would bind measure→proof is a **dead scaffold** (`loop_bound_witness_for_node` has zero callers, `cardinality.dag:278`), and `04_infer` has **no Loop arm** so the body is typed as an opaque conjunction with no per-iteration `τ→τ` relation. Fix = derive termination from the measure (fail-closed to `DescentUnknown`) + type the body as a repeated transform, both as `Loop` sugar readers (so `For`/`While`/`Retry`/recursion type at once). Blocked-on: a `DescentEvidence` §3 fork (`cardinality.dag:108` bare vs `dag/std/termination.dag` lattice) must consolidate first. → [body-lowering design](docs/plans/body-lowering-design.md) ## Building & checks diff --git a/docs/plans/body-lowering-design.md b/docs/plans/body-lowering-design.md new file mode 100644 index 00000000000..31e8ffd2053 --- /dev/null +++ b/docs/plans/body-lowering-design.md @@ -0,0 +1,200 @@ +# Body-lowering — make v2's inferred tree faithfully represent runtime iteration + +**Status:** design-first (model-before-implement). This document is the deliverable for the +BODY-LOWERING MILESTONE. It fixes the gap, the thesis, the fail-closed guarantees, the staged plan, +and the discriminating witnesses. No load-bearing pipeline/substrate edits land in the design PR; +each stage below is a separate, separately-signed implementation PR. + +Reasoned serially, per DESIGN.md's preamble: §1 fixes the gap from receipts; each later section is a +consequence, not a restatement. + +--- + +## 1. The gap (from receipts, not assertion) + +DESIGN.md §4 fixes the substrate's iteration model: *"cyclic relations via acyclic encodings, never +cyclic values; recursion is sugar over `Loop`."* A `Loop` node +(`src/v2/std/node.dag:26` — `Behavior = Value | Transform | Branch | Loop | Bind | Match`) carries its +cycle as an **acyclic encoding**: exactly one `Named { name: ^loop_bound_edge }` edge (the descent +**measure**) plus ≥1 positional child (the iteration **body**), enforced by `LoopBoundEdges` +(`node.dag:210,279-284,402`). The measure edge *is* the acyclic stand-in for the recursion — no +cyclic value. + +The substrate **models** this faithfully. The **inferred tree does not interpret it.** Three receipts: + +1. **The Loop multiplicity decision is tag-only — it never reads the measure.** + `node_multiplicity` (`cardinality.dag:230-235`) dispatches a `Loop` to + `behavior_multiplicity(b: Behavior)` (`cardinality.dag:219-228`), whose **entire input is the + behavior tag** — the `Node`, and therefore the `^loop_bound_edge` measure, is structurally not in + scope. It returns `RequiresTerminationProof` unconditionally, which + `multiplicity_termination_witness` (`cardinality.dag:199-207`) turns into a hard + `Violates { cardinality_descent_not_proven }`. **Every raw `Loop` is rejected regardless of the + descent evidence its measure edge carries.** The acyclic encoding of the cycle is present in the + tree and *ignored* by the type — the precise "does not faithfully represent runtime iteration" + symptom (this is the §5 "bounded-forever ≠ unknown" fail shape inverted: here a *provably-bounded* + loop is indistinguishable from an unbounded one because the proof input is never consulted). + +2. **The faithful carrier exists but is a dead scaffold.** + `loop_bound_witness_for_node` (`cardinality.dag:278-289`) already builds the right shape — + `LoopBound { measure: Node, termination: Witness }` (`cardinality.dag:119-122`) + — pairing the extracted measure (`loop_measure_node`, `cardinality.dag:161-181`) with a termination + witness. But (a) it has **zero callers** — `04_infer.dag` never consumes it; and (b) its + `termination` field is computed by the same `termination_proof_witness_for_node` → tag-only path, + so even the carrier that *names* the measure→proof binding **derives its proof without reading the + measure**. A scaffold that duplicates a fact it does not actually compute (§5 parallel-representation + debt; §6 named-dissolution-trigger missing). + +3. **The loop body is typed opaquely — no per-iteration relation.** + `04_infer.dag` has **no `Loop` arm.** `infer_gather_fold_init` (`04_infer.dag:933-985`) + special-cases `Branch` (`:935`) and `Match` (`:944`) — each gets real per-arm body-type rows + (`InferMatchArmRow { body_type }`, `:593-596`) unified across arms + (`infer_unify_branch_arm_types`, `:484-497`). `Loop` falls to the generic `_ =>` + (`:953`) → `infer_node_facts`, which types each positional child as an independent constraint-graph + node with **no relation asserted between the pre-iteration and post-iteration type.** The tree says + "these nodes exist," not "this body is applied repeatedly, threading a value." A loop is typed as + if it were a one-shot conjunction. + +**Net:** the substrate carries loop *shape* (measure + body edges) but the inferred tree carries +neither the loop's *termination fact* (gap 1/2) nor its *iteration fact* (gap 3). Body-lowering closes +both so the inferred tree is a faithful image of what runs. + +## 2. Adjacent finding — `DescentEvidence` is forked (§3), and it blocks the fix + +The descent derivation this milestone needs is **already modeled twice**: + +- `src/v2/std/cardinality.dag:108-111` — bare `DescentEvidence = Strict | NonIncreasing | + DescentUnknown`. No lattice, no combinator. +- `dag/std/termination.dag:5-` — the **same** `DescentEvidence` with the full authority: an + `evidence_rank`, a `descent_evidence_bounded_lattice: BoundedLattice` with + `meet`/`join` (`termination.dag:18-52`), `promote_to_strict`, and per-key merge. `dag/std/computation.dag` + consumes it. + +This is a §3 nickname — one concept, two homes — and it is **on the critical path**: a loop whose +iteration fold has several contributing measures terminates only if **all** descend, which is exactly +a **lattice meet** over their per-edge `DescentEvidence`. The bare v2 copy cannot express that; the +`dag/std/termination.dag` authority can. So the fix must **ground the v2 descent derivation on the +single `DescentEvidence` authority (the lattice one)**, not extend the bare copy — otherwise the fix +itself widens the fork (§2 net-concepts-must-not-grow test). Resolving which layer that authority +lives in (the v2 `src/v2/std` tree vs the `dag/std` tree) is FLAG A below. + +## 3. Thesis — derive the loop's type from its measure and its body, not from its tag + +Two faithful bindings, mirroring the two facts a loop carries: + +**T1 — termination is *derived from the measure*, fail-closed.** Replace the tag-only +`behavior_multiplicity(Loop) => RequiresTerminationProof` with a **node-aware** Loop multiplicity that +reads the `^loop_bound_edge` measure target and its contributing iteration-fold edges, extracts each +edge's `DescentEvidence`, combines them by **lattice meet** on the single authority, and maps: + +- `Strict` → `ProvenTermination { proof }` (a real `TerminationProof` naming the ranking dimension the + measure descends on); +- `NonIncreasing` → `ProvenTermination` **only** when paired with a strict dimension elsewhere in the + fold (that is precisely what `TerminationProof { non_increasing: List, strict: RankingDimension }` + at `cardinality.dag:115-118` already encodes — a lexicographic descent); a lone `NonIncreasing` + stays `RequiresTerminationProof`; +- `DescentUnknown` or absent/malformed measure → `RequiresTerminationProof` → `Violates` + (**construction-preserving fail-closed** — the honest bottom of the lattice; DESIGN.md §5: a + provably-bounded loop must be *distinguishable* from an unknown one, and an unknown one must still + refuse loudly). + +This makes the measure edge *load-bearing in the type*: perturb the measure and the loop's +termination verdict changes — the acyclic encoding is now interpreted, not decorative. `LoopBound` +(gap 2) becomes the live carrier of this binding, and `loop_bound_witness_for_node` gains its first +real consumer (dead scaffold dissolved). + +**T2 — the body is typed as a per-iteration transform.** Give `04_infer.dag` a `Loop` arm parallel to +`Branch`/`Match`: type the iteration-fold body (positional children, per +`loop_edge_contributes_to_iteration_fold`, `node.dag:374-387`) as a transform from the pre-iteration +carrier type to the post-iteration carrier type, and assert the **fixpoint relation** that the body's +output type unifies with its input type (a loop that changes the carrier's type each turn does not +have a runtime iteration semantics — it fails closed). The inferred tree then states "body : τ → τ, +repeated under measure μ," which *is* the runtime iteration. This reuses the existing arm-unification +machinery (`infer_unify_branch_arm_types`) rather than minting a parallel fold. + +Both bindings are **`Loop` sugar readers**: per DESIGN.md §4/§7, `For`/`While`/`Retry` (and recursion) +are sugar over `Loop`, so typing `Loop` faithfully types all of them at once — no per-form N×M work. +This is the same "one grammar, both directions" move: the descent measure is read *forward* to a +proof; body-lowering is the inference direction of the same edge discipline `content_hash` +canonicalizes. + +## 4. Non-goals / scope fence + +- **Not** touching `program.dag` or surface syntax — this is inference over the already-lowered + `Node` tree, not a parser change. +- **Not** adding orchestration `While.bound`/`Retry` emission — `orchestration.dag` already declares + `While { bound: DescentEvidence }` (`orchestration.dag:56`); this milestone makes the *inference* + that would justify such a bound faithful. The two meet at the shared `DescentEvidence` authority + (FLAG A), not by touching orchestration here. +- **Not** enriching `03_body_producer.dag`'s MVP-1 fixture bodies (gap 3's degenerate single-literal + body). That is a fixture-realism follow-on; T2 types whatever body the producer emits and does not + require a richer producer to be faithful about the *relation*. Flagged as Stage 4 (optional). + +## 5. Staged plan (each stage = one signed PR; strictly ordered) + +Ordered so every load-bearing edit lands *after* its model, and each stage is provable by a red→green +witness before the next begins. + +- **Stage 0 — this design PR (non-load-bearing).** This document + an open-thread bullet in DESIGN.md + registering the milestone. No behavior change. *This is the PR this session opens.* + +- **Stage 1 — resolve the `DescentEvidence` fork (§3 / FLAG A).** Ground the v2 descent path on the + single authority (the `dag/std/termination.dag` lattice), deleting the bare `cardinality.dag:108-111` + copy or making it a re-export, per the operator's single-authority ruling on the v2↔dag layer split. + Witness: `descent_evidence_meet` over the lattice, red control = a perturbed meet. **Model-before: + Stage 2 imports the consolidated authority; do it first.** + +- **Stage 2 — node-aware Loop multiplicity (T1).** Introduce `loop_multiplicity(n: Node)` deriving + `Multiplicity` from the measure via the Stage-1 authority; route `node_multiplicity` for + `ComputationNode { behavior: Loop }` through it (Branch/Value/etc. stay tag-only — their multiplicity + genuinely is tag-determined). Wire `loop_bound_witness_for_node` as the consumer (kills the dead + scaffold). **Discriminating witness:** a Loop with a `Strict`-descent measure infers + `ProvenTermination` (was `Violates`); the *same* Loop with the measure perturbed to `DescentUnknown` + infers `Violates` — the verdict is a function of the measure. Load-bearing (`cardinality.dag`): + higher bar, execution-proven, escalate if it touches beyond the Loop arm. + +- **Stage 3 — Loop body arm in `04_infer` (T2).** Add the `ComputationNode { behavior: Loop }` arm to + `infer_gather_fold_init`, typing the iteration fold as `τ → τ` and asserting the fixpoint + unification, reusing `infer_unify_branch_arm_types`. **Discriminating witness:** a loop whose body + preserves the carrier type infers a clean iteration type; a body whose output type diverges from its + input infers a located mismatch (was silently accepted as opaque conjunction). Load-bearing + (`04_infer.dag`): higher bar. + +- **Stage 4 (optional follow-on) — body-producer fixture realism.** Replace the degenerate + single-literal loop body (`03_body_producer.dag:851-874`) with a body that threads a binder across + the iteration, so the fixtures *exercise* T2's fixpoint relation with a non-trivial carrier. Only + after Stages 2–3 make the relation observable. May be split to a separate owner. + +Each of Stages 1–3 is independently mergeable and independently valuable; Stage 3 does not require +Stage 2 to *land* but reads cleaner after it. Stage 2 requires Stage 1. + +## 6. Fail-closed guarantees (§5) and construction-vs-validation + +- The `DescentUnknown`/absent-measure → `Violates` mapping is **construction-preserving**: it is the + lattice bottom, not a post-hoc check. A loop cannot be typed "terminating" without a measure that + *derives* the proof — the bad state (a loop admitted with no descent evidence) stays unwritable, + exactly as today, but now for the *right reason* (evidence absent) rather than the wrong one (all + loops rejected). +- **No fabricated proof:** `NonIncreasing`-only never fabricates a `Strict` dimension; it stays + `RequiresTerminationProof`. `promote_to_strict` (`termination.dag:52`) is applied only where a + strict dimension genuinely exists in the fold. +- **Discriminating red control is mandatory per stage** — the design is not "done" until a consumer + runs green *and* a perturbed measure/body runs red (DESIGN.md §5 spec-without-execution trap; my + standing anti-overclaim culture — the honest bar is the deliverable). + +## 7. Open flags for parent/operator sign + +- **FLAG A (blocks Stage 1):** which layer owns the single `DescentEvidence` authority — the v2 + `src/v2/std` tree or the `dag/std/termination.dag` tree? Both exist; the richer lattice is in + `dag/std`. Need the single-authority ruling before consolidating (this is the recurring v2↔dag + cross-tree grounding question, not new to this milestone). +- **FLAG B (Stage 2):** `behavior_multiplicity` currently takes `Behavior`; making Loop node-aware + means Loop's multiplicity is decided one layer up (`node_multiplicity`) while the other behaviors + stay in `behavior_multiplicity`. Is asymmetry acceptable, or should `behavior_multiplicity` be + retired in favor of a uniformly node-aware `node_multiplicity`? I lean asymmetric (the other + behaviors' multiplicity *is* genuinely tag-determined; forcing them node-aware is ceremony), but + flag it because it touches a load-bearing dispatch. +- **FLAG C (Stage 3):** the fixpoint relation `τ → τ` assumes the loop carrier is invariant across + iterations. Some faithful loops *narrow* a type monotonically (refinement). First cut requires + strict invariance (fail-closed); refinement-typed loops are a named follow-on, not silently + admitted. +``` From e0d9c52af1384ae338e28b8a031cfea467a00ac8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 3 Jul 2026 02:34:43 +0000 Subject: [PATCH 2/4] =?UTF-8?q?WIP:=20BODY-LOWERING=20MILESTONE=20(design-?= =?UTF-8?q?first,=20model-before-implement=20=E2=80=94=20do=20NOT=20s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/plans/body-lowering-design.md | 55 ++++++++++++++++++------------ 1 file changed, 34 insertions(+), 21 deletions(-) diff --git a/docs/plans/body-lowering-design.md b/docs/plans/body-lowering-design.md index 31e8ffd2053..e0b543bb393 100644 --- a/docs/plans/body-lowering-design.md +++ b/docs/plans/body-lowering-design.md @@ -137,11 +137,16 @@ witness before the next begins. - **Stage 0 — this design PR (non-load-bearing).** This document + an open-thread bullet in DESIGN.md registering the milestone. No behavior change. *This is the PR this session opens.* -- **Stage 1 — resolve the `DescentEvidence` fork (§3 / FLAG A).** Ground the v2 descent path on the - single authority (the `dag/std/termination.dag` lattice), deleting the bare `cardinality.dag:108-111` - copy or making it a re-export, per the operator's single-authority ruling on the v2↔dag layer split. - Witness: `descent_evidence_meet` over the lattice, red control = a perturbed meet. **Model-before: - Stage 2 imports the consolidated authority; do it first.** +- **Stage 1 — resolve the `DescentEvidence` fork (§3 / FLAG A — direction RULED, landing HELD).** + Ground the v2 descent path on the single authority: **`dag/std/termination.dag` is the authority** + (parent ruling 2026-07-03, §7 — `.dag` is truth, `src/v2/std` is the transient seed that shrinks to + zero; and the richer lattice already lives there). Consolidate the bare `cardinality.dag:108-111` + `DescentEvidence` **into** `dag/std/termination.dag`, then repoint/delete the v2 copy. Witness: + `descent_evidence_meet` over the lattice, red control = a perturbed meet. **Model-before: Stage 2 + imports the consolidated authority; do it first.** **LANDING HOLD:** design against this direction + now (unblocked), but do **not** land the consolidation until parent relays the operator's *standing* + confirmation that `dag/std` wins v2↔dag forks as a durable rule (covers this, the pending + `QualifiedName` de-fork, and future forks — imminent, direction very unlikely to flip). - **Stage 2 — node-aware Loop multiplicity (T1).** Introduce `loop_multiplicity(n: Node)` deriving `Multiplicity` from the measure via the Stage-1 authority; route `node_multiplicity` for @@ -181,20 +186,28 @@ Stage 2 to *land* but reads cleaner after it. Stage 2 requires Stage 1. runs green *and* a perturbed measure/body runs red (DESIGN.md §5 spec-without-execution trap; my standing anti-overclaim culture — the honest bar is the deliverable). -## 7. Open flags for parent/operator sign - -- **FLAG A (blocks Stage 1):** which layer owns the single `DescentEvidence` authority — the v2 - `src/v2/std` tree or the `dag/std/termination.dag` tree? Both exist; the richer lattice is in - `dag/std`. Need the single-authority ruling before consolidating (this is the recurring v2↔dag - cross-tree grounding question, not new to this milestone). -- **FLAG B (Stage 2):** `behavior_multiplicity` currently takes `Behavior`; making Loop node-aware - means Loop's multiplicity is decided one layer up (`node_multiplicity`) while the other behaviors - stay in `behavior_multiplicity`. Is asymmetry acceptable, or should `behavior_multiplicity` be - retired in favor of a uniformly node-aware `node_multiplicity`? I lean asymmetric (the other - behaviors' multiplicity *is* genuinely tag-determined; forcing them node-aware is ceremony), but - flag it because it touches a load-bearing dispatch. -- **FLAG C (Stage 3):** the fixpoint relation `τ → τ` assumes the loop carrier is invariant across - iterations. Some faithful loops *narrow* a type monotonically (refinement). First cut requires - strict invariance (fail-closed); refinement-typed loops are a named follow-on, not silently - admitted. +## 7. Flag dispositions (parent-signed 2026-07-03) + +- **FLAG A — RULED (direction), landing HELD.** The single `DescentEvidence` authority is + **`dag/std/termination.dag`** (§7: `.dag` is truth, `src/v2/std` is the shrinking seed; the richer + meet/join/`promote_to_strict` lattice already lives there). This is one instance of the recurring + v2↔dag fork class (same as the pending `QualifiedName` de-fork). Stage 1 is designed against this + direction now, but its **consolidation landing waits** on the operator's *standing* confirmation + (parent relaying) that `dag/std` wins these forks as a durable rule — so we don't re-escalate per + fork. Direction very unlikely to flip. +- **FLAG B — SIGNED (accept the asymmetry).** Loop's multiplicity is decided one layer up + (`node_multiplicity`, node-aware) while the other behaviors stay tag-only in `behavior_multiplicity` + — and that is **principled, not sloppy inconsistency**: Loop is genuinely different because its + termination *depends on the measure*, which is a node-level edge the `Behavior` tag structurally + cannot carry. The other behaviors' multiplicity **is** tag-determined; forcing them node-aware would + be false uniformity (ceremony over a distinction that isn't there). The Stage-2 implementation must + carry this rationale in-code so the asymmetry reads as a real distinction. +- **FLAG C — SIGNED, with one §5 requirement.** First cut handles carrier-invariant `τ → τ` loops + (typed + green). Refinement-typed loops (carrier narrows monotonically across iterations) are a + named follow-on — but they must be **fail-closed in the first cut**: a refinement loop is typed + `DescentUnknown` / **refused with a located diagnostic**, *never* silently fabricated as `τ → τ`. A + refinement loop mis-typed as invariant is a fabricated wrong answer (§5). So: `τ → τ` → proven; + detected-refinement → refused, with the refinement-typed follow-on as its named dissolution trigger. + The Stage-3 discriminating witness must include a refinement-shaped loop that goes **red/refused** + (not silently accepted). ``` From ceac3ea944800985a7e4a73a056b7d5b630cfde2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 3 Jul 2026 02:34:51 +0000 Subject: [PATCH 3/4] docs(body-lowering): fold in parent flag rulings (A ruled+held, B/C signed) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit FLAG A: DescentEvidence authority ruled dag/std/termination.dag (§7); Stage 1 designed against it now, consolidation LANDING held for operator standing v2<->dag-fork confirm. FLAG B signed — Loop-multiplicity node-awareness is principled (termination depends on the measure, a node-level fact the tag can't carry); rationale to live in-code. FLAG C signed with §5 requirement — refinement-typed loops fail-closed (refused, not silently fabricated as tau->tau); Stage-3 witness must include a refinement loop that goes red. Co-Authored-By: Claude Opus 4.8 --- DESIGN.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DESIGN.md b/DESIGN.md index 25c8f4ff60f..284b8f6a7c9 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -86,7 +86,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/` - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.) - floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction (M1: within-walk resolve memo ~105s; M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md) -- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** The substrate models a `Loop` faithfully (measure `^loop_bound_edge` + iteration-fold body, §4), but the inferred tree drops both loop facts: `behavior_multiplicity(Loop)` decides termination **tag-only** (never reading the measure) so every raw loop is `Violates` regardless of its descent evidence (`cardinality.dag:219-228`), the `LoopBound{measure,termination}` carrier that would bind measure→proof is a **dead scaffold** (`loop_bound_witness_for_node` has zero callers, `cardinality.dag:278`), and `04_infer` has **no Loop arm** so the body is typed as an opaque conjunction with no per-iteration `τ→τ` relation. Fix = derive termination from the measure (fail-closed to `DescentUnknown`) + type the body as a repeated transform, both as `Loop` sugar readers (so `For`/`While`/`Retry`/recursion type at once). Blocked-on: a `DescentEvidence` §3 fork (`cardinality.dag:108` bare vs `dag/std/termination.dag` lattice) must consolidate first. → [body-lowering design](docs/plans/body-lowering-design.md) +- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** The substrate models a `Loop` faithfully (measure `^loop_bound_edge` + iteration-fold body, §4), but the inferred tree drops both loop facts: `behavior_multiplicity(Loop)` decides termination **tag-only** (never reading the measure) so every raw loop is `Violates` regardless of its descent evidence (`cardinality.dag:219-228`), the `LoopBound{measure,termination}` carrier that would bind measure→proof is a **dead scaffold** (`loop_bound_witness_for_node` has zero callers, `cardinality.dag:278`), and `04_infer` has **no Loop arm** so the body is typed as an opaque conjunction with no per-iteration `τ→τ` relation. Fix = derive termination from the measure (fail-closed to `DescentUnknown`) + type the body as a repeated transform, both as `Loop` sugar readers (so `For`/`While`/`Retry`/recursion type at once). Blocked-on: a `DescentEvidence` §3 fork (`cardinality.dag:108` bare vs `dag/std/termination.dag` lattice) consolidates first — **authority ruled `dag/std/termination.dag`** (§7; parent 2026-07-03), landing held for the operator's *standing* v2↔dag-fork confirm. FLAG B (Loop-multiplicity asymmetry) SIGNED; FLAG C (refinement loops fail-closed, not fabricated `τ→τ`) SIGNED. → [body-lowering design](docs/plans/body-lowering-design.md) ## Building & checks From 23fcdb0069fe37201cbc434e053f32581cebdc0e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 3 Jul 2026 02:47:26 +0000 Subject: [PATCH 4/4] docs(body-lowering): fix gap-2 caller receipt (cursor REQUEST_CHANGES) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit loop_bound_witness_for_node is NOT zero-callers — it is consumed by the cost/complexity lenses (src/v2/lens/cost.dag:168 base_cost_for_loop and subject_complexity_budget_roster.dag:45), which read only its `measure` field for sizing. Correct gap 2 to its real, sound point: (a) no INFERENCE consumer of the carrier, and (b) its `termination` field is computed measure-blind (tag-only, cardinality.dag:284) — a hollow second representation of a proof the measure already determines. Retarget Stage 2 to "first measure-aware termination consumer" (not "first caller"), so wiring instructions don't misroute implementers. Drops the incorrect "dead scaffold" framing in the doc and the DESIGN.md bullet. Co-Authored-By: Claude Opus 4.8 --- DESIGN.md | 2 +- docs/plans/body-lowering-design.md | 35 ++++++++++++++++++++---------- 2 files changed, 25 insertions(+), 12 deletions(-) diff --git a/DESIGN.md b/DESIGN.md index 284b8f6a7c9..1ebc6c3d813 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -86,7 +86,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/` - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20) - the remaining deleted-`docs/` references in `.dag` comments — provenance / `bind:` pointers into the bankrupted `docs/` tree (e.g. `docs/planning/*`, `design-*.md`) — fold into the dep-graph reform, not a blind repoint. (The named-corpus ledger marks — `Practice N`, and `INVARIANTS` / `THESIS` / `MODELING` / `RELEASE_TODO` / … citations — were swept: dropped, or re-homed to DESIGN.md §-anchors.) - floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction (M1: within-walk resolve memo ~105s; M2: RunnableCompile node gated on v2.std.determinism #5941): [design sketch](docs/plans/floor-shared-compute-memoization.md) -- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** The substrate models a `Loop` faithfully (measure `^loop_bound_edge` + iteration-fold body, §4), but the inferred tree drops both loop facts: `behavior_multiplicity(Loop)` decides termination **tag-only** (never reading the measure) so every raw loop is `Violates` regardless of its descent evidence (`cardinality.dag:219-228`), the `LoopBound{measure,termination}` carrier that would bind measure→proof is a **dead scaffold** (`loop_bound_witness_for_node` has zero callers, `cardinality.dag:278`), and `04_infer` has **no Loop arm** so the body is typed as an opaque conjunction with no per-iteration `τ→τ` relation. Fix = derive termination from the measure (fail-closed to `DescentUnknown`) + type the body as a repeated transform, both as `Loop` sugar readers (so `For`/`While`/`Retry`/recursion type at once). Blocked-on: a `DescentEvidence` §3 fork (`cardinality.dag:108` bare vs `dag/std/termination.dag` lattice) consolidates first — **authority ruled `dag/std/termination.dag`** (§7; parent 2026-07-03), landing held for the operator's *standing* v2↔dag-fork confirm. FLAG B (Loop-multiplicity asymmetry) SIGNED; FLAG C (refinement loops fail-closed, not fabricated `τ→τ`) SIGNED. → [body-lowering design](docs/plans/body-lowering-design.md) +- **body-lowering — make v2's inferred tree faithfully represent runtime iteration.** The substrate models a `Loop` faithfully (measure `^loop_bound_edge` + iteration-fold body, §4), but the inferred tree drops both loop facts: `behavior_multiplicity(Loop)` decides termination **tag-only** (never reading the measure) so every raw loop is `Violates` regardless of its descent evidence (`cardinality.dag:219-228`), the `LoopBound{measure,termination}` carrier that would bind measure→proof is consumed only by the cost/complexity lenses (`cost.dag:168`) which read its `measure` for sizing but **never** its `termination` — and that `termination` field is itself computed **measure-blind** (tag-only, `cardinality.dag:284`), so **no inference consumes the loop's termination fact** (`loop_bound_witness_for_node`, `cardinality.dag:278`), and `04_infer` has **no Loop arm** so the body is typed as an opaque conjunction with no per-iteration `τ→τ` relation. Fix = derive termination from the measure (fail-closed to `DescentUnknown`) + type the body as a repeated transform, both as `Loop` sugar readers (so `For`/`While`/`Retry`/recursion type at once). Blocked-on: a `DescentEvidence` §3 fork (`cardinality.dag:108` bare vs `dag/std/termination.dag` lattice) consolidates first — **authority ruled `dag/std/termination.dag`** (§7; parent 2026-07-03), landing held for the operator's *standing* v2↔dag-fork confirm. FLAG B (Loop-multiplicity asymmetry) SIGNED; FLAG C (refinement loops fail-closed, not fabricated `τ→τ`) SIGNED. → [body-lowering design](docs/plans/body-lowering-design.md) ## Building & checks diff --git a/docs/plans/body-lowering-design.md b/docs/plans/body-lowering-design.md index e0b543bb393..b1ccb01e722 100644 --- a/docs/plans/body-lowering-design.md +++ b/docs/plans/body-lowering-design.md @@ -34,15 +34,23 @@ The substrate **models** this faithfully. The **inferred tree does not interpret symptom (this is the §5 "bounded-forever ≠ unknown" fail shape inverted: here a *provably-bounded* loop is indistinguishable from an unbounded one because the proof input is never consulted). -2. **The faithful carrier exists but is a dead scaffold.** +2. **The faithful carrier exists but its termination field is computed measure-blind, and no + *inference* consumes it.** `loop_bound_witness_for_node` (`cardinality.dag:278-289`) already builds the right shape — `LoopBound { measure: Node, termination: Witness }` (`cardinality.dag:119-122`) — pairing the extracted measure (`loop_measure_node`, `cardinality.dag:161-181`) with a termination - witness. But (a) it has **zero callers** — `04_infer.dag` never consumes it; and (b) its - `termination` field is computed by the same `termination_proof_witness_for_node` → tag-only path, - so even the carrier that *names* the measure→proof binding **derives its proof without reading the - measure**. A scaffold that duplicates a fact it does not actually compute (§5 parallel-representation - debt; §6 named-dissolution-trigger missing). + witness. It *is* consumed today — but only by the **cost/complexity** lenses + (`src/v2/lens/cost.dag:168` `base_cost_for_loop`, and the complexity-budget roster test + `src/v2/test/claim/complexity_gate/subject_complexity_budget_roster.dag:45`), and those read only + the `measure` field (via `loop_bound_measure`) to size cost — `linear_in_node(measure)` + (`cost.dag:170`) — never the `termination` field. The gap is two-fold: (a) **no inference + consumer** — `04_infer.dag` never reads this carrier, so the loop's termination fact never reaches + the inferred tree; and (b) the carrier's `termination` field is itself computed by the same + `termination_proof_witness_for_node` → tag-only path (`cardinality.dag:284`), so even the field that + *names* the measure→proof binding **derives its proof without reading the measure**. The carrier + names a fact it does not actually compute (§5 parallel-representation debt): a `LoopBound` whose + `termination` is measure-blind is a second, hollow representation of a proof that the measure + already determines. 3. **The loop body is typed opaquely — no per-iteration relation.** `04_infer.dag` has **no `Loop` arm.** `infer_gather_fold_init` (`04_infer.dag:933-985`) @@ -98,9 +106,11 @@ edge's `DescentEvidence`, combines them by **lattice meet** on the single author refuse loudly). This makes the measure edge *load-bearing in the type*: perturb the measure and the loop's -termination verdict changes — the acyclic encoding is now interpreted, not decorative. `LoopBound` -(gap 2) becomes the live carrier of this binding, and `loop_bound_witness_for_node` gains its first -real consumer (dead scaffold dissolved). +termination verdict changes — the acyclic encoding is now interpreted, not decorative. `LoopBound`'s +`termination` field (gap 2) stops being measure-blind: it is *derived from* the measure, so the +carrier's two fields become consistent, and `04_infer` gains the **first inference / measure-aware +termination consumer** of it (the cost/complexity lenses already read its `measure` for sizing, but +never the `termination` fact — this closes gap 2's hollow half). **T2 — the body is typed as a per-iteration transform.** Give `04_infer.dag` a `Loop` arm parallel to `Branch`/`Match`: type the iteration-fold body (positional children, per @@ -151,8 +161,11 @@ witness before the next begins. - **Stage 2 — node-aware Loop multiplicity (T1).** Introduce `loop_multiplicity(n: Node)` deriving `Multiplicity` from the measure via the Stage-1 authority; route `node_multiplicity` for `ComputationNode { behavior: Loop }` through it (Branch/Value/etc. stay tag-only — their multiplicity - genuinely is tag-determined). Wire `loop_bound_witness_for_node` as the consumer (kills the dead - scaffold). **Discriminating witness:** a Loop with a `Strict`-descent measure infers + genuinely is tag-determined). Make `loop_bound_witness_for_node`'s `termination` field derive from + the measure (not the tag-only path) and route inference through it — the **first measure-aware + termination consumer** (the existing cost/complexity readers at `cost.dag:168` / + `subject_complexity_budget_roster.dag:45` use only the `measure` field and are unaffected). + **Discriminating witness:** a Loop with a `Strict`-descent measure infers `ProvenTermination` (was `Violates`); the *same* Loop with the measure perturbed to `DescentUnknown` infers `Violates` — the verdict is a function of the measure. Load-bearing (`cardinality.dag`): higher bar, execution-proven, escalate if it touches beyond the Loop arm.