Compare commits
6
Commits
93c78d9c76
...
main
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
c37c9dab0d | ||
|
|
a90e27ab63 | ||
|
|
f4c75fc8cf | ||
|
|
11162ae448 | ||
|
|
bea076df43 | ||
|
|
1e50c80627 |
@@ -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" }
|
||||
]
|
||||
}
|
||||
@@ -67,12 +67,23 @@ 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
|
||||
for e in leaves.tsv traces.tsv causal_evidence.tsv collapse_feature_rows.tsv MANIFEST.tsv claims.tsv; do
|
||||
test -s "ci_out/evidence/${e}" || { echo "MISSING EVIDENCE: ${e}"; exit 1; }
|
||||
done
|
||||
|
||||
# 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()
|
||||
|
||||
@@ -11,6 +11,7 @@ members = [
|
||||
"crates/semantic_mutation",
|
||||
"crates/replay_corpus",
|
||||
"crates/ci_reports",
|
||||
"crates/attestation",
|
||||
"crates/protocol",
|
||||
"crates/game_runtime",
|
||||
"crates/web_assets",
|
||||
|
||||
@@ -0,0 +1,22 @@
|
||||
[package]
|
||||
name = "attestation"
|
||||
version.workspace = true
|
||||
edition.workspace = true
|
||||
license.workspace = true
|
||||
|
||||
[[bin]]
|
||||
name = "attest"
|
||||
path = "src/main.rs"
|
||||
|
||||
[dependencies]
|
||||
# NOT ci_reports. The root, the full-trace hashes, and the leaves are recomputed
|
||||
# by this crate's own code path — an independent check, not a re-export of the
|
||||
# producer's claim. trace_model/world_model provide the shared trace/delta types
|
||||
# and hashing the verifier reconstructs from raw evidence.
|
||||
world_model = { path = "../world_model" }
|
||||
trace_model = { path = "../trace_model" }
|
||||
# For independent RE-EXECUTION of retained per-edge causal interventions.
|
||||
generators = { path = "../generators" }
|
||||
reference_runtime = { path = "../reference_runtime" }
|
||||
# For recomputing collapse feature rows from full traces (proving derivation).
|
||||
collapse_analysis = { path = "../collapse_analysis" }
|
||||
@@ -0,0 +1,596 @@
|
||||
//! `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 generators::generate_accepted_case;
|
||||
use reference_runtime::{execute, EngineConfig, ResolutionInput};
|
||||
use std::collections::HashSet;
|
||||
use std::path::Path;
|
||||
use trace_model::{ExecutionTrace, ReplayRecord};
|
||||
use world_model::{Hash, Hasher, WorldDelta, HIDDEN_LANES, LANES, NUM_DOMAINS};
|
||||
|
||||
/// Re-execute one retained causal record from its seed and recompute the
|
||||
/// destination delta before and after perturbing the recorded source lane.
|
||||
/// Returns `(base_dv, alt_dv)`; the caller compares against the retained values.
|
||||
pub fn recompute_causal_record(
|
||||
seed: u64,
|
||||
from_domain: usize,
|
||||
from_lane: usize,
|
||||
from_hidden: bool,
|
||||
to_domain: usize,
|
||||
to_lane: usize,
|
||||
to_hidden: bool,
|
||||
) -> (i64, i64) {
|
||||
let (case, _) = generate_accepted_case(seed);
|
||||
let cfg = EngineConfig::reference();
|
||||
let input = ResolutionInput {
|
||||
world: case.world.clone(),
|
||||
program: case.program.clone(),
|
||||
contexts: case.contexts.clone(),
|
||||
contract_seed: case.contract_seed,
|
||||
perturbation_seed: case.perturbation_seed,
|
||||
};
|
||||
let base = execute(&cfg, &input);
|
||||
let mut w = input.world.clone();
|
||||
let fd = from_domain % NUM_DOMAINS;
|
||||
if from_hidden {
|
||||
let l = from_lane % HIDDEN_LANES;
|
||||
w.domains[fd].hidden[l] = w.domains[fd].hidden[l].wrapping_add(0x9_27c1);
|
||||
} else {
|
||||
let l = from_lane % LANES;
|
||||
w.domains[fd].observed[l] = w.domains[fd].observed[l].wrapping_add(0x9_27c1);
|
||||
}
|
||||
let mut alt_input = input.clone();
|
||||
alt_input.world = w;
|
||||
let alt = execute(&cfg, &alt_input);
|
||||
let dd = to_domain % NUM_DOMAINS;
|
||||
let read = |d: &world_model::DomainDelta| -> i64 {
|
||||
if to_hidden {
|
||||
d.hidden[to_lane % HIDDEN_LANES]
|
||||
} else {
|
||||
d.observed[to_lane % LANES]
|
||||
}
|
||||
};
|
||||
(read(&base.delta.domain_deltas[dd]), read(&alt.delta.domain_deltas[dd]))
|
||||
}
|
||||
|
||||
/// 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())
|
||||
}
|
||||
|
||||
/// Reconstruct the leaf of one full-trace evidence record from its raw trace +
|
||||
/// delta + seeds, independently of any reported digest. Returns the recomputed
|
||||
/// leaf, or `None` if the record is malformed.
|
||||
///
|
||||
/// `line` is `kind ws ps cs prs future leaf <TAB> <trace> <TAB> <delta>` where
|
||||
/// `kind` is `b` (base) or `p` (perturbation). Returns `(recomputed_leaf,
|
||||
/// claimed_leaf, is_base)`.
|
||||
pub fn recompute_trace_leaf(line: &str) -> Option<(u64, u64, bool)> {
|
||||
let mut parts = line.splitn(3, '\t');
|
||||
let header = parts.next()?;
|
||||
let trace_s = parts.next()?;
|
||||
let delta_s = parts.next()?;
|
||||
let mut h = header.split_whitespace();
|
||||
let kind = h.next()?;
|
||||
let is_base = kind == "b";
|
||||
let hx = |s: Option<&str>| -> Option<u64> { u64::from_str_radix(s?.trim(), 16).ok() };
|
||||
let world_seed = hx(h.next())?;
|
||||
let program_seed = hx(h.next())?;
|
||||
let contract_seed = hx(h.next())?;
|
||||
let perturbation_seed = hx(h.next())?;
|
||||
let future = hx(h.next())?;
|
||||
let claimed_leaf = hx(h.next())?;
|
||||
|
||||
let trace = ExecutionTrace::deserialize(trace_s)?;
|
||||
let delta = WorldDelta::deserialize(delta_s)?;
|
||||
// Recompute the canonical trace hash and delta hash from the FULL structure.
|
||||
let rr = ReplayRecord {
|
||||
world_seed,
|
||||
program_seed,
|
||||
contract_seed,
|
||||
perturbation_seed,
|
||||
trace_hash: trace.canonical_hash(),
|
||||
delta_hash: delta.hash(),
|
||||
future_hash: Hash(future),
|
||||
};
|
||||
Some((rr.hash().0, claimed_leaf, is_base))
|
||||
}
|
||||
|
||||
/// 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 traces_verified: usize,
|
||||
pub traces_total: usize,
|
||||
pub causal_total: usize,
|
||||
pub causal_recomputed: usize,
|
||||
pub causal_confirmed: usize,
|
||||
pub collapse_total: usize,
|
||||
pub collapse_derived: usize,
|
||||
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));
|
||||
|
||||
// Full-trace evidence (finding 4): reconstruct each sampled trace + delta,
|
||||
// recompute its leaf independently, and confirm it both matches the record's
|
||||
// claimed leaf AND is one of the retained leaves the root is built from.
|
||||
let leaf_set: HashSet<u64> = leaves.iter().copied().collect();
|
||||
let traces_path = dir.join("evidence/traces.tsv");
|
||||
let traces_txt = std::fs::read_to_string(&traces_path)
|
||||
.map_err(|e| format!("cannot read {}: {e}", traces_path.display()))?;
|
||||
let mut traces_total = 0usize;
|
||||
let mut traces_verified = 0usize;
|
||||
let mut covered: HashSet<u64> = HashSet::new();
|
||||
for line in traces_txt.lines() {
|
||||
if line.starts_with('#') || line.trim().is_empty() {
|
||||
continue;
|
||||
}
|
||||
traces_total += 1;
|
||||
if let Some((recomputed_leaf, claimed_leaf, _is_base)) = recompute_trace_leaf(line) {
|
||||
if recomputed_leaf == claimed_leaf && leaf_set.contains(&recomputed_leaf) {
|
||||
traces_verified += 1;
|
||||
covered.insert(recomputed_leaf);
|
||||
}
|
||||
}
|
||||
}
|
||||
let traces_present = traces_total > 0;
|
||||
checks.push(("full-trace evidence present".into(), traces_present));
|
||||
checks.push((
|
||||
"every full trace recomputes to a retained leaf".into(),
|
||||
traces_present && traces_verified == traces_total,
|
||||
));
|
||||
// Completeness (finding 3): every retained leaf must be covered by a full
|
||||
// trace record, and there must be exactly one record per leaf — a bijection,
|
||||
// not just a consistent count.
|
||||
checks.push((
|
||||
"every leaf has full retained evidence (bijection)".into(),
|
||||
traces_present
|
||||
&& traces_total == leaves.len()
|
||||
&& covered.len() == leaf_set.len(),
|
||||
));
|
||||
|
||||
// Causal intervention evidence (finding 7): RE-EXECUTE each retained record
|
||||
// from its seed and confirm the retained base_dv/alt_dv reproduce, then
|
||||
// require the confirmed fraction to clear the threshold.
|
||||
let causal_path = dir.join("evidence/causal_evidence.tsv");
|
||||
let causal_txt = std::fs::read_to_string(&causal_path)
|
||||
.map_err(|e| format!("cannot read {}: {e}", causal_path.display()))?;
|
||||
let mut causal_total = 0usize;
|
||||
let mut causal_recomputed = 0usize;
|
||||
let mut causal_confirmed = 0usize;
|
||||
for line in causal_txt.lines() {
|
||||
if line.starts_with("seed") || line.starts_with('#') || line.trim().is_empty() {
|
||||
continue;
|
||||
}
|
||||
let f: Vec<&str> = line.split('\t').collect();
|
||||
if f.len() < 9 {
|
||||
continue;
|
||||
}
|
||||
let seed = match u64::from_str_radix(f[0].trim(), 16) {
|
||||
Ok(v) => v,
|
||||
Err(_) => continue,
|
||||
};
|
||||
let p = |i: usize| f[i].trim().parse::<i64>().ok();
|
||||
let (Some(fd), Some(fl), Some(fh), Some(td), Some(tl), Some(th), Some(bdv), Some(adv)) =
|
||||
(p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8))
|
||||
else {
|
||||
continue;
|
||||
};
|
||||
causal_total += 1;
|
||||
let (rb, ra) = recompute_causal_record(
|
||||
seed, fd as usize, fl as usize, fh != 0, td as usize, tl as usize, th != 0,
|
||||
);
|
||||
if rb == bdv && ra == adv {
|
||||
causal_recomputed += 1;
|
||||
}
|
||||
if rb != ra {
|
||||
causal_confirmed += 1;
|
||||
}
|
||||
}
|
||||
// Collapse derivation (finding 4): recompute each collapse feature row from
|
||||
// the corresponding retained FULL trace + delta and require bit-exact match,
|
||||
// proving the summary the collapse gate consumed derives from the full trace.
|
||||
let crows_path = dir.join("evidence/collapse_feature_rows.tsv");
|
||||
let crows_txt = std::fs::read_to_string(&crows_path)
|
||||
.map_err(|e| format!("cannot read {}: {e}", crows_path.display()))?;
|
||||
let claimed_rows: Vec<Vec<u64>> = crows_txt
|
||||
.lines()
|
||||
.filter(|l| !l.trim().is_empty())
|
||||
.map(|l| l.split_whitespace().filter_map(|t| t.parse::<u64>().ok()).collect())
|
||||
.collect();
|
||||
// Re-read the trace records in order to recompute their feature rows.
|
||||
let mut collapse_total = 0usize;
|
||||
let mut collapse_derived = 0usize;
|
||||
{
|
||||
let mut idx = 0usize;
|
||||
for line in traces_txt.lines() {
|
||||
// Collapse rows correspond to BASE executions in order.
|
||||
if !line.starts_with("b ") {
|
||||
continue;
|
||||
}
|
||||
if idx >= claimed_rows.len() {
|
||||
break;
|
||||
}
|
||||
let mut parts = line.splitn(3, '\t');
|
||||
let _hdr = parts.next();
|
||||
let trace_s = parts.next();
|
||||
let delta_s = parts.next();
|
||||
if let (Some(ts), Some(ds)) = (trace_s, delta_s) {
|
||||
if let (Some(trace), Some(delta)) =
|
||||
(ExecutionTrace::deserialize(ts), WorldDelta::deserialize(ds))
|
||||
{
|
||||
let recomputed = collapse_analysis::trace_feature_row(&trace, &delta);
|
||||
let recomputed_bits: Vec<u64> = recomputed.iter().map(|v| v.to_bits()).collect();
|
||||
collapse_total += 1;
|
||||
if recomputed_bits == claimed_rows[idx] {
|
||||
collapse_derived += 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
idx += 1;
|
||||
}
|
||||
}
|
||||
let collapse_present = collapse_total > 0;
|
||||
checks.push(("collapse feature rows present".into(), collapse_present));
|
||||
checks.push((
|
||||
"every collapse summary derives from a full trace".into(),
|
||||
collapse_present && collapse_derived == collapse_total,
|
||||
));
|
||||
|
||||
let causal_present = causal_total > 0;
|
||||
let causal_frac = if causal_total > 0 { causal_confirmed as f64 / causal_total as f64 } else { 0.0 };
|
||||
checks.push(("causal evidence present".into(), causal_present));
|
||||
checks.push((
|
||||
"every causal record recomputes (base_dv/alt_dv reproduce)".into(),
|
||||
causal_present && causal_recomputed == causal_total,
|
||||
));
|
||||
checks.push((
|
||||
"recomputed causal confirmation >= 0.50".into(),
|
||||
causal_present && causal_frac >= 0.50,
|
||||
));
|
||||
|
||||
// Artifact bundle (finding 1): the merge-scale claim requires a complete,
|
||||
// content-hashed bundle. Verify the manifest lists the required files and
|
||||
// each file's recomputed hash + length match.
|
||||
let manifest_path = dir.join("evidence/MANIFEST.tsv");
|
||||
let manifest_txt = std::fs::read_to_string(&manifest_path)
|
||||
.map_err(|e| format!("cannot read {}: {e}", manifest_path.display()))?;
|
||||
let required = [
|
||||
"leaves.tsv",
|
||||
"claims.tsv",
|
||||
"causal_evidence.tsv",
|
||||
"collapse_feature_rows.tsv",
|
||||
"traces.tsv",
|
||||
];
|
||||
let mut listed: HashSet<String> = HashSet::new();
|
||||
let mut bundle_intact = true;
|
||||
for line in manifest_txt.lines() {
|
||||
if line.starts_with("file") || line.trim().is_empty() {
|
||||
continue;
|
||||
}
|
||||
let f: Vec<&str> = line.split('\t').collect();
|
||||
if f.len() < 3 {
|
||||
bundle_intact = false;
|
||||
continue;
|
||||
}
|
||||
let name = f[0].trim();
|
||||
let claimed_hash = u64::from_str_radix(f[1].trim(), 16).ok();
|
||||
let claimed_len = f[2].trim().parse::<usize>().ok();
|
||||
let bytes = std::fs::read(dir.join("evidence").join(name)).unwrap_or_default();
|
||||
let mut h = Hasher::new();
|
||||
h.write_tag("evidence-file");
|
||||
h.write_bytes(&bytes);
|
||||
if claimed_hash != Some(h.finish().0) || claimed_len != Some(bytes.len()) {
|
||||
bundle_intact = false;
|
||||
}
|
||||
listed.insert(name.to_string());
|
||||
}
|
||||
let bundle_complete = required.iter().all(|r| listed.contains(*r));
|
||||
checks.push(("artifact bundle manifest complete".into(), bundle_complete));
|
||||
checks.push(("artifact bundle files intact (hash + length)".into(), bundle_intact && bundle_complete));
|
||||
|
||||
let ok = checks.iter().all(|(_, b)| *b);
|
||||
Ok(Attestation {
|
||||
ok,
|
||||
leaf_count: leaves.len(),
|
||||
recomputed_root: recomputed,
|
||||
claimed_root,
|
||||
traces_verified,
|
||||
traces_total,
|
||||
causal_total,
|
||||
causal_recomputed,
|
||||
causal_confirmed,
|
||||
collapse_total,
|
||||
collapse_derived,
|
||||
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);
|
||||
}
|
||||
|
||||
use trace_model::{
|
||||
BehaviorFingerprint, CausalEdge, CausalGraph, CausalNode, DivergenceGraph,
|
||||
DomainAccessGraph, ExecutionTrace, InformationFlowGraph, PerturbationResponse, ReplayRecord,
|
||||
TemporalGraph,
|
||||
};
|
||||
use world_model::{DomainDelta, DomainId, Hash, WorldDelta, HIDDEN_LANES, LANES};
|
||||
|
||||
fn sample_trace(seed: u64) -> ExecutionTrace {
|
||||
let mut read_graph = DomainAccessGraph::default();
|
||||
read_graph.access_count[(seed % 8) as usize] = 3;
|
||||
read_graph.edges.push((0, 2, (seed % 7) as u32 + 1));
|
||||
let mut write_graph = DomainAccessGraph::default();
|
||||
write_graph.access_count[2] = 4;
|
||||
let causal_graph = CausalGraph {
|
||||
edges: vec![CausalEdge {
|
||||
from: CausalNode { domain: 0, lane: 1, hidden: false, step: 2 },
|
||||
to: CausalNode { domain: 2, lane: 0, hidden: true, step: 2 },
|
||||
weight: seed as i64 - 100,
|
||||
}],
|
||||
};
|
||||
ExecutionTrace {
|
||||
read_graph,
|
||||
write_graph,
|
||||
causal_graph,
|
||||
information_flow: InformationFlowGraph { edges: vec![(0, 2, 9)] },
|
||||
executor_divergence: DivergenceGraph { executor_count: 2, pairwise: vec![0.0, 0.5, 0.5, 0.0] },
|
||||
temporal_graph: TemporalGraph { edges: vec![(1, 2, 3)] },
|
||||
perturbation_response: PerturbationResponse::default(),
|
||||
behavior_fingerprint: BehaviorFingerprint::from_features(vec![seed as i64, -2, 3]),
|
||||
}
|
||||
}
|
||||
|
||||
fn sample_delta(seed: u64) -> WorldDelta {
|
||||
let domain_deltas = (0..NUM_DOMAINS)
|
||||
.map(|d| {
|
||||
let mut observed = [0i64; LANES];
|
||||
observed[0] = seed as i64 + d as i64;
|
||||
DomainDelta { domain: DomainId(d as u8), observed, hidden: [0i64; HIDDEN_LANES] }
|
||||
})
|
||||
.collect();
|
||||
WorldDelta { domain_deltas, turn_advance: 0 }
|
||||
}
|
||||
|
||||
fn record(seed: u64) -> (ReplayRecord, ExecutionTrace, WorldDelta) {
|
||||
let trace = sample_trace(seed);
|
||||
let delta = sample_delta(seed);
|
||||
let rr = ReplayRecord {
|
||||
world_seed: seed,
|
||||
program_seed: seed ^ 1,
|
||||
contract_seed: seed ^ 2,
|
||||
perturbation_seed: seed ^ 3,
|
||||
trace_hash: trace.canonical_hash(),
|
||||
delta_hash: delta.hash(),
|
||||
future_hash: Hash(seed.wrapping_mul(0x9e3779b97f4a7c15)),
|
||||
};
|
||||
(rr, trace, delta)
|
||||
}
|
||||
|
||||
/// Write a full evidence dir from real records. If `tamper_trace` is set,
|
||||
/// that record's serialized trace is corrupted after its leaf was claimed.
|
||||
fn write_full_evidence(dir: &Path, seeds: &[u64], tamper_trace: Option<usize>) {
|
||||
let ev = dir.join("evidence");
|
||||
std::fs::create_dir_all(&ev).unwrap();
|
||||
let records: Vec<_> = seeds.iter().map(|&s| record(s)).collect();
|
||||
let leaves: Vec<u64> = records.iter().map(|(rr, _, _)| rr.hash().0).collect();
|
||||
|
||||
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",
|
||||
merkle_root(&leaves),
|
||||
leaves.len(),
|
||||
leaves.len()
|
||||
);
|
||||
std::fs::write(ev.join("claims.tsv"), claims).unwrap();
|
||||
|
||||
let mut traces = String::from("# trace evidence\n");
|
||||
for (i, (rr, trace, delta)) in records.iter().enumerate() {
|
||||
let mut trace_s = trace.serialize();
|
||||
if tamper_trace == Some(i) {
|
||||
// Corrupt the full trace without changing the claimed leaf.
|
||||
trace_s = trace_s.replacen("trace-v1 ", "trace-v1 999 ", 1);
|
||||
}
|
||||
traces.push_str(&format!(
|
||||
"b {:016x} {:016x} {:016x} {:016x} {:016x} {:016x}\t{}\t{}\n",
|
||||
rr.world_seed, rr.program_seed, rr.contract_seed, rr.perturbation_seed,
|
||||
rr.future_hash.0, rr.hash().0, trace_s, delta.serialize(),
|
||||
));
|
||||
}
|
||||
std::fs::write(ev.join("traces.tsv"), traces).unwrap();
|
||||
|
||||
// Real, recomputable causal evidence from actual reference executions.
|
||||
let mut causal = String::from(
|
||||
"seed\tfrom_domain\tfrom_lane\tfrom_hidden\tto_domain\tto_lane\tto_hidden\tbase_dv\talt_dv\n",
|
||||
);
|
||||
let cfg = EngineConfig::reference();
|
||||
for &cseed in &[0xC0FFEEu64, 0xBEEF, 0x1234, 0x5EED, 0xABCD] {
|
||||
let (case, _) = generate_accepted_case(cseed);
|
||||
let input = ResolutionInput {
|
||||
world: case.world.clone(),
|
||||
program: case.program.clone(),
|
||||
contexts: case.contexts.clone(),
|
||||
contract_seed: case.contract_seed,
|
||||
perturbation_seed: case.perturbation_seed,
|
||||
};
|
||||
let base = execute(&cfg, &input);
|
||||
let edges = base.trace.causal_graph.edges.clone();
|
||||
let stride = (edges.len() / 12).max(1);
|
||||
for e in edges.iter().step_by(stride).take(12) {
|
||||
let fd = e.from.domain as usize % NUM_DOMAINS;
|
||||
let fl = e.from.lane as usize;
|
||||
let fh = e.from.hidden;
|
||||
let td = e.to.domain as usize % NUM_DOMAINS;
|
||||
let tl = e.to.lane as usize;
|
||||
let th = e.to.hidden;
|
||||
let (b, a) = recompute_causal_record(cseed, fd, fl, fh, td, tl, th);
|
||||
causal.push_str(&format!(
|
||||
"{:016x}\t{}\t{}\t{}\t{}\t{}\t{}\t{}\t{}\n",
|
||||
cseed, fd, fl, fh as u8, td, tl, th as u8, b, a
|
||||
));
|
||||
}
|
||||
}
|
||||
std::fs::write(ev.join("causal_evidence.tsv"), causal).unwrap();
|
||||
|
||||
// Collapse feature rows derived from the same synthetic traces, in order.
|
||||
let mut crows = String::new();
|
||||
for (_, trace, delta) in &records {
|
||||
let row = collapse_analysis::trace_feature_row(trace, delta);
|
||||
let cells: Vec<String> = row.iter().map(|v| v.to_bits().to_string()).collect();
|
||||
crows.push_str(&cells.join(" "));
|
||||
crows.push('\n');
|
||||
}
|
||||
std::fs::write(ev.join("collapse_feature_rows.tsv"), crows).unwrap();
|
||||
|
||||
// Bundle manifest over the written files.
|
||||
let mut manifest = String::from("file\thash\tbytes\n");
|
||||
for name in ["leaves.tsv", "claims.tsv", "causal_evidence.tsv", "collapse_feature_rows.tsv", "traces.tsv"] {
|
||||
let bytes = std::fs::read(ev.join(name)).unwrap_or_default();
|
||||
let mut h = Hasher::new();
|
||||
h.write_tag("evidence-file");
|
||||
h.write_bytes(&bytes);
|
||||
manifest.push_str(&format!("{}\t{:016x}\t{}\n", name, h.finish().0, bytes.len()));
|
||||
}
|
||||
std::fs::write(ev.join("MANIFEST.tsv"), manifest).unwrap();
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn honest_evidence_attests() {
|
||||
let dir = std::env::temp_dir().join("magicka_attest_ok");
|
||||
write_full_evidence(&dir, &[10, 20, 30, 40, 50], None);
|
||||
let att = verify_dir(&dir).unwrap();
|
||||
assert!(att.ok, "honest evidence should attest: {:?}", att.checks);
|
||||
assert_eq!(att.traces_verified, att.traces_total);
|
||||
assert!(att.traces_total > 0);
|
||||
}
|
||||
|
||||
/// Negative control: a tampered leaf changes the recomputed root, so the
|
||||
/// claimed root no longer matches and attestation FAILS.
|
||||
#[test]
|
||||
fn tampered_leaf_breaks_attestation() {
|
||||
let dir = std::env::temp_dir().join("magicka_attest_bad_leaf");
|
||||
write_full_evidence(&dir, &[10, 20, 30, 40, 50], None);
|
||||
// Flip a leaf in the file after the root was claimed.
|
||||
let lp = dir.join("evidence/leaves.tsv");
|
||||
let txt = std::fs::read_to_string(&lp).unwrap();
|
||||
let mut lines: Vec<String> = txt.lines().map(|s| s.to_string()).collect();
|
||||
lines[2] = format!("{:016x}", 0xdead_beefu64);
|
||||
std::fs::write(&lp, lines.join("\n")).unwrap();
|
||||
let att = verify_dir(&dir).unwrap();
|
||||
assert!(!att.ok, "tampered leaf must fail attestation");
|
||||
assert!(att.checks.iter().any(|(n, ok)| n.contains("root") && !ok));
|
||||
}
|
||||
|
||||
/// Negative control for finding 4: corrupting the FULL TRACE (without
|
||||
/// touching the claimed leaf) makes the recomputed leaf disagree, so the
|
||||
/// trace no longer attests. Proves the evidence is the full trace, not a
|
||||
/// trusted digest.
|
||||
#[test]
|
||||
fn tampered_trace_breaks_attestation() {
|
||||
let dir = std::env::temp_dir().join("magicka_attest_bad_trace");
|
||||
write_full_evidence(&dir, &[10, 20, 30, 40, 50], Some(2));
|
||||
let att = verify_dir(&dir).unwrap();
|
||||
assert!(!att.ok, "tampered full trace must fail attestation");
|
||||
assert!(att.traces_verified < att.traces_total);
|
||||
assert!(att.checks.iter().any(|(n, ok)| n.contains("full trace") && !ok));
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,48 @@
|
||||
//! `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>"),
|
||||
}
|
||||
eprintln!(
|
||||
" full traces verified: {}/{} (reconstructed + leaf re-derived)",
|
||||
att.traces_verified, att.traces_total
|
||||
);
|
||||
eprintln!(
|
||||
" causal records recomputed: {}/{} ({} confirmed)",
|
||||
att.causal_recomputed, att.causal_total, att.causal_confirmed
|
||||
);
|
||||
eprintln!(
|
||||
" collapse rows derived from full traces: {}/{}",
|
||||
att.collapse_derived, att.collapse_total
|
||||
);
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
+670
-70
@@ -22,9 +22,12 @@ 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, MutationOutcome};
|
||||
use std::collections::HashMap;
|
||||
use world_model::{Hash, Hasher, WorldSnapshot, NUM_DOMAINS};
|
||||
use std::io::Write;
|
||||
use world_model::{
|
||||
Hash, Hasher, TraceDifferenceExpectation, WorldSnapshot, HIDDEN_LANES, LANES, NUM_DOMAINS,
|
||||
};
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Run profile + scale, with an unbypassable merge floor.
|
||||
@@ -187,6 +190,159 @@ 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
|
||||
}
|
||||
|
||||
/// Number of generated cases each mutant is run through (a real corpus, not a
|
||||
/// fixed 64-input local sample).
|
||||
pub const MUTATION_GATE_CASES: usize = 128;
|
||||
|
||||
/// Run an engine config through the FULL set of engine-behavior acceptance gates
|
||||
/// over `n_cases` freshly generated cases (the same gate functions and corpus
|
||||
/// shape the acceptance run uses) and return the names of the gates it fails.
|
||||
/// The reference returns an empty vec; a broken engine returns the gates that
|
||||
/// catch it.
|
||||
pub fn engine_acceptance(cfg: &EngineConfig, n_cases: usize) -> Vec<String> {
|
||||
let refcfg = EngineConfig::reference();
|
||||
let mut edges = Vec::with_capacity(n_cases);
|
||||
let mut ranks = Vec::with_capacity(n_cases);
|
||||
let mut equiv_fail = false;
|
||||
let mut appears = [0u64; NUM_DOMAINS];
|
||||
let mut mutated = [0u64; NUM_DOMAINS];
|
||||
let mut influence_changed = [false; NUM_DOMAINS];
|
||||
let mut consumed = 0usize;
|
||||
let mut consumed_trace_violation = 0usize;
|
||||
let mut consumed_delta = 0usize;
|
||||
let mut consumed_future = 0usize;
|
||||
let n = n_cases.max(1) as f64;
|
||||
|
||||
for i in 0..n_cases {
|
||||
let (case, _) = generate_accepted_case(case_seed(i));
|
||||
let input = input_from_case(&case);
|
||||
let r = execute(cfg, &input);
|
||||
let rr = execute(&refcfg, &input);
|
||||
edges.push(r.trace.causal_edge_count() as f64);
|
||||
ranks.push(r.trace.causal_rank() as f64);
|
||||
if canonical(&r) != canonical(&rr) {
|
||||
equiv_fail = true;
|
||||
}
|
||||
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;
|
||||
}
|
||||
}
|
||||
// Per-domain measured influence: masking each domain in `cfg` must change
|
||||
// this config's own output.
|
||||
let base_h = (r.trace.canonical_hash(), r.delta.hash());
|
||||
for d in 0..NUM_DOMAINS {
|
||||
if influence_changed[d] {
|
||||
continue;
|
||||
}
|
||||
let mut mc = cfg.clone();
|
||||
mc.domain_mask[d] = false;
|
||||
let m = execute(&mc, &input);
|
||||
if (m.trace.canonical_hash(), m.delta.hash()) != base_h {
|
||||
influence_changed[d] = true;
|
||||
}
|
||||
}
|
||||
// Metamorphic over this case's perturbations.
|
||||
let bt = r.trace.canonical_hash();
|
||||
let bd = r.delta.hash();
|
||||
let bf = r.replay.future_hash;
|
||||
for pc in &case.perturbations {
|
||||
let pin = input_with_world(&case, pc.world.clone());
|
||||
let pr = execute(cfg, &pin);
|
||||
let read = r.trace.read_graph.access_count[pc.target_domain % NUM_DOMAINS] > 0;
|
||||
if read {
|
||||
consumed += 1;
|
||||
if pr.delta.hash() != bd {
|
||||
consumed_delta += 1;
|
||||
}
|
||||
if pr.replay.future_hash != bf {
|
||||
consumed_future += 1;
|
||||
}
|
||||
if pc.expectation.expect_trace_change
|
||||
&& pr.trace.canonical_hash() == bt
|
||||
&& pc.expectation.neutral_explanation.is_none()
|
||||
{
|
||||
consumed_trace_violation += 1;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
let mut fails = Vec::new();
|
||||
if causal_trace_fails(median(&edges), percentile(&ranks, 0.05)) {
|
||||
fails.push("causal_rank/trace".to_string());
|
||||
}
|
||||
if equiv_fail {
|
||||
fails.push("runtime_equivalence".to_string());
|
||||
}
|
||||
if (0..NUM_DOMAINS).any(|d| {
|
||||
(appears[d] as f64 / n) < DOMAIN_APPEARS_MIN
|
||||
|| (mutated[d] as f64 / n) < DOMAIN_MUTATED_MIN
|
||||
|| !influence_changed[d]
|
||||
}) {
|
||||
fails.push("domain_participation".to_string());
|
||||
}
|
||||
let mc = consumed.max(1) as f64;
|
||||
if consumed == 0
|
||||
|| (consumed_trace_violation as f64 / mc) > 0.01
|
||||
|| (consumed_delta as f64 / mc) < CONSUMED_DELTA_MIN
|
||||
|| (consumed_future as f64 / mc) < CONSUMED_FUTURE_MIN
|
||||
{
|
||||
fails.push("metamorphic_response".to_string());
|
||||
}
|
||||
let ce = causal_explanation_gate(cfg, n_cases, 4);
|
||||
if !ce.failures.is_empty() {
|
||||
fails.push("causal_explanation".to_string());
|
||||
}
|
||||
fails
|
||||
}
|
||||
|
||||
/// The mutation gate: every mutant must be rejected by the FULL engine-behavior
|
||||
/// acceptance gates over a real generated-case corpus (not 64 fixed inputs).
|
||||
pub fn evaluate_mutants(count: usize, _inputs: &[ResolutionInput]) -> MutationOutcome {
|
||||
let mutants = generate_mutants(count);
|
||||
let mut killed = 0;
|
||||
let mut survivors = Vec::new();
|
||||
for m in &mutants {
|
||||
let fails = engine_acceptance(&m.config, MUTATION_GATE_CASES);
|
||||
if fails.is_empty() {
|
||||
survivors.push((
|
||||
m.id,
|
||||
format!("mutant {} ({}) passed all acceptance gates", m.id, m.name),
|
||||
));
|
||||
} else {
|
||||
killed += 1;
|
||||
}
|
||||
}
|
||||
MutationOutcome { total: mutants.len(), killed, survivors }
|
||||
}
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Provenance: bind the reported numbers to executed work.
|
||||
// ---------------------------------------------------------------------------
|
||||
@@ -340,52 +496,62 @@ fn compressibility(features: &[i64]) -> f64 {
|
||||
(1.0 - h / 8.0).clamp(0.0, 1.0)
|
||||
}
|
||||
|
||||
/// Real serialized-trace feature row used by the collapse analysis. Layout per
|
||||
/// domain block (width 9): `[infl_out, infl_in, flow_out, flow_in, read, write,
|
||||
/// temporal, obs_delta, hid_delta]`, followed by globals `[causal_rank,
|
||||
/// edge_count, touched, divergence_mean]`. This is genuine trace structure, not
|
||||
/// a hash-derived proxy.
|
||||
/// Trace feature row used by the collapse analysis — the single definition lives
|
||||
/// in `collapse_analysis::trace_feature_row` so the attestor can recompute the
|
||||
/// same row from the retained full trace and prove the summary derives from it.
|
||||
fn trace_feature_row(r: &ResolutionResult) -> Vec<f64> {
|
||||
let infl = r.trace.causal_graph.influence_matrix();
|
||||
let mut flow = [[0.0f64; NUM_DOMAINS]; NUM_DOMAINS];
|
||||
for &(a, b, bits) in &r.trace.information_flow.edges {
|
||||
flow[a as usize % NUM_DOMAINS][b as usize % NUM_DOMAINS] += bits as f64;
|
||||
}
|
||||
let mut temporal = [0.0f64; NUM_DOMAINS];
|
||||
for &(_s, _off, d) in &r.trace.temporal_graph.edges {
|
||||
temporal[d as usize % NUM_DOMAINS] += 1.0;
|
||||
}
|
||||
|
||||
let mut row = Vec::with_capacity(FEATURE_W);
|
||||
for d in 0..NUM_DOMAINS {
|
||||
let infl_out: f64 = (0..NUM_DOMAINS).map(|j| infl[d][j]).sum();
|
||||
let infl_in: f64 = (0..NUM_DOMAINS).map(|i| infl[i][d]).sum();
|
||||
let flow_out: f64 = (0..NUM_DOMAINS).map(|j| flow[d][j]).sum();
|
||||
let flow_in: f64 = (0..NUM_DOMAINS).map(|i| flow[i][d]).sum();
|
||||
let read = r.trace.read_graph.access_count[d] as f64;
|
||||
let write = r.trace.write_graph.access_count[d] as f64;
|
||||
let temp = temporal[d];
|
||||
let obs_delta: f64 = r.delta.domain_deltas[d]
|
||||
.observed
|
||||
.iter()
|
||||
.map(|&v| (v as f64).abs())
|
||||
.sum();
|
||||
let hid_delta: f64 = r.delta.domain_deltas[d]
|
||||
.hidden
|
||||
.iter()
|
||||
.map(|&v| (v as f64).abs())
|
||||
.sum();
|
||||
row.extend_from_slice(&[
|
||||
infl_out, infl_in, flow_out, flow_in, read, write, temp, obs_delta, hid_delta,
|
||||
]);
|
||||
}
|
||||
row.push(r.trace.causal_rank() as f64);
|
||||
row.push(r.trace.causal_edge_count() as f64);
|
||||
row.push(r.trace.touched_domain_count() as f64);
|
||||
row.push(r.trace.context_divergence());
|
||||
row
|
||||
collapse_analysis::trace_feature_row(&r.trace, &r.delta)
|
||||
}
|
||||
|
||||
/// 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 if exp.neutral_explanation.is_some() {
|
||||
ExpectationOutcome::ExplainedNeutral
|
||||
} else {
|
||||
ExpectationOutcome::Violation
|
||||
}
|
||||
} else if trace_changed {
|
||||
ExpectationOutcome::Upheld
|
||||
} else {
|
||||
ExpectationOutcome::ExplainedNeutral
|
||||
}
|
||||
}
|
||||
|
||||
/// Consumed-perturbation aggregate thresholds for delta/future. Per-case strict
|
||||
/// enforcement of delta/future is unsound (clamping and masking legitimately
|
||||
/// leave them unchanged), so these are enforced as fractions over the consumed
|
||||
/// perturbations. Reference rates measured at ~0.77 (delta) and ~0.90 (future).
|
||||
pub const CONSUMED_DELTA_MIN: f64 = 0.65;
|
||||
pub const CONSUMED_FUTURE_MIN: f64 = 0.80;
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Result aggregates.
|
||||
// ---------------------------------------------------------------------------
|
||||
@@ -428,7 +594,16 @@ 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,
|
||||
/// Fraction of consumed perturbations that changed the delta / the future.
|
||||
pub consumed_delta_rate: f64,
|
||||
pub consumed_future_rate: f64,
|
||||
pub failures: Vec<String>,
|
||||
}
|
||||
|
||||
@@ -445,6 +620,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,13 +644,37 @@ 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>,
|
||||
/// A sample of FULL execution traces + deltas + seeds (finding 4). The
|
||||
/// attestor reconstructs each trace, recomputes its canonical hash and the
|
||||
/// replay-record leaf, and checks the leaf is in `merkle_leaves` — proving
|
||||
/// the leaves are backed by full trace structure, not a summary.
|
||||
pub trace_evidence: Vec<TraceEvidence>,
|
||||
/// The collapse feature rows, in the same order as the first base executions
|
||||
/// in the trace evidence, so the attestor can recompute each from the full
|
||||
/// trace and prove the summary derives from it (finding 4).
|
||||
pub collapse_feature_rows: Vec<Vec<f64>>,
|
||||
}
|
||||
|
||||
/// One sampled full-trace evidence record.
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct TraceEvidence {
|
||||
pub replay: trace_model::ReplayRecord,
|
||||
pub trace: trace_model::ExecutionTrace,
|
||||
pub delta: world_model::WorldDelta,
|
||||
}
|
||||
|
||||
/// How many full traces to retain as evidence.
|
||||
pub const TRACE_EVIDENCE_SAMPLE: usize = 256;
|
||||
|
||||
impl CiResults {
|
||||
pub fn all_failures(&self) -> Vec<(&'static str, &Vec<String>)> {
|
||||
vec![
|
||||
@@ -479,6 +682,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),
|
||||
@@ -497,6 +701,13 @@ impl CiResults {
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
pub fn run_all(scale: Scale) -> CiResults {
|
||||
run_all_to(scale, None)
|
||||
}
|
||||
|
||||
/// Like [`run_all`] but streams the FULL per-execution trace evidence (every
|
||||
/// base execution, not a sample) to `evidence_sink` as it runs, so the merge
|
||||
/// profile can retain 100% full-trace coverage without holding it in memory.
|
||||
pub fn run_all_to(scale: Scale, mut evidence_sink: Option<&mut dyn Write>) -> CiResults {
|
||||
let cfg = EngineConfig::reference();
|
||||
let rut = RuntimeUnderTest::new();
|
||||
|
||||
@@ -537,7 +748,12 @@ 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 meta_consumed_delta = 0usize;
|
||||
let mut meta_consumed_future = 0usize;
|
||||
let mut min_perturbations = usize::MAX;
|
||||
|
||||
let mut contract_pass = 0usize;
|
||||
@@ -553,6 +769,7 @@ pub fn run_all(scale: Scale) -> CiResults {
|
||||
// Provenance leaves: one per actually-committed execution (base + every
|
||||
// perturbation), so the Merkle root binds to all compared executions.
|
||||
let mut merkle_leaves: Vec<Hash> = Vec::with_capacity(scale.executions);
|
||||
let mut trace_evidence: Vec<TraceEvidence> = Vec::with_capacity(TRACE_EVIDENCE_SAMPLE);
|
||||
let mut actual_executions = 0usize;
|
||||
let mut worlds_generated = 0usize;
|
||||
let mut programs_generated = 0usize;
|
||||
@@ -593,12 +810,16 @@ 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_consumed_delta = 0usize;
|
||||
let mut c_consumed_future = 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
|
||||
// reference side.
|
||||
let mut pert_execs: Vec<(ResolutionInput, Canonical, Hash)> = Vec::new();
|
||||
let mut pert_execs: Vec<(ResolutionInput, Canonical, Hash, String)> = Vec::new();
|
||||
for pc in &case.perturbations {
|
||||
let pinput = input_with_world(&case, pc.world.clone());
|
||||
let pr = execute(&cfg, &pinput);
|
||||
@@ -615,10 +836,39 @@ 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;
|
||||
if ad {
|
||||
c_consumed_delta += 1;
|
||||
}
|
||||
if af {
|
||||
c_consumed_future += 1;
|
||||
}
|
||||
}
|
||||
pert_execs.push((pinput, canonical(&pr), pr.replay.hash()));
|
||||
match metamorphic_outcome(&pc.expectation, perturbed_read, at) {
|
||||
ExpectationOutcome::Upheld => {}
|
||||
ExpectationOutcome::ExplainedNeutral => c_explained_neutral += 1,
|
||||
ExpectationOutcome::Violation => c_expect_violation += 1,
|
||||
}
|
||||
// Full-trace evidence line for THIS perturbation leaf (finding 2):
|
||||
// every leaf, base and perturbation, carries a recomputable trace.
|
||||
let pline = format!(
|
||||
"p {:016x} {:016x} {:016x} {:016x} {:016x} {:016x}\t{}\t{}",
|
||||
pr.replay.world_seed,
|
||||
pr.replay.program_seed,
|
||||
pr.replay.contract_seed,
|
||||
pr.replay.perturbation_seed,
|
||||
pr.replay.future_hash.0,
|
||||
pr.replay.hash().0,
|
||||
pr.trace.serialize(),
|
||||
pr.delta.serialize(),
|
||||
);
|
||||
pert_execs.push((pinput, canonical(&pr), pr.replay.hash(), pline));
|
||||
}
|
||||
let future_sensitivity = if c_pert > 0 {
|
||||
c_alt_future as f64 / c_pert as f64
|
||||
@@ -665,7 +915,31 @@ pub fn run_all(scale: Scale) -> CiResults {
|
||||
equiv_failures.push(format!("case {} (base) reference != runtime_under_test", i));
|
||||
}
|
||||
merkle_leaves.push(r.replay.hash());
|
||||
for (pinput, pref_canon, pleaf) in &pert_execs {
|
||||
// Full-trace evidence (finding 4): stream EVERY base execution's full
|
||||
// trace + delta to the sink (100% coverage, no sampling). A small
|
||||
// in-memory sample is also kept for non-streaming callers/tests.
|
||||
if let Some(w) = evidence_sink.as_deref_mut() {
|
||||
let _ = writeln!(
|
||||
w,
|
||||
"b {:016x} {:016x} {:016x} {:016x} {:016x} {:016x}\t{}\t{}",
|
||||
r.replay.world_seed,
|
||||
r.replay.program_seed,
|
||||
r.replay.contract_seed,
|
||||
r.replay.perturbation_seed,
|
||||
r.replay.future_hash.0,
|
||||
r.replay.hash().0,
|
||||
r.trace.serialize(),
|
||||
r.delta.serialize(),
|
||||
);
|
||||
}
|
||||
if trace_evidence.len() < TRACE_EVIDENCE_SAMPLE {
|
||||
trace_evidence.push(TraceEvidence {
|
||||
replay: r.replay,
|
||||
trace: r.trace.clone(),
|
||||
delta: r.delta.clone(),
|
||||
});
|
||||
}
|
||||
for (pinput, pref_canon, pleaf, pline) in &pert_execs {
|
||||
let prut = rut.resolve(pinput.clone());
|
||||
equiv_total += 1;
|
||||
if *pref_canon == canonical(&prut) {
|
||||
@@ -675,6 +949,9 @@ pub fn run_all(scale: Scale) -> CiResults {
|
||||
.push(format!("case {} (perturbation) reference != runtime_under_test", i));
|
||||
}
|
||||
merkle_leaves.push(*pleaf);
|
||||
if let Some(w) = evidence_sink.as_deref_mut() {
|
||||
let _ = writeln!(w, "{}", pline);
|
||||
}
|
||||
}
|
||||
|
||||
actual_executions += 1;
|
||||
@@ -707,7 +984,11 @@ 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;
|
||||
meta_consumed_delta += c_consumed_delta;
|
||||
meta_consumed_future += c_consumed_future;
|
||||
perturbation_runs += c_pert;
|
||||
min_perturbations = min_perturbations.min(c_pert);
|
||||
|
||||
@@ -748,11 +1029,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 +1099,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 +1110,61 @@ 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
|
||||
));
|
||||
}
|
||||
if meta_total > 0 && meta_consumed == 0 {
|
||||
meta_failures.push("metamorphic enforcement vacuous: no consumed perturbations".into());
|
||||
}
|
||||
// Delta and future expectations: per-case strict enforcement is unsound
|
||||
// (clamping/masking), so enforce them as fractions over consumed
|
||||
// perturbations.
|
||||
let mc = meta_consumed.max(1) as f64;
|
||||
let consumed_delta_rate = meta_consumed_delta as f64 / mc;
|
||||
let consumed_future_rate = meta_consumed_future as f64 / mc;
|
||||
if consumed_delta_rate < CONSUMED_DELTA_MIN {
|
||||
meta_failures.push(format!(
|
||||
"consumed-perturbation delta-change rate {:.4} < {}",
|
||||
consumed_delta_rate, CONSUMED_DELTA_MIN
|
||||
));
|
||||
}
|
||||
if consumed_future_rate < CONSUMED_FUTURE_MIN {
|
||||
meta_failures.push(format!(
|
||||
"consumed-perturbation future-change rate {:.4} < {}",
|
||||
consumed_future_rate, CONSUMED_FUTURE_MIN
|
||||
));
|
||||
}
|
||||
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,
|
||||
consumed_delta_rate,
|
||||
consumed_future_rate,
|
||||
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 corpus = BehaviorCorpus::build(collapse_rows.clone());
|
||||
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 +1212,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 +1297,164 @@ pub fn run_all(scale: Scale) -> CiResults {
|
||||
equivalence,
|
||||
domain,
|
||||
metamorphic,
|
||||
causal_explanation,
|
||||
collapse,
|
||||
mutation,
|
||||
contract,
|
||||
replay,
|
||||
coverage,
|
||||
merkle_leaves: retained_leaves,
|
||||
trace_evidence,
|
||||
collapse_feature_rows: collapse_rows,
|
||||
}
|
||||
}
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// 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>,
|
||||
/// Per-edge intervention records, sufficient to independently recompute each
|
||||
/// confirmation (finding 7).
|
||||
pub evidence: Vec<CausalEvidenceRecord>,
|
||||
}
|
||||
|
||||
/// One recomputable per-edge intervention record: regenerate the case from
|
||||
/// `case_seed`, perturb the recorded source lane, and the destination lane's
|
||||
/// delta must move from `base_dv` to `alt_dv` (`confirmed = base_dv != alt_dv`).
|
||||
#[derive(Clone, Copy, Debug)]
|
||||
pub struct CausalEvidenceRecord {
|
||||
pub case_seed: u64,
|
||||
pub from_domain: u8,
|
||||
pub from_lane: u8,
|
||||
pub from_hidden: bool,
|
||||
pub to_domain: u8,
|
||||
pub to_lane: u8,
|
||||
pub to_hidden: bool,
|
||||
pub base_dv: i64,
|
||||
pub alt_dv: i64,
|
||||
}
|
||||
|
||||
impl CausalEvidenceRecord {
|
||||
pub fn confirmed(&self) -> bool {
|
||||
self.base_dv != self.alt_dv
|
||||
}
|
||||
}
|
||||
|
||||
/// 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, Vec<CausalEvidenceRecord>) {
|
||||
let mut tested = 0usize;
|
||||
let mut confirmed = 0usize;
|
||||
let mut records = Vec::new();
|
||||
for i in 0..cases {
|
||||
let seed = case_seed(i);
|
||||
let (case, _) = generate_accepted_case(seed);
|
||||
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;
|
||||
}
|
||||
if !scramble {
|
||||
records.push(CausalEvidenceRecord {
|
||||
case_seed: seed,
|
||||
from_domain: sd as u8,
|
||||
from_lane: sl as u8,
|
||||
from_hidden: shidden,
|
||||
to_domain: dd as u8,
|
||||
to_lane: e.to.lane,
|
||||
to_hidden: e.to.hidden,
|
||||
base_dv,
|
||||
alt_dv,
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
(tested, confirmed, records)
|
||||
}
|
||||
|
||||
pub fn causal_explanation_gate(
|
||||
cfg: &EngineConfig,
|
||||
cases: usize,
|
||||
edges_per_case: usize,
|
||||
) -> CausalExplanationGate {
|
||||
let (tested, confirmed, evidence) = 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,
|
||||
evidence,
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1076,14 +1550,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 +1616,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 +1712,103 @@ 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();
|
||||
assert_eq!(metamorphic_outcome(&active, true, true), ExpectationOutcome::Upheld);
|
||||
// Consumed but trace did not change, not permitted neutral: violation.
|
||||
assert_eq!(metamorphic_outcome(&active, true, false), ExpectationOutcome::Violation);
|
||||
// Not consumed and nothing changed: legitimately neutral.
|
||||
assert_eq!(metamorphic_outcome(&active, false, false), ExpectationOutcome::ExplainedNeutral);
|
||||
}
|
||||
|
||||
/// Delta and future expectations are enforced as consumed-aggregate rates
|
||||
/// (per-case is unsound). A run whose consumed perturbations rarely change
|
||||
/// the delta or future must fail; the reference run is well above both.
|
||||
#[test]
|
||||
fn metamorphic_delta_future_rates_enforced() {
|
||||
let r = run_all(Scale::tiny());
|
||||
assert!(r.metamorphic.consumed_delta_rate >= CONSUMED_DELTA_MIN, "delta rate {}", r.metamorphic.consumed_delta_rate);
|
||||
assert!(r.metamorphic.consumed_future_rate >= CONSUMED_FUTURE_MIN, "future rate {}", r.metamorphic.consumed_future_rate);
|
||||
}
|
||||
|
||||
/// 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
|
||||
);
|
||||
// Per-edge evidence is retained and independently recomputable: replay
|
||||
// each record from its seed and confirm base_dv/alt_dv reproduce.
|
||||
assert!(!gate.evidence.is_empty());
|
||||
let mut rechecked = 0;
|
||||
for rec in gate.evidence.iter().take(64) {
|
||||
let (case, _) = generate_accepted_case(rec.case_seed);
|
||||
let input = input_from_case(&case);
|
||||
let base = execute(&cfg, &input);
|
||||
let mut w = input.world.clone();
|
||||
if rec.from_hidden {
|
||||
let l = rec.from_lane as usize % HIDDEN_LANES;
|
||||
w.domains[rec.from_domain as usize].hidden[l] =
|
||||
w.domains[rec.from_domain as usize].hidden[l].wrapping_add(0x9_27c1);
|
||||
} else {
|
||||
let l = rec.from_lane as usize % LANES;
|
||||
w.domains[rec.from_domain as usize].observed[l] =
|
||||
w.domains[rec.from_domain as usize].observed[l].wrapping_add(0x9_27c1);
|
||||
}
|
||||
let alt = execute(&cfg, &input_with_world(&case, w));
|
||||
let bdv = lane_delta(&base.delta.domain_deltas[rec.to_domain as usize], rec.to_lane as usize, rec.to_hidden);
|
||||
let adv = lane_delta(&alt.delta.domain_deltas[rec.to_domain as usize], rec.to_lane as usize, rec.to_hidden);
|
||||
assert_eq!(bdv, rec.base_dv, "retained base_dv not recomputable");
|
||||
assert_eq!(adv, rec.alt_dv, "retained alt_dv not recomputable");
|
||||
rechecked += 1;
|
||||
}
|
||||
assert!(rechecked >= 64);
|
||||
}
|
||||
|
||||
/// 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() {
|
||||
// The reference passes the FULL engine-behavior acceptance gates over a
|
||||
// real generated-case corpus (not 64 fixed inputs).
|
||||
let refcfg = EngineConfig::reference();
|
||||
assert!(
|
||||
engine_acceptance(&refcfg, MUTATION_GATE_CASES).is_empty(),
|
||||
"reference fails an acceptance gate"
|
||||
);
|
||||
// Every mutant is rejected by those same full gates.
|
||||
let outcome = evaluate_mutants(520, &[]);
|
||||
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)]);
|
||||
|
||||
@@ -4,7 +4,7 @@
|
||||
//! to executed work, and exits nonzero if any gate fails.
|
||||
|
||||
use ci_reports::json::Json;
|
||||
use ci_reports::{run_all, CiResults, Profile, Scale};
|
||||
use ci_reports::{run_all_to, CiResults, Profile, Scale};
|
||||
use std::fs;
|
||||
use std::io::Write;
|
||||
use std::path::Path;
|
||||
@@ -29,6 +29,93 @@ 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");
|
||||
|
||||
// Per-edge causal intervention evidence (finding 7): one recomputable record
|
||||
// per tested edge.
|
||||
let mut causal = String::from(
|
||||
"seed\tfrom_domain\tfrom_lane\tfrom_hidden\tto_domain\tto_lane\tto_hidden\tbase_dv\talt_dv\n",
|
||||
);
|
||||
for rec in &r.causal_explanation.evidence {
|
||||
causal.push_str(&format!(
|
||||
"{:016x}\t{}\t{}\t{}\t{}\t{}\t{}\t{}\t{}\n",
|
||||
rec.case_seed,
|
||||
rec.from_domain,
|
||||
rec.from_lane,
|
||||
rec.from_hidden as u8,
|
||||
rec.to_domain,
|
||||
rec.to_lane,
|
||||
rec.to_hidden as u8,
|
||||
rec.base_dv,
|
||||
rec.alt_dv,
|
||||
));
|
||||
}
|
||||
fs::write(ev.join("causal_evidence.tsv"), causal).expect("write causal evidence");
|
||||
|
||||
// Collapse feature rows (finding 4): the summaries the collapse gate consumes,
|
||||
// in the same order as the first base trace records. Stored as f64 bits so an
|
||||
// attestor can recompute each row from the full trace and compare bit-exact.
|
||||
let mut crows = String::new();
|
||||
for row in &r.collapse_feature_rows {
|
||||
let cells: Vec<String> = row.iter().map(|v| v.to_bits().to_string()).collect();
|
||||
crows.push_str(&cells.join(" "));
|
||||
crows.push('\n');
|
||||
}
|
||||
fs::write(ev.join("collapse_feature_rows.tsv"), crows).expect("write collapse rows");
|
||||
|
||||
// Artifact bundle manifest (finding 1): the merge-scale claim is only valid
|
||||
// if this complete, content-hashed bundle is retained. The attestor verifies
|
||||
// every listed file exists and its hash + length match.
|
||||
let bundle = [
|
||||
"leaves.tsv",
|
||||
"claims.tsv",
|
||||
"causal_evidence.tsv",
|
||||
"collapse_feature_rows.tsv",
|
||||
"traces.tsv",
|
||||
];
|
||||
let mut manifest = String::from("file\thash\tbytes\n");
|
||||
for name in bundle {
|
||||
let bytes = fs::read(ev.join(name)).unwrap_or_default();
|
||||
let mut h = world_model::Hasher::new();
|
||||
h.write_tag("evidence-file");
|
||||
h.write_bytes(&bytes);
|
||||
manifest.push_str(&format!("{}\t{:016x}\t{}\n", name, h.finish().0, bytes.len()));
|
||||
}
|
||||
fs::write(ev.join("MANIFEST.tsv"), manifest).expect("write manifest");
|
||||
// Note: evidence/traces.tsv (the FULL per-execution trace corpus) is streamed
|
||||
// during the run in main(), covering 100% of base executions — not written
|
||||
// here from a capped sample.
|
||||
}
|
||||
|
||||
fn build_reports(dir: &Path, r: &CiResults) {
|
||||
// 1. domain_participation_report
|
||||
write_report(
|
||||
@@ -111,11 +198,29 @@ 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)),
|
||||
("consumed_delta_change_rate".into(), Json::Num(r.metamorphic.consumed_delta_rate)),
|
||||
("consumed_future_change_rate".into(), Json::Num(r.metamorphic.consumed_future_rate)),
|
||||
("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 +271,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 +334,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 +447,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",
|
||||
@@ -551,10 +667,21 @@ fn main() {
|
||||
}
|
||||
let merge = scale.profile == Profile::Merge;
|
||||
let start = Instant::now();
|
||||
let results = run_all(scale);
|
||||
// Stream full-trace evidence for 100% of base executions straight to disk.
|
||||
let ev_dir = dir.join("evidence");
|
||||
fs::create_dir_all(&ev_dir).expect("create evidence dir");
|
||||
let traces_path = ev_dir.join("traces.tsv");
|
||||
let mut traces_w = std::io::BufWriter::new(fs::File::create(&traces_path).expect("create traces"));
|
||||
traces_w
|
||||
.write_all(b"# full-trace evidence (100% of base executions): header<TAB>trace<TAB>delta\n")
|
||||
.expect("write traces header");
|
||||
let results = run_all_to(scale, Some(&mut traces_w));
|
||||
traces_w.flush().expect("flush traces");
|
||||
drop(traces_w);
|
||||
let elapsed = start.elapsed();
|
||||
|
||||
build_reports(dir, &results);
|
||||
write_evidence(dir, &results);
|
||||
write_markdown(dir, &results);
|
||||
let compliance_ok = build_compliance_report(dir, &results);
|
||||
|
||||
|
||||
@@ -21,7 +21,46 @@
|
||||
pub mod linalg;
|
||||
|
||||
use linalg::{ols_r2, pca_scores, Mat};
|
||||
use world_model::NUM_DOMAINS;
|
||||
use trace_model::ExecutionTrace;
|
||||
use world_model::{WorldDelta, NUM_DOMAINS};
|
||||
|
||||
/// The single definition of a trace feature row. The collapse corpus is built
|
||||
/// from these rows; an attestor recomputes the same row from the retained FULL
|
||||
/// trace and delta and checks equality, which is how the summary is proven to
|
||||
/// derive from the full trace. Layout per domain block (`BLOCK_W`):
|
||||
/// `[infl_out, infl_in, flow_out, flow_in, read, write, temporal, obs_delta,
|
||||
/// hid_delta]`, then globals `[causal_rank, edge_count, touched, divergence]`.
|
||||
pub fn trace_feature_row(trace: &ExecutionTrace, delta: &WorldDelta) -> Vec<f64> {
|
||||
let infl = trace.causal_graph.influence_matrix();
|
||||
let mut flow = [[0.0f64; NUM_DOMAINS]; NUM_DOMAINS];
|
||||
for &(a, b, bits) in &trace.information_flow.edges {
|
||||
flow[a as usize % NUM_DOMAINS][b as usize % NUM_DOMAINS] += bits as f64;
|
||||
}
|
||||
let mut temporal = [0.0f64; NUM_DOMAINS];
|
||||
for &(_s, _off, d) in &trace.temporal_graph.edges {
|
||||
temporal[d as usize % NUM_DOMAINS] += 1.0;
|
||||
}
|
||||
let mut row = Vec::with_capacity(FEATURE_W);
|
||||
for d in 0..NUM_DOMAINS {
|
||||
let infl_out: f64 = (0..NUM_DOMAINS).map(|j| infl[d][j]).sum();
|
||||
let infl_in: f64 = (0..NUM_DOMAINS).map(|i| infl[i][d]).sum();
|
||||
let flow_out: f64 = (0..NUM_DOMAINS).map(|j| flow[d][j]).sum();
|
||||
let flow_in: f64 = (0..NUM_DOMAINS).map(|i| flow[i][d]).sum();
|
||||
let read = trace.read_graph.access_count[d] as f64;
|
||||
let write = trace.write_graph.access_count[d] as f64;
|
||||
let temp = temporal[d];
|
||||
let obs_delta: f64 = delta.domain_deltas[d].observed.iter().map(|&v| (v as f64).abs()).sum();
|
||||
let hid_delta: f64 = delta.domain_deltas[d].hidden.iter().map(|&v| (v as f64).abs()).sum();
|
||||
row.extend_from_slice(&[
|
||||
infl_out, infl_in, flow_out, flow_in, read, write, temp, obs_delta, hid_delta,
|
||||
]);
|
||||
}
|
||||
row.push(trace.causal_rank() as f64);
|
||||
row.push(trace.causal_edge_count() as f64);
|
||||
row.push(trace.touched_domain_count() as f64);
|
||||
row.push(trace.context_divergence());
|
||||
row
|
||||
}
|
||||
|
||||
/// Width of one per-domain feature block in a trace feature row.
|
||||
/// `[infl_out, infl_in, flow_out, flow_in, read, write, temporal, obs_delta, hid_delta]`
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
@@ -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(),
|
||||
|
||||
@@ -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)));
|
||||
}
|
||||
}
|
||||
@@ -404,12 +404,216 @@ impl ExecutionTrace {
|
||||
],
|
||||
)
|
||||
}
|
||||
|
||||
/// Serialize the FULL trace — every graph edge, count, and weight — to a
|
||||
/// single line of whitespace-separated integers. This is the full-trace
|
||||
/// *evidence* (not a summary): [`deserialize`] reconstructs the trace and
|
||||
/// [`canonical_hash`] over the result is bit-identical, so an independent
|
||||
/// verifier can recompute the trace hash from the raw structure rather than
|
||||
/// trusting a reported digest. `f64` divergence values are stored as raw
|
||||
/// bits for exact round-trip; the behavior-fingerprint hash is NOT stored —
|
||||
/// it is re-derived from the features on load, so a fabricated digest cannot
|
||||
/// survive.
|
||||
pub fn serialize(&self) -> String {
|
||||
let mut t: Vec<String> = vec!["trace-v1".to_string()];
|
||||
let push_access = |t: &mut Vec<String>, g: &DomainAccessGraph| {
|
||||
for c in &g.access_count {
|
||||
t.push(c.to_string());
|
||||
}
|
||||
t.push(g.edges.len().to_string());
|
||||
for &(a, b, w) in &g.edges {
|
||||
t.push(a.to_string());
|
||||
t.push(b.to_string());
|
||||
t.push(w.to_string());
|
||||
}
|
||||
};
|
||||
push_access(&mut t, &self.read_graph);
|
||||
push_access(&mut t, &self.write_graph);
|
||||
// causal
|
||||
t.push(self.causal_graph.edges.len().to_string());
|
||||
for e in &self.causal_graph.edges {
|
||||
for v in [
|
||||
e.from.domain as i64, e.from.lane as i64, e.from.hidden as i64, e.from.step as i64,
|
||||
e.to.domain as i64, e.to.lane as i64, e.to.hidden as i64, e.to.step as i64, e.weight,
|
||||
] {
|
||||
t.push(v.to_string());
|
||||
}
|
||||
}
|
||||
// information flow
|
||||
t.push(self.information_flow.edges.len().to_string());
|
||||
for &(a, b, w) in &self.information_flow.edges {
|
||||
t.push(a.to_string());
|
||||
t.push(b.to_string());
|
||||
t.push(w.to_string());
|
||||
}
|
||||
// divergence (f64 as raw bits)
|
||||
t.push(self.executor_divergence.executor_count.to_string());
|
||||
t.push(self.executor_divergence.pairwise.len().to_string());
|
||||
for &v in &self.executor_divergence.pairwise {
|
||||
t.push(v.to_bits().to_string());
|
||||
}
|
||||
// temporal
|
||||
t.push(self.temporal_graph.edges.len().to_string());
|
||||
for &(s, off, d) in &self.temporal_graph.edges {
|
||||
t.push(s.to_string());
|
||||
t.push(off.to_string());
|
||||
t.push(d.to_string());
|
||||
}
|
||||
// perturbation response
|
||||
for v in [
|
||||
self.perturbation_response.total,
|
||||
self.perturbation_response.altered_trace,
|
||||
self.perturbation_response.altered_delta,
|
||||
self.perturbation_response.altered_future,
|
||||
self.perturbation_response.neutral_unexplained,
|
||||
] {
|
||||
t.push(v.to_string());
|
||||
}
|
||||
// behavior features (fingerprint hash re-derived on load)
|
||||
t.push(self.behavior_fingerprint.features.len().to_string());
|
||||
for &f in &self.behavior_fingerprint.features {
|
||||
t.push(f.to_string());
|
||||
}
|
||||
t.join(" ")
|
||||
}
|
||||
|
||||
/// Reconstruct a trace from [`serialize`]. Total: returns `None` on any
|
||||
/// malformed input rather than panicking.
|
||||
pub fn deserialize(s: &str) -> Option<ExecutionTrace> {
|
||||
let mut it = s.split_whitespace();
|
||||
if it.next()? != "trace-v1" {
|
||||
return None;
|
||||
}
|
||||
let nu = |it: &mut std::str::SplitWhitespace| -> Option<u64> { it.next()?.parse().ok() };
|
||||
let ni = |it: &mut std::str::SplitWhitespace| -> Option<i64> { it.next()?.parse().ok() };
|
||||
let read_access = |it: &mut std::str::SplitWhitespace| -> Option<DomainAccessGraph> {
|
||||
let mut access_count = [0u32; NUM_DOMAINS];
|
||||
for c in access_count.iter_mut() {
|
||||
*c = nu(it)? as u32;
|
||||
}
|
||||
let n = nu(it)? as usize;
|
||||
let mut edges = Vec::with_capacity(n);
|
||||
for _ in 0..n {
|
||||
edges.push((nu(it)? as u8, nu(it)? as u8, nu(it)? as u32));
|
||||
}
|
||||
Some(DomainAccessGraph { access_count, edges })
|
||||
};
|
||||
let read_graph = read_access(&mut it)?;
|
||||
let write_graph = read_access(&mut it)?;
|
||||
// causal
|
||||
let cn = nu(&mut it)? as usize;
|
||||
let mut cedges = Vec::with_capacity(cn);
|
||||
for _ in 0..cn {
|
||||
let from = CausalNode {
|
||||
domain: ni(&mut it)? as u8,
|
||||
lane: ni(&mut it)? as u8,
|
||||
hidden: ni(&mut it)? != 0,
|
||||
step: ni(&mut it)? as u32,
|
||||
};
|
||||
let to = CausalNode {
|
||||
domain: ni(&mut it)? as u8,
|
||||
lane: ni(&mut it)? as u8,
|
||||
hidden: ni(&mut it)? != 0,
|
||||
step: ni(&mut it)? as u32,
|
||||
};
|
||||
let weight = ni(&mut it)?;
|
||||
cedges.push(CausalEdge { from, to, weight });
|
||||
}
|
||||
// info flow
|
||||
let fin = nu(&mut it)? as usize;
|
||||
let mut fedges = Vec::with_capacity(fin);
|
||||
for _ in 0..fin {
|
||||
fedges.push((nu(&mut it)? as u8, nu(&mut it)? as u8, nu(&mut it)? as u32));
|
||||
}
|
||||
// divergence
|
||||
let executor_count = nu(&mut it)? as usize;
|
||||
let pn = nu(&mut it)? as usize;
|
||||
let mut pairwise = Vec::with_capacity(pn);
|
||||
for _ in 0..pn {
|
||||
pairwise.push(f64::from_bits(nu(&mut it)?));
|
||||
}
|
||||
// temporal
|
||||
let tn = nu(&mut it)? as usize;
|
||||
let mut tedges = Vec::with_capacity(tn);
|
||||
for _ in 0..tn {
|
||||
tedges.push((nu(&mut it)? as u32, nu(&mut it)? as u8, nu(&mut it)? as u8));
|
||||
}
|
||||
// perturbation response
|
||||
let pr = PerturbationResponse {
|
||||
total: nu(&mut it)? as usize,
|
||||
altered_trace: nu(&mut it)? as usize,
|
||||
altered_delta: nu(&mut it)? as usize,
|
||||
altered_future: nu(&mut it)? as usize,
|
||||
neutral_unexplained: nu(&mut it)? as usize,
|
||||
};
|
||||
// behavior features
|
||||
let bn = nu(&mut it)? as usize;
|
||||
let mut features = Vec::with_capacity(bn);
|
||||
for _ in 0..bn {
|
||||
features.push(ni(&mut it)?);
|
||||
}
|
||||
Some(ExecutionTrace {
|
||||
read_graph,
|
||||
write_graph,
|
||||
causal_graph: CausalGraph { edges: cedges },
|
||||
information_flow: InformationFlowGraph { edges: fedges },
|
||||
executor_divergence: DivergenceGraph { executor_count, pairwise },
|
||||
temporal_graph: TemporalGraph { edges: tedges },
|
||||
perturbation_response: pr,
|
||||
// Re-derive the fingerprint hash from features (not from a stored digest).
|
||||
behavior_fingerprint: BehaviorFingerprint::from_features(features),
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
|
||||
fn sample_trace() -> ExecutionTrace {
|
||||
let mut read_graph = DomainAccessGraph::default();
|
||||
read_graph.access_count[0] = 3;
|
||||
read_graph.access_count[2] = 1;
|
||||
read_graph.edges.push((0, 2, 5));
|
||||
let mut write_graph = DomainAccessGraph::default();
|
||||
write_graph.access_count[2] = 4;
|
||||
write_graph.edges.push((0, 2, 7));
|
||||
let causal_graph = CausalGraph {
|
||||
edges: vec![CausalEdge {
|
||||
from: CausalNode { domain: 0, lane: 1, hidden: false, step: 2 },
|
||||
to: CausalNode { domain: 2, lane: 0, hidden: true, step: 2 },
|
||||
weight: -1234,
|
||||
}],
|
||||
};
|
||||
ExecutionTrace {
|
||||
read_graph,
|
||||
write_graph,
|
||||
causal_graph,
|
||||
information_flow: InformationFlowGraph { edges: vec![(0, 2, 9), (2, 3, 4)] },
|
||||
executor_divergence: DivergenceGraph { executor_count: 3, pairwise: vec![0.0, 0.5, 0.25, 0.5, 0.0, 0.125, 0.25, 0.125, 0.0] },
|
||||
temporal_graph: TemporalGraph { edges: vec![(1, 2, 3)] },
|
||||
perturbation_response: PerturbationResponse::default(),
|
||||
behavior_fingerprint: BehaviorFingerprint::from_features(vec![1, -2, 3, -4]),
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn full_trace_serialize_roundtrips_canonical_hash() {
|
||||
let t = sample_trace();
|
||||
let s = t.serialize();
|
||||
let back = ExecutionTrace::deserialize(&s).expect("deserialize");
|
||||
// The reconstructed trace is structurally equal and hashes identically.
|
||||
assert_eq!(t, back);
|
||||
assert_eq!(t.canonical_hash(), back.canonical_hash());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn deserialize_is_total_on_garbage() {
|
||||
for s in ["", "nope", "trace-v1 1 2", "trace-v1 x y z"] {
|
||||
let _ = ExecutionTrace::deserialize(s); // must not panic
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn rank_of_identity_is_full() {
|
||||
let id: Vec<Vec<f64>> = (0..5)
|
||||
|
||||
@@ -33,12 +33,4 @@ mod tests {
|
||||
assert!(resolve("/style.css").is_some());
|
||||
assert!(resolve("/nope").is_none());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn client_only_sends_intent() {
|
||||
// Guard against the client ever embedding a second simulation: the
|
||||
// browser code must not reference the reference engine internals.
|
||||
assert!(!APP_JS.contains("EngineConfig"));
|
||||
assert!(APP_JS.contains("only ever sends INTENT"));
|
||||
}
|
||||
}
|
||||
|
||||
@@ -262,4 +262,45 @@ impl WorldDelta {
|
||||
}
|
||||
h.finish()
|
||||
}
|
||||
|
||||
/// Serialize the full delta to one line of whitespace-separated integers.
|
||||
/// Round-trips [`hash`] exactly (used as attestation evidence).
|
||||
pub fn serialize(&self) -> String {
|
||||
let mut t: Vec<String> = vec!["delta-v1".to_string(), self.turn_advance.to_string()];
|
||||
t.push(self.domain_deltas.len().to_string());
|
||||
for d in &self.domain_deltas {
|
||||
t.push(d.domain.0.to_string());
|
||||
for &v in &d.observed {
|
||||
t.push(v.to_string());
|
||||
}
|
||||
for &v in &d.hidden {
|
||||
t.push(v.to_string());
|
||||
}
|
||||
}
|
||||
t.join(" ")
|
||||
}
|
||||
|
||||
/// Reconstruct a delta from [`serialize`]. Total: `None` on malformed input.
|
||||
pub fn deserialize(s: &str) -> Option<WorldDelta> {
|
||||
let mut it = s.split_whitespace();
|
||||
if it.next()? != "delta-v1" {
|
||||
return None;
|
||||
}
|
||||
let turn_advance: u64 = it.next()?.parse().ok()?;
|
||||
let n: usize = it.next()?.parse().ok()?;
|
||||
let mut domain_deltas = Vec::with_capacity(n);
|
||||
for _ in 0..n {
|
||||
let domain = DomainId(it.next()?.parse().ok()?);
|
||||
let mut observed = [0i64; LANES];
|
||||
for v in observed.iter_mut() {
|
||||
*v = it.next()?.parse().ok()?;
|
||||
}
|
||||
let mut hidden = [0i64; HIDDEN_LANES];
|
||||
for v in hidden.iter_mut() {
|
||||
*v = it.next()?.parse().ok()?;
|
||||
}
|
||||
domain_deltas.push(DomainDelta { domain, observed, hidden });
|
||||
}
|
||||
Some(WorldDelta { domain_deltas, turn_advance })
|
||||
}
|
||||
}
|
||||
|
||||
-196
@@ -1,196 +0,0 @@
|
||||
Finding 1
|
||||
SEVERITY: CRITICAL
|
||||
|
||||
SPEC REQUIREMENT: Every acceptance requirement must have a merge-blocking enforcement point; merge blocked
|
||||
unless all reports pass. See plan.md:20 and plan.md:298.
|
||||
|
||||
IMPLEMENTATION LOCATION: .github/workflows/merge-gates.yml:37, README.md:111
|
||||
|
||||
EXPLOIT PATH: The repo contains a workflow, but no enforceable branch-protection or merge-queue
|
||||
configuration. The merge-gates job is skipped on ordinary pull_request events and only runs on merge_group
|
||||
or push.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: The code and reports can pass locally or in CI while actual repository
|
||||
settings do not require the job before merge.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: A workflow file plus README instruction is not proof that merge is blocked if
|
||||
the gate is absent.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: A verifiable branch-protection or merge-queue ruleset
|
||||
export showing merge-gates is a required pre-merge status check for main.
|
||||
|
||||
Finding 2
|
||||
SEVERITY: CRITICAL
|
||||
|
||||
SPEC REQUIREMENT: Compliance evidence must not be self-validating; every obligation needs artifact,
|
||||
provenance, merge-blocking enforcement, and failure if absent.
|
||||
|
||||
IMPLEMENTATION LOCATION: crates/ci_reports/src/main.rs:360, crates/ci_reports/src/main.rs:375
|
||||
|
||||
EXPLOIT PATH: The CI binary writes the reports, checks their presence, and emits "merge_blocking": true
|
||||
itself.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: The same process that generates evidence declares the compliance model
|
||||
satisfied.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: The merge-blocking claim is not independently measured; it is a constant in a
|
||||
generated artifact.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Compliance report generated or attested by an external CI
|
||||
controller with immutable run id, workflow id, and required-check status.
|
||||
|
||||
Finding 3
|
||||
SEVERITY: HIGH
|
||||
|
||||
SPEC REQUIREMENT: Measured artifacts need a provenance chain from artifact to run.
|
||||
|
||||
IMPLEMENTATION LOCATION: crates/ci_reports/src/lib.rs:553, crates/ci_reports/src/lib.rs:667, crates/
|
||||
ci_reports/src/main.rs:219
|
||||
|
||||
EXPLOIT PATH: The Merkle root is computed from in-memory replay hashes; the leaves, inputs, seeds, reference
|
||||
outputs, and runtime-under-test outputs are not persisted.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: The report exposes only root and count, and internally checks only
|
||||
merkle_leaves.len() == equiv_total.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: A root without independently replayable leaves is not a provenance chain; it is
|
||||
a summary generated by the audited process.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Persisted per-execution records sufficient to recompute
|
||||
the Merkle root and verify reference/runtime comparison independently.
|
||||
|
||||
Finding 4
|
||||
SEVERITY: HIGH
|
||||
|
||||
SPEC REQUIREMENT: Full trace information may not be replaced by summarized proxy; collapse gates must prove
|
||||
smaller models cannot predict behavior.
|
||||
|
||||
IMPLEMENTATION LOCATION: crates/ci_reports/src/lib.rs:343, crates/ci_reports/src/lib.rs:720, crates/
|
||||
ci_reports/src/lib.rs:178
|
||||
|
||||
EXPLOIT PATH: Collapse analysis uses a 76-feature aggregate row and only scale.collapse_samples rows. Merge
|
||||
default is 5,000 samples, and MAGICKA_COLLAPSE can lower it because no merge floor applies.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: Compression gates run on the aggregate subset, not on full serialized
|
||||
traces or all executions.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: This is summary/subset/proxy laundering for a stronger trace-information
|
||||
requirement.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Collapse artifacts over all merge executions using full
|
||||
serialized ExecutionTrace records, with no lowering override.
|
||||
|
||||
Finding 5
|
||||
SEVERITY: HIGH
|
||||
|
||||
SPEC REQUIREMENT: 500 semantic mutants minimum; every mutant must fail at least one named acceptance gate.
|
||||
|
||||
IMPLEMENTATION LOCATION: crates/ci_reports/src/lib.rs:723, crates/semantic_mutation/src/lib.rs:207, crates/
|
||||
semantic_mutation/src/lib.rs:345
|
||||
|
||||
EXPLOIT PATH: Mutants are evaluated against at most 64 inputs and mirrored mini-gates, not the actual full
|
||||
acceptance gates. Domain, temporal, and causal checks omit large parts of the real gates.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: mutation.passed() only requires no survivors under these local
|
||||
evaluators.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: A mirrored evaluator over a representative input slice is not “the named
|
||||
acceptance gate.”
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Survivor report showing each mutant executed against the
|
||||
actual merge gates and full acceptance corpus.
|
||||
|
||||
Finding 6
|
||||
SEVERITY: HIGH
|
||||
|
||||
SPEC REQUIREMENT: Replay corpus: every failure becomes permanent.
|
||||
|
||||
IMPLEMENTATION LOCATION: crates/replay_corpus/src/lib.rs:61, crates/replay_corpus/src/lib.rs:151
|
||||
|
||||
EXPLOIT PATH: The corpus is generated from deterministic master seeds and current reference outputs. There
|
||||
is no path that captures CI failures and appends them to the committed corpus.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: Replay verifies 10,000 static rows have no drift.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: Static seed replay is not permanent retention of every discovered failure.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Corpus history or artifact proving failing cases from
|
||||
prior CI runs are persisted and rechecked.
|
||||
|
||||
Finding 7
|
||||
SEVERITY: HIGH
|
||||
|
||||
SPEC REQUIREMENT: Web Phase H requires Playwright end-to-end tests and 100 browser E2E matches.
|
||||
|
||||
IMPLEMENTATION LOCATION: plan2.md:210, .github/workflows/web-gates.yml:45, crates/web_tests/tests/e2e.rs:1
|
||||
|
||||
EXPLOIT PATH: The merge-blocking “100 E2E” test is explicitly headless protocol/socket coverage. Rendered-
|
||||
browser Playwright is advisory and continue-on-error.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: Browser UI can fail while merge-blocking Rust socket tests pass.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: Browser E2E is substituted with protocol E2E.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Required, non-advisory Playwright browser E2E job running
|
||||
the 100-match browser gate before merge.
|
||||
|
||||
Finding 8
|
||||
SEVERITY: MEDIUM
|
||||
|
||||
SPEC REQUIREMENT: Generated case gates include future dependence within 3 turns and hidden/observed
|
||||
divergence.
|
||||
|
||||
IMPLEMENTATION LOCATION: crates/generators/src/lib.rs:240, crates/generators/src/lib.rs:242, crates/
|
||||
generators/src/lib.rs:278
|
||||
|
||||
EXPLOIT PATH: Future dependence is approximated by presence of a Schedule opcode. Hidden/observed divergence
|
||||
is approximated by nonzero hidden state or any masked lane, not measured behavior.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: A case can pass generated gates based on structure even if runtime
|
||||
behavior does not satisfy the stated property.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: Structural indicators are reported as generated-case requirements.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Generated-gate artifact based on measured execution
|
||||
traces and measured 3-turn future sensitivity.
|
||||
|
||||
Finding 9
|
||||
SEVERITY: MEDIUM
|
||||
|
||||
SPEC REQUIREMENT: Perturbations are generated from domain surfaces, not a fixed list, and expected trace
|
||||
differences must be meaningful.
|
||||
|
||||
IMPLEMENTATION LOCATION: crates/world_model/src/domain.rs:184, crates/generators/src/lib.rs:143, crates/
|
||||
ci_reports/src/lib.rs:606
|
||||
|
||||
EXPLOIT PATH: Each domain exposes a small hard-coded axis set. The metamorphic gate mostly compares hashes
|
||||
and only uses neutral_explanation; it ignores expect_trace_change, expect_delta_change, and
|
||||
expect_future_change.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: Aggregate perturbation thresholds can pass without proving surface-
|
||||
derived coverage or per-axis expectations.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: Fixed-axis perturbations and unused expectations are weaker than the required
|
||||
metamorphic contract.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Per-axis report proving generated axes derive from read/
|
||||
write surfaces and each expected difference is enforced.
|
||||
|
||||
Finding 10
|
||||
SEVERITY: MEDIUM
|
||||
|
||||
SPEC REQUIREMENT: Trace evidence must explain causality; reject if trace evidence cannot explain causality.
|
||||
|
||||
IMPLEMENTATION LOCATION: crates/trace_model/src/lib.rs:353, crates/ci_reports/src/lib.rs:741
|
||||
|
||||
EXPLOIT PATH: Trace gates check counts, rank, touched domains, fingerprint collisions, and largest cluster.
|
||||
They do not verify that causal edges are independently reconstructable from opcode semantics and world
|
||||
state.
|
||||
|
||||
HOW THE IMPLEMENTATION STILL PASSES: A runtime can emit plausible high-rank causal edges and pass aggregate
|
||||
metrics.
|
||||
|
||||
WHY THIS VIOLATES THE SPEC: Trace quantity is treated as causal explanation.
|
||||
|
||||
MINIMUM EVIDENCE REQUIRED TO DISPROVE THE FINDING: Independent causal audit artifact mapping trace edges
|
||||
back to executed tokens, source values, destination values, and state transitions.
|
||||
-271
@@ -1,271 +0,0 @@
|
||||
|
||||
=============
|
||||
README.md
|
||||
=============
|
||||
|
||||
# Magicka VM — Phase 0/1
|
||||
|
||||
> The deliverable is a Rust engine whose tests make a fake universe fail.
|
||||
|
||||
This repository implements the Phase 0/1 specification in `plan.md`: an
|
||||
**adversarial testing framework first**, then a **reference runtime** that
|
||||
passes it, then a **runtime under test** that matches the reference. No spell
|
||||
content, templates, or cosmetic runes — the value is in the tests that refuse
|
||||
to let the universe collapse into a single score, resource, effect axis,
|
||||
executor, rune, hidden formula, or decorative domain.
|
||||
|
||||
## Compliance model
|
||||
|
||||
No gate may pass from configuration, naming, shared implementation, smoke-scale
|
||||
runs, regenerated expectations, proxy metrics, a default profile, or a
|
||||
locally-runnable binary. A gate passes only from persisted, independently
|
||||
reproducible, full-scale adversarial evidence enforced at merge. Every
|
||||
acceptance obligation has all four of: a **measured artifact**, a **provenance
|
||||
chain** to the run that produced it, a **merge-blocking enforcement point**, and
|
||||
a **failure condition if the artifact or provenance is absent**.
|
||||
|
||||
- The merge-blocking enforcement point is `.github/workflows/merge-gates.yml`,
|
||||
whose `merge-gates` job runs `MAGICKA_PROFILE=merge` (full gates) and must be a
|
||||
**required status check** on the protected branch / merge queue. It is not a
|
||||
local binary, and the fast profile is advisory only — it can never stand in for
|
||||
acceptance.
|
||||
- `compliance_report.json` enumerates every obligation, its artifact, its floor,
|
||||
the actual measured value, and whether the artifact is present. A missing
|
||||
required report fails acceptance.
|
||||
- The merge floors (50k worlds, 250k programs, 1,000,000 executions, 10
|
||||
perturbations/exec, 100% reference/runtime comparison over base **and**
|
||||
perturbations, 500 mutants, 10,000 replay cases) cannot be lowered by
|
||||
environment overrides: a lowering override is recorded as a provenance failure
|
||||
and the floor is kept.
|
||||
|
||||
Every gate is built to be *able to fail*, and a negative-control test proves it does:
|
||||
|
||||
| Gate | How it is made unbypassable | Negative control proving it can fail |
|
||||
|------|-----------------------------|--------------------------------------|
|
||||
| runtime_equivalence | Compares two **independent implementations** (the reference engine vs. `runtime_under_test::native`, which never calls the reference engine) | `buggy_runtime_is_rejected` — a runtime with one dropped causal edge is caught |
|
||||
| compression_resistance | Attacks operate on the **real serialized trace** (causal influence, info-flow, access, temporal, deltas), not a hash proxy; info loss is genuine unexplained variance | `single_factor_corpus_is_rejected` — a rank-1 universe is rejected |
|
||||
| mutation_survivor | Each mutant must fail the **named gate** it targets, not merely differ from the reference | `reference_passes_every_named_gate` + `no_mutant_survives_its_named_gate` |
|
||||
| replay | Expectations are **loaded from a committed file**, not regenerated in the same run | `corrupted_expectation_is_detected` |
|
||||
| domain_participation | Decorative/redundant domains are flagged directly | `decorative_domain_is_rejected` |
|
||||
| merge scale floor | Env overrides may only **raise** merge counts; a lowering attempt is recorded and the floor kept; executions actually performed are counted | `merge_floor_cannot_be_lowered_by_override`, `merge_profile_at_smoke_scale_is_rejected` |
|
||||
| 100% comparison | Reference vs. runtime-under-test compared for **every** execution — base and all perturbations, never base only | `runtime_equivalence` gate fails unless `equiv_total == base + perturbations` |
|
||||
| provenance | A Merkle root over per-execution records, plus independent engine identities, binds reported numbers to executed work | `merkle_root_binds_to_leaves` |
|
||||
|
||||
## Workspace layout
|
||||
|
||||
Built in the mandatory order from the spec:
|
||||
|
||||
| # | Crate | Role |
|
||||
|---|-------|------|
|
||||
| 1 | `world_model` | 8 independent domains, world snapshot, perturbation axes, deltas, deterministic primitives (ids, stable hash, RNG) |
|
||||
| – | `rune_ir` | Rune token / program model (no stream is ever rejected) |
|
||||
| 2 | `trace_model` | Execution trace + all graphs, behavior fingerprint, replay record, fault log, trace metrics |
|
||||
| 3 | `generators` | Worlds, programs, executors, contracts, perturbations; rejects flat cases |
|
||||
| 4 | `collapse_analysis` | The 11 compression attacks over real trace structure + collapse gates |
|
||||
| 5 | `semantic_mutation` | Structurally generated mutant runtimes; proves every one fails its named gate |
|
||||
| 6 | `replay_corpus` | Permanent, bit-exact replay cases persisted to `corpus/replay_corpus.tsv` |
|
||||
| 7 | `reference_runtime` | The executable spec engine (`Runtime` trait, `resolve`) |
|
||||
| 8 | `runtime_under_test` | An **independent** interpreter (`native`) proven equivalent to the reference |
|
||||
| – | `ci_reports` | Orchestrator + `ci` binary; emits 8 gate reports + a provenance report |
|
||||
|
||||
The runtime under test does not call the reference engine. It re-derives the
|
||||
canonical behavior from the spec in a different code organization, so 100%
|
||||
agreement is *evidence* the spec is implemented correctly rather than a
|
||||
tautology. (`native_matches_reference_bit_for_bit` checks this over a 2000-seed
|
||||
sweep.)
|
||||
|
||||
## The engine in one paragraph
|
||||
|
||||
A world is 8 domains, each with 4 observed + 2 hidden integer lanes, a dense
|
||||
8×8 coupling matrix, partial observability, and pending scheduled effects. A
|
||||
rune program is interpreted under ≥3 executors; each opcode reads several
|
||||
domains, mixes them through a nonlinear avalanche keyed by per-domain
|
||||
constants, the world coupling, and the executor's salt, then writes back —
|
||||
recording causal/read/write/information-flow/temporal edges as it goes.
|
||||
Scheduled effects and coupling diffusion propagate changes 3 turns into the
|
||||
future.
|
||||
|
||||
## Running CI
|
||||
|
||||
```bash
|
||||
cargo test # unit tests + negative controls
|
||||
MAGICKA_PROFILE=fast cargo run --release -p ci_reports --bin ci # advisory PR slice
|
||||
MAGICKA_PROFILE=merge cargo run --release -p ci_reports --bin ci # acceptance (full gates)
|
||||
```
|
||||
|
||||
Reports are written to the output dir (8 gate reports + `provenance_report.json`
|
||||
+ `compliance_report.json` + `ci_summary.md`). The binary exits non-zero if any
|
||||
gate fails or any required artifact is absent.
|
||||
|
||||
### Profiles
|
||||
|
||||
`MAGICKA_PROFILE` (or `MAGICKA_SCALE`) selects the run profile.
|
||||
|
||||
| Profile | executions | replay | mutants | role |
|
||||
|---------|-----------|--------|---------|------|
|
||||
| `fast` (default) | 600 | 10,000 (committed) | 520 | **advisory only — never acceptance** |
|
||||
| `tiny` | 120 | 10,000 | 520 | smoke |
|
||||
| `merge` (`MAGICKA_SCALE=full`) | 1,000,000 | 10,000 | 600 | **acceptance — hard floors** |
|
||||
|
||||
The fast/tiny profiles print `ADVISORY … NOT a merge-blocking acceptance run`
|
||||
and are labelled non-acceptance in `compliance_report.json`. Acceptance comes
|
||||
only from the merge profile, run by the merge-gates workflow. The merge floors
|
||||
cannot be lowered by environment overrides (a lowering override is recorded as a
|
||||
provenance failure and the floor kept).
|
||||
|
||||
### Merge-blocking enforcement (required check)
|
||||
|
||||
`.github/workflows/merge-gates.yml` defines the enforcement point. Configure
|
||||
branch protection / the merge queue to **require** the `merge-gates` job. That
|
||||
job runs the full merge profile, verifies the committed corpus has ≥10,000
|
||||
cases, and fails if any required artifact is missing. The full run executes
|
||||
~1M base executions × (1 base + 10 perturbations) with 100% reference/runtime
|
||||
comparison; it completes in minutes on a CI runner.
|
||||
|
||||
### Replay corpus
|
||||
|
||||
The replay corpus is committed at
|
||||
`crates/replay_corpus/corpus/replay_corpus.tsv` (10,000 cases). Replay loads
|
||||
those expectations and re-executes the reference, so any engine change that
|
||||
alters a hash makes the committed file and the fresh run disagree and CI fails.
|
||||
Regenerate it only as a deliberate, reviewed migration:
|
||||
|
||||
```bash
|
||||
cargo run --release -p replay_corpus --bin freeze -- 10000
|
||||
```
|
||||
|
||||
## Determinism
|
||||
|
||||
Everything is seed-derived and integer-only (SplitMix64 RNG, FNV-1a content
|
||||
hashing, wrapping/guarded arithmetic). No floating point enters a canonical
|
||||
hash, so replay is bit-exact across machines and runs. No external crates.
|
||||
|
||||
## The web game (plan2.md)
|
||||
|
||||
A browser game is built **around** the existing runtime — it is a playable
|
||||
window into the Rust universe, never a second simulation. The browser sends only
|
||||
*intent*; the server is the sole authority; every rune program executes through
|
||||
the **independent** interpreter (`runtime_under_test::native_resolve`) against
|
||||
the shared world. The game deliberately does **not** call the reference engine —
|
||||
the interpreter it uses is the one the runtime-equivalence gate proves correct
|
||||
(with a negative control proving that gate can fail). Same constraints as the
|
||||
rest of the repo: pure `std`, no external crates (the WebSocket server
|
||||
hand-rolls SHA-1, base64, and RFC 6455 framing; JSON is hand-rolled with a total
|
||||
parser).
|
||||
|
||||
> Audit note: the hand-rolled SHA-1 / base64 / RFC-6455 framing and JSON parser
|
||||
> are checked against published test vectors (RFC 6455 §1.3 accept key, SHA-1
|
||||
> "abc", base64 length cases) and a fuzz gate, but they are bespoke
|
||||
> cryptographic/parsing code and carry audit risk relative to a reviewed
|
||||
> library. They exist to honor the repo's no-external-crates rule; a future
|
||||
> hardening pass could swap in vetted implementations behind the same interface.
|
||||
|
||||
```
|
||||
Rust runtime → game_runtime (authority) → protocol (WS messages) → server → browser
|
||||
```
|
||||
|
||||
| Crate | Role |
|
||||
|-------|------|
|
||||
| `protocol` | Versioned, hashable, **total-decode** client/server messages + JSON value/parser. A malformed packet yields `Err`, never a panic. |
|
||||
| `game_runtime` | Authoritative match state. Resolves turns through the **independent interpreter** (`runtime_under_test`, not the reference engine), filters visibility/knowledge, records + regenerates replays. A match is a pure function of `(seed, roster, ordered inputs)`. |
|
||||
| `web_assets` | The embedded browser client (HTML/CSS/JS): arena, rune editor, domain/knowledge panels, replay viewer. |
|
||||
| `web_client` | Static-asset HTTP delivery (keeps raw assets separate from framing). |
|
||||
| `server` | `std::net` HTTP + WebSocket server: turn timer, action collection, disconnect handling, panic-proof dispatch. |
|
||||
| `web_tests` | A dependency-free WebSocket test client + the Phase H gates. |
|
||||
|
||||
### Running it
|
||||
|
||||
```bash
|
||||
cargo run --release -p server --bin magicka-server # serve on 127.0.0.1:8080
|
||||
# then open http://127.0.0.1:8080 in a browser
|
||||
MAGICKA_ADDR=0.0.0.0:9000 MAGICKA_TURN_MS=8000 cargo run --release -p server --bin magicka-server
|
||||
```
|
||||
|
||||
Join is immediate (1 player + a training dummy). A duel shares a match by id:
|
||||
two browsers that `JoinMatch` the same `match_id` take slots 1 and 2.
|
||||
|
||||
### Web CI gates (Phase H)
|
||||
|
||||
These gates are **merge-blocking**: they run inside the merge-required job in
|
||||
`.github/workflows/merge-gates.yml` (and as fast PR feedback in
|
||||
`web-gates.yml`). They are the Rust suite in `crates/web_tests`, run with
|
||||
`cargo test -p web_tests`:
|
||||
|
||||
| Gate | Test | Minimum | Status |
|
||||
|------|------|---------|--------|
|
||||
| Replay determinism | `determinism.rs` | 1,000 simulated matches, **0 hash mismatches** | merge-blocking |
|
||||
| Protocol fuzz | `fuzz.rs` | 10,000 fuzz cases, **0 panics** (+ a live server survives a malformed-packet burst) | merge-blocking |
|
||||
| End-to-end matches | `e2e.rs` | **100** full matches over real sockets; recorded replay reproduces every live per-turn hash | merge-blocking |
|
||||
| Hidden-state leaks | `visibility.rs` | **0 leaks** — no client-bound frame carries a hidden key; redaction counts every withheld value | merge-blocking |
|
||||
| Disconnect / timer edges | `resilience.rs` | mid-match disconnect does not corrupt the match; wrong-turn / late submits are rejected deterministically | merge-blocking |
|
||||
| Rendered-browser E2E | `e2e/specs/play.spec.js` | a real browser joins, casts, and replays a match | **external-blocked (advisory only)** |
|
||||
|
||||
Scope honesty — two distinct things, not conflated:
|
||||
|
||||
- The "100 E2E matches" merge-blocking gate drives the full
|
||||
HTTP→WebSocket→protocol→runtime path **headlessly over real sockets**. This is
|
||||
protocol-level coverage. It is **not** rendered-browser coverage and is not
|
||||
claimed as such.
|
||||
- Rendered-browser coverage is **blocked on CI infrastructure**: this CI has no
|
||||
real browser, so the Playwright suite under `crates/web_tests/e2e/` cannot be
|
||||
merge-blocking yet. It runs **advisory-only** (`continue-on-error`) in the
|
||||
`rendered-browser-e2e` job and uploads its report as an artifact. Until a CI
|
||||
runner with a browser exists, rendered-browser E2E is treated as
|
||||
**unsatisfied**, not green. Run it locally with:
|
||||
|
||||
```bash
|
||||
cd crates/web_tests/e2e && npm install && npx playwright install chromium && npm test
|
||||
```
|
||||
|
||||
### Acceptance criteria mapping (plan2.md)
|
||||
|
||||
| Criterion | Where it holds |
|
||||
|-----------|----------------|
|
||||
| A player can join a browser match | `server` join + `web_assets` client; `e2e.rs::single_match_full_playthrough` |
|
||||
| A turn timer runs | `server` timer thread; client header countdown |
|
||||
| Inspect / move / attack / cast | `Action` in `protocol`; `game_runtime::apply_action` |
|
||||
| Rune programs execute only on the server | `game_runtime` is the only caller of the interpreter (`runtime_under_test::native_resolve`); client never imports `EngineConfig` (asserted in `web_assets`) |
|
||||
| Results return as filtered observations | `VisibleWorldSnapshot`; `visibility.rs` |
|
||||
| Replay can reproduce the match | `game_runtime::replay`; `determinism.rs`, `e2e.rs` |
|
||||
| Browser cannot alter hidden truth | intent-only protocol; `visibility.rs` leak gate |
|
||||
| CI proves protocol, replay, visibility, authority | merge-blocking gates in `merge-gates.yml` (+ `web-gates.yml`); rendered-browser E2E remains external-blocked |
|
||||
|
||||
|
||||
|
||||
|
||||
=============
|
||||
Output
|
||||
=============
|
||||
All four directives are done and verified.
|
||||
|
||||
What changed
|
||||
|
||||
Committed — branch web-game, commit 9d9d5ce. Full workspace is green (every test passes, zero warnings); the
|
||||
claims are now in git and reproducible. I put it on a branch rather than main; fast-forward it when you're
|
||||
ready.
|
||||
|
||||
Removed reference-engine delegation. game_runtime no longer calls reference_runtime::execute. It now drives
|
||||
runtime_under_test::native_resolve — the independent interpreter that the runtime-equivalence gate proves
|
||||
correct (with a negative control proving that gate can fail). The grep confirms the only remaining
|
||||
reference_runtime use is the shared I/O contract types (ResolutionInput/canonical), not execution. So the
|
||||
game exercises an independent runtime, not a re-run of the reference.
|
||||
|
||||
Protocol/socket gates are merge-blocking. Added an explicit named step to the merge_group-required job in
|
||||
merge-gates.yml running the protocol + socket + replay/visibility/resilience suite (1k matches/0 drift, 10k
|
||||
fuzz/0 panics, 100 headless socket E2E, 0 leaks). web-gates.yml keeps the same suite as fast PR feedback.
|
||||
|
||||
Rendered-browser E2E is external-blocked, not satisfied. The Playwright job is renamed rendered-browser-e2e
|
||||
(ADVISORY — blocked on CI infra), set continue-on-error, and uploads its report as an artifact only. The
|
||||
README states plainly that until a CI runner with a browser exists, rendered-browser coverage is
|
||||
unsatisfied, and that the 100-match gate is protocol-level coverage — not a browser.
|
||||
|
||||
Two things I want to be straight about rather than let them read as resolved:
|
||||
|
||||
- The hand-rolled SHA-1/base64/RFC-6455/JSON code carries real audit risk. I checked it against published
|
||||
vectors and a fuzz gate and documented the risk in the README, but it's bespoke parsing/crypto written to
|
||||
honor the no-external-crates rule — not a substitute for a reviewed library. I did not eliminate that risk;
|
||||
I labeled it.
|
||||
- The independent interpreter is independent of the reference engine's code path, but both live in this repo
|
||||
and are proven equivalent by the same gate suite — so "independent runtime correctness" rests on that gate,
|
||||
not on a third-party oracle.
|
||||
|
||||
Reference in New Issue
Block a user