open-standards/proof/proof-rs/crates/proof-cli/tests/headline.rs

//! 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: `<int>.<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::<u64>().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}");
    }
}