From 8312561d9a211ab6dcf80980e72fddd36d2e2663 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 5 May 2026 16:49:11 -0400 Subject: [PATCH 01/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] 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/10] =?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) |