open-standards/proof/proof-rs/crates/proof-cli/src/main.rs

//! `proof` — a headless demonstration of the energy-optimized cascade.
//!
//! Runs a proof workload through the cheapest-sufficient ladder — the T0
//! propositional decider and T1 resident `z3`, both real deciders. T0's
//! energy is estimated, not measured: each attempt's wall time ×
//! proof-solvers' default ~15 W power, which no host calibrated, so tagged
//! `Estimator`. T1's is the same estimate, except
//! where this host reads the resident `z3`'s own process tree (macOS, with
//! the kernel's per-process energy counter live), the decision's reading
//! saw nothing missing, and the operator has declared that the `z3` on
//! `PATH` decides each goal in its own process (`PROOF_Z3_SELF_CONTAINED=1`:
//! no container, VM or remote solver behind it, which no reading of the
//! tree could show): then that attempt is the reading, `HwShunt`. A goal's
//! figure sums every attempt on it, so an SMT goal, which T0 tries first and
//! fails, is still `Estimator`: its total holds T0's estimated attempt.
//! There is no T2/T3 rung, so goals that need
//! one come back unproved. It reports, per goal, the tier that closed it and
//! the joules it cost; then the headline — joules spent versus a frontier-only
//! run charged for the goals the cascade proved, the same verified output,
//! with the all-goals figure and its goal count beside it — the Amdahl
//! breakdown by tier, the cache flywheel, and a sealed + verified JCR-1
//! receipt. Only `--measure` attempts a hardware reading, and only through a
//! counter the meter has seen to be live (on macOS this process's CPU energy
//! counter, else IOReport's CPU energy rail; on Linux every RAPL package
//! counter).

use ed25519_dalek::SigningKey;
use proof_schema::{GoalKind, ProofGoal};
use proof_cascade::{EnergySummary, ProofCache, Router};
use proof_solvers::{resident_z3_ladder, z3_available};

