From 7cdc4ffc76c474ef0dbcf1b3158c2c44150b6fe2 Mon Sep 17 00:00:00 2001 From: Cryptskii <47649969+cryptskii@users.noreply.github.com> Date: Tue, 8 Sep 2026 19:12:27 -0400 Subject: [PATCH] fix(validation): the formal gates printed FAILED and exited 0 CI reads the process status, not the report text. All three dsm_vertical_validation steps summarized their own failures and returned Ok, so a violated invariant, a falsification config that stopped falsifying, a failed bridge property and a failed implementation trace were every one of them GREEN. Verified before changing anything: collect_tla_results computes all_passed, eprintln!s "FAILED specs: {}", and returns Ok(results) unconditionally. run_tla_check returns Ok(results). main does `run_tla_check(...).await?` and falls through to Ok(()). main.rs contains no process::exit, no ExitCode and no bail! on a verdict. The CI step is a bare `cargo run ... -- tla-check` with no grep on the log. run_property_tests and run_implementation_traces return () -- they collect, render and return, with no failure check at all. So the only things that could redden those jobs were a missing java, a missing .tla/.cfg, or a build failure. WHAT WAS ALREADY CORRECT, and is worth stating precisely: the expected-violation SEMANTICS were fully implemented. run_all already normalizes every verdict and inverts the falsification configs -- expected invariant violated is a pass, no violation is "the invariant is decoration", a different violation is "a different failure". None of that changes here. The defect was never the classification; it was that nothing turned the aggregate into an exit status. This adds: enforce(gate, total, failing) -- bails with the failing labels. Called AFTER the report prints, so the failing spec and the invariant it violated stay visible in the log. tla-check, property-tests and implementation-traces all route through it. property-tests and implementation-traces now return Result and their call sites propagate. EXPECTED_STANDARD_SPECS = 13, asserted in run_all. The TLA registry is Rust, not a glob, so a spec deleted from standard_specs leaves nothing for a file count to notice -- the suite just gets smaller and stays green. This is the analogue of the Lean gate's expected=12, which had no TLA counterpart. Two unit tests: the registry size, and that every falsification config names an invariant its own spec declares (a typo there degrades silently into "a different failure", which reads as a defect in the model rather than in the registry). MUTATION CONTROLS, all executed, all restored: A ordinary spec pointed at a falsifying config -> exit 1, "FAILED specs: EconRegisterObservation" B falsification config neutered so nothing violates -> exit 1, "must violate EmptinessIsGrounded, but saw no violation at all - the invariant is decoration" C falsification config names the WRONG invariant -> exit 1, "saw a different failure: ConflictUnreachable" D unmutated 13-spec suite -> exit 0, "All 13 specs PASSED" E one spec dropped from the registry -> exit 1, "registers 12 specs, expected 13" F one bridge property forced to fail -> exit 1, "1 of 7 FAILED - hash_chain_continuity" G one implementation trace forced to fail -> exit 1, "1 of 16 FAILED - state_machine_transfer_chain" The baseline suite is genuinely green, so this does not paper over a red spec -- it makes 13 specs, 7 properties and 16 traces load-bearing for the first time. Amendment 2c-C2's record is corrected in the same change. It said the five falsification configs "are machine-gated on the invariant each must violate". That was true of the runner's bookkeeping and false of CI. The sentence now says "classified", with a recorded correction naming the exit-status defect and this fix. Board: make lint exit 0 on the pinned 1.98.0 toolchain; cargo fmt --check clean; clippy --all-targets clean; the 2 new unit tests pass; tla-check exits 0 on the clean suite. --- .../amendment-2c-c2-verification-substrate.md | 12 +++- tools/vertical_validation/src/main.rs | 56 +++++++++++++++++-- tools/vertical_validation/src/tla_runner.rs | 55 ++++++++++++++++++ 3 files changed, 118 insertions(+), 5 deletions(-) diff --git a/docs/papers/amendment-2c-c2-verification-substrate.md b/docs/papers/amendment-2c-c2-verification-substrate.md index b83b95662..cf8e51348 100644 --- a/docs/papers/amendment-2c-c2-verification-substrate.md +++ b/docs/papers/amendment-2c-c2-verification-substrate.md @@ -1168,7 +1168,17 @@ named storage-substrate exception. **Formal-model coverage — DISCHARGED under the stated symbolic assumptions (ruling G).** `lean4/DSMEconomicSmtSeparation.lean` carries obligations 1–7; `tla/DSM_EconRegisterObservation.tla` carries the concurrent register-observation half, with five deliberate-falsification configs that -are machine-gated on the invariant each must violate. This is coverage of the normative **models**, +are classified on the invariant each must violate. + +> **Correction, recorded after the fact.** This sentence originally read *"machine-gated"*. The +> classification was real — `run_all` normalizes every verdict and inverts the expected-to-fail +> configs correctly — but **CI could not act on it**: `tla-check` printed `FAILED specs: …` and +> returned `Ok`, and neither `main` nor the CI step converted that into a non-zero exit. A violated +> invariant, a falsification config that stopped falsifying, and a spec silently dropped from the +> registry were all green. The same defect affected `property-tests` and `implementation-traces`. +> The gate became load-bearing only with the corrective change that added exit-status enforcement +> and a registry-count tripwire; until then, "machine-gated" was true of the runner's bookkeeping +> and false of CI. This is coverage of the normative **models**, not a refinement proof from the Rust — see the claim boundary in ruling G. **Conformance surface — OWED.** Rev 15 has no conformance row for the economic register, `R_econ`, diff --git a/tools/vertical_validation/src/main.rs b/tools/vertical_validation/src/main.rs index 69768d8f2..3ec79b76a 100644 --- a/tools/vertical_validation/src/main.rs +++ b/tools/vertical_validation/src/main.rs @@ -180,11 +180,11 @@ async fn main() -> anyhow::Result<()> { } Commands::PropertyTests { iterations, seed } => { - run_property_tests(iterations, seed); + run_property_tests(iterations, seed)?; } Commands::ImplementationTraces => { - run_implementation_traces(); + run_implementation_traces()?; } Commands::Adversarial => { @@ -223,6 +223,26 @@ async fn main() -> anyhow::Result<()> { Ok(()) } +/// Turn an aggregate verdict into a process exit status. +/// +/// A gate that PRINTS "FAILED" and then exits 0 is not a gate. CI reads the +/// process status, not the report text, so a suite that summarises its own +/// failures and returns `Ok` is indistinguishable from a green one to the only +/// consumer that matters. +/// +/// Enforcement runs AFTER the report is printed, so the failing spec, property +/// or trace — and the invariant it violated — stay visible in the log. +fn enforce(gate: &str, total: usize, failing: &[String]) -> anyhow::Result<()> { + if failing.is_empty() { + return Ok(()); + } + anyhow::bail!( + "{gate}: {} of {total} FAILED — {}", + failing.len(), + failing.join(", ") + ) +} + /// Collect TLAPS proof results (progress on stderr, no report printed). async fn collect_proof_results( root: &std::path::Path, @@ -341,6 +361,18 @@ async fn run_tla_check( }; print!("{}", report.render_ascii()); + + // A violated invariant, or a falsification config that failed to falsify, + // must redden CI. `run_all` has already NORMALISED every verdict, including + // inverting the expected-to-fail configs, so `passed` here is the gate's + // answer and not TLC's raw one. + let failing: Vec = results + .iter() + .filter(|(_, r)| !r.passed) + .map(|(s, _)| s.label.clone()) + .collect(); + enforce("TLA+ model checking", results.len(), &failing)?; + Ok(results) } @@ -368,8 +400,15 @@ async fn run_benchmark( } /// Run property tests standalone. -fn run_property_tests(iterations: u64, seed: u64) { +fn run_property_tests(iterations: u64, seed: u64) -> anyhow::Result<()> { let results = property_tests::collect_property_test_results(seed, iterations); + let total = results.results.len(); + let failing: Vec = results + .results + .iter() + .filter(|r| !r.passed) + .map(|r| r.property_name.clone()) + .collect(); let report = VerticalValidationReport { proof_results: Vec::new(), tla_results: Vec::new(), @@ -381,11 +420,19 @@ fn run_property_tests(iterations: u64, seed: u64) { bilateral_throughput_results: None, }; print!("{}", report.render_ascii()); + enforce("Real-code bridge properties", total, &failing) } /// Run deterministic implementation traces standalone. -fn run_implementation_traces() { +fn run_implementation_traces() -> anyhow::Result<()> { let results = implementation_traces::collect_implementation_trace_results(); + let total = results.results.len(); + let failing: Vec = results + .results + .iter() + .filter(|r| !r.passed) + .map(|r| r.trace_name.clone()) + .collect(); let report = VerticalValidationReport { proof_results: Vec::new(), tla_results: Vec::new(), @@ -397,6 +444,7 @@ fn run_implementation_traces() { bilateral_throughput_results: None, }; print!("{}", report.render_ascii()); + enforce("Implementation traces", total, &failing) } /// Run adversarial tests standalone. diff --git a/tools/vertical_validation/src/tla_runner.rs b/tools/vertical_validation/src/tla_runner.rs index a33a3d356..18b2f25e0 100644 --- a/tools/vertical_validation/src/tla_runner.rs +++ b/tools/vertical_validation/src/tla_runner.rs @@ -23,6 +23,16 @@ use crate::tla_trace_replay::{ }; /// Configuration for a single TLA+ model check run. +/// How many specs `standard_specs()` must register. +/// +/// The registry is Rust, not a glob, so a spec deleted from `standard_specs` +/// leaves nothing behind for a file count to notice — the suite simply gets +/// smaller and stays green. This is the analogue of the Lean gate's +/// `expected=12` module count in CI, and it exists for the same reason: an +/// anti-skip tripwire is cheap, and a silently shrinking formal suite is the +/// failure mode that looks most like success. +pub const EXPECTED_STANDARD_SPECS: usize = 13; + #[derive(Debug, Clone, Serialize)] pub struct TlaSpec { /// Human-readable label (e.g., "DSM_tiny") @@ -592,6 +602,14 @@ impl TlaRunner { include_liveness: bool, ) -> anyhow::Result> { let mut specs = Self::standard_specs(); + if specs.len() != EXPECTED_STANDARD_SPECS { + anyhow::bail!( + "standard_specs() registers {} specs, expected {EXPECTED_STANDARD_SPECS}. \ + A spec was added or removed. Update EXPECTED_STANDARD_SPECS deliberately, \ + so that dropping a spec from the registry cannot leave this gate green.", + specs.len() + ); + } if include_liveness { specs.extend(Self::extended_specs()); } @@ -644,6 +662,43 @@ impl TlaRunner { } } +#[cfg(test)] +mod registry_tests { + use super::*; + + /// The registry is the suite. `run_all` bails on a mismatch so CI cannot go + /// green on a shrunken suite, and this test fails the same way in + /// `cargo test` — before anyone waits on TLC — so the count is corrected + /// deliberately rather than discovered in a model-checking log. + #[test] + fn the_standard_spec_registry_is_the_expected_size() { + assert_eq!( + TlaRunner::standard_specs().len(), + EXPECTED_STANDARD_SPECS, + "standard_specs() changed size. Update EXPECTED_STANDARD_SPECS on purpose." + ); + } + + /// Every falsification config must name an invariant the spec actually + /// declares. A typo here degrades silently into "a different failure", + /// which reads as a real defect in the model rather than in the registry. + #[test] + fn every_falsification_config_names_an_invariant_its_spec_declares() { + for spec in TlaRunner::standard_specs() { + let Some(expected) = spec.expect_violation.as_deref() else { + continue; + }; + assert!( + spec.invariants.iter().any(|i| i == expected), + "{} expects a violation of `{expected}`, which is not in its own \ + declared invariants {:?}", + spec.label, + spec.invariants + ); + } + } +} + fn dfid_depth_for_config(config_text: &str) -> u64 { let Some(re) = Regex::new(r"(?m)^\s*(MaxStep|MaxChain)\s*=\s*(\d+)\b").ok() else { return 10;