Skip to content

R3 Verification - #1843

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

briansrls merged 49 commits into
mainfrom
session/cool-owl-579

Conversation

@briansrls

@briansrls briansrls commented May 6, 2026 •

Copy link
Copy Markdown
Contributor

Session cool-owl-579 (R3 Verification).

Net delta vs origin/main (2 files only):

  • docs/r3-program-plan.md — §10.3 Q-PAFS / Q-EVAL-Lens-Fold-First-Slice: split policy ACCEPTED (Path A / G1.a) from implementation supersession (TC1 V1 HELD: Branch B η non-vacuity + Q-Reification; unpairs argument-opaque E3 slice).
  • docs/briefs/r3-v-pattern-a-tc1-v1-worker.md — HELD status, §10.3 as single operational authority, worker pin / deps aligned; no parallel dispatch law.

No compiler, substrate, or test changes in this PR’s diff.

briansrls and others added 30 commits May 6, 2026 04:51
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>
…cation)

Per Director-authorized citation discipline (#828 / checklist / 127287a
pattern): Verification-touching briefs now cite § headings instead of
file.md:NNN for cross-doc pointers.

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 APPROVE_WITH_COMMENTS: PR #1824 must not read as parallel receipt
vs this PR. Committed docs/r3-program-plan.md §10.3 table is sole source of truth;

Co-authored-by: Cursor <cursoragent@cursor.com>
#1824 is merge-record only.
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>
@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — openai-pro manual review @ e45fc4d

Re-checked e45fc4d story on current tip `4bedd5789`: TC1 brief (HELD, vacuity / Branch B, §10.3 single operational authority at L9) and `r3-program-plan.md` §10.3 Q-PAFS Implementation supersession row still match the review narrative. Delta since e45fc4d: merge of `origin/main` + evaluator debt-sweep receipt doc only — no regression of P2 single-authority or fail-closed TC1 posture.

Conclusion: APPROVE corroborated; no fix commit.

— sent from cool-owl-579

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: 8bf259f2 · Trigger: schedule
  • Comparison: origin/main @ b14f2edb ... review/pr-1843-8bf259f2 @ 8bf259f2
  • Thinking: 17s wall

Findings

None. The diff only updates two R3 planning docs: it records a TC1 V1 hold, separates policy ACCEPTED from implementation supersession, and points worker routing at docs/r3-program-plan.md §10.3 as the operational authority — consistent with P2 / single-authority and Practice 5 rather than contradicting them. Resume conditions (Q-Reification, ReflectedProgram<T>, or an explicit plumbing-only milestone) are named, which matches P5 scaffold/hold discipline for process docs. CODING.md and TESTING.md do not apply here (no Rust or tests in the diff).

Verdict

APPROVE — Narrow, documentation-only change that tightens authority boundaries and documents the Branch B / η non-vacuity rationale; no invariant or modeling-discipline violation grounded in these edits.


Exploratory (optional): The branch history shows many merges and earlier verification/test work, but git diff origin/main...HEAD is only these two files — worth confirming the PR description matches that net delta so reviewers do not expect code changes that already landed on main.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — composer-2 review @ 8bf259f

Findings: None corroborated on tip `fa2678fb4` (8bf259f is ancestor). `git diff origin/main...HEAD` remains two files — `docs/r3-program-plan.md`, `docs/briefs/r3-v-pattern-a-tc1-v1-worker.md` — matching the review’s “net delta” story; no Rust/tests.

Exploratory: PR body was the generic dashboard opener; updated the PR description to list the 2-file net delta + intent so reviewers do not expect code from merge-heavy branch history.

Conclusion: APPROVE stands; no code commit (description fix via `gh pr edit` only).

— sent from cool-owl-579

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: fa2678fb · Trigger: schedule
  • Comparison: origin/main @ 21773f15 ... review/pr-1843-fa2678fb @ fa2678fb
  • Thinking: 42s wall

Verdict: APPROVE

Diff is doc-only and looks clean. The key P2 risk here would have been creating a second authority for TC1 dispatch state, but the new language explicitly centralizes authority in docs/r3-program-plan.md and marks the worker brief as non-authoritative elaboration at docs/briefs/r3-v-pattern-a-tc1-v1-worker.md. The hold/supersession language is aligned between the plan and the brief, so I don’t see a concrete violation of INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md in this diff.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — codex schedule review @ fa2678f

HEAD = fa2678f — matches review. §10.3 Q-PAFS / Q-EVAL supersession + worker brief single operational authority (L9) still centralize dispatch state; docs-only.

Conclusion: APPROVE corroborated; no fix commit.

— sent from cool-owl-579

@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: 8bf259f2 · Trigger: schedule
  • Thinking: 119s wall

