Skip to content

R3 gate #20: numeric inherited bake ins dissolved - #2673

Closed
briansrls wants to merge 1 commit into
mainfrom
session/zesty-lynx-761
Closed

briansrls wants to merge 1 commit into
mainfrom
session/zesty-lynx-761

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session zesty-lynx-761.
Pushing to session/zesty-lynx-761 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

@briansrls
briansrls marked this pull request as ready for review May 11, 2026 04:44
@briansrls

Copy link
Copy Markdown
Contributor Author

Response to codex review (review 9308 / stdout artifact) — Re-verified on the PR branch: docs/r3-program-plan.md §1.8 row #20 (numeric_inherited_bake_ins_dissolved) remains the single canonical ledger row; the Status at HEAD paragraph and the PM compile note (T-Numeric-Construction bullet) only mirror that row and cite the same consumer (numeric_inherited_bake_ins_dissolved_int_inherited_aliases_use_abstract_int in m2_substrate_inhabitance_test.rs) plus producer cites in dsl/std/types.dag. No thesis / invariant / coding / testing doc violations found; no additional code commit warranted.

Merge readiness note: waiting on v3 CI job green and on second dashboard/API-style approval per merge policy (codex artifact is APPROVE in prose but dashboard currently classifies verdict as unknown — operators should confirm the two-approval bar against live review state).

— sent from zesty-lynx-761

@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: d28a7ec3 · Trigger: schedule
  • Thinking: 137s wall

BLOCKING (1)

Root Cause

  • docs/r3-program-plan.md Gate #20 status promotion treats a hand-written integration ratchet as generated P2 evidence → either land/cite a generated consumer proof or keep #20 DECLARED while listing the Rust test as non-closure evidence.

⚠️ The producer declarations look aligned, but the canonical ledger cannot mark this substrate gate passing on hand-written ratchet evidence alone.

