//! The `proof` headline is like for like. "For the same verified output" must //! compare the cascade's whole spend with a frontier-only run charged ONLY for //! the goals the cascade proved; the all-goals baseline, which also charges //! goals nothing proved here, is printed with its goal count and never called //! the same output. Every figure is checked against the per-goal rows the same //! run printed, with the tests' own arithmetic: the frontier-only cost of a //! goal is 50 J (50,000,000 uJ, T3's nominal cost), and a ratio is printed in //! thousandths, rounded down. use std::process::Command; /// T3's nominal cost, the frontier-only charge per goal: the tests' own literal. const FRONTIER_UJ: u64 = 50_000_000; /// The text between `before` and `after` on `line`. fn between<'a>(line: &'a str, before: &str, after: &str) -> &'a str { let at = line.find(before).unwrap_or_else(|| panic!("no {before:?} in {line:?}")) + before.len(); let rest = &line[at..]; &rest[..rest.find(after).unwrap_or_else(|| panic!("no {after:?} after {before:?} in {line:?}"))] } fn num(s: &str) -> u64 { s.trim().parse().unwrap_or_else(|_| panic!("not a number: {s:?}")) } /// A ratio as printed: `.<3 digits>`, back to thousandths. fn milli(s: &str) -> u64 { let (int, frac) = s.split_once('.').unwrap_or_else(|| panic!("not a ratio: {s:?}")); assert_eq!(frac.len(), 3, "a ratio not in thousandths: {s:?}"); num(int) * 1000 + num(frac) } #[test] fn the_same_output_headline_charges_the_baseline_only_for_proved_goals() { let out = Command::new(env!("CARGO_BIN_EXE_proof")).output().expect("the proof binary runs"); let stdout = String::from_utf8_lossy(&out.stdout); assert!(out.status.success(), "proof exited {:?}\n{stdout}", out.status); // The per-goal rows: tier (or `unproved`), then its joules. let rows: Vec<(bool, u64)> = stdout .lines() .filter_map(|l| { let mut f = l.split_whitespace(); let tier = f.next()?; if !(tier.starts_with("T0:") || tier.starts_with("T1:") || tier.starts_with("T2:") || tier.starts_with("T3:") || tier == "unproved") { return None; } let uj = f.next()?.parse::().ok()?; (f.next() == Some("uj")).then_some((tier != "unproved", uj)) }) .collect(); let goals = rows.len() as u64; let proved = rows.iter().filter(|(p, _)| *p).count() as u64; let spent: u64 = rows.iter().map(|(_, uj)| uj).sum(); assert!(goals > 0 && proved > 0 && spent > 0, "no per-goal rows parsed:\n{stdout}"); let tally = stdout.lines().find(|l| l.trim_start().starts_with("proved ")).expect("a proved tally"); assert_eq!(between(tally, "proved ", " ·"), format!("{proved}/{goals}"), "the tally, against the rows"); let same: Vec<&str> = stdout.lines().filter(|l| l.contains("same verified output")).collect(); assert_eq!(same.len(), 1, "\"same verified output\" must be claimed exactly once:\n{stdout}"); let head = same[0]; let total = num(between(head, "energy ", " uj for all")); let head_goals = num(between(head, " uj for all ", " goals")); let baseline = num(between(head, " vs ", " uj frontier-only for the ")); let baseline_goals = num(between(head, " uj frontier-only for the ", " proved")); let ratio = milli(between(head, " → ", "× less for the same verified output")); eprintln!( "proof headline: rows={goals} proved={proved} spent={spent} | printed total={total} baseline={baseline} for \ {baseline_goals} proved, ratio={ratio}/1000" ); assert_eq!(total, spent, "the cascade's figure is not the sum of the rows it printed:\n{stdout}"); assert_eq!(head_goals, goals, "the cascade's figure must cover every goal it ran:\n{stdout}"); assert_eq!(baseline_goals, proved, "the same-output baseline is charged for the proved goals:\n{stdout}"); assert_eq!(baseline, proved * FRONTIER_UJ, "the same-output baseline is {proved} x 50 J:\n{stdout}"); assert_eq!(ratio, baseline * 1000 / total, "the same-output ratio, in thousandths rounded down:\n{stdout}"); let unproved = goals - proved; let all = stdout.lines().find(|l| l.contains("frontier-only for all ")); if unproved > 0 { let all = all.unwrap_or_else(|| panic!("{unproved} goals unproved, but no all-goals figure:\n{stdout}")); assert!(!all.contains("same verified output"), "the all-goals figure claims the same output: {all}"); assert_eq!(num(between(all, "frontier-only for all ", " goals:")), goals); let all_baseline = num(between(all, " goals: ", " uj, ")); assert_eq!(all_baseline, goals * FRONTIER_UJ, "the all-goals baseline is {goals} x 50 J: {all}"); assert_eq!(milli(between(all, " uj, ", "× — but")), all_baseline * 1000 / total, "{all}"); assert_eq!(num(between(all, "× — but ", " of them were not proved")), unproved, "{all}"); assert!(all_baseline > baseline, "the all-goals baseline must exceed the same-output one: {all}"); } else { assert!(all.is_none(), "every goal was proved, yet a separate all-goals figure:\n{stdout}"); } }