an uncalibrated power model is an estimate, not ModelBased #220

Merged

dcharlot merged 8 commits from fix/uncalibrated-model-is-estimate into main 2026-10-11 22:20:18 -04:00

Conversation 0 Commits 8 Files changed 35 +750 -318

dcharlot commented 2026-10-11 10:52:36 -04:00

Owner

Copy link

Why

The JCP metering ladder (jcp/SPEC.md §5.1) defines two of its rungs as:

• Rung 5: wall time × a host-calibrated active power, graded ModelBased.
• Rung 6: a constant estimate, graded Estimator.

Several crates multiplied wall time by a default power that was never calibrated on the host and graded the result ModelBased:

• jcp-energy: 15 W;
• proof-solvers: 15 W;
• aac-core: a constant that works out to 2 W;
• the sandbox microVM and WASM executors: nominal per-vCPU and per-fuel costs, plus a ×10 accelerator proxy;
• sandbox-meter's storage contention: nominal NVMe-class coefficients;
• jouleclaw-fabric: the CPU and AMX seeds;
• wai-web's OTT demo: a figure the page supplies.

By the spec's own ladder these are estimates. Grading them ModelBased claimed better provenance than the figures had.

What

Every figure computed from a constant nobody calibrated on the host is now Estimator. Where a host-calibrated path exists it stays ModelBased:

• jcp-energy: new Meter::UncalibratedTimePower and Rung::UncalibratedTimePower, graded Estimator. detect() falls back to it, and so do the counter, IOReport and per-process spans. Meter::time_power(mw) stays ModelBased and is documented as requiring a power the host measured. jcp-conformance C9 checks both grades.
• proof-solvers: the propositional, SMT and Lean rungs and the grade_attempt fallback are now Estimator. proof-schema gains Energy::estimator.
• aac-core: store receipts are estimates. A doc that said ~2 mW now matches the code, which computes 2 W.
• sandbox:
  • The microVM CPU fallback is Estimator unless the new MicroVmConfig.calibrated is set.
  • The accelerator proxy is always Estimator.
  • WASM fuel cost is Estimator unless the new WasmConfig.fuel_cost_calibrated is set.
  • Storage contention coefficients are Estimator.
  • The boot_microvm example's fallback is Estimator.
• jouleclaw-fabric: the CPU and AMX seeds are Estimated, as the GPU seeds already were.
• wai-web: a figure the page supplies is sealed Estimator.
• Docs: jcp SPEC §5 and rungs 5–6, the proof SPEC §5, sandbox SPEC §6.3 and spec/receipts.md, and the Provenance docs and READMEs.
• One more fix: sandbox-exec-microvm's RAPL/MSR meter tests drove their fake counters from a writer thread on a 2 ms timer. On a loaded host that thread was starved and the probe judged a live fake counter frozen, so the tests flaked on this branch and occasionally on main. The liveness tick now advances the counters itself.

API: the new names are additive. The two new public config fields, MicroVmConfig.calibrated and WasmConfig.fuel_cost_calibrated, would break struct-literal construction outside their crates; there is none in the repo.

Evidence

• Classification sweep: every ModelBased producer in non-test code was classified as calibrated (kept), uncalibrated (regraded), apportionment of a real reading (kept), or pass-through (kept).
• No signed or published vector changed.
  • jcp gen-vectors, proof gen-vectors and aac gen-vectors output is byte-identical.
  • The jcp, proof, aac and sandbox conformance binaries pass.
• Mutation checks: each regrading rule was mutated, and every mutant failed a test.
• Suites:
  • jcp-rs workspace: 484 passed.
  • proof-rs workspace: 161 passed, with z3 and lean present.
  • aac: 592 passed.
  • sandbox-rs workspace: 396 passed. The fixed RAPL/MSR tests passed 16/16, 6 of them with 40 extra busy threads.
  • joule-code-remediate, joulecontract-proof, wai-web, jouleclaw-fabric and l3-jouleclaw also pass.
  • Linux cross-checks are clean.

Not covered

Four sites are over-graded the same way, but regrading them would change signed vectors. They are left for the owner to decide:

• jouleclaw-jcr1 v1.1 vector 12, and the frozen vectors.json entry 6;
• WAI conformance fixtures that use invented ModelBased figures;
• joulecontract-receipt's demotion of an unattested Metered claim to ModelBased.

🤖 Generated with Claude Code

