Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
d61ea38
R3 gate 64 reflection closure executable receipt
briansrls May 11, 2026
2d65cfc
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
d23844a
Clarify gate 64 receipt is non-canonical plumbing
briansrls May 11, 2026
02f51bc
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
6f37c4c
Add gate 64 test harness to SG-0 census
briansrls May 11, 2026
5d004c8
Add PR 2694 SG-0 body receipt
briansrls May 11, 2026
18f01b5
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
c24794f
Tighten gate 64 residual receipt
briansrls May 11, 2026
8f7d12f
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
2066e43
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
00aa7c3
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
0b69cb2
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
01caa1d
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
2a1a5ad
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
8dc382b
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
fc4ae56
Keep v3 full-suite CI alive during long runs
briansrls May 11, 2026
6065c03
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
222ef2f
Merge origin/main into gate 64 receipt branch
briansrls May 11, 2026
e01ef0f
WIP: substrate_gap_reflection_closure_closed
briansrls May 11, 2026
399071d
Accept passing gate 64 residual census receipt
briansrls May 11, 2026
0deb47b
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
a00be38
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
c1273cd
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
bf45644
Stabilize v3 Zig setup in CI
briansrls May 11, 2026
717f7e0
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
56bdcbb
Tighten gate 64 residual pass receipt
briansrls May 11, 2026
90b5ac0
Add v3 prebuild CI heartbeat
briansrls May 11, 2026
8fc3b00
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
218b861
Merge remote-tracking branch 'origin/main' into session/sharp-stag-109
briansrls May 11, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 17 additions & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -218,6 +218,12 @@ jobs:

- name: Setup Zig C toolchain
uses: goto-bus-stop/setup-zig@v2
with:
# Pin a stable linker toolchain instead of the action default
# nightly/master download path; the self-hosted runner has lost
# contact repeatedly while resolving the moving Zig setup target.
version: 0.13.0
cache: false

- name: Configure user-space C linker
run: |
Expand Down Expand Up @@ -289,7 +295,17 @@ jobs:
# Tracked headroom: ratchet this ceiling back toward 300s once cold lane2d
# CI runs regularly complete under 300s after fixture compile amortization.
- name: Prebuild v3 integration test binary (lane2d wall-clock denominator)
run: cargo test -p v3-compiler --test integration --no-run
run: |
set -euo pipefail
heartbeat() {
while sleep 60; do
echo "v3 prebuild heartbeat: $(date -u +%FT%TZ)"
done
}
heartbeat &
heartbeat_pid=$!
trap 'kill "$heartbeat_pid" 2>/dev/null || true' EXIT
cargo test -p v3-compiler --test integration --no-run

