proof/README.md

@@ -36,15 +36,17 @@ proof/
 ### The reference implementation (`proof-rs/`)
 
 - **`proof-schema`** — the content-addressed goal (`blake3(statement‖0x00‖context)`), the cheapest-first tier ladder, the honest energy model (`HwShunt`/`ModelBased`/`Estimator` with the coupling enforced), `SpecGrounding`, the verdict, and the `Solver` trait every backend implements. Canonical det-CBOR content addressing.
-- **`proof-solvers`** — two **real** rungs with measured energy: a propositional decider (T0) that parses a boolean goal and decides validity by truth-table in process, and `z3` (T1) — shell or kept **resident** across goals — that decides an SMT-LIB goal (assert the negation; `unsat` ⇒ valid). Each refuses rather than fakes, so the router escalates. The model rungs (T2/T3) are honest stand-ins behind the same trait.
-- **`proof-cascade`** — the escalation router (every joule accounted, `wasted_uj` disclosed), the content-addressed proof cache (the energy flywheel, durable as line-delimited JSON), batch energy accounting against a frontier-only baseline with the per-tier Amdahl breakdown, and a **real hardware energy meter** (`meter` — the `HwShunt` backend): it brackets a real proof, run on every core, against an idle baseline using the platform's energy interface (IOReport via `macmon` on Apple Silicon, RAPL on Linux) and returns measured microjoules, so the headline `joules per verified proof` can be a real reading, not only a model. Returns nothing where no interface is reachable — the caller keeps the honestly-tagged `ModelBased` figure rather than inventing one.
+- **`proof-solvers`** — two **real** rungs, their energy modeled from measured wall time (`ModelBased`, a ~15 W power model — not a hardware reading): a propositional decider (T0) that parses a boolean goal and decides validity by truth-table in process, and `z3` (T1) — shell or kept **resident** across goals — that decides an SMT-LIB goal (assert the negation; `unsat` ⇒ valid). Each refuses rather than fakes, so the router escalates. The model rungs (T2/T3) are honest stand-ins behind the same trait.
+- **`proof-cascade`** — the escalation router (every joule accounted, `wasted_uj` disclosed), the content-addressed proof cache (the energy flywheel, durable as line-delimited JSON), batch energy accounting against a frontier-only baseline with the per-tier Amdahl breakdown, and a **real hardware energy meter** (`meter` — the `HwShunt` backend): it brackets a real proof, run on every core, against an idle baseline using the platform's energy interface (IOReport's Energy Model, read directly through its C API on Apple Silicon and used only while every CPU energy rail is live, one per die on a multi-die part; RAPL's package counters on Linux, used only while every one is live) and returns measured microjoules, so the headline `joules per verified proof` can be a real reading, not only a model. A vendor counter's reading is graded `HwShunt` only while the counter is live for the domain it claims ([`SPEC.md`](SPEC.md) §5), and the meter checks that before it brackets anything, by one rule on both platforms (the counter keeps advancing in at least 5 sample intervals, at least 4 of every 5, over at least 300 ms while the probe burns CPU): on Apple Silicon for every IOReport CPU energy rail the figure sums (`CPU Energy`, or each die's `DIE_<n>_CPU Energy`), on Linux for every RAPL package counter the figure sums (`psys` is neither summed nor probed). Returns nothing where no interface is reachable or its counter is not live — the caller keeps the honestly-tagged `ModelBased` figure rather than inventing one.
 - **`proof-receipt`** — the `proof/1` JCR-1 receipt: canonical det-CBOR + COSE_Sign1/EdDSA, vendored byte-compatible with the family's cross-language verifiers; refuses to seal an unproved goal.
 - **`proof-conformance`** — C1–C5 + a negative pack, all checks real, published vectors in `conformance/v1/`.
-- **`proof-cli`** — the `proof` reference demo: a proof workload reporting joules-per-proof against a frontier-only baseline, the Amdahl breakdown, the cache flywheel, and a sealed + verified receipt. `proof --measure` adds a **real hardware reading** of a non-trivial T0 proof (`HwShunt`, where an energy interface is present).
+- **`proof-cli`** — the `proof` reference demo: a proof workload reporting joules-per-proof against a frontier-only baseline — like for like, charged only for the goals the cascade proved, with the all-goals figure and its goal count beside it — the Amdahl breakdown, the cache flywheel, and a sealed + verified receipt. `proof --measure` adds a **real hardware reading** of a non-trivial T0 proof (`HwShunt`) where the meter produces one; that needs a counter the meter has seen to be live (on Apple Silicon every IOReport CPU energy rail, on Linux every RAPL package counter). On the Macs measured so far (macOS 27.0.1, an M5 Max and an M3 Ultra) IOReport's CPU energy rail is frozen for an unprivileged reader, so `--measure` declines there, says why, and leaves every figure `ModelBased`; on Linux, RAPL's `energy_uj` is root-only on current kernels.
 
-`cargo test --workspace` green; `cargo clippy --workspace --all-targets`
-warning-free. The two bottom rungs decide for real with measured energy; the
-model rungs are honestly marked as stand-ins until inference backends are wired.
+`cargo test --workspace` green; `cargo clippy --workspace --all-targets` is
+warning-free for Linux, and on macOS reports two lints in proof-cascade's
+IOReport FFI. The two bottom rungs decide for real, with energy modeled from
+wall time; the model rungs are honestly marked as stand-ins until inference
+backends are wired.
 
 ## Honesty the standard records
 

proof/SPEC.md

@@ -86,8 +86,10 @@ The normative requirement is that the figure is *reported and honestly tagged*
 
 Every reading is integer microjoules with a provenance tag:
 
-- `HwShunt` — read from a hardware energy interface (RAPL/NVML/SMC). REQUIRES a
-  present measured figure.
+- `HwShunt` — read from a hardware energy interface: a shunt or power meter, the
+  SMC, or a vendor energy counter (RAPL, NVML, Apple IOReport, ...). REQUIRES a
+  present measured figure. A vendor counter's reading is a hardware reading,
+  subject to the liveness requirement below.
 - `ModelBased` — computed from a calibrated per-operation model (e.g. measured
   wall time × a power model). A measured figure MAY be absent.
 - `Estimator` — a coarse constant. A measured figure MUST be absent.
@@ -95,6 +97,20 @@ Every reading is integer microjoules with a provenance tag:
 A conforming implementation MUST enforce this coupling: `HwShunt` without a
 measured figure, or `Estimator` with one, is invalid.
 
+**Liveness.** A reading from a vendor energy counter (RAPL, NVML, Apple
+IOReport, ...) MAY be graded as a hardware reading only while the counter is
+demonstrably live for the domain the figure claims: the implementation MUST
+have observed the counter covering that domain advance under load (for Apple
+IOReport: every CPU energy rail the figure sums - the rail itself, one per die
+on a multi-die part - advancing on its own in at least 5 sample intervals, in
+at least 4 of every 5, over at least 300 ms while the probing thread burns CPU;
+one rail that held leaves the whole figure not live). A counter that is
+present but not live - frozen, or republished in lumps - MUST NOT produce a
+hardware-graded figure; the implementation falls back to its estimator or
+reports the work unmetered, and SHOULD record why. In this standard a
+hardware-graded figure is `HwShunt`; the fallback is `ModelBased` or
+`Estimator`.
+
 Batch accounting reports, against a **frontier-only baseline** (every goal
 costed at T3), the total joules, the savings, and the energy attributed to each
 *closing* tier. The per-tier breakdown is REQUIRED so that Amdahl behaviour —

proof/proof-rs/crates/proof-cascade/src/lib.rs

@@ -388,7 +388,16 @@ pub struct EnergySummary {
     pub from_cache: u64,
     pub total_uj: u64,
     pub wasted_uj: u64,
+    /// The frontier-only baseline over EVERY goal recorded, proved or not
+    /// (SPEC §5).
     pub baseline_uj: u64,
+    /// The frontier-only baseline over the PROVED goals alone: what a
+    /// frontier-only run is charged for the same verified output. A goal the
+    /// cascade did not prove produced nothing to compare, so it is not
+    /// charged here (it is in `baseline_uj`). A comparison offered as "for the
+    /// same verified output" is this against `total_uj`
+    /// ([`EnergySummary::proved_ratio_milli`]), never `baseline_uj` against it.
+    pub proved_baseline_uj: u64,
     /// Count of goals closed at each tier, indexed by `Tier::LADDER` order.
     pub closed_by_tier: [u64; 4],
     /// Joules attributed to each closing tier (Amdahl visibility).
@@ -418,6 +427,7 @@ impl EnergySummary {
         self.baseline_uj = self.baseline_uj.saturating_add(r.baseline_uj);
         if r.proved {
             self.proved += 1;
+            self.proved_baseline_uj = self.proved_baseline_uj.saturating_add(r.baseline_uj);
         }
         if r.from_cache {
             self.from_cache += 1;
@@ -437,14 +447,26 @@ impl EnergySummary {
         self.baseline_uj.saturating_sub(self.total_uj)
     }
 
-    /// `baseline / total`, in thousandths (so 9703 = 9.703×). Saturates if no
-    /// energy was spent.
+    /// `baseline / total`, in thousandths (so 9703 = 9.703×), with the
+    /// baseline charged for EVERY goal recorded — including goals the cascade
+    /// did not prove, so it is not a comparison for the same output; see
+    /// [`EnergySummary::proved_ratio_milli`]. Saturates if no energy was spent.
     pub fn energy_ratio_milli(&self) -> u64 {
         if self.total_uj == 0 {
             return u64::MAX;
         }
         self.baseline_uj.saturating_mul(1000) / self.total_uj
     }
+
+    /// The like-for-like ratio, for the same verified output: the
+    /// frontier-only baseline charged only for the goals the cascade proved
+    /// ([`EnergySummary::proved_baseline_uj`]) ÷ every joule the cascade
+    /// spent, including those it spent on goals it did not prove — in
+    /// thousandths, rounded down. `None` if the cascade spent nothing (there
+    /// is no ratio to state); `Some(0)` if it proved nothing.
+    pub fn proved_ratio_milli(&self) -> Option<u64> {
+        (self.total_uj > 0).then(|| self.proved_baseline_uj.saturating_mul(1000) / self.total_uj)
+    }
 }
 
 #[cfg(test)]
@@ -681,6 +703,52 @@ mod tests {
         assert_eq!(restored.len(), cache.len());
     }
 
+    /// The same-output comparison charges the frontier-only baseline only for
+    /// the goals the cascade proved, against everything the cascade spent —
+    /// including the joules it spent failing on the goal it could not prove.
+    /// The all-goals ratio, which charges the baseline for the unproved goal
+    /// too, is larger, and is not a comparison for the same output.
+    #[test]
+    fn the_same_output_ratio_charges_the_baseline_only_for_proved_goals() {
+        // T0 closes Trivial, T1 Decidable; nothing closes Hard.
+        let r = Router::new(vec![
+            Box::new(Gate { tier: Tier::Automation, closes: GoalKind::Trivial }),
+            Box::new(Gate { tier: Tier::Smt, closes: GoalKind::Decidable }),
+        ]);
+        let mut cache = ProofCache::new();
+        let mut s = EnergySummary::default();
+        for g in [
+            ProofGoal::new("x=x", "c", GoalKind::Trivial),
+            ProofGoal::new("dec", "c", GoalKind::Decidable),
+            ProofGoal::new("hard", "c", GoalKind::Hard),
+        ] {
+            s.record(&r.prove(&g, &mut cache));
+        }
+        // The tests' own literals: T0 = 50 uJ, T1 = 5_000 uJ, T3 = 50 J.
+        let total = 50 + (50 + 5_000) + (50 + 5_000);
+        assert_eq!((s.goals, s.proved, s.total_uj), (3, 2, total));
+        assert_eq!(s.baseline_uj, 3 * 50_000_000, "the all-goals baseline charges the unproved goal too");
+        assert_eq!(s.proved_baseline_uj, 2 * 50_000_000, "the same-output baseline charges the 2 proved goals only");
+        assert_eq!(s.proved_ratio_milli(), Some(100_000_000_000 / total), "{s:?}");
+        assert_eq!(s.proved_ratio_milli(), Some(9_852_216));
+        assert_eq!(s.energy_ratio_milli(), 150_000_000_000 / total);
+        assert!(s.proved_ratio_milli().unwrap() < s.energy_ratio_milli());
+
+        // A cache hit is a proved goal served for nothing: charged to both
+        // baselines, adding no joules.
+        s.record(&r.prove(&ProofGoal::new("x=x", "c", GoalKind::Trivial), &mut cache));
+        assert_eq!((s.proved_baseline_uj, s.total_uj), (3 * 50_000_000, total));
+
+        // Nothing spent: no ratio to state. Nothing proved: zero.
+        let mut free = EnergySummary::default();
+        assert_eq!(free.proved_ratio_milli(), None);
+        free.record(&Router::new(Vec::new()).prove(&ProofGoal::new("hard", "c", GoalKind::Hard), &mut ProofCache::new()));
+        assert_eq!((free.proved, free.total_uj, free.proved_ratio_milli()), (0, 0, None));
+        let mut none_proved = EnergySummary::default();
+        none_proved.record(&r.prove(&ProofGoal::new("hard2", "c", GoalKind::Hard), &mut cache));
+        assert_eq!((none_proved.proved_baseline_uj, none_proved.proved_ratio_milli()), (0, Some(0)));
+    }
+
     #[test]
     fn summary_accounts_baseline_and_tiers() {
         let r = Router::new(ladder());

proof/proof-rs/crates/proof-cascade/tests/ioreport_once.rs

@@ -0,0 +1,106 @@
+//! The IOReport liveness probe behind `ioreport_status()` runs once per
+//! PROCESS, however many threads ask at once, through the status, the
+//! selection and the metering entry point: a probe per call or per thread
+//! would burn ~1 s on each caller's thread (inside `measure_marginal_uj`'s
+//! bracket, a whole probe in the busy window) and could flip the verdict
+//! mid-process. (`power_over` is private; the lib test
+//! `the_gated_entry_points_read_the_cached_status` pins it the same way, on
+//! the calling thread's CPU.)
+//!
+//! This file holds this one test, so that it runs in a process of its own and
+//! IS the first use of the meter in that process. The counter it reads,
+//! `real_probe_runs()`, counts runs of the production probe (`host_status`,
+//! whose first statement it is), not lookups of the cache in front of it.
+
+use proof_cascade::meter::{
+    hardware_meter_available, ioreport_status, measure_marginal_uj, real_probe_runs, IoReportStatus,
+};
+use std::sync::{Arc, Barrier};
+use std::time::Duration;
+
+/// Real, cheap, pure CPU work.
+fn cpu_work() {
+    std::hint::black_box((0..4000u64).fold(0u64, |a, b| a.wrapping_mul(31).wrapping_add(b)));
+}
+
+/// This thread's CPU time, read through this test's own binding of
+/// `clock_gettime(CLOCK_THREAD_CPUTIME_ID)` (16 on macOS).
+#[cfg(target_os = "macos")]
+fn thread_cpu() -> Duration {
+    #[repr(C)]
+    struct Timespec {
+        tv_sec: i64,
+        tv_nsec: std::os::raw::c_long,
+    }
+    unsafe extern "C" {
+        fn clock_gettime(clock_id: std::os::raw::c_int, tp: *mut Timespec) -> std::os::raw::c_int;
+    }
+    let mut ts = Timespec { tv_sec: 0, tv_nsec: 0 };
+    // SAFETY: ts is a valid, writable timespec.
+    assert_eq!(unsafe { clock_gettime(16, &mut ts) }, 0, "the thread CPU clock does not read");
+    Duration::new(ts.tv_sec as u64, ts.tv_nsec as u32)
+}
+
+#[cfg(not(target_os = "macos"))]
+fn thread_cpu() -> Duration {
+    Duration::ZERO
+}
+
+/// Eight threads, released together, each ask for the status and then select
+/// the meter the way a caller does (`hardware_meter_available()` is the
+/// selection; `measure_marginal_uj` selects and, declined, gives no figure).
+/// The probe must have run exactly once for all of them. Once a thread has its
+/// status, its selection calls must be warm: together they may not burn 10 ms
+/// of that thread's CPU, where re-running the probe by any route costs at
+/// least six reads of the Energy Model group (~7 ms of thread CPU each) and
+/// five 25 ms ticks, and normally ~1 s of burn.
+#[test]
+fn the_liveness_probe_runs_once_per_process() {
+    assert_eq!(real_probe_runs(), 0, "the meter was used in this process before this test: this is not its first use");
+    const THREADS: usize = 8;
+    let gate = Arc::new(Barrier::new(THREADS));
+    let handles: Vec<_> = (0..THREADS)
+        .map(|_| {
+            let gate = gate.clone();
+            std::thread::spawn(move || {
+                gate.wait();
+                let status = ioreport_status();
+                let c0 = thread_cpu();
+                let selected = hardware_meter_available();
+                let again = ioreport_status();
+                let figure = if selected { None } else { measure_marginal_uj(cpu_work) };
+                let warm = thread_cpu() - c0;
+                (status, again, selected, figure, warm)
+            })
+        })
+        .collect();
+    let seen: Vec<_> = handles.into_iter().map(|h| h.join().expect("a probing thread panicked")).collect();
+    let runs = real_probe_runs();
+    let warmest = seen.iter().map(|s| s.4).max().unwrap_or_default();
+    eprintln!(
+        "ioreport cache: {THREADS} threads saw (status={:?}, selected={}); real probe runs in this process: {runs}; \
+         warm selection calls burned at most {warmest:?} of a thread's CPU",
+        seen[0].0, seen[0].2
+    );
+    for (i, (status, again, selected, figure, _)) in seen.iter().enumerate() {
+        assert_eq!((*status, *again), (seen[0].0, seen[0].0), "thread {i} was given a different status");
+        assert_eq!(*selected, seen[0].2, "thread {i} made a different selection");
+        if !selected {
+            assert_eq!(*figure, None, "thread {i}: a declined meter gave a figure");
+        }
+    }
+    if cfg!(target_os = "macos") {
+        assert_eq!(seen[0].2, seen[0].0 == IoReportStatus::Live, "on macOS the meter is selected exactly when Live");
+        assert_eq!(runs, 1, "the liveness probe ran {runs} times in this process ({THREADS} threads asked at once)");
+        for (i, s) in seen.iter().enumerate() {
+            assert!(
+                s.4 < Duration::from_millis(10),
+                "thread {i}: its warm selection calls burned {:?} of its CPU: something probed again, uncached",
+                s.4
+            );
+        }
+    } else {
+        assert_eq!(seen[0].0, IoReportStatus::Unavailable, "IOReport off macOS");
+        assert_eq!(runs, 0, "a liveness probe ran off macOS");
+    }
+}

proof/proof-rs/crates/proof-cascade/tests/ioreport_unopenable.rs

@@ -0,0 +1,58 @@
+//! The unopenable path of the whole production chain — probe, status, cache,
+//! selection, metering — on any host. Neither Mac that runs these tests lacks
+//! an Energy Model group, so `simulate_no_energy_model_group()` makes this
+//! process's probe find none before the meter's first use. This file holds
+//! this one test so that it runs in a process of its own and the hook cannot
+//! reach any other test.
+
+use proof_cascade::meter::{
+    hardware_meter_available, ioreport_status, measure_marginal_uj, real_probe_runs, simulate_no_energy_model_group,
+    IoReportStatus,
+};
+use std::sync::atomic::{AtomicU64, Ordering};
+use std::sync::{Arc, Barrier};
+
+/// How many times [`counted_work`] has run in this process.
+static WORK_CALLS: AtomicU64 = AtomicU64::new(0);
+
+fn counted_work() {
+    WORK_CALLS.fetch_add(1, Ordering::SeqCst);
+    std::hint::black_box((0..4000u64).fold(0u64, |a, b| a.wrapping_mul(31).wrapping_add(b)));
+}
+
+/// With no Energy Model group to subscribe to, the status is `Unavailable` —
+/// never `Live`, never `CpuRailAbsent` — for every thread that asks, the meter
+/// is never selected, metering gives no figure and never runs the work, and the
+/// probe still ran exactly once.
+#[test]
+fn a_host_with_no_energy_model_group_is_unavailable_and_every_meter_declines() {
+    assert_eq!(real_probe_runs(), 0, "the meter was used in this process before this test: this is not its first use");
+    simulate_no_energy_model_group();
+    const THREADS: usize = 4;
+    let gate = Arc::new(Barrier::new(THREADS));
+    let handles: Vec<_> = (0..THREADS)
+        .map(|_| {
+            let gate = gate.clone();
+            std::thread::spawn(move || {
+                gate.wait();
+                let status = ioreport_status();
+                let selected = hardware_meter_available();
+                let figure = if cfg!(target_os = "macos") { measure_marginal_uj(counted_work) } else { None };
+                (status, selected, figure)
+            })
+        })
+        .collect();
+    let seen: Vec<_> = handles.into_iter().map(|h| h.join().expect("a thread panicked")).collect();
+    let runs = real_probe_runs();
+    let work = WORK_CALLS.load(Ordering::SeqCst);
+    eprintln!("ioreport unopenable: {THREADS} threads saw {seen:?}; real probe runs: {runs}; work calls: {work}");
+    for (i, (status, selected, figure)) in seen.iter().enumerate() {
+        assert_eq!(*status, IoReportStatus::Unavailable, "thread {i}: no Energy Model group, yet {status:?}");
+        if cfg!(target_os = "macos") {
+            assert!(!selected, "thread {i}: the meter was selected with no Energy Model group");
+            assert_eq!(*figure, None, "thread {i}: a figure came out with no Energy Model group");
+        }
+    }
+    assert_eq!(work, 0, "the work ran {work} times with no usable meter");
+    assert_eq!(runs, usize::from(cfg!(target_os = "macos")), "the liveness probe's runs in this process");
+}

proof/proof-rs/crates/proof-cascade/tests/rapl_once.rs

@@ -0,0 +1,41 @@
+//! The RAPL liveness probe behind `rapl_status()` runs once per PROCESS,
+//! however many threads ask at once: a probe per call would burn about a
+//! second of CPU on each caller's thread where the counters are readable, and
+//! could flip the verdict mid-process.
+//!
+//! This file holds this one test, so that it runs in a process of its own and
+//! IS the first use of the RAPL meter in that process. The counter it reads,
+//! `real_rapl_probe_runs()`, counts runs of the production probe
+//! (`rapl_host_status`, whose first statement it is), not lookups of the cache.
+//! Off Linux there is no RAPL: the status is `Unavailable` and no probe runs.
+
+use proof_cascade::meter::{rapl_status, real_rapl_probe_runs, CounterStatus};
+use std::sync::{Arc, Barrier};
+
+#[test]
+fn the_rapl_liveness_probe_runs_once_per_process() {
+    assert_eq!(real_rapl_probe_runs(), 0, "the RAPL meter was used in this process before this test");
+    const THREADS: usize = 8;
+    let gate = Arc::new(Barrier::new(THREADS));
+    let handles: Vec<_> = (0..THREADS)
+        .map(|_| {
+            let gate = gate.clone();
+            std::thread::spawn(move || {
+                gate.wait();
+                (rapl_status(), rapl_status())
+            })
+        })
+        .collect();
+    let seen: Vec<_> = handles.into_iter().map(|h| h.join().expect("a probing thread panicked")).collect();
+    let runs = real_rapl_probe_runs();
+    eprintln!("rapl cache: {THREADS} threads saw {:?}; real RAPL probe runs in this process: {runs}", seen[0].0);
+    for (i, (status, again)) in seen.iter().enumerate() {
+        assert_eq!((*status, *again), (seen[0].0, seen[0].0), "thread {i} was given a different status");
+    }
+    if cfg!(target_os = "linux") {
+        assert_eq!(runs, 1, "the RAPL liveness probe ran {runs} times in this process ({THREADS} threads asked at once)");
+    } else {
+        assert_eq!(seen[0].0, CounterStatus::Unavailable, "RAPL off Linux");
+        assert_eq!(runs, 0, "a RAPL liveness probe ran off Linux");
+    }
+}

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

@@ -1,11 +1,17 @@
 //! `proof` — a headless demonstration of the energy-optimized cascade.
 //!
-//! Runs a proof workload through the cheapest-sufficient ladder (T0 propositional
-//! decider + T1 resident `z3`, both real with measured energy; T2/T3 reference
-//! stand-ins) and reports, per goal, the tier that closed it and the joules it
-//! cost; then the headline — joules spent versus a frontier-only run — the
-//! Amdahl breakdown by tier, the cache flywheel, and a sealed + verified JCR-1
-//! receipt.
+//! Runs a proof workload through the cheapest-sufficient ladder — the T0
+//! propositional decider and T1 resident `z3`, both real deciders whose energy
+//! is modeled, not measured: each attempt's wall time × proof-solvers' ~15 W
+//! power model, tagged `ModelBased`. 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 Apple Silicon IOReport's CPU
+//! energy rail, on Linux every RAPL package counter).
 
 use ed25519_dalek::SigningKey;
 use proof_schema::{GoalKind, ProofGoal};
@@ -61,7 +67,6 @@ fn main() {
         }
     }
 
-    let ratio = summary.energy_ratio_milli();
     println!(
         "\n  proved {}/{} · tiers T0={} T1={} T2={} T3={}",
         summary.proved,
@@ -71,13 +76,39 @@ fn main() {
         summary.closed_by_tier[2],
         summary.closed_by_tier[3],
     );
-    println!(
-        "  energy {} uj  vs  {} uj frontier-only  →  {}.{:03}× less for the same verified output",
-        summary.total_uj,
-        summary.baseline_uj,
-        ratio / 1000,
-        ratio % 1000,
-    );
+    // 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)))
@@ -87,15 +118,29 @@ fn main() {
         summary.uj_by_tier[0], summary.uj_by_tier[1], summary.uj_by_tier[2], summary.uj_by_tier[3], t3,
     );
 
-    // --measure: upgrade the headline from a wall-time model to a REAL hardware
-    // reading. Bracket the whole batch against idle on the platform's energy
-    // interface (macmon/IOReport on Apple Silicon, RAPL on Linux) and report the
-    // marginal joules with HwShunt provenance — the schema's strongest tier.
+    // --measure: try to put a hardware reading beside the wall-time model.
+    // Bracket a real T0 proof against idle on the platform's energy interface
+    // (IOReport on Apple Silicon, used only while its CPU energy rail is live;
+    // RAPL on Linux, used only while every package counter is live) and report
+    // the marginal joules. The figure is tagged `Energy::measured`, i.e.
+    // HwShunt, on both platforms: a vendor 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 brackets anything. Where no
+    // interface is usable, print why: the figures above then stay ModelBased.
     if measure {
-        use proof_cascade::meter::{hardware_meter_available, measure_marginal_uj};
-        if !hardware_meter_available() {
+        use proof_cascade::meter::{hardware_meter_available, ioreport_status, measure_marginal_uj, rapl_status};
+        let available = hardware_meter_available();
+        // 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} · ioreport_status={:?} · rapl_status={:?}",
+            ioreport_status(),
+            rapl_status()
+        );
+        if !available {
             println!(
-                "\n  --measure: no hardware energy interface reachable here (need macmon on macOS\n             or RAPL on Linux). The figures above stay ModelBased — honestly tagged."
+                "  --measure: no hardware energy reading on this host: {}.\n             The figures above stay ModelBased — honestly tagged.",
+                no_hardware_reading_reason()
             );
         } else {
             // Meter a REAL, non-trivial T0 proof: validity of a 16-variable
@@ -104,7 +149,7 @@ fn main() {
             // and bracketed against idle. 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!("\n  --measure: metering a real 16-variable T0 proof against idle on the energy interface…");
+            println!("  --measure: metering a real 16-variable T0 proof 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_uj(|| {
@@ -122,9 +167,15 @@ fn main() {
                     );
                     println!("  the standard's headline (joules per verified proof) is now a real hardware reading, not a model.");
                 }
-                _ => println!(
+                // The interface 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 ModelBased.",
+                    no_hardware_reading_reason()
+                ),
             }
         }
     }
@@ -163,6 +214,40 @@ fn main() {
     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 status — IOReport's on Apple Silicon, RAPL's on Linux — so a
+/// counter that is not live is named as such instead of being misread as a
+/// noisy machine.
+fn no_hardware_reading_reason() -> &'static str {
+    use proof_cascade::meter::{ioreport_status, rapl_status, CounterStatus, IoReportStatus};
+    if cfg!(target_os = "macos") {
+        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",
+        }
+    } else if cfg!(target_os = "linux") {
+        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",
+        }
+    } else {
+        "no hardware energy interface is supported on this OS"
+    }
+}
+
 fn truncate(s: &str, n: usize) -> String {
     if s.chars().count() <= n {
         s.to_string()

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

@@ -0,0 +1,92 @@
+//! 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}");
+    }
+}

proof/proof-rs/crates/proof-cli/tests/measure.rs

@@ -0,0 +1,171 @@
+//! `proof --measure`, end to end: when the hardware meter declines, the output
+//! names the reason, nothing in it claims a hardware reading, and the cascade's
+//! own ModelBased figures stand; when it meters, the host really has a usable
+//! interface. Every check is against the decision the `proof` process printed,
+//! never a second probe in this process: two independent ~1 s probes of a
+//! borderline rail could disagree.
+//!
+//! The printed status is itself checked against what the process did with it.
+//! The CLI's reason for declining comes from the status it acted on, so on
+//! macOS every IOReport reason in the output must be the one for the printed
+//! status, and a declined meter must print that reason: a CLI that prints one
+//! status and acts on another fails here, whichever status either one is.
+
+use std::process::Command;
+
+/// The value after `key=` on the first line that has it, up to the next space.
+fn field<'a>(stdout: &'a str, key: &str) -> Option<&'a str> {
+    let at = stdout.find(key)? + key.len();
+    stdout[at..].split_whitespace().next()
+}
+
+/// Every `IoReportStatus` the CLI can print, each with the reason it gives
+/// when that status is why there is no hardware reading (`Live`'s is for a
+/// bracket that returned nothing). Each reason names exactly one status.
+const IOREPORT_REASONS: [(&str, &str); 4] = [
+    ("CpuRailFrozen", "its CPU energy rail is frozen"),
+    ("CpuRailAbsent", "has no CPU energy rail"),
+    ("Unavailable", "could not be opened, or opened but could not be sampled"),
+    ("Live", "CPU energy rail is live, but the bracket returned no reading"),
+];
+
+/// Every RAPL `CounterStatus` the CLI can print, each with the reason it
+/// gives on Linux when that status is why there is no hardware reading.
+const RAPL_REASONS: [(&str, &str); 4] = [
+    ("Unavailable", "no readable RAPL counter"),
+    ("Absent", "none of them is a package zone"),
+    ("Frozen", "a RAPL package counter is readable but did not keep advancing"),
+    ("Live", "RAPL's package counters are live, but the bracket returned no reading"),
+];
+
+#[test]
+fn measure_names_why_it_declined_and_claims_no_hardware_reading() {
+    let out = Command::new(env!("CARGO_BIN_EXE_proof"))
+        .arg("--measure")
+        .output()
+        .expect("the proof binary runs");
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    assert!(
+        out.status.success(),
+        "proof --measure exited {:?}\n{stdout}\n{}",
+        out.status,
+        String::from_utf8_lossy(&out.stderr)
+    );
+    let available = match field(&stdout, "--measure: hardware meter available=") {
+        Some("true") => true,
+        Some("false") => false,
+        other => panic!("proof --measure did not print its meter decision ({other:?}):\n{stdout}"),
+    };
+    let status = field(&stdout, "ioreport_status=")
+        .unwrap_or_else(|| panic!("proof --measure did not print its IOReport status:\n{stdout}"));
+    assert!(
+        IOREPORT_REASONS.iter().any(|&(s, _)| s == status),
+        "proof --measure printed an unknown IOReport status {status:?}:\n{stdout}"
+    );
+    let rapl = field(&stdout, "rapl_status=")
+        .unwrap_or_else(|| panic!("proof --measure did not print its RAPL status:\n{stdout}"));
+    assert!(
+        RAPL_REASONS.iter().any(|&(s, _)| s == rapl),
+        "proof --measure printed an unknown RAPL status {rapl:?}:\n{stdout}"
+    );
+    let declined = stdout.contains("--measure: no hardware energy reading on this host: ");
+    // Recorded so a log says which branch below was actually asserted.
+    eprintln!("proof --measure: declined={declined} available={available} ioreport_status={status} rapl_status={rapl}");
+
+    // The sealed receipt is the cascade's own figure for the first goal, on
+    // every branch: ModelBased and non-zero, never the --measure figure.
+    let receipt = stdout
+        .lines()
+        .find(|l| l.trim_start().starts_with("receipt: closed at"))
+        .unwrap_or_else(|| panic!("no sealed receipt in the output:\n{stdout}"));
+    let receipt_uj: u64 = receipt
+        .split(" · ")
+        .nth(1)
+        .and_then(|f| f.strip_suffix(" uj"))
+        .and_then(|n| n.parse().ok())
+        .unwrap_or_else(|| panic!("no uj figure in the receipt line: {receipt}"));
+    assert!(receipt_uj > 0, "the receipt carries a zero figure for a proof that ran: {receipt}");
+    assert!(receipt.contains("provenance ModelBased"), "the receipt's provenance changed: {receipt}");
+
+    assert_eq!(declined, !available, "the CLI's output disagrees with the decision it printed:\n{stdout}");
+    // RAPL is a Linux interface: elsewhere it is Unavailable and no RAPL
+    // reason is ever given. On Linux the meter is available exactly when RAPL
+    // is Live, and a declined meter gives the printed RAPL status's reason.
+    if cfg!(target_os = "linux") {
+        assert_eq!(available, rapl == "Live", "on Linux the meter is available exactly when RAPL is Live:\n{stdout}");
+        for (reason_status, reason) in RAPL_REASONS {
+            if stdout.contains(reason) {
+                assert_eq!(
+                    reason_status, rapl,
+                    "the CLI printed rapl_status={rapl} but gave the reason for {reason_status}:\n{stdout}"
+                );
+            }
+        }
+        if declined {
+            let (_, reason) = RAPL_REASONS.iter().find(|&&(s, _)| s == rapl).expect("a known status");
+            assert!(stdout.contains(reason), "declined with rapl_status={rapl}, but not for its reason:\n{stdout}");
+        }
+    } else {
+        assert_eq!(rapl, "Unavailable", "a RAPL status other than Unavailable off Linux:\n{stdout}");
+        for (reason_status, reason) in RAPL_REASONS {
+            assert!(!stdout.contains(reason), "a RAPL reason ({reason_status}) off Linux:\n{stdout}");
+        }
+    }
+    if cfg!(target_os = "macos") {
+        assert_eq!(
+            available,
+            status == "Live",
+            "on macOS the meter is available exactly when IOReport is Live:\n{stdout}"
+        );
+        // The reason is derived from the status the process acted on: it must
+        // be the printed status's own, and no other status's.
+        for (reason_status, reason) in IOREPORT_REASONS {
+            if stdout.contains(reason) {
+                assert_eq!(
+                    reason_status, status,
+                    "the CLI printed ioreport_status={status} but gave the reason for {reason_status}:\n{stdout}"
+                );
+            }
+        }
+        if declined {
+            let (_, reason) = IOREPORT_REASONS.iter().find(|&&(s, _)| s == status).expect("a known status");
+            assert!(
+                stdout.contains(reason),
+                "the meter declined with ioreport_status={status}, but not for that status's reason ({reason:?}):\n{stdout}"
+            );
+        }
+    } else {
+        // Off macOS there is no IOReport: the status is always Unavailable,
+        // and no IOReport reason is ever given.
+        assert_eq!(status, "Unavailable", "an IOReport status other than Unavailable off macOS:\n{stdout}");
+        for (reason_status, reason) in IOREPORT_REASONS {
+            assert!(
+                !stdout.contains(reason),
+                "an IOReport reason ({reason_status}) off macOS:\n{stdout}"
+            );
+        }
+    }
+    if declined {
+        assert!(
+            !stdout.contains("HwShunt"),
+            "the meter declined, yet the output claims a hardware reading:\n{stdout}"
+        );
+        assert!(
+            !stdout.contains("idle noise"),
+            "the meter declined, yet the output blames a noisy machine:\n{stdout}"
+        );
+        assert!(
+            !stdout.contains("--measure: metering a real"),
+            "the meter declined, yet the CLI metered:\n{stdout}"
+        );
+        assert!(
+            stdout.contains("The figures above stay ModelBased"),
+            "a declined meter must leave the ModelBased figures standing:\n{stdout}"
+        );
+    } else {
+        assert!(
+            stdout.contains("--measure: metering a real 16-variable T0 proof") && stdout.contains("  measured: "),
+            "neither a declined meter nor a measurement in the output:\n{stdout}"
+        );
+    }
+}

