diff --git a/docs/briefs/r3-substrate-emission-provenance-lens-worker.md b/docs/briefs/r3-substrate-emission-provenance-lens-worker.md index af7b01d97a4..97331e900ed 100644 --- a/docs/briefs/r3-substrate-emission-provenance-lens-worker.md +++ b/docs/briefs/r3-substrate-emission-provenance-lens-worker.md @@ -1,231 +1,256 @@ --- -status: PROPOSAL (worker brief; PM-authored under tactical authority per Director ratification 2026-05-06; **NOT dispatch-ready** pending Substrate Mgr canvas on Lens read-shape question raised by codex BLOCKING 2026-05-06; dispatch-readiness assessed by Substrate Mgr) +status: dispatchable per Director Reading C RATIFICATION at gunbc#1739 #issuecomment-4392797954 (2026-05-07). T-Rule-Enumeration retired (substrate gap closed structurally via existing field-path enumeration on `*SyntaxBinding`/`*OpsBinding` structs). Worker pin: smart-ram-167 (Mgr discretion per Director ratification; smart-ram has fresh context from substrate-state-grep that surfaced Reading C; valiant-ibex-312 already dispatched on Rust-primitive-full-coverage / T-Interval-Representation). authority parent: R3 Substrate Manager (#1739) -ratification: Director ratified scope at gunbc#828 #issuecomment-4392256151 (zesty-bear-812 — "Lens as another Lens instance per feedback_lenses_not_passes; Substrate authors instance carrier; Verification asserts gate"); Brian directive 2026-05-06 chat ("R3 has idle workers under several managers, so we should put them to work asap") -roadmap row: **TBD — gate authority pending** per codex BLOCKING 2026-05-06; no #89 (already taken by `section_ref_substrate_landed` under T-Lens-Application-Surface). Candidate retargets per Substrate Mgr disposition: (a) new gate added to T-CostLens-Composition lane scope (analogous to existing #37-#40 cluster); (b) new gate added to T-Lens-Application-Surface lane scope; (c) deferred until per-Behavior framing ratified +ratification: Q1 (a) per-Behavior Lens-compatible RATIFIED at gunbc#1739 #issuecomment-4392562911 (zesty-bear-812, 2026-05-06). Q1 (b) per-line instrumentation REJECTED. Q1 (d) parallel substrates REJECTED. Q3: gate `emission_provenance_lens_landed` under T-CostLens-Composition cluster. +roadmap row: §1.8 ledger row TBD slot — gate `emission_provenance_lens_landed` under T-CostLens-Composition cluster per Director Q3 ratification authority docs: - - src/v3/std/lens.dag — `Lens` substrate carrier (Director-locked 6-field shape; **`read: fn(Dag, Behavior) -> Witness`** — per-Behavior read; codex BLOCKING 2026-05-06 surfaced category mismatch with per-emitted-line goal) - - src/v3/compiler/src/diagnostics_generated.rs:5 — `SourceSpan { file, byte_start, byte_end }` shape - - src/v3/compiler/src/dag.rs:47-48 — "SourceSpan lives on every Behavior and every Declaration structurally" - - docs/design-lens-framework.md — lens framework parent doc - - docs/r3-design-schedule-2026-05-06.md — pre-authored brief queue discipline (Brian directive 2026-05-06) + - gunbc#1739 #issuecomment-4392562911 (Director Q1+Q2+Q3 RATIFICATION) + - docs/briefs/r3-substrate-emission-provenance-shape-canvas.md (Substrate Mgr canvas; parent) + - docs/briefs/r3-substrate-t-rule-enumeration-worker.md (PREREQUISITE — must land first) + - src/v3/std/lens.dag (Lens Director-locked 6-field carrier) + - PR #1879 (emission-intuition slide — visualization consumer) gates: - - TBD per Substrate Mgr canvas — not landed in §1.8 ledger + - `emission_provenance_lens_landed` (proposed §1.8 row; slot pending T-CostLens-Composition cluster) +worker pin: smart-ram-167 (Mgr discretion per Director Reading C ratification; fresh context on field-path enumeration from substrate-state-grep) --- -## STATUS — PROPOSAL pending Substrate Mgr canvas (codex BLOCKING 2026-05-06) +# R3 Substrate — `Lens>` worker brief (per (a) per-Behavior framing) -Codex BLOCKING review at sha `3c96212d` (PR #1902) surfaced 3 valid findings: +## Context -1. **Optional+invariant origin → typed-sum origin** (applied below; structural fix per `feedback_state_space_vs_behavioral_invariants`) -2. **Lens reads (Dag, Behavior) → Witness; emission provenance is per-line, not per-Behavior** (category mismatch — substantive Substrate Mgr canvas territory; brief stays PROPOSAL until ratified) -3. **§1.8 #89 already taken by `section_ref_substrate_landed`** (gate authority retargeting required; PM grep-error) +Director Q1 (a) RATIFIED at gunbc#1739 #issuecomment-4392562911: +per-Behavior Lens-compatible framing. Reasoning per Director: -**The load-bearing finding is #2**: this brief framed emission-provenance as `Lens`, but the Lens read shape is per-Behavior, not per-emitted-line. Two reframings possible: +> `feedback_lenses_not_passes`: analyses are lenses over physics; zero +> heuristics; heuristic = missing physics. Emission-provenance IS +> analysis (which lines came from where); the right substrate shape +> is a lens over physics, not runtime instrumentation. -- **(a) Per-Behavior provenance** (Lens-compatible): "for Behavior B, the emitted lines are [line-range / fold-rule] tuples." Lens reads (Dag, Behavior) → Witness>. Narrower scope but structurally faithful. Doesn't directly give the slide visualization Brian wanted. -- **(b) Per-emitted-line instrumentation** (NOT a lens): emission-fold instrumentation that runs DURING emission and records per-line origin. Different substrate shape entirely; matches Brian's slide visualization need; not a `Lens` instance. -- **(c) Withdraw brief**: pre-canvas the question via Substrate Mgr canvas first; re-author brief once shape ratified. +> `feedback_compositional_not_templating`: don't materialize parallel +> structures when one composes correctly. (a) composes; (b) is +> instrumentation that drops compositional structure. -PM read: recommend **(c)** — withdraw + canvas first. Brief was authored before this category mismatch was surfaced; substantive reshape needs Substrate Mgr substrate-state-grep + Director ratification on the right shape, not PM-tier pre-authoring. +(b) per-line instrumentation REJECTED; (d) parallel-substrates +REJECTED — Brian's slide visualization is served by (a) projection +(per-Behavior list flattens to per-line view at the visualization +layer), not parallel substrate. -# R3 Substrate — `Lens` worker brief +This brief revises the earlier PM-authored proposal (PR #1902 merged +at 54419badf, but the brief shape needed Substrate Mgr canvas + Director +re-ratification per the codex BLOCKING category-mismatch finding). -## Context +## No precondition gate (Reading C ratification) -PR #1879 (emission-intuition slide) surfaced that the structural fold's -emitted output is currently uncolored — there is no metadata stream -correlating each line of generated target-language code back to either -its `.dag` source span (when directly mirrored from a Behavior / -Declaration) OR the LangSpec fold-rule that produced it (when -auto-emitted, e.g., `#[derive(...)]`, `impl X { is_left }` predicates, -constructor accessors). +Earlier draft gated dispatch on T-Rule-Enumeration landing. Per +Director Reading C RATIFICATION at gunbc#1739 #issuecomment-4392797954: +T-Rule-Enumeration is RETIRED — substrate gap was a phantom; rule +enumeration is structurally already provided by the `*SyntaxBinding` +/ `*OpsBinding` field-path set in `src/v3/compiler/src/emit/rust_target.rs` +(~37 distinct field paths catalogued by smart-ram-167's substrate-state-grep +at gunbc#1759 #issuecomment-4392696623). -Forward-direction span tracking already exists structurally — every -`Behavior` and `Declaration` carries a `SourceSpan { file, byte_start, -byte_end }` per `diagnostics_generated.rs:5`, and "Spans flow forward -through lowering; no side tables, no reconstruction" per `dag.rs:47-48`. -Diagnostics consume these for compile-error reporting. +`EmissionRule` carrier IS the field-path string itself (e.g., +`"indexes.syntax.statements.let_binding"`). No new substrate +authoring needed; `EmissionRule = String` of field-path per Director +Q3 ratification: -The inverse direction — "this emitted line came from THAT `.dag` -declaration / OR from THIS LangSpec rule" — is **implicit in the fold** -(each emitted item is produced by a specific Conj/Disj structure + -LangSpec rule mapping) but **not currently exposed as a metadata -stream**. +> `feedback_reason_not_label`: field-path IS the stable reason; +> nominal alias is the volatile label. Substrate carries the structural +> truth; aliases are derived display surface. -Per `feedback_lenses_not_passes` ("analyses are lenses over physics; -zero heuristics; heuristic = missing physics"): emission-provenance -fits naturally as **`Lens` over the structural -fold** — analogous to `Lens` over algebra+realization -cost (T-CostLens-Composition pattern). Same `Lens` shape; new `C` -type. No new substrate carrier shape required — only a new instance. +Brief dispatches immediately. -## Slice +## Scope -### Phase 1 — `EmissionProvenance` `C`-type declaration +### Deliverable 1 — `EmissionProvenance` carrier (record form) -Author `EmissionProvenance` carrier in `src/v3/std/` (alongside other -`Lens` instance C-types). Shape: +Author carriers in `src/v3/std/`. Per codex Finding 1 reshape (typed-sum +origin, NOT optional-pair-with-runtime-invariant — applied in PR #1902 +at 0110f739d before supersession): ```dag -// Typed origin sum — codex BLOCKING 2026-05-06 finding 1: provenance origin -// must be a non-empty typed authority, NOT optional coordinates with a -// runtime-asserted "at-least-one" invariant. Per -// feedback_state_space_vs_behavioral_invariants: type enforcement > API enforcement. -type EmissionOrigin = - SubstrateDeclMirror { span: SourceSpan } // line directly mirrors a .dag Behavior / Declaration - | FoldRuleAutoEmit { rule_name: String } // LangSpec auto-emitted (e.g., "rust.derive_for_disj") - type EmissionProvenance { - emitted_line: Int // line number in emitted target output - origin: EmissionOrigin // REQUIRED, typed sum — fail-closed by construction + emitted_line: Int // line number in emitted target output + rule: EmissionRule // MANDATORY — every emitted line is produced by some rule + // (even trivial mirror-rules); type system enforces + source_span: Option // OPTIONAL — populated when the rule's input traces to a + // `.dag` source declaration; absent for purely structural + // emissions (e.g., headers, fixed scaffolding) } ``` -**Structural fail-closed (per codex BLOCKING finding 1 + `feedback_state_space_vs_behavioral_invariants`)**: the `Disj` carrier `EmissionOrigin` makes "at least one origin class is present" structurally true by construction; no runtime invariant required. Eliminates the structural-recovery pattern from the prior optional+invariant shape. - -### Phase 2 — `Lens` instance authoring - -Author the lens instance per existing `Lens` 6-field shape -(`src/v3/std/lens.dag` Director-locked): -- `read: fn(Dag, Behavior) -> Witness` -- `validate: fn(...) -> ...` -- ... (remaining 4 fields per existing T-CostLens-Composition precedent; - worker greps the `Lens` instance for shape parity) - -Per `Witness` semantics (NOT `C`): missing per-Behavior provenance -surfaces as `Violates` rather than silent None — matches the C-8 -discipline above structurally. - -### Phase 3 — Cementing test (acceptance criterion) +**Reshape rationale** (per codex BLOCKING at PR #1910 sha 2ed1046e Finding #1): earlier typed-sum form `EmissionOrigin = SubstrateDeclMirror(SourceSpan) | FoldRuleAutoEmit(EmissionRule)` conflated two orthogonal axes. A single emitted line genuinely can have BOTH attributions — e.g., `#[derive(Debug)]` emitted on a Foo enum has rule=`derive_for_disj` AND source-span attribution to the Foo declaration in the `.dag` source. The two facts are not mutually exclusive; modeling them as sum variants forced false either-or framing. Record (product) form with mandatory rule + optional span is faithful to actual emission semantics and structurally fail-closed (rule presence enforced by type system; never both-absent). + +`EmissionRule = String` (field-path; Director Q3 ratification at +gunbc#1739 #issuecomment-4392797954). Worker references the existing +`*SyntaxBinding` / `*OpsBinding` field-path set as the de-facto +enumeration; no new rule-name carrier authored. Field-path-string +preserves structural navigability (per `feedback_reason_not_label`); +nominal aliases live at display layer if desired (visualization-side +projection, not substrate-side). + +**Practice 4 classification**: N/A — `EmissionProvenance` is a record +(product), not a sum (coproduct). Practice 4 coproduct-dissolution +rubric (🟢 / 🟡 / 🔴) applies to N≥2-variant sum types; record types +are structurally classified by their field set, not coproduct status. + +The earlier draft used a typed-sum `EmissionOrigin` shape with GREEN +classification + terminal receipt; codex BLOCKING at PR #1910 sha +2ed1046e Finding #1 surfaced that the sum framing was mis-modeled +(the two facts can co-inhabit; sum forces false either-or). Record +form with mandatory `rule: EmissionRule` + optional `source_span: +Option` is the faithful shape. No Practice 4 ledger +entry needed; structural fail-closed is enforced by `rule` field's +required-presence in the record type. + +No §1.8 sibling-row needed (record-type, not coproduct; Practice 4 +ledger-entry-if-GREEN rubric doesn't apply). Parent gate +`emission_provenance_lens_landed` is the sole row. + +### Deliverable 2 — `Lens>` instance + +Author lens instance per Director-locked 6-field shape: + +- `name: "EmissionProvenance"` (or canonical project-naming convention) +- `read: fn(Dag, Behavior) -> Witness>` — + per-Behavior fold computing the provenance list. For each emitted + line attributable to this Behavior, populate: + - `rule: EmissionRule` (= field-path String) — the field-path of the + rule that produced this line (always present; trivial-mirror rules + count). Captured from the `render_named_template(...)` call site's + field-path argument at emission time. + - `source_span: Option` — populated when the rule's + input traces to a `.dag` source declaration; absent for purely + structural emissions (e.g., headers, fixed scaffolding rules + that don't have a per-line source-decl input) +- `sequential: Monoid>` — list-concat monoid + (`empty: []`, `concat: [...] ++ [...]`) +- `branch: (List, List) -> List` — concat over both arms (static + emission tracking captures both branches; runtime exclusivity is + orthogonal to static-emission analysis) +- `iterate: (List, LoopBound) -> List` — identity (body emitted once; + bound is data, not source). Worker confirms at dispatch via + substrate-state-grep on actual emission semantics; STOP if assumption + breaks +- `validate: fn(Dag, List) -> OptionalDiagnostic` — + record form makes "rule absent" structurally impossible (type system + enforces). Aggregate validation: surface diagnostic if `rule` + field-path doesn't correspond to a real field on + `*SyntaxBinding`/`*OpsBinding` structs (worker DFS-catalogs the + field set at dispatch; round-trip verifies the field-path resolves); + optional-`source_span` absence is structurally legal, NOT a diagnostic + +Per `feedback_compositional_not_templating`: per-Behavior fold composes +to per-line view at the visualization layer (flatten the per-Behavior +List); no parallel substrate needed for slide. + +### Deliverable 3 — Cementing test Author cementing test that: -1. Walks the structural fold over a representative `.dag` source -2. Emits target-language output (Rust acceptance target — extends - trivially to other targets per LangSpec) -3. Runs `Lens` over the same source + emission -4. **Verifies inverse mapping closes**: every emitted line has either - a non-empty `source_span` (and that span resolves to a real - `.dag` Behavior / Declaration in the input source) OR a non-empty - `fold_rule` (and that rule name is in the LangSpec's enumerated - rule set) -5. **No line uncovered** (fail-closed acceptance — both-absent is - test failure, not warning) - -Cementing test minimum: representative source with at least one of -each origin class: -- Substrate-decl mirror (e.g., `pub enum Foo { ... }` from a `.dag` - `type Foo = ... | ...` declaration → `source_span` populated) -- LangSpec auto-emit (e.g., `#[derive(...)]` from - `rust.derive_for_disj` rule → `fold_rule` populated, no span) -- LangSpec auto-emit predicate (e.g., `pub fn is_left(&self) -> bool` - from `rust.predicate_per_variant` rule → `fold_rule` populated) -- LEFT-sourced logic (e.g., `pub fn map<...>` from a `.dag` - `fn map(...) = match ...` → `source_span` populated) - -## Scope bars - -**`feedback_pre_authored_brief_queue` discipline applies**: this brief -is pre-authored before dispatch; substrate-state grep happens at -**both** brief-authoring time (PM-side, this commit) AND dispatch time -(worker-side, per substrate-grep-discipline). Worker adjusts brief -content lightly if substrate state has shifted between PR-merge and -dispatch. - -**`feedback_no_textual_enforcement_bridges` discipline**: the -provenance metadata stream IS structural (typed `EmissionProvenance` -records), NOT a side-channel comment annotation. If worker finds the -fold rule names aren't enumerable at the LangSpec layer (i.e., they're -implicit in the Rust LangSpec emission code rather than data-declared -rule identifiers), STOP and surface — that's a substrate gap that -needs separate disposition (likely: name the rules as enumerable -data first, then this lens instance lands cleanly). - -**`feedback_construction_over_ratchets` discipline**: this brief -adds a new `C`-type + `Lens` instance. Both are existing-substrate -extensions, NOT substrate-fact-introduction (per `INVARIANTS.md` P1). -If implementation surfaces a P1-violating addition (e.g., new -`OptionalSourceSpan` type because none exists at HEAD), worker -STOPs and surfaces — that's substrate-fact-introduction requiring -P1 procedure. - -## STOP triggers (fail-closed; do not bypass) - -1. **Missing fold-rule names — likely prerequisite, not mid-implementation STOP** (per claude review observation 2026-05-06; PM grep-verified): grep at PM-authoring-time for `RuleName` / `FoldRule` / `fn emit_derive` in `src/v3/compiler/src/` returns **0 hits**. Fold-rule names are NOT enumerable in LangSpec emission code today; they're implicit in the Rust LangSpec emission code rather than data-declared rule identifiers. **This is most likely a hard prerequisite to resolve BEFORE dispatch, not a mid-implementation STOP**. **Resolution path**: Substrate Mgr disposes — either (a) author rule-name enumeration substrate first as separate brief (lens instance lands downstream once rules are enumerable), OR (b) confirm that grep was incomplete and rule names ARE enumerable somewhere PM didn't check. If neither: brief should be re-scoped to land partial-provenance (only source-span side; fold-rule side deferred to post-rule-enumeration). PM-side recommendation: Substrate Mgr resolves this before worker dispatch rather than after. -2. **`Lens` shape gaps** — if instance authoring surfaces missing - substrate types from `Lens` (e.g., needing T-LAS-only types - that aren't yet landed), STOP and surface. Director's ratification - notes T-LAS gate #88 is NOT a hard prerequisite for instance - authoring, but if implementation reveals otherwise, surface and - re-ratify the dispatch trigger. -3. **`feedback_fail_closed_discipline` violation surface** — if - implementation reveals emitted lines that genuinely have NEITHER - source_span NOR fold_rule (i.e., a third origin class not - accounted for in the brief), STOP and surface. Either the brief's - 2-class enumeration is incomplete, OR the LangSpec emission has - a substrate gap. -4. **Substrate-state-grep mismatch** — if worker greps `src/v3/std/` - and finds the existing lens instances diverged from the - `Lens` precedent referenced here, surface for - Substrate Mgr triage before authoring against drifted shape. - -## Acceptance criteria - -1. **`EmissionProvenance` carrier landed** in `src/v3/std/` per - Phase 1 shape (or Mgr-adjusted equivalent if substrate-grep - surfaces drift). -2. **`Lens` instance landed** per Phase 2 (full - 6-field `Lens` shape; worker greps T-CostLens-Composition - precedent for parity). -3. **Cementing test passes** per Phase 3 (every emitted line has - either populated `source_span` or `fold_rule`; both-absent fails - closed). -4. **§1.8 ledger gate `emission_provenance_lens_landed` (#89)** - updates from DECLARED → CONSUMER_LANDED. -5. **No bridge introductions** — implementation does not introduce - any side-channel comment annotation, regex-based rule extraction, - or string-matching against emission code. All metadata flows - through typed `EmissionProvenance` records via `Lens` shape. - -## Cross-lane references - -- **T-Lens-Application-Surface (T-LAS, §1.8 #88 - `lens_application_carrier_landed`)**: `Lens` is - an instance that becomes consumable via `apply_lens(...)` once T-LAS - lands. R3 scope = instance landing only; downstream - `apply_lens(emission_provenance, dag, Introspect)` consumer is - T-LAS-downstream and out of scope here. -- **Grounding (post-R2 continuation)**: emission-side annotation - consumer optional; R3 scope = lens instance landing only. If - Grounding wants to consume for emit-side annotation (e.g., to - surface "this Rust line came from this `.dag` location" in - diagnostic context), that's a Grounding-tier consumer dispatch - separate from this brief. -- **T-CostLens-Composition (§1.8 #37-#40)**: shape precedent — - `Lens` is the existing instance pattern; worker greps - for shape parity at brief time. -- **PR #1879 (emission-intuition slide)**: surfaced this gap; the - visualization claim ("you didn't write this; the fold did") - benefits from this lens once landed. - -## Worker pin candidate - -Substrate Mgr discretion. PM observation: pre-authored-queue tier-2 -candidates per Substrate inventory at gunbc#846 #issuecomment-4390098574 -include freed-pool workers post-S11/S12 landings. **smart-ram-167** OR -**valiant-ibex-312** are candidate pins per Substrate Mgr's worker-pool -state at dispatch time. Final pin is Mgr's call. +1. Walks structural fold over a representative `.dag` source (likely + 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 +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 + field-path → no information loss); ≥1 entry has `source_span: + Some(...)` (substrate-decl-traceable); ≥1 entry has `source_span: + None` (structural-only emission); span-Some entries' SourceSpan + resolves to a real `.dag` Behavior/Declaration in the input source + +### Deliverable 4 — §1.8 ledger receipt + +Add `emission_provenance_lens_landed` to §1.8 ledger under +T-CostLens-Composition cluster (Director Q3). Advance DECLARED → +PRODUCER_LANDED on merge (cementing test verifies producer shape; no +Grounding-side visualization-consumer wiring in this PR). + +## Slice — single PR + +Phase ordering (PR-internal): +1. DFS-catalog `*SyntaxBinding`/`*OpsBinding` field set in `src/v3/compiler/src/emit/rust_target.rs` (Reading C confirmed ~37 field paths; worker re-greps at HEAD for actual count) +2. Author `EmissionProvenance` record carrier (Deliverable 1) +3. Author `Lens>` instance (Deliverable 2) +4. Author cementing test (Deliverable 3) +5. Verify all standard ratchets green +6. §1.8 ledger row receipt (Deliverable 4) + +## Acceptance + +- `EmissionProvenance` record carrier landed in `src/v3/std/` with + mandatory `rule: EmissionRule` field + optional + `source_span: Option` field. Record form per codex + BLOCKING reshape (PR #1910 sha 2ed1046e Finding #1) — replaces + earlier typed-sum framing; Practice 4 N/A (record, not coproduct) +- `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) +- §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 + bundled-scope discipline at gunbc#1739 #issuecomment-4392225548) +- `cargo test --workspace --exclude v2-compiler-tests` green +- `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 + +## 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 +- **`iterate` identity assumption breaks** (body emitted multiple times + per LoopBound, NOT once): STOP — surface to Substrate Mgr; lens + iterate field shape may need rework +- **Cementing test reveals provenance gap** — emitted line that the + per-Behavior fold cannot attribute to any rule: STOP. Record form + requires `rule` populated; rule absence indicates emission code path + not covered by T-Rule-Enumeration carrier (substrate-fact-introduction + cascade). Do NOT add a sentinel rule like "Unknown" — surface to + Substrate Mgr +- **Bundled-scope drift**: do NOT bundle T-Rule-Enumeration edits or + Grounding-side visualization-consumer wiring into this PR + +## Authority audit receipt + +1. **Substrate exists?** At brief-author time: + - `Lens` carrier landed (`src/v3/std/lens.dag`, 🟢 TERMINAL) ✓ + - `EmissionRule` carrier — gates on T-Rule-Enumeration landing + - `EmissionProvenance` record carrier — this brief is producer + - Lens instance — this brief is producer +2. **Existing brief?** PM-authored proposal at PR #1902 (merged at + 54419badf) is the prior artifact; this brief revises per Substrate + Mgr canvas + Director Q1 (a) RATIFICATION +3. **Design-doc match?** Director Q1 (a) RATIFIED + canvas Q1 disposition + + Lens Director-locked shape. T-CostLens-Composition is shape + precedent +4. **Citations live?** Worker re-verifies at dispatch +5. **Carrier dissolves the bridge?** Yes — record `EmissionProvenance` + with mandatory `rule` + optional `source_span` dissolves the + "what produced this emitted line?" bridge structurally (rule field + always present; no None possible; type system enforces). Per-Behavior + `Lens>` composes to per-line view at + visualization layer per `feedback_compositional_not_templating` ## Provenance -PM-authored under Director-ratified tactical authority 2026-05-06 -(role boundary item e: docs/audit authorship). Director ratification -at gunbc#828 #issuecomment-4392256151. Brian directive driving -priority: gunbc#846 chat 2026-05-06 ("R3 has idle workers under -several managers, so we should put them to work asap"). - -Substrate Mgr disposes dispatch readiness at brief-PR-merge time per -pre-authored-brief-queue discipline (`feedback_pre_authored_brief_queue`). -Adjustment-vs-from-scratch: Mgr adjusts brief content lightly at -dispatch if substrate state has shifted; doesn't re-author from -scratch. +Revised 2026-05-06 by Substrate Mgr per Director Q1 (a) RATIFICATION +at gunbc#1739 #issuecomment-4392562911. Brief revises PM-authored +proposal at PR #1902 (merged at 54419badf; brief shape needed canvas ++ re-ratification per codex BLOCKING category-mismatch finding). + +Cross-references: +- Canvas `r3-substrate-emission-provenance-shape-canvas.md` (parent) +- T-Rule-Enumeration brief (PREREQUISITE) +- PR #1902 (PM proposal — brief shape superseded by this revision) +- Lens Director-locked shape at `src/v3/std/lens.dag` +- T-CostLens-Composition shape precedent (#37-#40 cluster) diff --git a/docs/briefs/r3-substrate-rust-primitive-full-coverage-worker.md b/docs/briefs/r3-substrate-rust-primitive-full-coverage-worker.md new file mode 100644 index 00000000000..e66618d7ce2 --- /dev/null +++ b/docs/briefs/r3-substrate-rust-primitive-full-coverage-worker.md @@ -0,0 +1,154 @@ +--- +status: dispatchable per Director Path A RATIFICATION at gunbc#1739 #issuecomment-4392731264 (2026-05-06) +authority parent: R3 Substrate Manager (#1739) +ratification: Path A RATIFIED at gunbc#1739 #issuecomment-4392731264 (zesty-bear-812, 2026-05-06). Bundled substrate prerequisite for Grounding G2 Phase 2 full-coverage (u128 / isize / usize). Three-axis structurally-coupled slice authored as one bundled brief per "necessary structural fix" exception (bundled-scope discipline at gunbc#1739 #issuecomment-4392225548). +roadmap row: §1.8 ledger row TBD slot — gate `rust_primitive_full_coverage` (Director-ratified name); cluster TBD (T-Numeric-Construction-adjacent OR new T-Interval-Representation cluster — Mgr-discretion at PR-authoring time) +authority docs: + - gunbc#1739 #issuecomment-4392731264 (Director Path A RATIFICATION; named gate; named scope) + - gunbc#1907 #issuecomment-4392585090 (loyal-stag-699 STOP findings — substrate gaps surfaced) + - gunbc#1745 #issuecomment-4392594242 (Grounding STOP receipt; 3 substrate gaps enumerated) + - dsl/extdeps/languages/rust/primitives.dag (current Rust integer primitive rows; 9-row ratchet) + - src/v3/compiler/src/int_literal_ranges.rs (current i128 host repr; explicit u128 deferral) + - src/v3/spec/rust.dag (current Rust target spec; missing isize/usize PlatformDependent rows) +gates: + - `rust_primitive_full_coverage` (Director-ratified name; closure gate for full Rust integer primitive coverage) +worker pin: valiant-ibex-312 (freed-pool; substrate-authoring discipline fresh; numeric-domain-adjacent post-#1842 merge) +--- + +# R3 Substrate — Rust integer primitive full coverage (bundled substrate-fact-introduction) + +## Context + +Per Director Path A RATIFICATION at gunbc#1739 #issuecomment-4392731264: +Grounding G2 Phase 1 lands narrowed scope (i8-i64 + u8-u64) on existing +substrate; full-coverage (u128 / isize / usize) gates on three structurally- +coupled substrate gaps that this brief lands as **one bundled slice**. + +### Substrate gaps (per Grounding loyal-stag-699 STOP at gunbc#1907) + +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. + +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. + +## Scope + +### Deliverable 1 — `IntervalInt::ExactInterval` host-repr widening + +Refactor `src/v3/compiler/src/int_literal_ranges.rs` to support integer ranges beyond `i128` representable scope. Two shape options worker DFS-decides at dispatch: + +- **Option α (BigInt-based host repr)**: switch `ExactInterval` to BigInt (`num::BigInt` or workspace-equivalent). All existing 9 ratcheted rows continue parsing identically. Pro: simplest; covers all integer widths uniformly. Con: BigInt arithmetic vs native i128 — minor compile-time perf cost; minor dependency surface +- **Option β (typed-by-row variants)**: `enum ExactInterval { I128(i128, i128), U128(u128, u128), ... }` with per-row dispatch. Pro: native arithmetic preserved; explicit width-typing. Con: variant explosion; more complex pattern-matching at consumers + +**Mgr recommendation: α (BigInt)** — simpler; uniform; no variant explosion; perf cost is brief-time-only (parsing literal ranges; not hot-path runtime). Worker confirms via DFS at dispatch. + +Update consumers of `ExactInterval` at HEAD (worker greps for usage sites; refactor signatures; preserve semantic equivalence on the existing 9 i8-i64+u8-u64 rows via bootstrap snapshot + parse corpus manifest verification). + +### Deliverable 2 — `TargetIntegerInhabitanceBound` carrier alignment + +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. + +**Required path — wire BoundDeclaration into TargetIntegerInhabitanceBound**: + +Refactor `TargetIntegerInhabitanceBound` in `src/v3/std/emit_model.dag` to gain PlatformDependent semantics. Two structural shapes worker DFS-decides: + +- **(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. + +**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. + +Both options consume Deliverable 1's widened `Interval` representation for the u128 row. + +`dsl/extdeps/languages/rust/primitives.dag` is a separate file with its own `RustPrimitive` shape — worker confirms whether that file's rows are also a target for refactor at dispatch (per loyal-stag-699's STOP that surfaced both files as gap sites). If primitives.dag also needs structural-bound-field migration, scope expands to both files; bundled-scope check applies (likely allowed as "necessary structural fix" — same axis). + +### Deliverable 3 — `src/v3/spec/rust.dag` `TargetIntegerTypeInhabitance` rows for isize / usize + +Add `TargetIntegerTypeInhabitance` rows in `src/v3/spec/rust.dag` for `isize` / `usize` using `TargetIntegerInhabitanceBound` PlatformDependent-equivalent variant (post-Deliverable-2 carrier alignment if Option (i)). Per S7 Phase 1 brief framing — `PlatformDependent` is the substrate-side variant for compile-time-unknown bound facts. + +Worker DFS-catalogs existing row population convention at `src/v3/spec/rust.dag` lines 169-207 (5 existing rows: u32 / i32 / int64 / i128 / i32_at_program_bound) and aligns isize/usize rows to that convention. + +### Deliverable 4 — u128 row addition + +Add `u128` row to `dsl/extdeps/languages/rust/primitives.dag` consuming Deliverable 1's widened `Interval` (now BigInt-backed). Row shape: `RustPrimitive { name: "u128", bound: StaticBound(Interval { min: BigInt::from(0), max: BigInt::from(u128::MAX) }) }` (or canonical project-equivalent shape; worker confirms at dispatch). + +`int_literal_ranges.rs` ratchet update: 9 rows → 12 rows (+ u128, isize, usize). + +### 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) +- `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 + +### Deliverable 6 — §1.8 ledger row receipt + +Add `rust_primitive_full_coverage` to §1.8 ledger; advance DECLARED → CONSUMER_LANDED on merge (consumer = Grounding G2 Phase 2 full coverage; Grounding-side wiring may be same-PR co-authored OR follow-on per Mgr-Grounding discretion at dispatch). Cluster: T-Numeric-Construction-adjacent OR new T-Interval-Representation cluster — Mgr-discretion at PR-authoring time per Director ratification. + +## Slice — single PR + +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 +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 + +## 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 +- 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 +- `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; named consumer demand = Grounding G2 Phase 2; carrier-shape rationale per α/β decision) + +## 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 +- **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 + +## Authority audit receipt + +1. **Substrate exists?** At brief-author time: + - `BoundDeclaration` carrier landed (`src/v3/std/substrate.dag`) ✓ + - `RustPrimitive` rows + 9-row ratchet in `dsl/extdeps/languages/rust/primitives.dag` ✓ (current static-string form) + - `IntervalInt::ExactInterval` in `int_literal_ranges.rs` with i128 host repr ✓ (current narrow form; widening target) + - `spec/rust.dag` row population convention exists ✓ (current; missing isize/usize entries) + - This brief is producer of widened ExactInterval + structural-bound RustPrimitive + isize/usize/u128 rows +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 + +## Provenance + +Drafted 2026-05-06 by Substrate Mgr (quick-crab-830) per Director Path A RATIFICATION at gunbc#1739 #issuecomment-4392731264. Brief queues bundled substrate-prerequisite for Grounding G2 Phase 2 full-coverage; authored same window as Path A ratification per pre-authored-brief-queue discipline. + +Cross-references: +- S7 PR-F brief (`r3-substrate-s7-pr-f-bounddeclaration-consumer-worker.md`) — BoundDeclaration consumer; this brief is the Rust-target row-population side +- Grounding G2 Phase 1 narrowed dispatch (loyal-stag-699; bold-ferret-748 #1745) — runs in parallel on existing 8-primitive substrate; this brief unblocks Phase 2 +- Grounding loyal-stag-699 STOP at gunbc#1907 — surfaced the three gaps; this brief is the structural resolution