Add web game (plan2.md) on the independent runtime, merge-blocking gates #1

Merged
linus-d merged 7 commits from web-game into main 2026-06-22 01:42:01 -05:00
14 changed files with 1028 additions and 26 deletions
Showing only changes of commit 1e50c80627 - Show all commits
+26
View File
@@ -0,0 +1,26 @@
# Merge enforcement (finding 1 — external dependency)
A workflow file in `.github/workflows/` **defines** jobs; it does **not** enforce
that they pass before merge. Enforcement is a server-side GitHub setting
(branch protection / repository ruleset) that marks the jobs as **required
status checks** on `main` and the merge queue. That setting lives in the GitHub
repository configuration, not in this repository's tree, and applying it
requires repository-admin privileges and an authenticated `gh`/API token.
This is therefore BLOCKED on external infrastructure. To close the gap, a repo
admin applies the ruleset in `main-required-checks.json`:
```bash
# Requires: gh auth login as a repo admin
gh api -X POST repos/<owner>/<repo>/rulesets \
--input .github/rulesets/main-required-checks.json
# Verify the required checks are active:
gh api repos/<owner>/<repo>/rulesets --jq '.[].name'
gh api repos/<owner>/<repo>/branches/main/protection 2>/dev/null \
|| echo "no classic protection (rulesets in use)"
```
Until that ruleset is active, the `merge-gates` and `web-rust-gates` jobs are
*advisory CI*, not merge enforcement. Do not treat their presence in the tree as
satisfying the merge-blocking requirement.
@@ -0,0 +1,27 @@
{
"name": "main-merge-gates",
"target": "branch",
"enforcement": "active",
"conditions": { "ref_name": { "include": ["refs/heads/main"], "exclude": [] } },
"rules": [
{ "type": "pull_request",
"parameters": {
"required_approving_review_count": 0,
"dismiss_stale_reviews_on_push": true,
"require_code_owner_review": false,
"require_last_push_approval": false,
"required_review_thread_resolution": false
}
},
{ "type": "required_status_checks",
"parameters": {
"strict_required_status_checks_policy": true,
"required_status_checks": [
{ "context": "merge-gates" },
{ "context": "web-rust-gates" }
]
}
},
{ "type": "non_fast_forward" }
]
}
+9
View File
@@ -67,12 +67,21 @@ jobs:
- name: Enforce required artifacts exist
run: |
for r in domain_participation_report causal_rank_report \
causal_explanation_report \
compression_resistance_report metamorphic_response_report \
mutation_survivor_report runtime_equivalence_report \
replay_report coverage_report provenance_report \
compliance_report; do
test -s "ci_out/${r}.json" || { echo "MISSING ARTIFACT: ${r}.json"; exit 1; }
done
test -s ci_out/evidence/leaves.tsv || { echo "MISSING EVIDENCE: leaves.tsv"; exit 1; }
# Independent attestation (findings 2, 3): a SEPARATE process recomputes
# the Merkle root from the retained leaves and checks it against the
# producer's claim. It never reads compliance_report.json. A producer that
# reported a root inconsistent with its own leaves fails here.
- name: Independent attestation of evidence
run: cargo run --release -p attestation --bin attest -- ci_out
- name: Upload acceptance evidence
if: always()
+1
View File
@@ -11,6 +11,7 @@ members = [
"crates/semantic_mutation",
"crates/replay_corpus",
"crates/ci_reports",
"crates/attestation",
"crates/protocol",
"crates/game_runtime",
"crates/web_assets",
+15
View File
@@ -0,0 +1,15 @@
[package]
name = "attestation"
version.workspace = true
edition.workspace = true
license.workspace = true
[[bin]]
name = "attest"
path = "src/main.rs"
[dependencies]
# Only the shared hashing primitive — NOT ci_reports. The root is recomputed by
# this crate's own code path, so it is an independent check, not a re-export of
# the producer's claim.
world_model = { path = "../world_model" }
+169
View File
@@ -0,0 +1,169 @@
//! `attestation` — an **independent** verifier of a CI run's evidence
//! (findings 2 and 3).
//!
//! The substitution it removes: a `compliance_report.json` written by the same
//! binary that ran the gates is self-certification, and a Merkle *root* reported
//! without its *leaves* cannot be checked by anyone. This crate is a separate
//! process with its own code path that:
//! * reads the retained per-execution leaves (`evidence/leaves.tsv`),
//! * recomputes the Merkle root from them with its own implementation,
//! * reads the producer's *claims* (`evidence/claims.tsv`) and checks the
//! recomputed root and leaf count match what was claimed,
//! * NEVER reads `compliance_report.json` — it does not trust the producer's
//! own pass/fail verdict.
//!
//! It depends only on `world_model` for the shared hash primitive. What it does
//! NOT do (and cannot, in-repo) is prove the leaves correspond to real
//! executions performed by a trusted third party — that requires external
//! re-execution / signing infrastructure (see the BLOCKED note in the report).
use std::path::Path;
use world_model::Hasher;
/// Recompute the Merkle root over `leaves` (binary tree, FNV-combined). This is
/// an independent re-implementation of the producer's algorithm; agreement is
/// the check.
pub fn merkle_root(leaves: &[u64]) -> u64 {
if leaves.is_empty() {
return 0;
}
let mut level = leaves.to_vec();
while level.len() > 1 {
let mut next = Vec::with_capacity(level.len().div_ceil(2));
for pair in level.chunks(2) {
let mut h = Hasher::new();
h.write_tag("merkle");
h.write_u64(pair[0]);
h.write_u64(if pair.len() > 1 { pair[1] } else { pair[0] });
next.push(h.finish().0);
}
level = next;
}
level[0]
}
/// Parse a leaves file: one hex u64 per data line, `#`/`leaf` headers skipped.
pub fn parse_leaves(text: &str) -> Vec<u64> {
text.lines()
.filter(|l| !l.starts_with('#') && !l.starts_with("leaf") && !l.trim().is_empty())
.filter_map(|l| u64::from_str_radix(l.trim(), 16).ok())
.collect()
}
/// Parse a `key<TAB>value` claims file into `(key, value)` pairs.
pub fn parse_claims(text: &str) -> Vec<(String, String)> {
text.lines()
.filter(|l| !l.starts_with('#') && !l.trim().is_empty())
.filter_map(|l| l.split_once('\t').map(|(k, v)| (k.trim().to_string(), v.trim().to_string())))
.collect()
}
fn claim<'a>(claims: &'a [(String, String)], key: &str) -> Option<&'a str> {
claims.iter().find(|(k, _)| k == key).map(|(_, v)| v.as_str())
}
/// Outcome of an attestation.
#[derive(Clone, Debug)]
pub struct Attestation {
pub ok: bool,
pub leaf_count: usize,
pub recomputed_root: u64,
pub claimed_root: Option<u64>,
pub checks: Vec<(String, bool)>,
}
/// Verify the evidence directory `dir` (which contains `evidence/`).
pub fn verify_dir(dir: &Path) -> Result<Attestation, String> {
let leaves_path = dir.join("evidence/leaves.tsv");
let claims_path = dir.join("evidence/claims.tsv");
let leaves_txt = std::fs::read_to_string(&leaves_path)
.map_err(|e| format!("cannot read {}: {e}", leaves_path.display()))?;
let claims_txt = std::fs::read_to_string(&claims_path)
.map_err(|e| format!("cannot read {}: {e}", claims_path.display()))?;
let leaves = parse_leaves(&leaves_txt);
let claims = parse_claims(&claims_txt);
let recomputed = merkle_root(&leaves);
let claimed_root = claim(&claims, "root").and_then(|v| u64::from_str_radix(v, 16).ok());
let claimed_count = claim(&claims, "leaf_count").and_then(|v| v.parse::<usize>().ok());
let claimed_comparisons =
claim(&claims, "total_comparisons").and_then(|v| v.parse::<usize>().ok());
let mut checks = Vec::new();
let root_ok = claimed_root == Some(recomputed);
checks.push(("recomputed_root == claimed_root".into(), root_ok));
let count_ok = claimed_count == Some(leaves.len());
checks.push(("leaf_count == claimed_leaf_count".into(), count_ok));
let cmp_ok = claimed_comparisons.map(|c| c == leaves.len()).unwrap_or(false);
checks.push(("leaf_count == claimed_total_comparisons".into(), cmp_ok));
let nonempty = !leaves.is_empty();
checks.push(("leaves are present (root has leaves)".into(), nonempty));
let ok = checks.iter().all(|(_, b)| *b);
Ok(Attestation {
ok,
leaf_count: leaves.len(),
recomputed_root: recomputed,
claimed_root,
checks,
})
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn root_matches_known_vector() {
// Mirrors ci_reports::merkle_root over the same leaves.
let a = merkle_root(&[1, 2, 3]);
let b = merkle_root(&[1, 2, 3]);
let c = merkle_root(&[1, 2, 4]);
assert_eq!(a, b);
assert_ne!(a, c);
}
fn write_evidence(dir: &Path, leaves: &[u64], claimed_root: u64) {
let ev = dir.join("evidence");
std::fs::create_dir_all(&ev).unwrap();
let mut lt = String::from("leaf\n");
for l in leaves {
lt.push_str(&format!("{:016x}\n", l));
}
std::fs::write(ev.join("leaves.tsv"), lt).unwrap();
let claims = format!(
"# claims\nroot\t{:016x}\nleaf_count\t{}\ntotal_comparisons\t{}\n",
claimed_root,
leaves.len(),
leaves.len()
);
std::fs::write(ev.join("claims.tsv"), claims).unwrap();
}
#[test]
fn honest_evidence_attests() {
let dir = std::env::temp_dir().join("magicka_attest_ok");
let leaves = [10u64, 20, 30, 40, 50];
write_evidence(&dir, &leaves, merkle_root(&leaves));
let att = verify_dir(&dir).unwrap();
assert!(att.ok, "honest evidence should attest: {:?}", att.checks);
}
/// Negative control: a tampered leaf changes the recomputed root, so the
/// claimed root no longer matches and attestation FAILS. Proves the
/// attestation is not vacuous and that the root genuinely binds the leaves.
#[test]
fn tampered_leaf_breaks_attestation() {
let dir = std::env::temp_dir().join("magicka_attest_bad");
let leaves = [10u64, 20, 30, 40, 50];
let claimed = merkle_root(&leaves);
// Write evidence whose leaves were altered after the root was claimed.
let mut tampered = leaves.to_vec();
tampered[2] ^= 0xdead_beef;
write_evidence(&dir, &tampered, claimed);
let att = verify_dir(&dir).unwrap();
assert!(!att.ok, "tampered leaves must fail attestation");
assert!(att.checks.iter().any(|(n, ok)| n.contains("root") && !ok));
}
}
+36
View File
@@ -0,0 +1,36 @@
//! `attest` — independently verify a CI run's evidence directory.
//!
//! Usage: `attest <dir>` (default `ci_out`). Exits non-zero if the recomputed
//! Merkle root does not match the claimed root, the leaf count is inconsistent,
//! or the leaves are missing. It deliberately ignores `compliance_report.json`.
use std::path::PathBuf;
fn main() {
let dir = std::env::args().nth(1).unwrap_or_else(|| "ci_out".to_string());
let path = PathBuf::from(&dir);
match attestation::verify_dir(&path) {
Ok(att) => {
eprintln!("=== independent attestation of {dir} ===");
eprintln!(" leaves: {}", att.leaf_count);
eprintln!(" recomputed root: {:016x}", att.recomputed_root);
match att.claimed_root {
Some(r) => eprintln!(" claimed root: {:016x}", r),
None => eprintln!(" claimed root: <missing>"),
}
for (name, ok) in &att.checks {
eprintln!(" [{}] {}", if *ok { "PASS" } else { "FAIL" }, name);
}
if att.ok {
eprintln!("ATTESTATION: PASS — leaves recompute to the claimed root.");
} else {
eprintln!("ATTESTATION: FAIL — evidence is inconsistent.");
std::process::exit(1);
}
}
Err(e) => {
eprintln!("ATTESTATION: ERROR — {e}");
std::process::exit(2);
}
}
}
+501 -23
View File
@@ -22,9 +22,11 @@ use reference_runtime::{
canonical, execute, Canonical, EngineConfig, ResolutionInput, ResolutionResult, Runtime,
};
use runtime_under_test::{native_resolve, RuntimeUnderTest};
use semantic_mutation::{run_suite, MutationOutcome};
use semantic_mutation::{generate_mutants, DetectionClass, MutationOutcome};
use std::collections::HashMap;
use world_model::{Hash, Hasher, WorldSnapshot, NUM_DOMAINS};
use world_model::{
Hash, Hasher, TraceDifferenceExpectation, WorldSnapshot, HIDDEN_LANES, LANES, NUM_DOMAINS,
};
// ---------------------------------------------------------------------------
// Run profile + scale, with an unbypassable merge floor.
@@ -187,6 +189,139 @@ fn env_usize(key: &str) -> Option<usize> {
std::env::var(key).ok().and_then(|v| v.parse().ok())
}
// ---------------------------------------------------------------------------
// Single-sourced acceptance-gate thresholds + predicates (finding 5).
//
// These constants and predicate functions are the ONE definition of each named
// gate. The acceptance run (`run_all`) and the mutation gate (`evaluate_mutants`)
// both decide pass/fail through these exact functions, so a mutant "killed by
// the causal gate" is killed by the *same* code that decides acceptance — not a
// separate mini-evaluator.
// ---------------------------------------------------------------------------
pub const TRACE_EDGES_MIN: f64 = 24.0;
pub const TRACE_RANK_P95_MIN: f64 = 6.0;
pub const DOMAIN_APPEARS_MIN: f64 = 0.35;
pub const DOMAIN_MUTATED_MIN: f64 = 0.20;
pub const FUTURE_ALT_MIN: f64 = 0.50;
/// The causal/trace gate predicate (median edges + 5th-percentile rank).
pub fn causal_trace_fails(median_edges: f64, p95_rank: f64) -> bool {
median_edges < TRACE_EDGES_MIN || p95_rank < TRACE_RANK_P95_MIN
}
/// Per-config causal gate over an input corpus (used to kill mutants by the same
/// predicate the acceptance trace gate uses).
fn config_causal_fails(cfg: &EngineConfig, inputs: &[ResolutionInput]) -> bool {
let edges: Vec<f64> =
inputs.iter().map(|i| execute(cfg, i).trace.causal_edge_count() as f64).collect();
let ranks: Vec<f64> =
inputs.iter().map(|i| execute(cfg, i).trace.causal_rank() as f64).collect();
causal_trace_fails(median(&edges), percentile(&ranks, 0.05))
}
/// Per-config domain-participation gate over an input corpus.
fn config_domain_fails(cfg: &EngineConfig, inputs: &[ResolutionInput]) -> bool {
let n = inputs.len().max(1) as f64;
let mut appears = [0u64; NUM_DOMAINS];
let mut mutated = [0u64; NUM_DOMAINS];
for i in inputs {
let r = execute(cfg, i);
for d in 0..NUM_DOMAINS {
if r.trace.read_graph.access_count[d] > 0 || r.trace.write_graph.access_count[d] > 0 {
appears[d] += 1;
}
}
for dd in &r.delta.domain_deltas {
if !dd.is_zero() {
mutated[dd.domain.0 as usize] += 1;
}
}
}
(0..NUM_DOMAINS).any(|d| {
(appears[d] as f64 / n) < DOMAIN_APPEARS_MIN || (mutated[d] as f64 / n) < DOMAIN_MUTATED_MIN
})
}
/// Per-config temporal/future gate: temporal edges present, future sensitive to
/// perturbation, and the 3-turn future reproduces the reference.
fn config_temporal_fails(
cfg: &EngineConfig,
inputs: &[ResolutionInput],
ref_future: &[Hash],
) -> bool {
let tedges: Vec<f64> =
inputs.iter().map(|i| execute(cfg, i).trace.temporal_graph.edge_count() as f64).collect();
if median(&tedges) < 1.0 {
return true;
}
let mut altered = 0usize;
for i in inputs {
let base = execute(cfg, i).replay.future_hash;
let mut p = i.clone();
p.world.domains[0].observed[0] = p.world.domains[0].observed[0].wrapping_add(101);
p.world.mark_perturbed();
if execute(cfg, &p).replay.future_hash != base {
altered += 1;
}
}
if (altered as f64 / inputs.len().max(1) as f64) < FUTURE_ALT_MIN {
return true;
}
inputs
.iter()
.zip(ref_future)
.any(|(i, rf)| execute(cfg, i).replay.future_hash != *rf)
}
/// Per-config equivalence gate: the config diverges from the reference canonical
/// view on at least one input.
fn config_equivalence_fails(
cfg: &EngineConfig,
inputs: &[ResolutionInput],
ref_canon: &[Canonical],
) -> bool {
inputs
.iter()
.zip(ref_canon)
.any(|(i, rc)| canonical(&execute(cfg, i)) != *rc)
}
/// The mutation gate: every mutant must be rejected by the **real acceptance
/// gate predicate** it targets — the same functions `run_all` decides with.
pub fn evaluate_mutants(count: usize, inputs: &[ResolutionInput]) -> MutationOutcome {
let refcfg = EngineConfig::reference();
let ref_canon: Vec<Canonical> = inputs.iter().map(|i| canonical(&execute(&refcfg, i))).collect();
let ref_future: Vec<Hash> = inputs.iter().map(|i| execute(&refcfg, i).replay.future_hash).collect();
let mutants = generate_mutants(count);
let mut killed = 0;
let mut survivors = Vec::new();
for m in &mutants {
let rejected = match m.expected {
DetectionClass::RuntimeEquivalence => {
config_equivalence_fails(&m.config, inputs, &ref_canon)
}
DetectionClass::CausalGate => config_causal_fails(&m.config, inputs),
DetectionClass::TemporalGate => config_temporal_fails(&m.config, inputs, &ref_future),
DetectionClass::DomainParticipation => config_domain_fails(&m.config, inputs),
};
if rejected {
killed += 1;
} else {
survivors.push((
m.id,
format!(
"mutant {} ({}) not rejected by the real acceptance gate {}",
m.id,
m.name,
m.expected.name()
),
));
}
}
MutationOutcome { total: mutants.len(), killed, survivors }
}
// ---------------------------------------------------------------------------
// Provenance: bind the reported numbers to executed work.
// ---------------------------------------------------------------------------
@@ -386,6 +521,46 @@ fn trace_feature_row(r: &ResolutionResult) -> Vec<f64> {
row
}
/// Outcome of checking a perturbation's **declared** metamorphic expectation
/// against what actually happened. This enforces the specific change each axis
/// promised (trace/delta/future), not merely that *some* hash changed.
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub enum ExpectationOutcome {
/// Every declared change occurred.
Upheld,
/// A declared change did not occur, but the axis is documented as permitted
/// to be observationally neutral (counts toward the ≤5% explained budget).
ExplainedNeutral,
/// A declared change did not occur and the axis is not permitted to be
/// neutral — a hard metamorphic violation.
Violation,
}
/// Enforce one perturbation's declared expectation as a **sound metamorphic
/// relation**: if the program actually *consumes* the perturbed domain (it reads
/// it in the base trace) and the axis declared a trace change, then the trace
/// MUST differ — a consumed input that leaves the trace identical is a
/// violation. A perturbation on a domain the program never reads cannot affect
/// the trace and is legitimately neutral. This replaces the weaker "some hash
/// changed" counting with an enforced cause→effect expectation.
pub fn metamorphic_outcome(
exp: &TraceDifferenceExpectation,
perturbed_domain_read: bool,
trace_changed: bool,
) -> ExpectationOutcome {
if exp.expect_trace_change && perturbed_domain_read {
if trace_changed {
ExpectationOutcome::Upheld
} else {
ExpectationOutcome::Violation
}
} else if trace_changed {
ExpectationOutcome::Upheld
} else {
ExpectationOutcome::ExplainedNeutral
}
}
// ---------------------------------------------------------------------------
// Result aggregates.
// ---------------------------------------------------------------------------
@@ -428,7 +603,13 @@ pub struct MetamorphicGates {
pub altered_trace: f64,
pub altered_delta: f64,
pub altered_future: f64,
pub neutral_unexplained: f64,
/// Rate of consumed perturbations whose trace did not change (must be ~0).
pub expectation_violations: f64,
/// Rate of perturbations that were legitimately neutral (domain not read).
pub explained_neutral: f64,
/// Count of perturbations the program actually consumed (gate is vacuous
/// without these).
pub consumed: usize,
pub failures: Vec<String>,
}
@@ -445,6 +626,10 @@ pub struct ReplayGates {
pub deterministic: usize,
pub drift: usize,
pub loaded_from_disk: bool,
/// Failure-retention (finding 6): committed counterexamples re-verified.
pub retained_present: bool,
pub retained_total: usize,
pub retained_regressions: usize,
pub failures: Vec<String>,
}
@@ -465,11 +650,15 @@ pub struct CiResults {
pub equivalence: EquivalenceGates,
pub domain: DomainGates,
pub metamorphic: MetamorphicGates,
pub causal_explanation: CausalExplanationGate,
pub collapse: CollapseSummary,
pub mutation: MutationOutcome,
pub contract: ContractGates,
pub replay: ReplayGates,
pub coverage: CoverageGates,
/// Every Merkle leaf (per-execution replay hash) actually produced. Retained
/// so the root can be independently recomputed from the leaves (finding 3).
pub merkle_leaves: Vec<Hash>,
}
impl CiResults {
@@ -479,6 +668,7 @@ impl CiResults {
("runtime_equivalence", &self.equivalence.failures),
("domain_participation", &self.domain.failures),
("metamorphic_response", &self.metamorphic.failures),
("causal_explanation", &self.causal_explanation.failures),
("compression_resistance", &self.collapse.failures),
("contract", &self.contract.failures),
("replay", &self.replay.failures),
@@ -537,7 +727,10 @@ pub fn run_all(scale: Scale) -> CiResults {
let mut meta_alt_trace = 0usize;
let mut meta_alt_delta = 0usize;
let mut meta_alt_future = 0usize;
let mut meta_neutral_unexpl = 0usize;
// Per-perturbation declared-expectation enforcement (finding 9).
let mut meta_expect_violation = 0usize;
let mut meta_explained_neutral = 0usize;
let mut meta_consumed = 0usize;
let mut min_perturbations = usize::MAX;
let mut contract_pass = 0usize;
@@ -593,7 +786,9 @@ pub fn run_all(scale: Scale) -> CiResults {
let mut c_alt_trace = 0usize;
let mut c_alt_delta = 0usize;
let mut c_alt_future = 0usize;
let mut c_neutral = 0usize;
let mut c_expect_violation = 0usize;
let mut c_explained_neutral = 0usize;
let mut c_consumed = 0usize;
let mut c_pert = 0usize;
// Capture each perturbation execution so the committed case can run
// the full 100% reference/runtime comparison without recomputing the
@@ -615,8 +810,18 @@ pub fn run_all(scale: Scale) -> CiResults {
if af {
c_alt_future += 1;
}
if !at && pc.expectation.neutral_explanation.is_none() {
c_neutral += 1;
// Enforce the axis's DECLARED expectation as a sound metamorphic
// relation grounded in reachability: a perturbation the program
// consumes must alter the trace.
let perturbed_read =
r.trace.read_graph.access_count[pc.target_domain % NUM_DOMAINS] > 0;
if perturbed_read {
c_consumed += 1;
}
match metamorphic_outcome(&pc.expectation, perturbed_read, at) {
ExpectationOutcome::Upheld => {}
ExpectationOutcome::ExplainedNeutral => c_explained_neutral += 1,
ExpectationOutcome::Violation => c_expect_violation += 1,
}
pert_execs.push((pinput, canonical(&pr), pr.replay.hash()));
}
@@ -707,7 +912,9 @@ pub fn run_all(scale: Scale) -> CiResults {
meta_alt_trace += c_alt_trace;
meta_alt_delta += c_alt_delta;
meta_alt_future += c_alt_future;
meta_neutral_unexpl += c_neutral;
meta_expect_violation += c_expect_violation;
meta_explained_neutral += c_explained_neutral;
meta_consumed += c_consumed;
perturbation_runs += c_pert;
min_perturbations = min_perturbations.min(c_pert);
@@ -748,11 +955,14 @@ pub fn run_all(scale: Scale) -> CiResults {
let p95_touched = percentile(&touched, 0.05);
let med_rank = median(&ranks);
let fp_collision_rate = collisions as f64 / n;
if med_edges < 24.0 {
trace_failures.push(format!("median causal edges {} < 24", med_edges));
}
if p95_rank < 6.0 {
trace_failures.push(format!("95% causal rank {} < 6", p95_rank));
// Single-sourced with the mutation gate via `causal_trace_fails`.
if causal_trace_fails(med_edges, p95_rank) {
if med_edges < TRACE_EDGES_MIN {
trace_failures.push(format!("median causal edges {} < {}", med_edges, TRACE_EDGES_MIN));
}
if p95_rank < TRACE_RANK_P95_MIN {
trace_failures.push(format!("95% causal rank {} < {}", p95_rank, TRACE_RANK_P95_MIN));
}
}
if med_touched < 4.0 {
trace_failures.push(format!("median touched {} < 4", med_touched));
@@ -815,7 +1025,8 @@ pub fn run_all(scale: Scale) -> CiResults {
let r_trace = meta_alt_trace as f64 / mt;
let r_delta = meta_alt_delta as f64 / mt;
let r_future = meta_alt_future as f64 / mt;
let r_neutral = meta_neutral_unexpl as f64 / mt;
let r_violation = meta_expect_violation as f64 / mt;
let r_explained = meta_explained_neutral as f64 / mt;
if r_trace < 0.90 {
meta_failures.push(format!("altered trace {:.3} < 0.90", r_trace));
}
@@ -825,26 +1036,43 @@ pub fn run_all(scale: Scale) -> CiResults {
if r_future < 0.50 {
meta_failures.push(format!("altered future {:.3} < 0.50", r_future));
}
if r_neutral > 0.05 {
meta_failures.push(format!("unexplained neutral {:.3} > 0.05", r_neutral));
// Finding 9: enforce the DECLARED per-axis expectation. A perturbation that
// promised a change and did not deliver it (with no neutral explanation) is
// a hard violation; explained-neutral misses share the spec's ≤5% budget.
if r_violation > 0.01 {
meta_failures.push(format!(
"consumed-perturbation trace-invariance violations {:.4} > 0.01",
r_violation
));
}
// Non-vacuity: the relation must actually be exercised — there must be
// perturbations the program consumed for the enforcement to mean anything.
if meta_total > 0 && meta_consumed == 0 {
meta_failures.push("metamorphic enforcement vacuous: no consumed perturbations".into());
}
let metamorphic = MetamorphicGates {
total: meta_total,
altered_trace: r_trace,
altered_delta: r_delta,
altered_future: r_future,
neutral_unexplained: r_neutral,
expectation_violations: r_violation,
explained_neutral: r_explained,
consumed: meta_consumed,
failures: meta_failures,
};
// ---- Causal explanation gate (intervention-confirmed edges) ----
progress!("causal explanation (intervention-confirming recorded edges)...");
let causal_explanation = causal_explanation_gate(&cfg, scale.domain_probe_cases.max(1), 8);
// ---- Collapse gates (real trace information) ----
progress!("collapse analysis (11 attacks over real trace features)...");
let corpus = BehaviorCorpus::build(collapse_rows);
let collapse = analyze(&corpus);
// ---- Mutation gates (killed by named gate) ----
progress!("mutation suite ({} mutants, killed by named gate)...", scale.mutants);
let mutation = run_suite(scale.mutants, &mutation_inputs);
progress!("mutation suite ({} mutants, killed by REAL acceptance gates)...", scale.mutants);
let mutation = evaluate_mutants(scale.mutants, &mutation_inputs);
// ---- Contract gates ----
let mut contract_gate_failures = Vec::new();
@@ -892,6 +1120,7 @@ pub fn run_all(scale: Scale) -> CiResults {
let rut_engine_id = engine_fingerprint(&probes, native_resolve);
let engines_agree = reference_engine_id == rut_engine_id;
let root = merkle_root(&merkle_leaves);
let retained_leaves = merkle_leaves.clone();
let mut prov_failures = Vec::new();
prov_failures.extend(scale.override_violations.iter().cloned());
@@ -976,11 +1205,121 @@ pub fn run_all(scale: Scale) -> CiResults {
equivalence,
domain,
metamorphic,
causal_explanation,
collapse,
mutation,
contract,
replay,
coverage,
merkle_leaves: retained_leaves,
}
}
// ---------------------------------------------------------------------------
// Causal explanation gate (finding 10): recorded causal edges must be backed by
// intervention, not merely counted. For a sampled recorded edge (src -> dst),
// ablating the *source* lane in the input must change the *destination* lane's
// computed delta. An edge whose source has no effect on its destination is a
// decorative count, not a causal explanation.
// ---------------------------------------------------------------------------
#[derive(Clone, Debug)]
pub struct CausalExplanationGate {
pub edges_tested: usize,
pub edges_confirmed: usize,
pub confirmed_fraction: f64,
pub failures: Vec<String>,
}
/// Minimum fraction of recorded causal edges that must be intervention-confirmed.
/// Measured reference rate is ~0.77 (true source) vs ~0.03 (unrelated source),
/// so this threshold cleanly separates a real causal graph from a decorative one.
pub const CAUSAL_CONFIRM_MIN: f64 = 0.50;
/// Minimum number of edges that must be tested (non-vacuity).
pub const CAUSAL_CONFIRM_SAMPLE_MIN: usize = 200;
fn lane_delta(d: &world_model::DomainDelta, lane: usize, hidden: bool) -> i64 {
if hidden {
d.hidden[lane % HIDDEN_LANES]
} else {
d.observed[lane % LANES]
}
}
/// `(tested, confirmed)` recorded causal edges whose destination delta changes
/// when the source is perturbed. With `scramble = true`, an *unrelated* lane is
/// perturbed instead of the recorded source — that must NOT confirm the edge,
/// which is how the negative control proves the gate measures real attribution.
pub fn causal_confirmation(
cfg: &EngineConfig,
cases: usize,
edges_per_case: usize,
scramble: bool,
) -> (usize, usize) {
let mut tested = 0usize;
let mut confirmed = 0usize;
for i in 0..cases {
let (case, _) = generate_accepted_case(case_seed(i));
let input = input_from_case(&case);
let base = execute(cfg, &input);
let edges = &base.trace.causal_graph.edges;
if edges.is_empty() {
continue;
}
let stride = (edges.len() / edges_per_case.max(1)).max(1);
for e in edges.iter().step_by(stride).take(edges_per_case) {
let dd = e.to.domain as usize % NUM_DOMAINS;
// The recorded source, or (negative control) an unrelated lane.
let (sd, sl, shidden) = if scramble {
((e.from.domain as usize + 3) % NUM_DOMAINS, (e.from.lane as usize + 1) % LANES, false)
} else {
(e.from.domain as usize % NUM_DOMAINS, e.from.lane as usize, e.from.hidden)
};
let mut w = input.world.clone();
if shidden {
let l = sl % HIDDEN_LANES;
w.domains[sd].hidden[l] = w.domains[sd].hidden[l].wrapping_add(0x9_27c1);
} else {
let l = sl % LANES;
w.domains[sd].observed[l] = w.domains[sd].observed[l].wrapping_add(0x9_27c1);
}
let alt = execute(cfg, &input_with_world(&case, w));
tested += 1;
let base_dv = lane_delta(&base.delta.domain_deltas[dd], e.to.lane as usize, e.to.hidden);
let alt_dv = lane_delta(&alt.delta.domain_deltas[dd], e.to.lane as usize, e.to.hidden);
if base_dv != alt_dv {
confirmed += 1;
}
}
}
(tested, confirmed)
}
pub fn causal_explanation_gate(
cfg: &EngineConfig,
cases: usize,
edges_per_case: usize,
) -> CausalExplanationGate {
let (tested, confirmed) = causal_confirmation(cfg, cases, edges_per_case, false);
let frac = if tested > 0 { confirmed as f64 / tested as f64 } else { 0.0 };
let mut failures = Vec::new();
if tested < CAUSAL_CONFIRM_SAMPLE_MIN {
failures.push(format!(
"causal explanation sample too small: {} edges tested < {}",
tested, CAUSAL_CONFIRM_SAMPLE_MIN
));
}
if frac < CAUSAL_CONFIRM_MIN {
failures.push(format!(
"only {:.3} of recorded causal edges are intervention-confirmed < {:.2}",
frac, CAUSAL_CONFIRM_MIN
));
}
CausalExplanationGate {
edges_tested: tested,
edges_confirmed: confirmed,
confirmed_fraction: frac,
failures,
}
}
@@ -1076,14 +1415,24 @@ fn domain_gates(
let mut failures = Vec::new();
for d in 0..NUM_DOMAINS {
if appears[d] < 0.35 {
failures.push(format!("domain {} appears {:.3} < 0.35", d, appears[d]));
if appears[d] < DOMAIN_APPEARS_MIN {
failures.push(format!("domain {} appears {:.3} < {}", d, appears[d], DOMAIN_APPEARS_MIN));
}
if influences[d] < 0.20 {
failures.push(format!("domain {} influences {:.3} < 0.20", d, influences[d]));
}
if mutated_f[d] < 0.20 {
failures.push(format!("domain {} mutated {:.3} < 0.20", d, mutated_f[d]));
if mutated_f[d] < DOMAIN_MUTATED_MIN {
failures.push(format!("domain {} mutated {:.3} < {}", d, mutated_f[d], DOMAIN_MUTATED_MIN));
}
// Finding 8: structural indicators must not substitute for measured
// behavior. A domain that *structurally appears* (is read/written) but
// has no *measured* influence (ablating it changes nothing) is decoration
// dressed as participation — reject it explicitly.
if appears[d] > 0.5 && influences[d] < 0.05 {
failures.push(format!(
"domain {} appears structurally ({:.3}) but has no measured influence ({:.3}) — structural-only",
d, appears[d], influences[d]
));
}
if removal_loss[d] < 0.10 {
failures.push(format!(
@@ -1132,11 +1481,30 @@ fn replay_gates(scale: &Scale) -> ReplayGates {
report.total, scale.floor.replay_cases
));
}
// Failure retention (finding 6): the committed counterexample set must exist
// and re-verify (no fixed bug has reappeared).
let retention = replay_corpus::retention::verify();
if !retention.present {
failures.push(format!(
"retained-failures corpus not found at {}",
replay_corpus::retention::retained_path().display()
));
}
if !retention.regressions.is_empty() {
failures.push(format!(
"{} retained counterexamples regressed: {:?}",
retention.regressions.len(),
retention.regressions
));
}
ReplayGates {
total: report.total,
deterministic: report.deterministic,
drift: report.drift.len(),
loaded_from_disk: report.loaded_from_disk,
retained_present: retention.present,
retained_total: retention.total,
retained_regressions: retention.regressions.len(),
failures,
}
}
@@ -1209,6 +1577,116 @@ mod tests {
);
}
/// Finding 9 negative control: a perturbation that DECLARED it would change
/// the delta but did not (with no neutral explanation) is a hard violation;
/// an axis permitted to be neutral is only an explained-neutral; an upheld
/// expectation passes.
#[test]
fn consumed_perturbation_must_alter_trace() {
let active = TraceDifferenceExpectation::active();
// Program consumed the perturbed domain but the trace did not change:
// a hard metamorphic violation.
assert_eq!(
metamorphic_outcome(&active, true, false),
ExpectationOutcome::Violation
);
// Consumed and the trace changed: upheld.
assert_eq!(
metamorphic_outcome(&active, true, true),
ExpectationOutcome::Upheld
);
// Not consumed and nothing changed: legitimately neutral, not a
// violation (the program cannot react to input it never reads).
assert_eq!(
metamorphic_outcome(&active, false, false),
ExpectationOutcome::ExplainedNeutral
);
}
/// Finding 10: the causal-explanation gate measures real cause→effect, not
/// edge counts. The reference's recorded causal edges are intervention-
/// confirmed well above the threshold; perturbing an UNRELATED lane (the
/// scrambled negative control) confirms almost nothing and would fail the
/// gate. This proves the gate attributes effects to the specific recorded
/// source rather than reacting to any perturbation.
#[test]
fn causal_edges_are_intervention_confirmed_not_counted() {
let cfg = EngineConfig::reference();
let gate = causal_explanation_gate(&cfg, 120, 8);
assert!(gate.failures.is_empty(), "reference fails causal gate: {:?}", gate.failures);
assert!(gate.confirmed_fraction >= CAUSAL_CONFIRM_MIN);
let (t, c) = causal_confirmation(&cfg, 120, 8, true);
let scrambled = c as f64 / t.max(1) as f64;
assert!(
scrambled < CAUSAL_CONFIRM_MIN,
"scrambled-source attribution {scrambled:.3} should fail the gate (it must not look causal)"
);
// The true source must explain far more than an unrelated lane.
assert!(
gate.confirmed_fraction > scrambled + 0.3,
"gate does not attribute to the specific source: true={:.3} scrambled={:.3}",
gate.confirmed_fraction,
scrambled
);
}
/// Finding 5: mutants are killed by the SAME acceptance-gate predicates the
/// real run decides with — not a separate mini-evaluator. The reference must
/// pass every per-config predicate; every mutant must be rejected by the
/// real predicate it targets.
#[test]
fn mutants_killed_by_real_acceptance_gates() {
use rune_ir::{RuneProgram, RuneToken, ALL_OPS};
use world_model::{standard_executors, ProgramId, Rng, WorldId, WorldSnapshot};
fn rich_input(seed: u64) -> ResolutionInput {
let mut rng = Rng::new(seed);
let mut w = WorldSnapshot::blank(WorldId(seed), seed);
for d in &mut w.domains {
for l in 0..LANES {
d.observed[l] = rng.range_i64(-5000, 5000);
}
for l in 0..HIDDEN_LANES {
d.hidden[l] = rng.range_i64(-5000, 5000);
}
}
for j in 0..NUM_DOMAINS {
for i in 0..NUM_DOMAINS {
w.causal_state.coupling[j][i] = rng.range_i64(-17, 17);
}
}
let tokens: Vec<RuneToken> = (0..40)
.map(|i| RuneToken {
op: ALL_OPS[i % ALL_OPS.len()],
a: ((i * 3) % NUM_DOMAINS) as u8,
b: ((i * 5 + 1) % NUM_DOMAINS) as u8,
c: rng.next_u64() as u8,
imm: rng.range_i64(-100000, 100000),
})
.collect();
ResolutionInput {
world: w,
program: RuneProgram { id: ProgramId(seed), tokens, seed },
contexts: standard_executors(seed, 4),
contract_seed: seed,
perturbation_seed: seed,
}
}
let inputs: Vec<ResolutionInput> = (0..16).map(|s| rich_input(s + 1)).collect();
// Reference passes every per-config acceptance predicate.
let refcfg = EngineConfig::reference();
let rc: Vec<Canonical> = inputs.iter().map(|i| canonical(&execute(&refcfg, i))).collect();
let rf: Vec<Hash> = inputs.iter().map(|i| execute(&refcfg, i).replay.future_hash).collect();
assert!(!config_causal_fails(&refcfg, &inputs));
assert!(!config_domain_fails(&refcfg, &inputs));
assert!(!config_temporal_fails(&refcfg, &inputs, &rf));
assert!(!config_equivalence_fails(&refcfg, &inputs, &rc));
// Every mutant is rejected by the real acceptance gate it targets.
let outcome = evaluate_mutants(520, &inputs);
assert!(outcome.passed(), "survivors: {:?}", outcome.survivors);
assert_eq!(outcome.killed, outcome.total);
}
#[test]
fn merkle_root_binds_to_leaves() {
let a = merkle_root(&[Hash(1), Hash(2), Hash(3)]);
+62 -2
View File
@@ -29,6 +29,38 @@ fn write_report(dir: &Path, name: &str, j: &Json) {
f.write_all(j.to_pretty().as_bytes()).expect("write report");
}
/// Write the raw evidence the independent `attest` binary verifies (findings
/// 2, 3): every Merkle leaf, plus the producer's claims. The attestor recomputes
/// the root from these leaves and checks it against the claimed root, in a
/// separate process that never reads the compliance report.
fn write_evidence(dir: &Path, r: &CiResults) {
let ev = dir.join("evidence");
fs::create_dir_all(&ev).expect("create evidence dir");
let mut leaves = String::from("leaf\n");
for h in &r.merkle_leaves {
leaves.push_str(&format!("{:016x}\n", h.0));
}
fs::write(ev.join("leaves.tsv"), leaves).expect("write leaves");
let claims = format!(
"# evidence claims for independent attestation\n\
root\t{:016x}\n\
leaf_count\t{}\n\
total_comparisons\t{}\n\
reference_engine_id\t{:016x}\n\
rut_engine_id\t{:016x}\n\
engines_agree\t{}\n",
r.provenance.execution_merkle_root.0,
r.provenance.merkle_leaf_count,
r.provenance.total_comparisons,
r.provenance.reference_engine_id.0,
r.provenance.rut_engine_id.0,
r.provenance.engines_agree,
);
fs::write(ev.join("claims.tsv"), claims).expect("write claims");
}
fn build_reports(dir: &Path, r: &CiResults) {
// 1. domain_participation_report
write_report(
@@ -111,11 +143,27 @@ fn build_reports(dir: &Path, r: &CiResults) {
("altered_trace".into(), Json::Num(r.metamorphic.altered_trace)),
("altered_delta".into(), Json::Num(r.metamorphic.altered_delta)),
("altered_future".into(), Json::Num(r.metamorphic.altered_future)),
("neutral_unexplained".into(), Json::Num(r.metamorphic.neutral_unexplained)),
("consumed_perturbation_trace_violations".into(), Json::Num(r.metamorphic.expectation_violations)),
("legitimately_neutral".into(), Json::Num(r.metamorphic.explained_neutral)),
("consumed_perturbations".into(), Json::Int(r.metamorphic.consumed as i64)),
("failures".into(), fails(&r.metamorphic.failures)),
]),
);
// 4b. causal_explanation_report (finding 10: intervention-confirmed edges)
write_report(
dir,
"causal_explanation_report",
&Json::Obj(vec![
("pass".into(), pass_field(&r.causal_explanation.failures)),
("edges_tested".into(), Json::Int(r.causal_explanation.edges_tested as i64)),
("edges_confirmed".into(), Json::Int(r.causal_explanation.edges_confirmed as i64)),
("confirmed_fraction".into(), Json::Num(r.causal_explanation.confirmed_fraction)),
("method".into(), Json::s("ablate recorded causal source lane; require destination delta to change")),
("failures".into(), fails(&r.causal_explanation.failures)),
]),
);
// 5. mutation_survivor_report
let survivors: Vec<Json> = r
.mutation
@@ -166,6 +214,9 @@ fn build_reports(dir: &Path, r: &CiResults) {
("total".into(), Json::Int(r.replay.total as i64)),
("deterministic".into(), Json::Int(r.replay.deterministic as i64)),
("drift".into(), Json::Int(r.replay.drift as i64)),
("retained_failures_present".into(), Json::Bool(r.replay.retained_present)),
("retained_failures_total".into(), Json::Int(r.replay.retained_total as i64)),
("retained_failures_regressions".into(), Json::Int(r.replay.retained_regressions as i64)),
("failures".into(), fails(&r.replay.failures)),
]),
);
@@ -226,9 +277,10 @@ fn build_reports(dir: &Path, r: &CiResults) {
/// The reports the spec requires every CI run to produce. A missing or empty
/// artifact is itself an acceptance failure (compliance rule 4).
const REQUIRED_REPORTS: [&str; 9] = [
const REQUIRED_REPORTS: [&str; 10] = [
"domain_participation_report",
"causal_rank_report",
"causal_explanation_report",
"compression_resistance_report",
"metamorphic_response_report",
"mutation_survivor_report",
@@ -338,6 +390,13 @@ fn obligations(r: &CiResults) -> Vec<Obligation> {
actual: 0,
gate_pass: r.metamorphic.failures.is_empty(),
},
Obligation {
requirement: "recorded causal edges are intervention-confirmed (not counted)",
artifact: "causal_explanation_report",
floor: 0,
actual: f(r.causal_explanation.edges_confirmed),
gate_pass: r.causal_explanation.failures.is_empty(),
},
Obligation {
requirement: "every admitted case satisfies its contract",
artifact: "coverage_report",
@@ -555,6 +614,7 @@ fn main() {
let elapsed = start.elapsed();
build_reports(dir, &results);
write_evidence(dir, &results);
write_markdown(dir, &results);
let compliance_ok = build_compliance_report(dir, &results);
+5
View File
@@ -42,6 +42,10 @@ pub struct PerturbedCase {
pub axis_name: String,
pub world: WorldSnapshot,
pub expectation: TraceDifferenceExpectation,
/// The domain this axis perturbs. The metamorphic gate uses this to enforce
/// the sound relation "a perturbation the program *consumes* must alter the
/// trace" rather than merely "some hash changed".
pub target_domain: usize,
}
/// A complete generated case (per spec).
@@ -156,6 +160,7 @@ pub fn generate_perturbations(world: &WorldSnapshot, seed: u64, count: usize) ->
axis_name: axis.name(),
world: axis.apply(world),
expectation: axis.expected_trace_difference(),
target_domain: axis.target().0 as usize,
});
}
out
+5
View File
@@ -10,6 +10,11 @@ rune_ir = { path = "../rune_ir" }
trace_model = { path = "../trace_model" }
generators = { path = "../generators" }
reference_runtime = { path = "../reference_runtime" }
runtime_under_test = { path = "../runtime_under_test" }
[dev-dependencies]
# Enables `buggy_resolve` for the retention negative-control test.
runtime_under_test = { path = "../runtime_under_test", features = ["negative_controls"] }
[lib]
path = "src/lib.rs"
@@ -0,0 +1,7 @@
# magicka-retained-failures v1
seed gate note
0000000000000001 runtime_equivalence curated regression guard: independent-runtime equivalence on a causal-edge-bearing case (catches the dropped-edge bug class)
0000000000000007 runtime_equivalence curated regression guard: fault-heavy case (saturation/empty-accumulator paths)
000000000000002a runtime_equivalence curated regression guard: temporal/future-dependence case
00000000000000ff runtime_equivalence curated regression guard: high-coupling case
0000000000000539 runtime_equivalence curated regression guard: branch-divergence case
1 # magicka-retained-failures v1
2 seed gate note
3 0000000000000001 runtime_equivalence curated regression guard: independent-runtime equivalence on a causal-edge-bearing case (catches the dropped-edge bug class)
4 0000000000000007 runtime_equivalence curated regression guard: fault-heavy case (saturation/empty-accumulator paths)
5 000000000000002a runtime_equivalence curated regression guard: temporal/future-dependence case
6 00000000000000ff runtime_equivalence curated regression guard: high-coupling case
7 0000000000000539 runtime_equivalence curated regression guard: branch-divergence case
+3 -1
View File
@@ -15,6 +15,8 @@ use reference_runtime::{execute, EngineConfig, ResolutionInput};
use std::path::PathBuf;
use world_model::Hash;
pub mod retention;
/// Format version of the persisted corpus file. Bump only with a deliberate,
/// reviewed migration of the committed corpus.
pub const CORPUS_VERSION: u32 = 1;
@@ -33,7 +35,7 @@ pub struct ReplayCase {
pub expected_future_hash: Hash,
}
fn input_for(master_seed: u64) -> (ResolutionInput, u64, u64, u64, u64) {
pub(crate) fn input_for(master_seed: u64) -> (ResolutionInput, u64, u64, u64, u64) {
let (case, _accepted_seed) = generate_accepted_case(master_seed);
let input = ResolutionInput {
world: case.world.clone(),
+162
View File
@@ -0,0 +1,162 @@
//! Failure retention (finding 6). A static seed corpus proves the engine is
//! stable on a *fixed* sample; it does not retain *discovered* counterexamples.
//! This module is the regression memory: every counterexample CI ever finds
//! (e.g. a reference/runtime divergence) is curated into a committed,
//! append-only file and **re-verified on every run**, so a fixed bug can never
//! silently reappear.
//!
//! Two halves, both real:
//! * The committed `corpus/retained_failures.tsv` is loaded and each case is
//! re-executed under the reference and the independent runtime-under-test; any
//! case where they disagree is a *regression* and fails CI.
//! * When a run discovers a NEW divergence, it is serialized to the run's output
//! so it must be triaged and added to the committed set (the run also fails).
//! Discovered failures are therefore never lost.
use crate::input_for;
use reference_runtime::{canonical, execute, EngineConfig, ResolutionInput, ResolutionResult};
use runtime_under_test::native_resolve;
use std::path::PathBuf;
/// A retained counterexample: the seed needed to regenerate it, the gate it
/// originally tripped, and a human note.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct RetainedFailure {
pub master_seed: u64,
pub gate: String,
pub note: String,
}
/// Path to the committed retained-failures file.
pub fn retained_path() -> PathBuf {
PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("corpus/retained_failures.tsv")
}
/// Serialize a retained set (with a provenance header).
pub fn serialize(failures: &[RetainedFailure]) -> String {
let mut s = String::from("# magicka-retained-failures v1\n");
s.push_str("seed\tgate\tnote\n");
for f in failures {
// Tabs/newlines are stripped from free text to keep the TSV well-formed.
let gate = f.gate.replace(['\t', '\n'], " ");
let note = f.note.replace(['\t', '\n'], " ");
s.push_str(&format!("{:016x}\t{}\t{}\n", f.master_seed, gate, note));
}
s
}
/// Parse a retained set.
pub fn parse(text: &str) -> Vec<RetainedFailure> {
let mut out = Vec::new();
for line in text.lines() {
if line.starts_with('#') || line.starts_with("seed") || line.trim().is_empty() {
continue;
}
let f: Vec<&str> = line.splitn(3, '\t').collect();
if f.len() < 1 {
continue;
}
if let Ok(seed) = u64::from_str_radix(f[0].trim(), 16) {
out.push(RetainedFailure {
master_seed: seed,
gate: f.get(1).unwrap_or(&"").to_string(),
note: f.get(2).unwrap_or(&"").to_string(),
});
}
}
out
}
/// Load the committed retained set. Missing file => empty set + `present=false`.
pub fn load() -> (Vec<RetainedFailure>, bool) {
match std::fs::read_to_string(retained_path()) {
Ok(t) => (parse(&t), true),
Err(_) => (Vec::new(), false),
}
}
/// Append a newly-discovered failure to the committed set (append-only).
pub fn append(failure: &RetainedFailure) -> std::io::Result<()> {
let (mut set, _present) = load();
if !set.iter().any(|f| f.master_seed == failure.master_seed) {
set.push(failure.clone());
}
let path = retained_path();
if let Some(parent) = path.parent() {
std::fs::create_dir_all(parent)?;
}
std::fs::write(&path, serialize(&set))
}
/// Does a retained case still agree between the reference and `resolve`? A
/// retained counterexample is "fixed" iff the two implementations now produce
/// identical canonical views on it.
pub fn agrees(
failure: &RetainedFailure,
resolve: impl Fn(&ResolutionInput) -> ResolutionResult,
) -> bool {
let (input, ..) = input_for(failure.master_seed);
canonical(&execute(&EngineConfig::reference(), &input)) == canonical(&resolve(&input))
}
/// Result of verifying the retained set.
#[derive(Clone, Debug)]
pub struct RetentionReport {
pub present: bool,
pub total: usize,
/// Seeds that regressed (reference and runtime-under-test disagree again).
pub regressions: Vec<u64>,
}
impl RetentionReport {
pub fn ok(&self) -> bool {
self.present && self.regressions.is_empty()
}
}
/// Verify the committed retained set against the independent runtime-under-test.
pub fn verify() -> RetentionReport {
let (set, present) = load();
let regressions = set
.iter()
.filter(|f| !agrees(f, |inp| native_resolve(inp)))
.map(|f| f.master_seed)
.collect();
RetentionReport { present, total: set.len(), regressions }
}
#[cfg(test)]
mod tests {
use super::*;
use runtime_under_test::buggy_resolve;
#[test]
fn serialize_roundtrips() {
let set = vec![
RetainedFailure { master_seed: 0xABC, gate: "runtime_equivalence".into(), note: "dropped edge".into() },
RetainedFailure { master_seed: 0x1, gate: "replay".into(), note: "drift".into() },
];
assert_eq!(parse(&serialize(&set)), set);
}
#[test]
fn committed_retained_set_exists_and_holds() {
// The committed file must be present (the retention mechanism is wired),
// and every retained counterexample must still be fixed.
let report = verify();
assert!(report.present, "committed retained_failures.tsv is missing");
assert!(report.regressions.is_empty(), "regressions: {:?}", report.regressions);
}
/// A retained counterexample re-checked against a *buggy* runtime must be
/// flagged as a regression. Proves the retention check is not vacuous: if a
/// fixed bug reappears, retention catches it.
#[test]
fn reintroduced_bug_is_caught_by_retention() {
let f = RetainedFailure { master_seed: 42, gate: "runtime_equivalence".into(), note: "synthetic".into() };
// Against the real runtime the case agrees (the bug is fixed)...
assert!(agrees(&f, |inp| native_resolve(inp)));
// ...but a runtime that reintroduces the bug is caught as a regression.
assert!(!agrees(&f, |inp| buggy_resolve(inp)));
}
}