diff --git a/docs/r3-design-schedule-2026-05-06.md b/docs/r3-design-schedule-2026-05-06.md index 665b573522f..7b690557baa 100644 --- a/docs/r3-design-schedule-2026-05-06.md +++ b/docs/r3-design-schedule-2026-05-06.md @@ -37,7 +37,13 @@ ### S3 — `MachineConstraint` carrier design (Brian directive 2026-05-06) -**Scope**: design substrate carriers for **algebra × machine-constraints interaction modeling** per Brian directive: concrete types like `i64` emerge as products of independent constraint axes (algebra `Int = AbelianGroup` × machine `MachineWidth<64>`), NOT primary entities. +**Scope**: design substrate carriers for **algebra × machine-constraints interaction modeling** per Brian directive: concrete types like `i64` emerge as products of independent constraint axes (algebra side × machine `MachineWidth<64>`), NOT primary entities. + +**P1 axiom-violation paydown (2026-05-06; Brian directive)**: prior framing `Int = AbelianGroup` is **structurally false** — Nat is a commutative monoid under +, not the carrier of an Abelian group (no additive inverses in {0,1,2,...}). Per ratified self-correction at [gunbc#1739 issuecomment-4385432940](https://github.com/gunb-ai/gunbc/issues/1739#issuecomment-4385432940) (cross-ref: Director-side memory entry `feedback_verify_algebraic_axioms_in_ratification` logs the discipline going forward). Two mathematically sound options pending design selection (worker judgment per `feedback_compositional_not_templating`): +- **Option A** — `Int` as canonical AbelianGroup primitive (terminal, no Nat parameter). Severs the constructive Nat→Int edge; `Int` is just-ℤ, not derived. +- **Option B** — `Int ≡ GroupCompletion>` (Grothendieck). Algebra-faithful; preserves compositional Nat→Int edge; introduces `GroupCompletion` as new substrate (P1 procedure required: name second consumer beyond Int OR justify single-consumer via P1 carve-out). + +Prior `AbelianGroup` references in r3-structure.md, r3-program-plan.md, this doc are **DEFERRED-shorthand** until design selection lands. **T-Numeric-Construction further dispatch HELD** (Brian directive 2026-05-06) until algebra-side selection ratified. S3 (`MachineConstraint`) interaction modeling proceeds in parallel — once algebra-side resolves, the interaction `Int = Int × MachineWidth` semantics carries through identically under either option (Int participates as AbelianGroup carrier in both). Carriers needed: `MachineConstraint` + `MachineWidth` + interaction-lookup substrate. May require additional axes (`RegisterClass`, `EndianMode`, alignment) per use cases. diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index e3338e4bcee..0ceb595e9a8 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -71,7 +71,7 @@ Per `r3-debt-sweep-2026-05-06.md` §Class A (line 39): *"parser/grammar surface, | Class | TestClaim gate | Representative gap-test | Lane(s) producing closure | |---|---|---|---| -| 1 — parser/grammar surface | `substrate_gap_parser_grammar_closed` | v3 substrate models concrete types as the **interaction of independent constraint models** — abstract algebra × machine constraints — with concrete types emerging as consequences (per Brian directive 2026-05-06: *"these concepts should be the interaction of several constraint models i.e. abstract algebra × machine constraints — i64 would naturally emerge as a consequence"*). Refinement syntax `Type` expresses the interaction, NOT a primary entity. Pass condition: substrate declares abstract algebra (e.g., `Int = AbelianGroup`) and machine constraints (e.g., `MachineWidth`) as independent models; concrete types emerge via interaction (e.g., `Int<64>` = `Int × MachineWidth<64>`; target-language `i64` is derived artifact, NOT primary substrate entity). v3 parser handles generic interaction syntax; demonstrated against ≥3 algebra×constraint pairs — `Int<64>` (integer × 64-bit register), `Real<64>` (real × 64-bit float), `Nat<8>` (natural × 8-bit register) — without v2-fallback; gate Pass = all 3 interaction-derived programs produce 0 diagnostics + emitted artifact compiles to expected target primitive (`i64`/`f64`/`u8`) where the target primitive is consequence-of-interaction, not declared. The interaction-modeling requirement prevents single-axis (algebra-only or width-only) hard-coding. | T-V2-Retirement (parser path) + T-Numeric-Construction (algebra side) + Substrate (machine-constraint side, may require new substrate carrier `MachineConstraint`) + Substrate continuation | +| 1 — parser/grammar surface | `substrate_gap_parser_grammar_closed` | v3 substrate models concrete types as the **interaction of independent constraint models** — abstract algebra × machine constraints — with concrete types emerging as consequences (per Brian directive 2026-05-06: *"these concepts should be the interaction of several constraint models i.e. abstract algebra × machine constraints — i64 would naturally emerge as a consequence"*). Refinement syntax `Type` expresses the interaction, NOT a primary entity. Pass condition: substrate declares abstract algebra (e.g., `Int` as canonical AbelianGroup carrier — Option A canonical-primitive **OR** Option B `GroupCompletion>`; design selection pending per P1 axiom-violation paydown 2026-05-06 — prior `Int = AbelianGroup` shorthand was structurally false [Nat lacks additive inverses]; ratification at [gunbc#1739 issuecomment-4385432940](https://github.com/gunb-ai/gunbc/issues/1739#issuecomment-4385432940) + memory entry `feedback_verify_algebraic_axioms_in_ratification`) and machine constraints (e.g., `MachineWidth`) as independent models; concrete types emerge via interaction (e.g., `Int<64>` = `Int × MachineWidth<64>`; target-language `i64` is derived artifact, NOT primary substrate entity). v3 parser handles generic interaction syntax; demonstrated against ≥3 algebra×constraint pairs — `Int<64>` (integer × 64-bit register), `Real<64>` (real × 64-bit float), `Nat<8>` (natural × 8-bit register) — without v2-fallback; gate Pass = all 3 interaction-derived programs produce 0 diagnostics + emitted artifact compiles to expected target primitive (`i64`/`f64`/`u8`) where the target primitive is consequence-of-interaction, not declared. The interaction-modeling requirement prevents single-axis (algebra-only or width-only) hard-coding. | T-V2-Retirement (parser path) + T-Numeric-Construction (algebra side) + Substrate (machine-constraint side, may require new substrate carrier `MachineConstraint`) + Substrate continuation | | 2 — function-valued data | `substrate_gap_function_valued_data_closed` | `Lens` instance with function-typed payload executes through evaluator | T-Lens-Application-Surface + T-E-P-Producer-Broadening — **chain-break per YELLOW chain rule** (Substrate Mgr 2026-05-06): prereq T-Lens-Application-Surface ← T-Lens-Behavioral-Parity ← Q-Lens-Behavioral-Parity-R3-Closeability (RED). Class 2 inherits RED until LBP scope-calibration resolves. See Q-Class-2-Chain-Break in §10.3. | | 3 — file-ingestion | `substrate_gap_file_ingestion_closed` | One `.dag` program ingests external file (e.g., timing observation set) without `include_str!` | T-Workflow-As-Data | | 4 — workflow/scheduling | `substrate_gap_workflow_scheduling_closed` | CI workflow modeled as `.dag` data executes through evaluator | T-Workflow-As-Data + T-Lens-Self-Application | diff --git a/docs/r3-structure.md b/docs/r3-structure.md index 9484a852780..6651558cf00 100644 --- a/docs/r3-structure.md +++ b/docs/r3-structure.md @@ -89,7 +89,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine- - `pb_self_compile_fixed_point` (R1 gate; closes here under stronger interpretation) — v3 binary compiles `compiler.dag` and produces bit-identical stage0 Rust + bit-identical emitted artifacts. Predicate is the same R1 predicate; R3 closes it under fixed-point semantics rather than the looser "compiler can compile itself" reading - **Two-horizon clarification (per R1 Closure Manager review 2026-04-28):** the predicate name `pb_self_compile_fixed_point` carries TWO horizons: (i) **R1 lane gate** — Pass = current `verification.dag` + `test_runner` evaluation under the R1 acceptance discipline; this is what `#1050` + `#1074` made green at landing. (ii) **R3 thesis facet 2** — closes under the stronger interpretation (bit-identical fixed-point + SG-0 choreography per Director decisions). **R1 close does NOT wait on R3.** R1's gate Pass is whatever the current predicate evaluates to; R3's elevated bar is a separate release/thesis acceptance, not a silent rename of the R1 predicate. See `r2-structure.md` §"R1 closure criteria" for the R1-side framing. - **T-Numeric-Construction (REFRAMED 2026-05-01 from T-Int128).** Acceptance gates per [`docs/design-numeric-construction.md`](design-numeric-construction.md): - - `numeric_abstract_carriers_landed` — Magnitude (terminal), Nat (Semiring), Int (AbelianGroup), Rational (Field), Real (ApproximateField) declared in `dsl/std/integer.dag` + `dsl/std/float.dag` + - `numeric_abstract_carriers_landed` — Magnitude (terminal), Nat (Semiring), Int (canonical AbelianGroup primitive **OR** `GroupCompletion>` — **design selection pending** per P1 axiom-violation paydown 2026-05-06; prior `Int = AbelianGroup` shorthand is structurally false — Nat lacks additive inverses; see [gunbc#1739 issuecomment-4385432940](https://github.com/gunb-ai/gunbc/issues/1739#issuecomment-4385432940) + [`docs/design-numeric-construction.md`](design-numeric-construction.md) §3), Rational (Field), Real (ApproximateField) declared in `dsl/std/integer.dag` + `dsl/std/float.dag` - `numeric_width_refinements_landed` — `Int`, `Nat`, `Real` refinement chain resolves at compile time - `numeric_aliases_align_to_refinements` — `Int8`/.../`Int128`, `Float32`/`Float64`, `UInt8`/.../`UInt128` are refinements, not parallel substrate - `numeric_inherited_bake_ins_dissolved` — `Char`, `EpochMs`, `Duration`, `Milliseconds`, `Seconds` consume abstract `Int` (or appropriate refinement) @@ -170,7 +170,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine- - `apply_lens_self_application_demonstrated` — `apply_lens(timing, ci_workflow, Enforce { budget: max_ns })` enforced via existing `EnforcedApplication` carrier (per T-Lens-Application-Surface §2 + §3.2); fail-closed when observation reports `Missing | Ambiguous | Stale` per timing-lens design; demonstrates that user-authored apply_lens substrate generalizes to project-self-validation use case - `recursive_flex_demonstration_landed` — narrative-load-bearing thesis claim cashes in worked instance: *"the compiler that compiles gunbc programs validates the workflow that produces gunbc itself."* Compiler-people read this as the categorical move that the lens framework isn't just for user code — it applies recursively to gunbc's own runtime behavior. Either emit-back-to-CI-YAML (bidirectional case via T-Workflow-As-Data) OR direct execution. <1 min CI target tracked as informational SLO; **not a closure gate** (per Director ratification 2026-05-04 — performance metric, not structural commitment) - **Substrate-gap-class closure** (NEW 2026-05-06; per Brian directive at [gunbc#846](https://github.com/gunb-ai/gunbc/issues/846); closure-criteria over existing lane work, NOT new separate lanes — added without expanding R3 lane count). Five class-level closure gates each closing when **both** (per [`docs/r3-program-plan.md`](r3-program-plan.md) §1.4 conjunctive predicate; Director poke-hole 2026-05-06 finding 1.3 + openai-pro 2026-05-06 finding 2.2): **(a)** representative gap-test executes through v3 cleanly per Pass condition AND **(b)** systematic enumeration of class-bridges shows count = 0 (or any survivors carry explicit Director allocation per `docs/audit/r3-debt-sweep-2026-05-06.md` §3.A STRUCTURAL exception). Single-test-pass alone is sample-of-class, NOT closure-of-class; conjunctive predicate prevents class reading "GREEN" while real bridges in that class persist unexercised by the chosen representative. Per [`docs/r3-program-plan.md`](r3-program-plan.md) §1.4 + §4. - - `substrate_gap_parser_grammar_closed` — v3 substrate models concrete types as the **interaction of independent constraint models** — abstract algebra × machine constraints — with concrete types emerging as consequences (per Brian directive 2026-05-06 at [gunbc#846 inline](https://github.com/gunb-ai/gunbc/pull/1808): *"these concepts should be the interaction of several constraint models i.e. abstract algebra × machine constraints — i64 would naturally emerge as a consequence"*). Refinement syntax `Type` expresses the interaction, NOT a primary entity. Substrate declares abstract algebra (e.g., `Int = AbelianGroup`) and machine constraints (e.g., `MachineWidth`) as **independent** models; concrete types emerge via interaction (e.g., `Int<64>` = `Int × MachineWidth<64>`; target-language `i64` is derived artifact, not primary substrate entity). Pass condition: ≥3 algebra×constraint pairs (`Int<64>` / `Real<64>` / `Nat<8>`) lower through stage0 emission without v2-fallback; emitted artifact compiles to expected target primitive (`i64` / `f64` / `u8`) where target primitive is consequence-of-interaction. Closes via T-V2-Retirement parser path + T-Numeric-Construction (algebra side) + Substrate continuation (machine-constraint side; may require new `MachineConstraint` substrate carrier) + - `substrate_gap_parser_grammar_closed` — v3 substrate models concrete types as the **interaction of independent constraint models** — abstract algebra × machine constraints — with concrete types emerging as consequences (per Brian directive 2026-05-06 at [gunbc#846 inline](https://github.com/gunb-ai/gunbc/pull/1808): *"these concepts should be the interaction of several constraint models i.e. abstract algebra × machine constraints — i64 would naturally emerge as a consequence"*). Refinement syntax `Type` expresses the interaction, NOT a primary entity. Substrate declares abstract algebra (e.g., `Int` as canonical AbelianGroup carrier — design selection pending Option A canonical-primitive vs Option B `GroupCompletion>`; prior `Int = AbelianGroup` shorthand was structurally false per P1 axiom paydown 2026-05-06, see [gunbc#1739 issuecomment-4385432940](https://github.com/gunb-ai/gunbc/issues/1739#issuecomment-4385432940)) and machine constraints (e.g., `MachineWidth`) as **independent** models; concrete types emerge via interaction (e.g., `Int<64>` = `Int × MachineWidth<64>`; target-language `i64` is derived artifact, not primary substrate entity). Pass condition: ≥3 algebra×constraint pairs (`Int<64>` / `Real<64>` / `Nat<8>`) lower through stage0 emission without v2-fallback; emitted artifact compiles to expected target primitive (`i64` / `f64` / `u8`) where target primitive is consequence-of-interaction. Closes via T-V2-Retirement parser path + T-Numeric-Construction (algebra side) + Substrate continuation (machine-constraint side; may require new `MachineConstraint` substrate carrier) - `substrate_gap_function_valued_data_closed` — `Lens` instance with function-typed payload executes through evaluator and produces `DimensionReport` without Rust mediation. Closes via T-Lens-Application-Surface + T-E-P-Producer-Broadening - `substrate_gap_file_ingestion_closed` — One `.dag` program ingests external file (timing observation set, JSON config) without `include_str!`; exercises file-ingestion grammar. Closes via T-Workflow-As-Data - `substrate_gap_workflow_scheduling_closed` — CI workflow modeled as `.dag` data executes through evaluator + produces `DimensionReport`. Closes via T-Workflow-As-Data + T-Lens-Self-Application