.github/workflows/wai-web-wasm.yml

@@ -147,7 +147,8 @@ jobs:
       # every reject file with its listed class (quantum::tests), and the quantum IDE
       # builds its catalog circuits in its gateset to the same manifests, stores no
       # parameter on a gate other than P, and shows no hash for an invalid circuit
-      # (quantum_toolchain::tests). The count check turns a test that
+      # (quantum_toolchain::tests). The OTT demo seals a figure the page supplies as
+      # an estimate, never a reading (video_ott::tests). The count check turns a test that
       # stopped being compiled into a failure instead of a silent "0 passed".
       - name: wai-web native unit tests
         shell: bash
@@ -155,7 +156,7 @@ jobs:
         run: |
           set -euo pipefail
           cargo test --locked --lib 2>&1 | tee "$RUNNER_TEMP/wai-web-native.log"
-          grep -q "test result: ok. 31 passed; 0 failed" "$RUNNER_TEMP/wai-web-native.log"
+          grep -q "test result: ok. 32 passed; 0 failed" "$RUNNER_TEMP/wai-web-native.log"
       - name: wasm32 int_synth decode equals the frozen native corpus
         shell: bash
         working-directory: wai/wai-web

aac/aac-rs/crates/aac-core/src/store.rs

@@ -31,13 +31,14 @@ use crate::voice::VoiceConfig;
 // store's public API and the web app are unchanged. Transparency only; never billed.
 pub use access_core::Receipt as AacReceipt;
 
-/// Build a model-based receipt from an operation's elapsed wall-time
-/// (~2 mW idle draw for in-memory ops). The energy is an estimate, tagged
-/// `Provenance::ModelBased`.
+/// Build a receipt from an operation's elapsed wall-time: 2 µJ per µs (an
+/// assumed draw of ~2 W for in-memory ops), at least 1 µJ. No device
+/// calibrated that draw, so the figure is an estimate, tagged
+/// `Provenance::Estimator`; `ModelBased` is for a draw the device measured.
 fn timed_receipt(operation: &str, start: Instant) -> AacReceipt {
-    // ~2 mW idle CPU power draw for in-memory ops.
+    // 2 µJ/µs = 2 W, assumed, not measured on this device.
     let energy_uj = ((2.0 * start.elapsed().as_micros() as f64) as u64).max(1);
-    AacReceipt::model_based(operation, energy_uj)
+    AacReceipt::estimate(operation, energy_uj)
 }
 
 // ─── User profile ───────────────────────────────────────────────────────────
@@ -372,4 +373,26 @@ mod tests {
         assert_eq!(updated.boards.len(), 1);
         assert_eq!(updated.boards[0], board.id);
     }
+
+    /// Every store receipt prices its operation by elapsed time × a draw no
+    /// device calibrated, so it is graded `Estimator`, never `ModelBased`,
+    /// with nothing measured, and is at least 1 µJ for work that ran.
+    #[test]
+    fn store_receipts_are_estimates() {
+        use access_core::receipt::Provenance;
+        let mut store = AacStore::new();
+        let (profile, registered) =
+            store.register_user("Cleo", AccessMethod::DirectTouch, VocabularyLevel::Emergent);
+        let (_, board) = store
+            .create_board(&profile.id, "Home", BoardType::Grid, GridLayout::new(2, 2))
+            .expect("profile exists");
+        let levelled = store
+            .set_vocabulary_level(&profile.id, VocabularyLevel::Transitional)
+            .expect("profile exists");
+        for r in [registered, board, levelled, timed_receipt("op", Instant::now())] {
+            assert_eq!(r.provenance, Provenance::Estimator, "{r:?}");
+            assert_eq!(r.measured_uj, 0, "{r:?}");
+            assert!(r.estimated_uj >= 1, "{r:?}");
+        }
+    }
 }

aac/aac-rs/crates/access-core/src/receipt.rs

@@ -18,9 +18,12 @@ use serde::{Deserialize, Serialize};
 pub enum Provenance {
     /// Read from a hardware energy interface. Carries a non-zero `measured`.
     HwShunt,
-    /// Computed from a calibrated per-operation model (e.g. elapsed × draw).
+    /// Computed from a model calibrated on the device or against a reading
+    /// (e.g. elapsed × a draw the device measured).
     ModelBased,
-    /// Coarse constant estimator (e.g. a cascade tier floor). No `measured`.
+    /// A figure nothing calibrated: a coarse constant (e.g. a cascade tier
+    /// floor), or a model at an assumed parameter (e.g. elapsed × an assumed
+    /// draw). No `measured`.
     Estimator,
 }
 