proof/proof-rs/crates/proof-schema/src/lib.rs

@@ -101,8 +101,22 @@ impl Tier {
 /// How honest an energy reading is (SPEC §5) — the family's provenance model.
 #[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
 pub enum Provenance {
-    /// Read from a hardware energy interface (RAPL/NVML/SMC/shunt). Requires a
+    /// Read from a hardware energy interface: a shunt or power meter, the SMC,
+    /// or a vendor energy counter (RAPL, NVML, Apple IOReport, ...). Requires a
     /// present `measured_uj`.
+    ///
+    /// A vendor counter's reading is a hardware reading; what it lacks is
+    /// independent provenance, not accuracy. It is subject to the liveness
+    /// requirement of SPEC §5: a reading from a vendor energy counter (RAPL,
+    /// NVML, Apple IOReport, ...) MAY be graded as a hardware reading only
+    /// while the counter is demonstrably live for the domain the figure
+    /// claims: the implementation MUST have observed the counter covering that
+    /// domain advance under load (for Apple IOReport: the CPU energy rail
+    /// itself advancing in at least 5 sample intervals, in at least 4 of every
+    /// 5, over at least 300 ms while the probing thread burns CPU). A counter
+    /// that is present but not live - frozen, or republished in lumps - MUST
+    /// NOT produce a hardware-graded figure; the implementation falls back to
+    /// its estimator or reports the work unmetered, and SHOULD record why.
     HwShunt,
     /// Computed from a calibrated per-operation model (e.g. wall time × a power
     /// model). `measured_uj` may be absent.
@@ -150,7 +164,8 @@ impl Energy {
             provenance: Provenance::Estimator,
         }
     }
-    /// A true hardware reading.
+    /// A true hardware reading. For a vendor energy counter, only while it is
+    /// live for the domain the figure claims ([`Provenance::HwShunt`]).
     pub fn measured(uj: u64) -> Self {
         Energy {
             measured_uj: Some(uj),