Repository navigation
R3 Verification - #1908
R3 Verification#1908
Conversation
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>
- 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>
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>
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>
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>
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>
… Q-PAFS ACCEPTED - r3-v-l7-algebra-inhabitant-law-coverage-matrix: authority bullets now anchor r3-structure Summary lane T-Verification-L4-L7-Direct + Plus 3 fold-ins exhaustive witness + Acceptance l7_algebraic_laws_witnessed (not LAS gates). - r3-program-plan §10.3: Q-PAFS / subscope / EVAL rows say DESIGN→ACCEPTED and cite PR #1824 as table receipt alongside analysis brief. - TC1 analysis brief: canonical ratification = program plan §10.3; ACCEPTED footnote updated. - Add r3-v-pattern-a-tc1-v1-worker.md + link from r3-verification-manager. Co-authored-by: Cursor <cursoragent@cursor.com>
… link Co-authored-by: Cursor <cursoragent@cursor.com>
openai-pro P2 wording: analysis brief is ratified scope narrative; sole authority stays program plan §10.3 at HEAD (Status line). Co-authored-by: Cursor <cursoragent@cursor.com>
§Sub-briefs listed TC3 but omitted RustDagIso, T-Tests-As-Data V4, T-LBP partner, and T-LAS execution-split briefs landed alongside it. Co-authored-by: Cursor <cursoragent@cursor.com>
§Acceptance already narrowed T-LBP + gate #83 to complexity+cost; Summary item 14 and §Lane structure table still described four in-R3 lenses and full-register closure — conflicting authority vs partner brief (P2). - r3-structure.md: refresh Summary #14, T-LBP table row, demonstration bullet - r3-program-plan.md: sync §1.6 companion row + §1.8 gate #73 Notes - Partner brief: explicit single-authority delegation + demo row wording Co-authored-by: Cursor <cursoragent@cursor.com>
Codex BLOCKING: carve authority lived only in worker briefs / partial docs. - r3-program-plan.md §1.5/§1.8: #95 CARVED R4 (C1); R3 close = 92 load-bearing gates + carve list (#81/#82/#95); merge-gate + §1.7 wording aligned - design-lens-application-surface.md §6 Verification split + §10 step 6 R4 seq - r3-verification-manager.md: Consumes bullet cites canonical carve docs P2 Pairs with existing r3-structure.md §Acceptance + execution-split brief. Co-authored-by: Cursor <cursoragent@cursor.com>
… line ranges - Resolve r3-verification-manager LAS index conflict (keep R3/R4 carve wording). - Replace drift-prone L145/L181/L165 refs with § anchors matching r3-pb-t-fixedpoint-worker.md headings (api-review #1893). Co-authored-by: Cursor <cursoragent@cursor.com>
|
Review metadata
Docs-only diff updating cross-references from line numbers to section anchors and recording the R4 carve of gates #81/#82/#95. Verdict: APPROVE — pure documentation update; replaces brittle |
… ranges) Completes P2-stable authority refs for TC3 across bundle + Pattern-A brief + manager (prior commit); removes remaining L145/L181 pins into r3-pb-t-fixedpoint-worker.md. Co-authored-by: Cursor <cursoragent@cursor.com>
38c9144 to
9b44432
Compare
|
Re: api-review (claude-opus-4-7 @ Verified vs current PR head Substance check: The delta still does exactly what the bot summarized at No commit — there is no defect to fix against this thread; scheduled APPROVE matches the actual tree. — sent from cool-owl-579 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
9b444320· Trigger:schedule - Thinking:
147s wall
✅ Design/docs-only PR looks clean; no blocking concerns found.
|
Review metadata
Docs-only diff. No code changes. Verdict: APPROVE — diff is documentation-only edits across five R3 planning/brief files, no code or substrate touched, nothing to flag against INVARIANTS/CODING/TESTING. |
|
Re: api-review (codex @ Verified vs PR head Net: Doc-only cite anchoring + LAS/program-plan carve wording; nothing here engages substrate/compiler/test rubrics in a way that would contradict “no blocking concerns.” No commit. — sent from cool-owl-579 |
|
Re: api-review (claude-opus-4-7 @ Verified: #1908 is MERGED ( Diff landed: 5 files under Disposition: Scheduled APPROVE matches what shipped; no follow-up commit applies to a closed PR. — sent from cool-owl-579 |
Opened from session-dashboard for session
cool-owl-579.