|
| 1 | +//! Replay the D-TFLP 6.5 softmax fixtures. Usage: replay FIXTURE_DIR [--reciprocal source|exact] [--full] |
| 2 | +//! |
| 3 | +//! Order: manifest digests (integrity) → each table's digest → each fixture. The reduced suite runs by |
| 4 | +//! default; `--full` adds the complete 529-witness tier. Exit status 0 only if every check passes. |
| 5 | +//! `--reciprocal exact` is the negative control: the witnesses must then fail and the |
| 6 | +//! calibration-9 equivalence rows must still pass. |
| 7 | +use replay::*; |
| 8 | +use serde_json::Value; |
| 9 | +use sha2::{Digest, Sha256}; |
| 10 | +use std::{collections::BTreeMap, fs, path::Path, process::ExitCode}; |
| 11 | + |
| 12 | +fn hex(b: &[u8]) -> String { |
| 13 | + b.iter().map(|x| format!("{x:02x}")).collect() |
| 14 | +} |
| 15 | + |
| 16 | +fn table(v: &Value) -> Table { |
| 17 | + let arr = |k: &str| v[k].as_array().unwrap().iter().map(|x| x.as_i64().unwrap()).collect::<Vec<_>>(); |
| 18 | + let (adm, a, b) = (arr("admitted"), arr("A"), arr("B")); |
| 19 | + let mut t = Table { admitted: [false; 256], a: [0; 256], b: [0; 256] }; |
| 20 | + for i in 0..256 { |
| 21 | + t.admitted[i] = adm[i] == 1; |
| 22 | + t.a[i] = a[i] as i32; |
| 23 | + t.b[i] = b[i] as i32; |
| 24 | + } |
| 25 | + t |
| 26 | +} |
| 27 | + |
| 28 | +fn row_pairs(v: &Value) -> Vec<(i32, i32)> { |
| 29 | + match v { |
| 30 | + Value::Object(m) => m.iter().map(|(k, n)| (k.parse().unwrap(), n.as_i64().unwrap() as i32)).collect(), |
| 31 | + Value::Array(a) => { |
| 32 | + let mut c: BTreeMap<i32, i32> = BTreeMap::new(); |
| 33 | + for x in a { |
| 34 | + *c.entry(x.as_i64().unwrap() as i32).or_default() += 1; |
| 35 | + } |
| 36 | + c.into_iter().collect() |
| 37 | + } |
| 38 | + _ => panic!("row"), |
| 39 | + } |
| 40 | +} |
| 41 | + |
| 42 | +fn main() -> ExitCode { |
| 43 | + let args: Vec<String> = std::env::args().collect(); |
| 44 | + let dir = Path::new(&args[1]); |
| 45 | + let recip = if args.iter().any(|a| a == "exact") { Recip::Exact } else { Recip::Source }; |
| 46 | + let full = args.iter().any(|a| a == "--full"); |
| 47 | + let mut fails: Vec<String> = Vec::new(); |
| 48 | + let t0 = std::time::Instant::now(); |
| 49 | + // 1. integrity |
| 50 | + let man: Value = serde_json::from_str(&fs::read_to_string(dir.join("manifest65.json")).unwrap()).unwrap(); |
| 51 | + for (name, want) in man["sha256"].as_object().unwrap() { |
| 52 | + let got = hex(&Sha256::digest(fs::read(dir.join(name)).unwrap())); |
| 53 | + if &got != want.as_str().unwrap() { |
| 54 | + fails.push(format!("integrity {name}")); |
| 55 | + } |
| 56 | + } |
| 57 | + if !fails.is_empty() { |
| 58 | + println!("REFUSE integrity: {fails:?}"); |
| 59 | + return ExitCode::from(2); |
| 60 | + } |
| 61 | + let t_integrity = t0.elapsed(); |
| 62 | + // 2. tables |
| 63 | + let tj: Value = serde_json::from_str(&fs::read_to_string(dir.join("softmax_tables65.json")).unwrap()).unwrap(); |
| 64 | + let mut tables: BTreeMap<String, Table> = BTreeMap::new(); |
| 65 | + for (key, t) in tj["tables"].as_object().unwrap() { |
| 66 | + let d = hex(&Sha256::digest(serde_json::to_string(t).unwrap())); |
| 67 | + if d != tj["sha256"][key].as_str().unwrap() { |
| 68 | + fails.push(format!("table digest {key}")); |
| 69 | + } |
| 70 | + tables.insert(key.clone(), table(t)); |
| 71 | + } |
| 72 | + let t_tables = t0.elapsed() - t_integrity; |
| 73 | + // 3. fixtures |
| 74 | + let lines = |f: &str| fs::read_to_string(dir.join(f)).unwrap().lines().map(|l| serde_json::from_str::<Value>(l).unwrap()).collect::<Vec<_>>(); |
| 75 | + let mut ok = BTreeMap::<&str, u32>::new(); |
| 76 | + let mut check_w = |name: &'static str, ws: &[Value], fails: &mut Vec<String>| { |
| 77 | + for w in ws { |
| 78 | + let id = w["id"].as_str().unwrap(); |
| 79 | + let key = w["table"].as_str().unwrap(); |
| 80 | + if tj["sha256"][key] != w["table_sha256"] { |
| 81 | + fails.push(format!("{name} {id}: table_sha256")); |
| 82 | + continue; |
| 83 | + } |
| 84 | + // the calibration identity the witness claims must be the one its table was prepared for |
| 85 | + let claimed = format!("{}:{}", w["scale_bits"].as_str().unwrap_or(""), w["beta_bits"].as_str().unwrap_or("")); |
| 86 | + if claimed != key || tj["tables"][key]["scale_bits"].as_str() != w["scale_bits"].as_str() { |
| 87 | + fails.push(format!("{name} {id}: calibration identity {claimed} != table {key}")); |
| 88 | + continue; |
| 89 | + } |
| 90 | + let t = &tables[key]; |
| 91 | + let row = row_pairs(&w["row"]); |
| 92 | + let d = w["d"].as_i64().unwrap() as i32; |
| 93 | + let r = (|| -> Result<(), String> { |
| 94 | + // differences are relative to code 127: the row maximum is mandatory |
| 95 | + if row.iter().map(|&(c, _)| c).max() != Some(127) { |
| 96 | + return Err("no mandatory maximum (code 127)".into()); |
| 97 | + } |
| 98 | + let s = row_sum(t, &row).map_err(|e| e.to_string())?; |
| 99 | + if s != w["S"].as_i64().unwrap() { |
| 100 | + return Err(format!("sum {s} != stored S")); |
| 101 | + } |
| 102 | + if !row.iter().any(|&(c, _)| c == 127 + d) { |
| 103 | + return Err("no element at d".into()); |
| 104 | + } |
| 105 | + let bs = byte_of(t, &row, 127 + d, recip).map_err(|e| e.to_string())?; |
| 106 | + let bx = byte_of(t, &row, 127 + d, Recip::Exact).map_err(|e| e.to_string())?; |
| 107 | + if i64::from(bs) != w["byte_source"].as_i64().unwrap() || i64::from(bs) != w["kernel_byte"].as_i64().unwrap() { |
| 108 | + return Err(format!("source byte {bs} != stored")); |
| 109 | + } |
| 110 | + if i64::from(bx) != w["byte_exact"].as_i64().unwrap() || bs == bx { |
| 111 | + return Err(format!("exact byte {bx}")); |
| 112 | + } |
| 113 | + Ok(()) |
| 114 | + })(); |
| 115 | + match r { |
| 116 | + Ok(()) => *ok.entry(name).or_default() += 1, |
| 117 | + Err(e) => fails.push(format!("{name} {id}: {e}")), |
| 118 | + } |
| 119 | + } |
| 120 | + }; |
| 121 | + check_w("reduced", &lines("witness65_reduced.jsonl"), &mut fails); |
| 122 | + if full { |
| 123 | + check_w("full", &lines("witness65_full.jsonl"), &mut fails); |
| 124 | + } |
| 125 | + for e in lines("equivalence65.jsonl") { |
| 126 | + let t = &tables[e["table"].as_str().unwrap()]; |
| 127 | + let codes: Vec<i32> = e["row"].as_array().unwrap().iter().map(|x| x.as_i64().unwrap() as i32).collect(); |
| 128 | + let row = row_pairs(&e["row"]); |
| 129 | + let want: Vec<i64> = e["kernel_bytes"].as_array().unwrap().iter().map(|x| x.as_i64().unwrap()).collect(); |
| 130 | + let got: Result<Vec<i64>, Refusal> = codes.iter().map(|&c| byte_of(t, &row, c, recip).map(i64::from)).collect(); |
| 131 | + let got_x: Result<Vec<i64>, Refusal> = codes.iter().map(|&c| byte_of(t, &row, c, Recip::Exact).map(i64::from)).collect(); |
| 132 | + if got.as_ref() == Ok(&want) && got_x.as_ref() == Ok(&want) { |
| 133 | + *ok.entry("equivalence").or_default() += 1; |
| 134 | + } else { |
| 135 | + fails.push(format!("equivalence {}", e["id"])); |
| 136 | + } |
| 137 | + } |
| 138 | + for u in lines("unreachable65.jsonl") { |
| 139 | + let t = &tables[u["table"].as_str().unwrap()]; |
| 140 | + let (s, d) = (u["S"].as_i64().unwrap(), u["d"].as_i64().unwrap() as i32); |
| 141 | + let r = s - i64::from(t.b[255]) - if d != 0 { i64::from(t.b[(d + 255) as usize]) } else { 0 }; |
| 142 | + let proved = match u["status"].as_str().unwrap() { |
| 143 | + "unreachable_negative" => r < 0, |
| 144 | + _ => r >= 0 && r <= 4_000_000 && !representable(t, r as usize), |
| 145 | + }; |
| 146 | + if proved { |
| 147 | + *ok.entry("unreachable").or_default() += 1; |
| 148 | + } else { |
| 149 | + fails.push(format!("unreachable S={s} d={d}")); |
| 150 | + } |
| 151 | + } |
| 152 | + let t_total = t0.elapsed(); |
| 153 | + eprintln!("timing_us integrity={} tables={} fixtures={} total={}", t_integrity.as_micros(), t_tables.as_micros(), (t_total - t_integrity - t_tables).as_micros(), t_total.as_micros()); |
| 154 | + println!("recip={recip:?} passed={ok:?} failures={}", fails.len()); |
| 155 | + for f in fails.iter().take(10) { |
| 156 | + println!(" {f}"); |
| 157 | + } |
| 158 | + if fails.is_empty() { ExitCode::SUCCESS } else { ExitCode::from(1) } |
| 159 | +} |
| 160 | + |
| 161 | +/// Plain unbounded-coin DP over the admitted weights: is r a non-negative combination? |
| 162 | +fn representable(t: &Table, r: usize) -> bool { |
| 163 | + let coins: Vec<usize> = (0..256).filter(|&i| t.admitted[i] && t.b[i] > 0).map(|i| t.b[i] as usize).collect(); |
| 164 | + let mut rep = vec![false; r + 1]; |
| 165 | + rep[0] = true; |
| 166 | + for x in 1..=r { |
| 167 | + rep[x] = coins.iter().any(|&c| c <= x && rep[x - c]); |
| 168 | + } |
| 169 | + rep[r] |
| 170 | +} |
0 commit comments