## Why The JCP metering ladder (`jcp/SPEC.md` §5.1) defines two of its rungs as: - **Rung 5:** wall time × a **host-calibrated** active power, graded `ModelBased`. - **Rung 6:** a constant estimate, graded `Estimator`. Several crates multiplied wall time by a default power that was never calibrated on the host and graded the result `ModelBased`: - jcp-energy: 15 W; - proof-solvers: 15 W; - aac-core: a constant that works out to 2 W; - the sandbox microVM and WASM executors: nominal per-vCPU and per-fuel costs, plus a ×10 accelerator proxy; - sandbox-meter's storage contention: nominal NVMe-class coefficients; - jouleclaw-fabric: the CPU and AMX seeds; - wai-web's OTT demo: a figure the page supplies. By the spec's own ladder these are estimates. Grading them `ModelBased` claimed better provenance than the figures had. ## What Every figure computed from a constant nobody calibrated on the host is now `Estimator`. Where a host-calibrated path exists it stays `ModelBased`: - **jcp-energy:** new `Meter::UncalibratedTimePower` and `Rung::UncalibratedTimePower`, graded `Estimator`. `detect()` falls back to it, and so do the counter, IOReport and per-process spans. `Meter::time_power(mw)` stays `ModelBased` and is documented as requiring a power the host measured. jcp-conformance C9 checks both grades. - **proof-solvers:** the propositional, SMT and Lean rungs and the `grade_attempt` fallback are now `Estimator`. proof-schema gains `Energy::estimator`. - **aac-core:** store receipts are estimates. A doc that said ~2 mW now matches the code, which computes 2 W. - **sandbox:** - The microVM CPU fallback is `Estimator` unless the new `MicroVmConfig.calibrated` is set. - The accelerator proxy is always `Estimator`. - WASM fuel cost is `Estimator` unless the new `WasmConfig.fuel_cost_calibrated` is set. - Storage contention coefficients are `Estimator`. - The `boot_microvm` example's fallback is `Estimator`. - **jouleclaw-fabric:** the CPU and AMX seeds are `Estimated`, as the GPU seeds already were. - **wai-web:** a figure the page supplies is sealed `Estimator`. - **Docs:** jcp SPEC §5 and rungs 5–6, the proof SPEC §5, sandbox SPEC §6.3 and `spec/receipts.md`, and the `Provenance` docs and READMEs. - **One more fix:** sandbox-exec-microvm's RAPL/MSR meter tests drove their fake counters from a writer thread on a 2 ms timer. On a loaded host that thread was starved and the probe judged a live fake counter frozen, so the tests flaked on this branch and occasionally on main. The liveness tick now advances the counters itself. **API:** the new names are additive. The two new public config fields, `MicroVmConfig.calibrated` and `WasmConfig.fuel_cost_calibrated`, would break struct-literal construction outside their crates; there is none in the repo. ## Evidence - **Classification sweep:** every `ModelBased` producer in non-test code was classified as calibrated (kept), uncalibrated (regraded), apportionment of a real reading (kept), or pass-through (kept). - **No signed or published vector changed.** - jcp gen-vectors, proof gen-vectors and aac gen-vectors output is byte-identical. - The jcp, proof, aac and sandbox conformance binaries pass. - **Mutation checks:** each regrading rule was mutated, and every mutant failed a test. - **Suites:** - jcp-rs workspace: 484 passed. - proof-rs workspace: 161 passed, with z3 and lean present. - aac: 592 passed. - sandbox-rs workspace: 396 passed. The fixed RAPL/MSR tests passed 16/16, 6 of them with 40 extra busy threads. - joule-code-remediate, joulecontract-proof, wai-web, jouleclaw-fabric and l3-jouleclaw also pass. - Linux cross-checks are clean. ## Not covered Four sites are over-graded the same way, but regrading them would change signed vectors. They are left for the owner to decide: - `jouleclaw-jcr1` v1.1 vector 12, and the frozen `vectors.json` entry 6; - WAI conformance fixtures that use invented `ModelBased` figures; - `joulecontract-receipt`'s demotion of an unattested `Metered` claim to `ModelBased`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 7 commits 2026-10-11 10:52:36 -04:00

jcp-energy: grade time × the default power Estimator, not ModelBased ... 48db538a47

SPEC §5.1 grades rung 5 as wall time × a HOST-CALIBRATED active power
(ModelBased) and rung 6 as an estimate. jcp-energy's ladder fell to
Meter::TimePower at DEFAULT_ACTIVE_MILLIWATTS (15 W, an assumed figure no
host measured) and every counter rung's span degraded to the same 15 W
figure, all graded ModelBased: better provenance than how the figure was
obtained. The power is the whole of that model, so a default power is a
constant scaled by time, an estimate.

- Meter::UncalibratedTimePower { milliwatts } and Rung::UncalibratedTimePower
  (Estimator), built by Meter::uncalibrated_time_power; detect() falls to
  it, so Detection.selected, rung() and provenance() all say estimate.
