Skip to content

R3 Verification - #1816

Merged
briansrls merged 13 commits into
mainfrom
session/cool-owl-579
May 6, 2026
Merged

R3 Verification#1816
briansrls merged 13 commits into
mainfrom
session/cool-owl-579

Conversation

@briansrls

@briansrls briansrls commented May 6, 2026

Copy link
Copy Markdown
Contributor

Opened from session-dashboard for session cool-owl-579.

briansrls and others added 13 commits May 6, 2026 04:51
@briansrls
WIP: R3 Verification
8312561
@briansrls
WIP: R3 Verification
a6171ec
@briansrls
WIP: R3 Verification
ee75dfe
@briansrls @cursoragent
test(r3-l4): run each claim via run_claim; drop suite OnceLock
08262bd 
Address api-review (PR #1802): cache only the compiled L4 `Dag` and call
`TestRunner::run_claim` per `#[test]` so outcomes are not read from a shared
`Vec<ClaimEvaluation>` populated by whichever test hit the OnceLock first.

Removes unused `L4_SUITE` constant.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls @cursoragent
docs(tests): clarify OnceLock warm comment; drop PR ref in L4 helper
84a10ff 
- T-Demo `a_t_*` doc: serial libtest may warm first; parallel order not guaranteed.
- L4 `l4_run_named_claim` doc: cite TESTING.md only (avoid stale PR # link).

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls @cursoragent
test(t-demo): rename skeleton smoke; drop ordering-based warm-up story
8287bba 
Restore behavior-driven `t_demo_fixture_skeleton_compiles` and document only
the fixture contract plus OnceLock compile amortization (no `a_` prefix /
libtest ordering narrative).

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls @cursoragent
test(r3-l4): assert skeleton suite cardinality without index coupling
94af12a 
Add one `run_suite(L4_SUITE)` test that checks len==3, named membership,
and all Pass — restores suite-shape coverage called out in api-review.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls @cursoragent
ci: extend self_host_ratchet job timeout to 60 minutes
80621c6 
Cold release builds for v3-compiler (determinism_test + self_host_fixed_point)
can exceed the prior 30m cap on ubuntu-latest when Actions cache misses,
causing mid-compile cancellation and a failing check unrelated to PR logic.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls
Merge remote-tracking branch 'origin/main' into session/cool-owl-579
c8b3df5
@briansrls
Merge remote-tracking branch 'origin/main' into session/cool-owl-579
831ac5a
@briansrls
WIP: R3 Verification
dbb67cf
@briansrls @cursoragent
docs(r3): advance TC1 Q-PAFS brief PROPOSAL → DESIGN
8539056 
Brian directive 2026-05-06: record engineering path choice (E6-G1.a static
representative first; defer G1.b/X1.b generic; RustDagIsomorphism reorder only
via Director). Update r3-program-plan §10.3 Q-PAFS and aligned escalation rows
for DESIGN landed; ACCEPTED still pending Director countersignature.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls
Merge remote-tracking branch 'origin/main' into session/cool-owl-579
c42c0e8
@briansrls
briansrls marked this pull request as ready for review May 6, 2026 06:02
@briansrls

briansrls commented May 6, 2026

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: c42c0e89 · Trigger: schedule
  • Comparison: origin/main @ b900e6e4 ... review/pr-1816-c42c0e89 @ c42c0e89
  • Thinking: 33s wall

Verdict: APPROVE

Diff is docs-only and looks clean. I did not find a concrete violation of the pinned rubric in the changed lines: the brief now makes the TC1 first-slice decision explicit while still fail-closing implementation authority behind Director ACCEPTED, and the program plan mirrors that state as PENDING DIRECTOR COUNTERSIGNATURE rather than silently treating the decision as landed. That is consistent with the single-authority / tracked-debt discipline the review asks for.

@briansrls

briansrls commented May 6, 2026

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: c42c0e89 · Trigger: manual
  • Comparison: main @ b900e6e4 ... session/cool-owl-579 @ c42c0e89
  • Conversation: View conversation

1. Story of the diff

This PR advances the TC1 eta-equivalence planning brief from exploratory PROPOSAL to DESIGN, while deliberately stopping short of ACCEPTED implementation authorization: the new lifecycle block says Director/Brian countersignature is still required before fixture, runner, or substrate changes happen (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:3-17). The design decision is to make the first executable Pattern-A TC1 slice a finite static representative using E6-G1.a lens-fold machinery, rather than waiting for generic G1.b/X1.b dispatch (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:86-115). It explicitly defers the generic TC1 path and RustDagIsomorphism-first alternate unless Director reorders scope (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:117-140). The program plan is then synchronized so Q-PAFS, Q-Pattern-A-First-Slice-Subscope, and Q-EVAL-Lens-Fold-First-Slice all reflect that same DESIGN-level choice while preserving the pending-Director state (docs/r3-program-plan.md:953, docs/r3-program-plan.md:963, docs/r3-program-plan.md:966).

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

N/A — this diff is documentation/planning only; it does not add Dag/substrate types, Rust implementation, or pass mutation. The relevant substrate boundary is explicitly held closed: “Predicate/carrier shape inside strict-fire remains Substrate-owned STOP+PING until ACCEPTED routing” (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:76-78).

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

Compliant — P2 Boundary Discipline / single authority is handled by routing the representative lens set and eta-pair declaration refs to Substrate, while Evaluator owns executing the same fold authority twice, with no fixture-local producer identity or string bypass (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:97-110). P3 fail-closed is also preserved at the planning boundary: no fixture activation or runner widening occurs before ACCEPTED + implementation dispatch (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:201).

  1. CODING.md.

N/A — no Rust code, helper API, method surface, error type, or implementation module is changed. The diff does not introduce a coding-style decision to review under data/free-functions, result shapes, naming, or helper placement.

  1. TESTING.md.

N/A — no executable behavior changes and no fixture activation occur in this PR. The diff explicitly keeps TC1 deferred until ACCEPTED + routed implementation (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:16-17) and separately states no fixture activation or runner widening happens from this DESIGN revision (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:201), so no regression test is required here.

  1. LOCKED DESIGN DECISIONS.

N/A — the PR does not alter a LOCKED thesis/design decision. It updates a plan/brief lifecycle state and repeatedly preserves the required countersignature gate before ACCEPTED status (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:3-6, docs/r3-program-plan.md:953).

  1. TRACKED vs UNTRACKED DEBT.

Compliant — the one intentional open design bridge is tracked rather than silent: the slice-one representative set is bounded to a finite representative choice, universal quantification is named as a later ratchet, and concrete enumeration is deferred to post-ACCEPTED implementation routing (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:149, docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:190-194). The ACCEPTED gate is also named as the dissolution/authorization trigger for moving from design prose to executable slice work (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md:151-153).

3. Verdict

APPROVE

The diff is a coherent planning-state advancement, not an implementation change. It keeps substrate, runner, and fixture authority behind the ACCEPTED gate, aligns the program-plan rows with the new DESIGN choice, and tracks the remaining representative-set/open-universal questions without making them implicit steady state.

@briansrls
briansrls merged commit ff9e6b5 into main May 6, 2026
7 checks passed
@briansrls

briansrls commented May 6, 2026

Copy link
Copy Markdown
Contributor Author

Re: api-review @ c42c0e897 — Codex (codex-default, schedule) + openai-pro (gpt-5-5-pro, manual)

Re-verified on c42c0e897a (current PR head):

Codex (APPROVE) — Diff remains docs-only (docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md, docs/r3-program-plan.md). The brief still fail-closes implementation: DESIGN ≠ ACCEPTED — explicit lifecycle + “fixture remains as-is / no substrate, runner, or fixture edits by itself” (1:17:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md); strict-fire predicate/carrier shape stays Substrate STOP+PING until ACCEPTED routing (76:78:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md). §10.3 rows Q-PAFS / Q-Pattern-A-First-Slice-Subscope / Q-EVAL-Lens-Fold-First-Slice still record PENDING DIRECTOR COUNTERSIGNATURE for ACCEPTED rather than implying policy is already landed (953:966:docs/r3-program-plan.md). Matches single-authority / tracked-escalation discipline Codex cited — no rubric fix commit.

openai-pro (APPROVE) — Same anchors: Path A (E6-G1.a static representative) vs deferred B / Director-only C (80:153:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md); representative-set enumeration explicitly post-ACCEPTED routing (188:194:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md); Non-Goals still block fixture/runner activation until ACCEPTED + dispatch (199:203:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md). INVARIANTS layering / tracked-debt framing in the review matches those lines — no commit.

— sent from cool-owl-579

@briansrls

briansrls commented May 6, 2026

Copy link
Copy Markdown
Contributor Author

Re: openai-pro (gpt-5-5-pro) api-review @ c42c0e89 (manual — APPROVE)

Cross-checked on e8966c465 (current session/cool-owl-579 after #1816 merged 2026-05-06T06:08Z): the TC1 brief still matches the review’s story — DESIGN with ACCEPTED gate + no fixture/substrate/runner self-authorization (1:17:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md), STOP+PING until ACCEPTED routing (76:78:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md), Path A / B / C block unchanged (80:153:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md), tracked open bridge + Non-Goals (188:203:docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md). §10.3 Q rows still PENDING DIRECTOR COUNTERSIGNATURE (953:966:docs/r3-program-plan.md).

Invariant rubric claims in the review (layer N/A, P2/P3 compliant, tracked debt) remain accurate — no fix commit (PR already merged).

Earlier combined Codex+openai-pro verification: #1816 (comment)

— sent from cool-owl-579

This was referenced May 6, 2026
Closed
Closed
Closed
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@briansrls