Exact

Exact Union RegExp

Repository files (latest commit first)

Filename	Latest commit message	Latest commit date
Transaction Science a96c6154c4 proof: a live vendor counter's reading is HwShunt, and the docs say so ... The owner settled the grade question this branch left open: a vendor energy counter (RAPL, NVML, Apple IOReport) gives a real reading; what it lacks is independent provenance, not accuracy. So a figure read from a counter that is live for the domain it claims is HwShunt. proof-cli already tagged a --measure figure that way, but the crate still said elsewhere that a macOS reading was ModelBased, and the CLI's own comment called the grade "an open grade decision, not settled here". This commit makes the specification, the schema and the docs agree with the code, and adds the liveness requirement where the grades are defined. No behaviour changes; one test is tightened. What changed: - SPEC.md section 5 and proof-schema's Provenance::HwShunt doc. HwShunt now names vendor energy counters next to a shunt, a power meter and the SMC. Both carry the family's liveness MUST word for word: a vendor counter's reading MAY be graded as a hardware reading only while the counter is demonstrably live for the domain the figure claims, observed advancing under load (for Apple IOReport, the CPU energy rail itself, 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 spec adds that the fallback here is ModelBased or Estimator. Energy::measured's doc points at the requirement. No conformance vector is touched. - proof-cascade meter.rs. The module header said "a macOS reading is ModelBased, not a true coulomb-shunt HwShunt; Linux RAPL is the shunt-grade path". It now says a figure from this meter is HwShunt on both platforms, states the liveness condition, and says what each platform does about it. The docs on measure_marginal_uj and power_over say the same, and power_over's doc gives the probe's thresholds. The Linux section is new and honest about a gap: there is no liveness probe for RAPL. It is selected whenever a zone is readable, a frozen counter gives Some(0), which is not a figure, and nothing tells a counter that tracks the load from one that drops a lump into the busy window. - meter.rs's RAPL comment said energy_uj is "world-readable on most distros". It has not been since late 2020: kernel commit 949dd0104c49 ("powercap: restrict energy meter to root access", 5.10, backported to stable) made it root-only as the CVE-2020-8694 / PLATYPUS mitigation. An unprivileged process usually reads no zone, so the meter declines unless it runs as root or read access has been granted. - proof-cli main.rs. The module doc called T0 and T1 "both real with measured energy". Their energy is proof-solvers' wall time x a ~15 W power model, tagged ModelBased. It also said "T2/T3 reference stand-ins", but the CLI runs resident_z3_ladder, which has no T2/T3 rung. Those three goals come back unproved, as `proof` prints ("proved 6/9 ... T2=0 T3=0"). Both are fixed, and the --measure comment now states the grade. - proof/README.md. It said `--measure` gives an HwShunt reading "where an energy interface is present". It now says where the meter produces one, which on Apple Silicon needs a CPU rail seen to be live. It adds that on the Macs measured so far (macOS 27.0.1, M5 Max and M3 Ultra) --measure declines and every figure stays ModelBased, and that RAPL is root-only on Linux. It no longer says the solver rungs have "measured energy". It no longer says clippy is warning-free: that holds for the Linux target, but on macOS proof-cascade's IOReport FFI has two lints. (The "via macmon" text was already gone in bedef9b0.) - proof-cli tests/measure.rs. bedef9b0 had already moved this test off a second probe in the test process and onto the decision the CLI prints. But the printed status was tied to the CLI's behaviour for only two of its four values. A CLI that printed ioreport_status=CpuRailAbsent while acting on CpuRailFrozen passed: run against the unmodified test at 906ed1a6, it gave "ok. 1 passed". Now every IOReport reason in the output must belong to the printed status. A declined meter must print its own status's reason. The status must be one of the four. Off macOS it must be Unavailable, with no IOReport reason. Verified on the M5 Max (macOS 27.0.1, z3 present). The whole proof-rs workspace passes: proof-cascade 68, ioreport_once 1, ioreport_unopenable 1, measure 1, conformance pack 4 + soundness 5 + lib 1, receipt 8, schema 6, solvers 11. proof-conformance prints "all checks passed". The measure test passed 3 runs, each "declined=true available=false ioreport_status=CpuRailFrozen". clippy --no-deps --tests shows only the two existing proof-cascade lints, meter.rs's duplicated #[link] attribute and its hand-built nul-terminated string. It is clean for x86_64-unknown-linux-gnu, which type-checks the test's off-macOS branch but does not run it. rustdoc reports no warnings. Falsified, each mutation restored from a saved copy and its hash checked afterwards: - the CLI prints IoReportStatus::CpuRailAbsent in place of the status it used: "the CLI printed ioreport_status=CpuRailAbsent but gave the reason for CpuRailFrozen"; - prints Unavailable: "... printed ioreport_status=Unavailable but gave the reason for CpuRailFrozen"; - prints Live: "on macOS the meter is available exactly when IOReport is Live"; - prints !available: "the CLI's output disagrees with the decision it printed"; - the frozen reason is replaced by a generic one: "the meter declined with ioreport_status=CpuRailFrozen, but not for that status's reason". Not done here: - a RAPL liveness probe. Under the new MUST, the Linux path's only evidence is the bracket. Co-Authored-By: Claude Opus 5.5 <[email protected]>		2026-09-30 20:01:24 -04:00
..
src	proof: a live vendor counter's reading is HwShunt, and the docs say so	2026-09-30 20:01:24 -04:00
Cargo.toml	Add the proof open standard — a carrier for verified work	2026-06-07 15:30:07 -04:00