- Meter::TimePower / Meter::time_power stay ModelBased, documented as a
  power calibrated on this host.
- counter_span / ioreport_span / process_span degrade to the new
  uncalibrated_span (Estimator) instead of Energy::modeled.
- Tests that pinned the over-claim now pin Estimator: the RAPL/NVML/
  per-process/IOReport fallback-span tests, the declined-IOReport meter
  test, and the detect_with selection tests. New tests: a host-calibrated
  power stays ModelBased while the default is Estimator, detect() falls to
  the estimate, and the fallback span helper.
- jcp-conformance C9 now checks both grades.
- SPEC §5 / §5.1 rungs 5-6, jcp-schema's Provenance docs and the README
  say a default or assumed power is rung 6. No vector changes (jcp
  gen-vectors output is byte-identical; no jcp vector carries ModelBased).

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

proof-solvers: grade wall time × the default 15 W Estimator, not ModelBased ... e42c3d1c07

ns_to_uj prices an attempt at wall time × a fixed ~15 W that no host
calibrated, and Propositional, Z3Smt, LeanVerifier and every Z3Server
attempt that is not sealed as a tree reading graded that figure
ModelBased. By the JCP ladder (SPEC §5.1) and the proof SPEC's own
definition a model earns ModelBased by its calibration; an assumed power
scaled by time is an estimate, so the figure claimed better provenance
than how it was obtained.

- proof-schema: Energy::estimator(uj), and Provenance docs that say a
  default or assumed parameter makes a figure Estimator.
- proof-solvers: DEFAULT_ACTIVE_MILLIWATTS (15 W, same arithmetic) and
  wall_time_estimate; all four sites now Energy::estimator. The public
  Modelled / modelled_uj names are kept; their docs say estimate.
- Tests that pinned the over-claim now pin Estimator: grade_attempt's
  unit tests, z3_tree.rs (server(), refuted goal, settle bound, cascade
  total [Estimator, HwShunt] -> Estimator, undeclared z3), and proof-cli
  tests/measure.rs (receipt "provenance Estimator", "stay Estimator").
  New test: every wall-time rung (T0 proved/refused, one-shot z3, an
  absent Lean) is Estimator with no measurement.