fn main() {
    let measure = std::env::args().any(|a| a == "--measure");
    // The operator's declaration about the `z3` on PATH. Without it no T1
    // decision is sealed as a hardware reading, whole or not.
    let z3_self_contained = std::env::var("PROOF_Z3_SELF_CONTAINED").as_deref() == Ok("1");
    let router = Router::new(resident_z3_ladder(z3_self_contained));
    let mut cache = ProofCache::new();
    let mut summary = EnergySummary::default();

    // (statement, kind, label) — prop goals decide at T0, SMT-LIB goals at T1.
    let workload = [
        ("a | ~a", GoalKind::Trivial, "a ∨ ¬a   (prop, T0)"),
        ("a -> a", GoalKind::Trivial, "a → a   (prop, T0)"),
        ("~(a & b) <-> (~a | ~b)", GoalKind::Trivial, "De Morgan   (prop, T0)"),
        ("(a -> b) -> ((b -> c) -> (a -> c))", GoalKind::Trivial, "syllogism   (prop, T0)"),
        (
            "(declare-const x Int)\n(assert (not (=> (> x 0) (>= x 0))))",
            GoalKind::Decidable,
            "x>0 → x≥0   (LIA, z3 T1)",
        ),
        (
            "(declare-const a Int)(declare-const b Int)\n(assert (not (= (+ a b) (+ b a))))",
            GoalKind::Decidable,
            "a+b = b+a   (LIA, z3 T1)",
        ),
        ("∃ continuous f with property P", GoalKind::General, "∃ continuous f …   (model, T2)"),
        ("lemma needing proof search", GoalKind::General, "lemma needing search   (T2)"),
        ("an open research conjecture", GoalKind::Hard, "open conjecture   (frontier, T3)"),
    ];

    println!(
        "proof — cheapest-sufficient cascade (T0 prop + T1 z3 are real; z3 {})\n",
        match (z3_available(), z3_self_contained) {
            (false, _) => "ABSENT — T1 goals escalate",
            (true, true) => "present, declared self-contained",
            (true, false) => "present, not declared self-contained: T1 stays estimated (PROOF_Z3_SELF_CONTAINED=1 declares it)",
        }
    );
    let mut first = None;
    for (statement, kind, label) in workload {
        let goal = ProofGoal::new(statement, "lean4@mathlib", kind);
        let r = router.prove(&goal, &mut cache);
        let tier = r.closed_by.map(|t| t.label()).unwrap_or("unproved");
        println!(
            "  {:<14} {:>11} uj  ({:>9} uj wasted)   {}",
            tier,
            r.total_uj,
            r.wasted_uj,
            truncate(label, 38),
        );
        summary.record(&r);
        if first.is_none() {
            first = Some(r);
        }
    }

    println!(
        "\n  proved {}/{} · tiers T0={} T1={} T2={} T3={}",
        summary.proved,
        summary.goals,
        summary.closed_by_tier[0],
        summary.closed_by_tier[1],
        summary.closed_by_tier[2],
        summary.closed_by_tier[3],
    );
    // Like for like: the same verified output is the goals the cascade
    // proved, so the frontier-only baseline is charged for those alone, and
    // the cascade for every joule it spent — the goals it failed on included.
    // The all-goals baseline also charges goals nothing proved here, so it is
    // printed with its goal count and never called the same output.
    let unproved = summary.goals - summary.proved;
    match summary.proved_ratio_milli() {
        Some(ratio) if summary.proved > 0 => println!(
            "  energy {} uj for all {} goals  vs  {} uj frontier-only for the {} proved  →  {}.{:03}× less for the same verified output",
            summary.total_uj,
            summary.goals,
            summary.proved_baseline_uj,
            summary.proved,
            ratio / 1000,
            ratio % 1000,
        ),
        Some(_) => println!(
            "  energy {} uj for all {} goals, none proved: no verified output to compare with a frontier-only run",
            summary.total_uj, summary.goals,
        ),
        None => println!("  energy 0 uj: the cascade spent nothing, so there is no ratio to state"),
    }
    if unproved > 0 && summary.total_uj > 0 {
        let all = summary.energy_ratio_milli();
        println!(
            "  (frontier-only for all {} goals: {} uj, {}.{:03}× — but {} of them were not proved here, so not the same output)",
            summary.goals,
            summary.baseline_uj,
            all / 1000,
            all % 1000,
            unproved,
        );
    }
    let t3 = summary.uj_by_tier[3]
        .checked_mul(100)
        .and_then(|n| n.checked_div(summary.total_uj.max(1)))
        .unwrap_or(0);
    println!(
        "  by tier (uj): T0={} T1={} T2={} T3={}   — the hardest goal is {}% of the joules (Amdahl)",
        summary.uj_by_tier[0], summary.uj_by_tier[1], summary.uj_by_tier[2], summary.uj_by_tier[3], t3,
    );

    // --measure: try to put a hardware reading beside the wall-time estimate:
    // meter a real T0 proof with the first live source (`meter_source`) — on
    // macOS this process's CPU energy counter, else IOReport's Energy Model
    // (used only while its CPU energy rail is live); on Linux RAPL (used only
    // while every package counter is live) — and report the marginal joules.
    // The figure is graded by its source, HwShunt for each: a vendor or kernel
    // energy counter's reading is a hardware reading while the counter is live
    // for the domain it claims (SPEC §5), which the meter checks before it
    // meters anything; the figure's domain is printed beside it. Where no
    // source is live, print why: the figures above then stay Estimator.
    if measure {
        use proof_cascade::meter::{
            ioreport_status, measure_marginal, meter_source, process_energy_status, rapl_status, MeterSource,
        };
        let source = meter_source();
        let available = source.is_some();
        // The decision THIS process made, printed so tests/measure.rs checks it
        // instead of re-probing in its own process, which could disagree.
        println!(
            "\n  --measure: hardware meter available={available} · source={} · process_energy_status={:?} · \
             ioreport_status={:?} · rapl_status={:?}",
            source.map_or_else(|| "none".to_string(), |s| format!("{s:?}")),
            process_energy_status(),
            ioreport_status(),
            rapl_status()
        );
        if !available {
            println!(
                "  --measure: no hardware energy reading on this host: {}.\n             The figures above stay Estimator — honestly tagged.",
                no_hardware_reading_reason()
            );
        } else {
            // Why each source that is not used is not used: ranked below the
            // one used, or not live.
            if cfg!(target_os = "macos") && source == Some(MeterSource::ProcessEnergy) {
                let own = if ioreport_status() == proof_cascade::meter::IoReportStatus::Live {
                    "its CPU energy rail is live too"
                } else {
                    ioreport_reason()
                };
                println!("  --measure: IOReport not used: the process counter ranks above it. On its own: {own}.");
            } else if cfg!(target_os = "macos") {
                println!("  --measure: this process's CPU energy counter not used: {}.", process_reason());
            }
            // Meter a REAL, non-trivial T0 proof: validity of a 16-variable
            // propositional tautology, decided by the actual truth-table decider
            // (2^16 rows) — genuine, parallelizable compute, run on every core.
            // This is real proof work, not a spin.
            const HARD: &str =
                "(a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p) | (~a&~b&~c&~d&~e&~f&~g&~h&~i&~j&~k&~l&~m&~n&~o&~p)";
            println!(
                "  --measure: metering a real 16-variable T0 proof, on every spare core, {}…",
                match source {
                    Some(MeterSource::ProcessEnergy) => {
                        "on this process's CPU energy counter (no idle baseline: other processes are not in it)"
                    }
                    _ => "against idle on the energy interface",
                }
            );
            let parsed = proof_solvers::prop::parse(HARD).expect("tautology parses");
            assert_eq!(proof_solvers::prop::is_valid(&parsed), Some(true), "the probe goal must be valid");
            let measured = measure_marginal(|| {
                if let Some(e) = proof_solvers::prop::parse(HARD) {
                    std::hint::black_box(proof_solvers::prop::is_valid(&e));
                }
            });
            match measured {
                Some(m) if m.uj > 0 => {
                    let e = m.energy();
                    let _ = e.check_provenance();
                    println!(
                        "  measured: {} uj / proof  ·  provenance {} (measured_uj present, the schema's strongest tier)  ·  source {:?}",
                        m.uj,
                        e.provenance.jcr1_label(),
                        m.source,
                    );
                    println!("  domain: {}", m.source.domain());
                    println!(
                        "  this proof's joules are a hardware reading; the per-goal figures above stay Estimator, and the receipt seals them."
                    );
                }
                // The process counter advanced by under half a microjoule a call.
                Some(m) if m.source == MeterSource::ProcessEnergy => println!(
                    "  measured: under 0.5 uj per proof, below this meter's 1 uj resolution — not a zero-energy proof."
                ),
                // A bracket answered, and busy did not clear idle.
                Some(_) => println!(
                    "  measured: signal stayed inside the idle noise (a loaded/throttled box) — run on a quiet machine."
                ),
                // No reading at all: say why rather than blaming the machine.
                None => println!(
                    "  measured: no hardware reading: {}. The figures above stay Estimator.",
                    no_hardware_reading_reason()
                ),
            }
        }
    }

    // The flywheel: re-prove the first goal — served from cache, zero new joules.
    let again = router.prove(
        &ProofGoal::new(workload[0].0, "lean4@mathlib", workload[0].1),
        &mut cache,
    );
    println!(
        "\n  re-prove (cache): {} uj  (from_cache = {})  — the energy flywheel",
        again.total_uj, again.from_cache
    );

    // Seal + verify a signed JCR-1 receipt for the first proof.
    let first = first.unwrap();
    let sk = SigningKey::from_bytes(&[7u8; 32]);
    let steward = "did:example:proof-reference";
    match proof_receipt::seal(&first, &sk, steward) {
        Ok(env) => {
            let ok = proof_receipt::verify(&first, &env, steward, &sk.verifying_key().to_bytes()).is_ok();
            println!(
                "  receipt: closed at {} · {} uj · provenance {} · spec {} · verified {}",
                first.closed_by.map(|t| t.label()).unwrap_or("-"),
                first.total_uj,
                first.provenance.jcr1_label(),
                first.grounding.label(),
                ok,
            );
        }
        Err(e) => println!("  receipt: {e}"),
    }

    println!("\n  Correctness is the verifier's; the cascade only changes which tier pays for it.");
    println!("  A receipt attests the PROOF. spec=Ungrounded means the formal statement");
    println!("  was not validated against intent — a verified proof of an unverified spec.");
}

