From 7ee785168ee1f869f0ae2ac3ed736fa0c40a323f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 05:55:07 +0000 Subject: [PATCH] docs: reconcile numeric-tower grounding status post-#5428 + #5425 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #5428 (smart-crane) grounded Nat construction-side — Zero→Int(0), Succ{prev:Int(k)}→Int(k+1) — so native form == modeled form. Deferred doc update explicitly to lane manager post-#5425. DESIGN.md §5 open-thread (b): mark numeric tower GROUNDED; note that eval_binop CrossRepresentationEquality guard is dead-in-corpus for numerics but kept as fail-closed backstop until Value::Null split (guard removal bundled with that work, fenced out of this window). docs/plans/model-realization-fork.md §3.1: numeric row landed→grounded; records the exact realization, discriminating witness, and why the guard stays (bundled removal, not a regression). §3.2 (Value::Null split) unchanged — still the deeper root, its own runway. Co-Authored-By: Claude Sonnet 4.6 --- DESIGN.md | 8 ++++++-- docs/plans/model-realization-fork.md | 11 +++++++---- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/DESIGN.md b/DESIGN.md index d2a2f3bd5a0..f7dc2f9f8fb 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -236,8 +236,12 @@ still a violation) · internal review finds missing tests, external review finds `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 first, `Int = GroupCompletion` still bottoming in Peano `Nat`), which - dissolves the straddle and makes the guard dead code. (operator: `==` fail-closed, 2026-06-20) + 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.) ## Building & checks diff --git a/docs/plans/model-realization-fork.md b/docs/plans/model-realization-fork.md index a1e5a9be94a..5f61a17ee6d 100644 --- a/docs/plans/model-realization-fork.md +++ b/docs/plans/model-realization-fork.md @@ -45,10 +45,13 @@ other primitive is per-site. ## 3. Grounding order (does it dissolve the guards?) -1. **Numeric tower — grounds cleanly; YES, dissolves the guard.** Finish `Int = GroupCompletion` - bottoming in Peano `Nat`, so the native form *is* the modeled form. Then - `cross_representation_numeric_straddle` (and the `eval_binop` guard) become **dead code**. Highest - value / lowest risk. Start here. +1. **Numeric tower — GROUNDED (#5428, 2026-06-21).** Nat construction-side grounded: + `Zero → Value::Int(0)`, `Succ{prev:Int(k)} → Value::Int(k+1)` — native form == modeled form. + `cross_representation_numeric_straddle` is dead-in-corpus for numerics; `eval_binop`'s + `CrossRepresentationEquality` guard is **kept as fail-closed backstop** (not removed — guard removal + is bundled with the `Value::Null` split in §3.2, fenced out of this window). The discriminating + witness `cross_representation_equality_test` confirms: former fork cases now reconcile to `Bool(true)`; + genuine diffs (`1==2`, `Succ{Zero}==Zero → Int(1)==Int(0)`) stay `false`. **Done.** 2. **`Value::Null` overload — the deeper root; NO, needs SPLITTING not grounding-away.** `Value::Null` means *None* / *Absent* (Optional) / *miss* (map lookup) / *Violates* (Witness) **all at once**. So a blanket equality guard is wrong — `present == None → false` is *legitimate* at ~131 sites. The fix is