- proof-cli, proof-cascade, proof SPEC §5 / README, and joule-code-remediate
  (FormalOutcome docs, joule_fix's printed label) say Estimator.
  proof/conformance/v1 is unchanged: gen-vectors output is byte-identical
  (it seals the stand-in ladder's estimate_tier figures, never ns_to_uj).

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

aac-core: grade the store's elapsed-time receipts Estimator, not ModelBased ... 66137550bc

timed_receipt prices every store mutation (register_user, create_board,
add_cell, record_utterance, predict, set_vocabulary_level) at elapsed
wall time × an assumed draw no device calibrated, and tagged it
ModelBased while its own doc called it "an estimate". By the family's
metering ladder (JCP SPEC §5.1) a model earns ModelBased by its
calibration; an assumed draw scaled by time is rung 6, Estimator.

The figure is unchanged. Its doc said "~2 mW", but 2.0 × elapsed µs is
2 µJ per µs, i.e. 2 W: the doc now says what the code computes.

access-core's Provenance / Receipt docs now say ModelBased is a draw the
device measured and an assumed draw is an estimate. New test
store_receipts_are_estimates. No vector changes (aac gen-vectors output
is byte-identical; the vectors carry no provenance).

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

sandbox-exec-microvm, sandbox-exec-wasm, sandbox-meter: grade nominal-cost figures Estimator ... 490a592223

Three reference estimators priced work by a coefficient no host
calibrated and graded the figure ModelBased:
- sandbox-exec-microvm: with no live CPU counter, vCPU-seconds × the
  reference 12,000 µJ/vCPU-second (a nominal work-unit cost), and the
  accelerator's "coarse proxy" (that cost × 10);
- sandbox-exec-wasm: fuel × the reference 20,000 µJ per million fuel;
- sandbox-meter StorageActivity (from_samples, from_volume): ops and
  bytes × nominal NVMe-class pJ coefficients documented as "calibrated".
By the family's ladder (JCP SPEC §5.1) a model earns ModelBased by a
calibration on the host; a nominal coefficient is the whole of such a
model, so the figure is an estimate.

- MicroVmConfig.calibrated and WasmConfig.fuel_cost_calibrated (both
  false by default) keep a ModelBased path for a cost the operator
  calibrated on the host, as spec/receipts.md's "calibrated table"
  describes; the accelerator proxy is Estimator either way. Neither config
  is constructed outside its crate.
- Tests that pinned the over-claim now pin Estimator:
  cpu_only_run_meters_modelbased (renamed ..._an_estimate),
  a_cpu_counter_that_held_across_a_run_is_not_a_measured_zero, power.rs's
  two RAPL fallback tests, runs_a_unit_and_meters_cpu_energy,
  storage_globs_enforced_through_execution, contention_is_loaded_minus_
  baseline. New tests: a fallback is a model only at a host-calibrated
  cost (CPU) and never for the proxy (accelerator); the same for the fuel
  cost; both storage constructors are estimates.
- boot_microvm example's 15 W/vCPU fallback is Estimator too.
- SPEC §6.3, spec/receipts.md, SECURITY.md, README and sandbox-meter's
  Provenance docs say a nominal or assumed coefficient is Estimator.
No vector changes: sandbox-conformance passes every class, file-backed
vectors included, and conformance/v1 is untouched (its builders use
fixed constructors, none of these estimators).

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

wai-web: seal the OTT demo's page-supplied joules as Estimator, not ModelBased ... 66ed977282

OttSession::new seals whatever non-zero joules_micro the page hands it
as ModelBased. Nothing in the session measured, modelled or calibrated
that figure, so labelling it a model claims better provenance than how
it was obtained (the family's ladder, JCP SPEC §5.1: a model earns
ModelBased by its calibration). It is now sealed Estimator; zero stays
the unmetered marker with no class.

New test a_page_supplied_figure_is_sealed_as_an_estimate. No vector
changes: the OTT session is a demo surface, nothing under a conformance
or vectors directory is produced by it, and reach/record keeps the
package of record as it was.

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

jouleclaw-fabric: seed the CPU and AMX matmul figures Estimated, not Benchmarked ... b22d3cd496

local/cpu-neon (130 mJ/GFLOP) and local/amx (7 mJ/GFLOP) were seeded
Benchmarked, though each is a recorded throughput priced at an ASSUMED
~5 W core draw: the energy was never read. l3-jouleclaw's
projection_grade rightly treats Benchmarked as a calibrated input, so
with JOULECLAW_FABRIC=1 and no calibration row this host recorded, a
projection priced from these seeds was sealed ModelBased: an
uncalibrated constant claiming a model's grade (JCP SPEC §5.1 rung 6).

The seeds are now Estimated, as the GPU seeds already were, so a seeded
projection is an Estimator figure and a host calibration row still
replaces the seed at the grade its writer declared. EnergyProvenance's
docs say an assumed power makes a figure Estimated.

New tests: jouleclaw-fabric every_seeded_figure_is_an_estimate, and
l3-jouleclaw tests/fabric_grade_seeded.rs (fabric on, no calibration
file: the cpu-neon entry is Estimated and the receipt Estimator). The
existing calibrated/estimated fabric-grade tests are unchanged and pass.
No vector carries a fabric seed's grade.

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

sandbox-exec-microvm: the liveness tick advances the fake counters itself ... 93c6b2917c

The RAPL and MSR meter tests drove their fake counters from a writer
thread on a 2 ms timer while the liveness probe slept between samples. On
a loaded host (load ~85 here) the writer was starved for whole sample
intervals, and the probe then judged a live fake counter frozen: the two
tests failed in 1-3 of every 5 runs on this branch and occasionally on
main. Each tick now writes the next rising step and then sleeps, so every
interval the probe samples holds exactly one advance whatever the
scheduler does. 16 of 16 runs passed, 6 of them with 40 extra busy
threads.

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

dcharlot added 1 commit 2026-10-11 17:01:32 -04:00

ci(wai-web-wasm): the native unit-test count is 32 with the OTT grade test ... 743641234a

The wai-web native step pins its test count so a test that stops being
compiled fails instead of passing silently. This branch adds
video_ott::tests::a_page_supplied_figure_is_sealed_as_an_estimate, so the
count is 32; the gate still read 31 and failed the job with every test
green. Name the new test's group in the comment beside the others.

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

dcharlot merged commit fe0282d66b into main 2026-10-11 22:20:18 -04:00

dcharlot referenced this pull request from a commit 2026-10-11 22:20:18 -04:00

Merge pull request 'an uncalibrated power model is an estimate, not ModelBased' (#220) from fix/uncalibrated-model-is-estimate into main

dcharlot referenced this pull request 2026-10-11 22:25:20 -04:00

wai-ops: the bounds pass, certificates from two certifiers, and the operator set's Kani harnesses (D2b) #221

dcharlot referenced this pull request 2026-10-11 22:59:51 -04:00

wai-vector: the default stroke set and the test repertoire, as WSF1 sources expanded by Annex A, and the text vectors (D7-5) #224

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!220

No description provided.