Audit pass: full-corpus evidence, full-gate mutation, 3-way metamorphic, recomputable causal, bundle attestation
1 (artifact bundle): ci_reports writes evidence/MANIFEST.tsv (content hash+len of every evidence file); attestation verifies completeness+integrity; merge-gates requires the bundle. 2 (every leaf full evidence): run_all_to streams a full trace+delta record for EVERY leaf (base 'b' and perturbation 'p'), not a sample. 3 (attestation completeness): attestation enforces a leaf<->trace bijection (traces == leaves and covered set == leaf set), not just consistency. 4 (collapse derives from full traces): trace_feature_row single-sourced into collapse_analysis; attestation recomputes each collapse row from the retained full trace and requires bit-exact match. 5 (mutants through full gates): evaluate_mutants runs each mutant through engine_acceptance over 128 generated cases (trace/equivalence/domain/ metamorphic/causal), replacing the 64-input local predicates. 6 (trace+delta+future): metamorphic enforces consumed->trace per-case plus consumed-aggregate delta (>=0.65) and future (>=0.80) rates. 7 (recomputable causal): per-edge intervention records written to evidence/causal_evidence.tsv; attestation RE-EXECUTES each from its seed and recomputes base_dv/alt_dv. 8 (no string/comment proof): removed web_assets JS-substring test and the tautological string assert in ci_reports. Verified at fast scale end-to-end: 6600/6600 traces reconstructed, leaf bijection, 1600/1600 causal records recomputed, 600/600 collapse rows derived, bundle intact. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
Claude Opus 4.8
@@ -15,3 +15,8 @@ path = "src/main.rs"
|
||||
# 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" }
|
||||
|
||||
+283
-18
@@ -17,10 +17,57 @@
|
||||
//! 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};
|
||||
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
|
||||
@@ -68,13 +115,17 @@ fn claim<'a>(claims: &'a [(String, String)], key: &str) -> Option<&'a str> {
|
||||
/// delta + seeds, independently of any reported digest. Returns the recomputed
|
||||
/// leaf, or `None` if the record is malformed.
|
||||
///
|
||||
/// `line` is `ws ps cs prs future leaf <TAB> <trace> <TAB> <delta>`.
|
||||
pub fn recompute_trace_leaf(line: &str) -> Option<(u64, u64)> {
|
||||
/// `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())?;
|
||||
@@ -95,7 +146,7 @@ pub fn recompute_trace_leaf(line: &str) -> Option<(u64, u64)> {
|
||||
delta_hash: delta.hash(),
|
||||
future_hash: Hash(future),
|
||||
};
|
||||
Some((rr.hash().0, claimed_leaf))
|
||||
Some((rr.hash().0, claimed_leaf, is_base))
|
||||
}
|
||||
|
||||
/// Outcome of an attestation.
|
||||
@@ -107,6 +158,11 @@ pub struct Attestation {
|
||||
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)>,
|
||||
}
|
||||
|
||||
@@ -147,26 +203,174 @@ pub fn verify_dir(dir: &Path) -> Result<Attestation, String> {
|
||||
.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;
|
||||
match recompute_trace_leaf(line) {
|
||||
Some((recomputed_leaf, claimed_leaf)) => {
|
||||
if recomputed_leaf == claimed_leaf && leaf_set.contains(&recomputed_leaf) {
|
||||
traces_verified += 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);
|
||||
}
|
||||
None => {}
|
||||
}
|
||||
}
|
||||
let traces_present = traces_total > 0;
|
||||
checks.push(("full-trace evidence present".into(), traces_present));
|
||||
checks.push((
|
||||
"every sampled full trace recomputes to a retained leaf".into(),
|
||||
"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 {
|
||||
@@ -176,6 +380,11 @@ pub fn verify_dir(dir: &Path) -> Result<Attestation, String> {
|
||||
claimed_root,
|
||||
traces_verified,
|
||||
traces_total,
|
||||
causal_total,
|
||||
causal_recomputed,
|
||||
causal_confirmed,
|
||||
collapse_total,
|
||||
collapse_derived,
|
||||
checks,
|
||||
})
|
||||
}
|
||||
@@ -227,12 +436,14 @@ mod tests {
|
||||
}
|
||||
|
||||
fn sample_delta(seed: u64) -> WorldDelta {
|
||||
let mut observed = [0i64; LANES];
|
||||
observed[0] = seed as i64;
|
||||
WorldDelta {
|
||||
domain_deltas: vec![DomainDelta { domain: DomainId(2), observed, hidden: [0i64; HIDDEN_LANES] }],
|
||||
turn_advance: 0,
|
||||
}
|
||||
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) {
|
||||
@@ -280,12 +491,66 @@ mod tests {
|
||||
trace_s = trace_s.replacen("trace-v1 ", "trace-v1 999 ", 1);
|
||||
}
|
||||
traces.push_str(&format!(
|
||||
"{:016x} {:016x} {:016x} {:016x} {:016x} {:016x}\t{}\t{}\n",
|
||||
"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]
|
||||
|
||||
@@ -22,6 +22,14 @@ fn main() {
|
||||
" 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);
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user