adv-accept: harness, run script and report skeleton
The adv-accept harness crate (draw-path check, accepted-program sweep over class v4, closed-form distinct and per-site ratio, plant hooks), the box-2 run script, and the Deliverable-2 report with the status board. Draw path validated (shared devnet epoch-0 id a785001687d8688a). The plant fires on (a'). The 10k-seed sweep is running on box 2. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This commit is contained in:
parent
abb6d51cca
commit
8423de3eb9
5 changed files with 391 additions and 0 deletions
63
docs/analysis/cryptanalysis/report-acceptance-rule.md
Normal file
63
docs/analysis/cryptanalysis/report-acceptance-rule.md
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
# Report: adversarial pass on the program acceptance rule (class v4 sub-version 3)
|
||||
|
||||
internal adversarial pass, not an independent review
|
||||
|
||||
- Target commit: 017e70376489251e18564c0abce7e466e606c8b3 (class v4 sub-version 3, object byte 7).
|
||||
- Crate built: igneum-pow at the frozen commit (this worktree's igneum-pow/ is reset to it; build/master
|
||||
diverged by 635 deletions and is not used). Harness: tools/attack/adv-accept (depends on igneum-pow by path).
|
||||
- Binary sha256: e3d35f4464937f91aac0648e2ee7134f33c85c7aa314b87b33f91059dedc6682
|
||||
- Box: igneum-build-2 (build class, nice 10, core band 0-31). Logs under /srv/builds/igneum-wt-adv-accept/adv/.
|
||||
- rustc 1.99.0 both sides. First results by 8 October 2026 18:00 BST. GPU: not available, so any per-card
|
||||
hash-rate confirmation of a gain is BLOCKED and said so.
|
||||
- Box-hours spent so far: about 0.1 (one 7 s build, three short runs). Budget 8.
|
||||
|
||||
## Draw-path validation (must pass before any claim)
|
||||
|
||||
The shared devnet epoch-0 class v4 program drawn through Epoch::chain_program(ProgramClass::V4) has
|
||||
program id a785001687d8688a at attempt 1 (class mx8-erad810f22d+sh256x27), which matches the frozen
|
||||
pack proto-cuda/packs-ca3-v4/v4-devnet-epoch0/program.json and the brief. So my draw path is the
|
||||
chain's. Command: `adv-accept derive-check` on box 2. Devnet 3 epoch-0 (id fce15bf61030be57) derive
|
||||
check is owed once I copy its program.json read-only from build-1.
|
||||
|
||||
## Status board
|
||||
|
||||
| Q | Method | Known-failed shape (must fire) | Gate | Result | Status |
|
||||
|---|---|---|---|---|---|
|
||||
| Q1 | Steering/hot set: draw accepted class v4 programs over >=10^6 seeds, measure the hot set of the 128 live loads per hash (share of reads on top 0.1% / 1% of items vs uniform) | f8 const-item / quarter-lines / half-lines plant must FLAG; clean control within noise | X_f >= f flags a hot set; gain = implied on-die SRAM copy size | closed-form proxy sweep (10k seeds) running; live-dataset histogram owed | RUNNING |
|
||||
| Q2 | Stand-in gap: compare the (c) metrics (distinct-address sum, saturation, bias, per-site ratio) on the closed form vs the live memory-hard dataset for accepted programs; count and bound false accepts | a hand-built closed-form-accept / live-reject program must be reported as such | any false accept that reads a hot set on the live set | not started (rides on Q1 cache) | PENDING |
|
||||
| Q3 | Attempt grinding + last resort: variance of the hot set across attempts of one seed vs across seeds; what last_resort_v4 (256-cap, or/mul/mulhi->xor, no (c) check) hands an attacker | the forced last-resort program's live hot set must be measurable; derive check fce15bf61030be57 | a predictable or weak accepted program the hot-set rule never sees | not started | PENDING |
|
||||
| Q4 | Header grinding for locality: vary H and nonce_hi (init words only), measure distinct DRAM rows / cache lines a 32-lane group touches, search cost vs clustering gain | a harness-mirror patch making the address depend on I must let the search find a clustering header; the real path must not | best clustering over a header budget, cost in hashes | not started | PENDING |
|
||||
| Q5 | Generator distinguishers: over accepted programs count lossy last writes, contractions, register-set collapse, low-entropy sites in the 0.98 tail; headroom of the floor | reproduce the crate's ratio verdict: p15/p18/p19/p56 rejected, p23 attempt 1 accepted | a structural shape that lowers the live distinct-item count | per-site ratio distribution in the 10k sweep; F8 reproduction owed | RUNNING |
|
||||
| Q6 | Fixed (c) sample grindability; live-size invariance of the (c) verdict | a program tuned to the 2,048 fixed nonces but failing off-sample must be found or bounded | BOUND unless something fires | not started | PENDING |
|
||||
|
||||
The plant (known-failed shape for the harness itself) fired: planting an `or` write of a load's
|
||||
source register immediately before the load makes the rule reject with "(a') load at 1 reads r4, not
|
||||
fresh by dataflow in the loop's steady state". So the harness reads the real rule, not a copy.
|
||||
Command: `adv-accept plant --seed 0` on box 2.
|
||||
|
||||
## Q1 and Q5: the accepted-program sweep (RUNNING)
|
||||
|
||||
Command (box 2, background): `adv-accept sweep --seeds 10000 --threads 32 --ratio-units 256 --out
|
||||
/srv/builds/igneum-wt-adv-accept/adv/sweep-10k.txt`. Log
|
||||
/srv/builds/igneum-wt-adv-accept/adv/sweep-10k.log, pid file beside it. Seeds: epoch bytes =
|
||||
LE words of seed_words_from_bytes("igneum-adv-accept/epoch/k"), era bytes of ".../era/k", for
|
||||
k = 0..9999; each drawn through the chain path generate_era(V4_CLASS, V3_ALLOWED), which runs the
|
||||
full attempt loop and the real acceptance rule.
|
||||
|
||||
Per accepted program the sweep records: attempt, program id, the closed-form distinct-item mean per
|
||||
hash (the rule's own (c) metric; 128 is ideal, the rule floor is a mean above 120), the minimum
|
||||
per-site distinct-index ratio at 256 units (the (c'') metric sampled cheaply; the enforced floor is
|
||||
0.98 at 2^20 units), the saturated-final count and the output-bias max.
|
||||
|
||||
This is the closed-form proxy for Q1 and the headroom characterization for Q5. The live-dataset hot
|
||||
set (the memory-hard cache, items derived into a table, the cross-hash histogram with the hot-set
|
||||
test) is the next run and is what the chip model prices; the closed-form distinct mean is a cheap
|
||||
upper bound on how concentrated an accepted program can be on the stand-in.
|
||||
|
||||
Numbers land here when the run finishes (first results by 8 October 18:00 BST).
|
||||
|
||||
## Running notes
|
||||
|
||||
- Box-hours and commands are logged in each section with the seed, so every claim is reproducible by
|
||||
re-running the exact command on box 2.
|
||||
- No cargo on the Mac. Pushes to the build mirror only. Commits as igneum-labs.
|
||||
14
tools/attack/adv-accept/Cargo.lock
generated
Normal file
14
tools/attack/adv-accept/Cargo.lock
generated
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 4
|
||||
|
||||
[[package]]
|
||||
name = "adv-accept"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"igneum-pow",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "igneum-pow"
|
||||
version = "0.2.0"
|
||||
21
tools/attack/adv-accept/Cargo.toml
Normal file
21
tools/attack/adv-accept/Cargo.toml
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
[package]
|
||||
name = "adv-accept"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
description = "Internal adversarial pass on the program acceptance rule and its generator (class v4 sub-version 3, frozen commit 017e7037): draw-path check, accepted-program sweep, closed-form distinct and per-site ratio, with plant hooks"
|
||||
license = "MIT"
|
||||
publish = false
|
||||
|
||||
[[bin]]
|
||||
name = "adv-accept"
|
||||
path = "src/main.rs"
|
||||
|
||||
[dependencies]
|
||||
igneum-pow = { path = "../../../igneum-pow" }
|
||||
|
||||
[workspace]
|
||||
|
||||
[profile.release]
|
||||
opt-level = 3
|
||||
lto = true
|
||||
codegen-units = 1
|
||||
14
tools/attack/adv-accept/run-box.sh
Normal file
14
tools/attack/adv-accept/run-box.sh
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
#!/usr/bin/env bash
|
||||
# Start a long adv-accept run on build box 2 under this lane's rules: nice 10, core band 0-31, a pid
|
||||
# file beside the log, logs under /srv/builds/igneum-wt-adv-accept/adv/. Run ON box 2, from the built
|
||||
# crate dir. Kill only by the pid file (kill "$(cat <log>.pid)"), never by name.
|
||||
# run-box.sh <tag> <adv-accept args...>
|
||||
set -euo pipefail
|
||||
tag="$1"; shift
|
||||
dir=/srv/builds/igneum-wt-adv-accept/adv
|
||||
mkdir -p "$dir"
|
||||
bin=/srv/builds/igneum-wt-adv-accept/tools/attack/adv-accept/target/release/adv-accept
|
||||
log="$dir/$tag.log"
|
||||
nohup nice -n 10 taskset -c 0-31 "$bin" "$@" > "$log" 2>&1 &
|
||||
echo $! > "$log.pid"
|
||||
echo "started pid $(cat "$log.pid"); log $log"
|
||||
279
tools/attack/adv-accept/src/main.rs
Normal file
279
tools/attack/adv-accept/src/main.rs
Normal file
|
|
@ -0,0 +1,279 @@
|
|||
//! adv-accept: internal adversarial pass on the program acceptance rule and its generator
|
||||
//! (class v4 sub-version 3, frozen commit 017e7037). Nothing in igneum-pow is modified; every draw,
|
||||
//! the acceptance rule and the per-site ratio are the library's, reached through the public API.
|
||||
//!
|
||||
//! Commands:
|
||||
//! adv-accept derive-check
|
||||
//! The draw-path smoke test: the shared devnet epoch-0 class v4 program id must be
|
||||
//! a785001687d8688a (attempt 1). If a copied Devnet 3 program.json is given, its id must be
|
||||
//! fce15bf61030be57 (attempt 0). A mismatch means the draw path is wrong and nothing else counts.
|
||||
//! adv-accept sweep --seeds N [--threads T] [--ratio-units U] [--out FILE]
|
||||
//! Draw the chain's class v4 program for N epoch/era seed pairs (generate_era over V4_CLASS,
|
||||
//! the full attempt loop and the real acceptance rule), then on each accepted program record:
|
||||
//! the attempt, the closed-form distinct-item mean (the rule's own (c) metric, 128 is ideal),
|
||||
//! the min per-site distinct-index ratio at U evaluations per site (the (c'') metric; the floor
|
||||
//! is 0.98 at 2^20), the saturated count and the bias max. Reports the distribution and the
|
||||
//! worst (lowest distinct-mean, lowest ratio) seeds: the closed-form proxy for Q1/Q5.
|
||||
//! adv-accept plant [--seed S]
|
||||
//! The known-failed shape: take an accepted program and put one load's source back onto a
|
||||
//! lossily-written register; the rule MUST now reject it (UnfreshLoadSource, or the ratio).
|
||||
//! If the rule does not fire, the harness is not reading the rule and the sweep is void.
|
||||
|
||||
use igneum_pow::accept::{check, distinct_ratio_pass, AcceptReport, Reject, ACCEPT_DATASET_LOG2, MIN_DISTINCT_RATIO_V4};
|
||||
use igneum_pow::bind::{hex, unhex};
|
||||
use igneum_pow::generator::{generate_era, Op, Program, ProgramClass, V3_ALLOWED, V4_CLASS};
|
||||
use igneum_pow::seed::seed_words_from_bytes;
|
||||
use igneum_pow::verify::Epoch;
|
||||
use std::io::Write;
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
use std::time::Instant;
|
||||
|
||||
const GENESIS_HEX: &str = "edc4fa844da9dc98d37e965176f6558a31560e40502ab3ae5491b21aaaabfb07";
|
||||
|
||||
/// 32 epoch/era bytes for sweep index k: the little-endian words of a label-derived seed, as the
|
||||
/// attack-pass F8 harness builds its chain-shaped seeds.
|
||||
fn seed_bytes(tag: &str, k: u64) -> Vec<u8> {
|
||||
seed_words_from_bytes(format!("igneum-adv-accept/{tag}/{k}").as_bytes())
|
||||
.iter()
|
||||
.flat_map(|x| x.to_le_bytes())
|
||||
.collect()
|
||||
}
|
||||
|
||||
/// The chain's class v4 program of an (epoch, era) seed pair: the full attempt loop and the real
|
||||
/// acceptance rule inside generate_era. Returns an accepted program (or the last resort if a seed
|
||||
/// exhausts its 256 attempts, which a sweep never reaches).
|
||||
fn chain_v4(label: &str, epoch: &[u8], era: &[u8]) -> Program {
|
||||
generate_era(label, epoch, V4_CLASS, era, &V3_ALLOWED)
|
||||
}
|
||||
|
||||
fn derive_check(args: &[String]) {
|
||||
let g = unhex(GENESIS_HEX).unwrap();
|
||||
// The shared devnet's epoch 0: epoch seed and era seed are both the genesis hash (the F8 harness's p1).
|
||||
let p = Epoch::chain_program(&g, Some(&g), ProgramClass::V4, "p1-devnet-epoch0");
|
||||
let id = p.program_id();
|
||||
let want = 0xa785001687d8688au64;
|
||||
println!(
|
||||
"shared devnet epoch 0: generator {} attempt {} program id {:016x} (want a785001687d8688a) class {} -> {}",
|
||||
p.generator,
|
||||
p.attempt,
|
||||
id,
|
||||
p.class.name(),
|
||||
if id == want { "OK" } else { "MISMATCH" }
|
||||
);
|
||||
assert_eq!(id, want, "the draw path is wrong: shared devnet epoch-0 id mismatch");
|
||||
assert_eq!(p.generator, 4);
|
||||
assert!(check(&p).is_ok(), "the shared devnet program must pass the rule");
|
||||
// Optional Devnet 3 check: a copied program.json path as the only extra argument.
|
||||
if let Some(path) = args.iter().find(|a| a.ends_with(".json")) {
|
||||
match std::fs::read_to_string(path) {
|
||||
Ok(text) => {
|
||||
let field = |k: &str| -> Option<String> {
|
||||
let pat = format!("\"{k}\"");
|
||||
let i = text.find(&pat)?;
|
||||
let rest = &text[i + pat.len()..];
|
||||
let c = rest.find(':')?;
|
||||
let after = rest[c + 1..].trim_start();
|
||||
let after = after.trim_start_matches('"');
|
||||
let end = after.find(|ch| ch == '"' || ch == ',' || ch == '}')?;
|
||||
Some(after[..end].trim().trim_matches('"').to_string())
|
||||
};
|
||||
let epoch = unhex(&field("seed_bytes").expect("seed_bytes")).expect("hex seed");
|
||||
let era = unhex(&field("era_seed_bytes").expect("era_seed_bytes")).expect("hex era");
|
||||
let p3 = Epoch::chain_program(&epoch, Some(&era), ProgramClass::V4, "p-devnet3-epoch0");
|
||||
let id3 = p3.program_id();
|
||||
println!(
|
||||
"devnet 3 epoch 0: epoch {} era {} attempt {} program id {:016x} (want fce15bf61030be57) -> {}",
|
||||
hex(&epoch),
|
||||
hex(&era),
|
||||
p3.attempt,
|
||||
id3,
|
||||
if id3 == 0xfce15bf61030be57 { "OK" } else { "MISMATCH" }
|
||||
);
|
||||
assert_eq!(id3, 0xfce15bf61030be57, "devnet 3 epoch-0 id mismatch");
|
||||
}
|
||||
Err(e) => println!("devnet 3 program.json not readable ({e}); shared-devnet check alone"),
|
||||
}
|
||||
}
|
||||
println!("derive-check: PASS");
|
||||
}
|
||||
|
||||
struct Row {
|
||||
k: u64,
|
||||
attempt: u32,
|
||||
id: u64,
|
||||
distinct_mean: f64,
|
||||
min_ratio: f64,
|
||||
min_ratio_site: usize,
|
||||
saturated: u32,
|
||||
bias_max: u32,
|
||||
last_resort: bool,
|
||||
}
|
||||
|
||||
fn sweep(args: &[String]) {
|
||||
let get = |k: &str, d: &str| -> String {
|
||||
args.windows(2).find(|w| w[0] == k).map(|w| w[1].clone()).unwrap_or_else(|| d.to_string())
|
||||
};
|
||||
let seeds: u64 = get("--seeds", "1000").parse().unwrap();
|
||||
let threads: usize = get("--threads", "12").parse().unwrap();
|
||||
let ratio_units: usize = get("--ratio-units", "256").parse().unwrap();
|
||||
let out = get("--out", "");
|
||||
println!(
|
||||
"adv-accept sweep: {seeds} seeds, {threads} threads, ratio at {ratio_units} units per site (floor {MIN_DISTINCT_RATIO_V4} at 2^20, dataset 2^{ACCEPT_DATASET_LOG2})"
|
||||
);
|
||||
let t0 = Instant::now();
|
||||
let next = AtomicUsize::new(0);
|
||||
let rows: Vec<Vec<Row>> = std::thread::scope(|sc| {
|
||||
let mut hs = Vec::new();
|
||||
for _ in 0..threads {
|
||||
let next = &next;
|
||||
hs.push(sc.spawn(move || {
|
||||
let mut out = Vec::new();
|
||||
loop {
|
||||
let k = next.fetch_add(1, Ordering::Relaxed) as u64;
|
||||
if k >= seeds {
|
||||
break;
|
||||
}
|
||||
let epoch = seed_bytes("epoch", k);
|
||||
let era = seed_bytes("era", k);
|
||||
let label = format!("igneum-adv-accept/{k}");
|
||||
let p = chain_v4(&label, &epoch, &era);
|
||||
let verdict = check(&p);
|
||||
let last_resort = verdict.is_err();
|
||||
let report = verdict.unwrap_or(AcceptReport::default());
|
||||
// the min per-site distinct-index ratio at `ratio_units` (cheap; floor 0 so it never errs)
|
||||
let (min_ratio, min_site) = distinct_ratio_pass(&p, ratio_units, 0.0).unwrap_or((f64::NAN, 0));
|
||||
out.push(Row {
|
||||
k,
|
||||
attempt: p.attempt,
|
||||
id: p.program_id(),
|
||||
distinct_mean: report.distinct_mean(),
|
||||
min_ratio,
|
||||
min_ratio_site: min_site,
|
||||
saturated: report.saturated,
|
||||
bias_max: report.bias_max,
|
||||
last_resort,
|
||||
});
|
||||
}
|
||||
out
|
||||
}));
|
||||
}
|
||||
hs.into_iter().map(|h| h.join().unwrap()).collect()
|
||||
});
|
||||
let mut all: Vec<Row> = rows.into_iter().flatten().collect();
|
||||
let n = all.len();
|
||||
let el = t0.elapsed().as_secs_f64();
|
||||
let mean_attempt = all.iter().map(|r| r.attempt as f64).sum::<f64>() / n as f64;
|
||||
let max_attempt = all.iter().map(|r| r.attempt).max().unwrap_or(0);
|
||||
let last_resorts = all.iter().filter(|r| r.last_resort).count();
|
||||
let dmean = all.iter().map(|r| r.distinct_mean).sum::<f64>() / n as f64;
|
||||
let dmin = all.iter().map(|r| r.distinct_mean).fold(f64::MAX, f64::min);
|
||||
let rmean = all.iter().map(|r| r.min_ratio).sum::<f64>() / n as f64;
|
||||
let rmin = all.iter().map(|r| r.min_ratio).fold(f64::MAX, f64::min);
|
||||
let below_floor = all.iter().filter(|r| r.min_ratio < MIN_DISTINCT_RATIO_V4).count();
|
||||
println!(
|
||||
"swept {n} seeds in {el:.1} s ({:.1} seeds/s/thread); attempts mean {mean_attempt:.3} max {max_attempt}; last-resort programs {last_resorts}",
|
||||
n as f64 / el * threads as f64
|
||||
);
|
||||
println!(
|
||||
"closed-form distinct-item mean per hash: mean {dmean:.4} min {dmin:.4} (ideal 128, rule floor mean > 120)"
|
||||
);
|
||||
println!(
|
||||
"per-site distinct-index ratio at {ratio_units} units: mean {rmean:.4} min {rmin:.4}; {below_floor} of {n} below the 0.98 floor at this sample size (the floor is enforced at 2^20)"
|
||||
);
|
||||
all.sort_by(|a, b| a.distinct_mean.partial_cmp(&b.distinct_mean).unwrap());
|
||||
println!("lowest closed-form distinct-item mean (Q1/Q5 proxy):");
|
||||
for r in all.iter().take(10) {
|
||||
println!(
|
||||
" seed {} id {:016x} attempt {} distinct_mean {:.4} min_ratio {:.4} (site {}) saturated {} bias_max {}",
|
||||
r.k, r.id, r.attempt, r.distinct_mean, r.min_ratio, r.min_ratio_site, r.saturated, r.bias_max
|
||||
);
|
||||
}
|
||||
all.sort_by(|a, b| a.min_ratio.partial_cmp(&b.min_ratio).unwrap());
|
||||
println!("lowest per-site distinct-index ratio (headroom over the floor, Q5):");
|
||||
for r in all.iter().take(10) {
|
||||
println!(
|
||||
" seed {} id {:016x} attempt {} min_ratio {:.4} (site {}) distinct_mean {:.4}",
|
||||
r.k, r.id, r.attempt, r.min_ratio, r.min_ratio_site, r.distinct_mean
|
||||
);
|
||||
}
|
||||
if !out.is_empty() {
|
||||
let mut f = std::fs::File::create(&out).unwrap();
|
||||
writeln!(f, "# seed attempt program_id distinct_mean min_ratio min_ratio_site saturated bias_max last_resort").unwrap();
|
||||
all.sort_by_key(|r| r.k);
|
||||
for r in &all {
|
||||
writeln!(
|
||||
f,
|
||||
"{} {} {:016x} {:.5} {:.5} {} {} {} {}",
|
||||
r.k, r.attempt, r.id, r.distinct_mean, r.min_ratio, r.min_ratio_site, r.saturated, r.bias_max, r.last_resort as u8
|
||||
)
|
||||
.unwrap();
|
||||
}
|
||||
println!("wrote {out}");
|
||||
}
|
||||
println!("sweep DONE");
|
||||
}
|
||||
|
||||
/// The known-failed shape: an accepted program, then one load's source put onto a register the
|
||||
/// program writes with a lossy op (or/mul/mulhi) and nothing fresh after, so the source is not fresh
|
||||
/// by dataflow. The rule MUST reject it. This shows the harness reads the real rule firing.
|
||||
fn plant(args: &[String]) {
|
||||
let get = |k: &str, d: &str| -> String {
|
||||
args.windows(2).find(|w| w[0] == k).map(|w| w[1].clone()).unwrap_or_else(|| d.to_string())
|
||||
};
|
||||
let s: u64 = get("--seed", "0").parse().unwrap();
|
||||
let epoch = seed_bytes("epoch", s);
|
||||
let era = seed_bytes("era", s);
|
||||
let p = chain_v4(&format!("igneum-adv-accept/{s}"), &epoch, &era);
|
||||
assert!(check(&p).is_ok(), "seed {s} is accepted as drawn");
|
||||
println!("seed {s}: accepted, id {:016x} attempt {}", p.program_id(), p.attempt);
|
||||
// Known-failed shape: find a load at position `pos` (not at instr 0) and write its source
|
||||
// register with an `or` in the instruction immediately before it, with nothing between to
|
||||
// refresh it. `or` is never fresh by dataflow, so the load's source is not fresh in the loop's
|
||||
// steady state and the rule MUST reject (a'), unless an earlier check (a)/(b) fires first.
|
||||
let load_pos = p.instrs.iter().position(|i| i.op == Op::Load && i.src != 0).filter(|&pos| pos >= 1);
|
||||
match load_pos {
|
||||
Some(pos) => {
|
||||
let src = p.instrs[pos].src;
|
||||
let mut q = p.clone();
|
||||
// the instruction just before the load becomes `or dst=src, src=other` (src != dst)
|
||||
let other = (src + 1) % 8;
|
||||
q.instrs[pos - 1].op = Op::Or;
|
||||
q.instrs[pos - 1].dst = src;
|
||||
q.instrs[pos - 1].src = other;
|
||||
let v = check(&q);
|
||||
println!(
|
||||
"planted: instr {} -> or r{src} |= r{other} (lossy), load at instr {pos} reads r{src}; rule says {:?}",
|
||||
pos - 1,
|
||||
v.as_ref().err().map(|r| r.to_string())
|
||||
);
|
||||
assert!(v.is_err(), "the rule did not reject the planted not-fresh load source: the harness is not reading the rule");
|
||||
// the finding we want is specifically the dataflow rule, but an earlier part firing is still the rule working
|
||||
println!(
|
||||
"plant: the rule FIRED ({}) on the planted weakness; harness reads the real rule",
|
||||
match v {
|
||||
Err(Reject::UnfreshLoadSource { .. }) => "(a') unfresh load source, the intended part",
|
||||
Err(_) => "an earlier part",
|
||||
Ok(_) => unreachable!(),
|
||||
}
|
||||
);
|
||||
}
|
||||
None => println!("seed {s}: no distinct load past instr 0 to plant; try another --seed"),
|
||||
}
|
||||
}
|
||||
|
||||
fn main() {
|
||||
let args: Vec<String> = std::env::args().collect();
|
||||
if args.len() < 2 {
|
||||
eprintln!("adv-accept <derive-check|sweep|plant> [args]");
|
||||
std::process::exit(2);
|
||||
}
|
||||
match args[1].as_str() {
|
||||
"derive-check" => derive_check(&args[2..]),
|
||||
"sweep" => sweep(&args[2..]),
|
||||
"plant" => plant(&args[2..]),
|
||||
_ => {
|
||||
eprintln!("unknown command {}", args[1]);
|
||||
std::process::exit(2);
|
||||
}
|
||||
}
|
||||
}
|
||||
Loading…
Reference in a new issue