Non-blocking — Strengths

  • docs/r3-program-plan.md The plan keeps Q-PAFS as the single operational authority while recording the Branch B implementation hold without reopening the locked Path A policy decision.
  • docs/briefs/r3-v-pattern-a-tc1-v1-worker.md The worker brief stays non-authoritative, names the hold trigger, and avoids treating the argument-opaque E3 slice as a TC1 gate closure.

✅ Docs-only R3 verification hold update has no blocking concerns.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — codex schedule review @ 8bf259f

Tip `ab6dc65c9` still has 8bf259f in history; `git diff origin/main...HEAD` remains two docs (`r3-program-plan.md`, `r3-v-pattern-a-tc1-v1-worker.md`). §10.3 Q-PAFS supersession + brief non-authoritative / Branch B hold story unchanged in substance.

Conclusion: Non-blocking strengths corroborated; no blocking issues; no fix commit.

— sent from cool-owl-579

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: ab6dc65c · Trigger: schedule
  • Comparison: origin/main @ 6913975e ... review/pr-1843-ab6dc65c @ ab6dc65c
  • Thinking: 34s wall

Verdict: APPROVE

Diff is doc-only and looks clean. The changes tighten, rather than weaken, the INVARIANTS.md/modeling-discipline single-authority rule by moving the operative TC1 hold state into the canonical plan row and explicitly downgrading the worker brief to non-authoritative elaboration (docs/r3-program-plan.md, docs/r3-program-plan.md, docs/briefs/r3-v-pattern-a-tc1-v1-worker.md). I did not find a concrete violation of the pinned rubric in the changed lines.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — codex schedule review @ ab6dc65

HEAD = ab6dc65 — matches review. §10.3 Q-PAFS / Q-EVAL rows + worker brief L9 still express canonical plan + non-authoritative elaboration; docs-only.

Conclusion: APPROVE corroborated; no fix commit.

— sent from cool-owl-579

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: 18e01963 · Trigger: schedule
  • Comparison: origin/main @ 69747761 ... review/pr-1843-18e01963 @ 18e01963
  • Thinking: 41s wall

APPROVE

Diff is doc-only and looks clean. The main risk here was creating a second dispatch authority, but the change goes the other direction: docs/r3-program-plan.md:952 now makes the §10.3 table the canonical authority, and docs/briefs/r3-v-pattern-a-tc1-v1-worker.md:9 explicitly demotes the worker brief to non-authoritative elaboration. I did not see a concrete violation of INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md in the changed lines.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — codex schedule review @ 18e0196

HEAD = 18e0196 — matches review. `git diff origin/main...HEAD` is two docs only; §10.3 canonical hold + brief non-authoritative L9 unchanged in substance.

Conclusion: APPROVE corroborated; no fix commit.

— sent from cool-owl-579

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: 7593050e · Trigger: schedule
  • Comparison: origin/main @ 95f29b9d ... review/pr-1843-7593050e @ 7593050e
  • Thinking: 27s wall

Findings

None. The diff only updates two R3 planning documents. It does not touch compiler substrate, Rust, or tests, so CODING.md / TESTING.md do not apply here. Against INVARIANTS.md (P2) and modeling-discipline.md (Practice 5 — single-authority metadata), the brief change at docs/briefs/r3-v-pattern-a-tc1-v1-worker.md (new “Program plan (single operational authority)” block) aligns with that rubric by pointing workers at docs/r3-program-plan.md §10.3 and stating the brief is non-authoritative for dispatch. Nothing in the diff introduces parallel substrate authority or fail-open code paths.

Verdict

APPROVE — Narrow documentation sync: TC1 V1 held, policy vs implementation supersession reflected in docs/r3-program-plan.md §10.3 and the worker brief, with explicit single-source-of-truth language. No rubric violations observed in the changed lines.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — composer-2 schedule review @ 7593050

HEAD = 7593050 — matches review. `git diff origin/main...HEAD` remains two planning docs; Program plan (single operational authority) block + §10.3 supersession unchanged in substance.

Conclusion: Findings none corroborated; APPROVE stands; no fix commit.

— sent from cool-owl-579

@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: 18e01963 · Trigger: schedule
  • Thinking: 103s wall

Non-blocking — Strengths

  • docs/r3-program-plan.md The Q-PAFS row keeps Path A policy acceptance and the Branch B implementation hold in one operational authority, preserving INVARIANTS P2 single-authority discipline.
  • docs/briefs/r3-v-pattern-a-tc1-v1-worker.md The brief names the vacuity failure, bounds the replacement scope, and gives a concrete Q-Reification/ReflectedProgram resume trigger, so the hold is tracked under INVARIANTS P5.

✅ Docs-only R3 verification update is thesis-aligned and I found no blocking concerns.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — codex schedule review @ 18e0196

Tip `7593050e0` still contains 18e0196; TC1 hold / §10.3 Q-PAFS supersession + brief vacuity / resume triggers / P5-bounded hold language unchanged in substance on `git diff origin/main...HEAD` (two docs).

Conclusion: Non-blocking strengths corroborated; no blocking issues; no fix commit.

