diff --git a/docs/briefs/r3-substrate-emission-provenance-lens-worker.md b/docs/briefs/r3-substrate-emission-provenance-lens-worker.md index 97331e900ed..2a1f466c028 100644 --- a/docs/briefs/r3-substrate-emission-provenance-lens-worker.md +++ b/docs/briefs/r3-substrate-emission-provenance-lens-worker.md @@ -151,9 +151,14 @@ Author cementing test that: reuses T-CostLens cementing-test source corpus) 2. Emits target-language output (Rust acceptance target) 3. Runs `Lens>` over the same source -4. **Verifies**: every emitted line has a corresponding - `EmissionProvenance` entry in the per-Behavior aggregate; flatten - to per-line view matches emitted-line numbering +4. **Verifies (scoped to Behavior-attributable lines only)**: every + emitted line that traces to a Behavior in the source `.dag` has a + corresponding `EmissionProvenance` entry in the per-Behavior + aggregate; flatten to per-Behavior-attributable-line view matches + the emitted-line subset. Declarations + program scaffold + (prelude / function / main-wrapper sections) are OUT-OF-SCOPE per + codex Finding #2 at sha 4229cd09 — separate substrate cascade if + needed 5. **Verifies field population**: every entry's `rule` field-path resolves to a real `*SyntaxBinding`/`*OpsBinding` field (round-trip: emitter writes field-path → lens recovers same @@ -189,11 +194,15 @@ Phase ordering (PR-internal): - `Lens>` instance landed per 6-field Director-locked shape; T-CostLens-Composition precedent verified for shape parity -- Cementing test landed: per-Behavior fold output flattens to per-line - view matching emitted-line numbering; ≥1 entry with span-Some + ≥1 - entry with span-None; field-path round-trip verified (every - `rule` field-path resolves to a real `*SyntaxBinding`/`*OpsBinding` - field at HEAD) +- Cementing test landed (scope = **Behavior-attributable lines only**; + declarations + program scaffold OUT-OF-SCOPE per codex Finding #2 + at sha 4229cd09 — separate substrate cascade if needed): per-Behavior + fold output flattens to per-Behavior-attributable-line view; ≥1 + Behavior-attributable entry with span-Some + ≥1 Behavior-attributable + entry with span-None; field-path round-trip verified (every `rule` + field-path resolves to a real `*SyntaxBinding`/`*OpsBinding` field at + HEAD; STOP if field-path threading requires substrate cascade per + codex Finding #1) - §1.8 row `emission_provenance_lens_landed` advances DECLARED → PRODUCER_LANDED (Grounding-consumer for visualization wiring is a separate downstream brief if needed; not bundled per Director @@ -208,6 +217,8 @@ Phase ordering (PR-internal): ## STOP-AND-ESCALATE - **`*SyntaxBinding` / `*OpsBinding` field set materially differs from Reading C catalog at HEAD** (e.g., heavy refactor renamed the structs): STOP — substrate-state-divergence; surface to Substrate Mgr; brief absorbs corrected field-path enumeration before authoring +- **Field-path identity not threadable through emission runtime** (per codex BLOCKING at PR #1910 sha 4229cd09 Finding #1, post-merge): the `render_named_template(...)` call site receives a template *value* extracted from the binding struct field — the field-path that names the rule may not be carried alongside the value at emission time. If lens `read` cannot recover field-path from runtime emission state without structural threading (typed template-with-rule-path or DeclarationRef carrier wrapping the template), STOP and surface — that's a substrate-fact-introduction cascade (separate brief; thread rule-path through binding carrier before lens consumes). Worker DFS at dispatch confirms whether field-path threading is structurally possible OR requires substrate cascade +- **Non-Behavior emission coverage gap** (per codex BLOCKING at PR #1910 sha 4229cd09 Finding #2): `Lens.read: fn(Dag, Behavior) -> Witness>` is per-Behavior; emitted output also includes declarations + program scaffold (e.g., `pub mod`, file headers, `#[derive(...)]` on declared types). Brief Acceptance scope is **Behavior-attributable lines only** — declarations and program scaffold are out-of-scope for this slice. If cementing test surfaces emitted lines unattributable to any Behavior (i.e., the per-Behavior fold doesn't see them), STOP and surface — declared-provenance / scaffold-provenance is separate substrate-fact-introduction (different lens or per-Declaration extension). Acceptance bullet narrowed below to "≥1 Behavior-attributable span-Some + ≥1 Behavior-attributable span-None" rather than full-emission coverage - **`iterate` identity assumption breaks** (body emitted multiple times per LoopBound, NOT once): STOP — surface to Substrate Mgr; lens iterate field shape may need rework diff --git a/docs/briefs/r3-substrate-int-platform-uint-platform-worker.md b/docs/briefs/r3-substrate-int-platform-uint-platform-worker.md new file mode 100644 index 00000000000..2512b560d9e --- /dev/null +++ b/docs/briefs/r3-substrate-int-platform-uint-platform-worker.md @@ -0,0 +1,149 @@ +--- +status: pre-authored per pre-authored-brief-queue discipline; dispatchable post-PR-#1914 close (valiant-ibex-312 freed-pool) +authority parent: R3 Substrate Manager (#1739) +ratification: Director Q1 + Q2 + Q3 + Q4 RATIFIED at gunbc#1739 #issuecomment-4393248961 (zesty-bear-812, 2026-05-07). Naming: IntPlatform/UIntPlatform per `feedback_reason_not_label`. Algebra: `Compose>` + `Compose>` with Platform as substrate token (target-dependent at grounding). Substrate-concept layer (NOT target-only). Worker pin valiant-ibex-312. +roadmap row: §1.8 ledger row TBD slot — gate `int_platform_uint_platform_substrate_landed` (or canonical equivalent at PR-authoring time) +authority docs: + - gunbc#1739 #issuecomment-4393248961 (Director Q1+Q2+Q3+Q4 RATIFICATION) + - gunbc#1761 #issuecomment-4393222862 (valiant-ibex-312 STOP surfacing the substrate gap from Phase B) + - gunbc#828 #issuecomment-4385530115 (Q-MachineConstraint sub-decision 3 — Compose> shape; this brief extends N with substrate-token Platform) + - dsl/std/integer.dag (consumer site for IntPlatform/UIntPlatform declarations) + - src/v3/std/machine_constraints.dag (existing MachineWidth carrier; this brief extends to MachineWidth) + - PR #1914 (T-Interval-Representation; closes at partial coverage; this brief is the follow-on enabling isize/usize row population) +gates: + - `int_platform_uint_platform_substrate_landed` (proposed §1.8 row) +worker pin: valiant-ibex-312 (freed-pool post-PR-#1914 close; freshest substrate context from BigInt widening + Phase B coverage) +--- + +# R3 Substrate — `IntPlatform` / `UIntPlatform` substrate-fact-introduction worker brief + +## Context + +Per Director RATIFICATION at gunbc#1739 #issuecomment-4393248961 (Q1+Q2+Q3+Q4): + +PR #1914 (T-Interval-Representation; bundled Rust-primitive-full-coverage) closes at u128 + Phase A coverage; isize/usize rows in `src/v3/spec/rust.dag` deferred to this follow-on. Substrate gap surfaced by valiant-ibex-312 STOP at gunbc#1761 #issuecomment-4393222862: + +`TargetIntegerTypeInhabitance.kernel_integer: DeclarationRef` requires a std integer type. Existing rows reference `UInt32` / `Int32` / `Int` / `Int128` / `UInt128`. **`dsl/std/integer.dag` has no platform-sized integer carrier** (no IntPlatform / UIntPlatform / equivalent). + +This brief lands the substrate concepts. + +### Director ratifications absorbed + +- **Q1 — Naming: `IntPlatform` / `UIntPlatform`** per `feedback_reason_not_label` ("encode the stable reason"). Platform-dependence is the structural distinction; size alone doesn't distinguish (Int<32> also has size). +- **Q2 — Algebra: same Int / UInt; platform-axis on MachineConstraint**: + - `IntPlatform` = `Compose>` where `Int = AbelianGroup>` (per Slice 3 #1466) + - `UIntPlatform` = `Compose>` where `UInt = CommutativeSemiring` (per #1818) + - `Platform` is itself a substrate token (NOT a fixed numeric width); targets ground at emit time +- **Q3 — Substrate-concept layer (NOT target-only)** per `feedback_target_agnostic_ir`. Multiple targets have platform-sized integers; modeling them at substrate-concept layer keeps substrate target-agnostic +- **Q4 — Worker pin valiant-ibex-312** post-PR-#1914 close + +## Scope + +### Deliverable 1 — `Platform` substrate token + +Author `Platform` substrate token in `src/v3/std/machine_constraints.dag` (or canonical adjacent location — worker greps for existing convention). Shape: substrate token consumed by `MachineWidth` similarly to existing `MachineWidth` form for fixed widths. + +Two structural shapes worker DFS-decides at dispatch: + +- **Option α (sum type)**: `type Platform = Pointer | TargetSpecific(String)` or similar enumeration of platform-axis classes +- **Option β (opaque token)**: `type Platform` (uninhabited or single-witness) — used purely as type-level marker; targets project to specific width at emit time +- **Option γ (typed parameter)**: `MachineWidth` parameterized over a Platform type-parameter that's bound by target spec at grounding + +**Mgr recommendation**: γ (typed parameter) if the existing `MachineWidth` shape parameterizes over numeric N — adds Platform as a sibling-shape kind alongside numeric. β if simpler / matches existing token discipline. α only if explicit platform-axis enumeration carries structural meaning. + +Worker DFS catalogs current `MachineWidth<...>` parameterization shape at HEAD; chooses α/β/γ per existing convention. + +### Deliverable 2 — `IntPlatform` / `UIntPlatform` declarations + +Author in `dsl/std/integer.dag`: + +```dag +type IntPlatform = Compose> +type UIntPlatform = Compose> +``` + +Practice 4 classification: N/A — these are type aliases over existing `Compose<...>` carrier, not new sum types or coproducts. Worker confirms no new variant introduction. + +### Deliverable 3 — `src/v3/spec/rust.dag` isize/usize rows + TargetIntegerTypeInhabitance population + +Add rows: +- `rust_integer_inhabit_isize_platform`: `TargetIntegerTypeInhabitance` referencing `IntPlatform` via `kernel_integer` DeclarationRef + `bound: PlatformDependentFact` +- `rust_integer_inhabit_usize_platform`: parallel for `UIntPlatform` + +Existing `TypeRealization` rows for `rust_isize` / `rust_usize` co-author per `spec/rust.dag` row population convention. + +### Deliverable 4 — Cross-target signal (informational, not in-scope authoring) + +Targets without native platform-sized integers (Python's arbitrary-precision `int`, etc.) handle ground-time via target-conditioned **lowering** — NOT target-conditioned substrate. Per Director Q3 ratification: substrate stays clean; Grounding-lane handles target-side projection. + +This brief produces the substrate concepts; cross-target consumer wiring (Python / Go / etc.) is separate Grounding-tier work. + +### Deliverable 5 — §1.8 ledger row receipt + +Add `int_platform_uint_platform_substrate_landed` to §1.8 ledger; advance DECLARED → CONSUMER_LANDED on merge (consumer = Rust-target row population in same PR via Deliverable 3). Cluster: T-Numeric-Construction-adjacent (or new T-Platform-Integer cluster — Mgr discretion at PR-authoring time). + +Co-receipt: PR #1914's `rust_primitive_full_coverage` gate advances PARTIAL → CONSUMER_LANDED on this PR's merge (full Rust integer primitive coverage closed via this slice's isize/usize rows). + +## Slice — single PR + +Phase ordering (PR-internal): +1. DFS-catalog `MachineWidth<...>` parameterization at HEAD; choose α/β/γ for `Platform` token +2. Author `Platform` substrate token (Deliverable 1) +3. Author `IntPlatform` / `UIntPlatform` declarations (Deliverable 2) +4. Author `src/v3/spec/rust.dag` isize/usize TargetIntegerTypeInhabitance rows + TypeRealization rows (Deliverable 3) +5. Bootstrap snapshot regen + parse corpus manifest refresh; integer-row ratchet update (10 → 12 in `int_literal_ranges.rs`) +6. §1.8 ledger row receipt (Deliverable 5) + co-receipt for `rust_primitive_full_coverage` gate advancement +7. Cross-program handoff receipt to Grounding Mgr (#1745) for G2 Phase 2 isize/usize-coverage dispatch unblock + +## Acceptance + +- `Platform` substrate token landed in `src/v3/std/machine_constraints.dag` (or canonical equivalent) per α/β/γ shape worker chooses +- `IntPlatform` / `UIntPlatform` declarations landed in `dsl/std/integer.dag` consuming `Compose>` shape per Director Q2 ratification +- `src/v3/spec/rust.dag` has isize/usize TargetIntegerTypeInhabitance rows + TypeRealization rows; bound: PlatformDependentFact (existing variant per PR #1914 carrier-shape verification) +- Integer-row ratchet at `int_literal_ranges.rs` updated 10 → 12 rows (post-PR-#1914 baseline) +- Bootstrap snapshot + parse corpus manifest hold (semantic equivalence on existing 10 rows; 2 new rows added) +- §1.8 row `int_platform_uint_platform_substrate_landed` advances DECLARED → CONSUMER_LANDED upon merge +- Co-receipt: PR #1914's `rust_primitive_full_coverage` gate advances PARTIAL → CONSUMER_LANDED on this PR's merge +- Cross-program handoff receipt to Grounding Mgr (#1745) — G2 Phase 2 isize/usize coverage unblocked +- `cargo test --workspace --exclude v2-compiler-tests` green (3 pre-existing v2-compiler --lib failures verified unrelated) +- `cargo test -p v2-compiler-tests` green; strict-compile diagnostic ratchet at 0 +- `cargo clippy --all-targets -- -D warnings` clean +- `cargo fmt --all --check` clean +- Citation discipline per `docs/briefs/brief-authoring-checklist.md` +- 5-question authority audit in PR body +- P1 substrate-fact-introduction receipt: + - DFS-of-concept-DAG (no parallel platform-integer carrier already exists at HEAD) + - Named consumer demand (Rust-target isize/usize rows; Grounding G2 Phase 2 partial-coverage cascade) + - Carrier-shape rationale (α/β/γ decision) + +## STOP-AND-ESCALATE + +- **`MachineWidth<...>` parameterization shape doesn't accept `Platform` token** (e.g., parser blocks non-numeric type arguments in second slot): STOP — surface to Substrate Mgr; parser/lowerer extension may be needed OR β opaque-token form needed instead of γ typed-parameter +- **`Compose<...>` interaction syntax encoding doesn't accept the proposed `IntPlatform` / `UIntPlatform` shape**: STOP — surface; parallel concern to S3 Phase-2 parser-grammar work; coordinate with valiant-ant-72 if relevant +- **Bootstrap snapshot drift** during Platform/IntPlatform/UIntPlatform/spec-rust-row authoring: root-cause; do NOT bridge with placeholder +- **Cross-target Grounding-lane consumers surface unforeseen blockers** (e.g., Python target requires substrate-side decision rather than Grounding-side projection): STOP — surface; Director Q3 ratified substrate-clean; if breaks, re-ratify +- **Bundled-scope drift**: do NOT bundle Grounding G2 Phase 2 lowering rules / emit verification into this PR. Per Director bundled-scope ratification at gunbc#1739 #issuecomment-4392225548 — parallel infrastructure DISALLOWED. This brief produces substrate; Grounding consumes follow-on + +## Authority audit receipt + +1. **Substrate exists?** At brief-author time: + - `Compose` carrier landed (PR #1856) ✓ + - `MachineWidth` carrier landed (PR #1856) ✓ — for fixed numeric widths + - `Int` / `UInt` algebraic-concept carriers landed (#1466 / #1818) ✓ + - `TargetIntegerInhabitanceBound::PlatformDependentFact` variant exists on origin/main HEAD (per PR #1914 Phase B ratification-state-grep) ✓ + - `Platform` substrate token does NOT yet exist — this brief is producer + - `IntPlatform` / `UIntPlatform` carriers do NOT yet exist — this brief is producer +2. **Existing brief?** No prior brief on this axis. PR #1914 (T-Interval-Representation; partial coverage) is the upstream brief that surfaced the gap; this brief is the named follow-on +3. **Design-doc match?** Director Q1+Q2+Q3+Q4 RATIFIED at gunbc#1739 #issuecomment-4393248961 + Q-MC sub-decision 3 (gunbc#828 #issuecomment-4385530115) name the shape verbatim +4. **Citations live?** Worker re-verifies at dispatch (post-PR-#1914 close) +5. **Carrier dissolves the bridge?** Yes — `Platform` substrate token + `IntPlatform`/`UIntPlatform` declarations together dissolve the "isize/usize have no representable substrate concept" bridge. Substrate stays target-agnostic per `feedback_target_agnostic_ir`; targets ground at emit time + +## Provenance + +Drafted 2026-05-07 by Substrate Mgr (quick-crab-830) per Director Q1+Q2+Q3+Q4 RATIFICATION at gunbc#1739 #issuecomment-4393248961. Pre-authored per pre-authored-brief-queue discipline; dispatch fires post-PR-#1914 close (valiant-ibex-312 freed-pool from T-Interval-Representation; freshest context for follow-on per Director Q4). + +Cross-references: +- PR #1914 (T-Interval-Representation partial-coverage; this brief is named follow-on) +- Q-MC sub-decision 3 (`Compose>` shape; this brief extends N with substrate-token Platform) +- Grounding G2 Phase 2 (consumer; isize/usize coverage unblocks on this brief's PR merge) +- S3 Phase-2 parser-grammar (potential coordination point if `MachineWidth` non-numeric parameterization surfaces parser concerns) diff --git a/docs/briefs/r3-substrate-rust-primitive-full-coverage-worker.md b/docs/briefs/r3-substrate-rust-primitive-full-coverage-worker.md index e66618d7ce2..8e221ff39b8 100644 --- a/docs/briefs/r3-substrate-rust-primitive-full-coverage-worker.md +++ b/docs/briefs/r3-substrate-rust-primitive-full-coverage-worker.md @@ -28,13 +28,13 @@ coupled substrate gaps that this brief lands as **one bundled slice**. 1. **`IntervalInt::ExactInterval` host-repr gap**: `src/v3/compiler/src/int_literal_ranges.rs` parses all integer ranges as `i128` host representation; `u128::MAX` exceeds `i128` range. `dsl/extdeps/languages/rust/primitives.dag` explicitly defers `u128` because of this. Substrate widening required (BigInt-based or alternative encoding). -2. **Bound-carrier wiring gap on actual row surface**: the live row surface used by `src/v3/spec/rust.dag` is `TargetIntegerTypeInhabitance` (with bound-field type `TargetIntegerInhabitanceBound`) imported from `v3.std.emit_model` — NOT a generic `RustPrimitive` carrier. Per codex BLOCKING (PR #1910) verified at HEAD: live shape is `TargetIntegerInhabitanceBound = BoundUnspecified | StaticBoundFact(IntInterval)`. No PlatformDependent variant exists. `BoundDeclaration` is live in `src/v3/std/substrate.dag` (`StaticBound(Interval) | PlatformDependent`) but NOT wired into `TargetIntegerInhabitanceBound`. Carrier refactor is **required** (not optional) to unblock isize/usize rows. +2. **Bound-carrier wiring on actual row surface (CORRECTED — Option (ii) feasible)**: the live row surface used by `src/v3/spec/rust.dag` is `TargetIntegerTypeInhabitance` (with bound-field type `TargetIntegerInhabitanceBound`) imported from `v3.std.emit_model`. **Verified at origin/main HEAD post-valiant-ibex-312 ratification-state-grep at gunbc#1761 #issuecomment-4393074602**: `TargetIntegerInhabitanceBound = BoundUnspecified | StaticBoundFact(IntInterval) | PlatformDependentFact` — **3 variants including PlatformDependentFact** (mirrors `BoundDeclaration::PlatformDependent`; main moved since the earlier codex BLOCKING reading at PR #1910 sha 4229cd09 which was against pre-PlatformDependentFact state). **Option (ii) IS feasible at HEAD** — isize/usize rows populate via existing `PlatformDependentFact` variant directly; no carrier refactor needed. Earlier "carrier refactor required" framing was Mgr-tier ratification-state-grep miss against stale codex sha. 3. **`spec/rust.dag` PlatformDependentFact row population**: `src/v3/spec/rust.dag` has no Rust PlatformDependentFact row entries for isize / usize. Co-located with (2) — same brief / PR per "necessary structural fix" exception. ### Why bundled -All three gaps address the same axis: "support wider/platform-dependent integer primitives." (2) consumes (1)'s widened interval representation; (3) consumes (2)'s structural BoundDeclaration field. Splitting across separate PRs would create cross-PR dependency chains and partial-substrate intermediate states. Bundled-scope discipline allows same-PR per "necessary structural fix" exception. +All three gaps address the same axis: "support wider/platform-dependent integer primitives." (1) provides BigInt-widened ExactInterval which (3) u128 row consumes via `StaticBoundFact(IntInterval)`. (2) is no-op at HEAD per Option (ii) (existing `PlatformDependentFact` variant on `TargetIntegerInhabitanceBound` already serves the platform-dependent semantics). Splitting across separate PRs would create cross-PR dependency chains and partial-substrate intermediate states. Bundled-scope discipline allows same-PR per "necessary structural fix" exception. ## Scope @@ -53,18 +53,23 @@ Update consumers of `ExactInterval` at HEAD (worker greps for usage sites; refac Refactor target: `v3.std.emit_model` carrier `TargetIntegerInhabitanceBound` (the actual bound-field type used by `TargetIntegerTypeInhabitance` rows in `src/v3/spec/rust.dag` lines 169/180/191/199/207). -Per codex BLOCKING at PR #1910 sha 98507c432 inline finding (verified at HEAD): live shape is `TargetIntegerInhabitanceBound = BoundUnspecified | StaticBoundFact(IntInterval)`. No PlatformDependent variant exists. Earlier Option (ii) (populate via existing variants) is therefore INFEASIBLE — only carrier refactor unblocks isize/usize rows. +**Live shape at origin/main HEAD** (per valiant-ibex-312 ratification-state-grep at gunbc#1761 #issuecomment-4393074602): -**Required path — wire BoundDeclaration into TargetIntegerInhabitanceBound**: +``` +type TargetIntegerInhabitanceBound + = BoundUnspecified + | StaticBoundFact(IntInterval) + | PlatformDependentFact +``` -Refactor `TargetIntegerInhabitanceBound` in `src/v3/std/emit_model.dag` to gain PlatformDependent semantics. Two structural shapes worker DFS-decides: +3 variants including `PlatformDependentFact` (mirrors `BoundDeclaration::PlatformDependent`). -- **(i.a) — embed BoundDeclaration**: replace `TargetIntegerInhabitanceBound` body with `BoundDeclaration` (or `BoundDeclaration` newtype wrapper). Single source of truth for bound facts; existing variants `BoundUnspecified` / `StaticBoundFact(IntInterval)` map to `BoundDeclaration` variants (BoundUnspecified ≈ Phase 1 placeholder; StaticBoundFact ≈ StaticBound). Migration: 5 existing rows + new isize/usize/u128 rows populate via `BoundDeclaration` variants. -- **(i.b) — extend variant set**: keep TargetIntegerInhabitanceBound name but add PlatformDependent variant (3 variants: BoundUnspecified | StaticBoundFact(IntInterval) | PlatformDependent). Less integration with substrate.dag's BoundDeclaration carrier; worker confirms whether (i.a) is structurally preferred (single-authority) at dispatch. +**Path — Option (ii) populate via existing variants** (no carrier refactor needed): +- isize / usize rows populate `bound: PlatformDependentFact` directly +- u128 row populates `bound: StaticBoundFact(IntInterval)` consuming Deliverable 1's BigInt-widened ExactInterval +- Existing 5 rows untouched (no migration; carrier already serves the use case) -**Mgr recommendation: (i.a) embed BoundDeclaration** — single-authority discipline + consumes existing substrate (P2 boundary discipline). Worker confirms via DFS at dispatch. - -Existing 5 rows (rust_integer_inhabit_u32 / i32 / int64 / i128 / i32_at_program_bound) migrate to the chosen shape; bootstrap snapshot + parse corpus manifest verification on existing-row semantic equivalence is non-negotiable. +**Single-authority concern (note, not blocker)**: `TargetIntegerInhabitanceBound::PlatformDependentFact` and `BoundDeclaration::PlatformDependent` are parallel-named variants on different carriers. The doc-comment at emit_model.dag explicitly mirrors `BoundDeclaration::PlatformDependent`; explicit cross-carrier mirror is the existing convention. If future Substrate Mgr work wants to consolidate to single BoundDeclaration authority (per P2 boundary discipline), that's a separate substrate-fact-introduction — not required for this slice. Worker proceeds with Option (ii) verbatim. Both options consume Deliverable 1's widened `Interval` representation for the u128 row. @@ -85,7 +90,8 @@ Add `u128` row to `dsl/extdeps/languages/rust/primitives.dag` consuming Delivera ### Deliverable 5 — Practice 4 checkpoint Per `docs/modeling-discipline.md#4-coproduct-dissolution`: -- `BoundDeclaration` is existing 🟢 GREEN substrate (no new variants added; Deliverable 2/3 just consume existing variants on RustPrimitive rows) +- `TargetIntegerInhabitanceBound` is existing 🟢 GREEN substrate (3 variants including PlatformDependentFact; no new variants added; Deliverable 2 is no-op; Deliverable 3 just populates rows using existing variants) +- `BoundDeclaration` (substrate.dag) is parallel existing 🟢 GREEN substrate (mirror-by-convention with `TargetIntegerInhabitanceBound::PlatformDependentFact`; future single-authority consolidation is separate substrate-fact-introduction) - `ExactInterval` widening (α BigInt or β typed-variants) — α is type-substitution (no Practice 4 implication); β adds variants and needs 🟢/🟡/🔴 classification + checkpoint comment - Worker authors checkpoint comment if β chosen; α path doesn't require new checkpoint @@ -99,9 +105,9 @@ Phase ordering (PR-internal): 1. DFS-catalog `ExactInterval` consumers + `RustPrimitive` row shape + `rust.dag` row population convention at HEAD 2. Choose α vs β for ExactInterval widening; author Practice 4 checkpoint if β 3. Author Deliverable 1 (ExactInterval widening) + verify existing 9 rows hold via bootstrap snapshot -4. Author Deliverable 2 (RustPrimitive bound field refactor) + migrate existing 9 rows; bootstrap snapshot + manifest verification -5. Author Deliverable 3 (rust.dag PlatformDependent rows for isize/usize) -6. Author Deliverable 4 (u128 row) + ratchet update 9 → 12 rows +4. Author Deliverable 2 (no-op at HEAD — `TargetIntegerInhabitanceBound` already has `PlatformDependentFact` variant per origin/main verification at gunbc#1761 #issuecomment-4393074602; existing 5 rows untouched) +5. Author Deliverable 3 (`spec/rust.dag` `TargetIntegerTypeInhabitance` rows for isize/usize via existing `PlatformDependentFact` variant) +6. Author Deliverable 4 (u128 row via `StaticBoundFact(IntInterval)` consuming Phase 3's BigInt-widened ExactInterval) + ratchet update 9 → 12 rows in `dsl/extdeps/languages/rust/primitives.dag` IntegerPrimitive surface (worker DFS confirms whether primitives.dag IntegerPrimitive needs parallel additions or feeds into TargetIntegerTypeInhabitance row population) 7. §1.8 ledger row receipt (Deliverable 6) 8. Bootstrap snapshot regen + parse corpus manifest refresh 9. Cross-program handoff receipt to Grounding Mgr (#1745) for G2 Phase 2 full-coverage dispatch @@ -109,9 +115,10 @@ Phase ordering (PR-internal): ## Acceptance - `IntervalInt::ExactInterval` widened (α BigInt-based recommended; β typed-variants if α structurally infeasible) with existing 9 i8-i64+u8-u64 rows holding semantic equivalence -- `RustPrimitive` rows carry structural `BoundDeclaration` field; existing 9 rows migrated from static-string to `StaticBound(Interval)` form -- `dsl/extdeps/languages/rust/primitives.dag` has 12 rows (added u128, isize, usize); ratchet at `int_literal_ranges.rs` updated -- `src/v3/spec/rust.dag` has PlatformDependent rows for isize / usize +- `TargetIntegerInhabitanceBound` carrier untouched (3-variant shape including PlatformDependentFact already serves; Option (ii) per Mgr ratification at gunbc#1761 #issuecomment-4393159178) +- `src/v3/spec/rust.dag` gains `TargetIntegerTypeInhabitance` rows for isize / usize via `bound: PlatformDependentFact` +- u128 row added via `bound: StaticBoundFact(IntInterval)` consuming Phase A BigInt-widened ExactInterval +- `dsl/extdeps/languages/rust/primitives.dag` updates per worker DFS at HEAD — if IntegerPrimitive surface needs parallel u128/isize/usize additions, ratchet updates 9 → 12 rows; if IntegerPrimitive feeds into TargetIntegerTypeInhabitance row population, no parallel addition needed - Practice 4 checkpoint comment if β chosen for ExactInterval; α path no checkpoint required - §1.8 row `rust_primitive_full_coverage` advances DECLARED → CONSUMER_LANDED upon merge (cluster: Mgr-discretion T-Numeric-Construction-adjacent OR new T-Interval-Representation) - Cross-program handoff receipt to Grounding Mgr (#1745) in PR body — G2 Phase 2 full-coverage dispatch unblocked @@ -126,8 +133,8 @@ Phase ordering (PR-internal): ## STOP-AND-ESCALATE - **α BigInt dependency adds workspace surface beyond minor**: surface to Substrate Mgr; β typed-variants may be the right shape if dependency cost is high -- **`BoundDeclaration` variant set insufficient** (e.g., isize/usize needs a third variant beyond `StaticBound`/`PlatformDependent`): STOP — substrate-fact-introduction cascade; surface to Substrate Mgr with proposed third variant + named consumer demand + DFS-of-concept-DAG receipt -- **Bootstrap snapshot drift** during ExactInterval widening or RustPrimitive bound field refactor: root-cause; do NOT bridge with placeholder; semantic equivalence on existing 9 rows is non-negotiable +- **`TargetIntegerInhabitanceBound` variant set insufficient at HEAD** (worker DFS surfaces 4th class beyond BoundUnspecified/StaticBoundFact/PlatformDependentFact): STOP — substrate-fact-introduction cascade; surface to Substrate Mgr +- **Bootstrap snapshot drift** during ExactInterval widening or row population: root-cause; do NOT bridge with placeholder; semantic equivalence on existing 9 rows + 5 TargetIntegerTypeInhabitance rows is non-negotiable - **u128 / isize / usize add surfaces additional substrate gaps** (e.g., parser doesn't recognize `u128` literal suffix in `.dag` source): STOP — surface scope expansion; bundled-scope check (necessary-structural-fix vs parallel-infrastructure) - **Bundled-scope drift on consumer side**: do NOT bundle Grounding G2 Phase 2 lowering rules / emit verification into this PR. Per Director bundled-scope ratification — parallel infrastructure DISALLOWED. Grounding G2 Phase 2 PR is downstream consumer @@ -142,7 +149,7 @@ Phase ordering (PR-internal): 2. **Existing brief?** No prior brief on this axis at HEAD. T-E-P-Producer-Broadening (`r3-t-e-p-producer-broadening-worker.md`) and S7 PR-F (`r3-substrate-s7-pr-f-bounddeclaration-consumer-worker.md`) are adjacent precedents — neither covers this scope 3. **Design-doc match?** Director Path A RATIFIED scope at gunbc#1739 #issuecomment-4392731264 names all three gaps + bundling decision verbatim 4. **Citations live?** Worker re-verifies at dispatch; substrate-state-grep confirms Path A finding shape unchanged -5. **Carrier dissolves the bridge?** Yes — widened `ExactInterval` + structural `BoundDeclaration` field + populated isize/usize rows together dissolve the "u128 / isize / usize cannot be represented faithfully in current substrate" bridge. Ad-hoc string encoding (the bridge anti-pattern Director rejected) avoided structurally +5. **Carrier dissolves the bridge?** Yes — widened `ExactInterval` (Phase A) + populated isize/usize rows via existing `PlatformDependentFact` variant + u128 row via `StaticBoundFact(IntInterval)` together dissolve the "u128 / isize / usize cannot be represented faithfully in current substrate" bridge. Ad-hoc string encoding (the bridge anti-pattern Director rejected) avoided structurally; carrier shape unchanged (Option (ii)) ## Provenance