sandbox-meter: a CPU counter that does not keep moving is never a measurement, and no consumer relabels an estimate #114
Loading…
Reference in a new issue
No description provided.
Delete branch "sandbox-meter/cpu-rail-liveness"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
sandbox-meter's IOReport probe sealed a CPU counter that never moved as a hardware measurement. Four consumers then relabelled whatever they were given.
What was wrong: on main, measured on both chips
joule-meter, 1 s of all-core burn:Cpu: 0 µJ [HwShunt] · Npu: 0 µJ [HwShunt] · Gpu: 226790 µJ [HwShunt]0 µJ [HwShunt]Span::stopsealed every class delta, 0 included, asmeasured_uj: Some(delta)+ HwShunt. That breaks the module's own promise: "a probe can degrade but it can never lie … not a zero dressed as a measurement".run_attributedstayedattributed = truewithsoc_cpu_uj == 0.Energy::measured(HwShunt). Its "metered and debited" tests asserted only insideif metering_is_hardware(). They passed while the GPU drew, and on the M3 Ultra they failed (3/3 and 2/3). This is the root cause of the jcp-gateway failures seen on main.report.total_uj() > 0).0 µJ.What this does
IoReportProbe::new()declines unlessioreport_status()is Live, soPowerMeterfalls back to its estimator: wall × TDP,Estimator, nomeasured_uj.attributedis true only when the window's CPU record is a HwShunt reading > 0.is_hardware(), a trait default or a hard-coded grade:energy_of()uses jcp-schema's existing constructors:estimator,measured,measured_partialfor a CPU-less hardware reading, andmodeled. No wire fields are added.Estimator; JouleContractUnaccounted, withjoules_spentset to that figure). It is never an apportioned 0.SpanMeterseals each interaction with its own span's figure and grade. Thejoule-ui-interactionexamples get the same fix, and theMetertrait is unchanged.meter_cmdno longer prints a floored 0 as "the workload's honest share".IoReportProbe::open()never releaseddesired.After, on both chips: spans seal
Cpu: ~20,000,000 µJ/s [Estimator]and state the reason.allowed, 2309714 µJ [Estimator]where it used to print1541728 µJ measured.44.352 J estimated, not attributed (Unaccounted)where it used to print1.446 J (attributed).Verification of this PR (head
d35c99af)41d80434): joule-code-remediate discarded the results ofgit checkout -b,git addandgit commit. It reportedshipped: truefor fixes that were never committed, which happens in any environment without a git identity, including the CI container. It could also commit onto the wrong branch. A failed ship step now returnsHarnessError::Ship, saying where the verified change was left. (That commit's message has two errors, corrected in4b20ce2a: the two-run test came fromcee66773, and the falsification fails five tests.)Later rounds on this branch
f2f23c2d,7609bfea,1b7a6169andccbec44a:measured_uj(energy_provenance, plusenergy_coveragewhen partial).Meterdefaults to Estimator; the conformance fixture keeps HwShunt explicitly, so the vectors are byte-identical.Authorizer::chargecarries the full figure.JOULE_FIX_EXPECT_Z3=1makes a missing solver a failure.6b693aa4and7539c62e: RAPL and NVML are gated, and every summed rail must be live. joule-ui seals a GPU-only span as an Estimator figure for the interaction, because it has no coverage field.5e945eed: IOReport is live only if every CPU rail it sums keeps advancing.7cf1f036: RAPL sums only thepackage-Nzones, never psys or dram. Each zone wraps at its own range; an unknown range on a fall gives no figure and breaks the running count.8a3465e1: sandbox-exec-microvm's RAPL meter reuses the gated package reader. The MSR meter reads every package and die, and declines on hosts it can't fully see.a16e36cf: remediate's tests give each scratch crate its own target directory, so they pass with or withoutCARGO_TARGET_DIR. Productionjoule-fixstill honours it.3d70348a: a microVM run whose CPU counter held is a model estimate, never a measured zero.Why: what IOReport actually does on macOS 27.0.1
Measured by reading channels directly on the M5 Max (dev) and the M3 Ultra (10.10.10.2), both on macOS 27.0.1:
CPU EnergyandDIE_<n>_CPU Energydo not move under load for seconds to minutes. On the M3 Ultra both dies held for at least 22 minutes, then jumped about 1.3 kJ each.+61,764,485 mJ, then+3,435 mJ64 ms later.A meter that sums rails therefore reports CPU work as GPU-only energy (M5 Max) or 0 (M3 Ultra), labelled as a reading. A liveness check that accepts one advance, or two, gives a false Live whenever its window holds a refresh. After that, each later ~1.3 kJ lump is booked whole to whichever span straddles it.
The rule: identical in all five backends (#110, #114, #115, #116, #117)
CPU Energy, or eachDIE_<n>_CPU Energy), keyed by name and ordinal:namereadspackage-N, on every socket, and each must be live. It never sumspsys, which already includes the packages, nordramor the sub-zones.max_energy_range_uj. A wrap whose range is unknown gives no figure; it never becomes a ~1.8×10¹⁹ µJ reading.Livedeclines the backend, so the crate's existing honest fallback runs. The reason is public:IoReportStatus,ioreport_status(),rapl_status(),nvml_status().admits(status)(Live only).How it was verified
Six rounds of implementation, each checked by independent adversarial verification.
Pure tests on scripted samples and a scripted clock. They cover:
Fault hooks inside the real IOReport opener and sampler. The tests drive the real production status through each script: opener fails, a single lump, a two-step lump, constant values, and a sustained advance. So a bypass written into the glue fails a test.
Hardware tests against an independent oracle. The oracle has its own subscription, reads absolute values, burns on a helper thread, and counts a rail as moving only on a sustained change. The tests check:
Mutation-tested. Each of the following was applied as a temporary edit and failed a test:
admits()that accepts CpuRailAbsent.The counts per crate are below.
Robustness. Each crate passes under artificial CPU load and while another process samples every IOReport channel in a tight loop. The latter is what made an earlier wall-clock pin flaky, so the job now runs on the shared CI host without that flake. Each also passes on the M3 Ultra.
CI: these tests are behind
cfg(target_os = "macos"), and this workspace runs on a linux runner. They reach CI through #102, which merges last. #102 runs every backend's lib and integration tests on macOS, and fails any step whose frozen-rail test did not printioreport liveness:.Merge order: #110, #114, #115, #116 and #117 are independent of each other. #102 goes after all of them.
Open questions, now decided and implemented (per "fix it all")
measured_ujthat carry estimates. Their grade now sits beside them in plaintext: jcp-gateway's_metagetsenergy_provenance, plusenergy_coveragewhen partial. The keys stay, for compatibility.Meterdefaults to Estimator, and the conformance fixture keeps HwShunt explicitly, so the vectors are byte-identical.Authorizer::chargecarries the figure's provenance.ri_energy_nj: unprivileged, live on both Macs, and attributed to the work. It is wired in as stacked PRs #120–#124, only where the work runs in-process. (Privilegedpowermetricsis live too, but machine-wide and root-only, so it is not used.)Still open
joule-ui-servegives it honest grades, and the per-process probe in #121 gives it real readings.🤖 Generated with Claude Code
The crate's contract, in its probe module doc: "A probe can degrade but it can never lie: if the hardware path fails mid-span, the reading comes back `Estimator`, not a zero dressed as a measurement." On current macOS the IOReport probe broke that on every Apple Silicon host. Ground truth, measured 2026-09-29 by dumping the Energy Model channels while burning CPU, not by re-running tests: - M5 Max, macOS 27.0.1: 364 channels. Of the three that `class_for` maps, `CPU Energy` (mJ) held at 480,083,160 and `ANE0` held across 3 s of burn; `GPU Energy` (nJ) advanced 682,543,073. Nothing else moved. - M3 Ultra, macOS 27.0.1: 645 channels, none moved, including `DIE_0_CPU Energy`, `DIE_1_CPU Energy`, `ANE0_0`, `ANE0_1`, `GPU Energy`. The defect. `IoReportProbe::new()` accepted the probe once a subscription opened and one snapshot was non-empty, and `Span::stop` sealed every class delta, zero included, as `measured_uj: Some(delta)` under `HwShunt`. main's own `joule-meter 1`, busy on all cores, sealed and verified: M5 Max: Cpu: 0 µJ [HwShunt] Npu: 0 µJ [HwShunt] Gpu: 226790 µJ [HwShunt] M3 Ultra: Cpu: 0 µJ [HwShunt] Npu: 0 µJ [HwShunt] Gpu: 0 µJ [HwShunt] On the M5 Max the display's GPU energy is passed off as the energy of CPU work; on the M3 Ultra, three measured zeros. The same figure flows on: `sample_uj()` sums the classes, and `run_attributed` apportioned a 0 J "measurement" with `attributed = true`. That is why dependants fail on main on these machines. This crate's `attributed_run_captures_a_busy_child` fails at attribute.rs:297 ("a busy window costs SoC energy"). joule-code-remediate's `verified_fix_end_to_end_ships_with_receipt` fails with `report.total_uj() > 0`: it apportions the frozen rail's zero. jcp-gateway's `granted_tool_is_allowed_metered_and_debited` (lib.rs:585, `measured_uj > 0`) and `budget_exhaustion_denies_further_calls_and_the_log_verifies` (lib.rs:638, "the budget eventually exhausts") assert, under `metering_is_hardware()`, that a span's summed total moved. That holds only while the GPU rail happens to tick: 40/40 green on the M5 Max this morning with the display compositing, red when it idles, and 3/3 and 2/3 red on the M3 Ultra. The fix applies the contract in the three places the decision is made. 1. Selection. `IoReportProbe::new()` declines unless `ioreport_status()` is `Live`. The CPU rail itself (`CPU Energy`, or `DIE_<n>_CPU Energy` on multi-die parts, matched after stripping the die prefix) must advance while the probing thread burns CPU. It is sampled every ~25 ms for up to `CPU_RAIL_LIVENESS_BUDGET` (1 s), probed once per process and cached in a OnceLock. The probe reads the same absolute samples `snapshot()` reads, on the probe's own subscription, so it tests the path a span will use. It decides per rail on the raw integer, before unit conversion, paired by position and name. It never decides on a summed total, which the live GPU rail advances by itself. Otherwise `new()` returns `ProbeError::Unavailable` naming the frozen `CPU Energy` rail, and `PowerMeter` falls back to its estimator: wall × TDP, `Estimator`, no `measured_uj`. A probe whose snapshot carries no CPU class is refused too, because GPU and ANE alone would be the same defect. 2. The span. In a span this process ran in, a CPU-class delta of 0 is a counter that held, not a reading. The whole span now returns the estimator record, exactly as when every probe vanished. That covers a rail that freezes after the per-process probe, and RAPL: a package counter that did not advance is no measurement either. A probe set with no CPU class (NVML alone) is not subject to it. I checked for tests that would break: none expects a short span to be `HwShunt`. jcp-gateway's hardware-only asserts need only a positive figure, which an estimate is. Whether the Linux runners' containers can read RAPL was not verified here. 3. Attribution. `run_attributed` sets `attributed` only when the window's CPU-class record is an `HwShunt` reading that advanced, on top of the existing rusage and busy-tick conditions. An estimate is carried as context and never apportioned as a reading. `IoReportStatus` (`Unavailable`, `CpuRailAbsent`, `CpuRailFrozen`, `Live`, with a Display), `ioreport_status()` and `CPU_RAIL_LIVENESS_BUDGET` are public and re-exported at the crate root, so a caller or CLI can say why an Apple Silicon host is estimated. `joule-meter` now does. Its "machine-wide counters; subtract idle" note is printed only for a measured span, because it is false for an estimate. Grade names are untouched: a live IOReport reading is still `HwShunt`. Tests. Every IOReport test asserts against an independent oracle. The implementation reads absolute samples on its own subscription and strips a die prefix. The oracle opens its OWN subscription, reads DELTA samples with `IOReportCreateSamplesDelta` (the implementation never calls it), matches `ends_with("CPU Energy")`, and burns for three times the probe's budget. No branch passes without asserting. - `the_ioreport_probe_is_never_selected_on_a_frozen_cpu_rail` checks the property and prints "ioreport liveness: status=.. oracle=.. selected=..". - `the_liveness_probe_never_reports_a_frozen_rail_as_live` checks the dangerous direction, and checks every other status claim against the oracle. - `a_selected_ioreport_probe_meters_cpu_work`: when selected, a CPU burn meters an `HwShunt` CPU record > 0. When declined, the status is not Live, the span is the estimator's, and `sample_uj()` is None. - `a_cpu_rail_is_the_rail_itself_on_one_die_or_many` and `liveness_is_decided_per_cpu_rail_on_the_raw_integer` cover the matcher and the pairing, using the dumps' names and values. - Scripted-probe span tests replay the dumps and are deterministic on every platform: `a_span_whose_cpu_counter_held_is_estimated_even_though_the_gpu_advanced` (M5 Max), `a_span_where_every_counter_held_is_estimated` (M3 Ultra), `a_held_cpu_counter_estimates_the_whole_composite_span` (RAPL held, NVML moved), `a_span_whose_cpu_counter_advanced_is_measured`, and `a_probe_set_without_a_cpu_class_is_not_subject_to_the_cpu_rule`. - `detect_never_fails_and_records_validate` used to assert `total_uj() > 0`, which the GPU rail satisfied. It now asserts the CPU record or the estimator record, and on Apple Silicon that the probe exists exactly when the status is Live. - `attributed_run_captures_a_busy_child` used to assert `soc_cpu_uj > 0` and fails on main. It now asserts per status: Live means attributed; otherwise not hardware, not attributed, and an estimator figure > 0. Two scripted tests pin the rule itself: `a_window_whose_cpu_counter_held_is_never_attributed`, and `a_window_whose_cpu_counter_advanced_is_attributed` for the positive path, which no macOS 27 host reaches for real. Their child now runs 2–3 s, bounded by the clock and an iteration cap. The machine tick counters behind `busy_cpu_secs` update in bursts up to ~990 ms apart on both chips. A ~0.3 s child saw `busy_cpu_secs = 0.0` on the M3 Ultra and would have declined for the wrong reason. Observed with the same test binary on both chips, 5 runs each, 31/31 every time: M5 Max: ioreport liveness: status=CpuRailFrozen oracle=CpuRailMoved(false) selected=false M3 Ultra: ioreport liveness: status=CpuRailFrozen oracle=CpuRailMoved(false) selected=false Falsified. Each mutation was restored with git checkout, leaving a clean tree: - F1, the probe always says Live: the frozen-rail test fails ("the oracle saw the CPU rail hold under 3s of CPU burn", left: Live, right: CpuRailFrozen), and so do the never-Live, metering and attribution tests. - F2, main's ungated `new()`: it fails with "IOReport probe selected although its CPU rail did not move under 3s of CPU burn — every span would report GPU-only energy, or zero, as a measurement of CPU work", and 3 others fail. - F3, the per-span rule removed: the three held-counter span tests fail. The M5 Max one reproduces main's seal exactly: Cpu Some(0), Npu Some(0), Gpu Some(682543), all HwShunt. - F4, main's attribution rule: `a_window_whose_cpu_counter_held_is_never_attributed` fails because the estimator's 27.8 J is attributed as a reading. Dependants, run on main and on this branch: sandbox-attest, -runtime, -exec-wasm, -exec-microvm, -conformance (and its suite: all classes, no skips), -proof, -proof-wasm, -mcp, -build, -cli, -jcp, jcp-gateway, jcp-action-receipt, joule-ui-interaction and joule-ui-serve pass on the branch. joule-code-remediate passed 15 of 16 branch runs. The failure was `verified_fix_end_to_end_ships_with_receipt` with the assertion it fails with on every main run, `report.total_uj() > 0`. On the branch that figure is estimate × share, and the share is 0 when no machine tick burst lands in any of its cargo windows. jcp-gateway passes because its hardware-only asserts are now skipped. Both relabel the estimate this crate now returns: see below. Clippy is clean on this crate (--tests), and so is x86_64-unknown-linux-gnu. Not done here, deliberately: - Consumers that relabel the estimate this crate now returns: jcp-gateway debits and seals `Energy::measured(measurement.total_uj())` (lib.rs:255-259) and labels its eval by `meter.is_hardware()` (lib.rs:228, 430). Its hardware-only asserts are now skipped on Apple Silicon. joule-code-remediate seals an estimate-apportioned figure as `ModelBased` (lib.rs:656), and its end-to-end test passes here only because `total_uj()` is now an estimate > 0. jcp-action-receipt (examples/end_to_end.rs:139), sandbox-proof (lib.rs:1321) and joule-ui label by `is_hardware()` rather than by the span. They are for the next change, on this branch. - A GPU or ANE zero beside a CPU counter that advanced, and an NVML-only set's zero GPU delta, are still sealed `HwShunt` 0 (probe/mod.rs:340). - Reporting the live GPU rail as an explicitly partial reading instead of declining the probe is a receipt and wire decision. - `class_for`'s substring match (ioreport.rs:101-111) sums every `DIE_n_CPU Energy`, which is right for an Ultra. It would also sum a sub-rail named "…CPU Energy", and it takes any channel containing "ANE". On these two dumps only the top-level rails match; other chips need a dump. - `sample_uj()` sums every class, so its before/after users cannot apply the held-CPU rule. `Attribution` has no provenance for `soc_cpu_uj`. Both are API changes. - `busy_cpu_secs` inherits the ~1 s tick bursts, so windows under ~1 s are declined or skewed. Co-Authored-By: Claude Opus 5.5 <[email protected]>The contract, stated in jcp-energy and sandbox-meter alike: measured when the platform exposes it, estimated when it doesn't, "and the provenance always says which". The parent commit makes sandbox-meter keep it. On macOS 27.0.1 no Apple Silicon host checked exposes a live CPU energy counter, so PowerMeter declines IOReport and every span is the estimator's wall × TDP record. On a live host, a span whose CPU counter held is estimated too. The meter's consumers then threw that provenance away. Ground truth: the consumers' own output at the parent commit. The same binaries ran on an M5 Max and an M3 Ultra, both on macOS 27.0.1; the M5 Max comes first. - jcp-gateway printed "metering=estimator", then "allowed, 1541728 µJ measured", and sealed energy_provenance "HwShunt" in the receipt. It debited Energy::measured(total_uj()) whatever the span was. On the M3 Ultra: "999293 µJ measured", sealed HwShunt. - joule-ui-serve sealed every interaction as Estimator with estimated_uj 0, for 24-56 ms of work. Its sampler summed raw counters under the Meter trait's default HwShunt. It returned None once no hardware probe was left, and run_interaction turns None into 0 J. - joule-fix printed "energy per verified fix: 1.446 J (attributed)" for an estimate apportioned by CPU share, and sealed it ModelBased in the JCR-1 meter envelope (M3 Ultra: 7.377 J, ModelBased). The share is 0 whenever the machine tick counters miss every window, so the figure can be 0 J. The parent commit gave that as the likely cause of verified_fix_end_to_end's 1-in-16 failure. - sandbox-proof said "ESTIMATED" here only because it asked is_hardware(). On a live host it would say "measured" for a span the meter estimated. The defect. Each consumer labelled a span by the meter instead of by the span's own records: is_hardware(), a trait default, or a hard-coded "ModelBased" or "measured". Or it turned a meter with no reading into 0 J. The fix. Every consumer derives the label from the Measurement it got: the weakest of its records, because a sum is only as good as its weakest part. - jcp-gateway. energy_of() builds the ledger entry with jcp-schema's own constructors: - Energy::estimator for the estimator's record; - Energy::measured for a hardware reading that has a CPU record; - Energy::measured_partial for a hardware reading without one (a GPU counter alone, NVML without RAPL); - Energy::modeled for ModelBased. The figure is unchanged, so a runaway is still debited. Only what the receipt says about it changes, through fields it already had: energy_provenance, and energy_coverage when Partial. The flow monitor's scan is sealed with its own span's provenance (flow_energy_provenance) instead of is_hardware()'s. The binary's summary line reads the grade back from the receipt it just sealed ("[Estimator]") instead of printing "measured". The docs and the crate description said "metered on real hardware" and "the MEASURED joules"; both are corrected. jcp-gateway now depends on sandbox-schema directly, for the CPU class; the crate was already in the lock graph. - joule-code-remediate. An EnergyTally grades the run by its cargo windows. The run is ModelBased only when every window was attributed. main needed only one, and never reset the flag between runs. An attributed run's receipts carry the attributed figure, anchored as before. Any other run's receipts carry the unapportioned total over the windows, as an estimate: - the JCR-1 meter envelope seals it with the Estimator grade; - the JouleContract receipt seals it as Unaccounted; - total_uj() and uj_per_verified_fix() return it. An apportioned estimate is no better than an estimate, and apportioning can put 0 J on the receipt for work that ran. joule-fix prints "estimated, not attributed" and "(estimated)" to match. - joule-ui-serve. SpanMeter replaces the summing sampler. Every sample closes the span the previous sample opened, adds its figure to a running counter, and opens the next. provenance() returns that span's own grade, which run_interaction asks for right after its second sample. An estimated span is sealed as Estimator with the estimator's figure, not 0 J, and a hardware span as HwShunt. The Meter trait is untouched. The binary's doc and its Cargo.toml said every receipt's HwShunt was true; corrected. - sandbox-proof. prove_local says "measured" only when every record of the span is a hardware reading (energy_word). The records were, and still are, sealed verbatim into the receipt, the attestation and the proof cell. - jcp-action-receipt. The end_to_end example sealed energy_provenance from is_hardware(); it now takes the span's. Checked and left alone: - sandbox-jcp debits a declared ceiling as Energy::estimator and never reads a PowerMeter. - joule-ui-interaction's library labels nothing as a hardware reading that its meter did not declare one. Its jcp_metered example wraps whatever figure it is charged in Energy::measured, but only in a JCP runtime decision that it neither seals nor prints. See below. After the fix, with the same binaries on both chips: - jcp-gateway prints "allowed, 2309714 µJ [Estimator]" and seals Estimator (M3 Ultra: 973555 µJ, Estimator). - joule-ui-serve seals 482410 and 1121739 µJ as Estimator for intensities 3 and 7 (M3 Ultra: 481236 and 1121485 µJ). - joule-fix prints "44.352 J estimated, not attributed" and seals Estimator and Unaccounted (M3 Ultra: 20.723 J). - sandbox-proof still says ESTIMATED. Tests. The same test binaries ran 5/5 green on each chip. On the M3 Ultra, joule-code-remediate's the_shipped_formal_template_parses_and_validates cannot find formal.example.json, whose path is fixed at compile time on the dev machine, so the five runs there skip that one test. That host also has no z3, so the two existing formal-proof tests return early there. - jcp-gateway a_metered_span_enters_the_ledger_as_what_it_is: every span shape maps to its constructor, and the debit is the span's own figure. - jcp-gateway a_calls_receipt_says_how_its_joules_were_obtained: end to end, the sealed energy_provenance is Estimator when the meter has no hardware source ("gateway call: hardware=false sealed=Estimator cost_uj=30621"). Otherwise it is a reading or an estimate. cost_uj > 0 either way. - jcp-gateway granted_tool_is_allowed_metered_and_debited and budget_exhaustion_denies_further_calls_and_the_log_verifies asserted only under metering_is_hardware(), so on these hosts they passed without asserting. They now assert on every host: an estimate is debited, and the budget exhausts. - The exfiltration test now also checks flow_energy_provenance. - joule-code-remediate an_unattributed_run_is_sealed_as_an_estimate_never_an_apportioned_zero and a_run_is_attributed_only_when_every_window_was pin the tally. - joule-code-remediate verified_fix_end_to_end_ships_with_receipt now also checks that joules_spent equals total_uj(), the JouleContract class, and the grade inside the sealed meter envelope. It also checks that nothing is attributed without a live CPU rail. - joule-ui-serve each_served_interaction_carries_its_own_spans_provenance replays a HwShunt span, then an Estimator span, through the real Host. - joule-ui-serve the_served_meter_never_seals_zero_or_an_estimate_as_a_reading runs the served meter on this host. - sandbox-proof a_local_proof_says_estimated_for_an_estimated_span. Falsified. Each mutation was restored with git checkout, leaving a clean tree. - energy_of returns Energy::measured(total), main's rule: both new gateway tests fail. The end-to-end one fails with left "HwShunt", right "Estimator". - eval_prov is sealed as HwShunt, which is what main sealed here: the exfiltration test fails with "an estimated scan sealed as a reading". Reverting eval_prov to is_hardware()'s answer is not caught on these hosts, because with no hardware source both say Estimator. - energy_of returns Energy::measured(0), as main did on the M3 Ultra: four tests fail, including the two formerly hardware-only ones ("a real span costs joules, measured or estimated", "the budget eventually exhausts"). - figure_uj returns the apportioned sum: three joule-code tests fail. The unit tests see 10000000 against 60000000; end to end, 1.373789 J sealed against 65.634219 J. - The meter envelope is always graded ModelBased: three tests fail. End to end: "an estimate sealed in the meter envelope as ModelBased". - main's any-window attribution: the mixed-window test fails. - main's total_uj, the apportioned figure: the end-to-end test fails (45.799836 against 0.776724). - SpanMeter without its provenance() override, so the trait's HwShunt applies: both joule-ui-serve tests fail. - served_meter returns the parent commit's HardwareMeter: the end-to-end test fails with "~24 ms of work sealed at 0 J: Energy { measured_uj: None, estimated_uj: 0, provenance: Estimator }". - energy_word always says "measured": the sandbox-proof test fails. Not separately tested: the per-run reset of the tally. It is observable only with attributed windows, which need a live CPU rail. Clippy --no-deps --all-targets is clean on every changed crate. It is also clean for x86_64-unknown-linux-gnu, except that sandbox-proof could not be checked for that target: zstd-sys's build script needs a Linux C cross compiler, which is not installed here. One pre-existing warning, in jcp-action-receipt's ar-verify.rs, is untouched. Not done here, deliberately: - The joule-ui Meter trait: its default provenance is HwShunt, and its provenance is per meter, not per sample. SpanMeter relies on run_interaction asking for provenance right after its second sample. run_interaction also turns a None sample into Estimator(0), so an Authorizer charges 0 for work that ran. Authorizer::charge carries no provenance. Both joule-ui-interaction examples still use the summing sampler. These are public API and SPEC §5/§6: David's call. - Wire keys named measured_uj now carry estimates: jcp-gateway's _meta and Relayed::Allowed, and joule-ui-serve's POST /action response. The sealed provenance beside each key is right. - A GPU counter alone (NVML without RAPL): the gateway seals it Partial but still debits only the GPU figure, so CPU work goes undebited there. Its two budget tests would fail on such a host, correctly. joule-ui has no coverage field. Not observed: no such host here. - JouleContract §4.2 says an Unaccounted figure seals its method reference (energy_anchor). The harness leaves it None, as it always has. - proof-cascade's joules: FormalOutcome, "(real z3, ModelBased)" in joule-fix, and formal_fix's "µJ measured". Another change owns that meter. - joule-code-remediate's Cargo.toml description still says hardware-measured. This commit does not touch that file. Co-Authored-By: Claude Opus 5.5 <[email protected]>The liveness probe's hardware tests run in CI on the macOS runner, which is the M5 Max this was written on, at load averages of 24-104. The parent commit's tick spun for 25 ms of WALL time, so on a loaded machine each tick burned only the CPU the scheduler gave the thread. Its tests pinned the burn and the group-only subscription with load-dependent bounds: burned CPU at least a quarter of the ticks, and a Frozen verdict on at least 10 intervals. With the tick below, the probe completes 11-13 intervals in its 1 s budget under 2 x ncpu busy-loop spinners (29 on an idle machine), so that floor would have sat one to three intervals from failing. The tick (probe/liveness.rs): - spin(cpu, wall) burns until the thread's CPU clock has advanced PROBE_TICK (25 ms), with a 500 ms wall cap per tick. The real probe passes CLOCK_THREAD_CPUTIME_ID (thread_cpu in ioreport.rs) and a monotonic clock. A loaded machine makes a tick longer, never lighter. - Both clocks are injected, so the rule is tested with scripted ones: a full tick on a third of a core, and a thread that gets no CPU ending at the cap. The loop still takes an injected tick, and the scripted-loop tests are unchanged. What the probe records as it runs (ProbeTrace, returned beside the RailWatch): - the wall time of every FFI sample call; - per interval, the thread CPU its ticks burned, measured around the ticks, apart from the samples. The hardware test the_liveness_probe_never_reports_a_frozen_rail_as_live now asserts: - every interval burned at least PROBE_TICK/2 (only the wall cap can cut a tick short, and the message says so); - the median sample call took under 50 ms (a group sample is ~6-12 ms, one over every channel 0.13-0.8 s), and it prints that median. The ">= 10 intervals" floor, the "burned >= a quarter of the ticks" bound and the ">= 2 intervals for Frozen" check are gone. The cap check stays, with generous slack (5 budgets + 5.5 s). The sampler's values, against the oracle. The new test the_probe_sampler_reads_each_cpu_rails_own_value brackets each of three probe samples between two oracle reads on the oracle's own all-channel subscription. It matches each rail by name and ordinal in the Energy Model group: - where the oracle saw the rail hold, the probe's value must equal it; - where the rail moved, the value must lie between the two reads. This catches a sampler that returns 0, a sum over rails, or another rail's value. the_probe_samples_the_energy_model_group_alone also checks every sampled name with is_cpu_rail, so the FFI filter is pinned on any host (round-3 nit). The oracle reads for its window, and on past it until it has two reads, never past four windows. Fewer than two reads is a test failure with a message, never CpuRailMoved(false). Its load thread runs until the oracle stops reading. Pure pins, each its own test: - a decrease between consecutive samples is not an advance; - a rail new in a sample only sets its baseline; - probe_host is the open-watch-map path the real probe now goes through. A subscription that cannot open, or never yields a sample, goes through status_of to Unavailable, and is never watched; - status_of(None) is Unavailable. The once-per-process cache is pinned process-wide. Six threads, released by one barrier, ask for the status and build the backend at once, and the static PROBE_RUNS counter must read 1. The test that prints "ioreport liveness: status=" keeps its name, and no test was renamed. Evidence, from one lib test binary of this tree (55 tests): - M5 Max (macOS 27.0.1), 10 runs under 36 busy-loop spinners (2 x hw.ncpu), load averages 124-149 (other sessions included). 10/10 passed. Every run printed: 'ioreport liveness: status=CpuRailFrozen oracle=CpuRailMoved(false) selected=false available=false' - median sample cost: 6.93-9.01 ms; - intervals per probe: 11-13; - least burn in one interval: 25.0009-25.0015 ms; - oracle reads: 7-12. Afterwards all 36 spinner PIDs were confirmed gone. - M3 Ultra (macOS 27.0.1), 1 run: 55 passed; median 8.28 ms over 30 calls; 29 intervals; least burn 25.0003 ms; 17 oracle reads; both dies equal to the held oracle values. Mutations, each restored with git checkout (git status clean after each). Every one fails a test on the M5 Max except the one marked: - a decrease counts as an advance: 2 failed; - a rail new in a sample counts as an advance: 2 failed; - no subscription maps to Live: 1 failed; - per-thread cache: 1 failed ('left: 16 right: 1'); - sampler returns 0: 1 failed ('held at 1863990848 ...; the probe read 0'); - sampler reports the GPU rail as CPU Energy: 5 failed; - FFI filter also keeps the GPU rail: 6 failed; - spin sleeps: 4 failed ('a 25ms tick used 8.875µs'); - the real tick sleeps: 2 failed ('interval 0 of 26: the probe burned 8.541µs'); - spin is a no-op: 4 failed; - the real tick is a no-op: 2 failed; - the tick counts wall time: 3 failed; - all-channel subscription: 2 failed ('median sample call took 481.672458ms'); - None maps to CpuRailAbsent: 4 failed; - oracle cut to 1 ms: 2 failed ('the oracle got 1 read(s)'); - PROBE_TICK = 100 ms: 1 failed; - sampler gives each CPU rail the sum of all CPU rails: EQUIVALENT on the M5 Max, which has one CPU rail (55 passed). On the M3 Ultra it fails: 'DIE_0_CPU Energy #0 held at 28237793 ...; the probe read 59082835'. Co-Authored-By: Claude Opus 5.5 <[email protected]>The CPU-rail liveness rule said Live once the same rail advanced in two separate sample intervals. On 2026-09-30 the jouleclaw-energy verifier, on the M5 Max under macOS 27.0.1, showed that two advances can be one batch refresh. A group-only watcher sampling every ~16 ms saw `CPU Energy` go 2,643,843,378 -> 2,705,607,863 (+61,764,485) and then, 64 ms later, -> 2,705,611,298 (+3,435); `MCPU0`, `MCPU1` and `PCPU` each stepped twice with it. This probe samples about every 31 ms, so a probe window that holds such a refresh sees two advancing intervals and says Live, cached for the process. Two real probes did exactly that while the independent oracle saw no sustained movement, coinciding with a refresh. Refreshes are ~30 minutes apart, so this is rare, but it is the failure the rule exists to prevent: a Live status selects IOReport for the life of the process, and every later refresh lands whole in whichever span straddles it, sealed as a measurement. The rule now asks whether one rail KEEPS advancing. Live iff the same rail (name + ordinal) advanced in at least MIN_LIVE_ADVANCES = 5 separate intervals, those advancing intervals are at least 80% of all intervals observed so far (advancing * 5 >= intervals * 4), and the samples so far span at least MIN_LIVE_WINDOW = 300 ms of wall time from the first sample. It is evaluated after every interval and latches Live as soon as all three hold. A refresh of fewer than five steps can never pass; one of five or more steps inside 150 ms cannot pass at any steady sampling pace (five advances in 150 ms need intervals of 37.5 ms or less, and then 300 ms holds eight intervals or more, of which the burst advanced in under two thirds). A live rail at the probe's idle cadence proves itself at the tenth interval, ~310 ms. The rule needs each interval's wall time, so RailWatch::observe takes the wall-clock reading with each sample, and the loop (`watch`) passes its clock read just after the sample returned; RailWatch records them in `at`. LIVE_RAIL_ADVANCES (2) becomes MIN_LIVE_ADVANCES (5), with MIN_LIVE_WINDOW and a pure `sustained(advances, intervals)` beside it. The loop keeps sampling until Live, or until the 1 s budget has elapsed AND at least five intervals were observed; the hard cap stays five budgets. Frozen, Absent and Unavailable map exactly as before. Unchanged: per-rail keys, reading each interval against the previous sample, a decrease or a first appearance not being 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 seam, the Span::stop and run_attributed rules, and the "ioreport liveness: status=" line. The test oracle's "moved" verdict had the same hole: CpuRailMoved(true) on two changes, so the refresh that fooled the probe could also vouch for it. It now says moved only if one rail changed at five reads or more, at four reads in five at least (oracle_saw_it_keep_moving, its own literals). It reads for its whole window and past it until it has five reads, never past four windows, and still fails the test on fewer. Under contention it did extend: two runs took 5 reads over 3.64 s and 3.19 s of a 3 s window. Tests added (scripted clock, ~31 ms an interval unless stated). Those marked (*) fail under the old two-advance rule, as the old-rule run below shows. - (*) the_observed_two_step_refresh_is_frozen: [a,a,a,a+61764485, a+61764485+3435], then flat for a 1 s budget, and the same with the steps two intervals apart: Frozen, never live at any interval. - (*) a_refresh_in_three_to_five_steps_at_the_start_is_frozen: three, four and five steps in consecutive intervals inside 150 ms: Frozen. - (*) an_m3_ultra_refresh_stepping_twice_per_die_is_frozen: DIE_0 and DIE_1 each stepping twice within 64 ms, in step and apart: Frozen. - a_rail_advancing_every_interval_is_live_not_before_five_advances_and_300_ms: live first at interval 10 at 31 ms, 5 at 60 ms, 5 at 75 ms (where 300 ms arrives at the fourth), and stays live. - a_live_rail_missing_one_interval_in_five_is_live (80%, wherever the miss falls: interval 10 at 31 ms, 6 at 100 ms) and a_rail_missing_two_intervals_in_five_is_not_yet_live (60% never, and a rail that missed two of its first five is live only at the tenth, 8 of 10). - a_loaded_host_with_a_live_rail_is_live_after_five_intervals: 100 ms intervals, live at the fifth (500 ms), not the third or fourth; the loop stops there with six samples and five ticks. - two_rails_that_advance_in_turn_are_not_one_live_rail, for two dies and for twin channels, so per-rail keying still decides a verdict now that two single steps no longer could. - Keep-sampling: the_probe_samples_until_live_or_long_enough_to_tell and the_probe_loop_needs_the_budget_and_five_intervals_to_stop (continues past the budget while fewer than five intervals, stops at five, stops at the cap with three); the loop hands the rule each sample with the clock just after it (the_probe_loop_stops_as_soon_as_a_rail_is_live pins `at`). - the_oracle_says_moved_only_for_a_rail_that_changed_at_four_reads_in_five. Real-host-composition (F9) tests, through host_status on a scripted IOReport: the "two advances -> Live" script is now a rail advancing at every sample (Live after 6..=14 samples, and a scripted real_run shows from its own record that it stopped at the first interval the rule allows); new the_production_status_of_the_observed_two_step_refresh_is_frozen (CpuRailFrozen, watched >= 900 ms of the budget); the two-dies test now has the dies advancing in turn for the whole budget, so a sampler that summed the dies would be called Live; frozen-status tests expect five intervals. The same in-turn change was made to the probe_with sum test. Mutations, each a temporary edit restored with git checkout (tree clean after each): - the old rule (MIN_LIVE_ADVANCES = 2, no fraction, no window): 17 failed, including all three (*) tests and the F9 two-step refresh ("a two-step refresh was called Live"). - MIN_LIVE_ADVANCES = 2: 6 failed (e.g. the loaded host went live at the third interval, Some(3)). - fraction check removed: 5 failed (five-step refresh live at interval 10; in-turn dies live; 60% rail live). - window check removed: 7 failed (five-step refresh live at interval 5). - oracle back to ">= 2 changes": 1 failed, the oracle verdict test. Runs. sandbox-meter lib 83 passed, integration 1 passed, on this M5 Max (macOS 27.0.1). Three runs of the lib and integration binaries beside an all-channel IOReport reader (~337 ms a sample): 0 of 6 failed, each "ioreport liveness: status=CpuRailFrozen oracle=CpuRailMoved(false) selected=false available=false". The M3 Ultra (macOS 27.0.1), same binary: 83 passed, "ioreport probe: probed=CpuRailFrozen cached=CpuRailFrozen oracle=CpuRailMoved(false) took=1.240480083s intervals=28 window=1.002887292s rails=[("DIE_0_CPU Energy", 0, 0), ("DIE_1_CPU Energy", 0, 0)]". Consumers: jcp-gateway + jcp-action-receipt 32 passed, joule-code-remediate 13 passed, joule-ui-interaction + joule-ui-serve 12 passed, the rest of sandbox-rs 186 passed. clippy --no-deps on sandbox-meter, all targets: no warnings on aarch64-apple-darwin or x86_64-unknown-linux-gnu (x86_64-apple-darwin shows one pre-existing unused-mut in detect_given, untouched here). Not done here, deliberately: - A refresh of five or more steps whose last interval is stalled well past its tick (a heavily loaded host) could still meet all three conditions; no such refresh has been seen, and the observed ones have two steps. - The same rule in the four sibling meters is being changed separately. Co-Authored-By: Claude Opus 5.5 <[email protected]>WIP: sandbox-meter: a CPU counter that does not keep moving is never a measurement, and no consumer relabels an estimateto sandbox-meter: a CPU counter that does not keep moving is never a measurement, and no consumer relabels an estimateAn allowed `tools/call` comes back with `_meta["science.transaction/jcp"]`: the sealed receipt, `measured_uj` and `budget_remaining_uj`. Since this branch made the gateway seal each call's real provenance, `measured_uj` is the call's cost, which is a hardware reading only where the span was one. On a host with no live energy counter (every macOS 27 host checked) it is the meter's estimate, and the plaintext said nothing about which: the grade existed only inside `receipt_b64`, so a client that read the number without decoding the COSE envelope took an estimate for a measurement. The key keeps its name, because clients already read it. Beside it the block now carries `energy_provenance` (`HwShunt`, `ModelBased` or `Estimator`) and, when the figure reads only part of the call (a GPU counter with no CPU record), `energy_coverage: "Partial"`: the same two labels, with the same omit-when-Whole rule, that the sealed receipt carries. `attach_receipt` takes the cost `Energy` instead of its bare `u64`, so the label cannot drift from the figure. The change is additive: nothing is removed from the block, the receipt bytes are unchanged, and no published JCP or AR-1 vector moves. AR-1's `joules_uj` was documented as "Measured cost in microjoules". It is the work's cost however it was obtained, graded by `energy_provenance`; the field doc, the family table ("measured joules") and AR-1-spec §2.2 now say so, and §9's energy cross-check says it holds only where the figure is `HwShunt`. Doc-only: the encoding and the pack are untouched. Tests. `the_caller_gets_its_receipt_back` now decodes the receipt and asserts that the plaintext `energy_provenance` and `energy_coverage` equal what it sealed, and that a non-hardware meter's call is labelled `Estimator`; on this host it observes `"energy_provenance":"Estimator","measured_uj":26577`. A new `the_plaintext_figure_carries_its_grade` covers every cost shape: Estimator, HwShunt whole, HwShunt Partial, ModelBased. Falsified: removing the `energy_provenance` insert fails both tests (`energy_provenance beside measured_uj`; `left: None, right: Some("Estimator")`). jcp-gateway 13/13, jcp-action-receipt 17 + 3 conformance pass, and `jcp-conformance` reports all checks passed. Clippy is clean on jcp-gateway; its one jcp-action-receipt warning is in the untouched `ar-verify` binary. Co-Authored-By: Claude Opus 5.5 <[email protected]>The crate description promised "a JouleContract receipt with hardware-measured joules sealed by a sandbox meter attestation". The crate does not do that on a host without a live CPU energy counter (every macOS 27 host checked): there its receipts carry an estimate, sealed as JCR-1 `Estimator` / JouleContract `Unaccounted`, as its own module doc says. The description now says the joules are graded by how they were obtained: a hardware reading apportioned to the run and anchored to a sealed meter envelope only where the host exposes a live CPU counter, an estimate sealed as one everywhere else. Two `FormalEntry`/`FormalOutcome` docs that called the proof cascade's `ModelBased` accounting "measured joules" are corrected too. `a_proven_formal_obligation_lets_the_fix_ship` and `a_refuted_formal_obligation_reverts_the_fix` returned before asserting anything when `z3` was absent, so on a solverless host (the joule-code-rs CI job installs none) they passed in 0.00 s whatever the formal gate did. They now follow the convention proof-solvers and joulecontract-proof already use, and that the standards-build workflow's "Install z3" step documents: the suite passes with or without a solver and asserts something either way. With `z3` the solver's verdict is asserted as before. Without it, both assert the gate fails closed: the obligation is Unproved (neither proved nor refuted), the `formal-proof` gate fails while every other gate passes, the fix is reverted and not shipped, and the discharge evidence is still written. Each logs which branch it asserted. Where a solver is supposed to be installed, `JOULE_FIX_EXPECT_Z3=1` turns a missing `z3` into a test failure instead of the solverless branch; this is documented on the test helper and in Cargo.toml beside the proof dependencies. No workflow is changed, so CI still runs the solverless branch until a job installs z3 and sets the variable. The formal gate's detail, which a failed gate copies into its receipt entry, and joule-fix's summary line both said "real z3" even with no solver on PATH. They now say "no z3 on PATH: SMT goals left undecided" in that case. Verified, 13/13 each way: with z3 on PATH; with z3 removed from PATH; with no git identity (GIT_CONFIG_GLOBAL=/dev/null GIT_CONFIG_NOSYSTEM=1 and user.useConfigOnly=true); and with no identity and no z3. `JOULE_FIX_EXPECT_Z3=1` with no z3 fails both tests ("JOULE_FIX_EXPECT_Z3=1, but there is no working `z3` on PATH"); with z3 present it passes. Falsified: letting an unproved obligation pass the gate (`all_proved` without `unproved == 0`) fails both tests with no z3 on PATH. The same mutation against the previous tests passes both, in 0.00 s. Clippy --no-deps on the crate is clean. Co-Authored-By: Claude Opus 5.5 <[email protected]>