Comment thread docs/r3-program-plan.md
| 18 | `numeric_width_refinements_landed` | substrate-shape | T-Numeric-Construction | **CONSUMER_LANDED + PASSING for Grounding G2 primitive rows** (2026-05-10, PR #2570 squash `b96a51a2`). Producer-side substrate: Int<N> arm via `IntW32/64/128 = Compose<Int, MachineWidth<WordN>>` at `dsl/std/integer.dag:93-95` (PR #2161); Nat<N> arm via `UIntW32/64/128` at `dsl/std/integer.dag:96-98` + `UInt = Nat` axiom at `dsl/std/integer.dag:148`; Float/Real arm via `Float32/Float64 = Compose<Ieee754Float, MachineWidth<Word32|Word64>>` and `Real = ApproximateField<FieldOfFractions<Int>>` in `dsl/std/float.dag`. Consumer evidence: Rust `f32`/`f64` rows in `dsl/extdeps/languages/rust/primitives.dag`, `grounding_pilot` mirror routing, and `grounding_engine` full-list validation over loaded `rust_pilot_primitives`. | `Int<N>` / `Nat<N>` / `Real<N>` width-refinement surface has Grounding G2 primitive-row consumer evidence; broader Real<N> emission demonstrations remain under S9/Shape-A follow-ons. |
| 19 | `numeric_aliases_align_to_refinements` | substrate-shape | T-Numeric-Construction | DECLARED | Int8/.../Int128 as refinements |
| 20 | `numeric_inherited_bake_ins_dissolved` | substrate-shape | T-Numeric-Construction | DECLARED | Char/EpochMs/Duration consume abstract Int |
| 20 | `numeric_inherited_bake_ins_dissolved` | substrate-shape | T-Numeric-Construction | **CONSUMER_LANDED + PASSING** | Producer: `Char` / `EpochMs` / `Duration` / `Milliseconds` / `Seconds` at `dsl/std/types.dag:193-303` refine abstract `Int` (`unicode_scalar`, `range(min: 0)`, `brand` where-clauses). Consumer: integration `numeric_inherited_bake_ins_dissolved_int_inherited_aliases_use_abstract_int` (`m2_substrate_inhabitance_test.rs`) pins each `dsl/std/types.dag` declaration’s resolved structural base to `Int` with non-empty `Declaration.refinement` (no parallel fixed-width integer defining carrier). |

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: Gate #20 is a substrate-shape gate, but the new CONSUMER_LANDED + PASSING claim cites only the hand-written Rust integration test numeric_inherited_bake_ins_dissolved_int_inherited_aliases_use_abstract_int; INVARIANTS P2 and §1.7 require generated consumer proof for substrate boundary progress.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-thinking
  • Commit: d28a7ec3 · Trigger: manual
  • Comparison: main @ 2bcac69f ... session/zesty-lynx-761 @ d28a7ec3
  • Conversation: View conversation

1. Story of the diff

This PR is a status-promotion/doc-sync change in docs/r3-program-plan.md. It promotes R3 §1.8 gate #20, numeric_inherited_bake_ins_dissolved, from DECLARED to CONSUMER_LANDED + PASSING, then threads that promotion through the status-at-HEAD paragraph, the T-Numeric-Construction lane row, and the PM compile note. The mechanism claimed is not a new substrate declaration in this diff, but an existing producer/consumer receipt: Char, EpochMs, Duration, Milliseconds, and Seconds are said to refine abstract Int, and the proof is said to be the integration test numeric_inherited_bake_ins_dissolved_int_inherited_aliases_use_abstract_int in m2_substrate_inhabitance_test.rs at docs/r3-program-plan.md:246.

The load-bearing issue is that this same document defines CONSUMER_LANDED for substrate boundary gates as requiring a generated consumer proof, and explicitly says a hand-written integration ratchet alone does not claim the §P2 landed state at docs/r3-program-plan.md:142. The new #20 row appears to promote based on a Rust integration ratchet, so the status update overstates the gate’s maturity.

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

Finding — BLOCKING. docs/r3-program-plan.md:246 marks gate #20, a substrate-shape gate, as CONSUMER_LANDED + PASSING while naming the consumer as integration m2_substrate_inhabitance_test.rs. But the document’s own layer/status rule says substrate boundary discipline counts as landed only when “declaration + realization + generated consumer proof exist,” and that “a hand-written integration ratchet alone” does not claim §P2 landed status at docs/r3-program-plan.md:142. This is a layer-status mismatch: the diff promotes substrate boundary completion without the generated-consumer bar it says is required.

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

Finding — BLOCKING. Boundary Discipline / single authority is violated by the status semantics: docs/r3-program-plan.md:144 says numeric_inherited_bake_ins_dissolved is CONSUMER_LANDED + PASSING per m2_substrate_inhabitance_test.rs, and docs/r3-program-plan.md:246 repeats that the consumer is an integration ratchet. Since docs/r3-program-plan.md:142 reserves CONSUMER_LANDED for the generated bar, this creates parallel meanings for the same status label: generated consumer proof for #17, integration ratchet for #20.

  1. CODING.md.

N/A — diff is documentation/status ledger only; no Rust implementation style, function shape, error type, helper placement, or API surface changes.

  1. TESTING.md.

Finding — BLOCKING for the status claim, not for test existence. The diff does not add or modify a test; it changes the gate status based on an existing test. The problem is that docs/r3-program-plan.md:246 uses an integration test receipt as the basis for CONSUMER_LANDED + PASSING, while the same ledger distinguishes hand-written ratchets from generated consumer proof at docs/r3-program-plan.md:142. The test may be a good DECLARED/ratchet receipt, but this diff should not classify it as generated-consumer landing unless that generated consumer exists and is cited.

  1. LOCKED DESIGN DECISIONS.

Compliant. The diff does not alter the locked Pure Bootstrap zero-floor target, substrate shape, or thesis-level numeric construction target; it only updates R3 gate-status prose. The issue is status overclaiming, not a direct locked-design rewrite.

  1. TRACKED vs UNTRACKED DEBT.

Finding — BLOCKING. docs/r3-program-plan.md:424 removes #20 from the remaining DECLARED/in-flight work and says only #17 remains declared. If #20 still lacks the generated consumer required by docs/r3-program-plan.md:142, this converts remaining work into invisible debt: the missing generated-consumer proof is no longer tracked as a remaining gap, and no dissolution trigger or lane is named for closing it.

2.5. Top-down PM intent review

Finding — BLOCKING. PM-level intent in this program plan is that R3 close criteria require runtime-executable, consumer-landed verification rather than document-level claims: docs/r3-program-plan.md:146 says declarations alone do not satisfy R3 close criteria and closure requires runtime-executable verification. More specifically, the same local authority defines CONSUMER_LANDED for substrate boundary gates as generated-consumer proof, not a hand-written integration ratchet, at docs/r3-program-plan.md:142.

The diff dilutes that intent by promoting #20 to CONSUMER_LANDED + PASSING while citing only m2_substrate_inhabitance_test.rs as the consumer at docs/r3-program-plan.md:246, then propagating that closure into the lane row at docs/r3-program-plan.md:424 and PM compile note at docs/r3-program-plan.md:441. A worker following this faithfully would stop looking for the generated consumer proof for #20, even though the plan’s own status semantics say that is the required bar.

3. Verdict

REQUEST_CHANGES. The PR’s only substantive move is a gate-status promotion, and the cited evidence does not satisfy the document’s own CONSUMER_LANDED definition for substrate boundary gates. Keep #20 DECLARED or reword it as an integration ratchet/receipt until a generated consumer proof exists and is cited.

@briansrls briansrls closed this May 11, 2026
@briansrls
briansrls deleted the session/zesty-lynx-761 branch June 1, 2026 18:43
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