/// Why `--measure` has no hardware reading on this host. It comes from the
/// meter's cached statuses — on Apple Silicon the process counter's and
/// IOReport's, on Linux RAPL's — so a counter that is not live is named as
/// such instead of being misread as a noisy machine.
fn no_hardware_reading_reason() -> String {
    if cfg!(target_os = "macos") {
        format!("{}; and {}", process_reason(), ioreport_reason())
    } else if cfg!(target_os = "linux") {
        rapl_reason().to_string()
    } else {
        "no hardware energy interface is supported on this OS".to_string()
    }
}

/// Why this process's CPU energy counter is or is not used, from its status.
fn process_reason() -> &'static str {
    use proof_cascade::meter::{process_energy_status, CounterStatus};
    match process_energy_status() {
        CounterStatus::Unavailable => {
            "this process's CPU energy counter (proc_pid_rusage, ri_energy_nj) could not be read, or the measuring \
             thread's own energy count, which each of its reads is checked against, could not"
        }
        CounterStatus::Absent => "this process's CPU energy counter is absent",
        CounterStatus::Frozen => {
            "this process's CPU energy counter did not keep advancing while this process burned CPU"
        }
        CounterStatus::Live => "this process's CPU energy counter is live, but the measurement returned no reading",
    }
}

/// Why IOReport is or is not used, from its status.
fn ioreport_reason() -> &'static str {
    use proof_cascade::meter::{ioreport_status, IoReportStatus};
    match ioreport_status() {
        IoReportStatus::CpuRailFrozen => {
            "IOReport opens, but its CPU energy rail is frozen (it did not keep advancing while \
             this process burned CPU), so it cannot meter CPU work"
        }
        IoReportStatus::CpuRailAbsent => "IOReport's Energy Model group opens, but has no CPU energy rail",
        IoReportStatus::Unavailable => {
            "IOReport's Energy Model group could not be opened, or opened but could not be sampled \
             (opening it needs Apple Silicon, not Rosetta)"
        }
        IoReportStatus::Live => "IOReport's CPU energy rail is live, but the bracket returned no reading",
    }
}

/// Why RAPL is or is not used, from its status.
fn rapl_reason() -> &'static str {
    use proof_cascade::meter::{rapl_status, CounterStatus};
    match rapl_status() {
        CounterStatus::Unavailable => "no readable RAPL counter at /sys/class/powercap/intel-rapl:*/energy_uj",
        CounterStatus::Absent => "RAPL zones are readable, but none of them is a package zone",
        CounterStatus::Frozen => {
            "a RAPL package counter is readable but did not keep advancing while this process burned CPU, \
             so it cannot meter CPU work"
        }
        CounterStatus::Live => "RAPL's package counters are live, but the bracket returned no reading",
    }
}

fn truncate(s: &str, n: usize) -> String {
    if s.chars().count() <= n {
        s.to_string()
    } else {
        let mut t: String = s.chars().take(n - 1).collect();
        t.push('…');
        t
    }
}