proof-cascade: never meter CPU work through an IOReport CPU rail that does not keep moving #115

Merged

dcharlot merged 10 commits from proof-cascade/cpu-rail-liveness into main 2026-10-01 05:50:51 -04:00

Conversation 0 Commits 10 Files changed 11 +5157 -292

2026-09-30

Transaction Science

proof-cascade: IOReport is a hardware reading only while every CPU rail it sums keeps advancing ...

The IOReport watch, `CPU_RAILS`, was "any one": Live as soon as ONE CPU rail
met the sustained-advance rule. The power reading sums every CPU rail
(`counts_once`), and on a multi-die part that is two rails, `DIE_0_CPU
Energy` and `DIE_1_CPU Energy` on an M3 Ultra. So one die live beside a
frozen one would have admitted the meter and bracketed one die's energy as
the whole CPU's, as `HwShunt`. RAPL was already held to every package
counter it sums (9334ec0c); IOReport now is too.

The rule: Live only when every CPU rail present in the samples advanced in
at least five intervals, in at least 80% of those observed, over at least
300 ms; Frozen otherwise; Absent with no CPU rail. A rail is present if it is
in any sample, the first included (the watch already registered every
sample's rails; a test now pins it), and is judged over every interval
observed. With every source on the same rule there is nothing for
`Watched.every` to choose, so the field is gone: a `Watched` is which
channels to watch, and the watch needs every one of them.

Two test-side checks encoded the old rule and now encode this one: the
oracle behind the real-IOReport tests says "moved" only when every CPU rail
it reads changed at five reads or more and at 80% of them, and
`assert_verdict_matches_record`, the tests' own reading of a probe record,
calls a run Live only when every CPU rail seen, the first sample's included,
rose in at least 5 intervals at 80% over 300 ms. The oracle reads exactly the
probe's rails on both hosts: one on this M5 Max, the two dies on the M3
Ultra.

Docs: the meter module doc, `IoReportStatus`, `CpuRail`, `Watched`,
`CPU_RAILS`, `RailWatch` and `PACKAGES`; SPEC §5's liveness clause (for
IOReport, every CPU rail the figure sums, one per die, must advance on its
own); the proof README.

Tests, all scripted (macOS here). The rule:
`watch_two_dies_that_both_keep_advancing_is_live` (live at the tenth
interval, or at the fifteenth when one die misses its first three, either
die), `watch_one_die_that_keeps_advancing_beside_a_frozen_one_is_frozen` (the
other die held, stepped once, stepped five times, or advanced three
intervals in five, either die; and twin `CPU Energy` channels),
`watch_one_die_alone_that_keeps_advancing_is_live`, and
`watch_a_die_in_only_some_samples_is_a_rail_the_watch_needs`. The whole probe
loop: `the_probe_needs_every_die_to_keep_advancing`. The real `host_status()`
on scripted reads: `host_status_calls_two_dies_that_keep_advancing_live` and
`host_status_calls_one_live_die_beside_a_frozen_one_frozen`. The single-rail
tests are unchanged. Two existing tests encoded "any one":
`two_advances_of_the_same_rail_are_not_live_and_sustained_ones_are` held
DIE_0 constant and expected Live from DIE_1 alone, so DIE_0 now advances at
every interval and the verdict is still DIE_1's; and
`rapl_every_package_counter_must_keep_advancing` drops its contrast with the
any-one-rail watch, which no longer exists.

proof-cascade: 86 lib tests and the three integration files pass on this M5
Max. The same lib test binary passes 86/86 on the M3 Ultra (macOS 27.0.1),
where the real probe gave `CpuRailFrozen` over 25 and 26 intervals and the
oracle saw 0 changes on both dies in 19 reads. `cargo test --workspace`
passes (126 tests) and the proof-conformance binary passes all 10 checks.
Clippy adds nothing for aarch64-apple-darwin (two warnings in the IOReport
FFI predate this) and is clean for x86_64-unknown-linux-gnu.

Falsified, each restored from git and the suite re-run green: the rule back
to any one rail fails the one-live-die-beside-a-frozen-one tests (rule, loop
and `host_status`), the two-live-dies test, the some-samples test, the
updated two-advances test and the RAPL every-package test; registering a
rail only once an interval has closed fails
`watch_a_die_in_only_some_samples_is_a_rail_the_watch_needs`.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

0503e69b32

• View at this point in history

2026-09-30 21:33:56 -04:00

Transaction Science

proof-cli: "the same verified output" charges the baseline only for the goals proved ...

The headline said, on one run, "energy 375387 uj vs 450000000 uj frontier-only
→ 1198.762× less for the same verified output". The 450 J baseline charged a
frontier model for all nine goals; the cascade proved six. The three it did
not prove produced nothing, so the comparison was not for the same output: it
credited the cascade with 150 J of frontier work it never replaced.

`EnergySummary` gains `proved_baseline_uj`, the frontier-only baseline summed
over the proved goals alone, and `proved_ratio_milli()`, that baseline over
EVERY joule the cascade spent, the goals it failed on included, in thousandths
rounded down (`None` when nothing was spent; `Some(0)` when nothing was
proved). Both sides are charged conservatively: the frontier run only for the
output it would have to match, the cascade for its failures too. The existing
`baseline_uj` and `energy_ratio_milli()` are unchanged (the conformance check
C3 and the receipt wire use them), and their docs now say they charge every
goal.

The CLI now prints, verbatim from one run (the T1 figures are wall-time
models of a resident z3 and vary several-fold between runs):

  proved 6/9 · tiers T0=4 T1=2 T2=0 T3=0
  energy 58892 uj for all 9 goals  vs  300000000 uj frontier-only for the 6 proved  →  5094.070× less for the same verified output
  (frontier-only for all 9 goals: 450000000 uj, 7641.105× — but 3 of them were not proved here, so not the same output)

The all-goals figure stays, with its goal count, and is never called the same
output; with nothing proved, or nothing spent, the CLI says so instead of
printing a ratio.

Tests:
- `the_same_output_ratio_charges_the_baseline_only_for_proved_goals` (cascade):
  three goals, two proved, with the tests' own literals (T0 50 uJ, T1 5 mJ,
  T3 50 J): the same-output baseline is 2 × 50 J, the ratio is exactly
  100,000,000,000 / 10,150 = 9,852,216 thousandths, below the all-goals ratio;
  a cache hit is a proved goal for zero joules; nothing spent gives no ratio,
  nothing proved gives zero.
- `tests/headline.rs` (CLI): runs `proof` and checks the printed figures
  against the per-goal rows of the same run — the total is the sum of the rows,
  the same-output baseline is (proved rows) × 50 J, the all-goals one is (rows)
  × 50 J with the unproved count, both ratios are the printed baselines × 1000 ÷
  the total, rounded down, and "same verified output" is claimed exactly once,
  on the proved-goals line.

Falsified: printing the all-goals baseline and ratio on the same-output line
fails the CLI test ("the same-output baseline is 6 x 50 J"); charging the
proved baseline for every goal fails both tests. Each restored through git.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

4551c5f9a4

• View at this point in history

2026-09-30 20:40:11 -04:00

Transaction Science

proof-cascade: RAPL is a hardware reading only while every package counter keeps advancing ...

SPEC §5 says a vendor energy counter is a hardware reading only while it is
demonstrably live for the domain the figure claims. The macOS path enforces
that for IOReport's CPU rail; the Linux path did not. `hardware_meter_available`
selected RAPL whenever any `intel-rapl:<n>/energy_uj` was readable, and the
module doc admitted it: "On Linux there is no such probe." A counter that holds,
or republishes in a lump inside the busy window, would have been bracketed and
graded HwShunt.

