Skip to content

:Lens<EmissionProvenance> carrier + structural lens shape - #1928

Merged
briansrls merged 26 commits into
mainfrom
session/smart-ram-167-rule-enum
May 7, 2026
Merged

briansrls merged 26 commits into
mainfrom
session/smart-ram-167-rule-enum

Conversation

@briansrls

@briansrls briansrls commented May 7, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Per Director Q1(a) RATIFIED at gunbc#1739 #issuecomment-4392562911 — emission-provenance is a per-Behavior Lens<C>-shaped analysis (rejecting Q1(b) per-line instrumentation and Q1(d) parallel substrates).

Brief: docs/briefs/r3-substrate-emission-provenance-lens-worker.md.

What landed

  • src/v3/std/emission_provenance.dag — typed carrier

    • EmissionRule = String (field-path; per Director Q3 feedback_reason_not_label)
    • OptionalSourceSpan = NoSourceSpan | SomeSourceSpan { value: SourceSpan } (typed-sum idiom; v3 std has no generic Option<T>)
    • EmissionProvenance { emitted_line, rule, source_span } — record (product) per codex BLOCKING reshape (PR R3 Substrate #1910 sha 2ed1046 Finding Add SVG viz, test helpers, and makegen scaffold #1)
  • src/v3/lenses/emission_provenance.dag — Lens<List<EmissionProvenance>> structural fns (read_provenance / concat_provenance / branch_provenance / iterate_provenance / validate_provenance) per Director-locked 6-field Lens<C> shape

  • Cementing tests (emission_provenance_lens_test.rs):

    • emission_provenance_record_has_locked_three_field_shape — passes
    • optional_source_span_carries_none_and_some_arms — passes
    • emission_provenance_lens_binds_against_locked_carrier — #[ignore] (substrate-cascade STOP, see below)

Substrate-cascade STOP

Promoting data emission_provenance_lens: Lens<List<EmissionProvenance>> to a top-level declaration is blocked by Class 5 Gap 3 (top-level ValueBody boundary; sum-variant literals like Empty don't lower in data body context). Same constraint blocks the canonical generic data list_monoid<element>: Monoid<List<element>> documented at src/v3/std/list.dag:61-64.

Worker followed the named_function_count.dag / dag_shape.dag precedent (lens .dag files declare structural fns + types; data <name>_lens: Lens<C> instance lives in fixture context per e6_g1a_option3_static_lens_test.rs::mini_lens).

The #[ignore]d test contains the full fixture-bound lens declaration and serves as the dissolution-trigger landing pad: when Class 5 Gap 3 closes, un-ignore the test and (separately) promote the data declaration to the top-level lens .dag without lens-shape changes.

What's deferred

BEHAVIORALLY DEFERRED — emitter writes field-path → lens recovers same field-path round-trip. Producer wiring (instrumenting render_named_template call sites in rust_target.rs) is a separate downstream slice. Precedent: lenses.cost BEHAVIORALLY PROXY, lenses.dag_shape producer-only.

NOT bundled per Director ratification at gunbc#1739 #issuecomment-4392225548:

  • T-Rule-Enumeration edits (RETIRED per Reading C ratification)
  • Grounding-side visualization-consumer wiring

5-question authority audit

  1. Substrate exists? EmissionProvenance carrier + lens fns — this PR is producer. Lens<C> carrier landed (src/v3/std/lens.dag, 🟢 TERMINAL). T-Rule-Enumeration retired (Director Reading C — field-path enumeration is structurally already provided by *SyntaxBinding / *OpsBinding field set; substrate-state-grep confirmed at gunbc#1759 #issuecomment-4392696623).
  2. Existing brief? r3-substrate-emission-provenance-lens-worker.md (parent canvas: r3-substrate-emission-provenance-shape-canvas.md). PM-authored proposal at PR docs(briefs): Lens<EmissionProvenance> worker brief — PM-authored, Director-ratified #1902 superseded by Substrate Mgr canvas + Director Q1(a) re-ratification.
  3. Design-doc match? Director Q1(a) RATIFIED + canvas Q1 disposition + Director-locked Lens<C> 6-field shape. T-CostLens-Composition is shape precedent.
  4. Citations live? Director Q1+Q2+Q3 RATIFICATION at gunbc#1739 #issuecomment-4392562911; Reading C RATIFICATION at #issuecomment-4392797954; codex BLOCKING reshape at PR R3 Substrate #1910 sha 2ed1046 Finding Add SVG viz, test helpers, and makegen scaffold #1.
  5. Carrier dissolves the bridge? Yes for the carrier. Record EmissionProvenance with mandatory rule + optional source_span dissolves "what produced this emitted line?" structurally (rule field always present; type system enforces). Lens-instance promotion to top-level data cascades on Class 5 Gap 3.

Test plan

  • cargo build --workspace clean
  • cargo fmt --all --check clean
  • cargo clippy --all-targets -- -D warnings clean
  • new tests pass (2 of 3; 1 #[ignore] per substrate cascade above)
  • cargo test --workspace --exclude v2-compiler-tests green (CI verifies)
  • cargo test -p v2-compiler-tests green; strict-compile ratchet at 0 (CI verifies)

SG-0 net-shrink discipline

SG-0 hand-path delta: +1

SG-0 pairing: (c) structural deferral + named follow-up dispatch — the new test path src/v3/compiler/tests/integration/emission_provenance_lens_test.rs is the dissolution-trigger landing pad for the fixture-bound lens instance. Named follow-up: when Class 5 Gap 3 closes (top-level ValueBody carriers + fn-typed data-body fields land), un-ignore the emission_provenance_lens_binds_against_locked_carrier test and (separately) promote the data emission_provenance_lens declaration to top-level in src/v3/lenses/emission_provenance.dag. ROADMAP "Class 5 Gap 3" row tracks the dissolution.

briansrls added a commit that referenced this pull request May 7, 2026
…9cd0 post-merge findings)

Two findings from codex bundled review on now-merged PR #1910 sha
4229cd0 land as brief revisions for the in-flight smart-ram-167
authoring cycle (PR #1928):

1. Field-path identity threading: render_named_template call sites
   receive template values extracted from binding structs; field-path
   may not be carried alongside the value at emission time. New STOP
   trigger flags this as substrate-cascade if threading isn't
   structurally possible (typed template-with-rule-path or
   DeclarationRef carrier needed).

2. Read domain coverage gap: Lens<C>.read is per-Behavior; emitted
   output also includes declarations + program scaffold. Acceptance
   scope explicitly narrowed to Behavior-attributable lines only;
   declarations + scaffold provenance out-of-scope (separate substrate
   cascade if surfaced). Acceptance bullet retargeted to
   "Behavior-attributable span-Some + Behavior-attributable span-None"
   rather than full-emission coverage.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 7, 2026
…> structural shape

Per Director Q1(a) RATIFIED at gunbc#1739 #issuecomment-4392562911:
emission-provenance is per-Behavior Lens<C>-shaped analysis (rejecting
runtime instrumentation Q1(b) and parallel substrates Q1(d)).

Substrate authoring per brief:
  docs/briefs/r3-substrate-emission-provenance-lens-worker.md

- src/v3/std/emission_provenance.dag: typed carrier
  - EmissionRule = String (field-path per Director Q3
    "feedback_reason_not_label": substrate carries structural truth;
    nominal aliases are display-layer derived)
  - OptionalSourceSpan = NoSourceSpan | SomeSourceSpan { value: SourceSpan }
    (typed-sum idiom; v3 std has no generic Option<T>)
  - EmissionProvenance { emitted_line: Int, rule: EmissionRule,
    source_span: OptionalSourceSpan } — record (product) form per
    codex BLOCKING reshape at PR #1910 sha 2ed1046 Finding #1: rule
    + span are orthogonal and can co-inhabit; sum (coproduct) framing
    forced false either-or. Mandatory rule enforces structural
    fail-closed via type system; optional source_span is structurally
    legal absence.

- src/v3/lenses/emission_provenance.dag: Lens<List<EmissionProvenance>>
  structural fns (read / sequential.op / branch / iterate / validate)
  per Director-locked 6-field shape at src/v3/std/lens.dag. Behavioral
  read body is fail-closed Inhabits(Empty) stub; producer wiring
  (instrumenting render_named_template call sites in rust_target.rs)
  is a separate downstream slice (precedent: lenses.cost BEHAVIORALLY
  PROXY, lenses.dag_shape producer-only).

- Cementing tests:
  - emission_provenance_record_has_locked_three_field_shape (passes)
  - optional_source_span_carries_none_and_some_arms (passes)
  - emission_provenance_lens_binds_against_locked_carrier (#[ignore])
    — fixture-bound lens instance per mini_lens precedent, blocked on
    Class 5 Gap 3 substrate cascade (see PR body)

Substrate-cascade receipt: top-level
  data emission_provenance_lens: Lens<List<EmissionProvenance>> = { ... }
in src/v3/lenses/emission_provenance.dag is BLOCKED by Class 5 Gap 3
(top-level ValueBody boundary; sum-variant literals like Empty don't
lower in data body context). Same constraint blocks the canonical
generic data list_monoid<element>: Monoid<List<element>> documented at
src/v3/std/list.dag:61-64. Dissolution trigger: when Class 5 Gap 3
closes, the fixture-bound test instance promotes to top-level data here
without lens-shape changes (un-ignore the test).
@briansrls briansrls changed the title smart-ram-167 :Lens<EmissionProvenance> carrier + structural lens shape May 7, 2026
@briansrls
briansrls marked this pull request as ready for review May 7, 2026 00:25
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: c2cd8495 · Trigger: schedule
  • Comparison: origin/main @ 63044050 ... review/pr-1928-c2cd8495 @ c2cd8495
  • Thinking: 27s wall

Findings: none blocking.

Verdict: APPROVE — Small, additive substrate slice. New EmissionProvenance carrier is record-shaped with mandatory rule and OptionalSourceSpan typed-sum (no Option<T>), matches v3 std idiom, and is structurally fail-closed (illegal-state-unrepresentable for "rule absent"). Lens fns are pure, data + free functions per CODING.md. The #[ignore]'d cementing test has all three properties of tracked debt: documented, bounded, named dissolution trigger (Class 5 Gap 3 closure → un-ignore). The read_provenance stub returning Inhabits(Empty) is honest fail-closed scaffolding tied to a separately-tracked downstream slice (render_named_template instrumentation), not silent fabrication.

Exploratory observations:

  • The two doc blocks state the Class 5 Gap 3 blocker slightly differently — the file header at lenses/emission_provenance.dag:103 says "sum-variant literals like Empty don't lower in data body context," while the test attribute at emission_provenance_lens_test.rs:184 cites "opaque-body lowering rejects the nested-fn-reference identity empty_provenance_list in monoid identity field." Both plausibly true, but if both are real distinct blockers, the dissolution trigger ("just remove #[ignore]") may be optimistic — closing one gap may not unblock the other. Worth a sentence reconciling them when the gap closes.
  • EmissionRule = String is pragmatic per Director Q3 ratification, but it's the classic "stringly-typed enum" — every consumer will need to defend against malformed paths. Not a blocker (the doc is explicit this is by-design and the field-path enumeration is structurally pinned by the binding structs), just worth noting that the validate_provenance lens body will eventually need to do that defense, since the type can't.

briansrls added 2 commits May 6, 2026 20:30
…typed validate note

Per claude review on PR #1928 (sha c2cd849) exploratory observations:

1. Reconcile the two Class 5 Gap 3 receipt phrasings as facets of the
   same root: (a) bare sum-variant literal (identity: Empty) doesn't
   lower in data body, and (b) nested-fn reference (identity:
   empty_provenance_list) hits opaque-body rejection. Both reduce to
   'data bodies don't accept top-level non-scalar/non-record carriers.'
   Dissolution trigger now states 'when both facets close' rather than
   implying single-gap closure unblocks the test.

2. Add note on validate_provenance: EmissionRule = String is by-design
   per Director Q3 but the type can't enforce well-formed field-paths;
   when producer wiring lands, validate body assumes the
   field-path-resolves-to-real-field defense (round-trip against the
   *SyntaxBinding/*OpsBinding field set at HEAD).
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed both claude exploratory observations (sha c2cd849) in 32302cb:

  1. Reconciled two Class 5 Gap 3 phrasings as facets of the same root (data bodies don't accept top-level non-scalar/non-record carriers). Updated lens .dag file header AND the test #[ignore] attribute to use the unified two-facet framing; dissolution trigger now states 'when both facets close' so the un-ignore-after-Class-5-Gap-3 expectation isn't optimistic.

  2. Added stringly-typed defense note on validate_provenance lens body: when producer wiring lands, the validate body assumes the field-path-resolves-to-real-field defense (round-trip against the *SyntaxBinding / *OpsBinding field set at HEAD); malformed paths surface as aggregate diagnostic since the EmissionRule = String type can't enforce.

— sent from smart-ram-167

bootstrap_generated*.rs regen for new src/v3/std/emission_provenance.dag
+ src/v3/lenses/emission_provenance.dag (carrier types + lens fns added
in 59ffe49). Required by CI bootstrap-snapshot freshness gate
(`regen_bootstrap --verify`).
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: 6c7c3d85 · Trigger: schedule
  • Comparison: origin/main @ 617b3de1 ... review/pr-1928-6c7c3d85 @ 6c7c3d85
  • Thinking: 90s wall

Verdict: APPROVE — The substantive change is narrow: a substrate carrier (v3.std.emission_provenance), a lens module with a fail-closed read stub (Inhabits(Empty)), integration tests that pin the Director-locked record and OptionalSourceSpan sum shape, and bootstrap regen churn. Nothing in the diff clearly breaks INVARIANTS.md (faithful carrier + forward path for provenance, boundary comments for deferred emitter wiring, fail-closed stub rather than fabricated rows), docs/modeling-discipline.md (record vs mistaken coproduct for orthogonal rule/span is explicit; sum types that appear are documented; scaffold carries a named dissolution trigger for Class 5 Gap 3 and for producer wiring), CODING.md, or TESTING.md (integration-layer compile_to_dag for structural cementing matches the doc’s exception for pipeline/integration tests; the #[ignore]d test documents why and what unblocks it).

Exploratory (optional): In emission_provenance_lens_test.rs, the LENS_FIXTURE_SOURCE helpers concat_provenance / branch_provenance return only a / l, unlike src/v3/lenses/emission_provenance.dag which uses concat on both arms. The test is ignored today, but when Gap 3 closes it may be worth matching the real monoid bodies so the eventual compile receipt does not drift from the canonical lens file.

…; concat both arms in fixture

Two fixes:

1. After bootstrap regen at 6c7c3d8, the new EmissionProvenance /
   EmissionRule / OptionalSourceSpan declarations are part of the v3
   full-bootstrap Dag. The cementing tests' cached_compile_to_dag of
   the carrier source now collides with already-loaded declarations
   (duplicate-decl ResolveErrors). Switch to generated_full_bootstrap_dag()
   to query the same shapes from the bootstrap; carrier-shape
   assertions remain identical.

2. Per cursor exploratory finding on PR #1928 (sha 6c7c3d8): fixture
   helpers concat_provenance/branch_provenance now use concat(a,b) /
   concat(l,r) on both arms, matching the canonical lens .dag file at
   src/v3/lenses/emission_provenance.dag (avoids drift when Class 5
   Gap 3 closes and the #[ignore]'d test un-ignores).
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed cursor exploratory finding (sha 6c7c3d8) in 5197e4f: fixture helpers concat_provenance/branch_provenance now use concat(a, b) / concat(l, r) on both arms, matching the canonical lens .dag file. Avoids drift when Class 5 Gap 3 closes and the #[ignore]d test un-ignores.

Same commit also fixes a follow-on test failure that surfaced after the bootstrap regen at 6c7c3d8: switched the carrier-shape tests to query generated_full_bootstrap_dag() directly (the new declarations are now part of the bootstrap; re-compiling the carrier source collided with duplicate-declaration errors).

— sent from smart-ram-167

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 6c7c3d85 · Trigger: schedule
  • Thinking: 280s wall

BLOCKING (2)

Root Cause

  • src/v3/std/emission_provenance.dag Line-number semantics were introduced as a bare primitive instead of a positive line-coordinate carrier → type emitted_line as PositiveInt or a dedicated positive EmittedLine and cement that field type in the test.
  • src/v3/std/emission_provenance.dag The optional-span absence semantics are described but not classified under the coproduct receipt process → add the terminal or scaffold classification with its ledger or trigger at the declaration.

⚠️ Two substrate-shape issues should be fixed before this carrier becomes the downstream pattern.

Comment thread src/v3/std/emission_provenance.dag Outdated
// rule AND span (e.g., a derive line on a sum type), so record (product)
// is the faithful shape, not sum (coproduct).
type EmissionProvenance {
emitted_line: Int

This comment was marked as resolved.

// rather than fabricating a span. Per `feedback_no_textual_enforcement_bridges`:
// fail-closed at the substrate boundary, not via runtime sentinel.
type OptionalSourceSpan
= NoSourceSpan

This comment was marked as resolved.

briansrls added 2 commits May 7, 2026 00:56
…ipt on OptionalSourceSpan

Per codex BLOCKING (PR #1928 sha 6c7c3d8) — two substrate-shape fixes:

1. emitted_line: Int → PositiveInt (dsl/std/integer.dag:137,
   Nat where gt_zero). Line coordinates are 1-indexed and positive by
   construction; refinement type enforces the invariant in the type
   system instead of leaving it as a comment-only fact. Cementing test
   emitted_line_is_positive_int_refinement_not_bare_int verifies the
   field type is PositiveInt against the bootstrap Dag.

2. OptionalSourceSpan: added Practice 4 classification 🟢 PRIMITIVE
   per docs/modeling-discipline.md#4-coproduct-dissolution — closed
   2-variant typed sum, structurally distinguished (presence vs
   absence), irreducible. Direct analog of OptionalDiagnostic at
   v3.std.dimensions and the canonical 'absence-or-presence' idiom.
   No dissolution trigger; the two variants are exhaustive and the
   shape is terminal.

Bootstrap snapshots regen'd for the PositiveInt field-type change.
@briansrls

Copy link
Copy Markdown
Contributor Author

Both codex BLOCKING findings (sha 6c7c3d8) addressed in cbab07e:

Finding 1 (line-number positive-int carrier): emitted_line: Int → emitted_line: PositiveInt (dsl/std/integer.dag:137, Nat where gt_zero). Line coordinates are 1-indexed and positive by construction; refinement type now enforces the invariant in the type system. Cementing test emitted_line_is_positive_int_refinement_not_bare_int verifies the field type resolves to PositiveInt against the bootstrap Dag.

Finding 2 (Practice 4 receipt on OptionalSourceSpan): added 🟢 PRIMITIVE classification per docs/modeling-discipline.md#4-coproduct-dissolution — closed 2-variant typed sum, structurally distinguished (presence vs absence), irreducible. Direct analog of OptionalDiagnostic at v3.std.dimensions and the canonical 'absence-or-presence' idiom. No dissolution trigger; the two variants are exhaustive and the shape is terminal.

Bootstrap snapshots regen'd for the PositiveInt field-type change. fmt fix in e302cd5.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 6251a1e5 · Trigger: manual
  • Comparison: main @ 4d59ffa3 ... session/smart-ram-167-rule-enum @ e302cd5e
  • Conversation: View conversation

1. Story of the diff

This PR introduces v3.std.emission_provenance as the typed carrier for attributing emitted target lines: each EmissionProvenance record carries an emitted-line coordinate, a mandatory emission rule field-path, and an optional source span (src/v3/std/emission_provenance.dag:71-75). It then sketches a Lens<List<EmissionProvenance>> shape in src/v3/lenses/emission_provenance.dag, with per-behavior reads currently returning an empty witnessed list and the monoidal composition paths using concat for sequential and branch aggregation (src/v3/lenses/emission_provenance.dag:48-67). The Rust side regenerates bootstrap snapshots so the new std carrier exists in the bootstrapped DAG, and adds integration tests that pin the carrier’s declared labels plus an ignored fixture for the currently blocked top-level lens instance (src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:59-194).

2. Invariant categories

  1. LAYER MODEL — Finding, BLOCKING. This diff adds a substrate/std carrier, so illegal states need to be excluded at the model boundary. The comment defines the field as one-indexed — src/v3/std/emission_provenance.dag:58: // - \emitted_line: line number in emitted target output (1-indexed)— but the carrier stores it as unconstrainedsrc/v3/std/emission_provenance.dag:72: emitted_line: Int. That admits 0and negative line numbers as validEmissionProvenanceinhabitants. Because this is substrate shape, not implementation-only Rust, the carrier should use a structural line-number type/refinement/validated coordinate rather than rawInt.
  2. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING. The same line violates illegal states unrepresentable / fail-closed modeling discipline: src/v3/std/emission_provenance.dag:72: emitted_line: Int makes the invalid states representable even though the model explicitly says the coordinate is one-indexed. The record-vs-coproduct decision for rule plus source_span is otherwise the right modeling direction, but the line-coordinate field still leaves a forbidden state space open.
  3. CODING.md — Compliant. The new Rust test helpers are data + free functions over explicit inputs: src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:39: fn conj_field_labels(dag: &Dag, name: &str) -> Vec<String> { and src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:49: fn disj_variant_labels(dag: &Dag, name: &str) -> Vec<String> {; no hidden state or object-style behavior is introduced.
  4. TESTING.md — Finding, NON-BLOCKING. The active tests claim to cement the locked structural shape, but the helpers erase the field/variant payload types: src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:44: TypeConnective::Conj { children } => children.iter().map(|f| f.label.clone()).collect(), and src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:54: TypeConnective::Disj { variants } => variants.iter().map(|v| v.label.clone()).collect(),. As written, the tests would pass if rule stopped being EmissionRule, if source_span stopped being OptionalSourceSpan, or if SomeSourceSpan lost its value: SourceSpan payload. Tightening these to assert field order and child declaration/type shape would better match the stated “locked carrier” claim.
  5. LOCKED DESIGN DECISIONS — Compliant. The diff explicitly calls out the relevant locked/ratified decisions instead of silently diverging: the Lens framing is documented at src/v3/std/emission_provenance.dag:5-8, and the string field-path decision for EmissionRule is documented at src/v3/std/emission_provenance.dag:21-28. I did not find a diff line that contradicts those stated decisions.
  6. TRACKED vs UNTRACKED DEBT — Compliant. The behavioral deferral and scaffold are documented with bounds and dissolution triggers: producer wiring is scoped to future render_named_template instrumentation at src/v3/lenses/emission_provenance.dag:13-22, and the blocked top-level data emission_provenance_lens promotion names the Class 5 Gap 3 facets plus the trigger at src/v3/lenses/emission_provenance.dag:107-125. The ignored fixture also carries the same bounded trigger at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:167-180.

3. Verdict

REQUEST_CHANGES

The PR’s product-vs-coproduct reshape and tracked structural deferral are mostly disciplined, but the new substrate carrier admits invalid emitted-line coordinates despite declaring a one-indexed contract. Fixing that at the carrier boundary is cheaper now than after consumers start depending on EmissionProvenance.

@briansrls

Copy link
Copy Markdown
Contributor Author

Re inline finding at src/v3/std/emission_provenance.dag:72 (sha 6c7c3d8): already addressed in cbab07e + e302cd5 (current HEAD). emitted_line is now PositiveInt (dsl/std/integer.dag:137, Nat where gt_zero); zero/negative line numbers are no longer representable. Cementing test emitted_line_is_positive_int_refinement_not_bare_int verifies the field's type resolves to PositiveInt against the bootstrap Dag.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Re inline finding at src/v3/std/emission_provenance.dag:53 (sha 6c7c3d8): already addressed in cbab07e (current HEAD). OptionalSourceSpan now carries 🟢 PRIMITIVE classification per docs/modeling-discipline.md#4-coproduct-dissolution — closed 2-variant typed sum, structurally distinguished (presence vs absence), irreducible variants. Direct analog of OptionalDiagnostic at v3.std.dimensions (canonical 'absence-or-presence' idiom). No dissolution trigger because the two variants are exhaustive and the shape is terminal.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: e302cd5e · Trigger: schedule
  • Comparison: origin/main @ dd5a2cf6 ... review/pr-1928-e302cd5e @ e302cd5e
  • Thinking: 31s wall

Findings: None. The diff adds v3.std.emission_provenance (record carrier, PositiveInt, OptionalSourceSpan with explicit Practice 4 labels), lenses.emission_provenance (structural lens fns, stub read and validate with a named downstream trigger, scaffold comment with a concrete dissolution trigger for promoting the data instance), integration wiring, cementing tests against generated_full_bootstrap_dag() for locked field/refinement/shape, and an #[ignore] fixture test whose attribute documents the Class 5 Gap 3 trigger — aligned with P1 (carrier + forward wiring path), P2/P3 (single substrate carrier; stub returns honest empty lists rather than inventing provenance), and P5 (tracked scaffold, not an unnamed bridge). Regenerated bootstrap_generated*.rs churn matches introducing new .dag modules.

Verdict: APPROVE — Narrowly scoped structural landing with documented stubs and dissolution triggers; nothing in the diff clearly violates INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md.

Exploratory observations (optional): src/v3/lenses/emission_provenance.dag:31 imports Monoid but the module body never references it — worth deleting if the toolchain warns on unused imports; stale references to rust_target.rs line numbers in comments may need occasional touch-up as emit code moves.

briansrls added 2 commits May 6, 2026 20:59
…ield/payload types

Per openai-pro NON-BLOCKING TESTING finding on PR #1928 (sha 6251a1e):
prior cementing tests asserted only field/variant labels; would have
passed if rule stopped being EmissionRule, source_span stopped being
OptionalSourceSpan, or SomeSourceSpan lost its value: SourceSpan
payload.

Tightened:

1. emission_provenance_record_has_locked_three_field_shape_with_locked_field_types:
   asserts each field's type resolves to the locked carrier
   (emitted_line: PositiveInt, rule: EmissionRule, source_span:
   OptionalSourceSpan). Subsumes the standalone PositiveInt cementing
   test (codex BLOCKING sha 6c7c3d8), which is removed as redundant.

2. optional_source_span_carries_none_and_some_arms_with_locked_payload:
   asserts SomeSourceSpan variant payload contains a 'value' field
   that resolves to canonical SourceSpan from dsl/std/types.dag.

Removed unused conj_field_labels/disj_variant_labels helpers (now
inlined into the strengthened tests).
@briansrls

Copy link
Copy Markdown
Contributor Author

openai-pro NON-BLOCKING finding (sha da335d1) addressed in 6d5d908: fixture now mirrors production lens exactly.

  • Added Empty to fixture's std.list import (was using Empty at multiple sites without importing it).
  • read_provenance body: Inhabits(Empty) → Inhabits(_seed_list_provenance_empty()) to match production's seeded form.

Now when Class 5 Gap 3 closes, removing the #[ignore] is sufficient — no fixture/production mismatch hidden behind the substrate-cascade trigger.

— sent from smart-ram-167

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 0b0db483 · Trigger: schedule
  • Thinking: 236s wall

BLOCKING (1)

Root Cause

  • src/v3/std/emission_provenance.dag emitted_line was grounded through the conceptual integer module instead of the existing PositiveInt authority → import std.types { PositiveInt }, update the nearby dsl/std/types.dag reference/definition note, and mirror the import fix in the lens test fixture.

⚠️ One substrate authority edge needs to be corrected before this lands.


module v3.std.emission_provenance

import std.integer { PositiveInt }

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: PositiveInt is imported from std.integer even though its canonical declaration is std.types (dsl/std/types.dag:244), so this new substrate carrier records the wrong authority edge and violates M2/M9 single-authority grounding.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 6d5d9087 · Trigger: schedule
  • Comparison: origin/main @ fd1a65ab ... review/pr-1928-6d5d9087 @ 6d5d9087
  • Thinking: 32s wall

Verdict: APPROVE — clean substrate slice.

This adds the EmissionProvenance carrier (src/v3/std/emission_provenance.dag) and the structural Lens<List<EmissionProvenance>> (src/v3/lenses/emission_provenance.dag), with the four expected co-edits all present:

  • Bootstrap authority entry (src/v3/std/bootstrap_authority.dag:62).
  • Parse-corpus manifest hash bumped + new line (parse_corpus_manifest.txt:34,43).
  • SG-0 census expected-test entry (sg0_census_test.rs:352-358).
  • Generated bootstrap snapshots regenerated.

Modeling discipline: fail-closed shape is real, not cosmetic — rule: EmissionRule is mandatory (record over coproduct, per the cited reshape from PR #1910), and OptionalSourceSpan's two-arm typed sum follows the OptionalDiagnostic precedent rather than introducing a generic Option. emitted_line: PositiveInt lifts the 1-indexed contract into the type system. read_provenance returns Inhabits(Empty) — an honest "no attribution authored yet" rather than fabricating a span.

Scaffold accounting: the deferred fixture-bound data emission_provenance_lens instance has all three properties — documented (header comment in the lens .dag and the test ignore-reason), bounded (Class 5 Gap 3), named dissolution trigger (un-ignore when sum-variant + fn-typed ValueBody carriers land). The production_lens_module_compiles_cleanly smoke test plugs the gap that the #[ignore]d cementing test would otherwise leave (drift in the production .dag would be silent).

Nothing in the diff to flag against INVARIANTS / modeling-discipline / CODING / TESTING.

@briansrls

Copy link
Copy Markdown
Contributor Author

Re inline finding at src/v3/std/emission_provenance.dag:60 (sha da335d1): already addressed at HEAD in cbab07e. OptionalSourceSpan carries the 🟢 PRIMITIVE classification at line 46 of the current file:

// **Practice 4 classification: 🟢 PRIMITIVE** — closed 2-variant typed sum, structurally distinguished (presence vs absence), irreducible variants. Direct analog of OptionalDiagnostic at v3.std.dimensions and the canonical "absence-or-presence" idiom. No dissolution trigger — the two variants are exhaustive and the shape is terminal.

Per docs/modeling-discipline.md#4-coproduct-dissolution: 🟢 PRIMITIVE shapes don't require a dissolution trigger because they're already terminal. The classification + rationale satisfies the coproduct dissolution discipline.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Re inline finding at src/v3/std/emission_provenance.dag:32 (sha da335d1): finding is incorrect. The canonical declaration of PositiveInt is dsl/std/integer.dag:137 (type PositiveInt = Nat where gt_zero), NOT dsl/std/types.dag.

dsl/std/types.dag:260 documents the migration explicitly:

// 'NonNegativeInt' and 'PositiveInt' migrated to Nat-based shapes per S9

And dsl/std/types.dag:266 gives the canonical import shape:

// 'import std.integer { NonNegativeInt, PositiveInt }'

My import import std.integer { PositiveInt } matches the canonical authority and the precedent at src/v3/std/approximate_field.dag:19 (which imports the same way). Single-authority grounding is on std.integer, not std.types — types.dag only carries the migration receipt.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Re BLOCKING review on sha 0b0db48 (codex): finding is incorrect — same as the inline finding at line :32 already replied to. Re-stating for the top-level review:

PositiveInt canonical declaration is at dsl/std/integer.dag:137 (type PositiveInt = Nat where gt_zero), NOT dsl/std/types.dag. types.dag:260 carries the migration receipt for the S9 move ('NonNegativeInt' and 'PositiveInt' migrated to Nat-based shapes per S9); types.dag:266 documents the canonical import shape as import std.integer { NonNegativeInt, PositiveInt }.

grep 'type PositiveInt' dsl/std/ returns only dsl/std/integer.dag:137 — there is no PositiveInt declaration in types.dag. My import is correct; the precedent at src/v3/std/approximate_field.dag:19 matches.

If the codex reviewer's authority for 'canonical home is types.dag' is something other than the S9 migration receipt I'm citing, please surface — but on substrate-state-grep at HEAD, integer.dag is the single authority.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 6d5d9087 · Trigger: manual
  • Comparison: main @ e9152732 ... session/smart-ram-167-rule-enum @ 6d5d9087
  • Conversation: View conversation

1. Story of the diff

This PR introduces std.emission_provenance as a bootstrap-authoritative std module and regenerates the bootstrap snapshots around the new declarations. The new carrier models provenance as a product record, not a coproduct: each emitted line has a positive line number, a mandatory EmissionRule, and an optional SourceSpan via OptionalSourceSpan (src/v3/std/emission_provenance.dag:59-86). The lens side adds lenses.emission_provenance, which currently lands the structural functions for List<EmissionProvenance>: read returns an empty witness stub, sequential/branch compose by concat, iteration is identity, and validation is a placeholder while producer wiring is deferred (src/v3/lenses/emission_provenance.dag:43-104). The tests wire a new integration module, assert the bootstrap carrier and optional payload shapes, smoke-compile the production lens file, and record the new hand-authored test in the SG-0 census (src/v3/compiler/tests/integration.rs:60-61, src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:39-187, src/v3/compiler/tests/integration/sg0_census_test.rs:352-358).

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

Compliant — this is substrate-touching, and the new carrier is modeled on the Dag as declared std types rather than Rust-only implementation state: EmissionProvenance is a record with typed fields at src/v3/std/emission_provenance.dag:82-86, and the module is added to bootstrap authority at src/v3/std/bootstrap_authority.dag:62.

  1. INVARIANTS.md + modeling-discipline.md.

Finding (NON-BLOCKING) — P1 Documentation describes live state / Modeling Faithfulness. src/v3/std/emission_provenance.dag:7-8 says: “This file authors the typed carrier; the per-Behavior Lens<List<EmissionProvenance>> instance lives at lenses.emission_provenance.” But the landed lens file says the actual data emission_provenance_lens: Lens<List<EmissionProvenance>> declaration is not top-level production state: “the data emission_provenance_lens... instance declaration is authored as a TEST FIXTURE” and “rather than as a top-level data item here” at src/v3/lenses/emission_provenance.dag:106-113. The current live state is structural lens functions plus a fixture-bound/ignored instance, not a production Lens<C> data instance; update the std/lens headers to say the instance is fixture-bound until Class 5 Gap 3 closes so consumers do not treat a non-existent production declaration as an authority.

  1. CODING.md.

Compliant — the production lens logic follows data + free functions rather than object/method state: read_provenance, concat_provenance, branch_provenance, iterate_provenance, and validate_provenance are plain declared functions at src/v3/lenses/emission_provenance.dag:56-104; the Rust additions are test wiring and assertions, not new production object surfaces.

  1. TESTING.md.

Compliant — the PR adds active structural tests at the right seam: carrier field labels and field declaration IDs are asserted at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:61-99, the production lens file is smoke-compiled at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:110-124, and OptionalSourceSpan.SomeSourceSpan.value is checked against canonical SourceSpan at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:161-176. The ignored fixture-bound lens binding test is explicitly bounded with a Class 5 Gap 3 dissolution trigger at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:255-268.

  1. LOCKED DESIGN DECISIONS.

Compliant — the diff follows the referenced locked direction by choosing per-Behavior Lens<C> analysis rather than runtime instrumentation (src/v3/std/emission_provenance.dag:5-8, src/v3/lenses/emission_provenance.dag:7-11) and by keeping EmissionRule as the field-path reason carrier rather than adding a separate nominal rule enumeration (src/v3/std/emission_provenance.dag:21-42).

  1. TRACKED vs UNTRACKED DEBT.

Compliant — the new temporary shapes are documented, bounded, and carry triggers: the empty read_provenance stub names producer wiring as the lift condition at src/v3/lenses/emission_provenance.dag:47-55, and the top-level lens-instance scaffold records the Class 5 Gap 3 facets plus the promotion trigger at src/v3/lenses/emission_provenance.dag:106-134. The hand-authored test debt is also recorded in the SG-0 census at src/v3/compiler/tests/integration/sg0_census_test.rs:352-358.

3. Verdict

APPROVE_WITH_COMMENTS

No blocking substrate-shape issue: the carrier is modeled as the intended record, the optional span absence is typed, and the deferred lens work is tracked. The one cleanup I would make before or shortly after merge is to align the headers with live state: this PR lands structural lens functions and a fixture-bound instance scaffold, not a production Lens<List<EmissionProvenance>> instance.

briansrls added 2 commits May 7, 2026 01:52
…-rule-enum

Conflicts in src/v3/compiler/src/bootstrap_generated*.rs (decl-id renumbering
from main's recent landings) and parse_corpus_manifest.txt resolved by taking
main's snapshots and re-running:
  - regen_bootstrap (re-emits bootstrap_generated*.rs with both main's new
    declarations and our new emission_provenance carrier)
  - refresh_handwritten_parse_snapshot_manifest --ignored (refreshes the
    parse corpus manifest with the merged file set)

regen_bootstrap --verify confirms snapshots match fresh compile;
emission_provenance integration tests still 3/3 green (1 ignored).
…ro finding

Per openai-pro NON-BLOCKING P1 finding on PR #1928 (sha 6d5d908):
the carrier file header said 'the per-Behavior Lens<List<EmissionProvenance>>
instance lives at lenses.emission_provenance' — but in fact the lens .dag
only carries the structural fns; the data instance is fixture-bound until
Class 5 Gap 3 closes. Misleading consumers about live state.

Updated:

- src/v3/std/emission_provenance.dag header now says 'structural fns ...
  live at lenses.emission_provenance' and explicitly notes the data
  instance is fixture-bound in the integration test (cite path),
  blocked on Class 5 Gap 3, with promotion-to-top-level as the
  dissolution trigger.

- src/v3/lenses/emission_provenance.dag header status reframed from
  'STRUCTURALLY TERMINAL; BEHAVIORALLY DEFERRED' to 'STRUCTURALLY
  TERMINAL (fns); LENS-INSTANCE FIXTURE-BOUND; BEHAVIORALLY DEFERRED'
  with a 'What lives here vs. the test fixture' breakdown enumerating
  the five structural fns + seed and pointing at the fixture path.

Bootstrap snapshots regen'd (header edits shifted byte offsets); parse
manifest refreshed.
@briansrls

Copy link
Copy Markdown
Contributor Author

openai-pro NON-BLOCKING P1 finding (sha 6d5d908) addressed in 094be15: aligned both file headers with live state.

  • src/v3/std/emission_provenance.dag: changed "the per-Behavior Lens<List> instance lives at lenses.emission_provenance" → distinguishes between structural fns (live there) and the data instance (currently fixture-bound in the integration test, blocked on Class 5 Gap 3).
  • src/v3/lenses/emission_provenance.dag: status "STRUCTURALLY TERMINAL; BEHAVIORALLY DEFERRED" → "STRUCTURALLY TERMINAL (fns); LENS-INSTANCE FIXTURE-BOUND; BEHAVIORALLY DEFERRED" with a "What lives here vs. the test fixture" breakdown.

Bootstrap snapshots regen'd (header edits shifted byte offsets); parse manifest refreshed.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 094be156 · Trigger: manual
  • Comparison: main @ fd1a65ab ... session/smart-ram-167-rule-enum @ 094be156
  • Conversation: View conversation

1. Story of the diff

This PR adds a substrate carrier for emission provenance and a structural lens surface around it. The carrier lands in src/v3/std/emission_provenance.dag: EmissionRule is the field-path string carrier, OptionalSourceSpan is a typed absence/presence wrapper, and EmissionProvenance is a record with emitted_line: PositiveInt, mandatory rule, and optional source_span (src/v3/std/emission_provenance.dag:50, src/v3/std/emission_provenance.dag:67-69, src/v3/std/emission_provenance.dag:90-94). The lens file then declares the structural functions for Lens<List<EmissionProvenance>>: empty-seed/read, sequential concat, branch concat, loop identity, and aggregate validate (src/v3/lenses/emission_provenance.dag:57, src/v3/lenses/emission_provenance.dag:70-71, src/v3/lenses/emission_provenance.dag:75-79, src/v3/lenses/emission_provenance.dag:85-100, src/v3/lenses/emission_provenance.dag:117-118).

The production data emission_provenance_lens: Lens<List<EmissionProvenance>> instance is intentionally not landed yet: the diff documents it as fixture-bound because Class 5 Gap 3 blocks top-level ValueBody lowering for the needed list/sum/function-typed shape (src/v3/lenses/emission_provenance.dag:120-147). The rest of the diff wires the new std file into bootstrap authority and parse-corpus coverage (src/v3/std/bootstrap_authority.dag:62, src/v3/compiler/tests/integration/parse_corpus_manifest.txt:43), regenerates both bootstrap snapshots (src/v3/compiler/src/bootstrap_generated.rs:26209-26251, src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs:26209-26251), and adds integration tests for the carrier shape, production lens parsing, and the fixture-bound future lens instance (src/v3/compiler/tests/integration.rs:60-61, src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:39-282).

2. Invariant categories

  1. LAYER MODEL — Compliant. This is a substrate-touching PR, and the carrier shape uses product modeling for orthogonal facts rather than reintroducing the earlier coproduct compression: EmissionProvenance is a record with emitted_line, rule, and source_span fields (src/v3/std/emission_provenance.dag:87-94), while absence of source span is modeled as the typed NoSourceSpan | SomeSourceSpan { value: SourceSpan } carrier (src/v3/std/emission_provenance.dag:67-69). chatgpt-review-0f4e94a3-54ee-4a…
  2. INVARIANTS.md + modeling-discipline.md — Compliant. The diff handles the main modeling-pressure points explicitly: emitted_line: PositiveInt makes non-positive emitted-line coordinates unrepresentable (src/v3/std/emission_provenance.dag:73-77, src/v3/std/emission_provenance.dag:91), mandatory rule makes “rule absent” structurally impossible (src/v3/std/emission_provenance.dag:78-81, src/v3/std/emission_provenance.dag:92), and the record/product form dissolves the prior origin coproduct because rule and span can both apply to the same emitted line (src/v3/std/emission_provenance.dag:18-27, src/v3/std/emission_provenance.dag:87-89). chatgpt-review-0f4e94a3-54ee-4a…

chatgpt-review-0bd87144-fc54-49…

  1. CODING.md — Compliant. The new implementation-facing shape follows data + free functions rather than method/object scaffolding: the lens module exposes standalone functions such as read_provenance, concat_provenance, branch_provenance, iterate_provenance, and validate_provenance (src/v3/lenses/emission_provenance.dag:70, src/v3/lenses/emission_provenance.dag:75, src/v3/lenses/emission_provenance.dag:85, src/v3/lenses/emission_provenance.dag:96, src/v3/lenses/emission_provenance.dag:117). chatgpt-review-2b19e72f-5169-46…
  2. TESTING.md — Finding, NON-BLOCKING. The carrier tests say they are locking exact record/sum shapes, but the assertions collapse labels through HashSet, which masks duplicate fields/variants and extra copies. The field-shape test builds a set instead of asserting arity: src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:62: let expected_labels: HashSet<&str> = ["emitted_line", "rule", "source_span"] and src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:65: let actual_labels: HashSet<&str> = labels.iter().copied().collect();. The same pattern appears for OptionalSourceSpan at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:148-149. Testing principle: behavior-driven/cost-of-change tests should pin the actual published contract; here the published contract is “three fields” and “two variants,” so the tests should also assert children.len() == 3 and variants.len() == 2 before or alongside the set comparison. chatgpt-review-9bcb03db-dee6-43…
  3. LOCKED DESIGN DECISIONS — Compliant. The diff references the Director-ratified choices and implements them without silent divergence: per-Behavior lens framing is called out in the lens header (src/v3/lenses/emission_provenance.dag:21-25), and the top-level lens instance’s non-production status is explicit rather than disguised as complete (src/v3/std/emission_provenance.dag:10-16, src/v3/lenses/emission_provenance.dag:120-147).
  4. TRACKED vs UNTRACKED DEBT — Compliant. The scaffolds I found are tracked: behavioral producer wiring is bounded as a downstream slice (src/v3/lenses/emission_provenance.dag:27-36), the current read_provenance empty output is labeled a stub with a producer-wiring trigger (src/v3/lenses/emission_provenance.dag:61-69), the fixture-bound lens instance has a named Class 5 Gap 3 dissolution trigger (src/v3/lenses/emission_provenance.dag:129-147), and the ignored fixture test carries the same trigger in its attribute (src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:255-268).

3. Verdict

APPROVE_WITH_COMMENTS

The substrate/lens modeling choices look sound: the diff avoids the old coproduct compression, makes the mandatory provenance rule structural, and documents the fixture-bound lens instance as tracked debt rather than pretending it is production-complete. The only issue I would ask to follow up is the non-blocking test-strength gap: the HashSet assertions should also pin field/variant arity so the “locked shape” tests actually fail on duplicated or extra structural members.

…rier

Per openai-pro NON-BLOCKING TESTING finding on PR #1928 (sha 094be15):
the carrier-shape assertions used HashSet equality, which collapses
duplicates — a record with (e.g.) 'rule' declared twice or an
OptionalSourceSpan with a duplicate 'SomeSourceSpan' would have
passed the set comparison.

Added exact-arity assertions before the set comparison in both tests:
- EmissionProvenance: children.len() == 3
- OptionalSourceSpan: variants.len() == 2

Failure messages include the full label list so duplicate / extra
structural members are visible at the failure site.
@briansrls

Copy link
Copy Markdown
Contributor Author

openai-pro NON-BLOCKING TESTING finding (sha 094be15) addressed in c09e3a2: added exact-arity assertions before the HashSet membership comparison in both carrier-shape tests:

  • EmissionProvenance: children.len() == 3
  • OptionalSourceSpan: variants.len() == 2

A record/sum with duplicated structural members would pass the set comparison; the arity check catches it. Failure messages include the full label list for visibility.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: 094be156 · Trigger: schedule
  • Comparison: origin/main @ fd1a65ab ... review/pr-1928-094be156 @ 094be156
  • Thinking: 47s wall

Reviewed the non-bootstrap_generated* diff: new std carrier (emission_provenance.dag), bootstrap authority entry, lens module (lenses/emission_provenance.dag), integration tests and wiring, SG-0 census line, parse corpus manifest row, plus mechanical regen churn in the two bootstrap files.

Findings: None. The substrate carrier matches the locked record-vs-coproduct rationale (P1 / coproduct-vs-coordinate), OptionalSourceSpan is explicitly classified in-DAG, fixture-bound lens instance and stub read/validate bodies are documented with named dissolution triggers (Class 5 Gap 3 for top-level data, separate slice for emitter wiring), which satisfies the tracked-scaffold bar in your review rules. New hand-authored test Rust is registered in the SG-0 census. Nothing here violates fail-closed as “fabricate provenance entries” (empty list + NoDiagnostic is an honest stub, not a plausible fake row). CODING.md / TESTING.md stance for new code: integration/compile smoke for a standalone lens file matches the cited precedent pattern; test names state concrete behaviors.

Verdict: APPROVE — The change is narrowly scoped to the EmissionProvenance carrier and structural Lens<List<…>> shape with explicit deferrals and receipts; no concrete rubric violations surfaced in the reviewed diff.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: c09e3a21 · Trigger: manual
  • Comparison: main @ fd1a65ab ... session/smart-ram-167-rule-enum @ c09e3a21
  • Conversation: View conversation

1. Story of the diff

This PR lands emission provenance as a declared substrate carrier rather than as emitter-side instrumentation or a parallel per-line table. The new src/v3/std/emission_provenance.dag introduces EmissionRule, OptionalSourceSpan, and the product-shaped EmissionProvenance record, with emitted_line: PositiveInt, mandatory rule, and optional source attribution. src/v3/lenses/emission_provenance.dag then gives the structural Lens<List<EmissionProvenance>> functions: per-behavior read is currently an empty-list stub, sequential and branch composition use concat, iteration is identity, and aggregate validation is deferred.

The bootstrap authority, parse manifest, SG-0 census, and generated bootstrap snapshots are updated so the new std carrier is part of the bootstrapped Dag. The Rust integration test module actively pins the carrier shape and compiles the production lens module, while the full fixture-bound lens instance is present but ignored with an explicit Class 5 Gap 3 dissolution trigger.

2. Invariant categories

  1. LAYER MODEL — Compliant. This is substrate-touching, and the core carrier is modeled as a record rather than a compressed origin coproduct: src/v3/std/emission_provenance.dag:90-94 declares EmissionProvenance { emitted_line, rule, source_span }, and src/v3/std/bootstrap_authority.dag:62 adds the file to bootstrap authority.
  2. INVARIANTS.md + modeling-discipline.md — Compliant. Coproduct dissolution and illegal-state discipline are handled in the carrier: src/v3/std/emission_provenance.dag:87-94 states the rule/span axes are orthogonal and encodes them as a product, while src/v3/std/emission_provenance.dag:67-69 uses a typed OptionalSourceSpan instead of fabricating a span.
  3. CODING.md — Compliant. The added Rust is test-harness code, and it stays in the data + free-functions style: tests call explicit inputs such as generated_full_bootstrap_dag() at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:51 and cached_compile_to_dag(...) at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:130-133, without adding production-side methods, hidden state, or object-style APIs.
  4. TESTING.md — Finding (NON-BLOCKING). The production carrier declares the locked optional shape as NoSourceSpan | SomeSourceSpan { value: SourceSpan } at src/v3/std/emission_provenance.dag:67-69, but the test only searches the SomeSourceSpan payload for a field named value at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:184-188. It does not assert that SomeSourceSpan has exactly one payload field, and it does not inspect the NoSourceSpan payload at all. A future drift to SomeSourceSpan { value, extra } or NoSourceSpan { value: SourceSpan } would still pass this test even though the test name promises the locked payload shape.
  5. LOCKED DESIGN DECISIONS — Compliant. The PR explicitly names the locked/director decisions it depends on: per-behavior Lens<C> provenance rather than runtime instrumentation at src/v3/lenses/emission_provenance.dag:21-25, and EmissionRule = String as field-path identity at src/v3/std/emission_provenance.dag:29-36 plus the declaration at src/v3/std/emission_provenance.dag:50. I do not see an implicit divergence from a locked decision in the diff.
  6. TRACKED vs UNTRACKED DEBT — Compliant. The temporary shapes are documented, bounded, and have dissolution triggers. The read stub is marked as returning empty provenance until producer wiring lands at src/v3/lenses/emission_provenance.dag:61-69, and the fixture-bound lens instance scaffold names the Class 5 Gap 3 blocker plus the promotion trigger at src/v3/lenses/emission_provenance.dag:120-148. The ignored fixture test carries the same trigger at src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:273-286.

3. Verdict

APPROVE_WITH_COMMENTS. The substrate carrier shape, bootstrap integration, and scaffold accounting are sound in this diff. The only issue I found is a non-blocking test-ratchet gap around exact OptionalSourceSpan payload arity; the current production carrier is correct, but the regression test should pin both variant payload shapes exactly.

Per openai-pro NON-BLOCKING TESTING finding on PR #1928 (sha c09e3a2):
the variant-payload assertion only searched SomeSourceSpan for a 'value'
field; future drift to SomeSourceSpan { value, extra } or
NoSourceSpan { value: SourceSpan } would have passed silently.

Strengthened:

- SomeSourceSpan payload: assert children.len() == 1 before find()ing
  the 'value' field — extra payload fields fail loudly.
- NoSourceSpan payload: when payload connective is Conj, assert
  children.len() == 0 — a payload-bearing NoSourceSpan would collapse
  the absence/presence distinction with SomeSourceSpan and is now
  caught explicitly. Other connective kinds (unit/Top synthesized for
  unit variants) remain acceptable per the lowerer's representation
  choice; only payload-bearing NoSourceSpan fails.
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: c09e3a21 · Trigger: schedule
  • Comparison: origin/main @ fd1a65ab ... review/pr-1928-c09e3a21 @ c09e3a21
  • Thinking: 34s wall

Findings

None. The substantive diff adds a grounded substrate carrier (EmissionProvenance as a product type with a documented reshape from the old coproduct), registers it in bootstrap_authority.dag and the parse corpus, and implements a Lens<List<EmissionProvenance>> shape in src/v3/lenses/emission_provenance.dag with explicit 🟡 stub/scaffold notes and named dissolution triggers (Class 5 Gap 3) in both the lens file and emission_provenance_lens_test.rs (e.g. the #[ignore] reason and LENS_FIXTURE_SOURCE comments). OptionalSourceSpan includes a 🟢 classification with rationale per docs/modeling-discipline.md Practice 4. The new integration test is registered in sg0_census_test.rs with a PR-scoped receipt. The large bootstrap_generated*.rs churn is the expected mechanical follow-on from a new std module, not a separate design issue in this diff.

Verdict

APPROVE — The change matches the rubric: single-authority carrier in std, lens as declared analysis over that carrier, fail-closed framing for the empty read stub (no fabricated provenance rows), and scaffolds are bounded, documented, and tied to a concrete trigger. No invariant or doc violation stood out in the diff.

Exploratory (optional): After producer wiring exists, you may want a follow-up that tightens validate_provenance beyond NoDiagnostic; that is already explicitly deferred in the diff and is not a blocker for this structural slice.

@briansrls

Copy link
Copy Markdown
Contributor Author

openai-pro NON-BLOCKING TESTING finding (sha c09e3a2) addressed in a4a183b (+ 7a122e2 fmt):

  • SomeSourceSpan payload arity: some_children.len() == 1 before find()-ing the value field — SomeSourceSpan { value, extra } would now fail.
  • NoSourceSpan payload: when connective is Conj, assert children.len() == 0 — payload-bearing NoSourceSpan { value: SourceSpan } would collapse the absence/presence distinction with SomeSourceSpan and is now caught explicitly.

Other connective kinds (unit/Top synthesized for unit variants) remain acceptable — only payload-bearing NoSourceSpan fails.

— sent from smart-ram-167

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 7a122e2e · Trigger: manual
  • Comparison: main @ fd1a65ab ... session/smart-ram-167-rule-enum @ 7a122e2e
  • Conversation: View conversation

1. Story of the diff

This PR introduces emission provenance as a typed substrate carrier instead of leaving “what emitted this line?” as an emitter-side convention. The new v3.std.emission_provenance module defines EmissionRule as the stable field-path reason, models source-span presence explicitly with OptionalSourceSpan, and makes EmissionProvenance a product carrier with emitted_line: PositiveInt, mandatory rule, and optional source_span (src/v3/std/emission_provenance.dag:43-50, src/v3/std/emission_provenance.dag:67-69, src/v3/std/emission_provenance.dag:90-94). It is then admitted to bootstrap authority (src/v3/std/bootstrap_authority.dag:62) and regenerated into the bootstrap snapshots, including the new named declarations and payload carriers (src/v3/compiler/src/bootstrap_generated.rs:26209-26277, src/v3/compiler/src/bootstrap_generated.rs:62745-62774).

The lens side lands the structural functions for Lens<List<EmissionProvenance>>: an explicit typed Empty seed, per-behavior read currently returning empty provenance, list concatenation for sequential and branch composition, loop identity for static emission, and a no-op aggregate validator while producer wiring is deferred (src/v3/lenses/emission_provenance.dag:57-118). The PR is careful not to pretend the full production lens instance is landed: both the std carrier and lens file document that the top-level data emission_provenance_lens instance is fixture-bound until Class 5 Gap 3 closes (src/v3/std/emission_provenance.dag:10-16, src/v3/lenses/emission_provenance.dag:120-148). Tests then pin the carrier’s field arity/types, the optional span variant payload shape, and active compilation of the production lens .dag file (src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:39-134, src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:136-239).

2. Invariant categories

  1. LAYER MODEL — Compliant. This is substrate-touching: the new carrier lives in src/v3/std and is bootstrapped. The shape honors substrate modeling discipline by making the attribution record a product, not a lossy origin coproduct, and by making “rule absent” structurally impossible through the mandatory rule field (src/v3/std/emission_provenance.dag:18-27, src/v3/std/emission_provenance.dag:90-94). Bootstrap authority and generated declarations are updated in the same diff, so the new std file is not an orphan declaration (src/v3/std/bootstrap_authority.dag:62, src/v3/compiler/src/bootstrap_generated.rs:26251-26266).
  2. INVARIANTS.md + modeling-discipline.md — Compliant. Coproduct dissolution / modeling faithfulness is handled by the record form: the diff explicitly states that rule and span are orthogonal facts and models them as coordinates (src/v3/std/emission_provenance.dag:87-94). Fail-closed is also respected at the span boundary: NoSourceSpan is a real variant rather than a fabricated source span, while SomeSourceSpan carries the canonical SourceSpan payload (src/v3/std/emission_provenance.dag:60-69). Rubric reference applied from the supplied invariants/modeling docs. chatgpt-review-c8197a1c-8c5a-48…

chatgpt-review-1c1735c6-10a5-4e…

  1. CODING.md — Compliant. The production lens surface uses data + top-level functions rather than attaching behavior to a god object: _seed_list_provenance_empty, read_provenance, concat_provenance, branch_provenance, iterate_provenance, and validate_provenance are declared as independent functions over their explicit inputs (src/v3/lenses/emission_provenance.dag:57-118). The Rust additions are tests only, and they read the DAG through explicit query/accessor surfaces instead of introducing new production Rust state (src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:51-60, src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:147-156). chatgpt-review-ff8b4c60-cacd-49…
  2. TESTING.md — Compliant. The diff adds active integration coverage and wires it into the test module list (src/v3/compiler/tests/integration.rs:60-61). The tests are behavior/contract-shaped: one pins EmissionProvenance as exactly the locked three-field carrier and checks field types, one pins OptionalSourceSpan as exactly the two-arm shape with SomeSourceSpan.value: SourceSpan, and one actively compiles the production lens file so syntax/type drift is caught (src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:39-134, src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:136-239). The ignored fixture test is not silent coverage theater: it names the blocker and dissolution trigger in the attribute itself (src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:307-320). chatgpt-review-20b7b37b-5d34-43…
  3. LOCKED DESIGN DECISIONS — Compliant. The diff references Director-ratified/locked decisions and follows them rather than diverging: Q1 chooses per-Behavior Lens<C> analysis instead of runtime instrumentation (src/v3/lenses/emission_provenance.dag:21-36), and Q3 keeps the stable emission reason as a field-path string rather than a nominal enum (src/v3/std/emission_provenance.dag:29-36, src/v3/std/emission_provenance.dag:43-50). The tests also pin the locked carrier shape and field types rather than just checking name presence (src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:40-50, src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:65-107).
  4. TRACKED vs UNTRACKED DEBT — Compliant. The two temporary shapes I see are tracked bridges, not unbounded debt. The read/validate bodies are explicitly marked as a behavior-deferred stub until emitter producer wiring records real field-path provenance (src/v3/lenses/emission_provenance.dag:27-36, src/v3/lenses/emission_provenance.dag:61-69, src/v3/lenses/emission_provenance.dag:110-118). The missing top-level data emission_provenance_lens instance is documented with the exact blocking substrate gap, both known facets, bounds, and a named dissolution trigger: when Class 5 Gap 3 closes for top-level list/sum-variant carriers and fn-typed data-body fields, the fixture promotes without lens-shape changes (src/v3/lenses/emission_provenance.dag:120-148, src/v3/compiler/tests/integration/emission_provenance_lens_test.rs:307-320). The SG-0 hand-authored test entry is also explicitly accounted for (src/v3/compiler/tests/integration/sg0_census_test.rs:352-358).

3. Verdict

APPROVE

I did not find a blocking or non-blocking finding that is both tied to the diff and not already tracked by the PR’s own scaffold receipts. The substrate carrier shape is faithful and typed, the bootstrap/manifest/test wiring is present, and the remaining behavioral work is bounded with named dissolution triggers rather than smuggled in as steady state.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: 7a122e2e · Trigger: schedule
  • Comparison: origin/main @ fd1a65ab ... review/pr-1928-7a122e2e @ 7a122e2e
  • Thinking: 37s wall

APPROVE

Diff is small in substance despite the bootstrap regen volume, and I don’t see a concrete violation of the pinned modeling, coding, or testing docs. The new substrate carrier in src/v3/std/emission_provenance.dag uses a single-authority record shape for the two orthogonal facts, the OptionalSourceSpan coproduct is explicitly classified and terminal, the lens shape in src/v3/lenses/emission_provenance.dag is documented as tracked scaffold with a bounded dissolution trigger, and the same-PR structural consumers/tests are present.

briansrls added a commit that referenced this pull request May 7, 2026
* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* WIP: R3 Substrate

* fix(briefs): retire INVARIANTS.md line-number cites in r3-426 brief

Per codex review on PR #1782 (sha c2512cde): the new briefs
introduced fresh `INVARIANTS.md:<line>` citations — the same
stale-line-anchor shape the :425 sweep brief itself names as needing
dissolution. Replaces four line-number references in
r3-426-sfp-subdoc-rename-and-author-worker.md (lines 16, 28, 58, 85)
with prose-anchored locators citing the section anchor + bullet text.

The other PB-lane briefs codex flagged (r3-pb-runtime-equivalence-
corpus-seed-audit.md, r3-pb-t-fixedpoint-worker.md) belong to
neat-bear-351's lane and are not in this PR's scope; will route
separately.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(briefs): correct L6 type count + r3-435 dual-path retirement receipt

Per openai-pro review on PR #1782 (sha c2512cde):

1. L6 brief said acceptance ratchet asserts "five types" exist but
   declares six (ShapeATarget, FormAxis, BehaviorAxis,
   MethodTemplateContractKey, EmissionCell, EmissionPathProjection).
   Updated both occurrences to enumerate all six explicitly.

2. r3-435 brief authorized both Path A (typed-AST reader, deletes
   IntegrationRsScan) and Path B (scanner widening with Char state),
   but retirement receipt language only covered Path B. Updated
   ROADMAP/ledger retirement and authority-audit step 5 to cover
   both authorized dissolution paths.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(briefs): L6 second 'five types' site + T-E-P lookup-gate authority

Per cursor review on PR #1782 (sha 2072b986):

1. L6 brief acceptance bullet at :131 still said "five types" while
   the parenthetical and the Slice step at :117 said six. The prior
   fix only caught one of two sites; corrected the second.

2. T-E-P brief `e_p_call_pattern_lookup_authoritative` acceptance
   named only `lower_call_pattern` as "the only route from call
   site to LoweringTarget" — but Phase 2 explicitly requires
   lenses route through `per_call_pattern_at` (the L-7 single-
   authority lookup), NOT `lower_call_pattern` (compiler-internal).
   Acceptance text rewritten to name `per_call_pattern_at` as the
   consumer-facing gate and clarify `lower_call_pattern`'s
   internal-only scope.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(briefs): strengthen L6 ratchet from count-parity to per-row bijection

Per openai-pro REQUEST_CHANGES on PR #1782 (sha 2072b986): the L6
acceptance ratchet asserted only row-count parity between
emission_path_projections and the union of MethodTemplateContract
rows. Count parity permits duplicate projection keys and missing
source rows — the bridge from list-non-empty proxy to per-row
projection would not be mechanically proven. The whole point of
introducing MethodTemplateContractKey { target, dag_method } is to
provide 1:1 row identity.

Rewrites the ratchet to assert per-row bijection: every
MethodTemplateContract source row has exactly one matching
EmissionPathProjection row by key; every projection key resolves
to exactly one source row; duplicate projection keys fail closed.

(The other openai-pro BLOCKING finding — T-E-P
e_p_call_pattern_lookup_authoritative naming the wrong authority
— was already fixed at 6282a0704; the review citation was against
the pre-fix sha 2072b986.)

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(briefs): split L6 ratchet into slice-active vs deferred-activation gates

Per BLOCKING inline review on PR #1782 at d92459423: the prior
bijection ratchet was unsatisfiable as authored. The
*_method_template_contracts lists at HEAD (rust/python/go) are
non-empty; shipping emission_path_projections: [] alongside a
strict bijection requirement means the bijection cannot pass when
the slice lands — source rows would be uncovered. Prior text
incorrectly said "vacuously true on the empty source set" — the
SOURCE set isn't empty, only the projection set is.

Splits the ratchet into two gate categories:
- Slice-active gates: types/data shape exist + empty-state
  predicate (emission_path_projections == []).
- Deferred-activation gate: per-row key bijection, authored as a
  test scaffold by this slice but #[ignore]'d (or feature-gated
  on len > 0) until Grounding's follow-up populates rows. On
  activation, asserts the bijection over the populated set.

This honors P1 doc faithfulness: the slice's acceptance contract
is satisfiable as authored, and the bijection becomes the
load-bearing gate the row-population PR satisfies.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(briefs): require L6 bootstrap enrollment to honor P2 facts-flow-forward

Per BLOCKING inline review on PR #1782 at L6:34: the slice authored
src/v3/std/cross_target_coverage.dag but never required enrolling
it in the bootstrap/load authority. Without enrollment the file
is dead-letter on disk and EmissionPathProjection can be absent
from the downstream Dag — silent P2 facts-flow-forward violation.

Adds a new Slice step 2 requiring a cross_target_coverage field
on BootstrapFixtures in src/v3/std/extdeps_bootstrap_fixtures.dag
mirroring the *_method_template_contracts enrollment pattern, plus
a loader-visibility ratchet. Renumbers subsequent Slice steps.
Adds matching Acceptance bullet.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: R3 Substrate

* WIP: R3 Substrate

* docs(briefs): normalize Practice 4 citation in S3 brief per codex review

Codex review on PR #1782 (sha 2614217e) flagged stale citation
"Practice 4 (Step 4 of the type-introduction checklist)" in
S3 brief — no such checklist step exists in the pinned rubric.

Live rule per docs/modeling-discipline.md:131-134 is the "What to
check" checkpoint-comment requirement under Practice 4 (coproduct
dissolution). Updated the S3 reference to cite that line directly
and drop the stale "Step 4 of type-introduction checklist" wording.

S2/S8/S9 already use bare "Practice 4" without the stale steps wording.
S1 (committed earlier today) does not contain the stale phrase.
S6 (pre-existing brief flagged by reviewer as carrying the same
pattern) is out of this branch's scope; flag for separate paydown.

* docs(briefs): sweep stale Practice 4 citations corpus-wide

Codex review on PR #1782 flagged the stale "Step 4 of the
type-introduction checklist" wording — no such checklist exists in
docs/modeling-discipline.md. The live rule is the "What to check"
checkpoint-comment requirement under Practice 4 (coproduct
dissolution) at docs/modeling-discipline.md:131.

Sweep across docs/ found 2 additional briefs carrying the stale
phrasing (S3 fixed previously at 9db003d40):

- docs/briefs/r3-l6-emission-path-projection-substrate-worker.md
- docs/briefs/r3-x1b-s1-transform-dispatch-substrate-worker.md

Both updated to cite the live rule directly. Verified zero
remaining "type-introduction checklist" or "Step 4 of the"
references in docs/ tree.

* docs(briefs): add Practice 4 citation discipline note to authoring checklist

Per parent inbox status flag at gunbc#828 #issuecomment-4385346221:
add a Citation discipline section to brief-authoring-checklist.md
naming the correct shape — Practice 4 (coproduct dissolution) +
"What to check" rule at docs/modeling-discipline.md:131 — and
calling out the stale "Step 4 of the type-introduction checklist"
phrasing as a failure mode. References the corpus sweep at
2dc92f34f.

Prevents future briefs that copy old templates from re-introducing
the stale citation pattern.

* docs(r3): cascade work post-Director ratification — S1 worker, R4 routing, Unit/Quantity canvas

Per Director ratification at gunbc#828 inbox response 2026-05-06
(zesty-bear-812):

1. S1 Q1+Q2 RATIFIED → author S1 gap-test representative worker brief
   (`r3-substrate-s1-gap-test-representative-worker.md`). Dispatchable
   on T-E-P Phase 1 + E6-G0d landing; closes ledger row #61.

2. S2 Q2 RATIFIED (option-(b) T-LBP narrowing) + S3 + S8 deferrals →
   R4 carve-out routing ledger (`docs/r4-carve-out-routing.md`).
   Captures C1 (parallelism lens), C2 (effect_enum lens), C3
   (register narrowing), C4 (deferred MachineConstraint axes),
   C5 (rounding-mode product extension), C6 (Unit/Quantity).
   Cascade messages to Verification / Grounding / Debt-Paydown Mgrs.

3. S9 Phase-3 dimensional refinement boundary → Unit/Quantity carrier
   canvas (`r3-substrate-s9-unit-quantity-carrier-canvas.md`).
   Surfaces Q-Unit-1..5 for Director ratification: carrier name,
   2-axis vs 3-axis Phase-1, Duration/Seconds collapse, Refined
   composition order, Practice 4 classification.

Updates §1.8 ledger receipts for carved items; R3 closure receipts
treat carved items as explicitly-deferred (not drift).

* docs(briefs): citation-discipline fix-forward — anchors/quotes, not line numbers

Director redirect at gunbc#828 #issuecomment-... noted the citation
paydown's replacement form (`docs/modeling-discipline.md:131`) is the
same drift class as the original fabricated-step error. Bare line
numbers shift silently on any doc edit above the cited line.

Generalized fix:
- brief-authoring-checklist.md "Citation discipline" section
  rewritten to prohibit bare line-numbers across ALL cross-doc
  references (modeling-discipline.md, r3-program-plan.md,
  r3-structure.md, INVARIANTS.md, MODELING.md, etc.). Use section
  anchors (#section-name) or rule-text quotes.
- 3 briefs that swapped in :131 (S3, S6, X1B) re-converted:
  - docs/modeling-discipline.md#4-coproduct-dissolution anchor
  - "What to check" rule quoted inline (self-contained)

Brief-authoring-checklist failure-mode section names both vectors
(fabricated step + bare line numbers) and references both sweep
commits in audit trail.

Broader cross-doc citation sweep across briefs I authored on this
branch (frontmatter authority-docs lists, body prose) is recommended
per Director note — flagging as separate paydown task; this commit
closes the immediate recurrence vector.

* docs(briefs): fix unfaithful Int=AbelianGroup<Nat> + sweep stale 'Step 4' refs

Per openai-pro review on PR #1782 sha 0ecd4818 (gunbc#1782 #...):

BLOCKING fix (P1 modeling faithfulness):
- S9 + S3 directed workers to model `Int = AbelianGroup<Nat>`,
  but Nat is not an Abelian-group carrier (additive inverses
  not representable). Reframed:
  - `Int` is the additive Abelian group on integers (carrier Z);
    `Nat` is a commutative monoid under addition.
  - Algebraic relationship is **explicit group-completion**:
    `Int ≡ GroupCompletion<CommutativeMonoid<Nat>>` — NOT
    `AbelianGroup<Nat>` parameterization.
  - Worker either models `Int` directly as `AbelianGroup`
    (terminal Abelian-group instance) OR introduces explicit
    `GroupCompletion<M>` substrate carrier; decision lands in
    Phase-1 PR per P1 procedure.
- S3 cross-reference + Phase-4 algebra-axis preservation note
  reframed accordingly.

NON-BLOCKING in-PR cleanup (Practice 4 citation discipline):
- 6 briefs still carrying stale 'Practice 4 Step 4' wording
  (r3-coproduct-1/2/3, r3-l6, r3-t-e-p, r3-x1b) updated to use
  the section anchor (`docs/modeling-discipline.md#4-coproduct-dissolution`)
  + inline rule-text quote ("What to check") form per the
  citation discipline established in `b4cae5299`.

Closes both findings from openai-pro review.

* docs(briefs): Q-Unit-1..5 RATIFIED — apply Scale.Unit→One rename + ratification banner

Director ratified Q-Unit-1..5 at gunbc#828 #issuecomment-... 2026-05-06
(zesty-bear-812). All 5 questions ratified; one rename required:

- Scale enum's `Unit` value collides with outer `Unit<Q, S>` carrier
  name (`Unit<Time, Unit>` is shadowing-confusing). Rename to `One`.
- Duration ≡ Unit<Time, One> (collapses with Seconds per Q-Unit-3).
- Milliseconds ≡ Unit<Time, Milli>.

Canvas updated:
- Top-level RATIFICATION banner records all 5 ratifications + rename
- Scale enum: `Unit` → `One` (with inline rename receipt)
- Sketch product expansions use `Unit<Time, One>` / `Unit<Time, Milli>`
- Phase-3 reframe table products updated
- Q-Unit-3 prose collapse reference updated

Subsequent worker brief authoring (Unit/Quantity carrier landing
post-prerequisite) inherits the renamed shape.

* docs(briefs): Unit/Quantity carrier worker brief — Q-Unit-1..5 RATIFIED

Worker brief consumes the ratified Unit/Quantity canvas
(`5f22fd06e` ratification banner). Phase-1 lands `Unit<Q, S>` +
`Quantity` + `Scale` declarations at the ratified shape (Scale's
`One` value per Q-Unit-1 rename). Phase-2 reframes S9 Phase-3
dimensional refinements (Duration / Seconds / Milliseconds) to
outer-Refined / inner-Unit composition per Q-Unit-4 RATIFIED.
EpochMs deferred to R4 C6 (Aspect-axis follow-up).

Practice 4 marks pre-determined per Q-Unit-5: `Unit<Q, S>` 🟢
PRIMITIVE; `Quantity` + `Scale` 🟡 SCAFFOLD with "consumed by ≥1
emission rule" dissolution trigger.

Cross-program handoff to Grounding Mgr (#1745) for dimensional
emission consumption documented.

Worker pin TBD — dispatchable when idle pool refreshes.

* docs(briefs): S9 Phase-1 reframed — Int landed at #1466; UInt-only migration

Per proud-lynx-311 dispatch ack at gunbc#1739 #issuecomment-...
2026-05-06: re-grep at HEAD revealed substrate state diverges
materially from S9 brief's "Option A vs B decide" framing.

Reality check at HEAD:
- `dsl/std/integer.dag:55` already carries
  `type Int = AbelianGroup<GroupCompletion<Nat>>` per Slice 3 PR
  #1466 / commit `4ba0a6d04`. Single-authority Q6 audit doc at
  `docs/audit/t-numeric-construction-group-completion-6q.md`
  ratified this shape and explicitly rejected the compact form.
- `dsl/std/integer.dag:56` still on legacy `type UInt = UInt64`
  alias; UInt migration is the actual Phase-1 worker scope.

Brief Phase-1 step 1 reframed: Int landing acknowledged; worker
confirms HEAD match. Phase-1 step 2 reframed: UInt migration
target named (`type UInt = CommutativeMonoid<Nat>`); fixed-width
rows preserved per existing legacy-rows policy.

Historical Option A vs B framing kept as note (superseded).

Confirmed S9 dispatch ack from worker; UInt-only Phase-1 PR is
in-scope. Emission entries deferred per S3 (valiant-ant-72
pre-landing); Phase-2 deferred per S8 (quiet-boar-160 pre-landing).

* docs(briefs): fix two BLOCKING citation drift items per codex review

Codex review on PR #1782 sha 5f22fd06 flagged two authority-receipt
gaps:

1. brief-authoring-checklist.md:118 — `<this-commit>` placeholder in
   the failure-mode section was unverifiable post-merge. Replaced
   with `b4cae5299` (the actual anchor/quote conversion commit).

2. r3-378-http-path-helper-fail-open-worker.md:84 — `INVARIANTS.md
   C-8 fail-closed` cited without anchor or rule-text quote, in
   violation of the citation discipline added in this PR.
   Converted to `INVARIANTS.md#p3-fail-closed` (P3 heading anchor)
   + inline rule-text quote naming P3 + C-8.

PR's own discipline now consistently applied across the diff.

* docs(briefs): sweep bare .md:NNN citations in Substrate-Mgr-authored briefs

Per Director recommendation in citation-discipline thread (gunbc#828
follow-on): bare line-number references drift silently. Swept 19
remaining instances across 5 briefs I authored on this branch:

- docs/briefs/r3-substrate-s1-q-class-2-chain-break-gap-test-canvas.md
- docs/briefs/r3-substrate-s1-gap-test-representative-worker.md
- docs/briefs/r3-substrate-s2-t-lbp-scope-calibration-canvas.md
- docs/briefs/r3-substrate-s3-machine-constraint-carrier-worker.md

Conversion: bare `file.md:NNN` → `file.md §"Section name"` form.
Stable; survives doc edits; human-readable. Section names per
HEAD heading audit.

Verification: `grep -nE '.md:[0-9]+' docs/briefs/r3-substrate-*.md
docs/r4-carve-out-routing.md` returns zero results in
Substrate-Mgr-authored scope.

Broader corpus scope (~232 references across non-Substrate briefs)
remains as separate paydown task.

* docs(briefs): fix BLOCKING + NON-BLOCKING items per openai-pro review on a462f007

Three findings addressed; 2 BLOCKING + 1 NON-BLOCKING:

BLOCKING — R3/R4 dual authority for Unit/Quantity carrier:
R4 carve-out C6 narrowed from "Unit/Quantity carrier landing"
(deferred all of it) to **"Aspect-axis (PointKind) follow-on
for EpochMs and instant/rate-shaped refinements only"**. The
2-axis Measure<Q,S> carrier landing IS in R3 per Q-Unit-1..5
RATIFIED; only the Aspect axis (PointKind = Magnitude | Instant
| Rate) carves to R4. Cascade-message C6 reference + R4 program-
plan input list updated to match. Cross-Mgr message clarifies
Grounding consumes 2-axis dimensional refinements in R3.

BLOCKING — Locked design partially applied (Scale.Unit→One
rename in canvas alternate-sketch sections):
- Canvas line 105-108 alternate sketch ("Open question: Instant
  vs Duration axis") still used pre-rename `Unit` Scale value;
  added pre-ratification disclaimer marking the section as
  deferred to R4 C6 + noting `Unit` is pre-rename
- Canvas line 163 Q-Unit-3 collapse note: `Scale = Unit` → `Scale = One`

(BLOCKING — bare line-numbers in S1 canvas frontmatter): NOT
APPLICABLE — already fixed at sweep commit 127287a66 prior to
review; reviewer was on sha a462f007 pre-sweep.

NON-BLOCKING — placeholder receipts:
- brief-authoring-checklist.md `#issuecomment-...` → concrete ID
  4385393971 (Director's anchor-discipline reply)
- r3-substrate-unit-quantity-carrier-worker.md (3 occurrences)
  + canvas RATIFICATION banner: `#issuecomment-...` → concrete ID
  4385412256 (Q-Unit ratification reply)
- `<this-commit>` placeholder in checklist already fixed at 5be1c99f2

Verification: zero `#issuecomment-...` or `<this-commit>` placeholders
in docs/briefs/ + docs/r4-carve-out-routing.md.

* docs(briefs): codex BLOCKING review fixes — Practice 4 source-level + policy scope

Three BLOCKING findings on PR #1782 (codex sha b913e2f4):

1. **Citation-discipline policy scope**: addressed by scoping
   the rule prospectively to briefs landing after the policy
   commit (`b4cae5299`). Pre-existing corpus references are
   flagged as paydown but NOT individually blocking; coordinated
   single-PR sweep is the right paydown shape. Substrate-Mgr scope
   already swept at `127287a66`.

2. **R4 C6 reconciliation**: already fixed at `6e5a5481a` (R4 C6
   narrowed to Aspect-axis follow-on for EpochMs only; 2-axis
   carrier landing IS in R3). Codex sha b913e2f4 was pre-fix.

3. **Practice 4 source-level vs PR-body conflation**: corrected.
   Acceptance bullet for Unit/Quantity worker brief now requires
   inline checkpoint comments on the LIVE declarations in
   `dsl/std/units.dag` (load-bearing artifact per
   `docs/modeling-discipline.md#4-coproduct-dissolution` "What to
   check"). PR-body summary is supplementary, not substitute.

Closes the review's reconciliation gates.

* docs(briefs): absorb Q-MachineConstraint + Q-Unit-1-Recanvas ratifications

Two major Director ratifications absorbed:

1. Q-MachineConstraint-Carrier RATIFIED at gunbc#828
   #issuecomment-4385530115 (Brian directive 2026-05-06: "universal
   substrate, ratify defaults"; PR #1817 queued). 6 sub-decisions:
   - MachineWidth<bits> only for R3; defer RegisterClass / EndianMode
     / Alignment / signedness post-R3
   - Parametric Compose<Algebra, MachineConstraint> type-level
     interaction shape (lookup-maps REJECTED — AlgebraMachineProduct
     record-keyed table form retracted)
   - Int<64> ≡ Compose<AbelianGroup, MachineWidth<64>> (algebra-side
     options A and B preserve interaction semantics)
   - Real<64> ≡ Compose<ApproximateField<Rational>, MachineWidth<64>>
     (algebra approx + machine approx as independent composing axes)
   - ≥3 pairs is minimum, not target
   - UNIVERSAL substrate: every target carries machine-constraint
     facts; targets without native machine-width semantics handle
     omission at Grounding-level discharge (target-conditioned
     lowering NOT target-conditioned substrate)

   Reframed: S3 brief Phase-1, S3 Phase-3/4 emission entries,
   S8 Phase-1/2/3 (ApproximateField<Real> → ApproximateField<Rational>;
   AlgebraMachineProduct → Compose<...>), S9 emission entries.

2. Q-Unit-1-Recanvas RATIFIED Measure<Q, S> at gunbc#828
   #issuecomment-4385539791. valiant-ibex-312's substrate-state
   grep caught Unit<Q, S> collision with kernel Unit at
   dsl/std/types.dag:176; Director ratified Measure<Q, S> as
   outer carrier name (conventional in scientific computing;
   no dsl/std/ collision).

   Reframed: Unit/Quantity worker brief throughout (Unit<Q,S> →
   Measure<Q,S>; dsl/std/units.dag → dsl/std/measure.dag); canvas
   spec sections + sketch products (Refined<Measure<Time, ...>...>);
   R4 carve-out C6 with informal/formal name disambiguation note.

Both rename + reshape are now consistent across S3 / S8 / S9 /
Unit-Q briefs + canvas + R4 routing. Workers (valiant-ant-72 on S3,
quiet-boar-160 on S8, proud-lynx-311 on S9, valiant-ibex-312 on
Unit-Q) all dispatch against the ratified shape.

* docs(briefs): S11 Slice C worker brief — ROADMAP :425 retirement post-#1801

Cascade-clearance trigger fired post-#1801 (Slice B) merge
2026-05-06. S11 brief authored per B1 RATIFIED prose+regen
bundling discipline.

Phase 1: per-file edits across the post-A+B residual list (~10
files per smart-ram-167's Slice B post-rebase enumeration);
anchor + rule-text-quote pattern per current citation discipline;
bootstrap regen in same PR (no split).

Phase 2: ROADMAP :425 row PARTIAL → Retired with 3-slice receipt;
Q-Slice-C-Retirement-Receipt resolution.

Worker pin smart-ram-167 (#1759) — Slice B precedent owner.
Dispatch packet sent separately to #1759.

* docs(briefs): Q-Refined-Phantom-Composition (c) RATIFIED — defer literal Refined form

Director ratified option (c) at gunbc#828 #issuecomment-... 2026-05-06:
drop `non_negative` predicate at Measure (phantom) layer; rely on
`Quantity = Time` tagging for non-negative-magnitude semantics.

Q-Unit-4 outer-Refined / inner-Measure composition is preserved as
**conceptual model**; the literal `Refined<Measure<...>, predicate>`
form is **deferred to value-typed-integration follow-up** when
substrate gains Refined<> as first-class type expression and
dimensional refinements get value-typed integration.

Updates:
- Canvas RATIFICATION banner Q-Unit-4 row reframed to "conceptual
  model; literal form deferred"
- Canvas Phase-3 reframe table: Duration / Milliseconds drop the
  Refined<...> wrapper; rely on Quantity tag
- Worker brief Phase-2 prose + reframe table + Acceptance bullet
  all reflect deferred-literal-form posture

valiant-ibex-312 unblocked to proceed with Phase-2 (Grounding
handoff doc) per the (c)-shaped Acceptance.

* docs(briefs): S12 F2 + F8 doc-sharpening worker brief — post-#1820 cascade

#1820 (Slice C) merged 2026-05-06; ROADMAP :425 row Retired closes
the prose-reference paydown program. S12 cascade-clearance trigger
fires per B6 RATIFIED single bundled Mgr-tier doc-sharpening PR.

Scope: F2 (.v3 filename-suffix grammar dispatch) + F8 (bootstrap
load-order/exclusion authority) — single bundled PR per B6.
Cross-program coordination with PB Mgr (#1742) per design schedule
§3 P5 (comment-only OR co-author; no duplicate PR).

Worker pin smart-ram-167 (#1759) — Slice C precedent owner;
pattern-familiar with prose+regen bundling discipline. Dispatch
packet sent separately to #1759.

* docs(briefs): S9 brief — UInt landed via #1818; algebra label corrected to CommutativeSemiring

Per proud-lynx-311 merge report at gunbc#1746 #issuecomment-...
2026-05-06: PR #1818 landed `type UInt = Nat` after codex BLOCKING
review on initial `CommutativeMonoid<Nat>` form (P2 facts-flow-forward
violation — wrap projects out Nat's multiplicative monoid + identity 1).

Final landed form preserves full `CommutativeSemiring<Magnitude>`
surface — Nat IS a commutative semiring (addition + multiplication
+ 0 + 1). Algebra-side label for UInt is CommutativeSemiring, NOT
CommutativeMonoid (corrects my earlier dispatch labeling).

S9 Phase-1 step 2 marked LANDED with merge ref. Phase-1 step 3
emission entries reframed:
- Int<N> ≡ Compose<AbelianGroup, MachineWidth<N>>
- UInt<N> ≡ Compose<CommutativeSemiring, MachineWidth<N>>

Worker discipline + reviewer caught a substrate-state error in my
brief framing; brief now matches landed reality.

* docs(briefs): fix contradictory (c) guidance in Unit/Quantity worker brief

Codex BLOCKING review on PR #1825 sha 1bce0418 caught a real
contradiction: brief Phase-2 prose at lines 115-118 stated
"predicates do NOT attach at the Measure (phantom) layer" per
Q-Refined-Phantom-Composition (c) RATIFIED, but immediately
following paragraph at lines 130-132 still said "Refined predicate
non_negative applies at the Measure-typed level" — left over from
the original Q-Unit-4 framing.

Updated lines 130-137 to consistently apply (c) shape: predicates
deferred to value-typed-integration follow-up; dimensional semantics
ride on Quantity tag at Measure layer; worker authors 3 in-scope
refinements WITHOUT predicate at this layer.

P2 boundary discipline restored: brief now gives single-authority
guidance for Phase-2 substrate landing.

* docs(briefs): name predicate authority + concretize ratification ID — codex BLOCKING

Codex BLOCKING review on PR #1825 sha 32541a56:

1. (BLOCKING) Q-Refined-Phantom-Composition (c) ratification deferred
   phantom-carrier predicates without naming the value-level predicate
   authority. Updated canvas Q-Unit-4 RATIFICATION row to explicitly
   name: 'predicates re-attach at value-typed Int/UInt level via
   where-sugar (e.g., range(min: 0) per current dsl/std/types.dag
   precedent)' when value-typed integration lands.

2. (BLOCKING) Worker brief option-c reframe didn't sweep the audit
   receipt §5 (Carrier dissolves the bridge). Updated to consistently
   apply (c) shape — dimensional semantics ride on Quantity tag at
   Measure layer; value-level predicate authority deferred; until
   then, range/gt_zero constraints attach at value-typed Int/UInt
   via where-sugar per dsl/std/types.dag convention.

3. (NON-BLOCKING) Canvas had #issuecomment-... placeholder for the
   (c) ratification message ID. Replaced with concrete
   #issuecomment-4385687075 per dashboard relay header.

Brief now names a single value-level authority (Int/UInt where-sugar)
for value-range facts; phantom-layer Quantity tag carries only
dimensional semantics. P2 boundary discipline maintained.

* docs(briefs): S12 RETIRED per Director option (2) ratification

Director ratified option (2) at gunbc#828 #issuecomment-4385873...
2026-05-06 post smart-ram-167's substrate-state STOP-AND-ESCALATE:

- F2 absorbed by 2026-05-04 routing + #1662 closure
  (`Result/DivError span.file-keyed` retired)
- F8 topical concerns distributed across live rows
  (Class 5 Gap 3 `bootstrap.rs::std_fixtures()`; Character-level
  load-set / bootstrap; Filename-sentinel-bridges) with own owners
- Doc-discipline goals absorbed by per-Mgr citation paydown
  routing at gunbc#828 #issuecomment-4385583247

Frontmatter updated to RETIRED with absorption receipt. Worker
(smart-ram-167) pin freed.

Director-side acknowledgment of Substrate Mgr's option (2) recommendation:
"Substrate Mgr's option (2) recommendation is the right move
structurally. Most Mgrs default to 'synthesize work to fill the brief'
when canvas-vs-HEAD mismatch surfaces. Recommending retirement when
the work is genuinely absorbed is harder discipline."

* docs(briefs): S7 PR-F (BoundDeclaration consumer + ReferenceModel<T>) worker brief

Per cascade-clearance trigger fired post-#1782 merge 2026-05-06.
loyal-wolf-828 (#1764) acknowledged S7 dispatch with substrate-state
pre-flight grep (gunbc#1764 #issuecomment-4385872...) and surfaced
await-brief posture. This brief satisfies that prerequisite.

Worker pre-flight inventory absorbed:
- BoundDeclaration substrate landed (substrate.dag StaticBound +
  PlatformDependent); partial BoundDeclarationView consumer in
  fold.rs (ScratchIntExamples scope; doc-explicit partial)
- ReferenceModel<T> NOT yet in dsl/std/ (substrate-fact-introduction
  required; design-emission-model.md §Q2 framing)

Phase-1: BoundDeclaration consumer broadening to full
design-emission-model.md surface (u128 / isize / usize / walker
arms / pilot mirror).

Phase-2: ReferenceModel<T> P1 substrate-fact-introduction with
DFS-of-concept-DAG + Practice 4 in-source checkpoint comment +
named consumer demand (Grounding G1).

Phase-3: cross-program handoff to Grounding Mgr (#1745) for
G1 (T-Ground-Rust Phase 1).

Closure predicate: unblocks Grounding T-Ground-Rust Phase 1.
Worker pin loyal-wolf-828 holds; dispatch fires immediately
on this brief landing.

* docs(briefs): S9 Slice 2.5 — predicate-registry + PB-1 shim retirement (Path 3 RATIFIED)

Director ratified Path 3 at gunbc#828 #issuecomment-4390333451
post proud-lynx-311's pre-flight DFS at gunbc#1746 #issuecomment-4390253616.

Brief reframes Slice 2.5 from S-sized (primitive + 1 consumer) to
L-sized (predicate registry + PB-1 shim retirement). 5 deliverables:
1. gt_zero primitive predicate
2. Predicate registry infrastructure (resolver-side substrate-fact-introduction)
3. PB-1 shim retirement (span.file=='dsl/std/types.dag' special case dissolves)
4. Migration of existing types.dag predicates (range, pattern, etc.)
5. PositiveInt = Refined<Nat, gt_zero> consumer update

Per Director hard scope bars: no parallel predicate-resolution path;
no per-call-site special-casing; PB-1 shim retirement non-negotiable
in same slice. Single PR per Path 3 RATIFIED.

Discipline anchors: feedback_construction_over_ratchets (PB-1 shim
is bridge); feedback_dissolve_bridges (registry is structural fix);
feedback_no_textual_enforcement_bridges (file-path special-case is
anti-pattern shape); P1 substrate-fact-introduction procedure.

Worker pin proud-lynx-311 — Director pre-cleared on pre-flight DFS
context. PR #1840 (partial Slice 2 — NonNegativeInt = Nat) MERGED
at 16:54Z; Slice 2.5 dispatchable immediately on this brief landing.

* docs(briefs): Slice 2.5 audit receipt — Mgr independent grep parallel-verifies worker DFS

Codex BLOCKING review on PR #1845 sha 2d230949 flagged: external PR
receipt absorbed as live substrate state without re-grepping local
std declarations at brief authoring time. Authority receipt §1
cited proud-lynx-311's pre-flight DFS as authority but didn't
record Mgr-side independent verification.

Updated audit receipt §1 + §4 to record Mgr's independent grep at
HEAD as parallel verification:
- gt_zero zero matches in dsl/std/ + src/v3/ (verified)
- NonNegativeInt = Nat at dsl/std/integer.dag:133 (#1840 land)
- PositiveInt = Int where range(min: 1) at dsl/std/types.dag:255
- PB-1 shim doc-block confirms bridge-text framing
- Predicate registry confirmed not present

Worker DFS remains the dispatch-time discipline (substrate-state
grep at dispatch); Mgr's independent grep is parallel verification,
not substitute. Per Director's pattern note at gunbc#828
#issuecomment-4390199218 + #issuecomment-4390333451: dispatch-packet
authoring discipline includes Mgr-side substrate-state-grep, not
just relay of worker findings.

* docs(briefs): Slice 2.5 brief — Int extensibility scope-bound; lower.rs cites anchored

openai-pro REQUEST_CHANGES on PR #1845 sha 2d230949 flagged 2 issues:

BLOCKING — P1 modeling faithfulness / substrate scope leak:
`gt_zero` Int-side extensibility was left to 'worker judgment if
generalization cheap'. Per feedback_construction_over_ratchets:
don't speculatively extend predicate-carrier compatibility ahead
of named consumer demand. Reframed to **EXPLICITLY OUT-OF-SCOPE**
for Slice 2.5; Nat-only registration. Future Int-side consumer
surfaces as separate substrate-fact-introduction (P1 procedure)
brief with own consumer-demand receipt.

NON-BLOCKING — citation discipline self-violation:
3 instances of bare `lower.rs:821-835` line-range citations
contradict the brief's own 'no bare :NNN' requirement at line 211.
Converted to function-name anchored form:
`src/v3/compiler/src/lower.rs` (`lower_type_alias_refinements_phase` doc-block).

Both findings absorbed; no parallel scope ambiguity remains;
brief now self-consistent on citation discipline.

* WIP: R3 Substrate

* docs(briefs): Slice 2.5 brief — audit-receipt cites converted to declaration-name anchors

cursor APPROVE_WITH_COMMENTS on PR #1845 sha ebf6ac12 noted citation
self-inconsistency: audit-receipt section §1 + §4 used bare
`dsl/std/integer.dag:133` and `dsl/std/types.dag:255` line-number
pins despite the brief's own no-bare-:NNN rule.

Converted to declaration-name-anchored form:
- 'declaration named NonNegativeInt' (with reproducible grep command)
- 'declaration named PositiveInt' (with reproducible grep command)
- 'lower_type_alias_refinements_phase doc-block' for PB-1 location

Brief now fully self-consistent on its own citation discipline.
Verified zero remaining .dag:NNN / .rs:NNN / .md:NNN bare cites.

* docs(briefs): Slice 2.5 brief — Path (a) RATIFIED carrier+argument contract verification

Director Path (a) RATIFIED at gunbc#828 #issuecomment-4390760353
(triage) + #issuecomment-4390794121 (convergence ack):
predicate-body lowering with carrier+argument contract
verification at lower-time IN SAME SLICE. Placeholder semantics
REMOVED from registry path.

Codex REQUEST_CHANGES surfaced that registered-predicate-without-
contract = silent acceptance per feedback_fail_closed_discipline.
Brief reframe absorbs Path (a):

Hard scope bar #5 added:
- Same-slice carrier+argument-contract verification
- Mismatched carrier OR malformed argument → Diagnostic::ResolveError
- No 'named but not checked' path remains

Scope expansion section added (L → XL):
- Predicate-body lowering for all 7 registered predicates
- Per-predicate arg-shape validation
- Multi-session work acknowledged
- Carrier-check at 788d6acb4 retained; predicate-body builds on top

Acceptance bullets updated: gt_zero with arg-shape validation +
all 7 predicates with carrier+argument contract verification.

Director-pinned brief-authoring discipline: dissolution trigger
named in a brief authored as substrate-fact-introduction must
specify same-slice acceptance, not deferred follow-up. Otherwise
the brief encodes 'land bridge + defer dissolution' anti-pattern,
the same shape feedback_construction_over_ratchets warns against
at implementation layer applied at brief authoring layer.

This is the 11th miss this session — but the pattern surfacing it
(direct sweep + Codex REQUEST_CHANGES + Director ratification)
produces structural fixes that prevent the next miss class. Brief
revision is the structural recovery.

* docs(briefs): Slice 2.5 brief — Path 2 RATIFIED (Gap 1 discharge + Q-Regex carve-out)

Director Path 2 RATIFIED at gunbc#828 #issuecomment-4391985613
post Rung 3 STOP at gunbc#1746 #issuecomment-4391946213.

Path 2 narrowing of Path (a):
- gt_zero + range body synthesis already landed (5f3c40c3a)
- Gap 1 discharge mechanism: extends scalar-literal predicate
  evaluation at lower-time. L-class; lands SAME SLICE per
  same-slice-dissolution discipline
- non_empty + brand body synthesis: lands via Gap 1 discharge
- pattern / format / content: fail-closed-with-named-dep at
  user-code authoring layer (Diagnostic::ResolveError naming
  Q-Regex-Primitive). NOT placeholder; structural rejection
- PB-1 shim FULLY RETIRED per hard scope bar #3
- Q-Regex-Primitive carved as follow-on substrate-fact-introduction
  (XL substrate; not pre-authored per feedback_construction_over_ratchets)

Acceptance updated:
- 4 of 7 body-synthesized in same slice
- 3 of 7 fail-closed-with-named-dep (no placeholder semantics)
- Gap 1 discharge mechanism landed (no partial implementation)

Worker disposition: proud-lynx-311 continues Rung 3 with Gap 1
implementation + non_empty/brand body synthesis + pattern/format/
content fail-closed-with-named-dep diagnostic.

* docs(briefs): S9 Phase-1 Step 3 emission entries — Tier-1 brief authoring (1/5)

First Tier-1 brief landing post Director auto-nudge on assignment
#1858. Authored against Q-MachineConstraint sub-decisions ratified
shape now landed at #1856:

- Int<N> ≡ Compose<AbelianGroup, MachineWidth<N>> → Rust i32/i64/i128
- UInt<N> ≡ Compose<CommutativeSemiring, MachineWidth<N>> → Rust u32/u64/u128
- 6 concrete instantiations (≥3 minimum per sub-decision 5)
- Cross-program handoff to Grounding Mgr (#1745) for G2 emission consumption
- numeric_construction_demonstration Acceptance bullet (Int<32> round-trip);
  Real<64> half deferred to S9 Phase 2 / S8 Float cascade

Brief authored with substrate-state-grep discipline + same-slice-
dissolution discipline (no deferred trigger; demonstration in same
slice or explicitly carved). 5-question authority audit completed
in brief body.

Worker pin proud-lynx-311 (S9 holds); brief queues post-Slice-2.5
completion as natural follow-on.

Tier-1 brief queue progress:
- 1/5 authored (this brief)
- 4 remaining: S9 Phase-2 Float coordination; T-LBP complexity
  cementing; T-LBP cost cementing; S3 Phase-2 parser-grammar

* docs(briefs): S3 Phase-2 parser-grammar surface — Tier-1 brief 2/5

Authored per Director freed-pool pressure at gunbc#828
#issuecomment-4392095857 + Tier-1 brief-queue commitment.

Brief covers parser-grammar surface for Compose<Algebra, MachineConstraint>
interaction syntax post-#1856 (Phase-1 carrier slice landed):

- Phase 2.1: Parser surface per ratified Q-MachineConstraint-Grammar-Shape
- Phase 2.2: Bootstrap demonstrator with >=3 algebra*machine-axis pairs
- Phase 2.3: Class 1 5-criteria Pass receipt (criteria 1-4; criterion 5
  v2-oracle parity may carve)
- Phase 2.4: numeric_construction_demonstration co-receipt with S9 Phase-1
  Step 3 emission entries brief

Director ratification HOLDS on grammar bikeshed:
- Candidate A: Int @ Width<32> (annotation form)
- Candidate B: Int with MachineWidth<32> (with-form)
- Candidate C: Int<32> (positional generic — fits existing convention)
- Candidate D: Compose<AbelianGroup, MachineWidth<32>> (no parser change;
  type aliases provide convenience names)

Worker pin valiant-ant-72 holds (S3 Phase-1 precedent owner); freed-pool
until Director ratifies grammar shape.

Tier-1 brief queue progress: 2/5 authored (this brief + S9 Phase-1 Step 3).
Remaining: S9 Phase-2 Float coordination; T-LBP complexity cementing;
T-LBP cost cementing.

* docs(briefs): S3 Phase-2 brief — fix internal contradiction on Class 1 closure scope

Codex BLOCKING review on PR #1889 sha ec609b4a flagged real
contradiction:

- Provenance section claimed '5-criteria Pass closed' (line 229)
- Phase 2.3 said 'criterion 5 may queue separately' (line 154)
- STOP-AND-ESCALATE bullet 1 ratified 4-of-5 carve-out (line 181)

Updated Provenance to consistently state criteria 1-4 close in this
slice; criterion 5 (v2-oracle parity) cementing test may carve to
separate slice. Single 4-of-5 framing throughout. INVARIANTS.md
'Documentation Describes Live State' satisfied.

Per feedback_construction_over_ratchets: don't claim closure that
isn't structurally complete. 4-of-5 + named carve is the honest
shape; 5/5 only on cementing-test land.

* briefs: cite Q-MachineConstraint sub-decision 6 supersession of T-V2-Retirement gate

Address Codex BLOCKING #1 on PR #1889: S3 Phase-2 + S9 Phase-1 Step 3
worker briefs consumed Q-MachineConstraint ratification without
reconciling the historical T-V2-Retirement-landing-first cascade
gate. Add an explicit precondition-framing section to each brief
citing Director ratification at gunbc#828 #issuecomment-4385530115
(Q-MachineConstraint sub-decision 6 UNIVERSAL substrate posture)
as the implicit supersession; PR #1856 landing without T-V2-Retirement
first confirms supersession in practice. STOP-AND-ESCALATE if
supersession contested at dispatch.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* slice-2.5 brief: mark pattern/format/content Path 2 acceptance pending Director ratification

Address Codex BLOCKING #2 on PR #1889: Path 2 deliverable + acceptance
language asserted fail-closed-with-named-dep semantics for
pattern/format/content, but Director rejected that shape (Option 4)
at gunbc#828 #issuecomment-4392.... Options A (consumer migration),
B (Q-Regex bundled into slice), C (typed fail-closed exception with
named trigger) await ratification per migration-cost catalog at
#issuecomment-4392116215. Brief now flags those three predicates +
PB-1 shim retirement coupling as PENDING DIRECTOR RATIFICATION; worker
STOP-AND-ESCALATE if dispatched pre-ratification.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* slice-2.5 brief: reconcile PB-1 retirement shape with Options A/B/C gating

Address Codex BLOCKING #4 on PR #1889: prior text claimed "PB-1
FULLY RETIRED" while preceding bullet said retirement gates on
chosen path — internal contradiction. Reframe to gate the
pattern/format/content half of shim retirement on Options A/B/C
ratification while preserving Director hard scope bar #3 binding
on the gt_zero/range/non_empty/brand half (cleanly retired via
Gap 1). No path leaves PB-1 alive as parallel-authority shim on
slice landing.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: tier-1 3/5 — S9 Phase-2 Float emission coordination worker brief

Tier-1 brief queue progress (3/5): S9 Phase-2 Float<N> emission
entries (Float<32>/Float<64> via Compose<ApproximateField<Real>,
MachineWidth<N>>) + Real<64> round-trip demonstration completing
§1.8 #67 Acceptance bullet. Coordination/synthesis brief — gates on
both S8 (ApproximateField<F> + Real base carrier) and S9 Phase-1
Step 3 (Int<N>/UInt<N> emission-entry pattern) landing before
dispatch. Inherits T-V2-Retirement supersession framing from
Phase-1 Step 3. STOP-AND-ESCALATE on missing preconditions or
unratified Q-ApproximateField-Axiom-Set.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: ledger advancement honesty (PRODUCER_LANDED not CONSUMER_LANDED) + restore exact issuecomment IDs

Address openai-pro BLOCKING + NON-BLOCKING findings on PR #1889:

BLOCKING (boundary discipline / same-PR consumer): S9 Phase-1 Step 3
+ Phase-2 Float briefs claimed DECLARED → CONSUMER_LANDED upon merge
while only requiring cross-program handoff receipt to Grounding G2.
For target-primitive substrate entries, handoff is not landed-consumer
proof. Reframed both briefs to advance rows DECLARED → PRODUCER_LANDED;
Grounding G2 follow-on PR (per-pair lowering rules + emitted-Rust-
primitive verification) advances to CONSUMER_LANDED. Default
split-PR producer-then-consumer per bundled-scope discipline ratified
at gunbc#1739 #issuecomment-4392225548 (parallel infrastructure
DISALLOWED in same PR).

NON-BLOCKING (citation hygiene): replaced ellipsized
"#issuecomment-4392..." stubs in slice-2.5 brief with the exact
Director Option-4-rejection comment ID #issuecomment-4392081719 so
the ratification claim is mechanically checkable.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* slice-2.5 brief: absorb Director Option A revised RATIFICATION (final shape)

Director ratified Option A revised at gunbc#1739 #issuecomment-4392329709
(2026-05-06). Final brief shape:
- 4 predicates body-synthesize via Gap 1 (gt_zero / range / non_empty
  / brand)
- pattern / format / content STRUCTURALLY ABSENT from registry (not
  pending-with-placeholder); user-code where-clause produces
  Diagnostic::ResolveError naming Q-Regex-Primitive as separate
  substrate-fact-introduction follow-on
- ~12 types.dag refined-type declarations migrate to drop
  pattern/format/content where-clauses with inline-comment receipts
  pointing to Q-Regex restoration path; 1 extdep (sts_endpoint)
  adapts as needed
- PB-1 shim FULLY RETIRED — no exception, no preserved branch
- Q-Regex-Primitive as separate brief / worker pin / Director
  ratification cycle when concretely needed (Option B XXL bundling
  REJECTED)

Phase ordering rewritten to absorb migration as explicit phase
between predicate enrollment and shim retirement. proud-lynx-311
re-dispatches against revised brief; PR #1846 absorbs additional
scope per Director directive.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* s3-phase-2 brief: absorb Q-MC sub-decision 3 ratification (grammar shape was already answered)

Director observation at gunbc#1739 #issuecomment-4392382517: Q-MC
sub-decision 3 (Brian directive 2026-05-06 at gunbc#828
#issuecomment-4385530115) already ratified the grammar shape —
`Int<N>` user surface desugars to `Compose<Int, MachineWidth<N>>`
substrate parametrically. Earlier brief HOLD framing was redundant.

Brief revised:
- Replace bikeshed section with Q-MC sub-decision 3 quotation +
  surface/substrate framing (Candidate C user-facing; Candidate D
  substrate elaboration; A/B rejected per Director assessment)
- Phase 2.1 parser surface scoped to numeric-literal-position
  recognition + parametric desugar
- Front-matter status: dispatchable per ratification (not HOLD)
- Provenance: ratification-state-grep discipline pin folded into
  standing dispatch-checklist

valiant-ant-72 dispatch fires immediately per Director directive.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: remove truncated issuecomment-4392... stub from S9 Phase-1 Step 3 provenance

Address cursor NON-BLOCKING finding on PR #1889 sha 94292e48: line 144
truncated issuecomment ID. The originally-intended Director auto-nudge
comment doesn't map cleanly to a single ID, so replace with the
standing assignment reference (gunbc#1858) which is unambiguous.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: tier-1 4/5 + 5/5 — T-LBP complexity + cost lens cementing-test worker briefs

Tier-1 brief queue completes (4/5 + 5/5):

4/5 — T-LBP complexity-lens cementing test (§1.8 rows #79 + #87
first entry). Consumer-side cementing test against frozen v2-oracle
snapshot; producer-side Lens<Complexity> instance is upstream
precondition. Per Q-Lens-Behavioral-Parity-R3-Closeability option
(b) RATIFIED at gunbc#828 #issuecomment-4385329180 — T-LBP narrowed
to complexity + cost lenses only.

5/5 — T-LBP cost-lens cementing test + cost_lens_demonstration
(§1.8 rows #80 + #70 + #87 second entry). Absorbs row #70 demo
naturally — same source corpus + lens run; demonstration adds
observable-cost-bound assertions on top of parity check. ≥2
algebra-instances composed + ≥1 recursive call required per row #70.

Both briefs gate on:
- T-LBP per-lens substrate-producer brief landing (Lens<C> instance)
- Frozen v2-oracle snapshot capture (separate brief, pre-v2-retirement)
- DO NOT capture-against-live-oracle (violates
  v2_oracle_no_remaining_test_consumers)
- DO NOT bundle producer/snapshot/algebra-instance authoring per
  Director bundled-scope ratification at gunbc#1739
  #issuecomment-4392225548

Tier-1 5/5 complete. Worker pins assigned at dispatch time once
preconditions land.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* canvas: emission-provenance substrate shape disposition (supersedes PR #1902 PROPOSAL)

Substrate Mgr canvas authored post-codex BLOCKING + PM disposition
handoff at gunbc#846 #issuecomment-4392510255.

Two real substrate-shape questions stacked:

Q1 (category mismatch): Lens<C>.read is per-Behavior; emission
provenance is per-emitted-line. 4 options surfaced — (a) per-Behavior
Lens-compatible / (b) per-line instrumentation NOT a lens / (c)
withdraw + re-canvas / (d) Mgr-surface both substrates distinct.
Mgr recommends (d) if visualization is load-bearing; (a) suffices
if per-Behavior aggregate works for the slide. Brian-channel
sub-question surfaced.

Q2 (fold-rule enumerability): T-Rule-Enumeration substrate-fact-
introduction is prerequisite for every Q1 path (rust_target.rs uses
inline &str template names; rules not enumerable). Mgr recommends
parallel-dispatch with Q1 deliberation — satisfies Brian's ASAP
framing while shape ratifies.

Q3 (§1.8 ledger retarget): #89 already taken by T-LAS; new cluster
location follows Q1 disposition.

Director ratification ask + Brian-channel sub-question surfaced.
PR #1902 close-superseded post-ratification.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: reconcile Compose<...> slot-1 spellings to algebraic-concept names per Q-MC sub-decision 3

Address cursor NON-BLOCKING on PR #1889 sha 2b49b30f: S3 Phase-2
brief mixed Compose<AbelianGroup, ...> with Compose<Int, ...>; S9
Phase-1 Step 3 used Compose<AbelianGroup, ...> + Compose<CommutativeSemiring,
...>; S9 Phase-2 used Compose<ApproximateField<Real>, ...>. All wrong
per Q-MC sub-decision 3 critical correction at gunbc#828
#issuecomment-4385530115:

  "prior phrasing Compose<AbelianGroup, MachineWidth<64>> was wrong
  — AbelianGroup<T> is a witness shape over carrier T, not a carrier
  constructor; bare AbelianGroup in slot-1 composes witness rather
  than concept."

Slot-1 is the fully-applied algebraic-concept name:
- Int<N>  = Compose<Int,  MachineWidth<N>>   (Int = AbelianGroup<GroupCompletion<Nat>>)
- UInt<N> = Compose<UInt, MachineWidth<N>>   (UInt = CommutativeSemiring<Nat>)
- Real<N> = Compose<Real, MachineWidth<N>>   (Real = ApproximateField<Rational>)

Phase-2 Float brief also retargets user-facing surface from Float<N>
to Real<N> (Float is target-language name for the Rust primitive;
Real is the algebraic-concept name per Q-MC sub-decision 3 example).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* s9-p1-s3 brief: scope Deliverable 4 to producer-side verification (defer demonstration to Grounding G2)

Address Codex BLOCKING (line 82 inline + bundled review): brief
claimed end-to-end Int<32> → Rust i32 round-trip in Acceptance
while Deliverable 3 said lowering rules belong to Grounding G2
follow-on. Internal contradiction.

Reframe per Director bundled-scope discipline (gunbc#1739
#issuecomment-4392225548 — parallel infrastructure DISALLOWED
same-PR):

- Deliverable 4: producer-side substrate-axis verification only
  (type-check + carrier acceptance + bootstrap snapshot/manifest
  hold). NO end-to-end Rust emission in this PR.
- §1.8 #67 numeric_construction_demonstration receipts split:
  producer half here (entries exist), consumer half on Grounding
  G2 PR (full Int<32> → Rust i32 round-trip).
- Same-PR cross-program co-author available if Substrate Mgr
  coordinates with Grounding Mgr at dispatch; default is split.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: pre-author T-Rule-Enumeration substrate-fact-introduction worker brief

Pre-authored per pre-authored-brief-queue discipline; dispatch fires
on Director Q2 ratification of emission-provenance canvas at
gunbc#828 #issuecomment-4392519713.

Brief covers LangSpec emission-rule names as enumerable substrate
(rust_target.rs uses inline &str template names today; 0 hits on
RuleName/FoldRule/EmitRule across src/v3/). Two carrier shape options
(α sum-type / β named-string list) with worker DFS at dispatch
deciding shape; Practice 4 checkpoint discipline + ledger-row receipt.

Prerequisite to every Q1 path (a/b/d) — Lens<EmissionProvenance>,
per-line instrumentation, and the both-substrates option all consume
the rule-name set. Path (c) leaves substrate-unblocked-but-unconsumed.

Mgr authoring authority per PM concur at gunbc#846
#issuecomment-4392510255 / #issuecomment-4392543633 (substrate-fact-
introduction is Mgr-tier, not PM tactical authoring).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* t-rule-enumeration: align gate name + status to Director ratification at #4392562911

* emission-provenance lens brief: revise per Director Q1 (a) RATIFICATION

Director Q1 (a) per-Behavior Lens<C>-compatible RATIFIED at gunbc#1739
#issuecomment-4392562911 (2026-05-06); (b) instrumentation REJECTED;
(d) parallel-substrates REJECTED.

Brief revised:
- Carrier shape: Lens<List<EmissionProvenance>> per (a)
- EmissionOrigin = SubstrateDeclMirror(SourceSpan) | FoldRuleAutoEmit(EmissionRule)
  typed sum (closed; no third silent class; structural fail-closed)
- All 6 Lens<C> field bindings concrete (read/sequential/branch/iterate/validate)
- T-Rule-Enumeration named as PRECONDITION (must land first)
- §1.8 retarget under T-CostLens-Composition cluster per Director Q3
- Brian's slide visualization served by (a) projection (per-Behavior
  list flattens to per-line view at visualization layer; no parallel
  substrate needed)

Supersedes PM-authored proposal at PR #1902 (merged at 54419badf).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: bundled Rust-primitive-full-coverage substrate-prerequisite worker brief (Director Path A)

Author bundled substrate-prerequisite brief per Director Path A
RATIFICATION at gunbc#1739 #issuecomment-4392731264 (2026-05-06).

Three structurally-coupled gaps surfaced via Grounding loyal-stag-699
STOP at gunbc#1907 #issuecomment-4392585090 land as one bundled slice
per "necessary structural fix" exception (bundled-scope discipline):

1. IntervalInt::ExactInterval host-repr widening (α BigInt-based
   recommended; β typed-variants if α infeasible)
2. RustPrimitive structural BoundDeclaration field (replaces static
   range_min/max strings; consumes existing BoundDeclaration carrier
   StaticBound + PlatformDependent variants)
3. spec/rust.dag PlatformDependent row population for isize/usize +
   u128 row addition consuming widened ExactInterval

Closure gate: rust_primitive_full_coverage (Director-ratified name).
Worker pin: valiant-ibex-312 (freed-pool; substrate-authoring fresh;
numeric-domain-adjacent post-#1842).

Unblocks Grounding G2 Phase 2 full-coverage dispatch. G2 Phase 1
narrowed dispatch (i8-i64 + u8-u64) runs in parallel on existing
substrate; cleared at gunbc#1745 #issuecomment-4392795954.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: align Practice 4 classifications to GREEN/YELLOW rubric + add GREEN ledger receipts

Address codex BLOCKING on PR #1910 sha f36e1205: briefs used
PRIMITIVE/SCAFFOLD terminology that doesn't match docs/modeling-
discipline.md rubric. Per modeling-discipline.md lines 97/103/108:
the three classifications are 🟢 GREEN (terminal) / 🟡 YELLOW
(scaffold) / 🔴 RED (dissolvable-now); line 132 requires a ledger
entry if GREEN.

Replaced PRIMITIVE → GREEN, SCAFFOLD → YELLOW across all three
emission-provenance / Rust-primitive-full-coverage briefs. Added
explicit §1.8 ledger entry receipt for the GREEN classification on
EmissionOrigin (sibling row emission_origin_classification_green to
parent emission_provenance_lens_landed gate).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: Practice 4 terminal receipt for EmissionOrigin + bound for β scaffold

Address openai-pro BLOCKING (sha f36e1205, ran post-rubric-rename):

1. EmissionOrigin GREEN terminal classification needs documented
   attempted-dissolutions per modeling-discipline.md "no richer
   source exists" framing. Added 3 attempted dissolutions:
   - collapse to optional-pair (rejected by codex Finding 1 prior)
   - factor common richer source (orthogonal payload types prevent)
   - third arm for unattributable lines (rejected per Slice 2.5
     Option 4 placeholder anti-pattern)

2. T-Rule-Enumeration β (YELLOW) scaffold needs bound per three-part
   bridge rule. Added: allowed call sites scoped to emission code only;
   max lifetime gated on rule_name_typo_fail_closed_landed graduation;
   new emission-introspection consumers MUST author against closed-sum
   α form, not β.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: R3 Substrate

* briefs: address codex BLOCKING bundle (sha 2ed1046e) — record-form provenance + emit_model carrier alignment + T-Rule-Enumeration retirement flag

Three findings addressed:

1. Lens brief (Finding #1 — provenance shape conflates source vs rule
   attribution): replaced typed-sum EmissionOrigin with record
   EmissionProvenance { rule: EmissionRule [mandatory], source_span:
   Option<SourceSpan> [optional] }. Co-inhabitance is real (e.g.,
   #[derive(Debug)] line has both rule=derive_for_disj AND span
   attribution to Foo decl). Rule-mandatory enforces fail-closed
   structurally; Practice 4 N/A (record, not coproduct).

2. T-Rule-Enumeration brief (Finding #2 — rule authority lives in
   spec/rust.dag + v3.std.emit_model, not call-site strings): brief
   status flipped to FLAGGED FOR RETIREMENT. Same finding as
   smart-ram-167 STOP at gunbc#1759 #issuecomment-4392696623; Reading
   C surfaced to Director at gunbc#828 #issuecomment-4392780871.

3. Rust-primitive-full-coverage brief (Finding #3 — BoundDeclaration
   not wired into TargetIntegerInhabitanceBound row surface):
   reframed Deliverable 2 to target the actual carrier
   `v3.std.emit_model::TargetIntegerInhabitanceBound` (used by
   `TargetIntegerTypeInhabitance` rows in src/v3/spec/rust.dag lines
   169-207). Two paths surfaced: Option (i) wire BoundDeclaration into
   TargetIntegerInhabitanceBound; Option (ii) populate via existing
   variants if PlatformDependent already exists on the live carrier.
   Worker DFS at dispatch picks. Deliverable 3 retargeted to
   TargetIntegerTypeInhabitance rows (the actual surface).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* rust-primitive-full-coverage: codex inline confirms TargetIntegerInhabitanceBound has no PlatformDependent variant — Option (ii) infeasible; carrier refactor REQUIRED

Codex BLOCKING inline at PR #1910 line 65 (sha 98507c432) verified at
HEAD: TargetIntegerInhabitanceBound = BoundUnspecified | StaticBoundFact(IntInterval).
No PlatformDependent variant. Earlier brief framing of Option (ii)
(populate via existing variants) was infeasible.

Brief reframed: carrier refactor is required (not optional). Two
structural shapes for the refactor — (i.a) embed BoundDeclaration
(Mgr recommendation; single-authority discipline) vs (i.b) extend
variant set with PlatformDependent. Existing 5 rows migrate either
way; bootstrap snapshot semantic-equivalence non-negotiable.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* emission-provenance lane: T-Rule-Enumeration RETIRED + Lens brief revised per Director Reading C

Director Reading C RATIFIED at gunbc#1739 #issuecomment-4392797954
(2026-05-07):
- Q1: T-Rule-Enumeration retires (substrate gap was phantom; ~37
  *SyntaxBinding/*OpsBinding field paths already provide enumeration
  per smart-ram-167 substrate-state-grep at gunbc#1759 #issuecomment-4392696623)
- Q2: Lens<EmissionProvenance> dispatches now (no precondition gate)
- Q3: EmissionRule = String of field-path (per feedback_reason_not_label)

Actions:
- Delete docs/briefs/r3-substrate-t-rule-enumeration-worker.md
- Lens brief: replace T-Rule-Enumeration precondition gate with
  Reading C absorption section; EmissionRule = field-path String;
  cementing test verifies field-path round-trip; STOP triggers
  retargeted to *SyntaxBinding field-set divergence

Worker pin: smart-ram-167 (Mgr discretion per Director ratification;
fresh context on field-path enumeration). valiant-ibex-312 stays on
Rust-primitive-full-coverage / T-Interval-Representation.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* emission-provenance lens brief: absorb codex BLOCKING bundle (sha 4229cd09 post-merge findings)

Two findings from codex bundled review on now-merged PR #1910 sha
4229cd09 land as brief revisions for the in-flight smart-ram-167
authoring cycle (PR #1928):

1. Field-path identity threading: render_named_template call sites
   receive template values extracted from binding structs; field-path
   may not be carried alongside the value at emission time. New STOP
   trigger flags this as substrate-cascade if threading isn't
   structurally possible (typed template-with-rule-path or
   DeclarationRef carrier needed).

2. Read domain coverage gap: Lens<C>.read is per-Behavior; emitted
   output also includes declarations + program scaffold. Acceptance
   scope explicitly narrowed to Behavior-attributable lines only;
   declarations + scaffold provenance out-of-scope (separate substrate
   cascade if surfaced). Acceptance bullet retargeted to
   "Behavior-attributable span-Some + Behavior-attributable span-None"
   rather than full-emission coverage.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* rust-primitive-full-coverage: revert to Option (ii) — Mgr ratification-state-grep miss caught by valiant-ibex-312

valiant-ibex-312 ratification-state-grep at gunbc#1761
#issuecomment-4393074602 surfaced that origin/main HEAD has
TargetIntegerInhabitanceBound with 3 variants including
PlatformDependentFact (mirrors BoundDeclaration::PlatformDependent).
Earlier brief framing at 4229cd09d was against pre-PlatformDependentFact
state per codex BLOCKING reading; main moved since.

Option (ii) IS feasible: isize/usize rows populate via existing
PlatformDependentFact variant directly; u128 row populates StaticBoundFact
with BigInt-widened ExactInterval (Deliverable 1 unchanged). No
carrier refactor needed; 5 existing rows untouched.

Second Mgr-tier ratification-state-grep miss today (first was symbol-only
grep on T-Rule-Enumeration; now stale-codex-vs-current-HEAD on
TargetIntegerInhabitanceBound). Worker-tier discipline caught it before
sinking time into invasive Option (i.a) refactor.

Single-authority concern (parallel-named variants on
TargetIntegerInhabitanceBound vs BoundDeclaration) noted as future
substrate-fact-introduction; not blocking this slice — explicit-mirror
is the existing convention.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* rust-primitive-full-coverage: align Acceptance + Phase ordering + STOP triggers to Option (ii) (resolve codex internal-contradiction finding)

codex BLOCKING on PR #1929 sha 14f68b63 caught real internal contradiction: Context section flipped to Option (ii) feasible at 57ae4349b but Acceptance + Phase ordering still referenced BoundDeclaration migration / RustPrimitive bound field refactor from earlier Option (i.a) framing.

All sections now consistent with Option (ii):
- Phase 4 = no-op (TargetIntegerInhabitanceBound carrier untouched)
- Phase 5 = spec/rust.dag rows for isize/usize via existing PlatformDependentFact variant
- Phase 6 = u128 row via StaticBoundFact(IntInterval) + ratchet update
- Acceptance retargeted to row-population shape (no carrier refactor; existing 5 TargetIntegerTypeInhabitance rows untouched)
- STOP triggers retargeted to TargetIntegerInhabitanceBound variant-set sufficiency at HEAD
- Why-bundled rationale rewritten to Option (ii) shape (Phase A widening unblocks u128 StaticBoundFact; isize/usize use existing PlatformDependentFact)

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* lens brief: narrow Deliverable 3 verification step 4 to Behavior-attributable lines (resolve codex #2 consistency)

codex BLOCKING #2 on PR #1929 sha 812602b4 caught: Acceptance + STOP triggers narrowed to Behavior-attributable lines but Deliverable 3 cementing-test step 4 still said 'every emitted line'. Now consistent — step 4 explicitly scopes to Behavior-attributable subset; declarations + program scaffold OUT-OF-SCOPE per same Finding #2 framing.

(codex BLOCKING #1 — claim that PlatformDependentFact NOT on main — is wrong; verified at origin/main HEAD: TargetIntegerInhabitanceBound has 3 variants including PlatformDependentFact. Rebut on PR.)

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* briefs: pre-author IntPlatform/UIntPlatform substrate-fact-introduction follow-on (Director ratification at #4393248961)

Per Director Q1+Q2+Q3+Q4 RATIFICATION at gunbc#1739 #issuecomment-4393248961 (2026-05-07): pre-author follow-on brief for the substrate cascade surfaced by valiant-ibex-312 STOP at gunbc#1761 #issuecomment-4393222862.

Scope:
- Q1 naming: IntPlatform / UIntPlatform per feedback_reason_not_label
- Q2 algebra: Compose<Int, MachineWidth<Platform>> + Compose<UInt, MachineWidth<Platform>>; Platform is substrate token
- Q3 substrate-concept layer (target-agnostic per feedback_target_agnostic_ir)
- Q4 worker pin: valiant-ibex-312 post-PR-#1914 close (freshest substrate context)

Brief covers Platform substrate token + IntPlatform/UIntPlatform declarations + spec/rust.dag isize/usize row population + co-receipt advancing PR #1914's rust_primitive_full_coverage gate PARTIAL → CONSUMER_LANDED.

Closure gate: int_platform_uint_platform_substrate_landed.

Dispatchable post-PR-#1914 close per pre-authored-brief-queue discipline.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* intplatform brief: rename inner token Platform → PointerWidth per Director ack at…
@briansrls
briansrls merged commit 6680e05 into main May 7, 2026
3 checks passed

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 7a122e2e · Trigger: schedule
  • Thinking: 308s wall

Non-blocking — Strengths

  • src/v3/lenses/emission_provenance.dag The Class 5 Gap 3 deferral is documented, bounded to the top-level data-body boundary, and names the dissolution trigger.

⚠️ Prior blocking comment 3198478491 remains unresolved; no additional new blocking concerns found.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant