diff --git a/docs/r3-design-schedule-2026-05-06.md b/docs/r3-design-schedule-2026-05-06.md index 44efca14ff3..428de582ca8 100644 --- a/docs/r3-design-schedule-2026-05-06.md +++ b/docs/r3-design-schedule-2026-05-06.md @@ -49,10 +49,12 @@ Prior `AbelianGroup` references in r3-structure.md, r3-program-plan.md, thi 1. **Axes in R3 scope**: `MachineWidth` only. `RegisterClass` / `EndianMode` / alignment / signedness-as-axis deferred post-R3 absent a closure-gate forcing them. **Discipline note (Brian directive)**: this is a separation-of-facts/concerns exercise — algebra is one axis of fact, machine constraint is another, target lowering (e.g., Rust emission) is a *projection / coercion* over both. Integer modeling is the canonical exercise for this discipline; getting comfortable with the separation is the broader R3 modeling work. 2. **Interaction substrate shape**: **REST-API-style typed-contract interactions between models** (Brian directive 2026-05-06: *"these models interact a la rest apis interacting — scalable / no dual representations (.dag generated)"*). Each model (algebra, machine-constraint) declares its interface in `.dag`; the interaction substrate (composition, projection, coercion) is **`.dag`-generated**, not hand-coded. **Hard constraint: no dual representations** — any Rust counterpart must be generated from `.dag`, never hand-maintained (per `feedback_isomorphism_or_generation_for_mirrors` + `feedback_no_generated_code_on_disk`). Closed-enumeration lookup-maps and parallel Rust mirrors are both rejected (bridges). -3. **Type-level spelling**: `Int<64>` parses/elaborates as `Compose>` parametrically. Surface intuition is the literal product `Int × MachineWidth<64>`; substrate spelling is parametric. Equivalent under both algebra-side options per PR #1815. **Distinction (per claude review observation)**: the *elaboration* of a particular `Compose>` term is parser/elaborator behavior; the **interaction substrate** (composition/projection/coercion machinery operating *on* such Compose terms) is what's `.dag`-generated per sub-decision 2 — not the `Compose<...>` *type itself*. S3 worker brief should preserve this distinction. -4. **Approximate-algebra layering**: algebra-side approximation (`ApproximateField`) and machine-side approximation (`MachineWidth<64>`) stay as independent axes that compose. `Real<64>` = `Compose, MachineWidth<64>>` carries both layers explicitly per S8's named-axiom-relaxation discipline. +3. **Type-level spelling**: `Int<64>` parses/elaborates as **`Compose>`** parametrically — first slot is the **algebraic concept** (the fully-applied carrier+witness composite, e.g., `Int = AbelianGroup>` per #1466 already on main), second slot is the machine-constraint axis. **Critical correction (per codex BLOCKING 2026-05-06)**: prior phrasing `Compose>` was wrong — `AbelianGroup` is a *witness shape* generic over carrier `T`, not a carrier constructor (per `dsl/std/algebra.dag:148-150`: *"T = GroupCompletion is the carrier; AbelianGroup carries op/identity/inverse over that carrier"*). Putting bare `AbelianGroup` in `Compose<...>` slot-1 composes the witness rather than the integer concept; correct form is `Compose>` where `Int` IS the carrier+witness composite. Same pattern for: `UInt<64>` = `Compose>` (where `UInt = CommutativeMonoid` per #1818), `Real<64>` = `Compose>` (where `Real = ApproximateField`), `Nat<8>` = `Compose>`. Surface intuition is the literal product `Int × MachineWidth<64>`; substrate spelling is the parametric `Compose`. **Distinction (per claude review observation)**: the *elaboration* of a particular `Compose>` term is parser/elaborator behavior; the **interaction substrate** (composition/projection/coercion machinery operating *on* such Compose terms) is what's `.dag`-generated per sub-decision 2 — not the `Compose<...>` *type itself*. S3 worker brief should preserve this distinction. +4. **Approximate-algebra layering**: algebra-side approximation (`Real = ApproximateField`) and machine-side approximation (`MachineWidth<64>`) stay as independent axes that compose. `Real<64>` = `Compose>` carries both layers explicitly per S8's named-axiom-relaxation discipline (the algebra-side approximation is internal to `Real`'s definition; the machine-side approximation is the second slot). 5. **Demonstration breadth — NOT a target** (Brian directive 2026-05-06: *"3 is not a target, we shouldn't be 'targeting' modeling, we are just doing our best job to faithfully represent the concepts"*). The 3-pair demonstration (`Int<64>` / `Real<64>` / `Nat<8>`) is the **minimum existence proof** that the substrate carries the concept faithfully. **Faithful representation of the concept is the closure criterion**; pair-counting is not. Once the parser handles generic interaction syntax + the substrate carries the algebra+machine separation, all valid pairs work by construction. Closure-gate predicate phrasing should reflect "concept is faithfully modeled" not "≥3 pairs land". -6. **Target-specificity — universal substrate, faithful target lowering** (Brian directive 2026-05-06 elaborated): `MachineConstraint` is **universal substrate** — every target carries machine-constraint facts as substrate. Targets lacking native machine-width semantics handle lowering by **faithfully representing the concept in a target-available primitive**, NOT by omission. For Python u8: lower to `numpy.uint8` / `ctypes.c_uint8` / explicit literal-bits via `int & 0xFF` discipline — pick whichever Python idiom faithfully carries the 8-bit-natural-number concept. The substrate stays universal; Grounding handles per-target faithful-lowering selection. *Brian framing: "if python lacks — we would have to actually represent the struct using something that python faithfully provides — i.e. either literal bits or otherwise."* Faithful representation > target-conditioned omission. +6. **Target-specificity — universal faithful representation, cost lens as the discriminator** (Brian directive 2026-05-06 elaborated 2x): `MachineConstraint` is **universal substrate** — every target carries machine-constraint facts as substrate. **Universality of faithful representation** (Brian directive 2026-05-06: *"in all cases we should be able to represent the structure with literal bits/objects or whatever — the cost would be enormous — in those cases, we would look for alternatives like better modeling/libraries/int & 0xFF"*): every target language CAN faithfully represent every concept; literal-bits / direct-object construction is always available as the floor (universal but expensive). **The cost lens (T-CostLens-Composition) is the discriminator** that orders the faithful-representation alternatives by per-primitive realization cost: `cost_lens_reads_target_realization` reads the target language spec's per-primitive realization cost; `coercion_cost_equals_complexity_by_construction` makes "the choice between faithful representations IS the cost-lens application" structural-not-conventional. **Grounding selects the lowest-cost faithful representation** per target by reading the cost lens output. For Python u8: cost-tier 1 = `numpy.uint8` (low cost when numpy available; native operations align), cost-tier 2 = `ctypes.c_uint8` (always-available, medium cost), cost-tier 3 = `int & 0xFF` discipline (universal floor, high cost). All three are faithful (carry the 8-bit-natural-number structure); cost lens orders them; Grounding picks tier-1 when available, falls back through tiers as needed. **Faithful representation > target-conditioned omission** AND **cost lens > heuristic-or-bridge selection**. + + **Implication for `docs/design-numeric-construction.md:194-198`**: that doc's existing Python row (`Nat` for any N → Python `int` with "size hint informs runtime checks but doesn't change carrier") is **NOT a faithful representation** — it drops the width-structure to opaque metadata; the cost lens cannot read what isn't there. Reframing routes to **T-Numeric-Construction / Grounding lane paydown**: replace the size-hint-on-int row with a **cost-tiered table** of faithful representations (numpy.uint8 / ctypes.c_uint8 / int-and-mask-discipline) so the cost lens reads structural facts, not metadata. Not bundled here per scope; tracked-not-silent and routed to the cost-lens-bearing lane. **S3 dispatch unblocked on machine-constraint side** (independent of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815 — interaction semantics carries through under either). **Sub-decision 2's `.dag`-generated discipline** means S3 worker brief must specify the interaction substrate as `.dag`-declared with any Rust counterpart generated, not hand-authored. diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 56b3838dd00..598067e50d2 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -978,7 +978,7 @@ Substrate canvas + plan-poke-hole both folded in. Key absorptions: | Q-Anthropic-Variant-Aware | Variant-aware typed REST response projection carrier shape | Defer #1702 re-dispatch until Substrate authors variant-aware projection metadata carrier; #1702 branch preserved | RATIFIED-by-default | | Q-Emit-Shim-Handoff | Grounding direct execution vs PB/Substrate/v2-retirement consumption for `emit/rust_target.rs` family | Grounding consumes PB/v2-retirement milestones; no Grounding direct execution on these files | RATIFIED-by-default | | Q-Coercion-Fold-Scratch | Lane placement for `ScratchIntExamples` retirement | Grounding owns close after LanguageSpec projection executable | RATIFIED-by-default | -| Q-MachineConstraint-Carrier | Substrate carrier for `MachineConstraint` independent axis (per Brian directive 2026-05-06 — concrete types emerge from algebra × machine-constraint interaction; `i64` = `Int × MachineWidth<64>` consequence, NOT primary entity) | **6 sub-decisions ratified 2026-05-06 per Brian directives ("universal substrate, ratify defaults" + clarifying inline on sub-decisions 1, 2, 5, 6):** **(1) Axes in R3 scope** — `MachineWidth` only; `RegisterClass` / `EndianMode` / alignment / signedness-as-axis deferred post-R3. *Discipline note (Brian directive)*: this is a separation-of-facts/concerns exercise — algebra is one axis, machine constraint another, target lowering a *projection / coercion* over both; integer modeling is the canonical exercise. **(2) Interaction substrate shape** — **REST-API-style typed-contract interactions between models** (Brian directive: *"these models interact a la rest apis interacting — scalable / no dual representations (.dag generated)"*). Each model declares its interface in `.dag`; the interaction substrate is **`.dag`-generated**, never hand-coded. Hard constraint: **no dual representations** — any Rust counterpart must be generated from `.dag` (per `feedback_isomorphism_or_generation_for_mirrors` + `feedback_no_generated_code_on_disk`). Closed-enumeration lookup-maps and parallel Rust mirrors both rejected. **(3) Type-level spelling** — `Int<64>` parses/elaborates as `Compose>` parametrically; literal product `Int × MachineWidth<64>` is the surface intuition, not the substrate spelling. Equivalent under both algebra-side options per PR #1815. The interaction substrate that elaborates `Compose<...>` is `.dag`-generated per sub-decision 2. **(4) Approximate-algebra layering** — algebra-side approximation (`ApproximateField`) and machine-side approximation (`MachineWidth<64>`) stay as **independent axes that compose**; `Real<64>` = `Compose, MachineWidth<64>>` carries both layers explicitly per S8's named-axiom-relaxation discipline. **(5) Demonstration breadth — NOT a target** (Brian directive: *"3 is not a target, we shouldn't be 'targeting' modeling, we are just doing our best job to faithfully represent the concepts"*). 3-pair demonstration is the **minimum existence proof**, not the closure target. **Faithful representation of the concept is the closure criterion**; pair-counting is not. Once parser handles generic interaction syntax + substrate carries the algebra-machine separation, all valid pairs work by construction. Closure-gate predicate phrasing reflects "concept is faithfully modeled", not "≥3 pairs land". **(6) Target-specificity — universal substrate, faithful target lowering** (Brian directive elaborated): `MachineConstraint` is universal substrate. Targets lacking native machine-width semantics handle lowering by **faithfully representing the concept in a target-available primitive**, NOT by omission. For Python u8: lower to `numpy.uint8` / `ctypes.c_uint8` / explicit literal-bits — pick whichever Python idiom faithfully carries the 8-bit-natural-number concept. *Brian framing: "if python lacks — we would have to actually represent the struct using something that python faithfully provides — i.e. either literal bits or otherwise."* Faithful representation > target-conditioned omission. | RATIFIED 2026-05-06 (Brian initial directive + Brian clarifying inline on sub-decisions 1, 2, 5, 6). Substrate Mgr authors `MachineConstraint` + `MachineWidth` + `.dag`-generated interaction substrate per ratified scope. **Sub-decision 2's `.dag`-generated discipline binds**: any Rust counterpart for the interaction substrate must be generated, not hand-authored. S3 dispatch unblocked on machine-constraint side (independent of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815). | +| Q-MachineConstraint-Carrier | Substrate carrier for `MachineConstraint` independent axis (per Brian directive 2026-05-06 — concrete types emerge from algebra × machine-constraint interaction; `i64` = `Int × MachineWidth<64>` consequence, NOT primary entity) | **6 sub-decisions ratified 2026-05-06 per Brian directives ("universal substrate, ratify defaults" + clarifying inline on sub-decisions 1, 2, 5, 6):** **(1) Axes in R3 scope** — `MachineWidth` only; `RegisterClass` / `EndianMode` / alignment / signedness-as-axis deferred post-R3. *Discipline note (Brian directive)*: this is a separation-of-facts/concerns exercise — algebra is one axis, machine constraint another, target lowering a *projection / coercion* over both; integer modeling is the canonical exercise. **(2) Interaction substrate shape** — **REST-API-style typed-contract interactions between models** (Brian directive: *"these models interact a la rest apis interacting — scalable / no dual representations (.dag generated)"*). Each model declares its interface in `.dag`; the interaction substrate is **`.dag`-generated**, never hand-coded. Hard constraint: **no dual representations** — any Rust counterpart must be generated from `.dag` (per `feedback_isomorphism_or_generation_for_mirrors` + `feedback_no_generated_code_on_disk`). Closed-enumeration lookup-maps and parallel Rust mirrors both rejected. **(3) Type-level spelling** — `Int<64>` parses/elaborates as `Compose>` parametrically; first slot is the **algebraic concept** (fully-applied carrier+witness composite — `Int = AbelianGroup>` per #1466), second slot is the machine-constraint axis. **Critical correction (per codex BLOCKING 2026-05-06)**: prior phrasing `Compose>` was wrong — `AbelianGroup` is a *witness shape* over carrier `T` (per `dsl/std/algebra.dag:148-150`), not a carrier constructor; bare `AbelianGroup` in slot-1 composes witness rather than concept. Correct pattern: `UInt<64>` = `Compose>` (UInt = CommutativeMonoid), `Real<64>` = `Compose>` (Real = ApproximateField), `Nat<8>` = `Compose>`. Literal product `Int × MachineWidth<64>` is surface intuition; substrate spelling is parametric `Compose`. The interaction substrate that elaborates `Compose<...>` terms is `.dag`-generated per sub-decision 2 — *not* the `Compose<...>` *type itself* (parser/elaborator behavior). **(4) Approximate-algebra layering** — algebra-side approximation (`Real = ApproximateField`) and machine-side approximation (`MachineWidth<64>`) stay as **independent axes that compose**; `Real<64>` = `Compose>` carries both layers explicitly per S8's named-axiom-relaxation discipline (algebra approx is internal to `Real`'s definition; machine approx is the second slot). **(5) Demonstration breadth — NOT a target** (Brian directive: *"3 is not a target, we shouldn't be 'targeting' modeling, we are just doing our best job to faithfully represent the concepts"*). 3-pair demonstration is the **minimum existence proof**, not the closure target. **Faithful representation of the concept is the closure criterion**; pair-counting is not. Once parser handles generic interaction syntax + substrate carries the algebra-machine separation, all valid pairs work by construction. Closure-gate predicate phrasing reflects "concept is faithfully modeled", not "≥3 pairs land". **(6) Target-specificity — universal faithful representation, cost lens as the discriminator** (Brian directive elaborated 2x — initial "universal substrate, faithful lowering" + clarifying *"basically this would be represented by cost right — in all cases we should be able to represent the structure with literal bits/objects or whatever — the cost would be enormous — in those cases, we would look for alternatives like better modeling/libraries/int & 0xFF"*). `MachineConstraint` is universal substrate. **Universality of faithful representation**: every target language CAN faithfully represent every concept (literal-bits / direct-object construction is the always-available floor). **Cost lens (T-CostLens-Composition) is the discriminator** that orders faithful-representation alternatives by per-primitive realization cost — gates `cost_lens_reads_target_realization` + `coercion_cost_equals_complexity_by_construction` make "selection among faithful representations IS the cost-lens application" structural-not-conventional. Grounding selects the lowest-cost faithful representation by reading the cost-lens output. For Python u8: cost-tier 1 = `numpy.uint8` (low cost; native operations), cost-tier 2 = `ctypes.c_uint8` (medium), cost-tier 3 = `int & 0xFF` discipline (universal floor, high). All three are faithful; cost lens orders; Grounding picks. Faithful representation > target-conditioned omission; cost lens > heuristic-selection. **Implication for `docs/design-numeric-construction.md:194-198`**: existing Python row (`Nat` → `int` with size-hint metadata) is **non-faithful** — drops width-structure to opaque metadata, cost lens cannot read what isn't there. Reframe routes to T-Numeric-Construction / Grounding lane paydown: replace size-hint-on-int row with cost-tiered faithful-representation table so cost lens reads structural facts. Not bundled in this PR per scope; tracked-not-silent. | RATIFIED 2026-05-06 (Brian initial directive + Brian clarifying inline on sub-decisions 1, 2, 5, 6). Substrate Mgr authors `MachineConstraint` + `MachineWidth` + `.dag`-generated interaction substrate per ratified scope. **Sub-decision 2's `.dag`-generated discipline binds**: any Rust counterpart for the interaction substrate must be generated, not hand-authored. S3 dispatch unblocked on machine-constraint side (independent of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815). | | Q-Verification-NYI-Carry-Forward | Closure-criteria alignment for cross-program Verification rows: which predicates must execute in R3 vs remain honest NYI with explicit incomplete classification until evaluator lands? | Per §1.6 demonstration-gate minimum bar (Director finding 1.1): predicates without runtime evaluator execution canNOT claim "GREEN" closure; honest NYI classification with explicit carry-forward owner required. R3-Verification rows that depend on evaluator runtime that's NYI at R3 close → explicit NYI + named carry-forward Mgr (NOT silent assumption of evaluator landing). | RATIFIED-by-default per Director finding 1.1 minimum bar; closure-ledger reports separate "demonstration-executes" vs "static-fact" status per row (per §1.6). Verification Mgr ratifies per-row carry-forward classification at lane-close audit. | | Q-ValueBody-Isomorphism | ValueBody Rust↔.dag mirror drift gate — structural-isomorphism / conformance gate in R3 close, OR explicit post-R3 carry with named owner? Mirror divergence risk + no CI isomorphism gate currently. | Per `feedback_isomorphism_or_generation_for_mirrors`: Rust↔.dag mirrors need generation-or-isomorphism-test, not hand-maintenance. R3 zero-debt-close framing implies isomorphism gate IN R3 scope — gate fires at R3 close requiring CI conformance test. Owner: R3 Substrate Mgr (mirror authority) + Verification Mgr (test-only pressure). | OPEN — Director + R3 Substrate Mgr + Brian scoping needed (NEW 2026-05-06 from Verification Mgr canvas item 6) | | Q-Slice-C-Shape | Slice C `.dag` files in #1795 follow-up: prose+regen-bundling (path-(a) precedent) vs separate sub-slice carve-out | Path-(a) precedent from #1795 establishes regen-bundling-acceptable; default to single-PR prose+regen. | RATIFIED-by-default (Substrate Mgr B1) |