From 8312561d9a211ab6dcf80980e72fddd36d2e2663 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 16:49:11 -0400 Subject: [PATCH 01/16] WIP: R3 Verification --- .../r3_verification_l4_l7_l5_skeleton_test.rs | 71 ++++++++++--------- 1 file changed, 37 insertions(+), 34 deletions(-) diff --git a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs index f127ff80339..f9b86e006f1 100644 --- a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs +++ b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs @@ -11,7 +11,7 @@ use std::sync::OnceLock; use v3_compiler::compile_to_dag; use v3_compiler::dag::Dag; -use v3_compiler::test_runner::{ClaimResult, TestClaimValue, TestRunner}; +use v3_compiler::test_runner::{ClaimEvaluation, ClaimResult, TestClaimValue, TestRunner}; use v3_compiler::CompileError; const L4_FIXTURE: &str = include_str!("../fixtures/r3_verification_l4_emit_eval_match.dag"); @@ -47,6 +47,9 @@ const L5_CLAIM: &str = "r3_verification_l5_cross_target_skeleton"; const L5_AUTHORITY_PROGRAM: &str = include_str!("../fixtures/r3_l5_corpus/add_then_branch_seed.v3"); static L4_DAG: OnceLock = OnceLock::new(); +/// `TestRunner::run_suite(L4_SUITE)` is compile-heavy; three `#[test]`s assert disjoint rows. +/// Run the suite once and share results so the 2s per-test ratchet sees one suite wall-clock. +static L4_SUITE_RESULTS: OnceLock> = OnceLock::new(); static L4_MIXED_DAG: OnceLock = OnceLock::new(); static L7_DAG: OnceLock = OnceLock::new(); static L5_DAG: OnceLock = OnceLock::new(); @@ -73,6 +76,15 @@ fn cached_compile( }) } +fn l4_emit_eval_skeleton_suite_results() -> &'static [ClaimEvaluation] { + L4_SUITE_RESULTS.get_or_init(|| { + run_on_larger_stack(|| { + let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG); + TestRunner::new(dag).run_suite(L4_SUITE) + }) + }) +} + fn run_on_larger_stack(f: impl FnOnce() -> T + Send + 'static) -> T where T: Send + 'static, @@ -87,47 +99,38 @@ where #[test] fn r3_verification_l4_emit_eval_match_skeleton_passes_w1_emit_vs_eval() { - run_on_larger_stack(|| { - let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG); - let results = TestRunner::new(dag).run_suite(L4_SUITE); - assert_eq!(results.len(), 3); - assert_eq!(results[0].claim_name, L4_CLAIM); - assert!( - matches!(results[0].result, ClaimResult::Pass), - "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (branch literal 3); got {:?}", - results[0].result - ); - }); + let results = l4_emit_eval_skeleton_suite_results(); + assert_eq!(results.len(), 3); + assert_eq!(results[0].claim_name, L4_CLAIM); + assert!( + matches!(results[0].result, ClaimResult::Pass), + "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (branch literal 3); got {:?}", + results[0].result + ); } #[test] fn r3_verification_l4_emit_eval_false_branch_passes_w1_emit_vs_eval() { - run_on_larger_stack(|| { - let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG); - let results = TestRunner::new(dag).run_suite(L4_SUITE); - assert_eq!(results.len(), 3); - assert_eq!(results[1].claim_name, L4_FALSE_CLAIM); - assert!( - matches!(results[1].result, ClaimResult::Pass), - "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (false branch signed Int -4); got {:?}", - results[1].result - ); - }); + let results = l4_emit_eval_skeleton_suite_results(); + assert_eq!(results.len(), 3); + assert_eq!(results[1].claim_name, L4_FALSE_CLAIM); + assert!( + matches!(results[1].result, ClaimResult::Pass), + "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (false branch signed Int -4); got {:?}", + results[1].result + ); } #[test] fn r3_verification_l4_emit_eval_nested_branch_passes_w1_emit_vs_eval() { - run_on_larger_stack(|| { - let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG); - let results = TestRunner::new(dag).run_suite(L4_SUITE); - assert_eq!(results.len(), 3); - assert_eq!(results[2].claim_name, L4_NESTED_CLAIM); - assert!( - matches!(results[2].result, ClaimResult::Pass), - "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (nested branch Int 7); got {:?}", - results[2].result - ); - }); + let results = l4_emit_eval_skeleton_suite_results(); + assert_eq!(results.len(), 3); + assert_eq!(results[2].claim_name, L4_NESTED_CLAIM); + assert!( + matches!(results[2].result, ClaimResult::Pass), + "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (nested branch Int 7); got {:?}", + results[2].result + ); } #[test] From a6171ece77bf9449abae8f3a30a6a814c1e7d176 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 17:19:18 -0400 Subject: [PATCH 02/16] WIP: R3 Verification --- src/v3/compiler/tests/integration.rs | 30 +++++++++++++++------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 1aa5bea3c20..96516ef6b83 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -205,6 +205,7 @@ mod t_demo_fixture_test { use std::fs; use std::path::PathBuf; + use std::sync::OnceLock; use v3_compiler::compile_to_dag; use v3_compiler::dag::Dag; @@ -227,10 +228,15 @@ mod t_demo_fixture_test { crate::common::cached_compile_to_dag(source, FIXTURE) } + static T_DEMO_FIXTURE_DAG: OnceLock = OnceLock::new(); + + fn cached_t_demo_fixture_dag() -> &'static Dag { + T_DEMO_FIXTURE_DAG.get_or_init(|| compile_fixture(&fixture_source())) + } + #[test] fn t_demo_fixture_skeleton_compiles() { - let source = fixture_source(); - let dag = compile_fixture(&source); + let dag = cached_t_demo_fixture_dag(); assert!( dag.diagnostics().is_empty(), @@ -241,14 +247,13 @@ mod t_demo_fixture_test { #[test] fn t_demo_canonical_suites_are_runner_visible() { - let source = fixture_source(); - let dag = compile_fixture(&source); + let dag = cached_t_demo_fixture_dag(); for suite_name in [ "fixture_compiler_nerd_canonical", "fixture_integration_canonical", ] { - let results = TestRunner::new(&dag).run_suite(suite_name); + let results = TestRunner::new(dag).run_suite(suite_name); assert!( !results.is_empty(), "T-Demo suite `{suite_name}` should contain Day-1 Compiles claims" @@ -283,9 +288,8 @@ mod t_demo_fixture_test { #[test] fn t_demo_impossible_bug_suite_r1_passes() { - let source = fixture_source(); - let dag = compile_fixture(&source); - let results = TestRunner::new(&dag).run_suite("impossible_bug_class_suite_r1"); + let dag = cached_t_demo_fixture_dag(); + let results = TestRunner::new(dag).run_suite("impossible_bug_class_suite_r1"); assert_eq!(results.len(), 2); assert!( results @@ -301,9 +305,8 @@ mod t_demo_fixture_test { /// surface is user-extensible (THESIS §"User-defined dimensions"). #[test] fn t_demo_user_authored_lens_rejects_violating_program_passes() { - let source = fixture_source(); - let dag = compile_fixture(&source); - let results = TestRunner::new(&dag) + let dag = cached_t_demo_fixture_dag(); + let results = TestRunner::new(dag) .run_suite("demo_user_authored_lens_rejects_violating_program_suite"); assert_eq!(results.len(), 1); assert!( @@ -328,9 +331,8 @@ mod t_demo_fixture_test { #[test] fn t_demo_structural_cost_obligation_suite_observes_cost_bound_fail() { - let source = fixture_source(); - let dag = compile_fixture(&source); - let results = TestRunner::new(&dag).run_suite("t_demo_structural_cost_obligation_suite"); + let dag = cached_t_demo_fixture_dag(); + let results = TestRunner::new(dag).run_suite("t_demo_structural_cost_obligation_suite"); assert_eq!(results.len(), 1); let ClaimResult::Fail(msg) = &results[0].result else { panic!( From ee75dfeea79d39167d93c7c035afe1f67ad37e98 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 17:22:26 -0400 Subject: [PATCH 03/16] WIP: R3 Verification --- src/v3/compiler/tests/integration.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 96516ef6b83..48130998477 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -234,8 +234,10 @@ mod t_demo_fixture_test { T_DEMO_FIXTURE_DAG.get_or_init(|| compile_fixture(&fixture_source())) } + /// Lexicographic name sorts before `impossible_bug_*` in this module so libtest warms + /// [`T_DEMO_FIXTURE_DAG`] before suite-heavy tests (2s per-test ratchet on cold CI). #[test] - fn t_demo_fixture_skeleton_compiles() { + fn a_t_demo_fixture_skeleton_warms_dag_cache() { let dag = cached_t_demo_fixture_dag(); assert!( From 08262bd16adf1280de45f96f53fb0e27dfcdbf63 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 21:33:26 +0000 Subject: [PATCH 04/16] 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` populated by whichever test hit the OnceLock first. Removes unused `L4_SUITE` constant. Co-authored-by: Cursor --- .../r3_verification_l4_l7_l5_skeleton_test.rs | 50 +++++++++---------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs index f9b86e006f1..90a73210097 100644 --- a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs +++ b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs @@ -17,7 +17,6 @@ use v3_compiler::CompileError; const L4_FIXTURE: &str = include_str!("../fixtures/r3_verification_l4_emit_eval_match.dag"); const L4_FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag"; -const L4_SUITE: &str = "r3_verification_l4_emit_eval_skeleton_suite"; const L4_CLAIM: &str = "r3_verification_l4_emit_eval_match_skeleton"; const L4_FALSE_CLAIM: &str = "r3_verification_l4_emit_eval_false_branch"; const L4_NESTED_CLAIM: &str = "r3_verification_l4_emit_eval_nested_branch"; @@ -47,9 +46,6 @@ const L5_CLAIM: &str = "r3_verification_l5_cross_target_skeleton"; const L5_AUTHORITY_PROGRAM: &str = include_str!("../fixtures/r3_l5_corpus/add_then_branch_seed.v3"); static L4_DAG: OnceLock = OnceLock::new(); -/// `TestRunner::run_suite(L4_SUITE)` is compile-heavy; three `#[test]`s assert disjoint rows. -/// Run the suite once and share results so the 2s per-test ratchet sees one suite wall-clock. -static L4_SUITE_RESULTS: OnceLock> = OnceLock::new(); static L4_MIXED_DAG: OnceLock = OnceLock::new(); static L7_DAG: OnceLock = OnceLock::new(); static L5_DAG: OnceLock = OnceLock::new(); @@ -76,12 +72,19 @@ fn cached_compile( }) } -fn l4_emit_eval_skeleton_suite_results() -> &'static [ClaimEvaluation] { - L4_SUITE_RESULTS.get_or_init(|| { - run_on_larger_stack(|| { - let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG); - TestRunner::new(dag).run_suite(L4_SUITE) - }) +/// Runs one named `TestClaim` from the L4 fixture on a larger stack. The compiled `Dag` is +/// amortized via [`L4_DAG`]; each `#[test]` calls `run_claim` independently (no shared +/// `ClaimEvaluation` vector — see TESTING.md `OnceLock` carve-out / api-review on PR #1802). +fn l4_run_named_claim(claim_name: &'static str) -> ClaimEvaluation { + run_on_larger_stack(move || { + let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG); + let claim_decl = dag + .declaration_by_name(claim_name) + .unwrap_or_else(|| panic!("missing `{claim_name}` in {L4_FIXTURE_PATH}")); + let claim = TestClaimValue::from_declaration(claim_decl).unwrap_or_else(|reason| { + panic!("`{claim_name}` should lower to a structural TestClaim: {reason}"); + }); + TestRunner::new(dag).run_claim(&claim) }) } @@ -99,37 +102,34 @@ where #[test] fn r3_verification_l4_emit_eval_match_skeleton_passes_w1_emit_vs_eval() { - let results = l4_emit_eval_skeleton_suite_results(); - assert_eq!(results.len(), 3); - assert_eq!(results[0].claim_name, L4_CLAIM); + let evaluation = l4_run_named_claim(L4_CLAIM); + assert_eq!(evaluation.claim_name, L4_CLAIM); assert!( - matches!(results[0].result, ClaimResult::Pass), + matches!(evaluation.result, ClaimResult::Pass), "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (branch literal 3); got {:?}", - results[0].result + evaluation.result ); } #[test] fn r3_verification_l4_emit_eval_false_branch_passes_w1_emit_vs_eval() { - let results = l4_emit_eval_skeleton_suite_results(); - assert_eq!(results.len(), 3); - assert_eq!(results[1].claim_name, L4_FALSE_CLAIM); + let evaluation = l4_run_named_claim(L4_FALSE_CLAIM); + assert_eq!(evaluation.claim_name, L4_FALSE_CLAIM); assert!( - matches!(results[1].result, ClaimResult::Pass), + matches!(evaluation.result, ClaimResult::Pass), "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (false branch signed Int -4); got {:?}", - results[1].result + evaluation.result ); } #[test] fn r3_verification_l4_emit_eval_nested_branch_passes_w1_emit_vs_eval() { - let results = l4_emit_eval_skeleton_suite_results(); - assert_eq!(results.len(), 3); - assert_eq!(results[2].claim_name, L4_NESTED_CLAIM); + let evaluation = l4_run_named_claim(L4_NESTED_CLAIM); + assert_eq!(evaluation.claim_name, L4_NESTED_CLAIM); assert!( - matches!(results[2].result, ClaimResult::Pass), + matches!(evaluation.result, ClaimResult::Pass), "expected W1 DifferentialEquals(rust_emit_output, dag_eval_output) Pass (nested branch Int 7); got {:?}", - results[2].result + evaluation.result ); } From 84a10ffffcc2fd6b38a2b112a03e9f734521f4ca Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 21:42:27 +0000 Subject: [PATCH 05/16] 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 --- src/v3/compiler/tests/integration.rs | 6 ++++-- .../integration/r3_verification_l4_l7_l5_skeleton_test.rs | 3 ++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index 48130998477..fb5c9baca41 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -234,8 +234,10 @@ mod t_demo_fixture_test { T_DEMO_FIXTURE_DAG.get_or_init(|| compile_fixture(&fixture_source())) } - /// Lexicographic name sorts before `impossible_bug_*` in this module so libtest warms - /// [`T_DEMO_FIXTURE_DAG`] before suite-heavy tests (2s per-test ratchet on cold CI). + /// `a_…` sorts first among `t_demo_fixture_test::*` names so **serial** libtest runs (e.g. + /// `--test-threads=1`) tend to hit [`T_DEMO_FIXTURE_DAG`] before other module tests that use + /// it. With default parallelism, **order is not guaranteed**; correctness still comes from + /// `OnceLock` init being race-safe, this is only a best-effort compile warm for CI ratchets. #[test] fn a_t_demo_fixture_skeleton_warms_dag_cache() { let dag = cached_t_demo_fixture_dag(); diff --git a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs index 90a73210097..ca898f0a21f 100644 --- a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs +++ b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs @@ -74,7 +74,8 @@ fn cached_compile( /// Runs one named `TestClaim` from the L4 fixture on a larger stack. The compiled `Dag` is /// amortized via [`L4_DAG`]; each `#[test]` calls `run_claim` independently (no shared -/// `ClaimEvaluation` vector — see TESTING.md `OnceLock` carve-out / api-review on PR #1802). +/// `ClaimEvaluation` vector — see TESTING.md, “Don’t use cross-test shared state” / `OnceLock` +/// amortization carve-out). fn l4_run_named_claim(claim_name: &'static str) -> ClaimEvaluation { run_on_larger_stack(move || { let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG); From 8287bbab5467b315b50f1a2d28f149da7f27bd77 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 21:47:53 +0000 Subject: [PATCH 06/16] 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 --- src/v3/compiler/tests/integration.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index fb5c9baca41..db55bb737cc 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -234,12 +234,12 @@ mod t_demo_fixture_test { T_DEMO_FIXTURE_DAG.get_or_init(|| compile_fixture(&fixture_source())) } - /// `a_…` sorts first among `t_demo_fixture_test::*` names so **serial** libtest runs (e.g. - /// `--test-threads=1`) tend to hit [`T_DEMO_FIXTURE_DAG`] before other module tests that use - /// it. With default parallelism, **order is not guaranteed**; correctness still comes from - /// `OnceLock` init being race-safe, this is only a best-effort compile warm for CI ratchets. + /// Smoke: the checked-in T-Demo `.dag` fixture lowers with empty module diagnostics. Uses + /// `cached_t_demo_fixture_dag` so the compile is amortized with sibling tests (TESTING.md + /// `OnceLock` carve-out); the first caller pays `OnceLock::get_or_init`; libtest order is not + /// part of the contract. #[test] - fn a_t_demo_fixture_skeleton_warms_dag_cache() { + fn t_demo_fixture_skeleton_compiles() { let dag = cached_t_demo_fixture_dag(); assert!( From 94af12a5721543f24d299c3b21e7c05cf4a025df Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 21:58:14 +0000 Subject: [PATCH 07/16] test(r3-l4): assert skeleton suite cardinality without index coupling MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../r3_verification_l4_l7_l5_skeleton_test.rs | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs index ca898f0a21f..12543bb033a 100644 --- a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs +++ b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs @@ -17,6 +17,7 @@ use v3_compiler::CompileError; const L4_FIXTURE: &str = include_str!("../fixtures/r3_verification_l4_emit_eval_match.dag"); const L4_FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag"; +const L4_SUITE: &str = "r3_verification_l4_emit_eval_skeleton_suite"; const L4_CLAIM: &str = "r3_verification_l4_emit_eval_match_skeleton"; const L4_FALSE_CLAIM: &str = "r3_verification_l4_emit_eval_false_branch"; const L4_NESTED_CLAIM: &str = "r3_verification_l4_emit_eval_nested_branch"; @@ -134,6 +135,33 @@ fn r3_verification_l4_emit_eval_nested_branch_passes_w1_emit_vs_eval() { ); } +/// Suite-wide shape: exactly three named W1 claims, each passing (complements per-claim +/// `run_claim` tests without pinning suite result order). +#[test] +fn r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims() { + run_on_larger_stack(|| { + let dag = cached_compile(L4_FIXTURE, L4_FIXTURE_PATH, &L4_DAG); + let results = TestRunner::new(dag).run_suite(L4_SUITE); + assert_eq!( + results.len(), + 3, + "`{L4_SUITE}` should wire exactly three W1 row claims" + ); + for name in [L4_CLAIM, L4_FALSE_CLAIM, L4_NESTED_CLAIM] { + assert!( + results.iter().any(|r| r.claim_name == name), + "missing `{name}` in suite results: {results:?}" + ); + } + assert!( + results + .iter() + .all(|r| matches!(r.result, ClaimResult::Pass)), + "every wired L4 W1 claim in `{L4_SUITE}` should Pass; got {results:?}" + ); + }); +} + #[test] fn r3_verification_l4_emit_eval_mixed_lineage_stays_not_yet_implemented() { run_on_larger_stack(|| { From 80621c609ae02bc0a0844ac09a9b90c1c5dadaf9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 23:23:15 +0000 Subject: [PATCH 08/16] 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 --- .github/workflows/ci.yml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 694d177fb59..d4c2161b4f4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -329,12 +329,11 @@ jobs: # Lane 1 Stage 1e closes: do not block merges on this job yet. self_host_ratchet: if: github.event.pull_request.draft != true - # Same sizing rationale as `v3` above: cargo release builds + - # determinism_test (5x emit matrix) + self_host_fixed_point bin - # need >2 cores to clear the 30min cap. Hard-coded to - # ubicloud-standard-8. + # Same sizing rationale as `v3` above: DB-8 release builds run on + # ubicloud-standard-8. Use a 60m wall-clock cap so cold-cache / full release + # `cargo` work is unlikely to hit mid-compile cancellation (ratchet remains non-blocking). runs-on: ubicloud-standard-8 - timeout-minutes: 30 + timeout-minutes: 60 needs: [v3] continue-on-error: true steps: From dbb67cf6ddce3fe1a1b4ac496c82f64a3c2a67eb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 01:56:00 -0400 Subject: [PATCH 09/16] WIP: R3 Verification --- .../r3-v-tc1-eta-equivalence-deeper-analysis.md | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md index ccdd3fbe7d7..18d79d63f00 100644 --- a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md +++ b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md @@ -1,6 +1,20 @@ # R3 TC1 Eta-Equivalence Deeper Structural Verification Analysis -**Status:** PROPOSAL / research-only. TC1 fixture remains as-is; this brief explores the strict-fire extension surface only. No substrate, runner, or fixture changes are proposed here. +**Status:** **DESIGN** (2026-05-06). Verification Mgr engineering choice among Pattern-A +first-slice paths; **not** yet **ACCEPTED** (Director countersignature still required per +`docs/r3-program-plan.md` §10.3 **Q-PAFS** and Brian directive: PROPOSAL → DESIGN → +ACCEPTED). + +**Lifecycle** + +| Stage | Meaning | +| --- | --- | +| PROPOSAL | Exploratory surface map only (superseded by this revision). | +| **DESIGN** (here) | Chooses a concrete first-slice shape, defers alternatives, states runtime prereqs and scope deltas. | +| ACCEPTED | Director/Brian countersign; authorizes implementation dispatch (V1 TC1 executable slice + Evaluator **E6-G1.a** lens-fold first slice in lockstep). | + +TC1 deferred fixture remains **as-is** until ACCEPTED + routed implementation; this brief +still does **not** authorize substrate, runner, or fixture edits by itself. **Owning manager:** R3 Verification Manager, absorbed formal-grounding responsibility. From 8539056b5defc878691cb67d1c6b4906ca36a672 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 06:00:16 +0000 Subject: [PATCH 10/16] =?UTF-8?q?docs(r3):=20advance=20TC1=20Q-PAFS=20brie?= =?UTF-8?q?f=20PROPOSAL=20=E2=86=92=20DESIGN?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- ...3-v-tc1-eta-equivalence-deeper-analysis.md | 89 ++++++++++++++++++- docs/r3-program-plan.md | 6 +- 2 files changed, 88 insertions(+), 7 deletions(-) diff --git a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md index 18d79d63f00..e9262a8c01c 100644 --- a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md +++ b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md @@ -73,7 +73,84 @@ Potential substrate paths, for Director/Substrate ratification: - generalize `LensOutputEquals` into a binary structural equality predicate over two lens applications; - model eta-equivalence as a substrate relation over reflected functions, then reuse a generic `DifferentialEquals`-style output comparison. -This analysis does not choose among those paths. +**DESIGN resolution (which slice first):** concrete choice lives in **§DESIGN — Q-PAFS +first executable slice** below. Predicate/carrier *shape* inside strict-fire remains +Substrate-owned STOP+PING until ACCEPTED routing. + +## DESIGN — Q-PAFS first executable slice (Pattern-A / TC1) + +This section satisfies the Verification Mgr obligation called out in +`r3-program-plan.md` §10.3 **Q-PAFS**: PM default ("TC1 first") is not engineering +sign-off; **DESIGN** records the explicit tradeoff and recommended path. + +### Path A — TC1 **static representative** via **E6-G1.a** (**recommended**) + +**Shape:** Ratify a **finite**, Director-visible **representative set** (not universal +quantification over all `Lens` for the first executable slice): fixed eta pair of +programs (`f` and `lambda x.apply(f, [x])`) plus a named list of lens instances (or +substrate-approved typed lens handles) that the evaluator can fold with **existing** +`fold_lens` / `DimensionReport` machinery. + +**Runtime prereqs (Evaluator / E6, aligned with Evaluator Mgr F4 + program-plan +Q-EVAL-Lens-Fold-First-Slice / Q-Pattern-A-First-Slice-Subscope):** + +- **E6-G1.a** static lens fold: two **structurally named** programs in `.dag` (or + equivalent declared scope) each produce a **typed** `DimensionReport` through the + same evaluator-owned fold authority—no X1.b generic transform-dispatch requirement for + this slice. +- **T-Substrate-Lens-Primitive** + lens producer retirement progress assumed per existing + lane dependencies: TC1 strict-fire still does **not** rest on widening + `SubstrateResearchDeferredClaim` (see **Carrier Scope Analysis**). +- **Pattern-A consumer envelope** unchanged: `BinaryDimensionReportEquals` over the two + reports once producers exist (`docs/briefs/r3-v-pattern-a-coverage-rollup.md`). + +**Substrate vs evaluator scope:** Substrate names the **representative lens set** and +any eta-pair **declaration refs**; Evaluator proves it can **execute** the fold twice and +lift reports without fixture-local producer identity or string bypass (Evaluator #1131 +safe contract). + +**Engineering justification:** Smallest executable surface that honors the PM default +(TC1 before TC2/TC3/RustDagIsomorphism ordering) **without** blocking on **E6-G1.b** / +**X1.b** S1/S3 generic dispatch. Unblocks **V1** “TC1 first slice” and **Evaluator E3** +(E6-G1.a) on the **same** Director **ACCEPTED** gate, per PM coordination note. + +### Path B — TC1 **generic** via **E6-G1.b / X1.b** (**defer**) + +**Shape:** Universal or parametric coverage over `Lens` / programs requiring **X1.b** +transform dispatch and **G1.b** generic lens-fold substrate not required for Path A. + +**Runtime prereqs:** Substrate **X1.b** S1/S3 + generic dispatch path; substantially +larger than G1.a; sequenced **after** Path A strict-fire is green or explicitly reprioritized +by Director. + +**Scope delta vs A:** Shifts primary risk from “representative selection” to “generic +dispatch + substrate carrier completion.” **Not** chosen for first executable slice. + +### Path C — **RustDagIsomorphism** first (**alternate, not recommended for Q-PAFS default**) + +**Shape:** Prioritize shape-report producers for `DimensionReport` before TC1 eta +pair (`docs/briefs/r3-v-pattern-a-coverage-rollup.md` §4 row **RustDagIsomorphism**). + +**Runtime prereqs:** Still requires generic typed `DimensionReport` production and two +structural shape reports; **fewer eta-specific** obligations than TC1. + +**Why not for Q-PAFS default:** Conflicts with stated PM/Brian **Pattern-A ordering** +(TC1 first) unless Director explicitly reorders. Remains a **credible fallback** if Director +rules TC1 eta unblockers dominate calendar—would require explicit scope edit, not silent +Verification drift. + +### DESIGN verdict + +| Question | Decision | +| --- | --- | +| First Pattern-A executable slice for TC1? | **Path A** — static representative **E6-G1.a**. | +| Generic TC1 (Path B)? | **Deferred** after Path A closes or Director reprioritizes. | +| RustDagIsomorphism before TC1? | **Not** under Q-PAFS default; **Path C** only with Director reorder. | +| Universal vs representative for first fire? | **Representative finite set** for slice one; universal quantification is a **later** ratchet question (see Open Questions). | + +**Surface for Director countersign (ACCEPTED):** Path A as written + explicit acknowledgment +that PM default and **DESIGN** engineering choice align; any deviation (e.g., Path C first) +is Director-owned scope calibration. ## Lens-Framework Anchors @@ -110,13 +187,17 @@ Shared with TC3: ## Open Questions -- Is TC1 universal over all `Lens` instances, or strict-fire over the migrated built-in lens set plus user-authored lens fixture? +- **Representative set contents:** which built-in / staged lens instances and which + single eta pair land in slice-one (Substrate + Director visibility)—DESIGN defers + enumeration to implementation routing post-ACCEPTED. +- **Universal quantification:** remains **out of scope** for first executable slice (Path + A); revisit after Path A strict-fire or if Director mandates broader coverage. - Does eta-equivalence live as a function/program relation in substrate, or only inside a verification predicate? - Should equality include witness-list ordering, or compare `DimensionReport` modulo semantically irrelevant witness ordering? - Does lens producer retirement provide enough reflection authority to construct eta-expanded forms structurally, or is a lambda-calculus grounding carrier still needed? ## Non-Goals -- No fixture activation today. +- No fixture activation or runner widening until **ACCEPTED** + implementation dispatch. - No runner validity widening for `SubstrateResearchDeferredClaim`. -- No edits to `r2-closure-ledger.md`, `r3-v-formal-grounding-tc-bundle.md`, `r3-verification-manager.md`, or `r3-pb-t-fixedpoint-worker.md`. +- No edits to `r2-closure-ledger.md`, `r3-v-formal-grounding-tc-bundle.md`, `r3-verification-manager.md`, or `r3-pb-t-fixedpoint-worker.md` from this DESIGN revision alone. diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index e3338e4bcee..98bbde18e30 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -950,7 +950,7 @@ Substrate canvas + plan-poke-hole both folded in. Key absorptions: | ID | Question | PM recommendation (applied as default) | Status | |---|---|---|---| -| Q-PAFS | Which Pattern-A (DimensionReport-typed family) first executable slice (TC1 vs RustDagIsomorphism vs other) | **TC1 η-equivalence first as PM/Brian convenience default; needs Director countersignature** — `r3-v-tc1-eta-equivalence-deeper-analysis.md` is `Status: PROPOSAL / research-only` and explicitly does not choose among paths. PM-default ≠ Verification-Mgr engineering sign-off. | **PENDING DIRECTOR COUNTERSIGNATURE** (per Verification Mgr poke-hole 2026-05-06; PM convenience-default applies until then) | +| Q-PAFS | Which Pattern-A (DimensionReport-typed family) first executable slice (TC1 vs RustDagIsomorphism vs other) | **TC1 first slice = static representative via E6-G1.a (Path A)** — `docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md` advanced to **DESIGN** (2026-05-06): Path B (TC1 generic G1.b / X1.b) **deferred**; Path C (RustDagIsomorphism before TC1) **not** under Q-PAFS default (Director reorder only). **ACCEPTED** still requires Director countersignature (Brian directive: PROPOSAL → DESIGN → ACCEPTED). PM default and Verification Mgr engineering choice **align on Path A**. | **PENDING DIRECTOR COUNTERSIGNATURE** for **ACCEPTED** (DESIGN landed 2026-05-06) | | Q-NYI-Accounting | NYI claim coverage/completeness accounting | Mark NYI incomplete in aggregation reporting; ratchet to executable per evaluator-slice landing | RATIFIED-by-default | | Q-Std-Carrier-Phasing | Rust std-carrier phasing (Option/Cardinal/HigherOrderMethodSpec/allocator-hasher) | Phase 1 = default-only/default-instance; later phases as separate Substrate slices post-Phase-1 | RATIFIED-by-default | | Q-Drift-Reconcile | Drift items routing (#1638, #1499, declaration_by_name) | Single Debt-Paydown worker reconciles all three → one PR closing rows in ledger + ROADMAP | RATIFIED-by-default | @@ -960,10 +960,10 @@ Substrate canvas + plan-poke-hole both folded in. Key absorptions: | Q-PR-Anticipation-Gate | Add `pr_anticipation_discipline_ci_active` closure gate (CI verifiably enforcing §7 anticipation discipline) | Add to §1 closure-gate set; owner R3 Debt-Paydown Mgr (already routed at #1744 #issuecomment-4383628247); fires when `scripts/check-pr-sg0-net-shrink-discipline.sh` is in CI workflow + self-test passes | RATIFIED-by-default (per Director poke-hole 2026-05-06 finding 3.2) | | Q-PR-F | PR-F priority + sequencing (BoundDeclaration consumer + Rust ReferenceModel) | **Bandwidth-aware dispatch** (per Substrate Mgr poke-hole 2026-05-06 Y3 — Substrate's queued workers are saturated): PR-F is 2-axis substantial work. Per Substrate Mgr canvas D: only loyal-wolf + valiant-ant fully idle; proud-lynx/smart-ram/valiant-ibex holding on #1794 cascade. Dispatch worker = loyal-wolf-828 OR valiant-ant-72 (Substrate Mgr selects); brief shape = T-E-P-Producer-Broadening adjacent (per `docs/briefs/r3-t-e-p-producer-broadening-worker.md` precedent); critical-path slot = post-#1782 wait-window close + parallel to T-E-P dispatch (B3). Substrate Mgr authors brief + dispatches. | RATIFIED-by-default-with-bandwidth-routing | | Q-Workflow-As-Data-Carriers | Substrate carriers for CI-workflow-as-`.dag`-data Class 4 closure path: `WorkflowTrigger` sum + `WorkflowStep`/`WorkflowMatrix` step-graph + `WorkflowSecret` binding + `RunnerResource` + `Workflow` composing carrier | Substrate Mgr authors carriers as part of T-Workflow-As-Data lane; sequenced post-T-Lens-Behavioral-Parity COMPLETE (per `r3-structure.md` §"Dependency on R2"); folds into existing T-Workflow-As-Data scope without new lane spawn. Required for Class 4 substrate-gap-class closure per §1.4. | OPEN — Substrate Mgr scoping needed (NEW 2026-05-06 from Substrate Mgr poke-hole R3) | -| Q-Pattern-A-First-Slice-Subscope | Q-PAFS sub-question: TC1 first means **static representative** (E6-G1.a) or **generic** (E6-G1.b/X1.b)? Plan defaulted to TC1 first without specifying which sub-shape. Per Evaluator Mgr F1 + EVAL-3: substantial substrate/evaluator scope difference. | Per `docs/briefs/r3-v-pattern-a-coverage-rollup.md` + Evaluator Mgr canvas: TC1-static-representative via E6-G1.a is achievable with current evaluator + lens-fold infrastructure; TC1-generic requires X1.b S1/S3 + G1.b. PM-recommended: **TC1-static-representative first** (smallest viable slice); generic deferred to subsequent ratchet. | OPEN — Director / Brian ratification needed (NEW 2026-05-06 from Evaluator Mgr F1 + EVAL-3; sub-question of Q-PAFS) | +| Q-Pattern-A-First-Slice-Subscope | Q-PAFS sub-question: TC1 first means **static representative** (E6-G1.a) or **generic** (E6-G1.b/X1.b)? Plan defaulted to TC1 first without specifying which sub-shape. Per Evaluator Mgr F1 + EVAL-3: substantial substrate/evaluator scope difference. | Per `docs/briefs/r3-v-pattern-a-coverage-rollup.md` + Evaluator Mgr canvas: TC1-static-representative via E6-G1.a is achievable with current evaluator + lens-fold infrastructure; TC1-generic requires X1.b S1/S3 + G1.b. PM-recommended: **TC1-static-representative first** (smallest viable slice); generic deferred to subsequent ratchet. **Verification Mgr DESIGN** (`r3-v-tc1-eta-equivalence-deeper-analysis.md`, 2026-05-06) ratifies **G1.a static representative first**. | **PENDING DIRECTOR COUNTERSIGNATURE** for ACCEPTED (bundles with Q-PAFS / Q-EVAL-Lens-Fold-First-Slice) | | Q-EVAL-G0d-Dispatch | E6-G0d constructor runtime execution: authorize evaluator slice for non-Arrow constructor `Callable` using `Value::RecordValue` / `Value::VariantValue` + shared substrate declaration-walk authority | Evaluator Mgr (merry-gull-128) dispatches; Director needed only if shared helper extraction crosses ownership. Brief at `docs/briefs/r3-pr-e6-g0d-constructor-runtime-execution-worker.md` ready. | RATIFIED-by-default — Evaluator Mgr executes (NEW 2026-05-06 from Evaluator Mgr EVAL-1) | | Q-EVAL-Descent-Termination-Contract | E5 `LoopBound::Descent` execution: substrate carrier `descent_execution_proof(&Dag, ClusterId, PortId) -> Result` with `Missing \| Unknown \| Incomplete \| NonStrict` fail-closed residuals | Substrate Mgr authors carrier (quick-koi-190 implementation already authorized through quick-crab); Evaluator consume-side ack; sharp-ibex consumer wiring dispatch. | RATIFIED-by-default — Substrate-side already authorized; Evaluator consume-side dependency (NEW 2026-05-06 from Evaluator Mgr EVAL-2) | -| Q-EVAL-Lens-Fold-First-Slice | Overlaps with Q-Pattern-A-First-Slice-Subscope: E6-G1.a static representative vs G1.b generic for first executable lens/report slice | Same recommendation as Q-Pattern-A-First-Slice-Subscope: **G1.a static-representative first**; G1.b generic deferred. | OPEN — same scope-question as Q-Pattern-A-First-Slice-Subscope (NEW 2026-05-06 from Evaluator Mgr EVAL-3) | +| Q-EVAL-Lens-Fold-First-Slice | Overlaps with Q-Pattern-A-First-Slice-Subscope: E6-G1.a static representative vs G1.b generic for first executable lens/report slice | Same recommendation as Q-Pattern-A-First-Slice-Subscope: **G1.a static-representative first**; G1.b generic deferred. **Verification Mgr DESIGN** (`r3-v-tc1-eta-equivalence-deeper-analysis.md`, 2026-05-06) locks the same **G1.a** first-slice shape for Evaluator E3 sequencing. | **PENDING DIRECTOR COUNTERSIGNATURE** for ACCEPTED (same gate as Q-PAFS) | | Q-Class-6-Substrate-Extension-Lens | 3 ctrl-side substrate proposals (`SchemaPreservation` per ctrl#370/#407 LLVM TBAA; `ResourceCap` per ctrl#404/#405 Cloudflare; `TotalResult` per ctrl#404/#405) don't fit Classes 1-5; PM-side routing to Substrate Mgr (#1130) committed per ctrl#408 §3 | PER Brian no-post-R3-deferral discipline: include as Class 6 substrate-gap-class with closure-criterion. Add §4.6 "Class 6 — typed-metadata-preservation / extension-lens slice" with representative gap-test per substrate. Alternative: Director ratification of explicit post-R3-ecosystem-by-design scope-cession. **Director disposition 2026-05-06 at gunbc#828 #issuecomment-4384615320: HOLD pending more context** — needs (i) which proposals are R3-blocking vs nice-to-have; (ii) substrate-author capacity for the 3 carriers; (iii) cross-lane cascade implications. PM surfaces from Research PM with sharper framing before Director ratification. | HOLD pending Research PM sharper framing (Director disposition; NEW 2026-05-06 from Research PM R-1) | | Q-Timeline-Risk-Alternates | §6 8-12 week estimate is commitment, not bottoms-up derivation. Missing risk-weighted alternates for: C1-class candidate-gap budget (2-6 weeks/gap) + WEDGE-CORE-CLAIM Part A thesis-edit scope + ~9 demo-gate authoring (1-3 weeks/lane) | Per `feedback_holistic_over_patches`: §9.2 add explicit "+X weeks if {C1-gap surfaces / Tier-4 thesis-edit lands in scope / demo authoring exceeds budget}" branches. R3 close horizon: 2026-08-01 ± 2 weeks PROVISIONAL → range with explicit risk-weighted alternates. | RATIFIED-by-default — PM updates §9.2 with risk-weighted branches in subsequent commit (NEW 2026-05-06 from Research PM R-2) | | Q-Plan-vs-Structure-Drift-Discipline | §3 lane status table holds 19 rows replicating r3-structure.md §"Lane structure" data; drift risk if PM updates one but not the other | Per Research PM R-3 recommendation (a): §3 lane status becomes pointer-with-delta to r3-structure.md §"Lane structure" + delta-only annotations (current dispatch + blocker + ETA). Lane name/Mgr/scope columns NOT restated; r3-structure.md retains architectural-decision authority. | RATIFIED-by-default — PM refactors §3 in subsequent commit OR canonical-ledger-landing absorbs (path-(a) decision pending; NEW 2026-05-06 from Research PM R-3) | From 405b9c085d4b6843cb1f248813dd9db6077c1681 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 06:48:49 +0000 Subject: [PATCH 11/16] docs(briefs): replace bare .md line refs with section anchors (Verification) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per Director-authorized citation discipline (#828 / checklist / 127287a66 pattern): Verification-touching briefs now cite § headings instead of file.md:NNN for cross-doc pointers. Co-authored-by: Cursor --- .../r3-v-bridge-retirement-ledger-zero-audit.md | 2 +- .../r3-v-l7-algebra-inhabitant-law-coverage-matrix.md | 11 +++++++---- docs/briefs/r3-v-witness-shape-pattern-survey.md | 6 ++++-- docs/briefs/r3-verification-manager.md | 2 +- 4 files changed, 13 insertions(+), 8 deletions(-) diff --git a/docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md b/docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md index fd1acbb645c..768836e61f3 100644 --- a/docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md +++ b/docs/briefs/r3-v-bridge-retirement-ledger-zero-audit.md @@ -34,7 +34,7 @@ disposition only. | 2 | `bridge_mark_bootstrap_secret_nominal_opacity_retired` | `Retired` | Retired. `dag.rs::bridge_mark_bootstrap_secret_nominal_opacity_retired` asserts `Secret.nominal_opacity` exists in std, full bootstrap, and without-parse-surface snapshots. No live `mark_bootstrap_secret_nominal_opacity` helper remains. | Rust unit test in `src/v3/compiler/src/dag.rs`; Secret nominal-opacity lineage #1272 / old row authority `PR #937`. | None for status. Authority string is historical but not contradictory. | | 3a | `bridge_canonical_lens_name_dispatch_pr1183_slice_retired` | Pending substrate split; ratified target `Retired` | Retired at narrow PR #1183 scope. The specific dispatch path covered by #1183 is treated as closed by Director-ratified split. | PR #1183 dispatch path; `canonical_lens_bridge_ratchet_test.rs` narrow ratchet; Director #828 c#4358798673. | None after Substrate Mgr authors the split. The prior single-row drift is resolved by class enumeration, not by treating all canonical-lens-name patching as retired. | | 3b | `bridge_canonical_lens_name_patching_residual` | Pending substrate split; ratified target `Open` | Open. `canonical_lens_bridge_ratchet_test.rs` pins two canonical-lens `include_str!` constants, two `lens_decl.name.as_deref() == Some(...)` dispatch arms, and two generic name-keyed lookups in `test_runner.rs`. Dissolution trigger: PB-Runtime interpreter-as-data or a typed lens-registry carrier. | Broader exact-string canonical-lens-name class; Director #828 c#4358798673. | None after Substrate Mgr authors the split. Until then, the live single substrate row remains coarser than the ratified class model. | -| 4 | `bridge_include_str_side_channels_retired` | `Open` | Open. `pipeline_authority.rs` explicitly says compile-body cross-check remains suspended because `fn compile` lowers to `ArrowBody::Unparsed`; the prior `include_str!`/file-read side-channel is rejected until a structural compile-body witness exists. | `design-emission-model.md:944`; `pipeline_authority.rs`; PR #1171. | None. Ledger `Open` matches code. | +| 4 | `bridge_include_str_side_channels_retired` | `Open` | Open. `pipeline_authority.rs` explicitly says compile-body cross-check remains suspended because `fn compile` lowers to `ArrowBody::Unparsed`; the prior `include_str!`/file-read side-channel is rejected until a structural compile-body witness exists. | [`design-emission-model.md`](../design-emission-model.md) §"Per Director directive 2026-04-28 (gpt-5-5-pro reflective analysis)" (`include_str!` retirement / `bridge_include_str_side_channels_retired` bullet); `pipeline_authority.rs`; PR #1171. | None. Ledger `Open` matches code. | | 5 | `bridge_exact_string_patching_residual_retired` | `Open` | Open at umbrella scope. The lower-helper sub-slice is retired and ratcheted by `bridge_lower_helpers_patch_zero_residual_test.rs`, but other exact-string patch classes remain. `bootstrap.rs::patch_kernel_bool_boolean_algebra_inhabits` is a live class-5-style residual called from bootstrap paths. | `r3-structure.md` L91; `r2-closure-ledger.md` Tier-2 row; #1014 + #1192 narrow receipt. | None. Ledger `Open` correctly refuses to treat the lower-helper sub-slice as umbrella closure. | ## Code-State Evidence diff --git a/docs/briefs/r3-v-l7-algebra-inhabitant-law-coverage-matrix.md b/docs/briefs/r3-v-l7-algebra-inhabitant-law-coverage-matrix.md index ed3adc0cc03..883aa0c11ab 100644 --- a/docs/briefs/r3-v-l7-algebra-inhabitant-law-coverage-matrix.md +++ b/docs/briefs/r3-v-l7-algebra-inhabitant-law-coverage-matrix.md @@ -11,8 +11,10 @@ variants are proposed here. - Path-grounded sources verified at HEAD with `git cat-file -e`: `dsl/std/algebra.dag`, `docs/r3-structure.md`, and `docs/briefs/r3-v-l7-algebra-coverage-matrix.md`. -- `docs/r3-structure.md:155` and `:189` expand T-V-L4-L7-Direct to exhaustive - per-(algebra, inhabitant, law) witness coverage. +- [`docs/r3-structure.md`](../r3-structure.md) §"Acceptance" — gate row + `section_ref_substrate_landed` under **T-Lens-Application-Surface**, and the + **Demonstration principle** worked-example row `crdt_cost_basis_demonstrated`, + expand T-V-L4-L7-Direct to exhaustive per-(algebra, inhabitant, law) witness coverage. - PR #1419 is the direct lineage: it authored 17 enum-backed `(algebra, law)` rows for the current `AlgebraicLawKind` surface. - `dsl/std/algebra.dag:30-47` defines the law-emergence table; @@ -29,7 +31,8 @@ variants are proposed here. The pair matrix can say "Semiring x Distributivity exists" once, but that does not prove every semiring inhabitant has a witness. The motivating bug class is PR #1430 section A / the local design receipt at -`docs/design-cost-lens-sizevar-dimension-wiring.md:233-248`: `SymbolicCost` +[`docs/design-cost-lens-sizevar-dimension-wiring.md`](../design-cost-lens-sizevar-dimension-wiring.md) +§"3.2 Where the consumer attaches in the lens": `SymbolicCost` normalization treated additive zero and multiplicative zero with one helper, so a product containing zero failed to collapse to zero. The invariant is not just "Semiring has laws"; it is "`SymbolicCost` as a Semiring inhabitant has @@ -74,7 +77,7 @@ encoding. | Int8/16/32/64/128 | Declared: `dsl/std/integer.dag:50-54`; Rust target rows mirror signed OrderedRing carriers | OrderedRing | additive commutativity Wired; multiplicative identity NYI | additive inverse, order compatibility, distributivity P1 | Fixed-width signed rows stay distinct from abstract Int after the construction-chain pivot. | | Int | Declared: `dsl/std/integer.dag:83` is `AbelianGroup>`; kernel profile still maps "Int" to OrderedRingProfile | transitional abstract integer | Abelian-group identity NYI / commutativity Wired if using current enum surface | OrderedRing/Ring residual requires cascade decision; order and distributivity P1 | Audit-sensitive: do not collapse kernel profile and construction-chain alias into one witness without a lane decision. | | Float | Profile: `kernel_algebra_profile["Float"] = ApproximateFieldProfile`; denotational Float is ApproximateField | approximate field, not exact Field | exact associativity should not be claimed for floating addition; current enum laws need approximate semantics before fixture use | approximate identity/rounding, reciprocal/division, order laws P1 | Exclude from exact L7 law closure until approximate-law substrate shape exists. | -| SymbolicCost | Candidate: `docs/design-cost-lens-sizevar-dimension-wiring.md:248-268` proposes `Semiring`; `:427-433` resolves Semiring, not CommutativeSemiring | Semiring candidate | no PR #1419 fixture row yet | annihilation/product-zero, distributivity, add/mul identity P1 | Canonical proof that per-inhabitant coverage is required; author only after the semiring declaration lands. | +| SymbolicCost | Candidate: [`design-cost-lens-sizevar-dimension-wiring.md`](../design-cost-lens-sizevar-dimension-wiring.md) §"4. SymbolicCost commutative-semiring discipline (product-zero bug class)" proposes `Semiring`; §"8.3 `Dimension` declaration scope for slice 2" resolves Semiring, not CommutativeSemiring | Semiring candidate | no PR #1419 fixture row yet | annihilation/product-zero, distributivity, add/mul identity P1 | Canonical proof that per-inhabitant coverage is required; author only after the semiring declaration lands. | ## Implications for PR #1419 Fixture Lineage diff --git a/docs/briefs/r3-v-witness-shape-pattern-survey.md b/docs/briefs/r3-v-witness-shape-pattern-survey.md index abf8ceff674..c6d434ddfe3 100644 --- a/docs/briefs/r3-v-witness-shape-pattern-survey.md +++ b/docs/briefs/r3-v-witness-shape-pattern-survey.md @@ -156,8 +156,10 @@ structural comparison rather than shape-valid `NotYetImplemented`. Lane 1 and Lane 2 are runtime/corpus patterns, not `Lens` instances. Lane 1 L4 and L7 are still pending R3 implementation work per -`docs/v3-modeling-analysis.md:1774-1777` and -`docs/thesis/r2-r3-thesis-mapping.md:65-68`. The live runner surfaces listed +[`docs/v3-modeling-analysis.md`](../v3-modeling-analysis.md) §"Tier 3 — Verification from structure" +(L4–L7 status rows) and +[`docs/thesis/r2-r3-thesis-mapping.md`](../thesis/r2-r3-thesis-mapping.md) §"Disposition table — Tier 3 (Verification from structure)" +(L4 / L7 disposition rows). The live runner surfaces listed above are scaffolds, not closure claims. L4 is expected to use `DifferentialEquals` over `rust_emit_output` and `dag_eval_output`; `dag_eval_output` still requires real PR-B body evaluation, and the failure diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index d533735dabc..e92765f2f1f 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/docs/briefs/r3-verification-manager.md @@ -34,7 +34,7 @@ Per [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" T-Bridge-Ret | 1 | `SourceSpan.file` participation checks | **Substrate** | **R3-deferred** | #1273 STOP+PING audit landed; #1130 Director acceptance — partial string-check retirement rejected; structural prerequisites named (module/compilation-unit identity for lens reflection; typed authority/emit-scope carriers for lower/emit). Per [`r3-structure.md`](../r3-structure.md) §"Lane structure" T-Bridge-Retirement row item (1). | | 2 | `mark_bootstrap_secret_nominal_opacity()` | **Substrate** | **retired** | #1272 (refactor(v3): retire Secret bootstrap opacity bridge). | | 3 | Canonical lens-name dispatch | **PB** | **slice landed; ledger-zero pending** | #1183 — narrow-scope canonical lens-name dispatch slice. Broader exact-string lens-name patching not yet structurally retired. | -| 4 | `include_str!` side channels (e.g., `pipeline_authority.rs`) | **PB** | **outstanding-or-waiting** | #1171 suspended `reconcile_with_compile_body` rather than swapping `include_str!` for runtime file IO; **`bridge_include_str_side_channels_retired` still open** per [`docs/design-emission-model.md:944`](../design-emission-model.md). Awaits derivation or structural compile-body witness. | +| 4 | `include_str!` side channels (e.g., `pipeline_authority.rs`) | **PB** | **outstanding-or-waiting** | #1171 suspended `reconcile_with_compile_body` rather than swapping `include_str!` for runtime file IO; **`bridge_include_str_side_channels_retired` still open** per [`design-emission-model.md`](../design-emission-model.md) §"Per Director directive 2026-04-28 (gpt-5-5-pro reflective analysis)" (`include_str!` retirement bullet). Awaits derivation or structural compile-body witness. | | 5 | `patch_lower_helpers_*` residual | **PB** | **slice landed; narrow scope** | #1014 (first slice — generated field native) + #1192 (`bridge_lower_helpers_patch_zero_residual_test.rs` — narrow ratchet-zero). Broader exact-string patching outside this slice not claimed retired. | **Net position:** 1 retired (#1272), 2 narrow slices landed (#1183 canonical lens / #1014 + #1192 lower-helper), 1 outstanding (#1171 suspended `reconcile_with_compile_body` only — `bridge_include_str_side_channels_retired` still open; tracked separately by closure-ledger update #1283), 1 R3-deferred (#1273). **Unified `bridge_retirement_ledger_zero` gate remains open** until all 5 fire structurally — row stays in-flight per closure ledger discipline. From a0d849bccb20e1dcbdc851c3161cb5141738496e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 03:06:21 -0400 Subject: [PATCH 12/16] WIP: R3 Verification --- docs/briefs/r3-v-pattern-a-tc1-v1-worker.md | 67 +++++++++++++++++++ ...3-v-tc1-eta-equivalence-deeper-analysis.md | 14 ++-- 2 files changed, 72 insertions(+), 9 deletions(-) create mode 100644 docs/briefs/r3-v-pattern-a-tc1-v1-worker.md diff --git a/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md new file mode 100644 index 00000000000..57bb06a622c --- /dev/null +++ b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md @@ -0,0 +1,67 @@ +# R3 Pattern-A — TC1 first executable slice (V1) Worker Brief + +**Status:** DISPATCH-READY — **Q-PAFS Path A ACCEPTED** 2026-05-06 (Brian Director countersign; PR #1824). Policy-layer fork closed; implementation still coordinates **Evaluator E3** (**E6-G1.a** static lens fold) in the **same release step** as this slice. + +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — absorbed formal-grounding / Pattern-A cluster (not a fourth lane; see `r3-structure.md` §"Manager structure"). + +**Ratified scope authority:** [`docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md`](r3-v-tc1-eta-equivalence-deeper-analysis.md) §"DESIGN — Q-PAFS first executable slice (Pattern-A / TC1)" **Path A** — TC1 **static representative** via **E6-G1.a** (finite Director-visible lens set + fixed eta pair; `BinaryDimensionReportEquals` consumer envelope per [`docs/briefs/r3-v-pattern-a-coverage-rollup.md`](r3-v-pattern-a-coverage-rollup.md)). + +**Program plan:** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 rows **Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, **Q-EVAL-Lens-Fold-First-Slice** — **ACCEPTED 2026-05-06 (Path A / G1.a)**. + +## §1.8 closure predicate (this slice) + +| Gate ID | Gate name (canonical) | Target transition | +| --- | --- | --- | +| **#11** | `tc1_eta_equivalence_executable` | **DECLARED → CONSUMER_LANDED** when executable `TestClaim` + runner path land per this brief; **PASSING** when strict-fire evaluates green on CI. | + +Gates **#12–#14** (TC2 / TC3 / RustDagIsomorphism executables) stay **DECLARED** until their **separate** worker dispatches; **do not** fold them into this PR. + +## Worker pin (Verification Mgr partition) + +| Preference | Worker | Condition | +| --- | --- | --- | +| **Primary** | **bold-crane-790** ([gunbc#1748](https://github.com/gunb-ai/gunbc/issues/1748)) | When child session is active **and** **V6** (`bridge_retirement_ledger_zero` audit cadence) reaches a **clean checkpoint** acceptable to Verification Mgr — then route **V1** implementation PR(s) through bold-crane. | +| **Alternate** | **New worker** (spawn per `feedback_idle_workers_dispatchable_directly`) | If bold-crane remains saturated on **V6** or session stays archived — do **not** block V1 on crane availability; Brian / Director staffing read authorizes substitute. | + +**cool-heron-521** remains on **V2 / V4 / V5** prep per partition; **not** the default home for V1 unless explicitly redirected. + +## Scope (in) + +- First **executable** TC1 slice under **Path A** only: static representative **E6-G1.a**; consumer remains **`BinaryDimensionReportEquals`** over two typed `DimensionReport` reports once producers exist. +- Verification-owned: **TestClaim** wiring, integration tests, fixture **naming** for strict-fire slice, and **coverage** of the ratified representative set (no universal quantification in V1). +- Coordinated same-step landing of **Evaluator E3** / **E6-G1.a** (Evaluator Mgr [#1743](https://github.com/gunb-ai/gunbc/issues/1743)) — Verification does **not** own evaluator internals; this brief names the **interface** dependency. + +## Scope (out) — STOP+PING + +Hold **without** widening by inertia: + +| Item | Discipline | +| --- | --- | +| **Path B** (TC1 generic **E6-G1.b / X1.b**) | **Deferred-not-blocked** — out of **V1** scope; separate ratchet after Path A is green or Director reprioritizes. | +| **`SubstrateResearchDeferredClaim` widening** | **STOP+PING** until a **separate** Substrate-routed PR explicitly authorizes carrier shape — V1 does **not** reuse deferred carrier as strict-fire. | +| **Deferred TC1 fixture hard activation** | **STOP+PING** — `tc1_substrate_lens_eta_equivalence_deferred.dag` stays the staging fixture until strict-fire fixture + routing land via implementation PR; no silent runner widening. | +| **New substrate / evaluator predicate shapes** | **STOP+PING** — INVARIANTS §P1 + Substrate Mgr authority; Verification consumes unified **`BinaryDimensionReportEquals`** surface per Director ratification at [#828](https://github.com/gunb-ai/gunbc/issues/828). | + +## Dependencies (hard) + +| Dependency | Owner | Why | +| --- | --- | --- | +| **E6-G1.a static lens fold** | Evaluator Mgr | Two structurally named programs produce typed `DimensionReport` through evaluator-owned fold — **same release step** as V1 slice per ACCEPTED bundle. | +| **T-Substrate-Lens-Primitive + lens producer retirement progress** | Substrate / PB lanes | Path A assumes existing fold machinery; no parallel `lens_apply` interpretation for the fold receipts. | +| **Representative lens set + eta pair declaration refs** | Substrate (facts) + Verification (fixture refs) | Finite, Director-visible set enumerated in `.dag` / declarations — not “all `Lens`” in V1. | + +## Implementation slices (suggested PR shape) + +1. **Slice 1 — wiring receipt:** Substrate + Evaluator land minimal producers/refs so both `DimensionReport` sides are **typed** and **lifted** per Evaluator #1131 safe contract (no fixture-local producer identity). +2. **Slice 2 — executable `TestClaim`:** `tc1_eta_equivalence_executable` (or ratified final name per §1.8 ledger) + suite row; integration test exercises **Pass** on representative set. +3. **Slice 3 — ledger / doc receipt:** Update §1.8 **Status** column **DECLARED → CONSUMER_LANDED → PASSING** as CI proves; cross-link [`docs/briefs/r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) absorbed-responsibility audit row for TC1. + +Single PR per `feedback_brief_pr_cadence` if possible; if Substrate and Verification diffs must split, **Substrate lands first** — Verification PR must not invent carrier shapes. + +## Cross-refs + +- Analysis + Path A: [`r3-v-tc1-eta-equivalence-deeper-analysis.md`](r3-v-tc1-eta-equivalence-deeper-analysis.md) +- Roll-up consumer envelope: [`r3-v-pattern-a-coverage-rollup.md`](r3-v-pattern-a-coverage-rollup.md) +- Formal-grounding bundle (audit cadence): [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) +- Deferred staging fixture: `src/v3/compiler/tests/fixtures/tc1_substrate_lens_eta_equivalence_deferred.dag` +- Evaluator coordination: [gunbc#1743](https://github.com/gunb-ai/gunbc/issues/1743) diff --git a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md index e9262a8c01c..aa053de7e5b 100644 --- a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md +++ b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md @@ -1,20 +1,16 @@ # R3 TC1 Eta-Equivalence Deeper Structural Verification Analysis -**Status:** **DESIGN** (2026-05-06). Verification Mgr engineering choice among Pattern-A -first-slice paths; **not** yet **ACCEPTED** (Director countersignature still required per -`docs/r3-program-plan.md` §10.3 **Q-PAFS** and Brian directive: PROPOSAL → DESIGN → -ACCEPTED). +**Status:** **ACCEPTED** (2026-05-06 — Brian Director countersign: Path **A** / **G1.a**). Bundled with [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 **Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, and **Q-EVAL-Lens-Fold-First-Slice** (PR [#1824](https://github.com/gunb-ai/gunbc/pull/1824)). **Worker dispatch:** [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md). **Lifecycle** | Stage | Meaning | | --- | --- | -| PROPOSAL | Exploratory surface map only (superseded by this revision). | -| **DESIGN** (here) | Chooses a concrete first-slice shape, defers alternatives, states runtime prereqs and scope deltas. | -| ACCEPTED | Director/Brian countersign; authorizes implementation dispatch (V1 TC1 executable slice + Evaluator **E6-G1.a** lens-fold first slice in lockstep). | +| PROPOSAL | Exploratory surface map only (superseded). | +| DESIGN | Path A / B / C resolution recorded 2026-05-06 (superseded as policy stage by ACCEPTED). | +| **ACCEPTED** (here) | Path **A** ratified — implementation authorized in lockstep with Evaluator **E3** (**E6-G1.a**). | -TC1 deferred fixture remains **as-is** until ACCEPTED + routed implementation; this brief -still does **not** authorize substrate, runner, or fixture edits by itself. +This brief binds **Verification policy scope**; executable routing + carrier shapes land via coordinated PRs (see worker brief). **Do not** treat ACCEPTED as permission to widen `SubstrateResearchDeferredClaim` or activate strict-fire fixtures without those PRs. **Owning manager:** R3 Verification Manager, absorbed formal-grounding responsibility. From 41754b311d75750a808a9bfab101bade513dba46 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 07:12:50 +0000 Subject: [PATCH 13/16] =?UTF-8?q?docs(r3):=20fix=20Codex=20BLOCKING=20?= =?UTF-8?q?=E2=80=94=20L7=20matrix=20cites=20T-V-L4-L7-Direct;=20sync=20Q-?= =?UTF-8?q?PAFS=20ACCEPTED?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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 --- ...3-v-l7-algebra-inhabitant-law-coverage-matrix.md | 5 +---- docs/briefs/r3-v-pattern-a-tc1-v1-worker.md | 2 +- .../r3-v-tc1-eta-equivalence-deeper-analysis.md | 13 +++++++++---- docs/briefs/r3-verification-manager.md | 1 + docs/r3-program-plan.md | 6 +++--- 5 files changed, 15 insertions(+), 12 deletions(-) diff --git a/docs/briefs/r3-v-l7-algebra-inhabitant-law-coverage-matrix.md b/docs/briefs/r3-v-l7-algebra-inhabitant-law-coverage-matrix.md index 883aa0c11ab..3ce7ca3309f 100644 --- a/docs/briefs/r3-v-l7-algebra-inhabitant-law-coverage-matrix.md +++ b/docs/briefs/r3-v-l7-algebra-inhabitant-law-coverage-matrix.md @@ -11,10 +11,7 @@ variants are proposed here. - Path-grounded sources verified at HEAD with `git cat-file -e`: `dsl/std/algebra.dag`, `docs/r3-structure.md`, and `docs/briefs/r3-v-l7-algebra-coverage-matrix.md`. -- [`docs/r3-structure.md`](../r3-structure.md) §"Acceptance" — gate row - `section_ref_substrate_landed` under **T-Lens-Application-Surface**, and the - **Demonstration principle** worked-example row `crdt_cost_basis_demonstrated`, - expand T-V-L4-L7-Direct to exhaustive per-(algebra, inhabitant, law) witness coverage. +- [`docs/r3-structure.md`](../r3-structure.md) §"Summary" — numbered lane **T-Verification-L4-L7-Direct** (L4 emit/eval match + L7 algebraic-law witnesses; **scope expanded 2026-05-02**: per-(algebra, inhabitant, law) witness coverage exhaustive), **and** §"Plus 3 fold-ins (no new lanes; Director-ratified 2026-05-02)" — bullet **T-V-L4-L7-Direct exhaustive witness coverage** (`l7_algebraic_laws_witnessed` catches per-inhabitant bug classes such as SymbolicCost product-zero per PR #1430 §A). **Acceptance gate row** for the same lane: §"Acceptance — `.dag` gates"` sub-list **T-Verification-L4-L7-Direct** — `l7_algebraic_laws_witnessed`. - PR #1419 is the direct lineage: it authored 17 enum-backed `(algebra, law)` rows for the current `AlgebraicLawKind` surface. - `dsl/std/algebra.dag:30-47` defines the law-emergence table; diff --git a/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md index 57bb06a622c..d5f1719afa8 100644 --- a/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md +++ b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md @@ -2,7 +2,7 @@ **Status:** DISPATCH-READY — **Q-PAFS Path A ACCEPTED** 2026-05-06 (Brian Director countersign; PR #1824). Policy-layer fork closed; implementation still coordinates **Evaluator E3** (**E6-G1.a** static lens fold) in the **same release step** as this slice. -**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — absorbed formal-grounding / Pattern-A cluster (not a fourth lane; see `r3-structure.md` §"Manager structure"). +**Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — absorbed formal-grounding / Pattern-A cluster (not a fourth lane; see [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure"). **Ratified scope authority:** [`docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md`](r3-v-tc1-eta-equivalence-deeper-analysis.md) §"DESIGN — Q-PAFS first executable slice (Pattern-A / TC1)" **Path A** — TC1 **static representative** via **E6-G1.a** (finite Director-visible lens set + fixed eta pair; `BinaryDimensionReportEquals` consumer envelope per [`docs/briefs/r3-v-pattern-a-coverage-rollup.md`](r3-v-pattern-a-coverage-rollup.md)). diff --git a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md index aa053de7e5b..eef5aacc593 100644 --- a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md +++ b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md @@ -1,6 +1,11 @@ # R3 TC1 Eta-Equivalence Deeper Structural Verification Analysis -**Status:** **ACCEPTED** (2026-05-06 — Brian Director countersign: Path **A** / **G1.a**). Bundled with [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 **Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, and **Q-EVAL-Lens-Fold-First-Slice** (PR [#1824](https://github.com/gunb-ai/gunbc/pull/1824)). **Worker dispatch:** [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md). +**Status:** **ACCEPTED** (2026-05-06 — Brian Director countersign: Path **A** / **G1.a**). +**Canonical ratification:** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 rows +**Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, and **Q-EVAL-Lens-Fold-First-Slice** (PR +[#1824](https://github.com/gunb-ai/gunbc/pull/1824) lands the table receipt). This brief +is the **engineering scope narrative** aligned to that row. **Worker dispatch:** +[`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md). **Lifecycle** @@ -144,9 +149,9 @@ Verification drift. | RustDagIsomorphism before TC1? | **Not** under Q-PAFS default; **Path C** only with Director reorder. | | Universal vs representative for first fire? | **Representative finite set** for slice one; universal quantification is a **later** ratchet question (see Open Questions). | -**Surface for Director countersign (ACCEPTED):** Path A as written + explicit acknowledgment -that PM default and **DESIGN** engineering choice align; any deviation (e.g., Path C first) -is Director-owned scope calibration. +**ACCEPTED (2026-05-06):** Path **A** countersigned by Brian ("approved path A countersign"); +program-plan §10.3 rows updated; any deviation from Path A (e.g., Path C first) is a new +Director/Brian scope calibration — not silent Verification drift. ## Lens-Framework Anchors diff --git a/docs/briefs/r3-verification-manager.md b/docs/briefs/r3-verification-manager.md index e92765f2f1f..455ac9b5ad3 100644 --- a/docs/briefs/r3-verification-manager.md +++ b/docs/briefs/r3-verification-manager.md @@ -95,6 +95,7 @@ Each lane closes under a structural acceptance gate authored as a `.dag` `TestCl - [`r3-v-l4-l7-direct-worker.md`](r3-v-l4-l7-direct-worker.md) — Lane 1 standby brief. - [`r3-v-l5-corpus-worker.md`](r3-v-l5-corpus-worker.md) — Lane 2 standby brief. - [`r3-v-free-consequences-worker.md`](r3-v-free-consequences-worker.md) — Lane 3 standby brief. +- [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md) — Pattern-A V1 (TC1 first executable slice; Q-PAFS Path A **ACCEPTED** 2026-05-06). - [`r3-v-formal-grounding-tc-bundle.md`](r3-v-formal-grounding-tc-bundle.md) — absorbed-responsibility TC1/TC2/TC3 bundle (NOT a lane; audit-cadence artifact per `r3-structure.md` §"Manager structure" Item 2 3-lane authority). **Pending (post-spawn manager authors autonomously):** diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 4834532b1cf..1fc0ea19147 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -950,7 +950,7 @@ Substrate canvas + plan-poke-hole both folded in. Key absorptions: | ID | Question | PM recommendation (applied as default) | Status | |---|---|---|---| -| Q-PAFS | Which Pattern-A (DimensionReport-typed family) first executable slice (TC1 vs RustDagIsomorphism vs other) | **TC1 first slice = static representative via E6-G1.a (Path A)** — `docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md` advanced to **DESIGN** (2026-05-06): Path B (TC1 generic G1.b / X1.b) **deferred**; Path C (RustDagIsomorphism before TC1) **not** under Q-PAFS default (Director reorder only). PM default and Verification Mgr engineering choice **align on Path A**. **ACCEPTED 2026-05-06** per Brian directive ("approved path A countersign"). | **ACCEPTED 2026-05-06 (Path A)** — V1 first executable Pattern-A slice (TC1) + Evaluator E3 (E6-G1.a static lens fold) implementation dispatch unblocked simultaneously. Path B / Path C remain deferred-not-blocked. | +| Q-PAFS | Which Pattern-A (DimensionReport-typed family) first executable slice (TC1 vs RustDagIsomorphism vs other) | **TC1 first slice = static representative via E6-G1.a (Path A)** — `docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md`: **DESIGN → ACCEPTED** (2026-05-06): Path B (TC1 generic G1.b / X1.b) **deferred**; Path C (RustDagIsomorphism before TC1) **not** under Q-PAFS default (Director reorder only). PM default and Verification Mgr engineering choice **align on Path A**. **ACCEPTED 2026-05-06** per Brian directive ("approved path A countersign"). Canonical row authority: this table + PR #1824 receipt. | **ACCEPTED 2026-05-06 (Path A)** — V1 first executable Pattern-A slice (TC1) + Evaluator E3 (E6-G1.a static lens fold) implementation dispatch unblocked simultaneously. Path B / Path C remain deferred-not-blocked. | | Q-NYI-Accounting | NYI claim coverage/completeness accounting | Mark NYI incomplete in aggregation reporting; ratchet to executable per evaluator-slice landing | RATIFIED-by-default | | Q-Std-Carrier-Phasing | Rust std-carrier phasing (Option/Cardinal/HigherOrderMethodSpec/allocator-hasher) | Phase 1 = default-only/default-instance; later phases as separate Substrate slices post-Phase-1 | RATIFIED-by-default | | Q-Drift-Reconcile | Drift items routing (#1638, #1499, declaration_by_name) | Single Debt-Paydown worker reconciles all three → one PR closing rows in ledger + ROADMAP | RATIFIED-by-default | @@ -960,10 +960,10 @@ Substrate canvas + plan-poke-hole both folded in. Key absorptions: | Q-PR-Anticipation-Gate | Add `pr_anticipation_discipline_ci_active` closure gate (CI verifiably enforcing §7 anticipation discipline) | Add to §1 closure-gate set; owner R3 Debt-Paydown Mgr (already routed at #1744 #issuecomment-4383628247); fires when `scripts/check-pr-sg0-net-shrink-discipline.sh` is in CI workflow + self-test passes | RATIFIED-by-default (per Director poke-hole 2026-05-06 finding 3.2) | | Q-PR-F | PR-F priority + sequencing (BoundDeclaration consumer + Rust ReferenceModel) | **Bandwidth-aware dispatch** (per Substrate Mgr poke-hole 2026-05-06 Y3 — Substrate's queued workers are saturated): PR-F is 2-axis substantial work. Per Substrate Mgr canvas D: only loyal-wolf + valiant-ant fully idle; proud-lynx/smart-ram/valiant-ibex holding on #1794 cascade. Dispatch worker = loyal-wolf-828 OR valiant-ant-72 (Substrate Mgr selects); brief shape = T-E-P-Producer-Broadening adjacent (per `docs/briefs/r3-t-e-p-producer-broadening-worker.md` precedent); critical-path slot = post-#1782 wait-window close + parallel to T-E-P dispatch (B3). Substrate Mgr authors brief + dispatches. | RATIFIED-by-default-with-bandwidth-routing | | Q-Workflow-As-Data-Carriers | Substrate carriers for CI-workflow-as-`.dag`-data Class 4 closure path: `WorkflowTrigger` sum + `WorkflowStep`/`WorkflowMatrix` step-graph + `WorkflowSecret` binding + `RunnerResource` + `Workflow` composing carrier | Substrate Mgr authors carriers as part of T-Workflow-As-Data lane; sequenced post-T-Lens-Behavioral-Parity COMPLETE (per `r3-structure.md` §"Dependency on R2"); folds into existing T-Workflow-As-Data scope without new lane spawn. Required for Class 4 substrate-gap-class closure per §1.4. | OPEN — Substrate Mgr scoping needed (NEW 2026-05-06 from Substrate Mgr poke-hole R3) | -| Q-Pattern-A-First-Slice-Subscope | Q-PAFS sub-question: TC1 first means **static representative** (E6-G1.a) or **generic** (E6-G1.b/X1.b)? Plan defaulted to TC1 first without specifying which sub-shape. Per Evaluator Mgr F1 + EVAL-3: substantial substrate/evaluator scope difference. | Per `docs/briefs/r3-v-pattern-a-coverage-rollup.md` + Evaluator Mgr canvas: TC1-static-representative via E6-G1.a is achievable with current evaluator + lens-fold infrastructure; TC1-generic requires X1.b S1/S3 + G1.b. PM-recommended: **TC1-static-representative first** (smallest viable slice); generic deferred to subsequent ratchet. **Verification Mgr DESIGN** (`r3-v-tc1-eta-equivalence-deeper-analysis.md`, 2026-05-06) ratifies **G1.a static representative first**. **ACCEPTED 2026-05-06** with Q-PAFS bundle per Brian directive ("approved path A countersign"). | **ACCEPTED 2026-05-06 (G1.a static representative)** — bundled with Q-PAFS / Q-EVAL-Lens-Fold-First-Slice; TC1-generic via X1.b S1/S3 + G1.b deferred-not-blocked. | +| Q-Pattern-A-First-Slice-Subscope | Q-PAFS sub-question: TC1 first means **static representative** (E6-G1.a) or **generic** (E6-G1.b/X1.b)? Plan defaulted to TC1 first without specifying which sub-shape. Per Evaluator Mgr F1 + EVAL-3: substantial substrate/evaluator scope difference. | Per `docs/briefs/r3-v-pattern-a-coverage-rollup.md` + Evaluator Mgr canvas: TC1-static-representative via E6-G1.a is achievable with current evaluator + lens-fold infrastructure; TC1-generic requires X1.b S1/S3 + G1.b. PM-recommended: **TC1-static-representative first** (smallest viable slice); generic deferred to subsequent ratchet. **Verification analysis brief** (`r3-v-tc1-eta-equivalence-deeper-analysis.md`, 2026-05-06): **DESIGN → ACCEPTED** ratifies **G1.a static representative first**. **ACCEPTED 2026-05-06** with Q-PAFS bundle per Brian directive ("approved path A countersign"). | **ACCEPTED 2026-05-06 (G1.a static representative)** — bundled with Q-PAFS / Q-EVAL-Lens-Fold-First-Slice; TC1-generic via X1.b S1/S3 + G1.b deferred-not-blocked. | | Q-EVAL-G0d-Dispatch | E6-G0d constructor runtime execution: authorize evaluator slice for non-Arrow constructor `Callable` using `Value::RecordValue` / `Value::VariantValue` + shared substrate declaration-walk authority | Evaluator Mgr (merry-gull-128) dispatches; Director needed only if shared helper extraction crosses ownership. Brief at `docs/briefs/r3-pr-e6-g0d-constructor-runtime-execution-worker.md` ready. | RATIFIED-by-default — Evaluator Mgr executes (NEW 2026-05-06 from Evaluator Mgr EVAL-1) | | Q-EVAL-Descent-Termination-Contract | E5 `LoopBound::Descent` execution: substrate carrier `descent_execution_proof(&Dag, ClusterId, PortId) -> Result` with `Missing \| Unknown \| Incomplete \| NonStrict` fail-closed residuals | Substrate Mgr authors carrier (quick-koi-190 implementation already authorized through quick-crab); Evaluator consume-side ack; sharp-ibex consumer wiring dispatch. | RATIFIED-by-default — Substrate-side already authorized; Evaluator consume-side dependency (NEW 2026-05-06 from Evaluator Mgr EVAL-2) | -| Q-EVAL-Lens-Fold-First-Slice | Overlaps with Q-Pattern-A-First-Slice-Subscope: E6-G1.a static representative vs G1.b generic for first executable lens/report slice | Same recommendation as Q-Pattern-A-First-Slice-Subscope: **G1.a static-representative first**; G1.b generic deferred. **Verification Mgr DESIGN** (`r3-v-tc1-eta-equivalence-deeper-analysis.md`, 2026-05-06) locks the same **G1.a** first-slice shape for Evaluator E3 sequencing. **ACCEPTED 2026-05-06** with Q-PAFS bundle per Brian directive ("approved path A countersign"). | **ACCEPTED 2026-05-06 (G1.a)** — Evaluator E3 (E6-G1.a static lens fold) implementation dispatch unblocked; G1.b generic deferred-not-blocked. | +| Q-EVAL-Lens-Fold-First-Slice | Overlaps with Q-Pattern-A-First-Slice-Subscope: E6-G1.a static representative vs G1.b generic for first executable lens/report slice | Same recommendation as Q-Pattern-A-First-Slice-Subscope: **G1.a static-representative first**; G1.b generic deferred. **Verification analysis brief** (`r3-v-tc1-eta-equivalence-deeper-analysis.md`, 2026-05-06): **DESIGN → ACCEPTED** locks the same **G1.a** first-slice shape for Evaluator E3 sequencing. **ACCEPTED 2026-05-06** with Q-PAFS bundle per Brian directive ("approved path A countersign"). | **ACCEPTED 2026-05-06 (G1.a)** — Evaluator E3 (E6-G1.a static lens fold) implementation dispatch unblocked; G1.b generic deferred-not-blocked. | | Q-Class-6-Substrate-Extension-Lens | 3 ctrl-side substrate proposals (`SchemaPreservation` per ctrl#370/#407 LLVM TBAA; `ResourceCap` per ctrl#404/#405 Cloudflare; `TotalResult` per ctrl#404/#405) don't fit Classes 1-5; PM-side routing to Substrate Mgr (#1130) committed per ctrl#408 §3 | PER Brian no-post-R3-deferral discipline: include as Class 6 substrate-gap-class with closure-criterion. Add §4.6 "Class 6 — typed-metadata-preservation / extension-lens slice" with representative gap-test per substrate. Alternative: Director ratification of explicit post-R3-ecosystem-by-design scope-cession. **Director disposition 2026-05-06 at gunbc#828 #issuecomment-4384615320: HOLD pending more context** — needs (i) which proposals are R3-blocking vs nice-to-have; (ii) substrate-author capacity for the 3 carriers; (iii) cross-lane cascade implications. PM surfaces from Research PM with sharper framing before Director ratification. | HOLD pending Research PM sharper framing (Director disposition; NEW 2026-05-06 from Research PM R-1) | | Q-Timeline-Risk-Alternates | §6 8-12 week estimate is commitment, not bottoms-up derivation. Missing risk-weighted alternates for: C1-class candidate-gap budget (2-6 weeks/gap) + WEDGE-CORE-CLAIM Part A thesis-edit scope + ~9 demo-gate authoring (1-3 weeks/lane) | Per `feedback_holistic_over_patches`: §9.2 add explicit "+X weeks if {C1-gap surfaces / Tier-4 thesis-edit lands in scope / demo authoring exceeds budget}" branches. R3 close horizon: 2026-08-01 ± 2 weeks PROVISIONAL → range with explicit risk-weighted alternates. | RATIFIED-by-default — PM updates §9.2 with risk-weighted branches in subsequent commit (NEW 2026-05-06 from Research PM R-2) | | Q-Plan-vs-Structure-Drift-Discipline | §3 lane status table holds 19 rows replicating r3-structure.md §"Lane structure" data; drift risk if PM updates one but not the other | Per Research PM R-3 recommendation (a): §3 lane status becomes pointer-with-delta to r3-structure.md §"Lane structure" + delta-only annotations (current dispatch + blocker + ETA). Lane name/Mgr/scope columns NOT restated; r3-structure.md retains architectural-decision authority. | RATIFIED-by-default — PM refactors §3 in subsequent commit OR canonical-ledger-landing absorbs (path-(a) decision pending; NEW 2026-05-06 from Research PM R-3) | From cdd5c4ca4b19b10e7aae1b1bd59470cdb11a64b4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 07:22:39 +0000 Subject: [PATCH 14/16] docs(briefs): clarify r3-program-plan path for TC1 ACCEPTED authority link Co-authored-by: Cursor --- docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md index eef5aacc593..9649c4f3908 100644 --- a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md +++ b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md @@ -3,8 +3,11 @@ **Status:** **ACCEPTED** (2026-05-06 — Brian Director countersign: Path **A** / **G1.a**). **Canonical ratification:** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 rows **Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, and **Q-EVAL-Lens-Fold-First-Slice** (PR -[#1824](https://github.com/gunb-ai/gunbc/pull/1824) lands the table receipt). This brief -is the **engineering scope narrative** aligned to that row. **Worker dispatch:** +[#1824](https://github.com/gunb-ai/gunbc/pull/1824) lands the table receipt). **Path +check:** ratification lives in the committed file `docs/r3-program-plan.md`; from this +brief the relative link `../r3-program-plan.md` resolves to that path (same `docs/` +directory as `docs/briefs/`). This brief is the **engineering scope narrative** aligned +to that row. **Worker dispatch:** [`r3-v-pattern-a-tc1-v1-worker.md`](r3-v-pattern-a-tc1-v1-worker.md). **Lifecycle** From 0808cacc3ba7604b8617e50d0e5a546abb01079c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 07:52:15 +0000 Subject: [PATCH 15/16] =?UTF-8?q?docs(r3):=20single=20authority=20for=20Q-?= =?UTF-8?q?PAFS=20ACCEPTED=20=E2=80=94=20plan=20=C2=A710.3=20at=20HEAD?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 #1824 is merge-record only. --- docs/briefs/r3-v-pattern-a-tc1-v1-worker.md | 2 +- docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md | 9 ++++++--- docs/r3-program-plan.md | 2 +- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md index d5f1719afa8..61538dafc6f 100644 --- a/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md +++ b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md @@ -1,6 +1,6 @@ # R3 Pattern-A — TC1 first executable slice (V1) Worker Brief -**Status:** DISPATCH-READY — **Q-PAFS Path A ACCEPTED** 2026-05-06 (Brian Director countersign; PR #1824). Policy-layer fork closed; implementation still coordinates **Evaluator E3** (**E6-G1.a** static lens fold) in the **same release step** as this slice. +**Status:** DISPATCH-READY — **Q-PAFS Path A ACCEPTED** 2026-05-06 (Brian Director countersign; **authority** = committed [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 rows at `HEAD`; PR [#1824](https://github.com/gunb-ai/gunbc/pull/1824) is the **merge record** on `main`). Policy-layer fork closed; implementation still coordinates **Evaluator E3** (**E6-G1.a** static lens fold) in the **same release step** as this slice. **Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — absorbed formal-grounding / Pattern-A cluster (not a fourth lane; see [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure"). diff --git a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md index 9649c4f3908..ffdfe1252e1 100644 --- a/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md +++ b/docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md @@ -1,9 +1,12 @@ # R3 TC1 Eta-Equivalence Deeper Structural Verification Analysis **Status:** **ACCEPTED** (2026-05-06 — Brian Director countersign: Path **A** / **G1.a**). -**Canonical ratification:** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 rows -**Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, and **Q-EVAL-Lens-Fold-First-Slice** (PR -[#1824](https://github.com/gunb-ai/gunbc/pull/1824) lands the table receipt). **Path +**Canonical ratification:** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 — rows +**Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, and **Q-EVAL-Lens-Fold-First-Slice** +(**ACCEPTED** 2026-05-06, Path **A**). **Sole authority** = the committed §10.3 table at +repo `HEAD` (not any PR description). PR [#1824](https://github.com/gunb-ai/gunbc/pull/1824) +is the **merge record** that landed the countersign row text on `main`; later PRs only +edit surrounding briefs/citations. **Path check:** ratification lives in the committed file `docs/r3-program-plan.md`; from this brief the relative link `../r3-program-plan.md` resolves to that path (same `docs/` directory as `docs/briefs/`). This brief is the **engineering scope narrative** aligned diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 4ce48619178..e50fd04129d 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -950,7 +950,7 @@ Substrate canvas + plan-poke-hole both folded in. Key absorptions: | ID | Question | PM recommendation (applied as default) | Status | |---|---|---|---| -| Q-PAFS | Which Pattern-A (DimensionReport-typed family) first executable slice (TC1 vs RustDagIsomorphism vs other) | **TC1 first slice = static representative via E6-G1.a (Path A)** — `docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md`: **DESIGN → ACCEPTED** (2026-05-06): Path B (TC1 generic G1.b / X1.b) **deferred**; Path C (RustDagIsomorphism before TC1) **not** under Q-PAFS default (Director reorder only). PM default and Verification Mgr engineering choice **align on Path A**. **ACCEPTED 2026-05-06** per Brian directive ("approved path A countersign"). Canonical row authority: this table + PR #1824 receipt. | **ACCEPTED 2026-05-06 (Path A)** — V1 first executable Pattern-A slice (TC1) + Evaluator E3 (E6-G1.a static lens fold) implementation dispatch unblocked simultaneously. Path B / Path C remain deferred-not-blocked. | +| Q-PAFS | Which Pattern-A (DimensionReport-typed family) first executable slice (TC1 vs RustDagIsomorphism vs other) | **TC1 first slice = static representative via E6-G1.a (Path A)** — `docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md`: **DESIGN → ACCEPTED** (2026-05-06): Path B (TC1 generic G1.b / X1.b) **deferred**; Path C (RustDagIsomorphism before TC1) **not** under Q-PAFS default (Director reorder only). PM default and Verification Mgr engineering choice **align on Path A**. **ACCEPTED 2026-05-06** per Brian directive ("approved path A countersign"). **Canonical row authority:** the **committed text of this §10.3 table** at repo `HEAD` (PR #1824 is the **merge record** for the countersign landing on `main`, not a second source of truth). | **ACCEPTED 2026-05-06 (Path A)** — V1 first executable Pattern-A slice (TC1) + Evaluator E3 (E6-G1.a static lens fold) implementation dispatch unblocked simultaneously. Path B / Path C remain deferred-not-blocked. | | Q-NYI-Accounting | NYI claim coverage/completeness accounting | Mark NYI incomplete in aggregation reporting; ratchet to executable per evaluator-slice landing | RATIFIED-by-default | | Q-Std-Carrier-Phasing | Rust std-carrier phasing (Option/Cardinal/HigherOrderMethodSpec/allocator-hasher) | Phase 1 = default-only/default-instance; later phases as separate Substrate slices post-Phase-1 | RATIFIED-by-default | | Q-Drift-Reconcile | Drift items routing (#1638, #1499, declaration_by_name) | Single Debt-Paydown worker reconciles all three → one PR closing rows in ledger + ROADMAP | RATIFIED-by-default | From 61d6489127af1c9ec3aef3529a62b37abcd79816 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 08:11:47 +0000 Subject: [PATCH 16/16] =?UTF-8?q?docs(briefs):=20V1=20worker=20=E2=80=94?= =?UTF-8?q?=20scope=20line=20is=20narrative=20not=20second=20authority?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- docs/briefs/r3-v-pattern-a-tc1-v1-worker.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md index 61538dafc6f..eda0b6e8586 100644 --- a/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md +++ b/docs/briefs/r3-v-pattern-a-tc1-v1-worker.md @@ -4,7 +4,7 @@ **Parent:** [`docs/briefs/r3-verification-manager.md`](r3-verification-manager.md) — absorbed formal-grounding / Pattern-A cluster (not a fourth lane; see [`docs/r3-structure.md`](../r3-structure.md) §"Manager structure"). -**Ratified scope authority:** [`docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md`](r3-v-tc1-eta-equivalence-deeper-analysis.md) §"DESIGN — Q-PAFS first executable slice (Pattern-A / TC1)" **Path A** — TC1 **static representative** via **E6-G1.a** (finite Director-visible lens set + fixed eta pair; `BinaryDimensionReportEquals` consumer envelope per [`docs/briefs/r3-v-pattern-a-coverage-rollup.md`](r3-v-pattern-a-coverage-rollup.md)). +**Ratified scope narrative (engineering brief):** [`docs/briefs/r3-v-tc1-eta-equivalence-deeper-analysis.md`](r3-v-tc1-eta-equivalence-deeper-analysis.md) §"DESIGN — Q-PAFS first executable slice (Pattern-A / TC1)" **Path A** — TC1 **static representative** via **E6-G1.a** (finite Director-visible lens set + fixed eta pair; `BinaryDimensionReportEquals` consumer envelope per [`docs/briefs/r3-v-pattern-a-coverage-rollup.md`](r3-v-pattern-a-coverage-rollup.md)). **Program plan:** [`docs/r3-program-plan.md`](../r3-program-plan.md) §10.3 rows **Q-PAFS**, **Q-Pattern-A-First-Slice-Subscope**, **Q-EVAL-Lens-Fold-First-Slice** — **ACCEPTED 2026-05-06 (Path A / G1.a)**.