Skip to content

docs(r3): Q-PAFS Path A ACCEPTED — Brian Director countersign 2026-05-06 - #1824

Merged
briansrls merged 11 commits into
mainfrom
docs/q-pafs-accepted-path-a-2026-05-06
May 6, 2026
Merged

docs(r3): Q-PAFS Path A ACCEPTED — Brian Director countersign 2026-05-06#1824
briansrls merged 11 commits into
mainfrom
docs/q-pafs-accepted-path-a-2026-05-06

Conversation

@briansrls

@briansrls briansrls commented May 6, 2026

Copy link
Copy Markdown
Contributor

Summary

  • Brian directive 2026-05-06: "approved path A countersign"
  • Resolves 3 bundled §10.3 questions PENDING → ACCEPTED
  • Implementation dispatch unblocked simultaneously across 2 lanes (same release step): Verification V1 + Evaluator E3

What ACCEPTED unlocks

Question Decision Lane unblock
Q-PAFS Path A: TC1 first slice = static representative via E6-G1.a Verification V1 — Pattern-A executable cluster (TC1 first slice)
Q-Pattern-A-First-Slice-Subscope G1.a static representative (TC1-generic deferred) bundled with Q-PAFS
Q-EVAL-Lens-Fold-First-Slice G1.a first-slice shape for E3 sequencing Evaluator E3 — E6-G1.a static lens fold

What stays gated (not unlocked)

  • Path B — TC1 generic via E6-G1.b / X1.b (deferred-not-blocked)
  • Path C — RustDagIsomorphism first (Director-only reorder, not under Q-PAFS default)
  • SubstrateResearchDeferredClaim widening — STOP+PING until routed implementation PRs land
  • Deferred TC1 fixture activation — STOP+PING
  • Substrate / evaluator carrier-shape changes — STOP+PING (separate routing)

ACCEPTED closes the policy-layer scope fork (which slice first), not the substrate routing.

Files changed

File Change
docs/r3-program-plan.md §10.3 Q-PAFS / Q-Pattern-A-First-Slice-Subscope / Q-EVAL-Lens-Fold-First-Slice rows: PENDING → ACCEPTED 2026-05-06 (Path A / G1.a) with explicit Brian-directive citation in disposition column + clear "what unlocks / what stays deferred" framing in status column
docs/r3-design-schedule-2026-05-06.md §V1 + §E3 dispatch trigger updated from "pending Director countersignature" to "DISPATCH UNBLOCKED 2026-05-06" with cross-references to the bundled gate

