Skip to content

R3 Substrate - #1931

Merged
briansrls merged 136 commits into
mainfrom
session/quick-crab-830
May 7, 2026
Merged

briansrls merged 136 commits into
mainfrom
session/quick-crab-830

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Opened from session-dashboard for session quick-crab-830.

briansrls and others added 30 commits May 5, 2026 03:51
Per codex review on PR #1782 (sha c2512cd): 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>
Per openai-pro review on PR #1782 (sha c2512cd):

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>
Per cursor review on PR #1782 (sha 2072b98):

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>
…tion

Per openai-pro REQUEST_CHANGES on PR #1782 (sha 2072b98): 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 6282a07; the review citation was against
the pre-fix sha 2072b98.)

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

Per BLOCKING inline review on PR #1782 at d924594: 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>
briansrls and others added 18 commits May 6, 2026 19:52
…venance + 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>
…bitanceBound has no PlatformDependent variant — Option (ii) infeasible; carrier refactor REQUIRED

Codex BLOCKING inline at PR #1910 line 65 (sha 98507c4) 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>
…ised 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>
…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>
…n-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 4229cd0 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>
# Conflicts:
#	docs/briefs/r3-substrate-emission-provenance-lens-worker.md
#	docs/briefs/r3-substrate-rust-primitive-full-coverage-worker.md
…P triggers to Option (ii) (resolve codex internal-contradiction finding)

