ns_to_uj prices an attempt at wall time × a fixed ~15 W that no host calibrated, and Propositional, Z3Smt, LeanVerifier and every Z3Server attempt that is not sealed as a tree reading graded that figure ModelBased. By the JCP ladder (SPEC §5.1) and the proof SPEC's own definition a model earns ModelBased by its calibration; an assumed power scaled by time is an estimate, so the figure claimed better provenance than how it was obtained. - proof-schema: Energy::estimator(uj), and Provenance docs that say a default or assumed parameter makes a figure Estimator. - proof-solvers: DEFAULT_ACTIVE_MILLIWATTS (15 W, same arithmetic) and wall_time_estimate; all four sites now Energy::estimator. The public Modelled / modelled_uj names are kept; their docs say estimate. - Tests that pinned the over-claim now pin Estimator: grade_attempt's unit tests, z3_tree.rs (server(), refuted goal, settle bound, cascade total [Estimator, HwShunt] -> Estimator, undeclared z3), and proof-cli tests/measure.rs (receipt "provenance Estimator", "stay Estimator"). New test: every wall-time rung (T0 proved/refused, one-shot z3, an absent Lean) is Estimator with no measurement. - proof-cli, proof-cascade, proof SPEC §5 / README, and joule-code-remediate (FormalOutcome docs, joule_fix's printed label) say Estimator. proof/conformance/v1 is unchanged: gen-vectors output is byte-identical (it seals the stand-in ladder's estimate_tier figures, never ns_to_uj). Co-Authored-By: Claude Opus 5.5 <[email protected]>
275 lines
14 KiB
Rust
275 lines
14 KiB
Rust
//! `proof --measure`, end to end: when every hardware source declines, the
|
||
//! output names the reasons, nothing in it claims a hardware reading, and the
|
||
//! cascade's own Estimator figures stand; when a source meters, the output
|
||
//! names the source, its HwShunt figure and its domain, and the sealed receipt
|
||
//! is unchanged. 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 counter could disagree.
|
||
//!
|
||
//! The printed statuses are themselves checked against what the process did
|
||
//! with them. Each reason the CLI gives comes from the status it acted on, so
|
||
//! every reason in the output must be the one for its printed status, the
|
||
//! source must be the first live one in order, and a declined meter must
|
||
//! print every source's reason: a CLI that prints one status and acts on
|
||
//! another fails here, whichever status either one is.
|
||
//!
|
||
//! One check is against the hardware: on macOS this test's own process reads
|
||
//! its own CPU energy counter (its own binding of `proc_pid_rusage`) while it
|
||
//! burns CPU. Where that counter keeps moving, the CLI must have metered with
|
||
//! its process counter and printed a non-zero HwShunt figure.
|
||
|
||
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 IOReport is not used (`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 process-counter `CounterStatus` the CLI can print, each with its
|
||
/// reason on macOS.
|
||
const PROCESS_REASONS: [(&str, &str); 4] = [
|
||
("Unavailable", "CPU energy counter (proc_pid_rusage, ri_energy_nj) could not be read"),
|
||
("Absent", "CPU energy counter is absent"),
|
||
("Frozen", "CPU energy counter did not keep advancing"),
|
||
("Live", "CPU energy counter is live, but the measurement 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"),
|
||
];
|
||
|
||
/// Every reason of `table` in the output must be its printed status's own.
|
||
fn reasons_match(stdout: &str, table: &[(&str, &str)], printed: &str, what: &str) {
|
||
for (reason_status, reason) in table {
|
||
if stdout.contains(reason) {
|
||
assert_eq!(
|
||
*reason_status, printed,
|
||
"the CLI printed {what}={printed} but gave the reason for {reason_status}:\n{stdout}"
|
||
);
|
||
}
|
||
}
|
||
}
|
||
|
||
/// The reason `table` gives for `printed`.
|
||
fn reason_of<'a>(table: &[(&'a str, &'a str)], printed: &str) -> &'a str {
|
||
table.iter().find(|(s, _)| *s == printed).map(|(_, r)| *r).expect("a known status")
|
||
}
|
||
|
||
#[cfg(target_os = "macos")]
|
||
mod oracle {
|
||
use std::os::raw::c_int;
|
||
use std::time::{Duration, Instant};
|
||
unsafe extern "C" {
|
||
fn proc_pid_rusage(pid: c_int, flavor: c_int, buffer: *mut [u64; 58]) -> c_int;
|
||
fn getpid() -> c_int;
|
||
}
|
||
|
||
/// `ri_energy_nj` of `proc_pid_rusage(getpid(), 6)`, read at byte 336.
|
||
fn energy_nj() -> Option<u64> {
|
||
let mut buf = [0u64; 58];
|
||
// SAFETY: buf is 464 writable bytes, the size of rusage_info_v6.
|
||
(unsafe { proc_pid_rusage(getpid(), 6, &mut buf) } == 0).then_some(buf[42])
|
||
}
|
||
|
||
/// This test process's own counter, read every ~25 ms for 600 ms while
|
||
/// this thread burns CPU between reads: (reads, reads at which it had
|
||
/// changed), or `None` if it cannot be read.
|
||
pub fn watch() -> Option<(u32, u32)> {
|
||
let mut prev = energy_nj()?;
|
||
let (mut reads, mut changes) = (0u32, 0u32);
|
||
let start = Instant::now();
|
||
while start.elapsed() < Duration::from_millis(600) {
|
||
let t = Instant::now();
|
||
let mut acc = 0u64;
|
||
while t.elapsed() < Duration::from_millis(25) {
|
||
acc = std::hint::black_box(acc.wrapping_add(1));
|
||
}
|
||
let now = energy_nj()?;
|
||
reads += 1;
|
||
changes += u32::from(now != prev);
|
||
prev = now;
|
||
}
|
||
Some((reads, changes))
|
||
}
|
||
}
|
||
|
||
#[test]
|
||
fn measure_names_its_source_or_why_it_declined_and_leaves_the_receipt_alone() {
|
||
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 printed = |key: &str, table: &[(&str, &str)]| {
|
||
let v = field(&stdout, key).unwrap_or_else(|| panic!("proof --measure did not print {key}:\n{stdout}"));
|
||
assert!(table.iter().any(|&(s, _)| s == v), "proof --measure printed an unknown {key}{v:?}:\n{stdout}");
|
||
v.to_string()
|
||
};
|
||
let status = printed("ioreport_status=", &IOREPORT_REASONS);
|
||
let process = printed("process_energy_status=", &PROCESS_REASONS);
|
||
let rapl = printed("rapl_status=", &RAPL_REASONS);
|
||
let source = field(&stdout, " · source=").unwrap_or_else(|| panic!("no source printed:\n{stdout}")).to_string();
|
||
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} source={source} process_energy_status={process} \
|
||
ioreport_status={status} rapl_status={rapl}"
|
||
);
|
||
if let Some(line) = stdout.lines().find(|l| l.trim_start().starts_with("measured: ")) {
|
||
eprintln!("proof --measure: {}", line.trim());
|
||
}
|
||
|
||
// The sealed receipt is the cascade's own figure for the FIRST goal, on
|
||
// every branch: the first row's figure, Estimator (wall time × a default
|
||
// power no host calibrated), never the --measure figure.
|
||
let first_row_uj: u64 = stdout
|
||
.lines()
|
||
.find(|l| l.trim_start().starts_with("T0:automation"))
|
||
.and_then(|l| l.split_whitespace().nth(1))
|
||
.and_then(|n| n.parse().ok())
|
||
.unwrap_or_else(|| panic!("no first goal row:\n{stdout}"));
|
||
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_eq!(receipt_uj, first_row_uj, "the receipt is not the first goal's own figure: {receipt}\n{stdout}");
|
||
assert!(receipt.contains("provenance Estimator"), "the receipt's provenance changed: {receipt}");
|
||
assert!(receipt.contains("closed at T0:automation"), "the receipt is not the first goal's: {receipt}");
|
||
|
||
assert_eq!(declined, !available, "the CLI's output disagrees with the decision it printed:\n{stdout}");
|
||
assert_eq!(available, source != "none", "available={available} but source={source}:\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!(source, if rapl == "Live" { "Rapl" } else { "none" }, "on Linux the source is RAPL exactly when Live:\n{stdout}");
|
||
reasons_match(&stdout, &RAPL_REASONS, &rapl, "rapl_status");
|
||
if declined {
|
||
assert!(stdout.contains(reason_of(&RAPL_REASONS, &rapl)), "declined without RAPL's 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") {
|
||
// The first live source, in order: the process counter, then IOReport.
|
||
let want = if process == "Live" {
|
||
"ProcessEnergy"
|
||
} else if status == "Live" {
|
||
"IoReport"
|
||
} else {
|
||
"none"
|
||
};
|
||
assert_eq!(source, want, "process_energy_status={process} ioreport_status={status}, yet source={source}:\n{stdout}");
|
||
reasons_match(&stdout, &IOREPORT_REASONS, &status, "ioreport_status");
|
||
reasons_match(&stdout, &PROCESS_REASONS, &process, "process_energy_status");
|
||
if declined {
|
||
assert!(stdout.contains(reason_of(&IOREPORT_REASONS, &status)), "declined without IOReport's reason:\n{stdout}");
|
||
assert!(stdout.contains(reason_of(&PROCESS_REASONS, &process)), "declined without the process counter's reason:\n{stdout}");
|
||
}
|
||
if source == "IoReport" {
|
||
assert!(
|
||
stdout.contains("CPU energy counter not used: ") && stdout.contains(reason_of(&PROCESS_REASONS, &process)),
|
||
"IOReport metered, but the CLI did not say why the process counter was not used:\n{stdout}"
|
||
);
|
||
}
|
||
// Against the hardware: this process's own counter.
|
||
#[cfg(target_os = "macos")]
|
||
{
|
||
let seen = oracle::watch();
|
||
eprintln!("proof --measure: this test process's own counter (reads, changes) = {seen:?}");
|
||
if let Some((reads, changes)) = seen.filter(|&(r, c)| c >= 5 && c * 5 >= r * 4) {
|
||
assert_eq!(
|
||
source, "ProcessEnergy",
|
||
"this test's own process counter changed at {changes} of {reads} reads, yet the CLI metered with \
|
||
{source}:\n{stdout}"
|
||
);
|
||
} else {
|
||
assert_ne!(source, "ProcessEnergy", "the test's own counter did not keep moving ({seen:?}), yet:\n{stdout}");
|
||
}
|
||
}
|
||
} else {
|
||
// Off macOS there is no IOReport and no process counter: both are
|
||
// Unavailable, and neither reason is ever given.
|
||
assert_eq!(status, "Unavailable", "an IOReport status other than Unavailable off macOS:\n{stdout}");
|
||
assert_eq!(process, "Unavailable", "a process counter off macOS:\n{stdout}");
|
||
for (reason_status, reason) in IOREPORT_REASONS.iter().chain(&PROCESS_REASONS) {
|
||
assert!(!stdout.contains(reason), "an IOReport or process-counter 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 Estimator"),
|
||
"a declined meter must leave the Estimator 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}"
|
||
);
|
||
}
|
||
if source == "ProcessEnergy" {
|
||
let measured = stdout
|
||
.lines()
|
||
.find(|l| l.trim_start().starts_with("measured: "))
|
||
.unwrap_or_else(|| panic!("the process counter was selected, yet no measured line:\n{stdout}"));
|
||
let uj: u64 = measured
|
||
.trim_start()
|
||
.strip_prefix("measured: ")
|
||
.and_then(|r| r.split_whitespace().next())
|
||
.and_then(|n| n.parse().ok())
|
||
.unwrap_or_else(|| panic!("no figure in: {measured}"));
|
||
assert!(uj > 0, "the process counter metered a 2^16-row proof as {uj} uj: {measured}");
|
||
assert!(
|
||
measured.contains("provenance HwShunt") && measured.contains("source ProcessEnergy"),
|
||
"the process counter's figure is not graded HwShunt and named by its source: {measured}"
|
||
);
|
||
assert!(
|
||
stdout.contains("domain: this process's CPU energy") && stdout.contains("not other processes"),
|
||
"the process counter's figure was printed without its domain:\n{stdout}"
|
||
);
|
||
assert!(!stdout.contains("idle noise"), "the process counter has no idle baseline to blame:\n{stdout}");
|
||
assert_ne!(uj, receipt_uj, "the --measure figure leaked into the receipt:\n{stdout}");
|
||
}
|
||
}
|