Exact

Exact Union RegExp

Repository files (latest commit first)

Filename	Latest commit message	Latest commit date
Transaction Science 340313d6b3 jcp: a live vendor counter is a reading; intercept/1 keeps a partial figure partial ... The questions this branch left open are now decided. A vendor energy counter (RAPL, NVML, Apple IOReport) is a real reading; what it lacks is an independent root, which is a gap in provenance, not in accuracy. It earns the hardware grade only while it is live. The live GPU rail is not reported as a partial reading of CPU work. And a partial figure must stay partial on the intercept/1 wire. The grade. jcp-energy already graded RAPL and NVML `HwShunt`. The IOReport rung carried a live reading at `ModelBased`, in the modeled slot. It now takes the same grade: `Meter::provenance()` says `HwShunt` and a live span is `Energy::measured`. The declined paths keep their own grades: the time×power model is `ModelBased`, the constant estimator `Estimator`. Raising the grade raises the stakes of what `measure()` accepts, so it is gated per span as well. It took any rise of the summed SoC total as the span's energy, and that total rises through the GPU rail, which is machine-wide. On this M5 Max, in this commit's own test runs, the counter counted 32 mJ and then 9.1 J between two reads while an independent oracle saw the CPU rail hold and one other rail move. A rail that was live at selection can still hold across one span: a span shorter than its update interval, or a rail that stops publishing after the probe. The counter now reports the CPU rails' share beside its total, from the same delta sample. `measure()` grades a span `HwShunt` only when the CPU rail itself advanced. The figure is still the SoC total's rise, which, like a RAPL package counter, over-debits the work rather than leaving part of it out. A span whose CPU rail held, or whose read failed, is the time×power figure at `ModelBased`. A model figure is never `HwShunt`. The grading is one pure function, `ioreport_span`, so every branch runs on scripted reads on any platform. The oracle test that checks the counter's total value for value, against its own all-channel subscription, now checks the CPU share the same way. The GPU rail is not reported as a partial reading. It is machine-wide (display compositing moves it), so booking it to a task misattributes energy the task did not spend, and a partial figure would under-debit the budget because the CPU's share would go unmetered. The rung is declined to the whole-task estimate. That rationale now sits in the rung's docs and in SPEC §5.1. SPEC. §5 says `HwShunt` covers vendor counters as well as shunts, and carries the liveness MUST in the shared wording. Its dashes are typeset and `Partial` is code-formatted; the text is otherwise as decided. §5.1 adds the IOReport rung. A new §5.2 defines coverage and its wire encodings, carried only when `Partial`. One is jcp/2's `energy_coverage`, which jcp-receipt already emitted but the SPEC never listed, so §8's core field list gains it. The other is intercept/1's `coverage`. intercept/1. jcp-intercept dropped coverage, so a `Partial` figure handed to it was sealed as the whole step's energy. It now adds `"coverage": "Partial"` only when the figure is partial. `verify` recovers it in a new `InterceptReceipt::coverage`, and refuses any other value, an explicit "Whole" included, because a sealer never produces one. A whole figure seals the same bytes as before. The two envelopes a Redact-then-CallLimit chain sealed at 3fd35db5 were captured by building that commit in a scratch crate before the change, and are pinned hex for hex. A whole `HwShunt` figure's object is compared, key for key and in canonical bytes, against the pre-coverage object. No conformance vector changes, and none contains an intercept/1 receipt. Prose. Provenance::HwShunt's doc names vendor counters and the liveness rule. The README's jcp-energy bullet lists the IOReport rung. Its jcp-gateway bullet no longer says "metered on real hardware ... energy actually spent". jcp-efficiency's MAPPING §4 now says "real readings of the vendor's own energy counter" instead of "power-sensor readings", and that a counter counts only while live. It also no longer calls RAPL "a model, not a meter". Tests. jcp-energy has 54 lib tests (51 before) plus its integration test. jcp-intercept has 12 (8 before). jcp-schema has 30, jcp-conformance its unit test and 5 pack tests, all passing. `jcp-conformance` prints "all checks passed", and jcp-cli builds and runs. clippy --no-deps is clean on jcp-energy and jcp-intercept. jcp-schema's one warning, in flow.rs, is pre-existing. Falsified, each by a temporary edit restored with git checkout: - A live span built with `Energy::modeled` fails `a_span_the_ioreport_cpu_rail_advanced_over_is_a_hardware_reading` and `the_ioreport_rung_stamps_the_hardware_grade`. - `Meter::provenance()` for IOReport set back to `ModelBased` fails `the_ioreport_rung_stamps_the_hardware_grade`. - Gating the span on the SoC total instead of the CPU rail fails `a_span_the_ioreport_cpu_rail_held_over_is_the_models_figure` with "the GPU rail rose, the CPU rail held ... provenance: HwShunt". - A CPU share that counts every rail fails the hardware oracle test: "CPU share rose 18127 µJ ... CPU energy rails rose 0 µJ". That one needs a non-CPU rail to move during the window, and the GPU rail did. - Sealing coverage even when Whole fails the byte-identity tests (and every test that verifies a whole receipt). - Dropping coverage when Partial fails `a_partial_figure_seals_coverage_partial`. - Letting verify read an explicit "Whole" fails `verify_refuses_a_coverage_other_than_partial`. Not done here: - jcp-gateway still seals `Energy::measured` for whatever sandbox-meter returns, estimates included. The sandbox-meter liveness branch fixes that, so the README's gateway line states the rule rather than this branch's gateway. - The NVML rung reports GPU energy as a whole-task `HwShunt` figure. Under the new MUST, a figure for work its counter does not cover (the CPU's share) is `Partial`. That needs its own decision, and nothing here is built with `--features nvml`. Co-Authored-By: Claude Opus 5.5 <[email protected]>		2026-09-30 20:06:16 -04:00
..
src	jcp: a live vendor counter is a reading; intercept/1 keeps a partial figure partial	2026-09-30 20:06:16 -04:00
Cargo.toml	jcp-intercept: attested interceptor chains	2026-07-01 12:10:06 -04:00