Repository navigation
PR-PreF: consolidate interval substrate parent - #1154
Conversation
|
Review metadata
FindingsNone. The meaningful diff adds VerdictAPPROVE — The change is narrowly scoped, matches the invariants’ “shared parent / retrofit instances” story, and the large |
|
Review metadata
1. Story of the diffThis PR introduces The PR also adds a hand-written projection from the existing 2. Invariant categories
Finding — BLOCKING.
Finding — BLOCKING.
Compliant.
Compliant. The diff adds behavior-facing coverage at the right seam:
N/A — the diff references the P1 substrate-target rationale at
Compliant for the explicit bridge; blocked by the substrate findings above. The staged 3. VerdictREQUEST_CHANGES The PR is making the right architectural move by introducing a shared bound parent and proving the runtime projection path, but the new substrate carrier currently admits invalid intervals and lacks the required coproduct classification. Because those are substrate modeling issues, they should be fixed before this shape becomes authoritative. |
6034895 to
28119ae
Compare
|
Review metadata
Reviewed Findings: None that rise to a doc-backed violation with review teeth. The new Verdict: APPROVE — Diff is scoped to introducing the shared Exploratory (optional): |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
60348956· Trigger:schedule - Thinking:
319s wall
BLOCKING (2)
Root Cause
src/v3/std/substrate.dagInterval landed as a shared substrate parent before its ordered-bound invariant and dissolution receipt were encoded → add the order/refinement witness and the 🟢/🟡/🔴 receipt, or keep existing carriers until that evidence exists.
| // domains; this parent is the substrate target named by INVARIANTS.md §P1. | ||
| // Existing carriers retrofit as instances instead of growing new sibling | ||
| // bound declarations. | ||
| type Interval<D> |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified against current head 783808f1: Interval<D> now has the required coproduct classification directly above the declaration. Current src/v3/std/substrate.dag:93-96 reads // 🟢 TERMINAL. Interval is the durable shared bound parent... No dissolution trigger..., followed by type Interval<D> at line 97. This was addressed after the reviewed stale shape; no further code change is needed for this checkpoint.
— sent from eager-ram-167
| // Existing carriers retrofit as instances instead of growing new sibling | ||
| // bound declarations. | ||
| type Interval<D> | ||
| = ExactInterval { lower: D, upper: D } |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified against current head 6551dd625: this was fixed in ab87d39e1 and regenerated in bca173c77 / 6551dd625. ExactInterval no longer exists; Interval<D> now uses BoundedInterval { lower, upper, order: IntervalOrderWitness }, and the comment above it states the endpoint pair is not complete without the witness. CardinalityBound::interval() now emits EqualEndpoints for exact bounds and OrderedEndpoints for AtMostOne, with regression coverage in m2_substrate_inhabitance_test.
— sent from eager-ram-167
|
Review metadata
FindingsNone that tie to a concrete invariant violation in the diff. The substrate change matches INVARIANTS.md P1’s DAG-ancestor procedure ( VerdictAPPROVE — Scoped substrate addition ( Exploratory observations (optional)
|
|
Review metadata
1. Story of the diffThis PR introduces 2. Invariant categories
BLOCKING — substrate illegal state remains representable. The diff touches substrate directly:
Illegal states unrepresentable / API-level enforcement. The witness is modeled as a free nullary coproduct (
The implementation projection is total and typed:
The diff adds behavior-level regression coverage for both the substrate mirror and the projection.
The diff references
The staged 3. VerdictREQUEST_CHANGES The PR’s direction is aligned with the substrate-parent story, and the generator/tests are wired cleanly, but |
|
Review metadata
Verdict: APPROVE Clean PR. Adds No findings against the diff. |
|
Review metadata
Verdict: APPROVE — Adds an Exploratory observation (non-blocking): The doc says |
|
Review metadata
Findings: None. The diff adds substrate-level Verdict: APPROVE — Scoped substrate mirror + projection + tests; no concrete rubric violations spotted in the reviewed hunks. Exploratory observation (optional): |
|
Review metadata
APPROVE — Introduces Exploratory observation (non-blocking): reusing |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
0774ea5a· Trigger:schedule - Thinking:
491s wall
Non-blocking — Strengths
src/v3/std/substrate.dagThe interval parent is documented as a durable shared bound substrate and the CardinalityBound projection is covered by a focused test.
✅ No blocking concerns in this mixed substrate/runtime mirror change.
|
Review metadata
Verdict: APPROVE The diff is narrowly scoped: it adds the Verification note: I attempted |
|
Review metadata
Findings: None. The substantive diff introduces Verdict: APPROVE — Scoped substrate + mirror + test updates; modeling notes match INVARIANTS P1 / modeling-discipline (DAG parent, terminal coproduct classification). No diff-grounded violations of the pinned rubric. |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
ddc31fd7· Trigger:schedule - Thinking:
176s wall
Non-blocking — Strengths
src/v3/std/substrate.dagThe interval substrate is grounded as a shared parent for existing bound carriers and keeps the CardinalityBound projection as an instance rather than a sibling representation.src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rsThe new runtime mirror shapes and CardinalityBound-to-Interval projection are covered by focused inhabitance tests.
✅ No blocking concerns in this mixed substrate/runtime mirror update.
|
Review metadata
Findings (if any): Verdict: APPROVE — The diff is coherent and narrowly focused: a substrate-level interval parent, Rust mirrors + projections, spec realizations, and tests/ratchets. No policy violations grounded in the diff. |
|
Review metadata
Findings: None. The hand-authored diff adds Verdict: APPROVE — The change is focused, models the shared parent as substrate facts plus a small Rust projection, includes terminal coproduct documentation and tests; no principled issues grounded in this diff. |
|
Review metadata
Findings: None. The diff adds substrate parents and projections with explicit terminal classification, documents the P1 “shared parent” rationale, keeps bounded intervals as lower + nonnegative width (illegal inverted ranges not representable), wires regen/spec mirrors, and extends Verdict: APPROVE — Scoped modeling step: new Exploratory (optional): Substrate prose refers to projecting through |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
0fd716bd· Trigger:schedule - Thinking:
257s wall
✅ No blocking concerns in this mixed substrate/runtime mirror update.
53dab51 to
9b62f6f
Compare
|
Review metadata
Verdict: APPROVE — small, well-scoped substrate consolidation. Adds Exploratory observation (non-blocking): |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
53dab518· Trigger:schedule - Thinking:
289s wall
Non-blocking — Strengths
src/v3/std/substrate.dagThe shared interval parent is mirrored through the generated Rust carriers and covered by runtime-shape and projection tests.
✅ No blocking concerns in this mixed substrate/runtime mirror update.
|
Review metadata
1. Story of the diffThis PR introduces 2. Invariant categories
Finding — BLOCKING. This is substrate, not implementation-only:
Finding — BLOCKING. This violates illegal-states-unrepresentable / fail-closed modeling discipline: the authoritative carrier line
Compliant. The Rust implementation work is small and explicit:
Compliant for the behavior that actually landed, but not sufficient to rescue the substrate issue above. The diff adds reflection-shape coverage for both new coproducts at
N/A — no locked thesis/design decision is altered in the diff. The only explicit design-rule reference I see is the substrate comment pointing to
Finding — BLOCKING as part of the same substrate issue. The diff names a future enforcement seam — “typed constructors / reconciliation” at 3. VerdictREQUEST_CHANGES. The generated mirrors, target realizations, and |
Summary
IntervalWidth, neutralPositiveIntervalWidth, andInterval<D>substrate declarations for PR-PreF bound consolidation.Dag::new()exposes the interval declarations.CardinalityBound::interval()plus Rust/Go type realizations and focused inhabitance coverage.Local verification
python3 scripts/regen_runtime_mirrors.py --checkcargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verifycargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored --nocapturecargo test -p v3-compiler --test integration m2_substrate_inhabitance_test -- --nocapturecargo test -p v3-compiler --test integration handwritten_parse_snapshot_matches_manifest -- --nocapture