diff --git a/src/v3/compiler/tests/fixtures/tc3_strong_normalization_executable.v3 b/src/v3/compiler/tests/fixtures/tc3_strong_normalization_executable.v3 new file mode 100644 index 00000000000..faa5d8dda88 --- /dev/null +++ b/src/v3/compiler/tests/fixtures/tc3_strong_normalization_executable.v3 @@ -0,0 +1,9 @@ +// TC3 strict-fire - strong-normalization scaffold over typed `.dag` programs. +// Vacuity guard: evaluation has nontrivial step structure (function application +// + arithmetic) so baseline eval-step and termination-evidence projections do +// not collapse to a single trivial trace before producers land. +module user.tc3_strong_normalization_executable + +fn succ(n: Int) -> Int = n + 1 + +let _: Int = succ(succ(0)) diff --git a/src/v3/compiler/tests/fixtures/tc3_strong_normalization_strict_fire.dag b/src/v3/compiler/tests/fixtures/tc3_strong_normalization_strict_fire.dag new file mode 100644 index 00000000000..57612880b71 --- /dev/null +++ b/src/v3/compiler/tests/fixtures/tc3_strong_normalization_strict_fire.dag @@ -0,0 +1,59 @@ +// std.tc3_strong_normalization_strict_fire — TC3 (strong-normalization) first executable slice. +// +// Authority: `r3-program-plan.md` §1.8 gate #13 `tc3_pattern_a_second_mover_executable`; +// `r3-v-pattern-a-tc3-v1-worker.md` (Pattern-A second-mover; unified +// `BinaryDimensionReportEquals` envelope; two-stage gate (a)/(b)). +// +// Differences vs `tc3_strong_normalization_deferred.dag`: +// - Canonical TestClaim name `tc3_pattern_a_second_mover_executable` (deferred fixture uses +// the R2 research-receipt form `tc3_strong_normalization_substrate_introduced`). +// - Same predicate shape and same role-pair carrier `Dag` per +// `r3-v-tc3-pattern-a-second-mover-conformance-audit.md` §Witness-Shape Commitments +// (baseline evaluation-step projection vs bounded-step / termination-evidence projection). +// - Embeds a non-vacuous typed `.v3` source (sidecar `tc3_strong_normalization_executable.v3`) +// so the eval-step / termination-evidence projection pair is not trivially equal at the +// substrate flip. +// +// Runner status today: `BinaryDimensionReportEquals` shape-only — `eval_binary_dimension_report_ +// equals_shape` returns `NotYetImplemented` after structural validation (generic +// `DimensionReport` production/evaluation substrate not landed). Strict-fire **PASSING** +// requires bundle stage (b): T-FixedPoint termination semantics (gunbc#2087) + Evaluator +// eval-step / bounded-step producer surface. Integration test asserts shape-valid NYI today; +// flips to Pass when (a)+(b) land without changing this claim name. +// +// Vacuity guard (Pattern-A TC3): `TestClaim.source` is a structurally bounded computation +// (`succ(succ(0))`) — a multi-step evaluation whose baseline eval-step trace and termination- +// evidence projection diverge in step structure even before producers wire (audit §Non-Drift +// Findings — no serialized / string / byte / theorem encoding). +// +// NO new `TestPredicate` variants — consumer-only authoring per Director #828; no TC3-specific +// quantifier carrier, producer identity enum, or Verification-local report shape per audit §1 +// bullets 4–5. + +module std.tc3_strong_normalization_strict_fire + +import std.dimensions { DimensionReport } +import std.substrate { Dag } +import std.verification { BinaryDimensionReportEquals, TestClaim, TestSuite } + +// Role types: producers resolve these to evaluation-step (baseline) and bounded-step / +// termination-evidence projections. Same carrier `C = Dag` per audit §Contract bullet 2. +type tc3_evaluation_step_baseline_dimension_report = DimensionReport +type tc3_evaluation_step_compare_dimension_report = DimensionReport + +// §1.8 gate #13 canonical TestClaim name. +data tc3_pattern_a_second_mover_executable_claim: TestClaim = { + name: "tc3_pattern_a_second_mover_executable", + source: "// TC3 strict-fire - strong-normalization scaffold over typed `.dag` programs.\n// Vacuity guard: evaluation has nontrivial step structure (function application\n// + arithmetic) so baseline eval-step and termination-evidence projections do\n// not collapse to a single trivial trace before producers land.\nmodule user.tc3_strong_normalization_executable\n\nfn succ(n: Int) -> Int = n + 1\n\nlet _: Int = succ(succ(0))\n", + file_name: "tc3_strong_normalization_executable.v3", + predicate: BinaryDimensionReportEquals( + tc3_evaluation_step_baseline_dimension_report, + tc3_evaluation_step_compare_dimension_report + ), + requires: [] +} + +data tc3_strong_normalization_strict_fire_suite: TestSuite = { + name: "tc3_strong_normalization_strict_fire_suite", + claims: [tc3_pattern_a_second_mover_executable_claim] +} diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index e98b5ddec4f..d27645b5b46 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -219,6 +219,8 @@ mod tc1_substrate_lens_eta_equivalence_strict_fire_test; mod tc2_church_rosser_strict_fire_test; #[path = "integration/tc3_strong_normalization_deferred_test.rs"] mod tc3_strong_normalization_deferred_test; +#[path = "integration/tc3_strong_normalization_strict_fire_test.rs"] +mod tc3_strong_normalization_strict_fire_test; #[path = "integration/test_runner_test.rs"] mod test_runner_test; #[path = "integration/thesis_parallelism_test.rs"] diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index 386ad0ee6a5..6251d263b68 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -579,6 +579,10 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ // strategy-order `BinaryDimensionReportEquals` pairing per `r3-v-pattern-a-tc2-v1-worker.md`. "src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs", "src/v3/compiler/tests/integration/tc3_strong_normalization_deferred_test.rs", + // TC3 strict-fire — §1.8 gate #13 (`tc3_pattern_a_second_mover_executable`); strong- + // normalization / Pattern-A second-mover `BinaryDimensionReportEquals` pairing per + // `r3-v-pattern-a-tc3-v1-worker.md` (two-stage gate; PASSING gated on T-FixedPoint stage (b)). + "src/v3/compiler/tests/integration/tc3_strong_normalization_strict_fire_test.rs", "src/v3/compiler/tests/integration/test_runner_test.rs", "src/v3/compiler/tests/integration/thesis_parallelism_test.rs", "src/v3/compiler/tests/integration/thesis_validation_test.rs", diff --git a/src/v3/compiler/tests/integration/tc3_strong_normalization_strict_fire_test.rs b/src/v3/compiler/tests/integration/tc3_strong_normalization_strict_fire_test.rs new file mode 100644 index 00000000000..bd6ff3dd8d0 --- /dev/null +++ b/src/v3/compiler/tests/integration/tc3_strong_normalization_strict_fire_test.rs @@ -0,0 +1,120 @@ +//! **Layer:** integration +//! +//! TC3 strong-normalization / Pattern-A second-mover — strict-fire executable form +//! (§1.8 gate #13). +//! +//! Pairing `DimensionReport` for baseline evaluation-step vs bounded-step / +//! termination-evidence projections per `tc3_strong_normalization_deferred.dag` staging +//! and `r3-v-pattern-a-tc3-v1-worker.md`. Unified consumer envelope: +//! `BinaryDimensionReportEquals` (audit §Pattern A Compositionality Verdict). +//! +//! Today's runner returns `NotYetImplemented` with the canonical "structural shape is valid" +//! reason (`eval_binary_dimension_report_equals_shape` in `src/v3/compiler/src/test_runner.rs`). +//! Gate #13 stays **DECLARED** at this scaffold landing; the NYI receipt is fail-closed — +//! a real equality eval **must** flip this test to `Pass` when (a)+(b) wiring lands +//! (worker brief §Implementation slices). Strict-fire **PASSING** requires bundle +//! stage (b): T-FixedPoint termination semantics (gunbc#2087) + Evaluator eval-step / +//! bounded-step producer surface. +//! +//! **Vacuity guard:** embedded `TestClaim.source` is a structurally bounded computation +//! (`succ(succ(0))`) — a multi-step evaluation whose baseline eval-step trace and +//! termination-evidence projection diverge in step structure (Pattern-A TC3 worker brief). +//! +//! **INVARIANTS P5:** The §P5(b) **single checkable per-PR receipt** (SG-0 census / pairing / +//! `ROADMAP.md` deferral) lives on **the PR description**, not in this file — see GitHub PR +//! body for authoritative dissolution bookkeeping (`INVARIANTS.md` §P5 Dispatch-Discipline +//! mechanism (b)). + +use v3_compiler::compile_to_dag; +use v3_compiler::test_runner::{ClaimResult, TestClaimValue, TestRunner}; +use v3_compiler::CompileError; + +const FIXTURE_SOURCE: &str = include_str!("../fixtures/tc3_strong_normalization_strict_fire.dag"); +const FIXTURE_PATH: &str = + "src/v3/compiler/tests/fixtures/tc3_strong_normalization_strict_fire.dag"; +const SUITE_NAME: &str = "tc3_strong_normalization_strict_fire_suite"; + +/// Sidecar bytes for the §1.8 claim program — **must** match parsed `TestClaim.source` from the +/// `.dag` fixture (`tc3_strict_fire_suite_has_canonical_executable_claim_with_valid_binary_shape`). +const CLAIM_PROGRAM_SOURCE: &str = + include_str!("../fixtures/tc3_strong_normalization_executable.v3"); +const CLAIM_PROGRAM_PATH: &str = + "src/v3/compiler/tests/fixtures/tc3_strong_normalization_executable.v3"; + +const TC3_CLAIM_DATA_NAME: &str = "tc3_pattern_a_second_mover_executable_claim"; + +#[test] +fn tc3_strict_fire_suite_has_canonical_executable_claim_with_valid_binary_shape() { + 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::>() + ); + dag + } + Err(CompileError::Semantic(dag)) => panic!( + "{FIXTURE_PATH} should lower without module diagnostics. Got `Err(Semantic)`: {:?}", + dag.diagnostics().iter().collect::>() + ), + Err(other) => panic!("unexpected compile error for {FIXTURE_PATH}: {other:?}"), + }; + + let claim_decl = dag + .declaration_by_name(TC3_CLAIM_DATA_NAME) + .unwrap_or_else(|| panic!("missing `{TC3_CLAIM_DATA_NAME}` in {FIXTURE_PATH}")); + let claim = TestClaimValue::from_declaration(claim_decl).unwrap_or_else(|e| { + panic!("`{TC3_CLAIM_DATA_NAME}` should lower as TestClaim: {e}"); + }); + assert_eq!( + claim.source, CLAIM_PROGRAM_SOURCE, + "embedded `TestClaim.source` in {FIXTURE_PATH} must stay byte-identical to {CLAIM_PROGRAM_PATH} (single program authority per INVARIANTS P2)" + ); + assert_eq!( + claim.file_name, "tc3_strong_normalization_executable.v3", + "TestClaim.file_name must match the sidecar program path used in lowering checks" + ); + + let program_dag = match compile_to_dag(&claim.source, &claim.file_name) { + Ok(program_dag) => program_dag, + Err(CompileError::Semantic(program_dag)) => panic!( + "embedded TestClaim.source should lower cleanly; diagnostics: {:?}", + program_dag.diagnostics().iter().collect::>() + ), + Err(other) => panic!("embedded TestClaim.source compile error: {other:?}"), + }; + assert!( + program_dag.diagnostics().is_empty(), + "embedded claim program expected no diagnostics, got {:?}", + program_dag.diagnostics().iter().collect::>() + ); + + let results = TestRunner::new(&dag).run_suite(SUITE_NAME); + assert_eq!(results.len(), 1, "strict-fire suite has exactly one claim"); + assert_eq!( + results[0].claim_name, "tc3_pattern_a_second_mover_executable", + "claim name must be the §1.8 #13 canonical gate name" + ); + // Today: shape-valid NotYetImplemented (runner waits on stage (b): T-FixedPoint + // termination semantics + Evaluator eval-step producer). When (a)+(b) land, this + // assertion flips from NotYetImplemented to Pass — that is the §1.8 #13 + // CONSUMER_LANDED → PASSING transition without further fixture edits. + assert!( + matches!( + &results[0].result, + ClaimResult::NotYetImplemented(reason) + if reason.contains("BinaryDimensionReportEquals") + && reason.contains("structural shape is valid") + ), + "expected BinaryDimensionReportEquals shape-valid NotYetImplemented, got {:?}", + results[0].result + ); +} + +// INVARIANTS P1 / P5 — checkable receipt: this integration crate must not build if the cited +// worker brief is missing from the worktree. +const _: &str = include_str!(concat!( + env!("CARGO_MANIFEST_DIR"), + "/../../../docs/briefs/r3-v-pattern-a-tc3-v1-worker.md" +));