Test plan

  • All 3 §10.3 rows transitioned PENDING → ACCEPTED with verbatim Brian-directive citation
  • Zero remaining PENDING DIRECTOR COUNTERSIGNATURE strings in r3-program-plan.md (verified via grep)
  • §V1 + §E3 in design-schedule reflect DISPATCH UNBLOCKED with same release-step phrasing
  • Path B / Path C / SubstrateResearchDeferredClaim / deferred-TC1-fixture / substrate-routing all explicitly named as still-gated (not silently widened)
  • Verification Mgr (cool-owl-579 session/cool-owl-579 · cool-owl-579 #1740) authors V1 worker brief post-merge
  • Evaluator Mgr (merry-gull-128 session/merry-gull-128 · merry-gull-128 #1743) authors E3 worker brief post-merge

🤖 Generated with Claude Code

briansrls and others added 11 commits May 6, 2026 06:03
@briansrls @claude
docs(r3): Q-MachineConstraint-Carrier RATIFIED — universal substrate …
64ebf28 
…+ 5 PM defaults (Brian directive)

Brian directive 2026-05-06: "universal substrate, ratify defaults".

Resolves Q-MachineConstraint-Carrier (was OPEN per r3-program-plan.md §10.3)
with 6 sub-decisions ratified:

1. Axes in R3 scope: MachineWidth<bits> only. RegisterClass<R> / EndianMode<E>
   / alignment / signedness-as-axis deferred post-R3.
2. Interaction substrate shape: parametric Compose<Algebra, MachineConstraint>
   type-level construction. Closed-enumeration lookup-maps rejected (bridges).
3. Type-level spelling: Int<64> = Compose<AbelianGroup, MachineWidth<64>>
   parametrically. Equivalent under both algebra-side options per PR #1815.
4. Approximate-algebra layering: algebra approx + machine approx are
   independent composing axes. Real<64> = Compose<ApproximateField<Rational>,
   MachineWidth<64>> carries both layers per S8 discipline.
5. Class 1 demonstration breadth: ≥3 algebra×constraint pairs is minimum,
   not target. Broader coverage follows automatically once parser handles
   generic interaction syntax.
6. Target-specificity: MachineConstraint<C> is UNIVERSAL substrate (Brian
   directive). Every target carries machine-constraint facts as substrate;
   targets lacking native machine-width semantics (Python int/float) handle
   omission at Grounding-level discharge — target-conditioned lowering,
   NOT target-conditioned substrate.

Substrate Mgr S3 dispatch unblocked on machine-constraint side; independent
of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815
(interaction semantics carries through under either).

Updates:
- docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row: OPEN →
  RATIFIED 2026-05-06 with all 6 sub-decisions named.
- docs/r3-design-schedule-2026-05-06.md §S3: drops "open scope" framing;
  explicit ratified-scope block citing the 6 decisions; S3 dispatch noted
  as unblocked on machine-constraint side.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls @claude
docs(r3): Q-MachineConstraint sub-decisions 1/2/5/6 elaborated per Br…
8f5483b 
…ian clarifying inline

Brian clarifying directive 2026-05-06 on the 6 sub-decisions:

1. AXES — accept MachineWidth<bits> only; add separation-of-facts/concerns
   discipline note: algebra/machine-constraint/target-lowering are distinct
   axes. Integer modeling is the canonical exercise.

2. INTERACTION SHAPE (revised from "parametric Compose<...>" framing):
   "these models interact a la rest apis interacting — scalable / no dual
   representations (.dag generated)". The interaction substrate is
   .dag-DECLARED + .dag-GENERATED, never hand-coded. Hard constraint: no
   dual representations — any Rust counterpart must be generated, never
   hand-maintained (feedback_isomorphism_or_generation_for_mirrors +
   feedback_no_generated_code_on_disk).

3. SPELLING — Compose<AbelianGroup, MachineWidth<64>> ratified ("ok fine").
   Note added: the interaction substrate elaborating Compose<...> is
   .dag-generated per sub-decision 2.

4. LAYERING — independent composing axes ratified ("ok fine"). Real<64> =
   Compose<ApproximateField<Rational>, MachineWidth<64>> stays.

5. DEMONSTRATION BREADTH — strengthened: "3 is not a target, we shouldn't
   be 'targeting' modeling, we are just doing our best job to faithfully
   represent the concepts". Closure criterion is "concept is faithfully
   modeled", not "≥3 pairs land". 3-pair demonstration is minimum
   existence proof, not closure target.

6. TARGET-SPECIFICITY — universal substrate stays. Python lowering uses
   faithful target-available primitives (numpy.uint8 / ctypes.c_uint8 /
   explicit literal-bits), NOT omission. "if python lacks — we would have
   to actually represent the struct using something that python faithfully
   provides — i.e. either literal bits or otherwise". Faithful
   representation > target-conditioned omission.

Updates docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row +
docs/r3-design-schedule-2026-05-06.md §S3 ratified-scope block to reflect
clarifying inline.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
Merge remote-tracking branch 'origin/main' into docs/q-machine-constr…
83be121 
…aint-ratification-2026-05-06
@briansrls @claude
docs(r3): closure predicate aligned to faithful-modeling criterion (o…
e1ea7cf 
…penai-pro BLOCKING fix)

openai-pro REQUEST_CHANGES at sha 8f5483b on PR #1817 caught a real
internal inconsistency: ratification text said "Faithful representation of
the concept is the closure criterion; pair-counting is not" but the actual
closure predicates across r3-structure.md / r3-program-plan.md /
r3-design-schedule-2026-05-06.md still phrased Pass as "≥3 pairs emit to
target primitives". This violated single-authority + facts-flow-forward.

Fix: align all 5 Pass-condition / closure-predicate locations to the
faithful-modeling criterion ratified in Q-MachineConstraint sub-decision 5:

- docs/r3-program-plan.md:74 (gate #60 Pass condition in §1.4 ledger):
  "Gate Pass = concept faithfully modeled (per Brian directive 2026-05-06)
  — once substrate carries algebra + machine-constraint as independent
  composing axes with .dag-generated interaction substrate, all valid pairs
  work by construction. Minimum existence-proof evidence: 3 pairs lower
  without v2-fallback (evidence, not target)."
- docs/r3-program-plan.md:257 (§1.8 canonical ledger row): "concept
  faithfully modeled... min existence-proof = Int<64>/Real<64>/Nat<8>
  lower without v2-fallback (evidence, not target)"
- docs/r3-program-plan.md:430 (§1.4 Class 1 representative gap-test):
  "Representative gap-test (minimum existence-proof, NOT target) — substrate
  faithfully modeling algebra + machine-constraint separation IS the
  closure criterion; the 3 pairs below are the minimum existence-proof"
- docs/r3-structure.md:173 (canonical gate description): "Pass condition:
  concept faithfully modeled... Minimum existence-proof evidence (not
  closure target): 3 pairs lower without v2-fallback"
- docs/r3-design-schedule-2026-05-06.md:60 (S3 closure predicate cite):
  "Pass = concept faithfully modeled... 3-pair set is minimum
  existence-proof evidence, NOT the closure target"

Sub-decision 5 explanatory text retains "≥3 pairs land" as anti-reference
to the prior phrasing for traceability of the change.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls @claude
docs(r3): apply 2 claude APPROVE-with-observations precisions on Q-Ma…
8099ace 
…chineConstraint

Claude review at sha e1ea7cf (post-BLOCKING-fix) APPROVE with two
exploratory observations. Both worth applying:

1. Sub-decision 3: clarify Compose<...> elaboration vs interaction substrate.
   Sub-decision 2 says the *interaction substrate* (composition/projection/
   coercion machinery) is .dag-generated, not the Compose<...> type itself.
   Avoid an S3 worker reading "the Compose type is generated."

2. Closure predicate: explicit note that §1.4 conjunctive-closure rule still
   binds. Sub-decision 5 narrows what counts as Pass (concept faithfully
   modeled, not pair-counting), but does NOT relax the conjunctive form
   (representative gap-test executes AND class-bridge enumeration = 0).

Both are tightening clarifications; no disposition change.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
Merge remote-tracking branch 'origin/main' into docs/q-machine-constr…
a813097 
…aint-ratification-2026-05-06
@briansrls @claude
docs(r3): codex BLOCKING fix — Compose<concept, MachineWidth<...>> no…
150c28a 
…t Compose<witness, ...>

Codex BLOCKING at sha 8099ace on PR #1817 caught a real type-level error:
Compose<AbelianGroup, MachineWidth<64>> composes the *algebra witness shape*
rather than the integer carrier. Per dsl/std/algebra.dag:148-150:

  "T = GroupCompletion<M> is the carrier; AbelianGroup<T> carries
   op/identity/inverse over that carrier"

AbelianGroup<T> is a witness shape generic over carrier T, not a carrier
constructor. The bare AbelianGroup (without args) is just the kind/
constructor — putting it in Compose<...> slot-1 doesn't yield an integer
carrier.

Correct form: first slot of Compose<...> holds the **algebraic concept**
(the fully-applied carrier+witness composite that IS the Int / UInt /
Real / Nat type), second slot holds the machine-constraint:

- Int<64>  = Compose<Int, MachineWidth<64>>      (Int = AbelianGroup<GroupCompletion<Nat>> per #1466)
- UInt<64> = Compose<UInt, MachineWidth<64>>     (UInt = CommutativeMonoid<Nat> per #1818)
- Real<64> = Compose<Real, MachineWidth<64>>     (Real = ApproximateField<Rational>)
- Nat<8>   = Compose<Nat, MachineWidth<8>>

Updates sub-decision 3 (type-level spelling) + sub-decision 4 (approximate-
algebra layering) in both r3-design-schedule-2026-05-06.md §S3 and
r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row. Wrong-form
references retained as anti-references only ("prior phrasing was wrong";
critical correction note + dsl/std/algebra.dag citation).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls @claude
docs(r3): flag Python width-lowering divergence with design-numeric-c…
694db2e 
…onstruction.md (codex non-blocking)

Codex non-blocking improvement at sha 83be121: sub-decision 6's Python
faithful-lowering directive (numpy.uint8 / ctypes.c_uint8 / literal-bits)
competes with the existing default at docs/design-numeric-construction.md:
194-198 which lowers Nat<N> for any N to plain Python int with size-hint
metadata (width-omission default).

Brian's directive ("represent the struct using something that python
faithfully provides") shifts the standing default to faithful concrete
representation, but the existing design doc isn't updated yet.

Fix: explicit "Tracked divergence" callout in sub-decision 6 (both r3-design-
schedule.md §S3 and r3-program-plan.md §10.3 row). Routes reconciliation
to T-Numeric-Construction / Grounding lane paydown — update
design-numeric-construction.md Python row when the Grounding-side per-target
lowering authority lands. Not bundled in this PR per scope; the divergence
is tracked-not-silent.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls @claude
docs(r3): sub-decision 6 unified with cost lens — universal faithful …
a00010c 
…representation, cost as discriminator (Brian directive)

Brian directive 2026-05-06 elaborated 2x:
"basically this would be represented by cost right - in all cases we
should be able to represent the structure with literal bits/objects or
whatever - the cost would be enormous - in those cases, we would look for
alternatives like better modeling/libraries/int & 0xFF"

This unifies sub-decision 6 with T-CostLens-Composition: faithful
representation is universal (every target CAN represent every concept,
literal-bits is the always-available floor); the cost lens is the
discriminator that orders the alternatives.

Reframing:

- Universality of faithful representation: every target carries every
  concept faithfully (literal-bits as the floor)
- Cost lens (T-CostLens-Composition gates cost_lens_reads_target_realization
  + coercion_cost_equals_complexity_by_construction) reads per-primitive
  realization cost from target language spec
- Grounding selects the lowest-cost faithful representation by reading
  cost-lens output
- For Python u8: cost-tier 1 = numpy.uint8 (low cost), cost-tier 2 =
  ctypes.c_uint8 (medium), cost-tier 3 = int & 0xFF discipline (universal
  floor, high cost). All three faithful; cost lens orders.

Implication: existing docs/design-numeric-construction.md:194-198 Python
row (Nat<N> → int with size-hint metadata) is NON-FAITHFUL — drops width
structure to opaque metadata, cost lens cannot read what isn't there.
Reframe routes to T-Numeric-Construction / Grounding lane paydown:
replace with cost-tiered faithful-representation table.

This is the structurally-elegant unification: faithful-representation
universality + cost-lens-as-discriminator. Sub-decision 6 IS an instance
of "coercion cost = complexity by construction" thesis (T-CostLens-Composition
load-bearing claim).

Updates both r3-design-schedule-2026-05-06.md §S3 and r3-program-plan.md
§10.3 Q-MachineConstraint-Carrier row sub-decision 6.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
Merge remote-tracking branch 'origin/main' into docs/q-machine-constr…
b9f69e6 
…aint-ratification-2026-05-06
@briansrls @claude
docs(r3): Q-PAFS Path A ACCEPTED — Brian Director countersignature 20…
3d4edf3 
…26-05-06

Per Brian directive 2026-05-06: "approved path A countersign".

Resolves three bundled §10.3 questions to ACCEPTED:

- Q-PAFS: TC1 first slice = static representative via E6-G1.a (Path A);
  Path B (TC1 generic G1.b/X1.b) deferred; Path C (RustDagIsomorphism before
  TC1) deferred under Q-PAFS default.
- Q-Pattern-A-First-Slice-Subscope: G1.a static representative ratified;
  TC1-generic via X1.b S1/S3 + G1.b deferred-not-blocked.
- Q-EVAL-Lens-Fold-First-Slice: G1.a first-slice shape locked for Evaluator
  E3 sequencing.

Implementation dispatch unblocked simultaneously across two lanes (same
release step):

- Verification V1 — Pattern-A executable cluster, TC1 first slice
- Evaluator E3 — E6-G1.a static lens fold

Both Mgrs (cool-owl-579 #1740, merry-gull-128 #1743) author worker briefs
and dispatch in same release step. Substrate/evaluator carrier-shape
changes remain STOP+PING until routed implementation PRs land —
ACCEPTED closes the policy-layer scope fork (which slice first), not the
substrate routing.

Updates:
- docs/r3-program-plan.md §10.3: Q-PAFS / Q-Pattern-A-First-Slice-Subscope /
  Q-EVAL-Lens-Fold-First-Slice rows from PENDING DIRECTOR COUNTERSIGNATURE
  to ACCEPTED 2026-05-06 (Path A / G1.a).
- docs/r3-design-schedule-2026-05-06.md §V1 + §E3: dispatch trigger updated
  from "pending Director countersignature" to "DISPATCH UNBLOCKED 2026-05-06"
  with cross-references to the bundled gate.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 6, 2026
Closed
Closed
@briansrls
briansrls merged commit 961e78d into main May 6, 2026
3 checks passed
@briansrls briansrls mentioned this pull request May 6, 2026
Closed
briansrls added a commit that referenced this pull request May 6, 2026
@briansrls @cursoragent
docs(r3): fix Codex BLOCKING — L7 matrix cites T-V-L4-L7-Direct; sync…
41754b3 
… 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>
@briansrls briansrls mentioned this pull request May 6, 2026
Merged
briansrls added a commit that referenced this pull request May 6, 2026
@briansrls @cursoragent
docs(r3): single authority for Q-PAFS ACCEPTED — plan §10.3 at HEAD
0808cac 
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.
briansrls added a commit that referenced this pull request May 6, 2026
@briansrls @cursoragent
R3 Verification (#1822)
fa742a4 
* 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.

---------

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 6, 2026
@briansrls @cursoragent
R3 Verification (#1829)
70609c6 
* 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>

---------

Co-authored-by: Cursor <cursoragent@cursor.com>
This was referenced May 6, 2026
Closed
Closed
Merged
briansrls added a commit that referenced this pull request May 6, 2026
@briansrls @cursoragent
R3 Verification (#1893)
04e9e44 
* 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>
@briansrls briansrls mentioned this pull request May 7, 2026
Merged
6 of 8 tasks
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