codex BLOCKING on PR #1929 sha 14f68b6 caught real internal contradiction: Context section flipped to Option (ii) feasible at 57ae434 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>
…ibutable lines (resolve codex #2 consistency)

codex BLOCKING #2 on PR #1929 sha 812602b 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>
…on 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>

@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: 9f890f5b · Trigger: schedule
  • Thinking: 41s wall

✅ The provided diff is empty, so there are no changed lines to review.

…ector ack at #4393616097 (avoids std.types::Platform OS-identity collision)
@briansrls
briansrls marked this pull request as ready for review May 7, 2026 02:08
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

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

Findings

  • docs/briefs/r3-substrate-int-platform-uint-platform-worker.md:4 (NON-BLOCKING) — After renaming the algebra to MachineWidth<PointerWidth>, the same ratification sentence still says “with Platform as substrate token.” That mixes two labels for the nominal carrier unless “Platform” is explicitly defined as the axis and PointerWidth as the token (the sentence does not say that). Touches docs/modeling-discipline.md Practice 5 (single-authority metadata) / naming clarity more than a live invariant in compiler code.

Verdict

APPROVE_WITH_COMMENTS — origin/main...HEAD only changes this worker brief (no Rust/substrate/code paths). Nothing here violates fail-closed, substrate modeling in code, or test discipline because those surfaces are untouched. Consider tightening line 4 (and, if you want full consistency, the unchanged “substrate-token Platform” cross-refs and Option α/β spellings) so the brief names one substrate token consistently end-to-end.

Exploratory observations (optional)

  • Several passages still say Platform where Deliverable 1 is now PointerWidth (e.g. Options α–β, “Platform type-parameter,” provenance). Only :4 was edited in the same breath as the PointerWidth rename; the rest is pre-existing drift that may merit a quick editorial pass in a follow-up if the intent is a single canonical token name.

@briansrls

Copy link
Copy Markdown
Contributor Author

cursor NON-BLOCKING — addressed in 49bb141

Residual Platform refs cleaned up: line 4 ratification sentence + Options α/β type-decl spellings + 'Platform type-parameter' / 'sibling-shape' / 'substrate-token Platform' phrasings. Brief now consistently names PointerWidth end-to-end (excluding outer carrier names IntPlatform/UIntPlatform per Q1 verbatim, PlatformDependentFact existing carrier, and T-Platform-Integer cluster-naming option which is bikeshed-not-token).

— sent from quick-crab-830

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 49bb1410 · Trigger: schedule
  • Comparison: origin/main @ fd1a65ab ... review/pr-1931-49bb1410 @ 49bb1410
  • Thinking: 15s wall

APPROVE — pure documentation rename within a single pre-authored worker brief: Platform → PointerWidth to avoid colliding with the existing std.types::Platform OS-identity carrier. The rename is applied consistently across header, deliverables, options α/β/γ, acceptance, STOP triggers, DFS pre-flight, and cross-references; no code/substrate is touched. Naming change is well-motivated (collision avoidance) and is the correct discipline — distinct concepts get distinct tokens. No invariant, modeling, coding, or testing concerns in this diff.

@briansrls
briansrls merged commit fa9e81d into main May 7, 2026
4 checks passed
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 49bb1410 · Trigger: manual
  • Conversation: View conversation

1. Story of the diff

This PR is a brief-only substrate planning update for the future IntPlatform / UIntPlatform worker. The key change is that the proposed machine-width parameter is no longer named Platform; it is renamed to PointerWidth, while the brief explicitly preserves the existing std.types::Platform = Linux | Macos | Windows OS-identity carrier as a separate concept at docs/briefs/r3-substrate-int-platform-uint-platform-worker.md:4. The intended substrate shape becomes Compose<Int, MachineWidth<PointerWidth>> / Compose<UInt, MachineWidth<PointerWidth>>, with follow-on worker acceptance still covering the token, integer aliases, Rust isize/usize rows, ratchets, and bootstrap/parse-corpus receipts.

2. Invariant categories

  1. LAYER MODEL — Compliant with one caveat surfaced below. The diff is documentation/brief text rather than landed .dag substrate or Dag mutation, but it is still directing future substrate work. The rename itself respects layer separation: docs/briefs/r3-substrate-int-platform-uint-platform-worker.md:4 makes PointerWidth the inner substrate token and explicitly leaves the pre-existing OS Platform carrier untouched.
  2. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING. docs/briefs/r3-substrate-int-platform-uint-platform-worker.md:48 leaves a dispatch path for a new substrate coproduct: type PointerWidth = Pointer | TargetSpecific(String). The only Practice 4 note in the diff is docs/briefs/r3-substrate-int-platform-uint-platform-worker.md:65, which says classification is N/A because the IntPlatform / UIntPlatform aliases are not coproducts; it does not classify the possible PointerWidth sum type itself. Principle: coproduct dissolution / illegal states unrepresentable / API-level enforcement. If option α remains, the brief should require the worker to land a GREEN/YELLOW/RED coproduct classification for PointerWidth, and TargetSpecific(String) should be replaced or bounded by a typed target-spec authority rather than free-form string identity.
  3. CODING.md — N/A. The diff does not add or modify Rust implementation code; no data/function shape, Result/error carrier, helper placement, or method-style issue is introduced here.
  4. TESTING.md — N/A. The diff is a pre-authored brief rename and does not change executable compiler behavior. No test is required for this PR itself; the future worker brief still names implementation receipts such as bootstrap snapshot, parse corpus manifest, and integer-row ratchet updates.
  5. LOCKED DESIGN DECISIONS — Compliant. The diff keeps the Q-MachineConstraint shape aligned with the locked Compose<Algebra, MachineWidth<N>> framing while changing only the chosen token name: docs/briefs/r3-substrate-int-platform-uint-platform-worker.md:147 now says the brief extends N with substrate-token PointerWidth.
  6. TRACKED vs UNTRACKED DEBT — Finding, same blocking issue as above. The α branch at docs/briefs/r3-substrate-int-platform-uint-platform-worker.md:48 is an untracked substrate-shape branch if chosen: it names a possible new sum type but does not provide documentation, bounds, and a named dissolution/terminal-classification trigger for that coproduct. The line at docs/briefs/r3-substrate-int-platform-uint-platform-worker.md:52 narrows α to cases with “structural meaning,” but that is not a ledger entry or dissolution trigger.

3. Verdict

REQUEST_CHANGES. The rename from Platform to PointerWidth is directionally clean, but the brief still allows a future substrate worker to choose an unclassified sum-type token with a stringly TargetSpecific payload. Since this is substrate-authoring guidance, fixing the brief before dispatch is cheaper and safer than relying on the next PR to infer the missing modeling gate.

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