- name: v3 tests (Stage 2d integration module, 360s cold-compile-safe budget)
env:
Expand Down
2 changes: 1 addition & 1 deletion docs/r3-program-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -287,7 +287,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
| 61 | `substrate_gap_function_valued_data_closed` | substrate-gap-class | T-E-P-Producer-Broadening (Phase 1) + E6-G0d (landed #1813) | DECLARED YELLOW (NEW 2026-05-06; reframed RED→YELLOW 2026-05-06 per option (a) RATIFIED) | chain-break dissolved by Q-Class-2-Chain-Break option (a) gap-test re-pick + Q-LBP-R3-Closeability option (b) narrowing; single-prereq-blocked on T-E-P P1 / S10 |
| 62 | `substrate_gap_file_ingestion_closed` | substrate-gap-class | T-Workflow-As-Data | DECLARED (NEW 2026-05-06) | `.dag` program ingests external file w/o include_str! |
| 63 | `substrate_gap_workflow_scheduling_closed` | substrate-gap-class | T-Workflow-As-Data + T-Lens-Self-Application | DECLARED (NEW 2026-05-06) | CI workflow as `.dag` data; substrate prereqs in §4.4 |
| 64 | `substrate_gap_reflection_closure_closed` | substrate-gap-class | T-LensProducer-Retirement | DECLARED (NEW 2026-05-06) | `lens_apply.rs` reflection via PB-Runtime |
| 64 | `substrate_gap_reflection_closure_closed` | substrate-gap-class | T-LensProducer-Retirement | **DECLARED** (substrate-plumbing receipt via PR #2694 — `src/v3/compiler/tests/fixtures/r3_substrate_gap_reflection_closure.dag` adds non-canonical claim `substrate_gap_reflection_residual_census_receipt` over the live `CensusSubsetCount` lens-producer residual predicate; `r3_substrate_gap_reflection_closure_test.rs` proves the state-check receipt executes and reports residual count 3 while residuals remain. This is **NOT** the canonical reflection-closure consumer.) | `lens_apply.rs` reflection via PB-Runtime; canonical Pass-condition per `r3-structure.md:181`: `lens_apply.rs` reflection routes via PB-Runtime interpreter-as-data and reflection-as-data substrate is exercised end-to-end. Status re-promotes only when PB-Runtime + T-LensProducer-Retirement land that consumer; census state-check is one half of the conjunctive class closure and remains a placeholder per PR #2657 / `feedback_grep_consumer_surfaces_for_lane_completeness`. P5 deferral receipts: non-test residual tracked under `ROADMAP.md` §"Lane acceptance — .dag gates" / T-PB-A row `lens_producer_files_remaining` (anchor `#lane-acceptance--dag-gates`), whose dissolution target is the priority lens-producer non-test census reaching zero; new host test harness tracked under `ROADMAP.md` §"Lane acceptance — .dag gates" / T-PB-B row `pb_rust_tests_outside_residual_zero` plus `EXPECTED_HAND_AUTHORED_TEST` in `sg0_census_test.rs`, dissolving when the generic TestClaim runner can execute the receipt without this harness. |
| 65 | `tier3_dissolution_demonstration_executes` | demonstration | T-Tier3-Dissolution | PASSING | `src/v3/compiler/tests/dag/t_r3_tier3_dissolution_demonstration.dag` runs through `t_pb_b_1_dag_runner_test::r3_tier3_dissolution_demonstration_suite_passes_through_runner` |
| 66 | `lens_producer_retirement_executable_witness` | demonstration | T-LensProducer-Retirement | **DECLARED** (substrate-plumbing landed via PR #2595 squash `a085f6e9` 2026-05-10 15:52Z — `src/v3/compiler/tests/integration/r3_lens_producer_retirement_executable_witness_test.rs` runs near-term `lens_producer_files_remaining` state-check claim and reports residual `CURRENT_RESIDUAL_COUNT = 3` per `r3-structure.md:184` "near-term demo = retirement state-check + doc receipts"; this is **NOT** the canonical demonstration consumer) | NEW 2026-05-06; canonical Pass-condition per `r3-structure.md:184`: `lens_apply` reflection routes via PB-Runtime on representative lens program; **execution-ready witness DEFERRED** to Row-4 equivalence receipt + Item 4 landing per `docs/design-pb-runtime-interpreter.md` §5.1; "demonstration" status re-promotes to CONSUMER_LANDED only when Row-4 + Item 4 receipts exist (state-check is placeholder, not canonical consumer for this `demonstration`-family gate) |
| 67 | `numeric_construction_demonstration` | demonstration | T-Numeric-Construction | DECLARED (NEW 2026-05-06) | `Int<32>` + `Real<64>` round-trip |
Expand Down
4 changes: 2 additions & 2 deletions scripts/check-test-timeout.sh
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@
# TEST_TIMEOUT_EXEMPT Path to exemption file
# (default scripts/slow-test-exemptions.txt).
# TEST_TIMEOUT_MAX_EXEMPTIONS
# Ratchet floor for active exemption entries (default 78;
# Ratchet floor for active exemption entries (default 80;
# keep aligned with non-comment rows in
# scripts/slow-test-exemptions.txt). Raise or lower in the same PR
# as exemption rows; lower when deleting exemptions.
Expand All @@ -56,7 +56,7 @@ log_file_arg=${1:-}
budget_ms=${2:-${TEST_TIMEOUT_MS:-2000}}
pkg=${TEST_TIMEOUT_PACKAGE:-v3-compiler}
exempt_file=${TEST_TIMEOUT_EXEMPT:-scripts/slow-test-exemptions.txt}
max_exemptions=${TEST_TIMEOUT_MAX_EXEMPTIONS:-78}
max_exemptions=${TEST_TIMEOUT_MAX_EXEMPTIONS:-80}

script_dir=$(cd "$(dirname "$0")" && pwd)
repo_root=$(cd "$script_dir/.." && pwd)
Expand Down
2 changes: 2 additions & 0 deletions scripts/ci-merge/sg0-pr-body-append.2694.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
SG-0 hand-path delta: +1
SG-0 pairing: (c) follow-up dispatch for host-test residual under docs/briefs/t-pb-b-1.md; tracked by ROADMAP.md T-PB-B / pb_rust_tests_outside_residual_zero until the generic TestClaim runner executes this receipt without a Rust harness.
3 changes: 3 additions & 0 deletions scripts/slow-test-exemptions.txt
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ m2_lens_unused_parameters_migration_test::unused_parameters_dag_runs_end_to_end_
m2_lens_unused_parameters_migration_test::unused_parameters_dag_self_analysis_reports_zero_findings # Lane 2 migration harness roundtrip; compile-heavy self-analysis remains explicit until lens migration paydown.
r1c_e_emit_gates_dag_test::r1c_e_emit_gates_suite_passes_through_runner # R1C-E `.dag` wrapper shells through the runner/binary harness and sits on the 2s CI edge (2166ms on PR #1233); paydown owned by R1C-E emit-gates runner/shared-setup work, not this impossible-bugs row-removal slice.
r3_verification_l4_l7_l5_skeleton_test::r3_verification_l4_emit_eval_false_branch_passes_w1_emit_vs_eval # R3-V L4 W1 direct consumer fixture runs the full emit-vs-eval suite through TestRunner and can sit just above 2s on CI (2072ms on PR #1799); paydown owned by R3-V L4/L7 direct harness shared runner setup, see docs/briefs/r3-v-l4-l7-direct-w1-consumer-spec.md.
r3_verification_l4_l7_l5_skeleton_test::r3_verification_l4_l7_direct_suite_lists_four_l4_certification_seed_claims # R3-V L4/L7 direct suite inventory receipt runs the same L4 certification fixture through TestRunner and crossed the 2s Phase-0 ratchet on full-suite CI (2093ms on PR #2694). Paydown owned by R3-V L4/L7 shared runner setup; dissolution: delete this row and lower TEST_TIMEOUT_MAX_EXEMPTIONS in the same commit once cold ubuntu-latest reports <=2000ms.
r3_verification_l4_l7_l5_skeleton_test::r3_verification_l7_algebraic_law_matrix_has_current_runner_receipts # R3 gate #10 / issue #2382: single `L7_MATRIX_SUITE` runner pass + per-claim source receipts ~2.4s cold CI (PR #2394); paydown: slimmer witness applications or shared runner amortization with other Lane 1 L7 rows.

complexity_lens_behavioral_completion::literal_bind_cements_constant_complexity_summary # R3 T-Lens-Behavioral-Parity cementing receipt: cold compile_to_dag + COMPLETE complexity lens summary assertion can exceed 2s on CI; paydown owned by lens behavioral parity shared-fixture/testgen migration.
Expand All @@ -77,6 +78,8 @@ cost_lens_symbolic_consumer_test::literal_bind_pins_symbolic_cost_of_constant_on
cost_lens_symbolic_consumer_test::recursive_countdown_pins_symbolic_cost_linear_and_sizevar_on_fixture # ROADMAP Lane E-P + R3 program gate #80 (`cost_lens_behaviorally_complete`, `docs/r3-program-plan.md` §1.8; PROXY `cost.dag` per `docs/v3-lens-capability-register.md`); verification `cost_lens_symbolic_consumer_test` (gunbc#1968). Recursive fixture + `symbolic_cost_of` same wall class as `complexity_lens_behavioral_completion::recursive_countdown_*` — paydown: shared fixture warming + cost row Band-C / v2-oracle closure per `docs/briefs/r3-v-t-lbp-narrowed-scope-partner-worker.md` and ROADMAP Lane E-P acceptance bullet.
cost_lens_symbolic_consumer_test::e_p_sub_value_relation_per_call_landed_cost_lens_routes_through_per_call_pattern_query # R3 gate #78 (`e_p_sub_value_relation_per_call_landed`): cold `compile_to_dag` + `symbolic_cost_of` / span-filtered Callable harness — ~15s wall on full-suite CI; paydown: shared fixture/`compile_to_dag` warming with sibling cost consumer tests (TESTING.md Phase-0). Dissolution: delete this line and lower `TEST_TIMEOUT_MAX_EXEMPTIONS` in `scripts/check-test-timeout.sh` in the same commit once `RUSTC_BOOTSTRAP=1 cargo test -p v3-compiler cost_lens_symbolic_consumer_test::e_p_sub_value_relation_per_call_landed_cost_lens_routes_through_per_call_pattern_query -- -Z unstable-options --report-time` shows <=2000ms wall on cold ubuntu-latest after shared cost-consumer fixture warming with sibling `cost_lens_symbolic_consumer_test::*` tests (TESTING.md Phase-0).

e6_g1a_option3_static_lens_test::e6_g1a_option3_static_lens_mini_report_executes_without_reflection_imports # E6/G1a option-3 static lens fixture: compile_to_dag + mini-report execution can sit just above the 2s Phase-0 ratchet on full-suite CI (2038ms on PR #2694). Paydown: shared fixture warming or fixture slimming in the E6/G1a static-lens lane; dissolution: delete this row and lower TEST_TIMEOUT_MAX_EXEMPTIONS in the same commit once cold ubuntu-latest reports <=2000ms.

bootstrap::tests::kernel_bool_path_a_attaches_diagnostic_when_boolean_algebra_unresolvable # Lane 1e-2b Path A regression: two `Dag::new()` paths + mutation; can exceed 2s wall on cold ubuntu-latest when compiled alongside heavy integration neighbors — keep explicit bootstrap diagnostic coverage. Paydown trigger: when the Bool/`BooleanAlgebra` kernel bootstrap bridge dissolves into `dsl/std/types.dag` (see `bootstrap.rs` + `dsl/std/types.dag` dissolution notes), collapse fixtures and/or adopt shared `Dag::new` warming; re-measure and remove if under 2s.

lens_behavioral_parity_demonstration_test::r3_gate_73_demonstrates_complexity_certainty_is_proven # R3 program gate #73 (`lens_behavioral_parity_demonstration`, `docs/r3-program-plan.md` §1.8): alphabetically first split complexity receipt pays cold `compile_to_dag` + generated complexity/cost lens reads through shared OnceLock warming and matches the same wall class as sibling T-Lens-Behavioral-Parity cementing tests. Paydown: T-Tests-As-Data rows 84/87 express this frozen snapshot as `.dag` TestClaim data, then delete the host test and this exemption.
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
// std.r3_substrate_gap_reflection_closure - R3 gate #64 substrate-plumbing receipt.
//
// This is NOT the canonical `substrate_gap_reflection_closure_closed` gate
// predicate. The class-level gate remains conjunctive per r3-structure.md:
// representative reflection execution via PB-Runtime plus zero residual
// class bridges. This fixture covers only the second half's current
// lens-producer residual census.

module std.r3_substrate_gap_reflection_closure

import std.verification {
CensusSubsetCount,
TestClaim,
TestSuite,
expected_hand_authored_non_test,
lens_producer_files_subset_predicate
}

type Sg0CensusAuthority {}

data sg0_census_test_authority: Sg0CensusAuthority = {}

data substrate_gap_reflection_residual_census_receipt: TestClaim = {
name: "substrate_gap_reflection_residual_census_receipt",
source: "// Reflection residual-census receipts read external census state, not this source.\nlet _: Int = 0\n",
file_name: "r3_substrate_gap_reflection_residual_census_receipt.v3",
predicate: CensusSubsetCount {
authority: sg0_census_test_authority,
list_constant: expected_hand_authored_non_test,
subset_predicate: lens_producer_files_subset_predicate
},
requires: []
}

data r3_substrate_gap_reflection_closure_suite: TestSuite = {
name: "r3_substrate_gap_reflection_closure_suite",
claims: [substrate_gap_reflection_residual_census_receipt]
}
2 changes: 2 additions & 0 deletions src/v3/compiler/tests/integration.rs
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,8 @@ mod r3_gate_87_lens_cementing_regen_receipts_test;
mod r3_lens_producer_retirement_executable_witness_test;
#[path = "integration/r3_pb_runtime_evaluator_corpus_seed_test.rs"]
mod r3_pb_runtime_evaluator_corpus_seed_test;
#[path = "integration/r3_substrate_gap_reflection_closure_test.rs"]
mod r3_substrate_gap_reflection_closure_test;
#[path = "integration/r3_v3_self_host_demonstration_dag_test.rs"]
mod r3_v3_self_host_demonstration_dag_test;
#[path = "integration/r3_verification_l4_l7_l5_skeleton_test.rs"]
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
//! **Layer:** integration

This comment was marked as resolved.

//!
//! R3 gate #64 — reflection-closure substrate-plumbing receipt.
//!
//! This is not the canonical `substrate_gap_reflection_closure_closed` consumer.
//! It proves the live T-LensProducer-Retirement residual census is executable
//! as plumbing for the bridge-count half of the class-level closure condition.

use v3_compiler::compile_to_dag;
use v3_compiler::test_runner::{ClaimResult, TestRunner};
use v3_compiler::CompileError;

const FIXTURE_SOURCE: &str = include_str!("../fixtures/r3_substrate_gap_reflection_closure.dag");
const FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_substrate_gap_reflection_closure.dag";
const SUITE_NAME: &str = "r3_substrate_gap_reflection_closure_suite";
const CLAIM_NAME: &str = "substrate_gap_reflection_residual_census_receipt";
const CURRENT_REFLECTION_RESIDUAL_COUNT: i64 = 3;

#[test]
fn r3_gate_64_reflection_residual_census_receipt_executes() {
let dag = match compile_to_dag(FIXTURE_SOURCE, FIXTURE_PATH) {
Ok(dag) => {
assert!(
dag.diagnostics().is_empty(),
"{FIXTURE_PATH}: expected empty module diagnostics, got {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
);
dag
}
Err(CompileError::Semantic(dag)) => panic!(
"{FIXTURE_PATH} should lower without module diagnostics. Got `Err(Semantic)`: {:?}",
dag.diagnostics().iter().collect::<Vec<_>>()
),
Err(other) => panic!("unexpected compile error for {FIXTURE_PATH}: {other:?}"),
};

let results = TestRunner::new(&dag).run_suite(SUITE_NAME);
let result = results
.iter()
.find(|result| result.claim_name == CLAIM_NAME)
.unwrap_or_else(|| panic!("missing `{CLAIM_NAME}` in `{SUITE_NAME}` results: {results:?}"));

match &result.result {
ClaimResult::Pass => assert_eq!(
CURRENT_REFLECTION_RESIDUAL_COUNT, 0,
"`{CLAIM_NAME}` passed before the frozen live reflection residual count reached zero"
),
ClaimResult::Fail(reason) => {
assert!(
reason.contains(&format!(
"lens-producer subset observed {CURRENT_REFLECTION_RESIDUAL_COUNT}"
)),
"`{CLAIM_NAME}` should report the live reflection residual count; got {reason:?}"
);
}
ClaimResult::NotYetImplemented(reason) => {
panic!("`{CLAIM_NAME}` receipt must be executable for R3 gate #64 plumbing, got NYI: {reason}")
}
}
}
8 changes: 8 additions & 0 deletions src/v3/compiler/tests/integration/sg0_census_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -595,6 +595,14 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
// Dissolves when Row-4 producers land and the runner can execute the PB-Runtime /
// R2-Evaluator corpus comparison directly without this host-side harness.
"src/v3/compiler/tests/integration/r3_pb_runtime_evaluator_corpus_seed_test.rs",
// R3 gate #64 substrate-plumbing receipt: hand-Rust driver for the
// non-canonical `.dag` residual-census receipt until the canonical
// PB-Runtime reflection consumer lands. P5 test-subset deferral:
// ROADMAP.md § "Nine lanes" row `T-PB-B` and § "Lane acceptance — .dag
// gates" row `T-PB-B` / `pb_rust_tests_outside_residual_zero`; dissolves
// when the generic TestClaim runner can execute the receipt without this
// host-side harness.
"src/v3/compiler/tests/integration/r3_substrate_gap_reflection_closure_test.rs",
// R3 gate #71 (`v3_self_host_demonstration`): `.dag` + `CARGO_BIN_EXE` splice for
// `ExecuteCommand(self_host_fixed_point, [--r3-gate-71-demonstration], 0)` — strict DB-8 slice
// (non-zero unless `compiler.dag` parses + `fixed_point_diff` ok). Unignored compile-only smoke
Expand Down
Loading