@@ -38,7 +41,8 @@ pub struct Receipt {
 }
 
 impl Receipt {
-    /// A coarse estimator receipt (cascade-tier floor, no hardware reading).
+    /// An estimator receipt: a figure nothing calibrated (a cascade-tier
+    /// floor, or elapsed wall-time × an assumed draw), no hardware reading.
     pub fn estimate(operation: impl Into<String>, estimated_uj: u64) -> Self {
         Self {
             operation: operation.into(),
@@ -48,7 +52,9 @@ impl Receipt {
         }
     }
 
-    /// A model-based receipt (e.g. elapsed wall-time × idle draw).
+    /// A model-based receipt: a model calibrated on the device or against a
+    /// reading (e.g. elapsed wall-time × a draw the device measured). An
+    /// assumed draw is an estimate: [`Receipt::estimate`].
     pub fn model_based(operation: impl Into<String>, estimated_uj: u64) -> Self {
         Self {
             operation: operation.into(),

jcp/README.md

@@ -45,7 +45,7 @@ jcp/
 - **`jcp-trace`** — ingests an agent run's **OpenTelemetry GenAI trace** (`gen_ai.*` semantic conventions: `chat` / `tool` / `retriever` spans with token usage) and its **evaluation assessments** (judge / human / code feedback), attaches **per-span joules** (measured where a meter is present, else `Estimator` from token counts — provenance never silently upgrades), and seals one **`eval/1` JCR-1 receipt**: the per-span token + joule breakdown with the headline `uj_per_accepted_token` at the **weakest** provenance present, the assessments, a deterministic **quality-gate** verdict (the sealed, declarative analog of a CI assert), and a **readiness projection** an ARL validation-axis claim consumes. The observability stacks *record* a trace and *log* a judge score in a table; this is the interop projection that **seals** the same trace, puts a joule on it, and hash-chains it via `EvalLog` — no new cryptography. The **gate is content-addressed**, so the sealed receipt commits to exactly which bar it was judged against (a tamper-evident artifact, not a mutable in-code `assert`), and **`align_threshold` / `Judge`** calibrate a judge's decision threshold to human pass/fail labels — judge alignment as a reproducible number, not a UI click. Behind the `server` feature, a std-only **OTLP `/v1/traces` receiver** lets any OpenTelemetry exporter POST a `gen_ai.*` trace (with its assessments) and get the sealed `eval/1` receipt back the instant the run ends.
 - **`jcp-intercept`** — **attested interceptor chains**: a composable, ordered pipeline of transforms *around* each model and tool call — the `before_model` / `after_model` / `before_tool` seams an agent's middleware stack runs, composed onion-order (forward in, reverse out) and stopping at the first refusal or human-approval hold. An interceptor may inspect or **rewrite** the request (redact a secret before it reaches the model, trim stale context), **refuse** it, or **hold** it for a human. The difference from the incumbent's arbitrary in-process hooks: every step seals an **`intercept/1`** JCR-1 receipt carrying the request digest **before and after** the step (so a redaction or a trim is provable — the content itself never sealed, only its hash), the seam, the outcome, and the **metered joules** at their honest provenance, hash-chained — the exact transform pipeline that produced a model request becomes reconstructable and verifiable by anyone, and a step cannot run un-sealed. Three reference interceptors — `Redact` (a content transform), `CallLimit` (a guardrail), `Approve` (a human-in-the-loop hold) — each reuse a primitive the family already holds rather than reinventing it.
 - **`jcp-efficiency`** — the **energy-efficiency spec**, surfaced as a sealed receipt. The dark-factory economics turn on four figures — **joules per accepted token, tokens per second, value per token, and the tokens/joules/dollars spent per COMPLETED, VERIFIED unit of work** — and the incumbents publish, at best, a *rate* (cost per token) that can't tell you whether the spend bought a result. An **`efficiency/1`** JCR-1 receipt records all four at honest provenance, hash-chained, with the one thing the rates omit: the **outcome anchor** (`completed` + a verdict). A measurement that didn't complete is spend that bought nothing, and the receipt says so. `aggregate` then splits value-delivered from total spend across a chain — charging *every* attempt (including the failed ones) against the results actually delivered — so `tokens_per_completed_unit` / `uj_per_completed_unit` / `value_per_joule` become the honest efficiency a "cost per token" number is designed to hide. Integers and strings only (JCR-1 forbids bools/floats); the rate figures recompute from the sealed inputs on read.
-- **`jcp-energy`** — the metering ladder (SPEC §5.1): RAPL package counters (Linux powercap, wraparound-corrected, `HwShunt`, only while every package counter is live — `rapl_status()`), NVML GPU energy behind the `nvml` feature (`HwShunt` and `Partial`, since it does not read the CPU's share; only while live — `nvml_status()`), the macOS kernel's per-process CPU energy count (`proc_pid_rusage`'s `ri_energy_nj`; `HwShunt`, whole for in-process CPU work, only while live — `process_energy_status()`; it covers this process's threads, not children, the GPU or DRAM, so a span that reaps a child process or ends with one is `Partial`; it is live on macOS 27.0.1 where IOReport's CPU rails are not), Apple Silicon IOReport (`HwShunt`, only while every CPU energy rail, each die's on a multi-die part, is live — on macOS 27.0.1 that rail is republished in lumps, so there the rung is declined and `ioreport_status()` says why; `Meter::detect_explained()` names the rung selected and why each one above it was declined), a time×calibrated-power model (`ModelBased`, always available), and a constant per-op estimator (`Estimator`). A vendor counter's reading is real but vendor-opaque and relayed by the platform, and it counts as a reading only while the counter is live (SPEC §5). Measured when the platform exposes it, estimated when it doesn't — and the provenance always says which; a hardware backend that fails mid-reading degrades honestly to the model.
+- **`jcp-energy`** — the metering ladder (SPEC §5.1): RAPL package counters (Linux powercap, wraparound-corrected, `HwShunt`, only while every package counter is live — `rapl_status()`), NVML GPU energy behind the `nvml` feature (`HwShunt` and `Partial`, since it does not read the CPU's share; only while live — `nvml_status()`), the macOS kernel's per-process CPU energy count (`proc_pid_rusage`'s `ri_energy_nj`; `HwShunt`, whole for in-process CPU work, only while live — `process_energy_status()`; it covers this process's threads, not children, the GPU or DRAM, so a span that reaps a child process or ends with one is `Partial`; it is live on macOS 27.0.1 where IOReport's CPU rails are not), Apple Silicon IOReport (`HwShunt`, only while every CPU energy rail, each die's on a multi-die part, is live — on macOS 27.0.1 that rail is republished in lumps, so there the rung is declined and `ioreport_status()` says why; `Meter::detect_explained()` names the rung selected and why each one above it was declined), a time×power model at a power the host calibrated (`ModelBased`, `Meter::time_power`), and estimates no host calibrated (`Estimator`): time × the documented default power — the rung `Meter::detect()` falls to, always available — and a constant per-op figure. A vendor counter's reading is real but vendor-opaque and relayed by the platform, and it counts as a reading only while the counter is live (SPEC §5). Measured when the platform exposes it, estimated when it doesn't — and the provenance always says which; a hardware backend that fails mid-reading degrades honestly to the default-power estimate.
 - **`jcp-gateway`** — the **energy-native MCP gateway**: a JCP enforcement point that sits in front of an MCP server so an existing client/server pair keeps its transport while every `tools/call` becomes capability-scoped, joule-budgeted, and sealed. The novel mechanic is two-phase metered enforcement: the call is *authorized* before it runs (no debit, because the cost isn't yet known), the upstream call is **metered** by the sibling Sandbox standard's energy probe (Apple Silicon IOReport, RAPL, NVML — vendor energy counters, whose readings are real but vendor-opaque and relayed by the platform, and which count as readings only while the counter is live for the work, SPEC §5; otherwise the figure is an estimate and is graded as one), and the metered joules are debited from the grant — so the budget that stops a runaway agent is denominated in joules, not a token estimate. Where the upstream server is a local process whose CPU energy the host's kernel counts live (macOS `proc_pid_rusage`), each call is read on that server's own process tree, the work's own process rather than the machine (SPEC §5.1, rung 3): sealed `HwShunt`, and `Whole` only when nothing was seen missing from the tree (no descendant reaped or exited in the span, no GPU client held, no in-process Neural Engine memory, every member read and quiet at both ends) and the operator has declared, with `--upstream-self-contained`, that the server hands no work to a process outside its tree; otherwise `Partial`, with the response's `_meta` naming why. Every decision, allow and deny, seals into a **hash-chained receipt log**: excise, reorder, or splice a receipt and the chain breaks at that point. A denied call never reaches the server (the live 2025–26 MCP exploits land on tool *output*, which the gateway frames as untrusted `data` that can never exercise a capability), and the `jcp-gateway` binary runs it over stdio in front of any MCP-server subprocess. This is the chokepoint the AI-gateway field occupies, on the two axes nobody there holds: the unit of account is the joule, and the audit is cryptographic and tamper-evident rather than a dollar figure and a span.
 - **`jcp-wire`** — the `jcp/1` wire binding (SPEC §11): 4-byte length prefix + canonical det-CBOR over any byte stream, with TCP and Unix-socket endpoints and a client. The decoder rejects non-canonical bodies, so a message has exactly one wire form. Requests carry the full delegation chain and are **caller-signed** — the endpoint authenticates from the request itself and denies an impersonation `bad-signature`, sealed like any other decision. Responses carry the deterministic decision and the sealed receipt.
 - **`jcp-threshold`** — threshold actors (SPEC §2.2): a `did:key` whose private key is split k-of-n with FROST (RFC 9591); the group key is an ordinary Ed25519 key, so a 2-of-3 team issues, holds, and signs wire requests with nothing else in JCP changing. Shares come from a trusted dealer or **distributed key generation** — with DKG the group's private key never exists anywhere, not even momentarily. The two-agent rule for irreversible actions, refused by arithmetic rather than policy.

jcp/SPEC.md

@@ -517,9 +517,11 @@ choosing between those without asking is a decision the record does not support.
 ## 5. Energy (REQUIRED)
 
 Every metered cost is integer microjoules with a provenance tag: `HwShunt`
-(hardware reading; a measured figure REQUIRED), `ModelBased` (calibrated model;
-measured MAY be absent), or `Estimator` (coarse constant; measured MUST be
-absent). The runtime debits `cost.uj()` from a grant's remaining budget on every
+(hardware reading; a measured figure REQUIRED), `ModelBased` (a model
+calibrated on the host or against a reading, or a real reading apportioned by
+a model; measured MAY be absent), or `Estimator` (a figure nothing calibrated:
+a coarse constant, or a model run at a default or assumed parameter, such as
+time × a default power; measured MUST be absent). The runtime debits `cost.uj()` from a grant's remaining budget on every
 allow; the coupling MUST be enforced. The energy axis is what no existing
 agentic protocol standardizes — JCP makes it a precondition, not a report.
 
@@ -596,7 +598,8 @@ and the provenance always says which.** There is always an estimate: an
 environment with no energy interface still yields a usable figure, it just
 carries `ModelBased` or `Estimator` provenance instead of `HwShunt`. A figure
 MUST NOT claim better provenance than how it was obtained — including when a
-hardware backend fails mid-reading and the figure degrades to a model.
+hardware backend fails mid-reading and the figure degrades to a model or an
+estimate (rungs 5 and 6 below).
 
 Recommended ladder, best first:
 
@@ -807,9 +810,19 @@ Recommended ladder, best first:
    moves it), so booking it to a task misattributes energy the task did not
    spend, and the partial figure would under-debit the budget, the CPU's share
    going unmetered. The whole-task estimate below is the honest figure.
-5. **Time × calibrated power** — wall-clock duration times a host-calibrated
-   active power → `ModelBased`. Always available.
-6. **Constant per-operation estimate** → `Estimator`.
+5. **Time × calibrated power** — wall-clock duration times an active power
+   calibrated on the host (a measurement of that host's draw, such as its
+   draw under load read from a shunt or a live counter) → `ModelBased`.
+6. **Estimate** → `Estimator`: a figure no host calibrated. Either wall-clock
+   duration times a default or assumed active power — a documented default,
+   a nameplate or datasheet figure, another host's calibration — or a
+   constant per-operation figure. Always available. Time × power is graded by
+   its power: the power is the whole of the model, so a power not calibrated
+   on the host makes the figure a constant scaled by time, and grading it
+   `ModelBased` would claim better provenance than how it was obtained. A
+   counter rung's span that degrades because its counter did not read the
+   span (above) lands here, unless the implementation holds a host-calibrated
+   power, in which case it lands on rung 5.
 
 ### 5.2 Coverage (REQUIRED where a figure is partial)
 

jcp/jcp-rs/crates/jcp-conformance/src/lib.rs

@@ -527,7 +527,8 @@ fn c9_energy() -> Result<(), String> {
     let detected = jcp_energy::Meter::detect();
     let (_, e) = detected.measure(|| ());
     e.check_provenance().map_err(|err| format!("detected meter dishonest: {err}"))?;
-    // the model backend scales with work and says it's a model
+    // the model backend, at a power the host calibrated, scales with work and
+    // says it's a model
     let tp = jcp_energy::Meter::time_power(15_000);
     let (_, modeled) = tp.measure(|| std::thread::sleep(std::time::Duration::from_millis(2)));
     if modeled.measured_uj.is_some() {
@@ -536,6 +537,19 @@ fn c9_energy() -> Result<(), String> {
     if modeled.uj() == 0 {
         return Err("the time×power model produced zero energy for real work".into());
     }
+    if modeled.provenance != Provenance::ModelBased {
+        return Err(format!("a host-calibrated time×power figure was graded {:?}", modeled.provenance));
+    }
+    // the same arithmetic at the default power, which no host calibrated, is
+    // an estimate (SPEC §5.1 rung 6), never a model
+    let default = jcp_energy::Meter::uncalibrated_time_power(jcp_energy::DEFAULT_ACTIVE_MILLIWATTS);
+    let (_, assumed) = default.measure(|| std::thread::sleep(std::time::Duration::from_millis(2)));
+    if assumed.provenance != Provenance::Estimator || assumed.measured_uj.is_some() || assumed.uj() == 0 {
+        return Err(format!("the default-power time×power figure is not an estimate: {assumed:?}"));
+    }
+    if detected.rung() == jcp_energy::Rung::UncalibratedTimePower && e.provenance != Provenance::Estimator {
+        return Err(format!("the ladder's default-power rung graded its figure {:?}", e.provenance));
+    }
     // the constant estimator is constant and says it's an estimate
     let (_, est) = jcp_energy::Meter::constant(500).measure(|| ());
     if est.uj() != 500 || est.measured_uj.is_some() {

jcp/jcp-rs/crates/jcp-energy/src/lib.rs

@@ -22,14 +22,14 @@
 //!    wraparound-corrected at its own range; never `psys` (the platform zone,
 //!    which already includes the packages), a top-level `dram` zone, or a
 //!    package's subzones. A span over which no package counter advanced is the
-//!    time×power model's figure.
+//!    default-power estimate (rung 6).
 //! 2. **NVML** (feature `nvml`) — GPU energy via `libnvidia-ml`,
 //!    `Provenance::HwShunt` with `Coverage::Partial`: the counter reads the
 //!    GPU, so the CPU's share of the work is unmetered and the figure never
 //!    claims the whole task. Only while the counter is live ([`nvml_status`])
 //!    and plausibly counts the board's energy: over the probe it ran no
 //!    faster than the board can draw ([`CounterStatus::Implausible`]); a span
-//!    over which it did not advance is the model's whole-task figure.
+//!    over which it did not advance is the whole-task default-power estimate.
 //! 3. **Per-process CPU energy** (macOS) — the kernel's count of this
 //!    process's own CPU energy, `ri_energy_nj` from
 //!    `proc_pid_rusage(getpid(), RUSAGE_INFO_V6)` (public libproc, no
@@ -44,7 +44,8 @@
 //!    IOReport because it attributes the work's own CPU energy, where
 //!    IOReport's SoC-wide counter includes every other process. It is live
 //!    for an unprivileged reader on macOS 27.0.1, where IOReport's CPU rails
-//!    are not. A span over which it did not advance is the model's figure.
+//!    are not. A span over which it did not advance is the default-power
+//!    estimate.
 //! 4. **IOReport** (Apple Silicon) — the on-die SoC Energy Model counters via
 //!    Apple's IOReport C API (no sudo, no external binary), `Provenance::HwShunt`.
 //!    Like RAPL and NVML it is a vendor energy counter: the count is a real
@@ -63,8 +64,9 @@
 //!    steps, is not a live rail, and one live die beside a frozen one is not a
 //!    live CPU: the figure would miss the frozen die. Otherwise the
 //!    platform is not exposing CPU energy, so by the rule above this rung is
-//!    declined and the time×power model estimates instead. A span whose CPU
-//!    rail did not advance is the model's figure too, never a reading.
+//!    declined and the default-power time×power figure estimates instead. A
+//!    span whose CPU rail did not advance is that estimate too, never a
+//!    reading.
 //!
 //!    Declined, the rung does not report the GPU rail as a partial reading of
 //!    the work, though on an M5 Max that rail stays live: it is machine-wide —
@@ -72,19 +74,30 @@
 //!    energy the task did not spend, and a partial figure would under-debit the
 //!    budget, the CPU's share of the work going unmetered. The whole-task
 //!    estimate stands.
-//! 5. **Time × power model** — wall-clock duration times a calibrated active
-//!    power, `Provenance::ModelBased`. Always available.
-//! 6. **Constant estimator** — a fixed per-operation figure,
-//!    `Provenance::Estimator`. For environments without even a usable clock.
+//! 5. **Time × calibrated power** — wall-clock duration times an active power
+//!    the host calibrated ([`Meter::time_power`]), `Provenance::ModelBased`.
+//! 6. **Estimate** — a figure no host calibrated, `Provenance::Estimator`:
+//!    wall-clock duration times a default active power
+//!    ([`Meter::uncalibrated_time_power`], [`DEFAULT_ACTIVE_MILLIWATTS`]),
+//!    which [`Meter::detect`] falls to when no counter rung is admitted and
+//!    which every counter rung's span degrades to when its counter did not
+//!    read the span; or a fixed per-operation figure ([`Meter::constant`]),
+//!    for environments without even a usable clock. Always available.
+//!
+//! A time×power figure is `ModelBased` only when its power was calibrated on
+//! the host: the power is the whole of the model, so a default power is a
+//! constant the figure merely scales by time, and the figure is an estimate.
 
 use std::time::Instant;
 
 use jcp_schema::{Energy, Provenance};
 
-/// Default calibrated active power for the time×power model, in milliwatts.
-/// A deliberate, documented calibration point — order-of-magnitude package
-/// draw for a busy core — meant to be replaced by a measured calibration on
-/// the deployment host (`Meter::time_power(mw)`).
+/// Default active power for the time×power figure, in milliwatts: an
+/// order-of-magnitude package draw for a busy core, assumed, not measured on
+/// any host. A figure at this power is an estimate, `Provenance::Estimator`
+/// ([`Meter::uncalibrated_time_power`]); a power calibrated on the deployment
+/// host makes the figure a model, `Provenance::ModelBased`
+/// ([`Meter::time_power`]).
 pub const DEFAULT_ACTIVE_MILLIWATTS: u64 = 15_000;
 
 /// RAPL package-energy reader (Linux `powercap`). Reads `energy_uj` for every
@@ -716,7 +729,7 @@ fn rapl_probe_runs() -> usize {
 /// sums them all: one live package beside a frozen one would leave the frozen
 /// package's energy out of a figure graded whole. A counter that holds, or is
 /// republished in lumps (a virtualised powercap tree can be either), is
-/// declined to the time×power model. Only the package zones are probed, as
+/// declined to the default-power estimate. Only the package zones are probed, as
 /// only they are summed: a live `psys` or `dram` zone beside a held package
 /// does not make the counter live. Where there is no readable powercap tree —
 /// not Linux, no RAPL, no package zone (a host exposing only `psys`), or an
@@ -4837,9 +4850,10 @@ mod ioreport {
         ///
         /// When it is not, the status says why (never `Live`), and the meter
         /// the ladder fell to still meters real work honestly: 100 ms of CPU
-        /// work is the time×power model's figure, at least 100 ms at the
-        /// documented default power, tagged `ModelBased` with no measurement.
-        /// Never a floored or zero figure for work that ran.
+        /// work is the time×power figure, at least 100 ms at the documented
+        /// default power, tagged `Estimator` with no measurement — the power
+        /// is assumed, not calibrated on this host. Never a floored or zero
+        /// figure for work that ran.
         #[test]
         fn a_selected_ioreport_meter_meters_cpu_work() {
             let _hw = crate::ioreport_hw_lock();
@@ -4890,7 +4904,7 @@ mod ioreport {
                     e.measured_uj
                 );
                 e.check_provenance().expect("the declined meter's figure must be internally consistent");
-                assert_eq!(e.provenance, jcp_schema::Provenance::ModelBased, "the declined meter's figure is not ModelBased");
+                assert_eq!(e.provenance, jcp_schema::Provenance::Estimator, "the declined meter's figure is not an estimate");
                 assert!(e.measured_uj.is_none(), "the declined meter claimed a measurement: {:?}", e.measured_uj);
                 assert!(e.uj() > 0, "the declined meter metered {work:?} of CPU work as 0 µJ");
                 assert!(
@@ -5069,7 +5083,7 @@ pub const CPU_RAIL_LIVENESS_BUDGET: std::time::Duration = std::time::Duration::f
 /// calling thread: about one `CPU_RAIL_LIVENESS_BUDGET` of wall time burning CPU
 /// when the rail is not live (at most five, if IOReport samples are very slow or keep
 /// failing), less when it is. Exposed so a caller, or a receipt, can say *why* an Apple
-/// Silicon host is being metered by the time×power model instead.
+/// Silicon host is being metered by the default-power estimate instead.
 pub fn ioreport_status() -> IoReportStatus {
     #[cfg(target_os = "macos")]
     {
@@ -5177,15 +5191,15 @@ pub fn ioreport_energy_model_opens() -> usize {
 pub enum Meter {
     /// Hardware CPU package energy → `Provenance::HwShunt`. [`Meter::detect`]
     /// selects it only while every package counter is live ([`rapl_status`]), and
-    /// a span over which no package counter advanced is the time×power model's
-    /// figure.
+    /// a span over which no package counter advanced is the default-power
+    /// estimate (`counter_span`).
     Rapl(Rapl),
     /// Hardware GPU energy → `Provenance::HwShunt`, `Coverage::Partial`: the
     /// counter reads the GPU, and the CPU's share of the work goes unmetered,
     /// so a figure from it never claims the whole task (SPEC §5).
     /// [`Meter::detect`] selects it only while the counter is live
     /// ([`nvml_status`]), and a span over which it did not advance is the
-    /// time×power model's whole-task figure.
+    /// whole-task default-power estimate.
     #[cfg(feature = "nvml")]
     Nvml(Box<Nvml>),
     /// This process's CPU energy, as the kernel counts it for this process's
@@ -5200,17 +5214,25 @@ pub enum Meter {
     /// handed to the GPU is not detected. [`Meter::detect`] selects it only
     /// while the counter is live
     /// ([`process_energy_status`]), and a span over which it did not advance is
-    /// the time×power model's figure (`process_span`).
+    /// the default-power estimate (`process_span`).
     #[cfg(target_os = "macos")]
     ProcessEnergy(process_energy::ProcessEnergy),
     /// Apple Silicon IOReport Energy Model energy → `Provenance::HwShunt`, the
     /// grade of RAPL's and NVML's vendor counters. [`Meter::detect`] selects it
     /// only while every CPU energy rail is live, and a span over which no CPU
-    /// rail advanced is the time×power model's figure (`ioreport_span`).
+    /// rail advanced is the default-power estimate (`ioreport_span`).
     #[cfg(target_os = "macos")]
     IoReport(ioreport::IoReport),
-    /// Wall-clock × calibrated active power → `Provenance::ModelBased`.
+    /// Wall-clock × an active power calibrated on this host →
+    /// `Provenance::ModelBased` ([`Meter::time_power`]).
     TimePower { milliwatts: u64 },
+    /// Wall-clock × an active power no host calibrated — the documented
+    /// default ([`DEFAULT_ACTIVE_MILLIWATTS`]), or any other assumed figure →
+    /// `Provenance::Estimator` ([`Meter::uncalibrated_time_power`]). The rung
+    /// [`Meter::detect`] falls to when no counter rung is admitted: it scales
+    /// with the work's duration, but the power it scales by is a constant
+    /// nothing measured, so the figure claims no better than an estimate.
+    UncalibratedTimePower { milliwatts: u64 },
     /// Fixed per-operation figure → `Provenance::Estimator`.
     Const { per_op_uj: u64 },
 }
@@ -5228,8 +5250,10 @@ pub enum Rung {
     ProcessEnergy,
     /// IOReport's SoC Energy Model counters (Apple Silicon).
     IoReport,
-    /// The time×power model.
+    /// The time×power model at a host-calibrated power (`ModelBased`).
     TimePower,
+    /// The time×power figure at a power no host calibrated (`Estimator`).
+    UncalibratedTimePower,
     /// The constant per-operation estimator.
     Constant,
 }
@@ -5297,8 +5321,12 @@ impl Ladder<'static> {
 
 impl Meter {
     /// Pick the best backend this environment exposes. Never fails: when no
-    /// hardware interface exists the result is the time×power model — there is
-    /// always an estimate, it just says so in its provenance.
+    /// hardware interface exists the result is the time×power figure at the
+    /// default power ([`Meter::UncalibratedTimePower`], `Estimator`) — there
+    /// is always an estimate, it just says so in its provenance. Nothing here
+    /// calibrates a power, so `detect` never selects the `ModelBased`
+    /// [`Meter::TimePower`]: a caller holding a power the host measured builds
+    /// that rung itself ([`Meter::time_power`]).
     ///
     /// A vendor counter rung is selected only while its counter is live (SPEC
     /// §5): RAPL on [`rapl_status`], NVML on [`nvml_status`], the per-process
@@ -5329,8 +5357,13 @@ impl Meter {
     /// [`Meter::detect_explained`] on a given ladder. Each counter rung is
     /// opened only when its status admits it ([`select`], [`admits`]).
     fn detect_with(ladder: &Ladder<'_>) -> (Self, Detection) {
-        let mut why =
-            Detection { selected: Rung::TimePower, rapl: None, nvml: None, process_energy: None, ioreport: None };
+        let mut why = Detection {
+            selected: Rung::UncalibratedTimePower,
+            rapl: None,
+            nvml: None,
+            process_energy: None,
+            ioreport: None,
+        };
         // Opening a counter is not enough: it must be live (SPEC §5), or a
         // count republished in lumps landing in one span is graded a hardware
         // reading of that span's work.
@@ -5359,7 +5392,7 @@ impl Meter {
                 return why.selecting(Meter::IoReport(m));
             }
         }
-        why.selecting(Meter::TimePower { milliwatts: DEFAULT_ACTIVE_MILLIWATTS })
+        why.selecting(Meter::uncalibrated_time_power(DEFAULT_ACTIVE_MILLIWATTS))
     }
 
     /// The rung this meter is.
@@ -5373,15 +5406,29 @@ impl Meter {
             #[cfg(target_os = "macos")]
             Meter::IoReport(_) => Rung::IoReport,
             Meter::TimePower { .. } => Rung::TimePower,
+            Meter::UncalibratedTimePower { .. } => Rung::UncalibratedTimePower,
             Meter::Const { .. } => Rung::Constant,
         }
     }
 
-    /// A time×power model with a host-calibrated active power.
+    /// A time×power model with an active power calibrated on this host — a
+    /// figure a measurement on the deployment host produced, such as its draw
+    /// under load read from a shunt or a live counter → `ModelBased` (SPEC
+    /// §5.1 rung 5). A power taken from anywhere else (the documented
+    /// default, a nameplate or datasheet figure, another host's calibration)
+    /// is not a calibration of this host: build
+    /// [`Meter::uncalibrated_time_power`] with it, an estimate.
     pub fn time_power(milliwatts: u64) -> Self {
         Meter::TimePower { milliwatts }
     }
 
+    /// A time×power figure with an active power no host calibrated — the
+    /// documented default ([`DEFAULT_ACTIVE_MILLIWATTS`]), a nameplate or
+    /// datasheet figure → `Estimator` (SPEC §5.1 rung 6).
+    pub fn uncalibrated_time_power(milliwatts: u64) -> Self {
+        Meter::UncalibratedTimePower { milliwatts }
+    }
+
     /// A constant per-operation estimator.
     pub fn constant(per_op_uj: u64) -> Self {
         Meter::Const { per_op_uj }
@@ -5398,14 +5445,14 @@ impl Meter {
             #[cfg(target_os = "macos")]
             Meter::IoReport(_) => Provenance::HwShunt,
             Meter::TimePower { .. } => Provenance::ModelBased,
-            Meter::Const { .. } => Provenance::Estimator,
+            Meter::UncalibratedTimePower { .. } | Meter::Const { .. } => Provenance::Estimator,
         }
     }
 
     /// Run `work` and meter it. The returned [`Energy`] carries the honest
     /// provenance of however the figure was obtained — including when a
     /// hardware backend fails mid-read and the figure degrades to the
-    /// time×power estimate.
+    /// time×power figure at the default power, an `Estimator` figure.
     pub fn measure<T>(&self, work: impl FnOnce() -> T) -> (T, Energy) {
         match self {
             Meter::Rapl(r) => {
@@ -5454,6 +5501,11 @@ impl Meter {
                 let out = work();
                 (out, Energy::modeled(time_power_uj(started.elapsed().as_nanos(), *milliwatts)))
             }
+            Meter::UncalibratedTimePower { milliwatts } => {
+                let started = Instant::now();
+                let out = work();
+                (out, Energy::estimator(time_power_uj(started.elapsed().as_nanos(), *milliwatts)))
+            }
             Meter::Const { per_op_uj } => (work(), Energy::estimator(*per_op_uj)),
         }
     }
@@ -6165,28 +6217,39 @@ struct IoReportReading {
 /// span shorter than its update interval, or a rail that has since stopped
 /// publishing — and then the total can rise only through rails this work did
 /// not drive (the machine-wide GPU rail moves with display compositing). That
-/// is not a reading of the work, so the span is the time×power model's figure,
-/// `ModelBased`, as it is when a read fails. Never `HwShunt` on a model figure.
+/// is not a reading of the work, so the span is the time×power figure at the
+/// default power, `Estimator`, as it is when a read fails
+/// ([`uncalibrated_span`]). Never `HwShunt` on a figure no counter read.
 #[cfg_attr(not(target_os = "macos"), allow(dead_code))]
 fn ioreport_span(before: Option<IoReportReading>, after: Option<IoReportReading>, elapsed_ns: u128) -> Energy {
     match (before, after) {
         (Some(b), Some(a)) if a.cpu_uj > b.cpu_uj => Energy::measured(a.total_uj.saturating_sub(b.total_uj)),
-        _ => Energy::modeled(time_power_uj(elapsed_ns, DEFAULT_ACTIVE_MILLIWATTS)),
+        _ => uncalibrated_span(elapsed_ns),
     }
 }
 
+/// The figure for a span no counter read: its wall-clock duration times the
+/// default active power ([`DEFAULT_ACTIVE_MILLIWATTS`]), `Estimator`. The
+/// power is assumed, not calibrated on this host, so the figure is an
+/// estimate (SPEC §5.1 rung 6), never `ModelBased`: a model's grade is earned
+/// by its calibration, and this one has none.
+fn uncalibrated_span(elapsed_ns: u128) -> Energy {
+    Energy::estimator(time_power_uj(elapsed_ns, DEFAULT_ACTIVE_MILLIWATTS))
+}
+
 /// The figure a counter rung gives one span, from how much its counter rose
 /// across it: `reading(rise)` only when the counter advanced. A counter that
 /// was live at selection can still hold across one span — a span shorter than
 /// its update interval, or a counter that has since stopped publishing — and a
 /// rise of zero is then not a reading of zero energy: the work ran, and the
 /// counter did not publish it. That span, and one whose read failed (`None`),
-/// is the time×power model's figure, `ModelBased`, as IOReport's held spans
-/// are ([`ioreport_span`]). Never `HwShunt` on a model figure.
+/// is the time×power figure at the default power, `Estimator`
+/// ([`uncalibrated_span`]), as IOReport's held spans are ([`ioreport_span`]).
+/// Never `HwShunt` on a figure no counter read.
 fn counter_span(rose: Option<u64>, elapsed_ns: u128, reading: fn(u64) -> Energy) -> Energy {
     match rose {
         Some(uj) if uj > 0 => reading(uj),
-        _ => Energy::modeled(time_power_uj(elapsed_ns, DEFAULT_ACTIVE_MILLIWATTS)),
+        _ => uncalibrated_span(elapsed_ns),
     }
 }
 
@@ -6197,7 +6260,7 @@ fn counter_span(rose: Option<u64>, elapsed_ns: u128, reading: fn(u64) -> Energy)
 /// [`Energy::measured_partial`], `HwShunt` with `Coverage::Partial`, which
 /// MUST NOT be presented as the task's total (SPEC §5.2). A counter that fell
 /// (a driver reload resets it) or held, or a read that failed, is no reading:
-/// the time×power model's whole-task figure ([`counter_span`]).
+/// the whole-task time×power estimate at the default power ([`counter_span`]).
 #[cfg_attr(not(feature = "nvml"), allow(dead_code))]
 fn nvml_span(before_uj: Option<u64>, after_uj: Option<u64>, elapsed_ns: u128) -> Energy {
     let rose = match (before_uj, after_uj) {
@@ -6216,8 +6279,9 @@ fn nvml_span(before_uj: Option<u64>, after_uj: Option<u64>, elapsed_ns: u128) ->
 /// reads as zero and the work is never under-debited by the rounding. The
 /// count changes about every 0.5 ms on a busy thread, so a shorter span can see
 /// no rise though the work ran; that span, a count that fell, and a failed read
-/// are the time×power model's figure, `ModelBased`, as IOReport's held spans
-/// are ([`ioreport_span`]). Never `HwShunt` on a model figure.
+/// are the time×power figure at the default power, `Estimator`, as IOReport's
+/// held spans are ([`ioreport_span`]). Never `HwShunt` on a figure no counter
+/// read.
 ///
 /// The reading covers the whole span only when no child process can have
 /// worked in it unseen: the reaped children's CPU time held across the span,
@@ -6297,6 +6361,60 @@ mod tests {
         assert!(short.uj() > 10_000 && short.uj() < 1_000_000, "got {}", short.uj());
     }
 
+    /// A time×power figure's grade is its power's: a power calibrated on the
+    /// host makes it a model, `ModelBased` (SPEC §5.1 rung 5); the documented
+    /// default, which no host calibrated, makes the same arithmetic an
+    /// estimate, `Estimator` (rung 6). Both scale with the work's duration and
+    /// claim no measurement; the rung, the grade it says it stamps, and the
+    /// grade its spans carry agree for each.
+    #[test]
+    fn only_a_host_calibrated_power_makes_the_time_power_figure_a_model() {
+        let calibrated = Meter::time_power(DEFAULT_ACTIVE_MILLIWATTS);
+        let default = Meter::uncalibrated_time_power(DEFAULT_ACTIVE_MILLIWATTS);
+        for (meter, rung, grade) in [
+            (&calibrated, Rung::TimePower, Provenance::ModelBased),
+            (&default, Rung::UncalibratedTimePower, Provenance::Estimator),
+        ] {
+            assert_eq!((meter.rung(), meter.provenance()), (rung, grade), "{meter:?}");
+            let (_, short) = meter.measure(|| std::thread::sleep(Duration::from_millis(2)));
+            let (_, long) = meter.measure(|| std::thread::sleep(Duration::from_millis(20)));
+            for e in [short, long] {
+                assert_eq!((e.provenance, e.measured_uj), (grade, None), "{meter:?}: {e:?}");
+                assert!(e.is_whole(), "{meter:?}: {e:?}");
+                e.check_provenance().unwrap();
+            }
+            assert!(short.uj() >= time_power_uj(2_000_000, DEFAULT_ACTIVE_MILLIWATTS), "{meter:?}: {short:?}");
+            assert!(long.uj() > short.uj(), "{meter:?}: {short:?} then {long:?}");
+        }
+    }
+
+    /// With no counter rung admitted, `detect()` falls to the time×power
+    /// figure at the documented default power, and since nothing on the
+    /// ladder calibrated that power the rung, its stamped grade and its
+    /// spans' grade are all an estimate's, never `ModelBased`.
+    #[test]
+    fn the_ladder_falls_to_the_default_power_estimate() {
+        #[cfg(target_os = "macos")]
+        let _hw = ioreport_hw_lock();
+        let (meter, why) = Meter::detect_with(&Ladder::none());
+        assert!(matches!(meter, Meter::UncalibratedTimePower { milliwatts: DEFAULT_ACTIVE_MILLIWATTS }), "{meter:?}");
+        assert_eq!((why.selected, meter.rung()), (Rung::UncalibratedTimePower, Rung::UncalibratedTimePower));
+        assert_eq!(meter.provenance(), Provenance::Estimator, "{meter:?}");
+        let (_, e) = meter.measure(|| std::thread::sleep(Duration::from_millis(2)));
+        assert_eq!((e.provenance, e.measured_uj), (Provenance::Estimator, None), "{e:?}");
+        assert!(e.uj() >= time_power_uj(2_000_000, DEFAULT_ACTIVE_MILLIWATTS), "{e:?}");
+    }
+
+    /// A span no counter read is the default-power figure for its duration,
+    /// graded `Estimator`, whole, with no measurement.
+    #[test]
+    fn a_span_no_counter_read_is_an_estimate() {
+        let e = uncalibrated_span(4_000_000);
+        assert_eq!(e, Energy::estimator(time_power_uj(4_000_000, DEFAULT_ACTIVE_MILLIWATTS)));
+        assert_eq!(e.uj(), 60_000, "4 ms at 15 W");
+        e.check_provenance().unwrap();
+    }
+
     #[test]
     fn constant_estimator_is_constant_and_says_so() {
         let meter = Meter::constant(500);
@@ -6469,7 +6587,8 @@ mod tests {
     /// SoC total did: the total rising through other rails (the machine-wide
     /// GPU rail) is not this work's energy, and a span that did not move at
     /// all, or whose read failed, measured nothing. Each is the time×power
-    /// model's figure for the span, `ModelBased`, with no measured figure.
+    /// figure for the span at the default power, `Estimator` (no host
+    /// calibrated that power), with no measured figure.
     #[test]
     fn a_span_the_ioreport_cpu_rail_held_over_is_the_models_figure() {
         let elapsed_ns = 2_000_000; // 2 ms
@@ -6484,10 +6603,10 @@ mod tests {
         ];
         for (what, before, after) in cases {
             let e = ioreport_span(before, after, elapsed_ns);
-            assert_eq!(e.provenance, Provenance::ModelBased, "{what}: {e:?}");
-            assert_eq!(e.measured_uj, None, "{what}: a model figure claimed a measurement: {e:?}");
+            assert_eq!(e.provenance, Provenance::Estimator, "{what}: {e:?}");
+            assert_eq!(e.measured_uj, None, "{what}: an estimate claimed a measurement: {e:?}");
             assert_eq!(e.uj(), model, "{what}: not the time×power figure for the span: {e:?}");
-            e.check_provenance().expect("a model figure must be internally consistent");
+            e.check_provenance().expect("an estimate must be internally consistent");
         }
     }
 
@@ -6510,7 +6629,7 @@ mod tests {
             assert_eq!(meter.provenance(), live.provenance, "the rung's grade is not the grade of its live spans");
         } else {
             assert!(ioreport::IoReport::open().is_none(), "a Live status did not build the rung, though the counter opens");
-            assert!(matches!(meter, Meter::TimePower { .. }), "{meter:?}");
+            assert!(matches!(meter, Meter::UncalibratedTimePower { .. }), "{meter:?}");
         }
     }
 
@@ -6525,7 +6644,7 @@ mod tests {
         for status in [S::Unavailable, S::CpuRailAbsent, S::CpuRailFrozen] {
             let (meter, _) = Meter::detect_with(&Ladder { ioreport: &|| status, ..Ladder::none() });
             assert!(
-                matches!(meter, Meter::TimePower { milliwatts: DEFAULT_ACTIVE_MILLIWATTS }),
+                matches!(meter, Meter::UncalibratedTimePower { milliwatts: DEFAULT_ACTIVE_MILLIWATTS }),
                 "status {status:?} gave {meter:?}"
             );
         }
@@ -7096,7 +7215,7 @@ mod tests {
             assert_eq!(matches!(meter, Meter::Rapl(_)), live, "status {status:?} gave {meter:?}");
             assert_eq!(opened.get(), usize::from(live), "status {status:?} opened the counter {} times", opened.get());
             if !live {
-                assert!(matches!(meter, Meter::TimePower { milliwatts: DEFAULT_ACTIVE_MILLIWATTS }), "{meter:?}");
+                assert!(matches!(meter, Meter::UncalibratedTimePower { milliwatts: DEFAULT_ACTIVE_MILLIWATTS }), "{meter:?}");
             }
         }
     }
@@ -7104,7 +7223,7 @@ mod tests {
     /// The RAPL rung's spans, through `measure` itself on a fake tree. A span
     /// over which a package counter rose is a reading of the rise, `HwShunt`
     /// and whole, wraparound-corrected; a span over which no counter rose is
-    /// the time×power model's figure, not a hardware reading of zero.
+    /// the default-power estimate, not a hardware reading of zero.
     #[test]
     fn a_rapl_span_is_a_reading_only_if_a_counter_rose() {
         let fake = FakePowercap::new(&["1000", "50"]);
@@ -7118,20 +7237,21 @@ mod tests {
         let (_, e) = meter.measure(|| fake.write(1, "150"));
         assert_eq!((e.provenance, e.measured_uj), (Provenance::HwShunt, Some(1_000)), "{e:?}");
         let ((), held) = meter.measure(|| std::thread::sleep(Duration::from_millis(2)));
-        assert_eq!((held.provenance, held.measured_uj), (Provenance::ModelBased, None), "{held:?}");
+        assert_eq!((held.provenance, held.measured_uj), (Provenance::Estimator, None), "{held:?}");
         assert!(held.uj() >= time_power_uj(2_000_000, DEFAULT_ACTIVE_MILLIWATTS), "{held:?}");
         held.check_provenance().unwrap();
     }
 
     /// The figure a counter rung gives a span: a reading only when the
-    /// counter rose; a rise of zero and a failed read are the model's figure.
+    /// counter rose; a rise of zero and a failed read are the default-power
+    /// estimate, `Estimator`.
     #[test]
     fn a_counter_span_is_a_reading_only_when_the_counter_rose() {
         let model = time_power_uj(3_000_000, DEFAULT_ACTIVE_MILLIWATTS);
         assert_eq!(counter_span(Some(7), 3_000_000, Energy::measured), Energy::measured(7));
         for rose in [Some(0), None] {
             let e = counter_span(rose, 3_000_000, Energy::measured);
-            assert_eq!((e.provenance, e.measured_uj, e.uj()), (Provenance::ModelBased, None, model), "{rose:?}: {e:?}");
+            assert_eq!((e.provenance, e.measured_uj, e.uj()), (Provenance::Estimator, None, model), "{rose:?}: {e:?}");
         }
     }
 
@@ -7139,7 +7259,7 @@ mod tests {
     /// of PART of the work: `HwShunt`, `Coverage::Partial`, the counter's
     /// rise as the measured figure — never a whole-task figure, since the
     /// CPU's share is unmetered. A counter that held, fell (a driver reload)
-    /// or failed to read is the time×power model's whole-task figure.
+    /// or failed to read is the whole-task default-power estimate.
     #[test]
     fn an_nvml_span_is_a_partial_reading_of_the_work() {
         let e = nvml_span(Some(48_000_000_000), Some(48_000_350_000), 10_000_000);
@@ -7152,8 +7272,8 @@ mod tests {
         let b = Some(48_000_000_000);
         for (what, before, after) in [("held", b, b), ("fell", b, Some(1_000)), ("before failed", None, b), ("after failed", b, None)] {
             let e = nvml_span(before, after, 10_000_000);
-            assert_eq!((e.provenance, e.measured_uj, e.uj()), (Provenance::ModelBased, None, model), "{what}: {e:?}");
-            assert!(e.is_whole(), "{what}: the model's figure is a whole-task estimate: {e:?}");
+            assert_eq!((e.provenance, e.measured_uj, e.uj()), (Provenance::Estimator, None, model), "{what}: {e:?}");
+            assert!(e.is_whole(), "{what}: the default-power estimate is a whole-task figure: {e:?}");
         }
     }
 
@@ -7293,7 +7413,7 @@ mod tests {
     /// A per-process span is a reading only when `ri_energy_nj` advanced:
     /// `HwShunt` and whole (no child reaped, none at the end), the rise in µJ
     /// rounded up, so a rise under 1 µJ is 1 µJ and never 0. A count that held
-    /// or fell, or a failed read, is the time×power model's figure.
+    /// or fell, or a failed read, is the default-power estimate.
     #[test]
     fn a_process_span_is_a_reading_only_when_the_count_advanced() {
         let (none, kids) = (Some(0), 4_565_861);
@@ -7308,7 +7428,7 @@ mod tests {
             [("held", b, b), ("fell", b, Some(usage(1, 0))), ("before failed", None, b), ("after failed", b, None)]
         {
             let e = process_span(before, after, none, 200_000_000);
-            assert_eq!((e.provenance, e.measured_uj, e.uj()), (Provenance::ModelBased, None, model), "{what}: {e:?}");
+            assert_eq!((e.provenance, e.measured_uj, e.uj()), (Provenance::Estimator, None, model), "{what}: {e:?}");
         }
     }
 
@@ -7325,7 +7445,7 @@ mod tests {
     ///
     /// The figure stays the count's rise either way: `Partial` changes what it
     /// claims to cover, not what it read. A span whose count held is the
-    /// model's whole-task figure whatever the children did.
+    /// whole-task default-power estimate whatever the children did.
     #[test]
     fn a_span_a_child_may_have_worked_in_is_a_partial_reading() {
         let (b, kids) = (1_000_000, 4_565_861);
@@ -7349,8 +7469,8 @@ mod tests {
         let e = span(0, Some(0));
         assert_eq!((e.provenance, e.measured_uj, e.is_whole()), (Provenance::HwShunt, Some(480_001), true), "{e:?}");
         let held = process_span(Some(usage(b, kids)), Some(usage(b, kids + 9)), Some(2), 200_000_000);
-        assert_eq!((held.provenance, held.measured_uj), (Provenance::ModelBased, None), "{held:?}");
-        assert!(held.is_whole(), "the model's figure is a whole-task estimate: {held:?}");
+        assert_eq!((held.provenance, held.measured_uj), (Provenance::Estimator, None), "{held:?}");
+        assert!(held.is_whole(), "the default-power estimate is a whole-task figure: {held:?}");
     }
 
     /// The per-process probe's rule on a scripted `ri_energy_nj`: rising
@@ -7384,7 +7504,7 @@ mod tests {
             assert_eq!(matches!(meter, Meter::ProcessEnergy(_)), live, "status {status:?} gave {meter:?}");
             assert_eq!(opened.get(), usize::from(live), "status {status:?} opened the counter {} times", opened.get());
             let expect = Detection {
-                selected: if live { Rung::ProcessEnergy } else { Rung::TimePower },
+                selected: if live { Rung::ProcessEnergy } else { Rung::UncalibratedTimePower },
                 rapl: Some(S::Unavailable),
                 nvml: Some(S::Unavailable),
                 process_energy: Some(status),
@@ -7453,8 +7573,8 @@ mod tests {
     fn the_process_energy_rung_is_never_selected_off_macos() {
         assert_eq!(process_energy_status(), CounterStatus::Unavailable);
         let (meter, why) = Meter::detect_with(&Ladder { process_energy: &|| CounterStatus::Live, ..Ladder::none() });
-        assert!(matches!(meter, Meter::TimePower { .. }), "{meter:?}");
-        assert_eq!((why.selected, why.process_energy), (Rung::TimePower, Some(CounterStatus::Live)));
+        assert!(matches!(meter, Meter::UncalibratedTimePower { .. }), "{meter:?}");
+        assert_eq!((why.selected, why.process_energy), (Rung::UncalibratedTimePower, Some(CounterStatus::Live)));
     }
 
     /// Each meter names its rung.
@@ -7463,6 +7583,7 @@ mod tests {
         #[cfg(target_os = "macos")]
         let _hw = ioreport_hw_lock();
         assert_eq!(Meter::time_power(1).rung(), Rung::TimePower);
+        assert_eq!(Meter::uncalibrated_time_power(1).rung(), Rung::UncalibratedTimePower);
         assert_eq!(Meter::constant(1).rung(), Rung::Constant);
         let fake = FakePowercap::new(&["1"]);
         assert_eq!(Meter::Rapl(Rapl::open_in(&fake.root).unwrap()).rung(), Rung::Rapl);
@@ -7790,9 +7911,9 @@ mod tests {
     /// 0.1 J ceiling of `sleeping_200_ms_meters_under_a_tenth_of_a_joule`, so
     /// no counter that reads wall time at a fixed power passes both. A counter
     /// that holds fails here before the floor: `detect()` declines it, and a
-    /// span over which it held is the model's figure, not `HwShunt`. A counter
-    /// that advances, but by a fixed step per read rather than with the work,
-    /// fails the floor.
+    /// span over which it held is the default-power estimate, not `HwShunt`. A
+    /// counter that advances, but by a fixed step per read rather than with the
+    /// work, fails the floor.
     #[cfg(target_os = "macos")]
     #[test]
     fn one_thread_burning_200_ms_is_a_whole_hardware_reading() {
@@ -8163,7 +8284,7 @@ mod tests {
     /// the reader open with a package left out: one whose `energy_uj` does
     /// not read, or a top-level zone whose `name` does not (it may be a
     /// package). A package whose range does not read opens, and a span over
-    /// which it fell is the model's figure, not an invented reading.
+    /// which it fell is the default-power estimate, not an invented reading.
     #[test]
     fn a_rapl_figure_never_leaves_a_package_out_or_takes_another_zone() {
         let psys_only = FakePowercap::with_zones(&[
@@ -8192,7 +8313,7 @@ mod tests {
         let (_, e) = meter.measure(|| no_range.write(0, "950"));
         assert_eq!((e.provenance, e.measured_uj), (Provenance::HwShunt, Some(50)), "{e:?}");
         let (_, e) = meter.measure(|| no_range.write(0, "50"));
-        assert_eq!((e.provenance, e.measured_uj), (Provenance::ModelBased, None), "a fall with no range: {e:?}");
+        assert_eq!((e.provenance, e.measured_uj), (Provenance::Estimator, None), "a fall with no range: {e:?}");
         e.check_provenance().unwrap();
     }
 }

jcp/jcp-rs/crates/jcp-schema/src/lib.rs

@@ -116,9 +116,13 @@ pub enum Provenance {
     /// that is present but frozen, or republished in lumps, never yields an
     /// `HwShunt` figure. Requires a measured figure.
     HwShunt,
-    /// A calibrated per-operation model. A measured figure may be absent.
+    /// A model calibrated on the host or against a reading (time × a power
+    /// the host measured, say), or a real reading apportioned by a model. A
+    /// measured figure may be absent.
     ModelBased,
-    /// A coarse constant estimator. A measured figure MUST be absent.
+    /// A figure nothing calibrated: a coarse constant, or a model run at a
+    /// default or assumed parameter — time × a default power is one. A
+    /// measured figure MUST be absent.
     Estimator,
 }
 

joule-code/examples/l3-jouleclaw/tests/common/mod.rs

@@ -63,3 +63,20 @@ pub fn resolve_priced_at(tag: &str, grade: Option<EnergyProvenance>) -> (Energy,
     let _ = std::fs::remove_file(&path);
     (res.receipt.energy, window)
 }
+
+/// Switch the fabric on for this process with NO calibration file (a path that
+/// does not exist, so not the machine's own either): every member keeps its
+/// seeded figure. Resolve one L3 request and return its receipt energy with the
+/// ledger window it was priced from. Call once per test process.
+#[allow(dead_code)]
+pub fn resolve_seeded() -> (Energy, Vec<LedgerEntry>) {
+    let path = std::path::Path::new(env!("CARGO_TARGET_TMPDIR")).join("l3-fabric-grade-seeded-absent.json");
+    let _ = std::fs::remove_file(&path);
+    std::env::set_var("JOULECLAW_FABRIC_CALIBRATION", &path);
+    std::env::set_var("JOULECLAW_FABRIC", "1");
+    let stage = l3_jouleclaw_binding::jouleclaw_l3_stage(Box::new(OneMatmul));
+    let res = stage
+        .try_resolve(&Request { prior: "b3:AAAA".into(), intent: "write a hello function".into() })
+        .expect("L3 resolved");
+    (res.receipt.energy, ledger_snapshot())
+}

joule-code/examples/l3-jouleclaw/tests/fabric_grade_seeded.rs

@@ -0,0 +1,21 @@
+//! The L3 stage grades a fabric-priced figure by its weakest input: with no
+//! calibration row, the member that ran is priced by its seeded figure, an
+//! assumed power over a throughput, which no host calibrated, so the receipt
+//! says Estimator, never ModelBased.
+//! Its own test process, because the fabric is discovered once per process.
+
+mod common;
+
+use joule_code_receipt::Provenance;
+use jouleclaw_fabric::EnergyProvenance;
+
+#[test]
+fn a_call_priced_by_seeded_figures_is_an_estimate() {
+    let (energy, window) = common::resolve_seeded();
+    eprintln!("window: {window:?}\nenergy: {energy:?}");
+    let neon = window.iter().find(|e| e.member_id == "local/cpu-neon").expect("the m=1 matmul ran on cpu-neon");
+    assert_eq!(neon.projected_grade, Some(EnergyProvenance::Estimated), "a seeded figure is an estimate");
+    assert!(neon.projected_uj.is_some_and(|uj| uj > 0.0), "the seeded figure priced the matmul: {neon:?}");
+    assert_eq!((energy.provenance, energy.measured_uj), (Provenance::Estimator, None), "{energy:?}");
+    assert!(energy.check_provenance().is_ok());
+}

joule-code/joule-code-rs/crates/joule-code-remediate/src/bin/joule_fix.rs

@@ -67,7 +67,7 @@ fn main() {
     }
     if let Some(f) = &report.formal {
         println!(
-            "\nformal proof: {} proved, {} refuted, {} unproved — {:.3} J ({}, ModelBased)",
+            "\nformal proof: {} proved, {} refuted, {} unproved — {:.3} J ({}, Estimator)",
             f.proved,
             f.refuted,
             f.unproved,

joule-code/joule-code-rs/crates/joule-code-remediate/src/lib.rs

@@ -433,7 +433,8 @@ pub struct FormalEntry {
     /// The counter-model witness (when refuted by a decision procedure).
     pub counter_model: Option<String>,
     /// Joules for this obligation's proof attempts, as the proof cascade
-    /// accounted them (`ModelBased`, in-process).
+    /// accounted them (`Estimator`, in-process: wall time × proof-solvers'
+    /// default power, which no host calibrated).
     pub uj: u64,
 }
 
@@ -443,7 +444,7 @@ pub struct FormalOutcome {
     pub proved: usize,
     pub refuted: usize,
     pub unproved: usize,
-    /// Total joules across all proof attempts (`ModelBased`, in-process —
+    /// Total joules across all proof attempts (`Estimator`, in-process —
     /// distinct from the cargo-attributed gate energy).
     pub proof_uj: u64,
     /// True iff at least one formalization was supplied and **every** one

jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs

@@ -13,12 +13,15 @@ pub fn detect_local() -> Vec<FabricMember> {
 
     // ── CPU SIMD — the reference oracle, always present ──
     let mut cpu_energy = BTreeMap::new();
-    // Benchmarked: NEON BF16 sustains ~38 GFLOPS/core
-    // (BENCHMARKS.md); M-series core ~5 W under load →
-    // ~130 mJ per GFLOP order of magnitude.
+    // Estimated: NEON BF16 sustains ~38 GFLOPS/core
+    // (BENCHMARKS.md, a recorded run), but the ~5 W an
+    // M-series core draws under load is assumed, not read →
+    // ~130 mJ per GFLOP order of magnitude. A figure with an
+    // assumed power in it is an estimate until a calibration
+    // row this host recorded replaces it.
     cpu_energy.insert(
         "matmul".to_string(),
-        EnergyCost { uj_per_gflop: 130_000.0, provenance: EnergyProvenance::Benchmarked, calibration: None },
+        EnergyCost { uj_per_gflop: 130_000.0, provenance: EnergyProvenance::Estimated, calibration: None },
     );
     members.push(FabricMember {
         id: "local/cpu-neon".into(),
@@ -72,12 +75,13 @@ fn probe_amx() -> Option<FabricMember> {
         return None;
     }
     let mut energy = BTreeMap::new();
-    // Benchmarked: AMX sgemm peaks ~742 GFLOPS at m=32
-    // (BENCHMARKS.md) on the same ~5 W core budget — ~7 mJ
-    // per GFLOP order of magnitude in its favoured regime.
+    // Estimated: AMX sgemm peaks ~742 GFLOPS at m=32
+    // (BENCHMARKS.md, a recorded run) on the same assumed
+    // ~5 W core budget — ~7 mJ per GFLOP order of magnitude
+    // in its favoured regime; the power is not read.
     energy.insert(
         "matmul".to_string(),
-        EnergyCost { uj_per_gflop: 7_000.0, provenance: EnergyProvenance::Benchmarked, calibration: None },
+        EnergyCost { uj_per_gflop: 7_000.0, provenance: EnergyProvenance::Estimated, calibration: None },
     );
     Some(FabricMember {
         id: "local/amx".into(),

jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/lib.rs

@@ -31,8 +31,9 @@
 //!   the runtime was told about but cannot verify.
 //! - Energy figures carry provenance: `Measured` (a meter
 //!   read it, live for the domain the figure claims),
-//!   `Benchmarked` (a recorded run on this member class),
-//!   `Estimated` (a coarse model). Placement may use any of
+//!   `Benchmarked` (a recorded run of the op's energy on this
+//!   member class), `Estimated` (a coarse model, or any figure
+//!   with an assumed power in it). Placement may use any of
 //!   them; receipts must not upgrade one into another, and
 //!   neither does loading one: a calibration row is loaded at
 //!   the grade its writer declared, with its method, and a row
@@ -127,9 +128,11 @@ pub enum EnergyProvenance {
     /// the meter was live for the domain the figure claims
     /// (JouleClaw SPEC §1.3): a hardware-graded reading.
     Measured,
-    /// Recorded benchmark on this member class.
+    /// Recorded benchmark of the op's energy on this member
+    /// class. A recorded throughput priced at an assumed power
+    /// is not one: that is `Estimated`.
     Benchmarked,
-    /// Coarse model.
+    /// Coarse model, or a figure with an assumed power in it.
     Estimated,
 }
 
@@ -359,6 +362,23 @@ mod tests {
         Fabric { members: detect_local() }
     }
 
+    /// Every seeded figure divides a power nobody read on this host (a
+    /// core's or a GPU's assumed draw) by a throughput, so it is an
+    /// estimate: `Estimated`, never `Benchmarked` or `Measured`, until a
+    /// calibration row this host recorded replaces it. A projection priced
+    /// from seeds is graded an estimate downstream for it.
+    #[test]
+    fn every_seeded_figure_is_an_estimate() {
+        let fabric = local();
+        assert!(fabric.get("local/cpu-neon").is_some(), "the CPU member is always seeded");
+        for m in &fabric.members {
+            for (op, cost) in &m.energy {
+                assert!(cost.calibration.is_none(), "{} {op}: a seeded figure carries a calibration row", m.id);
+                assert_eq!(cost.provenance, EnergyProvenance::Estimated, "{} {op}: a seeded figure", m.id);
+            }
+        }
+    }
+
     fn row(op: &str, uj_per_gflop: f64, provenance: Option<EnergyProvenance>) -> CalibrationEntry {
         CalibrationEntry {
             member_id: "local/cpu-neon".into(),

proof/README.md

@@ -36,15 +36,15 @@ proof/
 ### The reference implementation (`proof-rs/`)
 
 - **`proof-schema`** — the content-addressed goal (`blake3(statement‖0x00‖context)`), the cheapest-first tier ladder, the honest energy model (`HwShunt`/`ModelBased`/`Estimator` with the coupling enforced), `SpecGrounding`, the verdict, and the `Solver` trait every backend implements. Canonical det-CBOR content addressing.
-- **`proof-solvers`** — two **real** rungs, their energy modeled from measured wall time (`ModelBased`, a ~15 W power model — not a hardware reading): a propositional decider (T0) that parses a boolean goal and decides validity by truth-table in process, and `z3` (T1) — shell or kept **resident** across goals — that decides an SMT-LIB goal (assert the negation; `unsat` ⇒ valid). The resident `z3` is the one rung read off hardware: where the kernel counts each process's CPU energy live (macOS), each decision is read off the resident `z3`'s own process tree, and the attempt is that reading (`HwShunt`) only when the reading saw nothing missing — no gap of any kind — the decision ran entirely in the tree, and the operator has declared that the `z3` it runs decides in its own process (`Z3Server::declared_self_contained`; `proof` reads `PROOF_Z3_SELF_CONTAINED=1`) — a tree reading cannot see work handed to a container, VM or remote solver, so a forwarding `z3` would read whole. Otherwise (a gapped reading, no declaration, a refutation whose counter-model a one-shot `z3` fetches outside the tree, Linux) it keeps the model figure and records why, beside the absolute path of the `z3` binary that ran. Each goal is decided as a fresh `z3` would decide it: the answer is read off the crate's own `(check-sat)` before an unpredictable per-goal end marker, an error anywhere is undecided, and the resident session is replaced after any goal that sets an option or is not answered cleanly. Each refuses rather than fakes, so the router escalates. The model rungs (T2/T3) are honest stand-ins behind the same trait.
-- **`proof-cascade`** — the escalation router (every joule accounted, `wasted_uj` disclosed, and a goal's figure graded by the weakest of the attempts it sums), the content-addressed proof cache (the energy flywheel, durable as line-delimited JSON), batch energy accounting against a frontier-only baseline with the per-tier Amdahl breakdown, and a **real hardware energy meter** (`meter` — the `HwShunt` backend): it runs a real proof on every spare core and returns its measured microjoules from the first live source — on macOS **this process's own CPU energy counter** (`proc_pid_rusage`'s `ri_energy_nj`, public API, no privilege), read before the workers start and after they are joined, so other processes are excluded by construction and no idle baseline is subtracted; else IOReport's Energy Model, read directly through its C API on Apple Silicon and bracketed against idle; on Linux RAPL's package counters, bracketed against idle — so the headline `joules per verified proof` can be a real reading, not only a model. A vendor or kernel counter's reading is graded `HwShunt` only while the counter is live for the domain it claims ([`SPEC.md`](SPEC.md) §5), and the meter checks that before it meters anything, by one rule for every source (the counter keeps advancing in at least 5 sample intervals, at least 4 of every 5, over at least 300 ms while the probe burns CPU): the process counter itself, every IOReport CPU energy rail the figure sums (`CPU Energy`, or each die's `DIE_<n>_CPU Energy`), every RAPL package counter the figure sums (`psys` is neither summed nor probed). Each figure carries its domain: the process counter's is this process's CPU energy only — not other processes, child processes, GPU, ANE or DRAM. Returns nothing where no source is live — the caller keeps the honestly-tagged `ModelBased` figure rather than inventing one.
+- **`proof-solvers`** — two **real** rungs, their energy estimated from measured wall time (`Estimator`: wall time × a default ~15 W power that no host calibrated — not a hardware reading, and not a calibrated model): a propositional decider (T0) that parses a boolean goal and decides validity by truth-table in process, and `z3` (T1) — shell or kept **resident** across goals — that decides an SMT-LIB goal (assert the negation; `unsat` ⇒ valid). The resident `z3` is the one rung read off hardware: where the kernel counts each process's CPU energy live (macOS), each decision is read off the resident `z3`'s own process tree, and the attempt is that reading (`HwShunt`) only when the reading saw nothing missing — no gap of any kind — the decision ran entirely in the tree, and the operator has declared that the `z3` it runs decides in its own process (`Z3Server::declared_self_contained`; `proof` reads `PROOF_Z3_SELF_CONTAINED=1`) — a tree reading cannot see work handed to a container, VM or remote solver, so a forwarding `z3` would read whole. Otherwise (a gapped reading, no declaration, a refutation whose counter-model a one-shot `z3` fetches outside the tree, Linux) it keeps the wall-time estimate and records why, beside the absolute path of the `z3` binary that ran. Each goal is decided as a fresh `z3` would decide it: the answer is read off the crate's own `(check-sat)` before an unpredictable per-goal end marker, an error anywhere is undecided, and the resident session is replaced after any goal that sets an option or is not answered cleanly. Each refuses rather than fakes, so the router escalates. The model rungs (T2/T3) are honest stand-ins behind the same trait.
+- **`proof-cascade`** — the escalation router (every joule accounted, `wasted_uj` disclosed, and a goal's figure graded by the weakest of the attempts it sums), the content-addressed proof cache (the energy flywheel, durable as line-delimited JSON), batch energy accounting against a frontier-only baseline with the per-tier Amdahl breakdown, and a **real hardware energy meter** (`meter` — the `HwShunt` backend): it runs a real proof on every spare core and returns its measured microjoules from the first live source — on macOS **this process's own CPU energy counter** (`proc_pid_rusage`'s `ri_energy_nj`, public API, no privilege), read before the workers start and after they are joined, so other processes are excluded by construction and no idle baseline is subtracted; else IOReport's Energy Model, read directly through its C API on Apple Silicon and bracketed against idle; on Linux RAPL's package counters, bracketed against idle — so the headline `joules per verified proof` can be a real reading, not only a model. A vendor or kernel counter's reading is graded `HwShunt` only while the counter is live for the domain it claims ([`SPEC.md`](SPEC.md) §5), and the meter checks that before it meters anything, by one rule for every source (the counter keeps advancing in at least 5 sample intervals, at least 4 of every 5, over at least 300 ms while the probe burns CPU): the process counter itself, every IOReport CPU energy rail the figure sums (`CPU Energy`, or each die's `DIE_<n>_CPU Energy`), every RAPL package counter the figure sums (`psys` is neither summed nor probed). Each figure carries its domain: the process counter's is this process's CPU energy only — not other processes, child processes, GPU, ANE or DRAM. Returns nothing where no source is live — the caller keeps its honestly-tagged estimate rather than inventing a figure.
 - **`proof-receipt`** — the `proof/1` JCR-1 receipt: canonical det-CBOR + COSE_Sign1/EdDSA, vendored byte-compatible with the family's cross-language verifiers; refuses to seal an unproved goal.
 - **`proof-conformance`** — C1–C5 + a negative pack, all checks real, published vectors in `conformance/v1/`.
-- **`proof-cli`** — the `proof` reference demo: a proof workload reporting joules-per-proof against a frontier-only baseline — like for like, charged only for the goals the cascade proved, with the all-goals figure and its goal count beside it — the Amdahl breakdown, the cache flywheel, and a sealed + verified receipt. `proof --measure` adds a **real hardware reading** of a non-trivial T0 proof (`HwShunt`) where the meter produces one, and prints which source metered it, its domain, and why each other source was not used; that needs a counter the meter has seen to be live. On the Macs measured so far (macOS 27.0.1, an M5 Max and an M3 Ultra) IOReport's CPU energy rail is frozen for an unprivileged reader, but this process's CPU energy counter is live, so `--measure` meters with it; the receipt still seals the cascade's own `ModelBased` figure for the first goal. On Linux, RAPL's `energy_uj` is root-only on current kernels.
+- **`proof-cli`** — the `proof` reference demo: a proof workload reporting joules-per-proof against a frontier-only baseline — like for like, charged only for the goals the cascade proved, with the all-goals figure and its goal count beside it — the Amdahl breakdown, the cache flywheel, and a sealed + verified receipt. `proof --measure` adds a **real hardware reading** of a non-trivial T0 proof (`HwShunt`) where the meter produces one, and prints which source metered it, its domain, and why each other source was not used; that needs a counter the meter has seen to be live. On the Macs measured so far (macOS 27.0.1, an M5 Max and an M3 Ultra) IOReport's CPU energy rail is frozen for an unprivileged reader, but this process's CPU energy counter is live, so `--measure` meters with it; the receipt still seals the cascade's own `Estimator` figure for the first goal. On Linux, RAPL's `energy_uj` is root-only on current kernels.
 
 `cargo test --workspace` green; `cargo clippy --workspace --all-targets` is
 warning-free for Linux, and on macOS reports two lints in proof-cascade's
-IOReport FFI. The two bottom rungs decide for real, with energy modeled from
+IOReport FFI. The two bottom rungs decide for real, with energy estimated from
 wall time (the resident `z3`'s decisions read off its own process tree where
 that reading is whole and the `z3` declared self-contained); the model rungs are honestly marked as stand-ins until
 inference backends are wired.

proof/SPEC.md

@@ -90,9 +90,12 @@ Every reading is integer microjoules with a provenance tag:
   SMC, or a vendor energy counter (RAPL, NVML, Apple IOReport, ...). REQUIRES a
   present measured figure. A vendor counter's reading is a hardware reading,
   subject to the liveness requirement below.
-- `ModelBased` — computed from a calibrated per-operation model (e.g. measured
-  wall time × a power model). A measured figure MAY be absent.
-- `Estimator` — a coarse constant. A measured figure MUST be absent.
+- `ModelBased` — computed from a model calibrated on the host or against a
+  reading (e.g. measured wall time × a power the host measured). A measured
+  figure MAY be absent.
+- `Estimator` — a figure nothing calibrated: a coarse constant, or a model run
+  at a default or assumed parameter (e.g. measured wall time × a default power
+  no host calibrated). A measured figure MUST be absent.
 
 A conforming implementation MUST enforce this coupling: `HwShunt` without a
 measured figure, or `Estimator` with one, is invalid.

proof/proof-rs/crates/proof-cascade/src/lib.rs

@@ -39,9 +39,10 @@ pub struct CascadeResult {
     /// before it, because a sum is only as good as its weakest part. It is the
     /// closing solver's own whenever every earlier attempt was graded at least
     /// as well, which holds on any ladder whose rungs share one grade. A rung
-    /// that reads hardware (`HwShunt`) above one that models its figure
-    /// therefore seals as `ModelBased` while the modelled waste is in the
-    /// total, never as a hardware reading of it. `Estimator` when unproved,
+    /// that reads hardware (`HwShunt`) above one that models or estimates its
+    /// figure therefore seals as the cheaper rung's grade (`ModelBased` or
+    /// `Estimator`) while that waste is in the total, never as a hardware
+    /// reading of it. `Estimator` when unproved,
     /// and for a proof served from cache: a hit's `total_uj` of 0 is the
     /// lookup's nominal cost, nothing read and nothing modelled, so it never
     /// carries the grade of the solver whose proof it serves — a hardware

proof/proof-rs/crates/proof-cascade/src/meter.rs

@@ -16,8 +16,8 @@
 //!    no `macmon`, no sudo): SoC power bracketed busy against idle.
 //! 3. **RAPL** `energy_uj` (Linux): package power bracketed busy against idle.
 //!
-//! Returns `None` where no source is live — the caller keeps the
-//! honestly-tagged `ModelBased` reading rather than inventing a number. No
+//! Returns `None` where no source is live — the caller keeps its
+//! honestly-tagged estimate rather than inventing a number. No
 //! elevated privileges and no external binaries.
 //!
 //! **A figure from this meter is a hardware reading, `HwShunt`, from every
@@ -166,7 +166,7 @@ impl Measurement {
 /// - `None` if no source is live ([`meter_source`] is `None`: a counter that
 ///   is not live yields `None` before any window runs, and `work` never runs),
 ///   if the selected source gave no reading, or if `work` never completed a
-///   call. The caller keeps its own `ModelBased` figure.
+///   call. The caller keeps its own estimate.
 /// - From the process counter, `Some` is the counter's advance across the
 ///   calls ÷ the calls; `Some(0)` means under half a microjoule a call, below
 ///   this API's resolution — not a zero-energy call.
@@ -335,7 +335,7 @@ pub enum IoReportStatus {
 /// quiet host is called live after about ten. If fewer than five intervals
 /// were observed when it runs out, the probe keeps sampling, up to five
 /// budgets. A live rail slower than that fails safe: declined, and the caller
-/// keeps its `ModelBased` figure. Paid once per process; see
+/// keeps its own estimate. Paid once per process; see
 /// [`ioreport_status`].
 #[cfg(target_os = "macos")]
 pub const CPU_RAIL_LIVENESS_BUDGET: std::time::Duration = std::time::Duration::from_millis(1000);
@@ -5398,7 +5398,7 @@ mod tests {
     /// figure at all: on a host whose interface is declined, real CPU work (a
     /// direct call burns 80 ms) put through `measure_marginal_uj` gives `None`
     /// — not `Some(0)`, not a floored figure — before any bracket runs, so the
-    /// work is never called and the caller keeps its own `ModelBased` figure.
+    /// work is never called and the caller keeps its own estimate.
     /// Where an interface is usable, the bracket really runs the work. How
     /// long the call took is logged, not asserted: a loaded host can stall
     /// any thread, and the work-call count is the pin.

proof/proof-rs/crates/proof-cli/src/main.rs

@@ -2,8 +2,9 @@
 //!
 //! Runs a proof workload through the cheapest-sufficient ladder — the T0
 //! propositional decider and T1 resident `z3`, both real deciders. T0's
-//! energy is modeled, not measured: each attempt's wall time × proof-solvers'
-//! ~15 W power model, tagged `ModelBased`. T1's is the same model, except
+//! energy is estimated, not measured: each attempt's wall time ×
+//! proof-solvers' default ~15 W power, which no host calibrated, so tagged
+//! `Estimator`. T1's is the same estimate, except
 //! where this host reads the resident `z3`'s own process tree (macOS, with
 //! the kernel's per-process energy counter live), the decision's reading
 //! saw nothing missing, and the operator has declared that the `z3` on
@@ -11,7 +12,7 @@
 //! no container, VM or remote solver behind it, which no reading of the
 //! tree could show): then that attempt is the reading, `HwShunt`. A goal's
 //! figure sums every attempt on it, so an SMT goal, which T0 tries first and
-//! fails, is still `ModelBased`: its total holds T0's modelled attempt.
+//! fails, is still `Estimator`: its total holds T0's estimated attempt.
 //! There is no T2/T3 rung, so goals that need
 //! one come back unproved. It reports, per goal, the tier that closed it and
 //! the joules it cost; then the headline — joules spent versus a frontier-only
@@ -63,7 +64,7 @@ fn main() {
         match (z3_available(), z3_self_contained) {
             (false, _) => "ABSENT — T1 goals escalate",
             (true, true) => "present, declared self-contained",
-            (true, false) => "present, not declared self-contained: T1 stays modelled (PROOF_Z3_SELF_CONTAINED=1 declares it)",
+            (true, false) => "present, not declared self-contained: T1 stays estimated (PROOF_Z3_SELF_CONTAINED=1 declares it)",
         }
     );
     let mut first = None;
@@ -135,7 +136,7 @@ fn main() {
         summary.uj_by_tier[0], summary.uj_by_tier[1], summary.uj_by_tier[2], summary.uj_by_tier[3], t3,
     );
 
-    // --measure: try to put a hardware reading beside the wall-time model:
+    // --measure: try to put a hardware reading beside the wall-time estimate:
     // meter a real T0 proof with the first live source (`meter_source`) — on
     // macOS this process's CPU energy counter, else IOReport's Energy Model
     // (used only while its CPU energy rail is live); on Linux RAPL (used only
@@ -144,7 +145,7 @@ fn main() {
     // energy counter's reading is a hardware reading while the counter is live
     // for the domain it claims (SPEC §5), which the meter checks before it
     // meters anything; the figure's domain is printed beside it. Where no
-    // source is live, print why: the figures above then stay ModelBased.
+    // source is live, print why: the figures above then stay Estimator.
     if measure {
         use proof_cascade::meter::{
             ioreport_status, measure_marginal, meter_source, process_energy_status, rapl_status, MeterSource,
@@ -163,7 +164,7 @@ fn main() {
         );
         if !available {
             println!(
-                "  --measure: no hardware energy reading on this host: {}.\n             The figures above stay ModelBased — honestly tagged.",
+                "  --measure: no hardware energy reading on this host: {}.\n             The figures above stay Estimator — honestly tagged.",
                 no_hardware_reading_reason()
             );
         } else {
@@ -213,7 +214,7 @@ fn main() {
                     );
                     println!("  domain: {}", m.source.domain());
                     println!(
-                        "  this proof's joules are a hardware reading; the per-goal figures above stay ModelBased, and the receipt seals them."
+                        "  this proof's joules are a hardware reading; the per-goal figures above stay Estimator, and the receipt seals them."
                     );
                 }
                 // The process counter advanced by under half a microjoule a call.
@@ -226,7 +227,7 @@ fn main() {
                 ),
                 // No reading at all: say why rather than blaming the machine.
                 None => println!(
-                    "  measured: no hardware reading: {}. The figures above stay ModelBased.",
+                    "  measured: no hardware reading: {}. The figures above stay Estimator.",
                     no_hardware_reading_reason()
                 ),
             }

proof/proof-rs/crates/proof-cli/tests/measure.rs

@@ -1,6 +1,6 @@
 //! `proof --measure`, end to end: when every hardware source declines, the
 //! output names the reasons, nothing in it claims a hardware reading, and the
-//! cascade's own ModelBased figures stand; when a source meters, the output
+//! cascade's own Estimator figures stand; when a source meters, the output
 //! names the source, its HwShunt figure and its domain, and the sealed receipt
 //! is unchanged. Every check is against the decision the `proof` process
 //! printed, never a second probe in this process: two independent ~1 s probes
@@ -147,8 +147,8 @@ fn measure_names_its_source_or_why_it_declined_and_leaves_the_receipt_alone() {
     }
 
     // The sealed receipt is the cascade's own figure for the FIRST goal, on
-    // every branch: the first row's figure, ModelBased, never the --measure
-    // figure.
+    // every branch: the first row's figure, Estimator (wall time × a default
+    // power no host calibrated), never the --measure figure.
     let first_row_uj: u64 = stdout
         .lines()
         .find(|l| l.trim_start().starts_with("T0:automation"))
@@ -167,7 +167,7 @@ fn measure_names_its_source_or_why_it_declined_and_leaves_the_receipt_alone() {
         .unwrap_or_else(|| panic!("no uj figure in the receipt line: {receipt}"));
     assert!(receipt_uj > 0, "the receipt carries a zero figure for a proof that ran: {receipt}");
     assert_eq!(receipt_uj, first_row_uj, "the receipt is not the first goal's own figure: {receipt}\n{stdout}");
-    assert!(receipt.contains("provenance ModelBased"), "the receipt's provenance changed: {receipt}");
+    assert!(receipt.contains("provenance Estimator"), "the receipt's provenance changed: {receipt}");
     assert!(receipt.contains("closed at T0:automation"), "the receipt is not the first goal's: {receipt}");
 
     assert_eq!(declined, !available, "the CLI's output disagrees with the decision it printed:\n{stdout}");
@@ -240,8 +240,8 @@ fn measure_names_its_source_or_why_it_declined_and_leaves_the_receipt_alone() {
         assert!(!stdout.contains("idle noise"), "the meter declined, yet the output blames a noisy machine:\n{stdout}");
         assert!(!stdout.contains("--measure: metering a real"), "the meter declined, yet the CLI metered:\n{stdout}");
         assert!(
-            stdout.contains("The figures above stay ModelBased"),
-            "a declined meter must leave the ModelBased figures standing:\n{stdout}"
+            stdout.contains("The figures above stay Estimator"),
+            "a declined meter must leave the Estimator figures standing:\n{stdout}"
         );
     } else {
         assert!(

proof/proof-rs/crates/proof-schema/src/lib.rs

@@ -118,10 +118,12 @@ pub enum Provenance {
     /// NOT produce a hardware-graded figure; the implementation falls back to
     /// its estimator or reports the work unmetered, and SHOULD record why.
     HwShunt,
-    /// Computed from a calibrated per-operation model (e.g. wall time × a power
-    /// model). `measured_uj` may be absent.
+    /// Computed from a model calibrated on the host or against a reading (e.g.
+    /// wall time × a power the host measured). `measured_uj` may be absent.
     ModelBased,
-    /// A coarse constant estimator. `measured_uj` MUST be absent.
+    /// A figure nothing calibrated: a coarse constant, or a model run at a
+    /// default or assumed parameter (e.g. wall time × a default power).
+    /// `measured_uj` MUST be absent.
     Estimator,
 }
 
@@ -147,8 +149,9 @@ pub struct Energy {
 }
 
 impl Energy {
-    /// A model-based reading (e.g. measured wall time × a power model). No
-    /// hardware shunt, so `measured_uj` stays absent.
+    /// A model-based reading (e.g. measured wall time × a power the host
+    /// calibrated). No hardware shunt, so `measured_uj` stays absent. A model
+    /// at a power nothing calibrated is an estimate: [`Energy::estimator`].
     pub fn modeled(uj: u64) -> Self {
         Energy {
             measured_uj: None,
@@ -156,6 +159,15 @@ impl Energy {
             provenance: Provenance::ModelBased,
         }
     }
+    /// An estimate of `uj`: a figure nothing calibrated (e.g. measured wall
+    /// time × a default power). `measured_uj` stays absent.
+    pub fn estimator(uj: u64) -> Self {
+        Energy {
+            measured_uj: None,
+            estimated_uj: uj,
+            provenance: Provenance::Estimator,
+        }
+    }
     /// The estimator of last resort: a coarse per-tier constant.
     pub fn estimate_tier(tier: Tier) -> Self {
         Energy {

proof/proof-rs/crates/proof-solvers/src/lib.rs

@@ -1,7 +1,8 @@
 //! Solvers for the proof tier ladder (SPEC §4).
 //!
-//! The two bottom rungs are **real** and report energy with `ModelBased`
-//! provenance (measured wall time × a power model), but for one case:
+//! The two bottom rungs are **real** and report energy with `Estimator`
+//! provenance (measured wall time × a default power no host calibrated,
+//! [`DEFAULT_ACTIVE_MILLIWATTS`]), but for one case:
 //!
 //! - [`Propositional`] (T0) → parses a boolean goal and decides validity by
 //!   truth-table, in process.
@@ -10,7 +11,7 @@
 //!   and where this host's kernel counts each process's CPU energy live
 //!   (macOS), reads each decision off the resident `z3`'s own process tree:
 //!   `HwShunt` when the reading saw nothing missing and the operator has
-//!   declared that `z3` decides in its own tree, the model otherwise (see
+//!   declared that `z3` decides in its own tree, the estimate otherwise (see
 //!   [`Z3Server`] for exactly when).
 //! - [`LeanVerifier`] → runs Lean and reports what the kernel accepted.
 //!
@@ -41,13 +42,24 @@ use std::time::{Duration, Instant};
 use proof_schema::{Attempt, ContentId, Energy, GoalKind, ProofGoal, Solver, Tier, Verdict};
 use sandbox_meter::{TreeError, TreeGap, TreeMeter, TreeReading};
 
-/// Convert elapsed nanoseconds to microjoules under a documented single-core
-/// power model (~15 W active). The reading is `ModelBased`: a hardware interface
-/// (RAPL/NVML) would make it `HwShunt`; from wall time alone it is honestly
-/// modeled.
+/// The active power the wall-time figure assumes, in milliwatts: an
+/// order-of-magnitude draw for one busy core (~15 W), documented, not
+/// measured on any host.
+pub const DEFAULT_ACTIVE_MILLIWATTS: u64 = 15_000;
+
+/// Convert elapsed nanoseconds to microjoules at [`DEFAULT_ACTIVE_MILLIWATTS`].
 fn ns_to_uj(ns: u128) -> u64 {
-    // 15 W = 15 µJ/µs = 0.015 µJ/ns  →  µJ = ns × 15 / 1000.
-    (ns.saturating_mul(15) / 1000) as u64
+    // mW × ns = 10⁻¹² J = 10⁻⁶ µJ; at 15 W, µJ = ns × 15 / 1000.
+    (ns.saturating_mul(DEFAULT_ACTIVE_MILLIWATTS as u128) / 1_000_000) as u64
+}
+
+/// The figure for `ns` of solver wall time: [`ns_to_uj`], at least 1 µJ,
+/// graded `Estimator`. The power is assumed, not calibrated on this host, so
+/// wall time × it is an estimate (the JCP metering ladder's rung 6), never
+/// `ModelBased`, which a model earns by its calibration; a hardware interface
+/// read live over the work would make it `HwShunt`.
+fn wall_time_estimate(ns: u128) -> Energy {
+    Energy::estimator(ns_to_uj(ns).max(1))
 }
 
 fn proved(goal: &ProofGoal) -> Verdict {
@@ -166,11 +178,10 @@ impl Solver for Propositional {
             },
             _ => Verdict::Unproved,
         };
-        let uj = ns_to_uj(start.elapsed().as_nanos()).max(1);
         Attempt {
             tier: Tier::Automation,
             verdict,
-            energy: Energy::modeled(uj),
+            energy: wall_time_estimate(start.elapsed().as_nanos()),
         }
     }
 }
@@ -402,11 +413,10 @@ impl Solver for Z3Smt {
             Some(CheckSat::Sat) => refutation_or_undecided(&goal.statement),
             _ => Verdict::Unproved,
         };
-        let uj = ns_to_uj(start.elapsed().as_nanos()).max(1);
         Attempt {
             tier: Tier::Smt,
             verdict,
-            energy: Energy::modeled(uj),
+            energy: wall_time_estimate(start.elapsed().as_nanos()),
         }
     }
 }
@@ -692,15 +702,16 @@ fn admit(statement: &str) -> Option<Admitted> {
 ///    first on `PATH` with symlinks resolved — decides each goal in its own
 ///    process tree ([`Z3Server::declared_self_contained`]; proof-cli reads
 ///    `PROOF_Z3_SELF_CONTAINED=1`). Undeclared, the default, a whole reading
-///    keeps the model figure ([`Modelled::NotDeclaredSelfContained`]).
+///    keeps the wall-time estimate ([`Modelled::NotDeclaredSelfContained`]).
 ///    Condition 1 still applies to every reading, so a declared `z3` that
 ///    forked or used the GPU is graded down by its gaps.
 ///
-/// Otherwise the attempt keeps the model figure it always had — the
-/// solver's wall time × the crate's ~15 W model, [`Energy::modeled`] — and
-/// never seals the reading: [`Energy`] has no coverage field, so a reading of
-/// part of the decision sealed as `HwShunt` would claim the whole. The
-/// model is the figure when:
+/// Otherwise the attempt keeps the figure it always had — the solver's wall
+/// time × the crate's default power ([`DEFAULT_ACTIVE_MILLIWATTS`], ~15 W,
+/// which no host calibrated), an estimate, [`Energy::estimator`] — and never
+/// seals the reading: [`Energy`] has no coverage field, so a reading of part
+/// of the decision sealed as `HwShunt` would claim the whole. The estimate is
+/// the figure when:
 ///
 /// - the reading has a gap ([`Modelled::Gaps`]: it is short of the tree's
 ///   energy, or with a member still running at the start may hold a little
@@ -717,8 +728,9 @@ fn admit(statement: &str) -> Option<Admitted> {
 ///   counter-model is fetched by a ONE-SHOT `z3`, a child of this process,
 ///   not of the resident one, so it is outside the tree. Its span is never
 ///   opened over it — the tree span covers the resident decision alone — and
-///   its work is in the attempt's figure only through the model, which then
-///   covers the whole attempt: the resident decision and the one-shot run.
+///   its work is in the attempt's figure only through the estimate, which
+///   then covers the whole attempt: the resident decision and the one-shot
+///   run.
 ///
 /// Why each attempt was graded as it was is kept beside it, not on the wire:
 /// [`Z3Server::last_account`].
@@ -727,15 +739,15 @@ fn admit(statement: &str) -> Option<Admitted> {
 /// The tree is walked until it is quiet: `z3` blocks on its next read as
 /// soon as it has written the end marker, so on a quiet host that is a few
 /// walks of one process (tens of µs each), and on a loaded one up to the
-/// settle bound, after which a reading still unsettled is a gap (the model
-/// figure). And the GPU clients are read from the I/O Registry — before the
+/// settle bound, after which a reading still unsettled is a gap (the
+/// estimate). And the GPU clients are read from the I/O Registry — before the
 /// start walk and after the stop walk, outside the settle bound — which
 /// takes about a millisecond on the hosts measured and has been seen at
 /// tens of milliseconds under heavy load. Together, on a loaded development
 /// host at the production bound, that has come to a few milliseconds for a
 /// typical goal, several at the 90th percentile and tens at worst; the test
 /// `the_production_settle_bound_grades_every_attempt_consistently` logs the
-/// figures on the host it runs on. The model figure times the solver's work
+/// figures on the host it runs on. The estimate times the solver's work
 /// alone — the resident decision and, when it runs, the one-shot `z3` —
 /// never the meter's walks or reads, nor a retired session's replacement
 /// starting after the span.
@@ -777,8 +789,9 @@ impl Resident {
     }
 }
 
-/// Why a [`Z3Server`] attempt's figure is the model rather than a reading of
-/// the resident `z3`'s tree. An attempt can have several.
+/// Why a [`Z3Server`] attempt's figure is the wall-time estimate (`Estimator`)
+/// rather than a reading of the resident `z3`'s tree. An attempt can have
+/// several.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum Modelled {
     /// The goal never reached the resident `z3`: the shape guard refused it,
@@ -807,8 +820,8 @@ pub enum Modelled {
 }
 
 /// How one [`Z3Server`] attempt's energy was obtained: the figure the attempt
-/// reported, the reading it was graded from, and why the model was kept where
-/// it was. The gateway's plaintext account, in-process: the attempt's figure
+/// reported, the reading it was graded from, and why the estimate was kept
+/// where it was. The gateway's plaintext account, in-process: the attempt's figure
 /// and its provenance are what travels; this says why.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct Z3EnergyAccount {
@@ -818,11 +831,12 @@ pub struct Z3EnergyAccount {
     /// opened: `None` when the goal never reached `z3` or there is no meter.
     pub reading: Option<Result<TreeReading, TreeError>>,
     /// Empty when the figure is the reading; otherwise every reason the
-    /// model figure was kept.
+    /// estimate was kept.
     pub modelled_because: Vec<Modelled>,
-    /// The model figure, µJ: the solver's wall time (the resident decision,
-    /// and the one-shot `z3` when it ran) × the crate's ~15 W model, at least
-    /// 1. The attempt's figure whenever `modelled_because` is not empty.
+    /// The estimate, µJ: the solver's wall time (the resident decision, and
+    /// the one-shot `z3` when it ran) × the crate's default power
+    /// ([`DEFAULT_ACTIVE_MILLIWATTS`]), at least 1. The attempt's figure,
+    /// graded `Estimator`, whenever `modelled_because` is not empty.
     pub modelled_uj: u64,
     /// The solver's own wall time: what `modelled_uj` is computed from.
     pub work: Duration,
@@ -841,11 +855,11 @@ pub struct Z3EnergyAccount {
 /// over the decision, `None` when no span was opened; `ran`: the goal reached
 /// the resident `z3`; `self_contained`: the operator's declaration;
 /// `one_shot`: a one-shot `z3` fetched a counter-model outside the tree;
-/// `modelled_uj`: the model figure.
+/// `modelled_uj`: the wall-time estimate.
 ///
 /// `HwShunt` only for a reading with no gap at all, of a decision that ran
 /// entirely in the tree, of a `z3` declared self-contained; otherwise the
-/// model, with every reason. Pure, so its tests drive every case without a
+/// wall-time estimate, `Estimator`, with every reason. Pure, so its tests drive every case without a
 /// process.
 fn grade_attempt(
     reading: Option<&Result<TreeReading, TreeError>>,
@@ -876,7 +890,7 @@ fn grade_attempt(
     }
     match reading {
         Some(Ok(r)) if because.is_empty() => (Energy::measured(r.cpu_nj.div_ceil(1_000)), because),
-        _ => (Energy::modeled(modelled_uj.max(1)), because),
+        _ => (Energy::estimator(modelled_uj.max(1)), because),
     }
 }
 
@@ -896,9 +910,9 @@ impl Z3Server {
     /// The same server, its tree meter waiting up to `bound` at each end of
     /// a decision for the resident `z3` to go quiet (default
     /// [`sandbox_meter::probe::SETTLE_BOUND`]). A `z3` still running when it
-    /// runs out is a gap, so that decision keeps the model figure; a longer
-    /// bound trades latency on a loaded host for fewer of those. It holds for
-    /// every session the server starts.
+    /// runs out is a gap, so that decision keeps the wall-time estimate; a
+    /// longer bound trades latency on a loaded host for fewer of those. It
+    /// holds for every session the server starts.
     pub fn with_settle_bound(mut self, bound: Duration) -> Self {
         self.settle_bound = Some(bound);
         if let Ok(Some(r)) = self.resident.get_mut() {
@@ -913,7 +927,7 @@ impl Z3Server {
     /// VM, service or remote solver. A whole reading of a decision is sealed
     /// `HwShunt` only with it. Only the operator can make it: this crate
     /// names `z3` by `PATH`, and whatever answers to that name is what runs.
-    /// Undeclared (the default), every decision keeps the model figure
+    /// Undeclared (the default), every decision keeps the wall-time estimate
     /// ([`Modelled::NotDeclaredSelfContained`]). proof-cli reads it from
     /// `PROOF_Z3_SELF_CONTAINED=1`.
     pub fn declared_self_contained(mut self, declared: bool) -> Self {
@@ -1044,7 +1058,7 @@ impl Solver for Z3Server {
 ///
 /// The goal→Lean encoding is the caller's (`context` carries the dialect, e.g.
 /// `"lean4"`); the backend only attempts goals whose context names Lean. Energy
-/// is `ModelBased` (wall time × the crate's power model), like the z3 rung.
+/// is `Estimator` (wall time × the crate's default power), like the z3 rung.
 pub struct LeanVerifier {
     tier: Tier,
     lean_bin: String,
@@ -1148,7 +1162,7 @@ impl Solver for LeanVerifier {
         Attempt {
             tier: self.tier,
             verdict,
-            energy: Energy::modeled(ns_to_uj(started.elapsed().as_nanos())),
+            energy: Energy::estimator(ns_to_uj(started.elapsed().as_nanos())),
         }
     }
 }
@@ -1400,7 +1414,7 @@ mod tests {
         let taut = ProofGoal::new("a | ~a", "prop", GoalKind::Trivial);
         let a = Propositional.attempt(&taut);
         assert!(a.verdict.is_proved());
-        assert!(a.energy.measured_uj.is_none()); // ModelBased: no hardware shunt
+        assert!(a.energy.measured_uj.is_none()); // Estimator: no hardware shunt
         assert!(a.energy.uj() >= 1);
         assert!(!Propositional
             .attempt(&ProofGoal::new("a -> b", "prop", GoalKind::Trivial))
@@ -1413,6 +1427,33 @@ mod tests {
         assert_eq!(reference_ladder_with_real_t0().len(), 4);
     }
 
+    /// Every rung that prices its attempt by wall time × the crate's default
+    /// power grades the figure `Estimator`, never `ModelBased`: no host
+    /// calibrated that power, so the figure is a constant scaled by time, an
+    /// estimate. Holds whether or not the work decided anything, and whether
+    /// or not the tool was there to run.
+    #[test]
+    fn a_wall_time_figure_at_the_default_power_is_an_estimate() {
+        let e = wall_time_estimate(4_000_000);
+        assert_eq!(e, Energy::estimator(60_000), "4 ms at the default 15 W is 60,000 µJ, an estimate");
+        assert_eq!(wall_time_estimate(0), Energy::estimator(1), "a figure for work that ran is at least 1 µJ");
+        assert_eq!(ns_to_uj(1_000_000_000), DEFAULT_ACTIVE_MILLIWATTS * 1_000, "1 s at the default power, in µJ");
+
+        let smt = ProofGoal::new("(declare-const x Int)\n(assert (not (> x 0)))", "smt2", GoalKind::Decidable);
+        let lean = ProofGoal::new("example : 1 + 1 = 2 := by decide", "lean4", GoalKind::Arithmetic);
+        let absent_lean = LeanVerifier::new().with_bin("/nonexistent/proof-solvers-test/lean");
+        for (name, a) in [
+            ("T0 proved", Propositional.attempt(&ProofGoal::new("a | ~a", "prop", GoalKind::Trivial))),
+            ("T0 refused", Propositional.attempt(&ProofGoal::new("a -> b", "prop", GoalKind::Trivial))),
+            ("one-shot z3", Z3Smt.attempt(&smt)),
+            ("lean absent", absent_lean.attempt(&lean)),
+        ] {
+            assert_eq!(a.energy.provenance, proof_schema::Provenance::Estimator, "{name}: {:?}", a.energy);
+            assert_eq!(a.energy.measured_uj, None, "{name}: {:?}", a.energy);
+            a.energy.check_provenance().unwrap();
+        }
+    }
+
     #[test]
     fn z3_decides_real_smt_goals_when_available() {
         let valid = ProofGoal::new(
@@ -1749,14 +1790,14 @@ mod tests {
         }
     }
 
-    /// Every gap the meter can report grades the attempt down to the model,
+    /// Every gap the meter can report grades the attempt down to the estimate,
     /// and the reading is never sealed: Energy has no coverage field, so a
     /// partial reading as `HwShunt` would claim the whole decision. This
     /// includes the gap that can put energy from BEFORE the span into the
     /// figure (`Unsettled` at the start), and the GPU and Neural Engine gaps
     /// a CPU reading cannot cover.
     #[test]
-    fn a_reading_with_any_gap_keeps_the_model_figure() {
+    fn a_reading_with_any_gap_keeps_the_estimate() {
         use sandbox_meter::SpanEnd;
         let gaps = [
             TreeGap::Unreadable { pid: 7, errno: 1, end: SpanEnd::Stop },
@@ -1777,37 +1818,37 @@ mod tests {
         for gap in gaps {
             let r: Result<TreeReading, TreeError> = Ok(reading(5_000_000, vec![gap.clone()]));
             let (e, because) = grade_attempt(Some(&r), true, true, false, 77);
-            assert_eq!(e, Energy::modeled(77), "{gap:?} was sealed as the reading");
+            assert_eq!(e, Energy::estimator(77), "{gap:?} was sealed as the reading");
             assert_eq!(because, vec![Modelled::Gaps(vec![gap])]);
         }
     }
 
-    /// No reading, no meter, nothing run: the model figure, each with its
+    /// No reading, no meter, nothing run: the estimate, each with its
     /// reason. And a refuted goal, whose counter-model a one-shot `z3`
-    /// fetched outside the resident tree, keeps the model for the whole
+    /// fetched outside the resident tree, keeps the estimate for the whole
     /// attempt even when the resident decision's reading was whole: the
     /// one-shot run is in no span, and a reading of the decision alone
     /// sealed as `HwShunt` would claim the attempt.
     #[test]
-    fn an_attempt_with_no_whole_reading_of_all_its_work_keeps_the_model() {
+    fn an_attempt_with_no_whole_reading_of_all_its_work_keeps_the_estimate() {
         let gone: Result<TreeReading, TreeError> = Err(TreeError::RootGone { pid: 4242 });
         let (e, because) = grade_attempt(Some(&gone), true, true, false, 12);
-        assert_eq!((e, because), (Energy::modeled(12), vec![Modelled::NoReading(TreeError::RootGone { pid: 4242 })]));
+        assert_eq!((e, because), (Energy::estimator(12), vec![Modelled::NoReading(TreeError::RootGone { pid: 4242 })]));
 
         let (e, because) = grade_attempt(None, true, true, false, 12);
-        assert_eq!((e, because), (Energy::modeled(12), vec![Modelled::NoTreeMeter]));
+        assert_eq!((e, because), (Energy::estimator(12), vec![Modelled::NoTreeMeter]));
 
         let (e, because) = grade_attempt(None, false, true, false, 0);
-        assert_eq!((e, because), (Energy::modeled(1), vec![Modelled::NotRun]), "the model figure is at least 1 µJ");
+        assert_eq!((e, because), (Energy::estimator(1), vec![Modelled::NotRun]), "the estimate is at least 1 µJ");
 
         let whole: Result<TreeReading, TreeError> = Ok(reading(3_000_000, Vec::new()));
         let (e, because) = grade_attempt(Some(&whole), true, true, true, 900);
-        assert_eq!((e, because), (Energy::modeled(900), vec![Modelled::CounterModelOutsideTree]));
+        assert_eq!((e, because), (Energy::estimator(900), vec![Modelled::CounterModelOutsideTree]));
 
         // Both reasons, when both hold.
         let gapped: Result<TreeReading, TreeError> = Ok(reading(3_000_000, vec![TreeGap::Gone { pid: 9 }]));
         let (e, because) = grade_attempt(Some(&gapped), true, true, true, 900);
-        assert_eq!(e, Energy::modeled(900));
+        assert_eq!(e, Energy::estimator(900));
         assert_eq!(because, vec![Modelled::Gaps(vec![TreeGap::Gone { pid: 9 }]), Modelled::CounterModelOutsideTree]);
     }
 
@@ -1816,14 +1857,14 @@ mod tests {
     /// reason rides beside any other; with no reading there is nothing the
     /// declaration would change, and it is not given as a reason.
     #[test]
-    fn an_undeclared_z3_keeps_the_model_for_any_reading() {
+    fn an_undeclared_z3_keeps_the_estimate_for_any_reading() {
         let whole: Result<TreeReading, TreeError> = Ok(reading(5_000_000, Vec::new()));
         let (e, because) = grade_attempt(Some(&whole), true, false, false, 77);
-        assert_eq!((e, because), (Energy::modeled(77), vec![Modelled::NotDeclaredSelfContained]));
+        assert_eq!((e, because), (Energy::estimator(77), vec![Modelled::NotDeclaredSelfContained]));
 
         let gapped: Result<TreeReading, TreeError> = Ok(reading(5_000_000, vec![TreeGap::Gone { pid: 9 }]));
         let (e, because) = grade_attempt(Some(&gapped), true, false, true, 77);
-        assert_eq!(e, Energy::modeled(77));
+        assert_eq!(e, Energy::estimator(77));
         assert_eq!(
             because,
             vec![
@@ -1865,10 +1906,10 @@ mod tests {
     }
 
     /// Off macOS there is no per-process energy counter, so no tree meter:
-    /// every attempt that reaches `z3` keeps the model figure and says why.
+    /// every attempt that reaches `z3` keeps the estimate and says why.
     #[cfg(not(target_os = "macos"))]
     #[test]
-    fn off_macos_a_resident_decision_keeps_the_model_and_says_why() {
+    fn off_macos_a_resident_decision_keeps_the_estimate_and_says_why() {
         // Declared, so the one reason is the missing meter.
         let server = Z3Server::new().declared_self_contained(true);
         assert!(!server.is_tree_metered());
@@ -1881,7 +1922,7 @@ mod tests {
         assert!(a.verdict.is_proved());
         let acct = server.last_account().expect("an account of the attempt");
         eprintln!("z3 resident (no tree meter): {acct:?}");
-        assert_eq!(a.energy, Energy::modeled(acct.modelled_uj));
+        assert_eq!(a.energy, Energy::estimator(acct.modelled_uj));
         assert_eq!(acct.modelled_because, vec![Modelled::NoTreeMeter]);
         assert_eq!(acct.reading, None);
     }

proof/proof-rs/crates/proof-solvers/tests/z3_tree.rs

@@ -103,7 +103,7 @@ fn theorems() -> Vec<(&'static str, ProofGoal)> {
 
 /// The server for a test, or `None` (said) when there is no `z3` to decide
 /// with. On a host whose per-process counter is not live there is no tree
-/// meter, and an attempt keeps the model and says why: checked here, so
+/// meter, and an attempt keeps the estimate and says why: checked here, so
 /// that branch also asserts before the test returns.
 fn server(bound: Duration) -> Option<Z3Server> {
     if !z3_available() {
@@ -118,7 +118,7 @@ fn server(bound: Duration) -> Option<Z3Server> {
         let a = server.attempt(goal);
         let acct = server.last_account().expect("an account");
         eprintln!("z3 resident (counter {status:?}): {acct:?}");
-        assert_eq!(a.energy, Energy::modeled(acct.modelled_uj));
+        assert_eq!(a.energy, Energy::estimator(acct.modelled_uj));
         assert_eq!(acct.modelled_because, vec![Modelled::NoTreeMeter]);
         return None;
     }
@@ -162,10 +162,10 @@ fn a_resident_decision_is_hwshunt_and_equals_the_oracle() {
 /// A refuted goal: the resident `z3` decides `sat`, and a one-shot `z3`,
 /// outside the resident tree, fetches the counter-model. The span read the
 /// resident decision alone — exactly the oracle's advance on the resident
-/// `z3`, no other process in it — and the attempt keeps the model figure
-/// for the whole attempt, saying why.
+/// `z3`, no other process in it — and the attempt keeps the wall-time
+/// estimate for the whole attempt, saying why.
 #[test]
-fn a_refuted_goal_keeps_the_model_because_its_counter_model_ran_outside_the_tree() {
+fn a_refuted_goal_keeps_the_estimate_because_its_counter_model_ran_outside_the_tree() {
     let _one = alone();
     let Some(server) = server(TEST_SETTLE) else { return };
     let pid = server.pid().expect("a resident z3") as i32;
@@ -183,8 +183,8 @@ fn a_refuted_goal_keeps_the_model_because_its_counter_model_ran_outside_the_tree
         );
         assert!(matches!(a.verdict, Verdict::Refuted { .. }), "{:?}", a.verdict);
         assert_eq!(acct.modelled_because, vec![Modelled::CounterModelOutsideTree]);
-        assert_eq!(a.energy, Energy::modeled(acct.modelled_uj));
-        assert_eq!(a.energy.provenance, Provenance::ModelBased);
+        assert_eq!(a.energy, Energy::estimator(acct.modelled_uj));
+        assert_eq!(a.energy.provenance, Provenance::Estimator);
         assert!(r.is_whole(), "{:?}", r.gaps);
         assert_eq!(r.pids, vec![pid as u32], "the one-shot z3 is not in the resident tree");
         assert_eq!(r.cpu_nj, oracle, "the span is the resident decision alone");
@@ -194,7 +194,7 @@ fn a_refuted_goal_keeps_the_model_because_its_counter_model_ran_outside_the_tree
 /// The production settle bound, on this host as it is: what the metering
 /// adds to a goal's latency, and how often a decision is read whole. Every
 /// attempt is graded consistently either way — a whole reading `HwShunt` at
-/// its rounded-up figure, a gapped one the model with its gaps — and the
+/// its rounded-up figure, a gapped one the estimate with its gaps — and the
 /// numbers are logged for the record rather than asserted, because they
 /// depend on the host's load.
 #[test]
@@ -216,7 +216,7 @@ fn the_production_settle_bound_grades_every_attempt_consistently() {
                 assert!(acct.modelled_because.is_empty());
             } else {
                 gapped += 1;
-                assert_eq!(a.energy, Energy::modeled(acct.modelled_uj), "{name}: {:?}", r.gaps);
+                assert_eq!(a.energy, Energy::estimator(acct.modelled_uj), "{name}: {:?}", r.gaps);
                 assert_eq!(acct.modelled_because, vec![Modelled::Gaps(r.gaps.clone())]);
             }
             overheads.push(acct.overhead);
@@ -238,10 +238,10 @@ fn the_production_settle_bound_grades_every_attempt_consistently() {
 }
 
 /// Through the cascade: an SMT goal fails the T0 propositional decider (its
-/// figure modelled) and is proved by the resident `z3` (read whole,
-/// `HwShunt`). The goal's headline cost sums both, so it is sealed
-/// `ModelBased`, never as a hardware reading of a total that holds a model;
-/// the T1 attempt's own record keeps its hardware grade.
+/// figure the wall-time estimate) and is proved by the resident `z3` (read
+/// whole, `HwShunt`). The goal's headline cost sums both, so it is sealed
+/// `Estimator`, never as a hardware reading of a total that holds an
+/// estimate; the T1 attempt's own record keeps its hardware grade.
 #[test]
 fn a_cascade_total_holding_modelled_waste_is_not_sealed_as_hardware() {
     use proof_cascade::{ProofCache, Router};
@@ -257,8 +257,8 @@ fn a_cascade_total_holding_modelled_waste_is_not_sealed_as_hardware() {
     );
     assert!(r.proved);
     let grades: Vec<Provenance> = r.attempts.iter().map(|a| a.provenance).collect();
-    assert_eq!(grades, vec![Provenance::ModelBased, Provenance::HwShunt]);
-    assert_eq!(r.provenance, Provenance::ModelBased);
+    assert_eq!(grades, vec![Provenance::Estimator, Provenance::HwShunt]);
+    assert_eq!(r.provenance, Provenance::Estimator);
 }
 
 /// Without its operator's declaration, a resident decision read whole off
@@ -267,7 +267,7 @@ fn a_cascade_total_holding_modelled_waste_is_not_sealed_as_hardware() {
 /// container or on another host reads whole here (only the forwarding
 /// client is in the tree) while the decision's energy is charged elsewhere.
 #[test]
-fn an_undeclared_resident_decision_keeps_the_model() {
+fn an_undeclared_resident_decision_keeps_the_estimate() {
     let _one = alone();
     if !z3_available() || process_energy_status() != CounterStatus::Live {
         eprintln!("no z3, or no live per-process counter: nothing to seal either way");
@@ -279,8 +279,8 @@ fn an_undeclared_resident_decision_keeps_the_model() {
         assert!(a.verdict.is_proved(), "{name}");
         let acct = server.last_account().expect("an account of the attempt");
         eprintln!("z3 tree meter: undeclared {name}: sealed {:?}, because {:?}", a.energy, acct.modelled_because);
-        assert_eq!(a.energy.provenance, Provenance::ModelBased, "{name}: an undeclared z3 was sealed as hardware");
-        assert_eq!(a.energy, Energy::modeled(acct.modelled_uj), "{name}");
+        assert_eq!(a.energy.provenance, Provenance::Estimator, "{name}: an undeclared z3 was sealed as hardware");
+        assert_eq!(a.energy, Energy::estimator(acct.modelled_uj), "{name}");
         let r = acct.reading.clone().expect("a span was opened").expect("a reading");
         let mut want = if r.is_whole() { Vec::new() } else { vec![Modelled::Gaps(r.gaps.clone())] };
         want.push(Modelled::NotDeclaredSelfContained);

sandbox/README.md

@@ -42,7 +42,7 @@ Sandbox draws its design from two Transaction Science runtimes and generalizes a
 
 ## Status
 
-v0.1.0 draft. Specification core published (the unit, the ladder, the grant model, the per-device receipt, the attestation); the reference library lands the schema, capability, meter, attest, runtime, and conformance crates with the `sandbox` CLI, plus two **real tier executors**: a wasmtime-backed S2 executor that runs untrusted WASM under fuel and memory caps, meters fuel→joules, and brokers every capability the guest exercises (kv, clock, randomness) through the deny-by-default `Enforcer` — journaling each nondeterministic input so the run's attestation carries a replay-journal root; and a Firecracker-driver S5 executor that boots a microVM (API-socket or supervised-child lifecycle) and meters CPU and an assigned accelerator **separately** through pluggable power meters (RAPL/NVML-class, with an honest `ModelBased` fallback). Energy receipts seal as **JCR-1** envelopes (canonical det-CBOR + COSE_Sign1, EdDSA), the signed-receipt format shared across the family; attestations sign Ed25519 over JCS-canonicalized JSON, interoperable with ARL-S. The conformance vectors in [`conformance/v1/`](conformance/v1/) are real, cryptographically computed values — including a committed pack of adversarial **negatives** a conformant host must reject — regenerated by `gen_vectors` and verified by the harness (in-code and file-backed).
+v0.1.0 draft. Specification core published (the unit, the ladder, the grant model, the per-device receipt, the attestation); the reference library lands the schema, capability, meter, attest, runtime, and conformance crates with the `sandbox` CLI, plus two **real tier executors**: a wasmtime-backed S2 executor that runs untrusted WASM under fuel and memory caps, meters fuel→joules, and brokers every capability the guest exercises (kv, clock, randomness) through the deny-by-default `Enforcer` — journaling each nondeterministic input so the run's attestation carries a replay-journal root; and a Firecracker-driver S5 executor that boots a microVM (API-socket or supervised-child lifecycle) and meters CPU and an assigned accelerator **separately** through pluggable power meters (RAPL/NVML-class, with an honest fallback: `Estimator` at the reference per-vCPU-second cost, `ModelBased` only at a cost calibrated on the host). Energy receipts seal as **JCR-1** envelopes (canonical det-CBOR + COSE_Sign1, EdDSA), the signed-receipt format shared across the family; attestations sign Ed25519 over JCS-canonicalized JSON, interoperable with ARL-S. The conformance vectors in [`conformance/v1/`](conformance/v1/) are real, cryptographically computed values — including a committed pack of adversarial **negatives** a conformant host must reject — regenerated by `gen_vectors` and verified by the harness (in-code and file-backed).
 
 Readiness is classified per component (Solid / Engineering / Research / Theory) in [`SPEC.md`](SPEC.md) §9 and respected when sequencing work. The S2 (WASM) executor runs and meters real guests; the S4–S5 (microVM) driver is real Firecracker integration (it boots a guest on Linux+KVM); and the **S6/S7 confidential and sovereign tiers** are implemented end-to-end — the host obtains a TEE report, verifies it (real ECDSA-P384/SHA-384 signature + measurement/TCB/debug/report-data policy), seals the evidence into the attestation, binds a locality, and links the run into a tamper-evident audit chain. The single honest caveat (SPEC §9): *generating* a genuine vendor-signed report requires the CPU's security processor — the `configfs-tsm` provider does so on real confidential hardware and reports `Unavailable` elsewhere, while a tagged software-grounded provider, which never claims a hardware root, covers wiring and tests.
 

sandbox/SECURITY.md

@@ -59,12 +59,13 @@ to **reason about, bound, and price** them, with two levers and one inversion:
 ## Provenance honesty
 
 Every energy figure carries a provenance tag — `HwShunt` (measured at a hardware
-interface for that class), `ModelBased` (calibrated model), or `Estimator`
-(coarse constant) — and the (provenance, measured) coupling is enforced (SPEC
+interface for that class), `ModelBased` (a model calibrated on the host), or
+`Estimator` (a coarse constant, or a nominal coefficient no host calibrated) —
+and the (provenance, measured) coupling is enforced (SPEC
 §6.3, vector class C3). The standard's claim is that the figure is **reported and
 honestly tagged**, never that an estimate is a measurement. Remote silicon a
 prover does not own is metered by token-level `Estimator`, not dressed as
-measured; a contention probe is `ModelBased`, not a shunt.
+measured; a contention probe's figure is an `Estimator`, not a shunt.
 
 ## Reporting
 

sandbox/SPEC.md

@@ -215,8 +215,8 @@ A host that ran accelerated work **MUST** emit a separate record for each accele
 `provenance` is one of:
 
 - `HwShunt` — read from a hardware energy interface for that class (RAPL/powercap for CPU; NVML for NVIDIA; ROCm SMI for AMD; Level Zero for Intel; an SMC/shunt otherwise). **MUST** correspond to a present `measured_uj`.
-- `ModelBased` — computed from a calibrated per-operation model for that class. `measured_uj` **MAY** be absent.
-- `Estimator` — a coarse constant estimator. **MUST NOT** carry a `measured_uj`.
+- `ModelBased` — computed from a per-operation model for that class calibrated on the host (or against a reading), or a hardware reading apportioned by a model. `measured_uj` **MAY** be absent.
+- `Estimator` — a figure nothing calibrated: a coarse constant estimator, or a model at a nominal or assumed coefficient (wall-clock × TDP, a reference per-vCPU-second cost, a datasheet J/op). **MUST NOT** carry a `measured_uj`.
 
 A host **MUST NOT** report `measured_uj` it did not obtain from a hardware interface for that specific device class. At tiers **S5 and above**, where a hardware energy interface for a used class is available on the host, the host **MUST** use it (`HwShunt`) rather than estimate.
 

sandbox/sandbox-rs/crates/sandbox-exec-microvm/examples/boot_microvm.rs

@@ -15,8 +15,8 @@
 //! our unix-socket HTTP/1.1 client, lets the guest run briefly, and reads the
 //! package energy counters (every package's, and every die's) before and
 //! after. A genuine `HwShunt` figure where the MSRs read and every package's
-//! counter proved live; an honest `ModelBased` vCPU-seconds estimate
-//! otherwise.
+//! counter proved live; an honest vCPU-seconds `Estimator` figure otherwise
+//! (a per-vCPU-second power no host calibrated).
 
 use sandbox_exec_microvm::firecracker::{FirecrackerConfig, FirecrackerVmm, VmState, Vmm};
 use sandbox_exec_microvm::power::PowerMeter;
@@ -52,7 +52,7 @@ fn main() {
 
     // The meter: real RAPL via MSR where available (root on Nitro metal),
     // every package's and every die's, once each has proved live; else None
-    // → an honest vCPU-seconds ModelBased estimate.
+    // → an honest vCPU-seconds estimate (Estimator).
     #[cfg(target_os = "linux")]
     let meter: Option<sandbox_exec_microvm::power::MsrRaplMeter> =
         match sandbox_exec_microvm::power::MsrRaplMeter::host() {
@@ -68,7 +68,7 @@ fn main() {
     let before = meter.as_ref().and_then(|m| m.sample_uj());
     println!(
         "meter: {}",
-        if before.is_some() { "RAPL via MSR (HwShunt)" } else { "none — ModelBased fallback" }
+        if before.is_some() { "RAPL via MSR (HwShunt)" } else { "none — Estimator fallback" }
     );
 
     let cfg = FirecrackerConfig {
@@ -97,7 +97,7 @@ fn main() {
     let booted = matches!(outcome.map(|o| o.state), Ok(VmState::Booted | VmState::Completed));
     println!("guest ran {:.2}s; booted={booted}", wall.as_secs_f64());
 
-    // Build the energy record: HwShunt from the MSR delta, else ModelBased.
+    // Build the energy record: HwShunt from the MSR delta, else an estimate.
     let device = match (before, after) {
         (Some(a), Some(b)) => {
             let uj = b.saturating_sub(a);
@@ -110,14 +110,15 @@ fn main() {
             }
         }
         _ => {
-            // No hardware: vCPU-seconds × a coarse per-vCPU-second figure.
+            // No hardware: vCPU-seconds × a coarse per-vCPU-second figure (15 W),
+            // assumed, not calibrated on this host: an estimate.
             let est = (cfg.vcpus as u64).saturating_mul(wall.as_secs().max(1)).saturating_mul(15_000_000);
             println!("CPU energy (estimate): {:.3} J", est as f64 / 1e6);
             DeviceEnergy {
                 class: DeviceClass::Cpu,
                 measured_uj: None,
                 estimated_uj: est,
-                provenance: Provenance::ModelBased,
+                provenance: Provenance::Estimator,
             }
         }
     };

sandbox/sandbox-rs/crates/sandbox-exec-microvm/src/firecracker.rs

@@ -80,8 +80,8 @@ pub enum VmState {
 #[derive(Clone, Copy, Debug)]
 pub struct VmOutcome {
     pub state: VmState,
-    /// Consumed vCPU-seconds, the CPU-work proxy used for a `ModelBased`
-    /// energy estimate when no hardware meter is available.
+    /// Consumed vCPU-seconds, the CPU-work proxy priced into an energy
+    /// estimate when no hardware meter is available.
     pub vcpu_seconds: u64,
 }
 

sandbox/sandbox-rs/crates/sandbox-exec-microvm/src/lib.rs

@@ -6,8 +6,10 @@
 //! direct device assignment (SPEC §5.1). Per the heterogeneity clause, each
 //! used device class is metered **separately** (SPEC §6.2): the CPU and any
 //! assigned accelerator each get their own [`PowerMeter`], and at S5 a hardware
-//! reading is preferred (`HwShunt`) with an honest `ModelBased` fallback
-//! (SPEC §6.3).
+//! reading is preferred (`HwShunt`) with an honest fallback (SPEC §6.3): an
+//! `Estimator` figure from the reference per-vCPU-second cost, or `ModelBased`
+//! where the operator supplies a cost calibrated on this host
+//! ([`MicroVmConfig::calibrated`]).
 //!
 //! The [`firecracker`] driver is the real integration surface (it boots a guest
 //! on Linux+KVM); the [`Vmm`] trait lets the executor's assembly and metering
@@ -23,19 +25,38 @@ use sandbox_meter::{DeviceEnergy, Provenance};
 use sandbox_runtime::{ExecError, Executor, RunReport, Unit};
 use sandbox_schema::{DeviceClass, Tier};
 
-/// Tuning for the S5 executor's `ModelBased` fallback (non-normative, SPEC §6).
+/// Tuning for the S5 executor's fallback when no hardware meter reads a run
+/// (non-normative, SPEC §6).
 #[derive(Clone, Copy, Debug)]
 pub struct MicroVmConfig {
     /// Microjoules per vCPU-second, used to estimate CPU energy when no hardware
     /// meter is available. The reference figure follows the IS-Compute work-unit
-    /// cost (≈0.012 J / vCPU-second).
+    /// cost (≈0.012 J / vCPU-second), a nominal figure no host calibrated.
     pub uj_per_vcpu_second: u64,
+    /// Whether `uj_per_vcpu_second` was calibrated on this host (measured
+    /// against a reading of its draw). Only then is the CPU fallback a model,
+    /// `ModelBased`; otherwise — the reference figure, the default — it is an
+    /// estimate, `Estimator` (SPEC §6.3; JCP SPEC §5.1 rung 6).
+    pub calibrated: bool,
 }
 
 impl Default for MicroVmConfig {
     fn default() -> Self {
         MicroVmConfig {
             uj_per_vcpu_second: 12_000,
+            calibrated: false,
+        }
+    }
+}
+
+impl MicroVmConfig {
+    /// The grade of a figure priced by `uj_per_vcpu_second`: `ModelBased` for
+    /// a cost calibrated on this host, else `Estimator`.
+    fn fallback_provenance(&self) -> Provenance {
+        if self.calibrated {
+            Provenance::ModelBased
+        } else {
+            Provenance::Estimator
         }
     }
 }
@@ -95,20 +116,21 @@ impl MicroVmExecutor {
             // S5 with a hardware interface: HwShunt measured (SPEC §6.3) - but
             // only if the counter advanced. vCPU work ran, so a CPU counter that
             // held across it is not a reading of that work (a frozen or
-            // lump-refreshed counter); it falls to the model estimate below,
-            // never a measured zero. (Same rule as sandbox-meter's `Span::stop`.)
+            // lump-refreshed counter); it falls to the estimate below, never a
+            // measured zero. (Same rule as sandbox-meter's `Span::stop`.)
             (Some(b), Some(a)) if a > b => DeviceEnergy {
                 class: DeviceClass::Cpu,
                 measured_uj: Some(a - b),
                 estimated_uj: a - b,
                 provenance: Provenance::HwShunt,
             },
-            // No hardware reading: honest ModelBased estimate.
+            // No hardware reading: vCPU-seconds × the configured cost, graded
+            // by whether that cost was calibrated on this host.
             _ => DeviceEnergy {
                 class: DeviceClass::Cpu,
                 measured_uj: None,
                 estimated_uj: vcpu_seconds.saturating_mul(self.cfg.uj_per_vcpu_second),
-                provenance: Provenance::ModelBased,
+                provenance: self.cfg.fallback_provenance(),
             },
         }
     }
@@ -131,8 +153,10 @@ impl MicroVmExecutor {
                 class: accel.class,
                 measured_uj: None,
                 // Coarse proxy: accelerators dominate, so scale the vCPU figure.
+                // Nothing calibrated that factor on the accelerator, whatever
+                // the CPU cost's calibration, so this is always an estimate.
                 estimated_uj: vcpu_seconds.saturating_mul(cfg.uj_per_vcpu_second * 10),
-                provenance: Provenance::ModelBased,
+                provenance: Provenance::Estimator,
             },
         }
     }
@@ -252,7 +276,7 @@ mod tests {
     }
 
     #[test]
-    fn cpu_only_run_meters_modelbased() {
+    fn cpu_only_run_meters_an_estimate() {
         let exec = MicroVmExecutor::new(
             Box::new(MockVmm {
                 state: VmState::Completed,
@@ -270,12 +294,12 @@ mod tests {
         assert_eq!(report.device_energy.len(), 1);
         let cpu = report.device_energy[0];
         assert_eq!(cpu.class, DeviceClass::Cpu);
-        assert_eq!(cpu.provenance, Provenance::ModelBased);
+        assert_eq!(cpu.provenance, Provenance::Estimator);
         assert_eq!(cpu.estimated_uj, 4 * 12_000);
     }
 
     /// vCPU work ran, so a CPU counter that held across it is not a reading
-    /// of that work: the figure is the model estimate, never a measured zero.
+    /// of that work: the figure is the estimate, never a measured zero.
     /// A counter that advanced is the reading.
     #[test]
     fn a_cpu_counter_that_held_across_a_run_is_not_a_measured_zero() {
@@ -285,7 +309,7 @@ mod tests {
             Box::new(NoMeter),
         );
         let held = exec.cpu_energy(Some(5_000), Some(5_000), 4);
-        assert_eq!(held.provenance, Provenance::ModelBased, "a held counter sealed as {held:?}");
+        assert_eq!(held.provenance, Provenance::Estimator, "a held counter sealed as {held:?}");
         assert_eq!(held.measured_uj, None);
         assert_eq!(held.estimated_uj, 4 * 12_000);
 
@@ -361,6 +385,46 @@ mod tests {
             .any(|d| d.class == DeviceClass::Gpu && d.model == "NVIDIA H100"));
     }
 
+    /// The CPU fallback's grade is its cost's: the reference per-vCPU-second
+    /// figure, which no host calibrated, prices an estimate (`Estimator`); a
+    /// cost the operator calibrated on this host prices a model
+    /// (`ModelBased`). The accelerator's proxy (the CPU cost × 10) is an
+    /// estimate either way: nothing calibrated that factor.
+    #[test]
+    fn a_fallback_is_a_model_only_at_a_host_calibrated_cost() {
+        let exec = |cfg: MicroVmConfig| {
+            MicroVmExecutor::new(
+                Box::new(MockVmm { state: VmState::Completed, vcpu_seconds: 4 }),
+                template(),
+                Box::new(NoMeter),
+            )
+            .with_config(cfg)
+        };
+        let accel = Accelerator {
+            class: DeviceClass::Gpu,
+            identity: DeviceIdentity { class: DeviceClass::Gpu, model: "gpu".into(), driver: "vfio".into() },
+            meter: Box::new(NoMeter),
+        };
+        let reference = MicroVmConfig::default();
+        assert!(!reference.calibrated, "the reference cost is not a calibration of any host");
+        let calibrated = MicroVmConfig { uj_per_vcpu_second: 3_000_000, calibrated: true };
+        for (cfg, grade) in [(reference, Provenance::Estimator), (calibrated, Provenance::ModelBased)] {
+            let cpu = exec(cfg).cpu_energy(None, None, 4);
+            assert_eq!(
+                (cpu.provenance, cpu.measured_uj, cpu.estimated_uj),
+                (grade, None, 4 * cfg.uj_per_vcpu_second),
+                "{cfg:?}"
+            );
+            cpu.check_provenance().unwrap();
+            let gpu = MicroVmExecutor::accel_energy(&accel, None, None, 4, &cfg);
+            assert_eq!(
+                (gpu.provenance, gpu.measured_uj, gpu.estimated_uj),
+                (Provenance::Estimator, None, 4 * cfg.uj_per_vcpu_second * 10),
+                "{cfg:?}"
+            );
+        }
+    }
+
     #[test]
     fn unconfigured_accelerator_is_rejected() {
         // Grant a TPU but configure no accelerator ⇒ Unsupported.

sandbox/sandbox-rs/crates/sandbox-exec-microvm/src/power.rs

@@ -3,7 +3,7 @@
 //! At tier S5 and above, where a hardware energy interface for a used class is
 //! available, the host MUST read it (`HwShunt`) rather than estimate
 //! (SPEC §6.3). A [`PowerMeter`] abstracts that interface so the executor can
-//! prefer a hardware reading and fall back to an honest `ModelBased` estimate
+//! prefer a hardware reading and fall back to an honest estimate
 //! where none exists — tagging the provenance accordingly.
 //!
 //! **A CPU figure is every package's, and only a live counter's.** Both CPU
@@ -357,7 +357,7 @@ mod msr {
 }
 
 /// A meter with no hardware interface — `sample_uj` is always `None`, forcing
-/// the executor onto the honest `ModelBased` estimate path (SPEC §6.3).
+/// the executor onto the honest estimate path (SPEC §6.3).
 pub struct NoMeter;
 
 impl PowerMeter for NoMeter {
@@ -387,7 +387,7 @@ mod tests {
     use sandbox_runtime::{Executor, Unit};
     use sandbox_schema::DeviceClass;
     use std::path::PathBuf;
-    use std::sync::atomic::{AtomicBool, AtomicUsize, Ordering::SeqCst};
+    use std::sync::atomic::{AtomicUsize, Ordering::SeqCst};
     use std::time::Duration;
 
     #[test]
@@ -438,32 +438,22 @@ mod tests {
         std::fs::rename(&tmp, &path).unwrap();
     }
 
-    /// Run `f` while another thread calls `write` with a rising step every
-    /// 2 ms; the thread stops when `f` returns or panics.
-    fn advancing<T>(write: impl Fn(u64) + Sync, f: impl FnOnce() -> T) -> T {
-        struct StopOnDrop<'a>(&'a AtomicBool);
-        impl Drop for StopOnDrop<'_> {
-            fn drop(&mut self) {
-                self.0.store(true, SeqCst);
-            }
+    /// A liveness tick that advances the fake counters itself: each call
+    /// writes the next rising step through `write`, then sleeps as
+    /// [`sleep_tick`] does. Every interval the probe samples therefore holds
+    /// exactly one advance, however the host schedules threads. A writer
+    /// thread on a timer, as these tests once used, can be starved on a loaded
+    /// host, and the probe then rightly judged a live fake counter frozen.
+    fn advancing_tick(write: impl Fn(u64)) -> impl FnMut() -> TickOutcome {
+        let mut step = 0;
+        move || {
+            step += 1;
+            write(step);
+            sleep_tick()
         }
-        let stop = AtomicBool::new(false);
-        std::thread::scope(|s| {
-            s.spawn(|| {
-                let mut step = 0;
-                while !stop.load(SeqCst) {
-                    step += 1;
-                    write(step);
-                    std::thread::sleep(Duration::from_millis(2));
-                }
-            });
-            let _stop = StopOnDrop(&stop);
-            f()
-        })
     }
 
-    /// The liveness tick the tests drive: a sleep, while a writer thread
-    /// advances the counters.
+    /// The sleep half of the liveness tick the tests drive.
     /// A scripted stand-in for the production burn: these trees are fakes and
     /// the load that matters is the script's writes. It reports a turn, so the
     /// probe's "did the tick run" rule is satisfied honestly rather than by a
@@ -546,15 +536,15 @@ mod tests {
     }
 
     /// `RaplMeter::live_in` over `tree` while the zones in `advancing_zones`
-    /// rise by 4 mJ every 2 ms and the rest hold.
+    /// rise by 4 mJ every tick and the rest hold.
     fn rapl_live_in(tree: &FakeTree, advancing_zones: &[&str]) -> RaplMeter {
-        advancing(
-            |step| {
+        RaplMeter::live_in(
+            &tree.root,
+            advancing_tick(|step| {
                 for dir in advancing_zones {
                     set_uj(&tree.root, dir, 100_000 + 4_000 * step);
                 }
-            },
-            || RaplMeter::live_in(&tree.root, sleep_tick),
+            }),
         )
     }
 
@@ -615,7 +605,7 @@ mod tests {
         assert!(why.contains("RAPL"), "{why}");
         assert_eq!(meter.sample_uj(), None);
         let cpu = cpu_record_of(Box::new(meter), || {});
-        assert_eq!((cpu.measured_uj, cpu.provenance), (None, Provenance::ModelBased));
+        assert_eq!((cpu.measured_uj, cpu.provenance), (None, Provenance::Estimator));
 
         for (tree, expect) in [
             (powercap(&[("intel-rapl:0", "psys", 90_000, Some(262_143_328_850))]), "no RAPL package zone"),
@@ -649,7 +639,7 @@ mod tests {
         assert_eq!(meter.sample_uj(), None, "a broken count read again");
         let root = tree.root.clone();
         let cpu = cpu_record_of(Box::new(meter), move || set_uj(&root, "intel-rapl:0", 2_100_000_000));
-        assert_eq!((cpu.measured_uj, cpu.provenance), (None, Provenance::ModelBased));
+        assert_eq!((cpu.measured_uj, cpu.provenance), (None, Provenance::Estimator));
     }
 
     // ---- RAPL through the MSRs: Unix only, where the meter is built under test.
@@ -699,16 +689,16 @@ mod tests {
         }
 
         /// `MsrRaplMeter::live_in` over `tree` while the CPUs in `advancing_cpus`
-        /// count up by 4,096 every 2 ms (a multiple of 256, so every figure here
+        /// count up by 4,096 every tick (a multiple of 256, so every figure here
         /// is a whole number of microjoules at ESU 14) and the rest hold.
         fn msr_live_in(tree: &FakeTree, advancing_cpus: &[u32]) -> Result<msr::MsrRaplMeter, String> {
-            advancing(
-                |step| {
+            msr::MsrRaplMeter::live_in(
+                &tree.root,
+                advancing_tick(|step| {
                     for cpu in advancing_cpus {
                         set_msr(&tree.root, *cpu, unit_raw(14), 1_000_192 + 4_096 * step);
                     }
-                },
-                || msr::MsrRaplMeter::live_in(&tree.root, sleep_tick),
+                }),
             )
         }
 

sandbox/sandbox-rs/crates/sandbox-exec-wasm/src/lib.rs

@@ -4,9 +4,11 @@
 //! [`Tier::S2`] (SPEC §2.2): the unit runs inside a managed WASM runtime with
 //! **fuel metering** (the instruction-budget proxy for CPU work) and a
 //! **memory cap**, derived from the unit's [`ComputeGrant`]. Fuel consumed is
-//! converted to energy and reported on the [`DeviceClass::Cpu`] record with
-//! `Provenance::ModelBased` — honest for a tier below S5, where no per-unit
-//! hardware energy interface is asserted (SPEC §6.3).
+//! converted to energy and reported on the [`DeviceClass::Cpu`] record — honest
+//! for a tier below S5, where no per-unit hardware energy interface is asserted
+//! (SPEC §6.3) — graded `Estimator` at the reference cost per fuel, which no
+//! host calibrated, and `ModelBased` only for a cost the operator calibrated on
+//! this host ([`WasmConfig::fuel_cost_calibrated`]).
 //!
 //! **Convention:** a conforming unit exports `run` with signature `() -> i32`
 //! (0 = success). A non-zero return is recorded as `Outcome::Failed`; a trap
@@ -34,6 +36,11 @@ pub struct WasmConfig {
     /// Microjoules attributed per million fuel units consumed. Fuel is the
     /// WASM instruction-execution proxy.
     pub uj_per_million_fuel: u64,
+    /// Whether `uj_per_million_fuel` was calibrated on this host (measured
+    /// against a reading of its draw). Only then is the CPU figure a model,
+    /// `ModelBased`; otherwise — the reference figure, the default — it is an
+    /// estimate, `Estimator` (JCP SPEC §5.1 rung 6).
+    pub fuel_cost_calibrated: bool,
     /// Fuel budget per granted millisecond of CPU time. Bounds the run.
     pub fuel_per_cpu_ms: u64,
     /// Memory cap (bytes) used when the grant leaves `memory_bytes` at 0.
@@ -45,7 +52,8 @@ pub struct WasmConfig {
 impl Default for WasmConfig {
     fn default() -> Self {
         WasmConfig {
-            uj_per_million_fuel: 20_000, // 0.02 J / Mfuel
+            uj_per_million_fuel: 20_000, // 0.02 J / Mfuel, nominal
+            fuel_cost_calibrated: false,
             fuel_per_cpu_ms: 5_000_000,  // ~5M instructions ≈ 1ms (order-of-magnitude)
             default_memory_bytes: 64 * 1024 * 1024,
             default_fuel: 50_000_000,
@@ -106,7 +114,7 @@ impl WasmExecutor {
             class: DeviceClass::Cpu,
             measured_uj: None,
             estimated_uj: est,
-            provenance: Provenance::ModelBased,
+            provenance: if self.cfg.fuel_cost_calibrated { Provenance::ModelBased } else { Provenance::Estimator },
         }
     }
 
@@ -207,7 +215,7 @@ impl Executor for WasmExecutor {
         let journal = data.journal;
         // The broker counted storage I/O for ceiling enforcement; surface it as
         // a metered line (volume-only — the in-process vfs has no device to
-        // time, so contention is not measured). Honest `ModelBased`.
+        // time, so contention is not measured). An honest estimate.
         let storage = if data.storage_ops > 0 {
             Some(sandbox_meter::StorageActivity::from_volume(
                 data.storage_ops,
@@ -315,11 +323,26 @@ mod tests {
         assert_eq!(report.device_energy.len(), 1);
         let cpu = report.device_energy[0];
         assert_eq!(cpu.class, DeviceClass::Cpu);
-        assert_eq!(cpu.provenance, Provenance::ModelBased);
+        assert_eq!(cpu.provenance, Provenance::Estimator, "the reference fuel cost is no host's calibration");
         assert!(cpu.estimated_uj > 0, "some fuel was consumed");
         assert_eq!(report.device_identity[0].driver, "wasmtime");
     }
 
+    /// The CPU figure's grade is its fuel cost's: the reference cost, which
+    /// no host calibrated, prices an estimate; a cost calibrated on this host
+    /// prices a model. The figure is the same arithmetic either way.
+    #[test]
+    fn a_fuel_figure_is_a_model_only_at_a_host_calibrated_cost() {
+        let reference = WasmExecutor::with_defaults().unwrap();
+        let calibrated =
+            WasmExecutor::new(WasmConfig { fuel_cost_calibrated: true, ..WasmConfig::default() }).unwrap();
+        for (exec, grade) in [(&reference, Provenance::Estimator), (&calibrated, Provenance::ModelBased)] {
+            let cpu = exec.cpu_energy(3_000_000);
+            assert_eq!((cpu.provenance, cpu.measured_uj, cpu.estimated_uj), (grade, None, 60_000));
+            cpu.check_provenance().unwrap();
+        }
+    }
+
     #[test]
     fn nonzero_return_is_failure() {
         let exec = WasmExecutor::with_defaults().unwrap();
@@ -493,11 +516,11 @@ mod tests {
             .any(|e| matches!(e, sandbox_attest::JournalEntry::HostCall { name, .. } if name == "storage_read")));
 
         // The brokered I/O is metered as a storage line (SPEC §6.5): one write +
-        // one read ⇒ 2 ops, 7 bytes read ("payload"), honest ModelBased.
+        // one read ⇒ 2 ops, 7 bytes read ("payload"), an honest estimate.
         let storage = report.storage.expect("storage activity was metered");
         assert_eq!(storage.iops, 2);
         assert_eq!(storage.bytes, 7);
-        assert_eq!(storage.provenance, sandbox_meter::Provenance::ModelBased);
+        assert_eq!(storage.provenance, sandbox_meter::Provenance::Estimator);
         assert!(storage.estimated_uj > 0);
     }
 

sandbox/sandbox-rs/crates/sandbox-meter/src/contention.rs

@@ -5,11 +5,14 @@
 //! **cooperatively by the host and disclosed**, a legitimate measurement
 //! instrument for a resource the platform usually cannot meter: the SSD. A
 //! probe issues page-cache-busting reads, times them against an idle baseline,
-//! and reports the device's observed activity plus a model-based energy figure.
+//! and reports the device's observed activity plus an estimated energy figure.
 //!
-//! The measurement is ALWAYS `ModelBased` (or coarser, `Estimator`): a timing
-//! channel is not a hardware shunt, and the standard's provenance honesty
-//! (SPEC §6.3) forbids dressing a derived figure as a measured one. Storage is
+//! The energy figure is NEVER `HwShunt`: a timing channel is not a hardware
+//! shunt, and the standard's provenance honesty (SPEC §6.3) forbids dressing a
+//! derived figure as a measured one. Nor is it `ModelBased`: the op/byte
+//! coefficients below are nominal NVMe-class figures, not a calibration of
+//! this host's device, so the figure is an estimate, `Estimator` (JCP SPEC
+//! §5.1 rung 6). Storage is
 //! a distinct resource axis from the compute device classes, so this is its own
 //! line — it does not enter the per-device-class energy sum of a [`Receipt`],
 //! and adding it never perturbs the sealed receipt format or its vectors.
@@ -48,23 +51,24 @@ pub struct StorageActivity {
     /// Contention signal — how much load slowed reads, nanoseconds
     /// (`loaded_ns − baseline_ns`, floored at zero).
     pub contention_ns: u64,
-    /// Modeled energy for the storage activity, integer microjoules.
+    /// Estimated energy for the storage activity, integer microjoules.
     pub estimated_uj: u64,
     /// How honest the figure is. Never [`Provenance::HwShunt`] — a timing
     /// channel is not a shunt.
     pub provenance: Provenance,
 }
 
-/// Calibrated NVMe-class energy model (integer picojoules). Coarse but honest:
-/// the figure is `ModelBased`, never claimed as measured.
+/// Nominal NVMe-class energy coefficients (integer picojoules), not measured
+/// on this host's device. Coarse but honest: the figure is `Estimator`, never
+/// claimed as measured or as a calibrated model.
 const PJ_PER_OP: u128 = 1_200_000; // ~1.2 µJ for a 4 KiB random read
 const PJ_PER_BYTE: u128 = 50; // ~0.05 nJ per byte transferred
 
 impl StorageActivity {
     /// Build a measurement from a window of under-load read-latency samples
     /// (nanoseconds), an idle baseline, and the byte/op counts. Energy is the
-    /// integer picojoule model above, reported in microjoules and tagged
-    /// [`Provenance::ModelBased`].
+    /// integer picojoule coefficients above, reported in microjoules and
+    /// tagged [`Provenance::Estimator`].
     pub fn from_samples(
         baseline_ns: u64,
         loaded_ns_samples: &[u64],
@@ -85,15 +89,15 @@ impl StorageActivity {
             loaded_ns,
             contention_ns,
             estimated_uj,
-            provenance: Provenance::ModelBased,
+            provenance: Provenance::Estimator,
         })
     }
 
     /// Build a measurement from **counted I/O volume only**, for a host that
     /// brokers and counts storage operations but does not run a timing probe
     /// (e.g. the in-process WASM executor, whose virtual filesystem has no real
-    /// device to time). The energy figure is the same `ModelBased` op/byte
-    /// model; the timing fields are zero, meaning *not measured* — there is no
+    /// device to time). The energy figure is the same `Estimator` op/byte
+    /// figure; the timing fields are zero, meaning *not measured* — there is no
     /// contention signal without a probe, and the standard does not invent one.
     pub fn from_volume(iops: u64, bytes: u64) -> Self {
         let pj = PJ_PER_OP * iops as u128 + PJ_PER_BYTE * bytes as u128;
@@ -104,7 +108,7 @@ impl StorageActivity {
             loaded_ns: 0,
             contention_ns: 0,
             estimated_uj: (pj / 1_000_000) as u64,
-            provenance: Provenance::ModelBased,
+            provenance: Provenance::Estimator,
         }
     }
 
@@ -137,7 +141,7 @@ mod tests {
         let a = StorageActivity::from_samples(100, &[260, 300, 280], 4096 * 3, 3).unwrap();
         assert_eq!(a.loaded_ns, 280); // median of the three
         assert_eq!(a.contention_ns, 180);
-        assert_eq!(a.provenance, Provenance::ModelBased);
+        assert_eq!(a.provenance, Provenance::Estimator, "nominal coefficients are no host's calibration");
         assert!(a.estimated_uj > 0);
         a.check_provenance().unwrap();
     }
@@ -157,6 +161,20 @@ mod tests {
         );
     }
 
+    /// Both constructors grade the figure `Estimator`: the coefficients are
+    /// nominal, so neither the timed window nor the counted volume makes it a
+    /// calibrated model.
+    #[test]
+    fn the_nominal_storage_figure_is_an_estimate() {
+        let timed = StorageActivity::from_samples(100, &[200], 4096, 2).unwrap();
+        let counted = StorageActivity::from_volume(2, 4096);
+        for a in [timed, counted] {
+            assert_eq!(a.provenance, Provenance::Estimator, "{a:?}");
+            assert_eq!(a.estimated_uj, 2, "2 ops × 1.2 µJ + 4096 B × 50 pJ = 2.6 µJ, floored");
+            a.check_provenance().unwrap();
+        }
+    }
+
     #[test]
     fn timing_cannot_claim_a_shunt() {
         let mut a = StorageActivity::from_samples(100, &[200], 4096, 1).unwrap();

sandbox/sandbox-rs/crates/sandbox-meter/src/lib.rs

@@ -38,9 +38,13 @@ pub enum Provenance {
     /// Read from a hardware energy interface for this device class
     /// (RAPL/NVML/ROCm SMI/Level Zero/SMC). Requires a present `measured_uj`.
     HwShunt,
-    /// Computed from a calibrated per-operation model. `measured_uj` may be absent.
+    /// Computed from a per-operation model calibrated on the host or against a
+    /// reading, or a real reading apportioned by a model (`probe::attribute`).
+    /// `measured_uj` may be absent.
     ModelBased,
-    /// A coarse constant estimator. `measured_uj` MUST be absent.
+    /// A figure nothing calibrated: a coarse constant, or a model at a nominal
+    /// or assumed coefficient (wall-clock × TDP, a datasheet J/op). `measured_uj`
+    /// MUST be absent.
     Estimator,
 }
 

sandbox/spec/receipts.md

@@ -37,8 +37,8 @@ This is the clause that distinguishes a Sandbox receipt from a process-sandbox c
 | Tag | Meaning | `measured_uj` |
 |---|---|---|
 | `HwShunt` | read from a hardware energy interface for **this class** | **MUST** be present |
-| `ModelBased` | from a calibrated per-operation model for this class | **MAY** be absent |
-| `Estimator` | a coarse constant estimator | **MUST** be absent |
+| `ModelBased` | from a per-operation model for this class calibrated on the host, or a reading apportioned by a model | **MAY** be absent |
+| `Estimator` | a figure nothing calibrated: a coarse constant, or a model at a nominal or assumed coefficient | **MUST** be absent |
 
 Per-class hardware interfaces the reference recognizes: **CPU** — Linux powercap/RAPL, AMD energy, Apple SMC; **GPU** — NVIDIA NVML `nvmlDeviceGetTotalEnergyConsumption`, AMD ROCm SMI, Intel Level Zero; **NPU/TPU/LPU/Photonic/Quantum** — the device's own energy or power-integration interface where one exists.
 
@@ -52,18 +52,18 @@ Rules:
 
 When no hardware interface is available, a host estimates. The reference coefficients (microjoules) are tunable; the **standard is that the figure is reported and honestly tagged, not the constant**:
 
-- CPU: per vCPU-millisecond cost from a calibrated table.
-- Accelerator: per device-operation (e.g. per TFLOP-second, per inference forward pass) from a calibrated table, tagged `ModelBased`.
-- Last resort: a coarse constant per class, tagged `Estimator`.
+- CPU: per vCPU-millisecond cost from a table calibrated on the host, tagged `ModelBased`.
+- Accelerator: per device-operation (e.g. per TFLOP-second, per inference forward pass) from a table calibrated on the host, tagged `ModelBased`.
+- Otherwise — a reference or nominal coefficient no host calibrated (the reference executors' defaults: a per-vCPU-second cost, a cost per million WASM fuel units, an accelerator proxy scaled from the CPU figure), or a coarse constant per class — tagged `Estimator`. The coefficient is the whole of such a model, so an uncalibrated one makes the figure an estimate.
 
 ## Storage activity — measurement from contention (non-normative)
 
-Storage is a resource the platform usually cannot meter: there is no per-tenant SSD energy interface the way there is RAPL for the CPU. The standard turns the **measurement technique behind a known side channel** to honest use. The contention a unit creates — random-read latency rising as a shared device saturates (`SECURITY.md` describes the adversarial version) — is, **measured cooperatively by the host and disclosed**, a real signal: a probe times page-cache-busting reads against an idle baseline and reports the device's observed activity (`iops`, `bytes`, `contention_ns`) and a model-based energy figure.
+Storage is a resource the platform usually cannot meter: there is no per-tenant SSD energy interface the way there is RAPL for the CPU. The standard turns the **measurement technique behind a known side channel** to honest use. The contention a unit creates — random-read latency rising as a shared device saturates (`SECURITY.md` describes the adversarial version) — is, **measured cooperatively by the host and disclosed**, a real signal: a probe times page-cache-busting reads against an idle baseline and reports the device's observed activity (`iops`, `bytes`, `contention_ns`) and an estimated energy figure.
 
 Two disciplines keep it honest:
 
 1. **It is a distinct axis, not a device class.** Storage activity is its own line (`sandbox-meter::StorageActivity`); it does **not** enter the per-device-class energy sum of §6.2, and reporting it never perturbs the sealed receipt format or its vectors. Storage is not folded into a compute class it did not consume.
-2. **It is never `HwShunt`.** A timing-derived figure is `ModelBased` (or coarser, `Estimator`); a timing channel is not a hardware shunt, and the provenance coupling (§6.3) is enforced for it exactly as for a device record. The same physics that leaks information when undisclosed becomes auditable telemetry when the host runs it on itself and tags it truthfully.
+2. **It is never `HwShunt`.** A timing-derived figure is `Estimator` at the reference's nominal per-op and per-byte coefficients (`ModelBased` only with coefficients calibrated on the host's device); a timing channel is not a hardware shunt, and the provenance coupling (§6.3) is enforced for it exactly as for a device record. The same physics that leaks information when undisclosed becomes auditable telemetry when the host runs it on itself and tags it truthfully.
 
 ## Signed form (JCR-1)
 

wai/wai-web/src/video_ott.rs

@@ -75,6 +75,8 @@ pub struct OttSession {
 impl OttSession {
     /// Compose a session class, render its manifest and seal the receipt.
     /// `blackouts` is a comma-separated set (order-independent by construction).
+    /// `joules_micro` is the page's figure: sealed `Estimator` when non-zero,
+    /// since nothing here measured or calibrated it, and unmetered at zero.
     #[wasm_bindgen(constructor)]
     #[allow(clippy::too_many_arguments)]
     pub fn new(
@@ -110,7 +112,11 @@ impl OttSession {
             joule_ceiling_micro: u64::MAX,
             funds_ceiling: None,
         };
-        let prov = (joules_micro > 0).then_some(EnergyProvenance::ModelBased);
+        // The page supplies the figure; nothing here measured or modelled it,
+        // and no host calibrated it, so it is sealed as what it is: an
+        // estimate (`Estimator`), never `ModelBased`. Zero is the unmetered
+        // marker, with no class.
+        let prov = (joules_micro > 0).then_some(EnergyProvenance::Estimator);
         let receipt = ManifestReceipt::seal(
             &demo_key(),
             "did:key:demo-packager",
@@ -268,3 +274,25 @@ impl OttAdBreak {
         format!("[{}]", rows.join(","))
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    /// The page hands the session a joule figure that nothing here measured,
+    /// modelled or calibrated: a non-zero one is sealed `Estimator`, never
+    /// `ModelBased`, and zero is the unmetered marker, with no class. The
+    /// receipt verifies either way.
+    #[test]
+    fn a_page_supplied_figure_is_sealed_as_an_estimate() {
+        let session = |uj: u64| OttSession::new("film-1", "svod", "US", "", "pod-1", 60, 3, "ad-1", 4, uj);
+        let metered = session(8_000);
+        assert_eq!(metered.receipt.energy_provenance, Some(EnergyProvenance::Estimator));
+        assert_eq!(metered.uj_per_viewer(), 2_000.0);
+        assert!(metered.verify() && metered.verify_delivered());
+        let unmetered = session(0);
+        assert_eq!(unmetered.receipt.energy_provenance, None);
+        assert_eq!(unmetered.uj_per_viewer(), -1.0);
+        assert!(unmetered.verify());
+    }
+}