RAPL now goes through the same probe loop and the same sustained-advance rule
as IOReport: while the probe burns 25 ms of its own thread's CPU before each
re-read, a counter is live only if it advanced in at least five sample
intervals, in at least 80% of the intervals observed, over at least 300 ms. The
domain is the package: the rule watches the zones whose `name` is
`package-<n>`, and because the figure sums all of them, EVERY package counter
must meet it (IOReport needs one CPU rail of either die; RAPL needs each
counter it adds up). A decrease (a wrap) is not an advance. `rapl_status()` is
probed once per process behind a `OnceLock` and cached; the selection and
`rapl_power_over` gate on it through `admits_counter`, which admits only
`Live`, so a counter that is readable but not live yields `None` before any
window runs and the work never runs. The new public `CounterStatus`
(`Unavailable`, `Absent`, `Frozen`, `Live`) says why, and `proof --measure`
prints `rapl_status=` beside `ioreport_status=` and gives the RAPL reason on
Linux.

The figure itself changes in one place: it sums the package zones only.
Before, every readable top-level zone was summed, and on machines that expose
`psys` (the platform zone, which covers the package) that counted the package
energy twice. `psys` is neither summed nor probed now.

To share the machinery rather than copy it: the thread CPU clock, the wall
clock and the burn tick move out of the macOS-only IOReport module into a
`probe_clock` module built on macOS and Linux (CLOCK_THREAD_CPUTIME_ID is 16
on macOS, 3 on Linux). `RailWatch` takes a `Watched` — which channels, and one
or every one — whose default is the IOReport CPU rails with "any one", so the
IOReport rule and every IOReport test are unchanged. `probe_with` is now
`probe_watching(CPU_RAILS, ..)`. The RAPL composition, `rapl_probe_with`, is
generic over its zone reader, so the tests run that very composition on
scripted zones on every platform.

Tests (all pure and scripted, run here on macOS):
- a package counter advancing at every read is Live at the twelfth 25 ms
  interval, and the rule was handed each value as read;
- constant, one-step and two-step counters are Frozen after the whole budget;
- one package advancing and one holding is Frozen — the same reads under the
  any-one-rail rule are Live, which pins what `every` decides — both advancing
  is Live, and two packages advancing in alternate intervals are Frozen;
- a moving `psys` beside a holding package is Frozen, and zones with no package
  are Absent; a wrap that then holds is Frozen;
- no readable zone is Unavailable with no read or tick, and zones readable only
  at the open give no verdict after the five-budget cap;
- the status maps one to one and only `Live` meters: declined statuses run no
  bracket and no work;
- the package name and the read: `package-<n>` only, each package counter with
  its own value, `psys` left out;
- `tests/rapl_once.rs`: eight threads asking at once see one status, and on
  Linux the production probe ran once (off Linux: Unavailable, zero runs).

Falsified, each restored through git before the next: RAPL's `every` set to
"any" fails the every-package test; reading `psys` into the sample fails the
read and psys tests; watching IOReport's CPU rails instead of the package
counters fails five tests; mapping Frozen to Live fails five; admitting every
status fails four.

`cargo test --workspace` and the proof-conformance binary pass on macOS (M5
Max, macOS 27.0.1). The Linux path is compile-checked only:
`cargo check --workspace --tests` and `cargo clippy --workspace --all-targets`
for x86_64-unknown-linux-gnu are clean. Not run on Linux here, so the real
sysfs reader and the Linux-only gate (`hardware_meter_available` and
`rapl_power_over` gating on the cached status) have no runtime test; a mutation
of that gate cannot be caught on macOS.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

9334ec0c21

• View at this point in history

2026-09-30 20:39:39 -04:00

Transaction Science

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]>

a96c6154c4

• View at this point in history

2026-09-30 20:01:24 -04:00

Transaction Science

proof-cascade: a rail is live only if it keeps advancing, never on a two-step refresh ...

The liveness rule said Live once the same CPU rail advanced in two separate
sample intervals. That was meant to stop a batch refresh (one step, then a
hold) from vouching for a frozen rail. But a refresh is not always one step.
On an M5 Max running macOS 27.0.1, the jouleclaw-energy verifier ran a
group-only watcher that sampled the Energy Model group every ~16 ms. It saw
`CPU Energy` go 2,643,843,378 -> 2,705,607,863 (+61,764,485), then 64 ms
later -> 2,705,611,298 (+3,435). `MCPU0`, `MCPU1` and `PCPU` each stepped
twice with it. The probe's intervals are ~31 ms, so a probe window that
holds such a refresh sees the rail advance in two intervals and says Live.
That answer is cached for the process. There, two real probes said Live
while the oracle saw no sustained movement, at the time of a refresh.
Refreshes come ~30 minutes apart, so this is rare. But it is exactly the
failure the rule exists to prevent: the meter is selected over a frozen
rail, and every later refresh lands whole in some bracket.

The rule, the same in all five crates that carry it. Live iff, after some
interval, the same CPU rail (name + ordinal):
- advanced in at least MIN_LIVE_ADVANCES = 5 separate intervals;
- advanced in at least 80% of all intervals seen so far
  (advances * 5 >= intervals * 4);
- was watched for at least MIN_LIVE_WINDOW = 300 ms of wall clock since
  the first sample.
The rule is checked after each interval. Live is declared, and the probe
stops, the first time all three hold. The pure rule now takes each sample's
wall-clock reading. The probe passes the read's `end`, and the tests script
the clock. Sampling goes on until Live, or until the 1 s budget has passed
and at least 5 intervals were seen. The hard cap stays at 5 budgets. On a
quiet M5 Max a live rail is now called live after ~10 intervals (~310 ms),
not 2.

Unchanged: per-rail keys; consecutive samples; a decrease or a first
appearance is not an advance; one advance per rail per interval; the
group-only subscription; the thread-CPU tick; the pure status mapping; the
OnceLock cache; the F9 fault hooks; proof-cli's messages; the RAPL per-zone
wrap code; and the "ioreport liveness: status=" log line.

The oracle. It called a rail moving after 2 changes, so a two-step refresh
in its window could vouch for a false Live. Now it calls a rail moving only
if the rail changed at 5 or more of its reads and at 80% or more of them.
Its count moves into an `OracleTally` that the tests feed scripted reads.
It still extends its window while it has fewer than 5 reads, but the cap is
now 8 budgets (was 3). Under contention it needed up to 6.8 s of the old
9 s cap to get 5 reads. Too few reads is still a failure, never a "not
moved".

Tests. Those marked (*) fail under the old rule.
- (*) The observed two-step refresh, with MCPU0/MCPU1/PCPU stepping beside
  it. Frozen after the whole budget: in the pure loop, in the composition,
  and in the real `host_status()` on scripted reads (CpuRailFrozen).
- (*) A refresh in 3, 4 or 5 steps within its first 150 ms, back to back or
  spread out: Frozen.
- (*) The M3 Ultra shape, where DIE_0 and DIE_1 each step twice within
  64 ms: Frozen.
- (*) Two advances of one rail over 300 ms: not live. Five advances in six
  intervals over 600 ms: live.
- A rail that advances every 31 ms interval is Live at the tenth (310 ms).
  It is not Live after 5 advances (155 ms) or 9 (279 ms), and it stays Live.
- A rail missing one interval in five is Live at exactly 80% (8 of 10). One
  missing two in five is never Live. One that missed two of its first five
  is not yet Live at intervals 7-9, where the count and window are already
  met, and is Live at the tenth.
- On a loaded host (100 ms intervals), Live comes at the fifth interval
  (500 ms), not the third (300 ms).
- The probe keeps sampling past the budget while it has fewer than 5
  intervals and stops at 5. It stops at the cap with 3.