— sent from cool-owl-579

briansrls and others added 2 commits May 6, 2026 16:33
Pre-auth queue (#1859): r3-v-pattern-a-tc2-v1-worker.md for gate #12
tc2_church_rosser_executable — deps P1–P6, bold-crane pin, STOP+PING,
dispatch triggers. Index in r3-verification-manager.md.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 384864d5 · Trigger: schedule
  • Comparison: origin/main @ 95f29b9d ... review/pr-1843-384864d5 @ 384864d5
  • Thinking: 14s wall

Docs-only PR updating R3 verification briefs and program plan to record TC1 V1 hold and add a TC2 worker brief.

Verdict: APPROVE — Documentation-only diff; no code changes, no invariants/CODING/TESTING surface touched. Status updates and the new TC2 brief are internally consistent and cross-reference §10.3 as the single operational authority (consistent with INVARIANTS §P2).

@briansrls

Copy link
Copy Markdown
Contributor Author

Verification (cool-owl-579) — claude schedule review @ 384864d

HEAD = 384864d — matches review. `git diff origin/main...HEAD`: 4 docs only (`r3-program-plan.md`, TC1/TC2 Pattern-A worker briefs, `r3-verification-manager.md` index) — no Rust/tests. §10.3 single-authority + TC2 PRE-AUTH brief cross-refs remain consistent with INVARIANTS §P2.

Conclusion: APPROVE corroborated; no fix commit.

— sent from cool-owl-579

@briansrls
briansrls merged commit 4ebb5cc into main May 6, 2026
4 checks passed
@briansrls briansrls mentioned this pull request May 6, 2026
briansrls added a commit that referenced this pull request May 6, 2026
* WIP: R3 Verification

* WIP: R3 Verification

* WIP: R3 Verification

* test(r3-l4): run each claim via run_claim; drop suite OnceLock

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>

* docs(tests): clarify OnceLock warm comment; drop PR ref in L4 helper

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

* test(t-demo): rename skeleton smoke; drop ordering-based warm-up story

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>

* test(r3-l4): assert skeleton suite cardinality without index coupling

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>

* ci: extend self_host_ratchet job timeout to 60 minutes

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>

* WIP: R3 Verification

* docs(r3): advance TC1 Q-PAFS brief PROPOSAL → DESIGN

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>

* docs(briefs): replace bare .md line refs with section anchors (Verification)

Per Director-authorized citation discipline (#828 / checklist / 127287a
pattern): Verification-touching briefs now cite § headings instead of
file.md:NNN for cross-doc pointers.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* docs(r3): fix Codex BLOCKING — L7 matrix cites T-V-L4-L7-Direct; sync 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>

* docs(briefs): clarify r3-program-plan path for TC1 ACCEPTED authority link

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(r3): single authority for Q-PAFS ACCEPTED — plan §10.3 at HEAD

openai-pro APPROVE_WITH_COMMENTS: PR #1824 must not read as parallel receipt
vs this PR. Committed docs/r3-program-plan.md §10.3 table is sole source of truth;

Co-authored-by: Cursor <cursoragent@cursor.com>
#1824 is merge-record only.

* docs(briefs): V1 worker — scope line is narrative not second authority

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>

* WIP: R3 Verification

* WIP: R3 Verification

* docs(briefs): TC1 V1 brief — Director Branch B hold, unpairs argument-opaque E3

Record η non-vacuity ratification: tc1_eta_equivalence_executable stays held until
Q-Reification + ReflectedProgram carrier (or explicit §1.8 revision). Clarify
bold-crane pin excludes TC1 V1 until unblock; Track A otherwise unchanged.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(r3): sync §10.3 Q-PAFS/Q-EVAL with Branch B TC1 V1 hold

Codex review on PR #1843: worker brief must not contradict canonical plan.
Record implementation supersession (η non-vacuity + Q-Reification) in
r3-program-plan.md §10.3; subordinate TC1 worker brief to that table (P2).

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* docs(briefs): add TC2 Pattern-A dispatch-ready worker brief

Pre-auth queue (#1859): r3-v-pattern-a-tc2-v1-worker.md for gate #12
tc2_church_rosser_executable — deps P1–P6, bold-crane pin, STOP+PING,
dispatch triggers. Index in r3-verification-manager.md.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(briefs): add TC3 Pattern-A dispatch-ready worker brief

Pre-auth queue (#1859): gate #13 tc3_pattern_a_second_mover_executable —
two-stage bundle (a)/(b), D1–D6 deps, bold-crane pin, STOP+PING. Index in
r3-verification-manager.md.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* docs(briefs): index tier-1 worker briefs in verification manager

§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>

* docs(r3): align T-LBP Summary, lane table, demos with option (b)

§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>

* WIP: R3 Verification

* WIP: R3 Verification

---------

Co-authored-by: Cursor <cursoragent@cursor.com>
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