- The oracle's bar, on scripted reads: a one- or two-step refresh is never
  "moved".
Scripts whose meaning changed were rewritten so they still catch what they
were written for:
- "Two advances -> Live" became a sustained-advance script. It must be Live
  after 5 or more intervals and 300 ms or more of the real clock, at the
  first interval where the tests' own reading of the record says so.
- The one-step-per-die scripts became two dies that advance in alternate
  intervals, so a sum of the rails advances every interval and fails.
- The decrease and first-appearance tests now come after four advances over
  400-500 ms.
- The record test pins which wall reading the rule gets.
`assert_verdict_matches_record` recomputes the new rule with the tests' own
literals, and checks that a Live run stopped at the first interval that met
it.

Mutations. Each was a temporary edit, restored with git checkout; the tree
was clean after each.
- The old rule (2 advances, no share check, no window): 21 lib tests fail,
  including every (*) test, e.g. "a two-step refresh counted as a live rail:
  Run { verdict: Some(Live), intervals: 4, ...".
- MIN_LIVE_ADVANCES = 2: 7 fail. For one, the loaded host is "Run { verdict:
  Some(Live), intervals: 3, samples: 4, took: 300ms".
- Share check removed: 6 fail, e.g. "a rail advancing in 60% of intervals
  counted as live" and "a refresh in steps [1, 2, 3, 4, 5] counted as live:
  Run { verdict: Some(Live), intervals: 10, ...".
- Window check removed: 8 fail, e.g. "a refresh in steps [1, 2, 3, 4, 5]
  counted as live: Run { verdict: Some(Live), intervals: 5, samples: 6,
  took: 150ms" and "Live after 127.469542ms of window".
- Oracle back to ">= 2 changes": "two steps in consecutive reads: the
  oracle called a refresh moving".

Runs.
- proof-cascade tests, 3 times, beside an all-channel IOReport sampler
  (150-570 ms a sample on this loaded host): 68 + 1 + 1 passed each time,
  e.g. "status=CpuRailFrozen oracle=CpuRailMoved(false) selected=false
  probe_intervals=29 ... oracle_reads=5". The sampler was killed after each
  run.
- M3 Ultra (macOS 27.0.1): the lib test binary was built here, run once,
  then deleted. 68 passed, with "status=CpuRailFrozen
  oracle=CpuRailMoved(false) selected=false probe_intervals=27 ...
  oracle_reads=20".
- The proof-rs workspace is green, and proof-conformance prints "all checks
  passed". clippy --no-deps shows no new warnings; the two in proof-cascade
  were already there.

Not done here:
- The Live branch is tested only on scripted rails. Neither Mac exposes a
  live CPU rail to an unprivileged reader, so a real Live has not been
  seen.
- The other four crates that carry this rule get it in their own commits.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

906ed1a60f

• View at this point in history

2026-09-30 18:54:00 -04:00

Transaction Science

proof-cascade: one counted production probe, pinned on what it was handed ...

The re-verification of 79375a1c left the decision rules pinned but the
production chain around them loose: a wall-clock pin that flaked whenever
another process sampled IOReport, a run counter that counted cache
initialisations, an unopened subscription that could be mapped straight to
Live inside probe() or the cache, and no pin on the values between the FFI
reader and the rule (a sum of the CPU rails there survived on the M3 Ultra).
Those were the dangerous survivors. The fail-safe ones were a wrong clock id,
a stale reader and a reader that drops rails. Each now fails a test.

The chain. `host_status()` is the one production composition: it increments
REAL_PROBE_RUNS, then returns the pure `status_of` of
`probe_with(EnergyModelSub::open, EnergyModelSub::read, spin_tick,
wall_clock, thread_cpu_time, budget)`, with no branch. It is the only
production caller of `probe_with`. `ioreport_status()` caches it in one
process-wide OnceLock. `hardware_meter_available()` is
`admits(ioreport_status())`, and `power_over` and `measure_marginal_uj`
select only through it. `admits` accepts Live alone. `status_of` reads the
run's `opened` flag: a subscription that did not open is Unavailable whatever
verdict the run carries. `macos_ioreport::probe`, `available`, `cached_probe`
and `status_from` are gone.

Once per process. The concurrent test moved to tests/ioreport_once.rs, so
it is its process's first use of the meter. Eight threads released through a
Barrier ask for the status, the selection and measure_marginal_uj. The
counter must read 1, and each thread's warm calls must burn under 10 ms of
its own CPU. power_over is private, so the lib test
the_gated_entry_points_read_the_cached_status pins it, and the other two,
the same way on the calling thread's CPU.

Fault injection. #[cfg(test)] hooks inside the real opener and the real
reader (`seam`, per thread) let unit tests run the real, uncached
`host_status()`. With the group denied, it gives Unavailable with no read,
no tick and no verdict. On scripted channel reads, with the real tick and
clocks, a single batch jump, a constant rail, and one step on each die in
different intervals each give CpuRailFrozen. A rail that advances at every
read gives Live after two intervals. Each scripted run must have been handed
exactly the script. Measured on the tests' own clock, it must also have
burned at least 12.5 ms of CPU per tick. For the cache,
tests/ioreport_unopenable.rs drives the whole chain in a process of its own
after `simulate_no_energy_model_group()`, a doc-hidden hook that can only
turn the meter off. Four threads see Unavailable, no selection and no
figure, the work never runs, and the probe runs once.

Group-only, structurally (F1). Every sample the probe read listed only
Energy Model channels, exactly as many as the group has: 364 of 11,886 on the
M5 Max, and 645 of 14,345 on the M3 Ultra. The median thread CPU of a read
is under 50 ms; measured, 6-9 ms. The wall-clock median is logged, never
asserted. No wall-clock bound or ratio remains in these tests.

What the rule was handed (F4). The rule records, for every sample, the
(name, ordinal) keys and raw integers of every CPU rail and every `GPU
Energy` channel it was handed. A test runs `host_status()` uncached between
two all-channel oracle reads:
- the keys in every sample equal the oracle's Energy Model keys;
- a rail that held was handed exactly the oracle's value;
- a rail that moved was handed a value within the two reads.
For freshness, an independent watcher reads the group on its own thread.
Every GPU Energy rise it saw strictly between two probe reads must appear as
two different GPU values in the record. The FFI pin also asserts the key
sets and brackets the GPU rail. A raw-reader test alternates the group and
the all-channel subscriptions, so a reader that is stale for the process
fails whether or not anything moves.

Clocks (F3). The tests bind their own clock_gettime(16). The production
thread clock stays still across a 100 ms sleep, and while a helper thread
burns 100 ms as this thread waits. It moves with this thread's own burn, and
never by more than the tests' clock. Each production tick burns at least
25 ms of thread CPU by the tests' clock, unless it ran into the 500 ms wall
cap, and never more CPU than wall time. The probe's wall clock is checked
against Instant around a sleep.

Counting CPU energy once, the rule from eoc-meter 7aa42418. counts_once,
now pure and in `liveness`, summed per-cluster accumulators and CPU power
managers beside the `CPU Energy` aggregate they add up to:
- on the M5 Max, `PACC_*`, `MCPM*`, `PCPM` and their `_SRAM` rails;
- on the M3 Ultra, `DIE_n_*_CPM` and their `_CPM_SRAM` rails.
It now drops `PACC*`, `EACC*`, `MACC*` and `*CPM*`. A test pins this on both
chips' real channel names. It only matters on a live host, so no reading here
was affected. Also, `open()` now releases `subscribed` when the subscription
is null.

Falsified. Each mutation was applied, run and restored with git checkout.
git status was clean after each. Every one failed a test:
- compare with the first sample: 10 lib tests, e.g. "one refresh counted as
  a live rail";
- a decrease counts as an advance: "a decrease counted as an advance";
- no subscription -> Live inside host_status: "an unopenable Energy Model
  group left: Live". The CpuRailAbsent variant fails the same test;
- no subscription -> Live inside the cache: the lib tests pass, and
  ioreport_unopenable fails ("no Energy Model group, yet Live");
- a single advance -> Live inside host_status's read closure: "one refresh
  counted as a live rail";
- the sum of the CPU rails in host_status's read closure:
  - scripted, on any host: "one step on each die added up to a live rail";
  - on the M3 Ultra also "("DIE_0_CPU Energy", 0) held at 38945708 across
    the probe, yet it handed the rule 81077035";
  - inside probe_with: 3 tests;
- a no-op tick in host_status: "interval 0 of 92 consumed 27.584µs", and
  "host_status() ticked 2 times, yet this thread burned only 14.167µs".
  spin_tick as a no-op: "tick 0 burned 333ns";
- a per-thread cache: "the liveness probe ran 8 times";
- hardware_meter_available() probing uncached:
  - "hardware_meter_available() burned 1.007352584s of this thread's CPU";
  - "ran 17 times";
  - ioreport_unopenable: 9;
- power_over probing uncached: "a declined power_over burned 730.585083ms";
- the reader returns constant 0: "held at 2588973125 ..., yet the probe read
  0";
- stale readers:
  - process-wide at the FFI: "listed 364 channels for the group and 364 for
    every channel";
  - process-wide in EnergyModelSub: the GPU bracket;
  - per probe in the closure: "GPU Energy rose ... yet both handed the rule
    the same GPU value", and the scripted tests;
- the thread clock as CLOCK_MONOTONIC: "advanced 101.41ms while this thread
  slept 100 ms". As process CPU: 598.246ms;
- admits() accepting CpuRailAbsent: "no CPU rail admitted the meter";
- the probe subscribing to every channel: "sample 0 listed 11886 channels,
  some outside the Energy Model group".

Runs on this tree:
- M5 Max: the lib tests 5x while a helper process sampled every IOReport
  channel in a tight loop. Sibling suites' IOReport readers were also running
  on the host, at load 16-23. 5/5 passed, 58 each; the median read was
  6.1-8.8 ms of thread CPU, and the minimum interval 25.02-25.03 ms of thread
  CPU. The helper was killed on exit, and none remain.
- M3 Ultra, once: 58 passed, with "status=CpuRailFrozen
  oracle=CpuRailMoved(false) selected=false probe_intervals=26". The
  once-per-process and unopenable tests also pass there.
- The proof-rs workspace is green, and the proof-conformance binary prints
  "all checks passed".
- clippy reports only the two warnings that are also on origin/main.
- x86_64 Linux is compile-checked only.

Not done, deliberately:
- The oracle's evidence floor, at least 2 reads of every channel within at
  most 3x its window, is the one hardware assertion still sensitive to
  IOReport contention. Under the helper plus the sibling readers it got 2,
  the edge. It fails loudly rather than passing without evidence.
- GPU freshness is asserted only when the watcher saw GPU Energy rise between
  two probe reads, and the log says how many. With the GPU and CPU rails
  both idle, a reader made stale between the test hook and the FFI call, in
  EnergyModelSub, would survive. That is fail-safe: it can only decline.
- power_over and measure_marginal_uj are pinned warm on a declined host only.
  On a live one they do real sampling work.
- Which provenance grade a live IOReport reading earns, and a macOS CI job
  for this crate, are left for David.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

c085945c7a

• View at this point in history

2026-09-30 17:49:43 -04:00

Transaction Science

proof-cascade: the probe burns thread CPU time, and tests pin how it samples ...

The re-verification of bedef9b0 left four mutations alive. All four are in
how the probe samples, not in what it decides:
- an advance was any change (`now != before`), so a decrease counted;
- a rail missing from the previous sample counted as an advance;
- spin_tick slept instead of burning;
- the probe passed a no-op tick.
It also found two docs that claimed more coverage than the tests had.
two_advances_of_the_same_rail_are_live claimed to cover decreases and new
rails. MIN_PROBE_INTERVALS claimed to pin the ~25 ms tick. This commit makes
each of those fail a test, and applies the family's round-4 test design
(R1-R8).

R1, the tick. A tick now burns 25 ms of the probing thread's own CPU time,
read with clock_gettime(CLOCK_THREAD_CPUTIME_ID), with a cap of 500 ms of wall
time. Before, it spun for 25 ms of wall time, which gives the thread only a
fraction of that in CPU on a loaded host. The tick is still passed into the
generic loop, so the scripted tests keep their scripted ticks.

The probe's record. probe() now returns a ProbeRun: the verdict, the interval
count, whether the Energy Model subscription opened, and for every FFI sample
call, its wall time and the thread CPU clock just before and after the call.
The once-per-process cache keeps this record, so a test can check the run that
actually made the decision. Two pins read it; neither is a wall-clock ratio:
- R2, the probe burns CPU. In every interval, the thread CPU time between
  sample calls is at least PROBE_TICK/2. Host load cannot shorten a CPU-time
  burn. Only the 500 ms cap can, and the assertion message says so. A
  separate test checks that one tick burns at least PROBE_TICK.
- R3, the probe samples the group alone. The median wall time of the probe's
  own sample calls is under 50 ms (the group takes ~6-12 ms, every channel
  130-800 ms). This replaces the floor of at least 10 intervals. Under load
  the probe saw as few as 4 intervals (load average 92), which the old floor
  would have failed.
Both hardware tests check R2 and R3, one on the cached probe and one on a
fresh probe, and print the median.

R4, the FFI value pin. A new test places one probe sample between two
independent all-channel oracle reads, three times over. It matches each CPU
rail by group, name and ordinal. Where the oracle saw the rail hold, the
probe's value must be equal to it. Where the rail moved, the value must lie
between the two reads. On both hosts every rail held and matched exactly: M5
Max `CPU Energy` 1,863,990,848; M3 Ultra `DIE_0_` 28,237,793 and `DIE_1_`
30,845,042.

R5, oracle evidence. The oracle's window is extended, up to 3x, only while it
has fewer than 2 reads. If it still has fewer than 2 at the end, the test
fails. It never reports CpuRailMoved(false) from 0 or 1 reads.

R6, the pure rules, one test each:
- a decrease between consecutive samples is not an advance;
- a rail that is new in a sample only sets its baseline (a new name, or a
  second channel with the same name);
- an Energy Model subscription that cannot be opened, or never yields a
  sample, gives no verdict, which maps to Unavailable, never to Live or
  Absent. This goes through the new pure `liveness::probe_with`;
- no verdict is Unavailable (`no_verdict_is_unavailable`).
One behaviour changes. A host where IOReport opens but the Energy Model group
cannot be subscribed used to report CpuRailAbsent; it now reports Unavailable.
Both decline. The enum variants are unchanged, and the docs and proof-cli's
reason strings now say which status means what. The sampler's FFI code now
only reads each channel's (group, name, integer). Which channels are kept is
decided by the pure `energy_model_sample_from`, and a test checks that each
channel keeps its own value.

R7, the cache. STATUS_PROBE_RUNS was already a process-wide static
AtomicUsize. The cache test now releases 8 threads together through a Barrier.
Each asks for the status and selects the meter: hardware_meter_available and
available, and on a declined host also measure_marginal_uj and power_over.
The test asserts that the probe ran exactly once.

R8. the_ioreport_meter_is_never_available_on_a_frozen_cpu_rail still prints
"ioreport liveness: status=...". The line now also carries median_sample,
min_interval_cpu and oracle_reads.

Flake removals. The M5 Max is also the macOS CI runner and is often heavily
loaded, so three timing assertions are gone:
- the warm-cache `< 25 ms` check (the probe counter is the pin);
- the declined path's `took < 80 ms` check (the work-call count is the pin,
  and the time is still printed);
- the fixed 30 ms sleep in a_busy_window_with_no_reading_stops_its_workers
  (the test now waits until the workers have run).

Falsified. Each mutation was applied, run, and restored with git checkout,
with git status clean afterwards. Each one failed a test:
- a decrease counts (`now != before`): "a decrease counted as an advance";
- a new rail counts: "a rail's first appearance counted as an advance";
- no group subscription maps to Live, or to Absent: "left: (Some(Live), 0)" /
  "(Some(Absent), 0)";
- status_from(None) is Live: 4 tests fail, including no_verdict_is_unavailable;
- a per-thread cache: "probe runs in this process: 14"; skipping the
  OnceLock: 54;
- the sampler returns constant 0: "held at 1863990848 across the oracle's
  reads, yet the probe's sampler read 0";
- the sampler gives each CPU rail the sum of all CPU rails, applied in the
  pure assembly: caught on the M5 Max. Applied at the FFI boundary: an
  equivalent mutant on the M5 Max, which has one CPU rail (44/44 pass). It is
  caught on the M3 Ultra: "held at 28237793 ... read 59082835";
- the sampler reads the GPU rail: 4 tests fail;
- the tick sleeps: "one tick burned 10.75µs"; "interval 0 of 25 consumed
  27.25µs";
- the tick is a no-op: "interval 0 of 114 consumed 15.792µs";
- the probe uses the all-channel subscription: median sample calls of 528 ms
  and 293 ms on the M5 Max, and 174 ms and 163 ms on the M3 Ultra;
- the oracle is starved: "the oracle got only 0 read(s)".
The round-3 wall-clock spin, as an extra check, is caught only by the
one-tick test (24.70 ms < 25 ms), and narrowly.

Runs on this tree:
- M5 Max, lib tests 10x under 36 extra busy-loop processes (2 x 18 CPUs),
  load average 50-168: 10/10, 44 passed each. Median sample call 7.5-11.4 ms,
  minimum interval CPU 25.019 ms, 6-8 intervals. Every run printed
  "ioreport liveness: status=CpuRailFrozen oracle=CpuRailMoved(false)
  selected=false".
- M3 Ultra, once: 44 passed, median 8.7 ms, 29 intervals.
- The proof-rs workspace is green, and the proof-conformance binary prints
  "all checks passed". joulecontract-proof passes 6/6 and joule-code-release
  6/6.
- joule-code-remediate fails verified_fix_end_to_end_ships_with_receipt. It
  fails the same way with bedef9b0's meter.rs, so the failure predates this
  change; that crate meters through sandbox-meter, not this crate.
- clippy reports only the two pre-existing warnings. The x86_64 Linux build
  is compile-checked only (no Linux host).

Not changed, for David: which provenance grade a live IOReport reading earns
(the module header still says HwShunt), and adding this crate to a macOS CI job.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

79375a1c48

• View at this point in history

2026-09-30 09:02:37 -04:00

Transaction Science

proof-cascade: the liveness rule pairs consecutive samples itself, per rail ...

The family's energy contract: "measured when the platform exposes it,
estimated when it doesn't, and the provenance always says which ... A reading
never silently upgrades its own provenance." 5d01888f put this meter's probe on
the family liveness rule. An adversarial review of it found two medium defects
and several low ones. All of them are fixed here, and the family test design is
applied.

The two medium defects:
- The rule keyed rails by channel name and counted every same-named entry in
  an interval. So two channels with the same name that stepped together in one
  batch refresh counted as one rail advancing twice, which gave Live. The M3
  Ultra's Energy Model group already lists 264 of its 645 names twice (e.g.
  ECPUDTL00..22, once per die, with no DIE_ prefix). Its CPU aggregates are
  unique today, so neither measured host reached this.
- The half of the rule that says "between CONSECUTIVE samples" lived only in
  the FFI loop, and no test pinned it. With `prev = cur` removed, so every
  sample was compared with the FIRST one, all 23 tests still passed. That is
  the a5c77d8d shape: one batch refresh in the window then reads as an advance
  in every later interval, and the rail looks Live.

What holds now:
- D1, a pure sample layer. `RailWatch::observe` takes each whole sample as
  (channel name, ABSOLUTE raw integer) pairs. It keeps the previous sample
  itself and compares each CPU rail with it. A rail is keyed by (name, ordinal
  among the same-named channels in that sample), so it advances at most once
  per interval. The FFI sampler (`energy_model_sample`) only extracts the pairs
  from one IOReportCreateSamples call. The probe no longer uses
  IOReportCreateSamplesDelta.
- D2, a generic loop. `liveness::watch(sample, tick, now, budget)` is the
  probe loop. The real probe passes the FFI sampler, a 25 ms spin and Instant.
  A failed sample is not an interval: the next good one is compared with the
  last good one, and failures keep sampling up to the five-budget cap. It is
  tested with scripted samples and a scripted clock:
  (a) the M5 Max refresh [480083160, 480083160, 541893638, ...], with a GPU rail
      that moves every sample, is Frozen after 40 intervals;
  (b) the M3 Ultra's two dies stepping together once, among unprefixed per-die
      sub-rails listed twice, is Frozen;
  (c) two "CPU Energy" channels stepping together once is Frozen;
  (d) one rail advancing every sample is Live after exactly 2 intervals and 3
      samples, and the loop stops there;
  (e) failing samples run to exactly 5 budgets (201 samples), with no verdict,
      which maps to Unavailable;
  (f) past the budget it keeps sampling with 1 interval and stops with 2
      (Frozen at 1.6 s, 5 samples on a 400 ms clock);
  (g) one step on each die, in different intervals, is Frozen.
- D3. The verdict-to-status mapping is a pure fn, `status_from`, with a test.
- D4. The once-per-process cache is pinned: STATUS_PROBE_RUNS counts the runs
  behind ioreport_status(). A test calls it several times, and also
  hardware_meter_available(), available(), power_over() and
  measure_marginal_uj(). It asserts that exactly one probe ran and that a warm
  call returns within one tick.
- D5, cadence. The cached probe keeps its interval count. The frozen-rail test
  prints "ioreport liveness: status=.. probe_intervals=N", and when the status
  is CpuRailFrozen it asserts N >= 10. The fresh-probe test asserts the same
  floor for Frozen, and for Absent when the group opened. The group-only probe
  sees 26-32 intervals. The all-channel one gives 2-3 on the M5 Max tonight
  and 5-6 on the M3 Ultra.
- D6, the declined path. This meter's honest fallback is no figure at all. A
  test burns 80 ms of real CPU per call through measure_marginal_uj on a
  declined host and asserts three things: the result is None (not Some(0)),
  the work closure never ran (no bracket), and the call returned in under
  80 ms. proof-cli's test asserts the sealed receipt stays ModelBased with a
  non-zero figure.

Also fixed:
- RAPL wrap. rapl_power_over took wrapping_sub over the SUM of the per-zone
  counters, but each zone wraps at its own max_energy_range_uj. One zone
  wrapping therefore gave ~1.8e19 uJ, which proof-cli would have printed as
  HwShunt. The pure `rapl::delta_uj` now sums per-zone deltas, each taken
  modulo that zone's range. It gives no figure if a zone that wrapped has an
  unreadable range, or if the zone sets differ. Tests cover no wrap, a wrap in
  one zone, and an unreadable range with and without a wrap.
- A worker leak in bracket(). It returned at `busy_power()?` before stopping
  its workers, so a busy window with no reading left every core spinning for
  the rest of the process. The RAPL change adds such a None, so the workers are
  now stopped and joined first. `bracket_with` takes the power readers, and a
  test pins that the workers stop.
- measure_marginal_uj's doc said None when "the signal stays inside the idle
  noise", but the code returns Some(0) there. The doc now says so, and that it
  is not a measured zero. The behaviour is unchanged.
- Unavailable. Its doc and the CLI's reason now cover a subscription that
  opens but can never be sampled. They no longer blame Rosetta alone.
- proof-cli prints the decision it made ("--measure: hardware meter
  available=.. · ioreport_status=.."). tests/measure.rs asserts against that
  line instead of running a second probe, which could disagree on a
  borderline rail.
- strip_die_prefix now requires at least one digit and matches DIE_ in any
  case.
- The oracle's doc now says it shares the CFString helper, not only the FFI.

Claims in pushed messages and docs that were not true:
- 5d01888f says "Live means the same rail advanced in at least two separate
  sample intervals" and "The IOReport FFI only feeds it". With same-named
  channels, "the same rail" was one name. The FFI also did the
  consecutive-sample pairing, the part no test reached.
- 5d01888f says the rule is "the one jouleclaw-energy (b9d7e945) and
  eoc-meter (c6378629) implement". Its shape matched jouleclaw-energy's, which
  has the same duplicate-name defect. eoc-meter keys by channel index and
  computes steps inside its pure struct.
- 5d01888f deferred asserting the group-only probe because "a count threshold
  would flake under load". A floor of 10 is asserted here. The green runs saw
  26-32, and 15-16 under concurrent load.
- The test comments said "so a CI log says/shows". No CI job on this branch
  runs proof-cascade's macOS tests: proof-rs builds on the linux runner, where
  the IOReport code is cfg'd out. They now say "a log of a macOS run".
- a5c77d8d says it "drops the stale `macmon` references", but proof/README.md
  still said "IOReport via `macmon`". The README now describes the direct C
  API, used only while the CPU rail is live.

Observed, macOS 27.0.1. proof-cascade lib went from 23 to 36 tests:
  M5 Max, 3 runs: ioreport liveness: status=CpuRailFrozen
            oracle=CpuRailMoved(false) selected=false probe_intervals=29/31/30
            ioreport probe: probe=Some(Frozen) ... probe_took=1.097s/1.094s/
            1.102s intervals=28/31/29
            declined path: available=false ioreport_status=CpuRailFrozen
            figure=None work_runs=0 took=250ns
            test result: ok. 36 passed; 0 failed (each run)
  M3 Ultra: ioreport liveness: status=CpuRailFrozen
            oracle=CpuRailMoved(false) selected=false probe_intervals=32
            ioreport probe: probe=Some(Frozen) ... probe_took=1.10663325s
            intervals=32
            test result: ok. 36 passed; 0 failed
The whole proof-rs workspace passes on the M5 Max (z3 present), and so does
the proof-conformance binary ("all checks passed"). `proof --measure` declines
on both chips with "available=false · ioreport_status=CpuRailFrozen" and the
frozen-rail reason. Its receipt stays "provenance ModelBased" (167 uj on the M5
Max, 345 uj on the M3 Ultra, where z3 is absent). clippy --no-deps --tests
shows the same 2 warnings as 5d01888f and none new, and is clean for
x86_64-unknown-linux-gnu.

Dependants: joulecontract-proof (6) and joule-code-release (6) pass on both
chips. joule-code-remediate's verified_fix_end_to_end_ships_with_receipt
fails with "assertion failed: report.total_uj() > 0". It fails identically
with 5d01888f's meter.rs checked out; it meters through sandbox-meter. On the
M3 Ultra, the formal-template test also fails, from a baked
CARGO_MANIFEST_DIR path.

Falsified on the M5 Max. Each mutation was applied, the tests run, then
restored with git checkout, with a clean tree after each:
- Survivors of the last review. Skip the OnceLock (M4): "the liveness probe
  ran more than once in this process left: 25 right: 1". Compare with the
  first sample (M7): 6 rule tests fail, e.g. the M5 Max refresh "Run {
  verdict: Some(Live), intervals: 3 ..}". Probe on the all-channel
  subscription (M8): "Frozen after only 2 interval(s) in 1.367s" and "the
  cached probe called the rail frozen after 3 intervals". On the M3 Ultra, M8
  gives 5 and 6 intervals and fails the same two tests.
- Key rails by name alone, or count every same-named entry: (c) fails, Live.
- Sum advances across rails: (b), (c) and (g) fail.
- One advance is live: 9 tests fail.
- Stop at the budget with under 2 intervals: (e), (f) and the stopping-rule
  test fail.
- Don't stop when Live: (d) fails, 40 intervals.
- Give up on a failed sample: (e) and (f) fail.
- Treat every channel as a CPU rail: the rule tests fail, and on hardware
  "probe=Some(Live) ... oracle=CpuRailMoved(false)".
- Swap Frozen/Absent in status_from: the mapping test and the frozen-rail
  test fail.
- A declined meter returns Some(0), or runs a bracket before declining: D6
  fails.
- bracket() returns early without stopping its workers: "workers kept running
  after the bracket returned".
- RAPL wrapping_sub with no modulo, or an unreadable range taken as u64::MAX:
  the rapl tests fail, e.g. "left: Some(18446743811566228266) right:
  Some(5500)".
- proof-cli meters regardless, or prints the wrong decision: measure.rs fails
  with "the CLI's output disagrees with the decision it printed".

Left for David:
- The CLI tags a live IOReport figure Energy::measured, i.e. HwShunt, while
  the module header says a macOS Energy Model reading is ModelBased. The
  comment now states this instead of endorsing it.
- No macOS CI job runs this crate's tests yet.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

bedef9b08e

• View at this point in history

2026-09-30 07:58:43 -04:00

Transaction Science

proof-cascade: IOReport is live only when one CPU rail advances twice ...

The family's energy contract: "measured when the platform exposes it,
estimated when it doesn't, and the provenance always says which ... A reading
never silently upgrades its own provenance." a5c77d8d stopped this meter from
bracketing a frozen CPU rail, but its probe had two defects of its own.

- It called the rail Live on ONE advance. On macOS 27.0.1 the Energy Model CPU
  rails are not permanently frozen for an unprivileged reader: they are
  refreshed in rare batches. Both of an M3 Ultra's `DIE_<n>_CPU Energy` rails
  held for at least 22 minutes, then stepped +1,344,869 and +1,391,637 mJ in a
  single 100 ms sample and held again; an M5 Max's `CPU Energy` went from
  480,083,160 to 541,893,638 mJ between ~10:30 and 10:47 but did not change in
  13,614 samples over the next 25 minutes. A probe whose window straddles a
  refresh sees one jump, says Live, and caches that for the process; from then
  on `bracket()` would hand each later ~1.3 kJ refresh, whole, to whichever
  idle or busy window straddled it, tagged HwShunt. This false Live was seen
  at ~10:46 on the M5 Max by the jouleclaw-energy work.
- It sampled an all-channel subscription (~11,900 channels on the M5 Max), so
  "spins ~25 ms before each re-sample" was not what happened: at the 0.4-0.8 s
  a5c77d8d measured per sample, the 1 s budget bought two or three samples,
  each compared with the first.

The fix brings the probe onto the family liveness rule, the one
jouleclaw-energy (b9d7e945) and eoc-meter (c6378629) implement, copied in so
the crate stays self-contained:

1. The probe samples its OWN subscription to the "Energy Model" group only
   (IOReportCopyChannelsInGroup, then IOReportCreateSubscription). If the
   group cannot be subscribed, opening the all-channel subscription tells
   "no such group" (CpuRailAbsent) from "no IOReport" (Unavailable).
   `power_over()`'s own all-channel read path is unchanged.
2. Liveness is decided per CPU rail (the name, after stripping `DIE_<n>_`,
   equals "CPU Energy" case-insensitively), on the raw integer between
   CONSECUTIVE samples, never on a summed total: Live means the same rail
   advanced in at least two separate sample intervals.
3. It spins 25 ms on the calling thread before each sample, until Live, or
   until the 1 s budget has elapsed and at least two intervals were observed,
   with a hard cap of five budgets.
4. Live, Frozen, Absent or Unavailable (no sample could be taken), cached once
   per process as before; anything but Live declines the rung.
5. The rule is a pure struct, `liveness::RailWatch`, in a module compiled on
   every platform, so proof-rs's Linux CI job runs its tests too. The IOReport
   FFI only feeds it.

The public API is unchanged: IoReportStatus and its variants,
ioreport_status(), CPU_RAIL_LIVENESS_BUDGET, hardware_meter_available() and
measure_marginal_uj(). Docs made false by the change are corrected: the module
header, IoReportStatus::CpuRailFrozen / Live, CPU_RAIL_LIVENESS_BUDGET ("buys
two or three samples, each compared with the first"),
hardware_meter_available's probe cost, and probe_cpu_rail. proof-cli keeps
its messages; the frozen-rail reason's parenthetical now says "it did not keep
advancing" instead of "it did not advance", since a rail that stepped once is
also frozen. tests/measure.rs is unchanged.

Measured tonight (01:24-01:29) with a standalone timer: one
IOReportCreateSamples on the Energy Model group (364 channels on the M5 Max,
645 on the M3 Ultra) takes 5.1-5.4 ms median on both chips, all on-CPU. One on
every channel took ~106-111 ms on the M5 Max (75 ms on-CPU) and ~133 ms on the
M3 Ultra, well under a5c77d8d's 0.4-0.8 s figure, so that cost varies. The
docs give 0.1-0.8 s. The probe now takes 1.09-1.14 s for a Frozen verdict,
over 29-32 intervals of ~35 ms, both chips; under a full-core burst from a
concurrent test it saw 16.

Tests. Seven rule tests, no hardware: a_single_jump_is_a_batch_refresh_not_a_
live_rail, one_jump_on_each_die_is_not_a_live_rail,
both_dies_stepping_together_once_is_not_a_live_rail (the M3 Ultra's observed
refresh), two_advances_of_the_same_rail_are_live,
no_interval_is_no_verdict_and_no_cpu_rail_is_absent,
the_probe_samples_until_live_or_long_enough_to_tell (budget, two-interval
floor, five-budget cap, one advance does not stop it) and
only_the_cpu_energy_aggregate_is_a_cpu_rail. The hardware oracle keeps its own
all-channel subscription, ABSOLUTE values and the helper thread that burns
CPU for the whole 3x-budget window. It now matches names with
ends_with("CPU Energy"), as the family rule says, where it used a lowercase
match, and reports CpuRailMoved(true) only when one rail's absolute value
changed at two or more separate reads. The old oracle took any single change.
It logs "ioreport oracle: N reads in T, changes per CPU rail [..]". The probe
test now checks every outcome against the oracle, not only Live, requires a
Frozen verdict to rest on at least two intervals unless the cap cut it short,
and logs probe_took and intervals.

Observed, proof-cascade lib tests, macOS 27.0.1:
  M5 Max:   ioreport liveness: status=CpuRailFrozen oracle=CpuRailMoved(false)
            selected=false
            ioreport probe: probe=Some(Frozen) status=CpuRailFrozen
            oracle=CpuRailMoved(false) probe_took=1.093259666s intervals=31
            test result: ok. 23 passed; 0 failed
  M3 Ultra: ioreport liveness: status=CpuRailFrozen oracle=CpuRailMoved(false)
            selected=false (oracle: changes per CPU rail [0, 0])
            ioreport probe: probe=Some(Frozen) status=CpuRailFrozen
            oracle=CpuRailMoved(false) probe_took=1.137413416s intervals=32
            test result: ok. 23 passed; 0 failed
(16 before this commit.)

Falsified on the M5 Max. Each mutation was applied to this commit, then
restored with git checkout, with a clean tree after each:
- F-rule, LIVE_RAIL_ADVANCES = 1: five of the seven rule tests fail, e.g.
  "one refresh counted as a live rail", "one advance is not yet live", "one
  interval, past budget: keep going", and one_jump_on_each_die "left:
  Some(Live) right: Some(Frozen)".
- F1, the probe always says Live: the frozen-rail test fails with "IOReport
  meter available although its CPU rail did not keep moving under 3s of CPU
  burn — it would bracket GPU-only energy, zero, or a refresh as the energy of
  CPU work" (status=Live oracle=CpuRailMoved(false) selected=true). The probe
  test and the selected-meter test also fail ("a live CPU rail metered a
  multi-core CPU burst as Some(0)").
- F2, main's ungated available(): the frozen-rail test fails with the same
  message (status=CpuRailFrozen oracle=CpuRailMoved(false) selected=true), and
  so does the selected-meter test ("selected on a CPU rail that is not live").
- F-sum, liveness decided on the summed Energy Model total: the live GPU rail
  makes the probe say Live after 2 intervals in 167 ms. The frozen-rail test
  fails with the message above (status=Live selected=true), and so do the
  probe and selected-meter tests.

The proof-rs workspace passes on the M5 Max (z3 present), as does the
proof-conformance binary (10/10, "all checks passed"). `proof --measure`
declines with the frozen-rail reason on both chips, with no "HwShunt" and no
"idle noise" in its output. The run takes 1.24 s (M5 Max) and 1.17 s (M3
Ultra). Dependants: joule-code-release (6) and joulecontract-proof (6) pass on
both. joule-code-remediate's verified_fix_end_to_end_ships_with_receipt fails
with "assertion failed: report.total_uj() > 0" (7 passed, 1 failed on the M5
Max), the same as on a5c77d8d run from a git archive. On the M3 Ultra it is 6
passed, 2 failed: that test and the formal-template test described below. It meters through sandbox-meter; no
dependant calls proof_cascade::meter. On the M3 Ultra the shipped binaries of
proof-rs's lib/soundness tests pass. measure.rs, proof-conformance's pack.rs
and remediate's formal-template test bake this checkout's absolute paths into
the binary (CARGO_BIN_EXE_*, CARGO_MANIFEST_DIR), so they cannot run on
another host. There, measure.rs's assertions were checked by hand against
`proof --measure`. clippy --no-deps --tests on proof-cascade and proof-cli
adds no warnings (the duplicated #[link] attribute and the b"..\0" literal are
on a5c77d8d). clippy for x86_64-unknown-linux-gnu is clean, including the
liveness module off macOS.

Not done here, deliberately:
- The group-only probe is shown by the logged interval count, not asserted.
  A count threshold would flake under load (16 intervals under a concurrent
  full-core burst).
- power_over() still reads an all-channel subscription and divides by the
  sleep, not the sample-to-sample window. The grade, the partial GPU reading,
  a rail that stops tracking after the cached probe, and the RAPL notes all
  stand as a5c77d8d listed them.
- proof/README.md still says the meter reads IOReport "via `macmon`", which
  has been stale since a5c77d8d.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

5d01888f20

• View at this point in history

2026-09-30 01:33:30 -04:00

2026-09-29

Transaction Science

proof-cascade: never meter CPU work through a frozen IOReport CPU rail ...

The family's energy contract: "measured when the platform exposes it, estimated
when it doesn't, and the provenance always says which ... A reading never
silently upgrades its own provenance." proof-cascade's meter broke it on current
macOS, and `proof --measure` then blamed the machine for what the platform did.

Ground truth, macOS 27.0.1 (measured for PR #110 by dumping the channels): on an
M5 Max the IOReport Energy Model CPU rails do not advance for an unprivileged
reader while `GPU Energy` does; on an M3 Ultra every Energy Model rail is frozen.
Re-observed through this crate: the probe added below matched `CPU Energy` on the
M5 Max and `DIE_0_CPU Energy` / `DIE_1_CPU Energy` on the M3 Ultra, with a raw
delta of 0 on every sample.

The defect. `hardware_meter_available()` was true as soon as an IOReport
subscription opened, and `power_over()` summed every Energy Model rail,
returning `None` only when the SUM was zero. Instrumenting `bracket()` on main
showed what that meant:
- M5 Max: idle_w=0.345 W, busy_w=0.281 W with every spare core burning (then
  0.315/0.291 and 0.308/0.295 on two more runs): the GPU rail alone. The
  marginal clamps to Some(0) and the CLI printed "signal stayed inside the idle
  noise (a loaded/throttled box)". A run in which the GPU rail drew more in the
  busy window than at idle would print that difference as the proof's energy,
  tagged HwShunt, "a real hardware reading".
- M3 Ultra: idle_power=None (every rail frozen, sum 0), and the CLI printed the
  same "loaded/throttled box" misdiagnosis.
Its two tests could not see it: one returned early without IOReport and
asserted only inside `if let Some(w)`, the other asserted only an upper bound
inside `if let Some(uj)`, so every None passed silently, on the M3 Ultra always.

The fix, with jcp-energy's semantics (PR #110), copied in so the crate stays
self-contained. `macos_ioreport::probe_cpu_rail` opens a subscription and spins
~25 ms on the calling thread before each re-sample, for up to
`CPU_RAIL_LIVENESS_BUDGET` (1 s), deciding on the raw integer of the Energy
Model channel named `CPU Energy` after stripping a `DIE_<n>_` prefix, never on
the summed total that the live GPU rail corrupts: Live, Frozen or Absent.
`ioreport_status()` probes once per process and caches the answer as the public
`IoReportStatus` {Unavailable, CpuRailAbsent, CpuRailFrozen, Live}, so callers
can say why. `available()`, and so `hardware_meter_available()`, is true only
when Live; `power_over()` and `measure_marginal_uj()` return None otherwise,
before any window runs. None keeps meaning "no hardware interface", so callers
keep their ModelBased figure, and a live reading keeps its existing grade.

proof-cli prints the status as the reason ("IOReport opens, but its CPU energy
rail is frozen (it did not advance while this process burned CPU), so it cannot
meter CPU work. The figures above stay ModelBased"), keeps the idle-noise
message for a live interface whose busy window did not clear idle, and drops
the stale `macmon` references. The sealed receipt is unchanged: it is built
from the first CascadeResult, never from the --measure figure.

One measurement the reference does not state: sampling every channel is slow.
One IOReportCreateSamples call took 0.4-0.8 s on the M5 Max, mostly waiting (75
ms of 0.81 s on-CPU, timed on the thread clock), so the 1 s budget buys two or
three samples over a 1.1-1.9 s window and the probe's spin is a small share of
it. That cannot produce a false Live, since only the rail's own integer moving
can, so it errs only toward declining. The docs say so, and the test oracle
burns on a helper thread instead.

Tests. The two silent tests are replaced and three oracle-based ones added.
Every branch asserts something:
- the_ioreport_meter_is_never_available_on_a_frozen_cpu_rail, against an
  independent oracle: its own subscription, each CPU rail's ABSOLUTE value (no
  deltas), names matched by lowercase ends_with("cpu energy") in any group (a
  superset of the probe's rails), and a helper thread burning CPU for the whole
  3x-budget window (3.54 s of user CPU for this test alone). It logs
  "ioreport liveness: status=.. oracle=.. selected=..", asserts a frozen rail is
  never selected and that power_over and measure_marginal_uj return None there,
  and on every branch that selection equals status == Live.
- the_liveness_probe_never_reports_a_frozen_rail_as_live: a fresh probe and the
  oracle, the implication evaluated on every host, not only one claiming Live.
- a_selected_ioreport_meter_meters_cpu_work: when selected, status and a fresh
  probe are Live and a multi-core burst meters Some(>0); when not, the status
  is not Live and the meter returns None.
- power_over_declines_unless_the_cpu_rail_is_live and meter_is_total_or_nothing
  replace the silent pair: a declined interface must give None, a usable one a
  figure. ioreport_status_is_unavailable_off_macos covers other platforms.
- proof-cli tests/measure.rs runs `proof --measure`: when it declines, the
  output gives the reason (the frozen rail when that is the status) and holds no
  "HwShunt" and no idle-noise blame; when it meters, the host's meter must be
  available.

Observed with 16/16 proof-cascade lib tests passing on both chips, macOS 27.0.1:
"ioreport liveness: status=CpuRailFrozen oracle=CpuRailMoved(false)
selected=false" on the M5 Max and on the M3 Ultra, and the CLI prints the
frozen-rail reason on both.

Falsified on the M5 Max, each restored with git checkout:
- F1, probe always Live: the frozen-rail test fails with "IOReport meter
  available although its CPU rail did not move under 3s of CPU burn — it would
  bracket GPU-only energy, or zero, as the energy of CPU work" (status=Live
  oracle=CpuRailMoved(false) selected=true). The probe test fails, and so does
  the selected-meter test, with "a live CPU rail metered a multi-core CPU burst
  as Some(0)": main's bracket on GPU-only rails.
- F2, main's ungated available() and power_over(): the frozen-rail test fails
  with the same message (status=CpuRailFrozen oracle=CpuRailMoved(false)
  selected=true), so main fails it today.
- F3, main's proof-cli over this meter: tests/measure.rs fails with "neither a
  declined meter nor a measurement in the output".

The proof-rs workspace passes, as does the proof-conformance suite (10/10);
joule-code-release and joulecontract-proof pass. joule-code-remediate's
verified_fix_end_to_end_ships_with_receipt fails with "assertion failed:
report.total_uj() > 0", identically on unmodified origin/main; it meters through
sandbox-meter, not this crate. clippy adds no warnings (two pre-existing ones
remain). Off macOS, `cargo check --tests` passes for x86_64-unknown-linux-gnu;
aarch64 Linux and Windows could not be checked here, because blake3's C build
needs a target sysroot or MSVC.

Not done here, deliberately:
- The grade. The module header calls this the HwShunt backend and proof-cli tags
  a live figure `Energy::measured` (HwShunt), while the same header says a macOS
  Energy Model reading is ModelBased. Which grade IOReport earns is a
  family-wide decision.
- Reporting the live GPU rail as an explicitly partial reading.
- A rail that freezes after the cached probe; that needs a residency witness.
- measure_marginal_uj's doc promises None "inside the idle noise", but the code
  returns Some(0) when busy <= idle (observed above), and no test covers noise.
- power_over divides by the sleep `d` while its sample-to-sample window also
  holds a 0.4-0.8 s IOReportCreateSamples call, overstating a live reading.
- The Linux RAPL path: its "world-readable" comment predates the 2020 root-only
  change, and wrapping_sub over the sum of per-zone counters turns one zone
  wrapping into an absurd figure.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

a5c77d8d47

• View at this point in history

2026-09-29 10:51:22 -04:00