From cbf57f71a844f54481d7ffa06fed5250c44c5d3d Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sun, 11 Oct 2026 22:47:45 -0400 Subject: [PATCH 1/2] joulecontract: an unattested Metered tag falls to the class its evidence supports MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A Metered tag whose meter attestation did not bind was always demoted to ModelBased, but ModelBased is defined (SPEC §4.2) as a figure anchored to a metered baseline, with that anchor sealed. A receipt with no meter and no anchor was therefore certified ModelBased on evidence it did not carry. An unbound reading is no reading: the class now falls to ModelBased only where the metered-baseline anchor is sealed, else to Unaccounted (with the `unaccounted` demotion), on the issue side and on the sealed-evidence side alike; an unresolved anchor still demotes a ModelBased figure to Unaccounted after that. SPEC §4.2 and the §15 demotion table say so. The metered_unattested negative vector, regenerated by gen_vectors, now composes to ⟨JR-3 · Unaccounted · certified⟩ with demotions metered_unattested and unaccounted; the other 21 vectors are byte-identical. A unit test pins both branches (no anchor → Unaccounted; anchor → ModelBased). Co-Authored-By: Claude Opus 5.5 --- joulecontract/SPEC.md | 4 +- joulecontract/conformance/v1/MANIFEST.json | 4 +- .../v1/negative-metered_unattested.json | 9 +-- .../src/bin/gen_vectors.rs | 2 +- .../crates/joulecontract-receipt/src/lib.rs | 65 ++++++++++++++++--- 5 files changed, 66 insertions(+), 18 deletions(-) diff --git a/joulecontract/SPEC.md b/joulecontract/SPEC.md index b77a82ac7..2cec7da83 100644 --- a/joulecontract/SPEC.md +++ b/joulecontract/SPEC.md @@ -110,7 +110,7 @@ Correctness clauses are binary; the ceiling yields a **measured residual** (allo Every joule figure MUST carry one of three measurement categories, and the category itself is a trust-bearing field under §1 — it binds or it demotes: -- **`Metered`** — hardware-measured, and the claim MUST be bound: the figure resolves (within the sealed evidence, §5.1.3) to a **meter or substrate attestation** — a signed reading or telemetry statement from the metering subsystem (hardware shunt, PDU, substrate/cloud telemetry endpoint) — signed by a key **distinct from the receipt signer**, validity-windowed per §6.1's pattern. A `Metered` tag without a resolving meter attestation serializes **`metered_unattested`** and is treated as `ModelBased` for the Energy class. Whoever owns the meter owns the unit of account; on producer-owned bare metal with no independent meter, the lower categories exist precisely to record that honestly. +- **`Metered`** — hardware-measured, and the claim MUST be bound: the figure resolves (within the sealed evidence, §5.1.3) to a **meter or substrate attestation** — a signed reading or telemetry statement from the metering subsystem (hardware shunt, PDU, substrate/cloud telemetry endpoint) — signed by a key **distinct from the receipt signer**, validity-windowed per §6.1's pattern. A `Metered` tag without a resolving meter attestation serializes **`metered_unattested`**: an unbound reading is no reading, so the Energy class falls to what the receipt's remaining evidence supports — `ModelBased` where it seals the metered-baseline anchor that class is defined by, else `Unaccounted`. Whoever owns the meter owns the unit of account; on producer-owned bare metal with no independent meter, the lower categories exist precisely to record that honestly. - **`ModelBased`** — anchored to a metered baseline for a comparable workload; the anchor reference is sealed. - **`Unaccounted`** — estimated by published energy-traceability methods where the substrate exposes nothing; the method reference is sealed. @@ -368,7 +368,7 @@ Three adversarial rounds, each finding the layer beneath the last repair: the v0 | `recourse_undeclared` | Verifier under no recognized liability regime | Profiles MAY reject; relying parties weight accordingly | | `self_attested` | Generation-loop receipt discharged only by the generator | Non-promotable (§6.3) | | `unterminated` | Trust chain reaching no defined root (§5.1.2) | Treated as unattested; qualification trigger (§6.1) | -| `metered_unattested` | `Metered` tag without a sealed, non-signer meter attestation | Treated as `ModelBased` for Energy class (§4.2) | +| `metered_unattested` | `Metered` tag without a sealed, non-signer meter attestation | Energy class falls to `ModelBased` where a metered-baseline anchor is sealed, else `Unaccounted` (§4.2) | | `ceiling_unanchored` | Ceiling without a derivation binding to its EnB | Residual carries no evidentiary weight (§4.2) | | `component_unattributed` | Composed energy figure without per-component attribution | Cannot feed ratchet or residual claims (§3.3) | | `breach_unamended` | Deviation with no forward-looking amendment or fix-receipt | Caps Governance class until closed (§5.2) | diff --git a/joulecontract/conformance/v1/MANIFEST.json b/joulecontract/conformance/v1/MANIFEST.json index a6026befc..ab3944e67 100644 --- a/joulecontract/conformance/v1/MANIFEST.json +++ b/joulecontract/conformance/v1/MANIFEST.json @@ -14,7 +14,7 @@ "negative-generator_unattested.json": "sha2-256:086f11b41086cc6ff43fc8b53340e4b7787176d69a79089163e885dcb137aa58", "negative-independent_false.json": "sha2-256:86075e4473d3952590477530987436fba84084f163a3343ab435bd43c9af99c3", "negative-independent_key_only.json": "sha2-256:6fa2299f250e74fbbbc955581d092cf443b37191a38a697cfd2df372fff3dbd8", - "negative-metered_unattested.json": "sha2-256:3ca3bf3374d6c8a41af459d8614e79f98aa5c5d55e6f4edf92ad19448db055b5", + "negative-metered_unattested.json": "sha2-256:840e7d84527487328e4e67e6208dafe642597500c2abdce7945a23de6d06de80", "negative-recourse_undeclared.json": "sha2-256:4e0fc3e8dfedd6b1fac2440605d03e8696e117ab561121247f6bdc3fc3bc1c6e", "negative-self_attested_loop.json": "sha2-256:e6a7fe5a9c436e2a473c2b1110f2c9b13f838524c1877a2ba91836e5d3fe7579", "negative-static_only_frame.json": "sha2-256:b9a33251abf91dbe2d6d7d9b778471c3bfd8eefabd42d6f3e74ba71ee7a2bbcb", @@ -23,6 +23,6 @@ "receipt-conformant.json": "sha2-256:ee72f1ad293415bbc1f2564cbd1a5e463daba49ca1683ad0ca41164ae0aced07", "receipt-jr4-conformant.json": "sha2-256:0ac9b7c564b757b1a48f57786be8bdeb3774569da0cc45cea006e1200c51a47c" }, - "manifest_address": "sha2-256:f936637603e48847dd68d65f562924abddc91fb694cd316e3f4445b40dd52f13", + "manifest_address": "sha2-256:173e47148f01ed4dc311f1fbdb2d8daa2728272632717b8a6010af85771181e0", "pack": "joulecontract-conformance/v1" } \ No newline at end of file diff --git a/joulecontract/conformance/v1/negative-metered_unattested.json b/joulecontract/conformance/v1/negative-metered_unattested.json index 956017c78..aa53c0b86 100644 --- a/joulecontract/conformance/v1/negative-metered_unattested.json +++ b/joulecontract/conformance/v1/negative-metered_unattested.json @@ -1,12 +1,13 @@ { - "description": "Metered tag with no meter attestation: Energy class demotes to ModelBased; the Metered claim is illegal.", + "description": "Metered tag with no meter attestation and no metered-baseline anchor: an unbound reading is no reading, so the Energy class demotes to Unaccounted; the Metered claim is illegal.", "expected_composed": { - "claim": "⟨JR-3 · ModelBased · certified⟩ — demotions: metered_unattested", + "claim": "⟨JR-3 · Unaccounted · certified⟩ — demotions: metered_unattested; unaccounted", "demotions": [ - "metered_unattested" + "metered_unattested", + "unaccounted" ], "max_profile": { - "energy": "ModelBased", + "energy": "Unaccounted", "governance": "certified", "rigor": "JR-3" }, diff --git a/joulecontract/joulecontract-rs/crates/joulecontract-conformance/src/bin/gen_vectors.rs b/joulecontract/joulecontract-rs/crates/joulecontract-conformance/src/bin/gen_vectors.rs index af9f442c9..009decf8e 100644 --- a/joulecontract/joulecontract-rs/crates/joulecontract-conformance/src/bin/gen_vectors.rs +++ b/joulecontract/joulecontract-rs/crates/joulecontract-conformance/src/bin/gen_vectors.rs @@ -138,7 +138,7 @@ fn main() { let negatives: Vec<(&str, &str, Mutation)> = vec![ ( "metered_unattested", - "Metered tag with no meter attestation: Energy class demotes to ModelBased; the Metered claim is illegal.", + "Metered tag with no meter attestation and no metered-baseline anchor: an unbound reading is no reading, so the Energy class demotes to Unaccounted; the Metered claim is illegal.", Box::new(|r: &mut Receipt| r.meter = None), ), ( diff --git a/joulecontract/joulecontract-rs/crates/joulecontract-receipt/src/lib.rs b/joulecontract/joulecontract-rs/crates/joulecontract-receipt/src/lib.rs index 955cac48d..15d9d02b6 100644 --- a/joulecontract/joulecontract-rs/crates/joulecontract-receipt/src/lib.rs +++ b/joulecontract/joulecontract-rs/crates/joulecontract-receipt/src/lib.rs @@ -313,6 +313,21 @@ pub struct Verdict { pub max_profile: Profile, } +/// The Energy class a `Metered` tag falls to when its meter attestation +/// does not bind: the class the receipt's remaining evidence supports. +/// `ModelBased` is a figure anchored to a metered baseline, so it needs +/// the sealed anchor; with none, the figure is `Unaccounted`. +fn metered_unattested_class(receipt: &Receipt, demotions: &mut Vec) -> EnergyClass { + if receipt.energy_anchor.is_some() { + EnergyClass::ModelBased + } else { + if !demotions.contains(&Demotion::Unaccounted) { + demotions.push(Demotion::Unaccounted); + } + EnergyClass::Unaccounted + } +} + /// The exact §15 token for a demoted state — the normative claim vocabulary. /// (Free-text reasons never enter the token list.) pub fn demotion_token(d: &Demotion) -> &'static str { @@ -554,8 +569,12 @@ fn local_facts(contract: &Contract, receipt: &Receipt) -> Result { @@ -693,6 +712,7 @@ pub fn validate_sealed( f.generator_attested = false; } } + let mut meter_unresolved = false; if let Some(m) = &receipt.meter { let mut m_ok = true; resolve( @@ -700,9 +720,7 @@ pub fn validate_sealed( &[Demotion::MeteredUnattested], &mut m_ok, ); - if !m_ok && f.max_energy == EnergyClass::Metered { - f.max_energy = EnergyClass::ModelBased; - } + meter_unresolved = !m_ok; } if let Some(d) = &contract.ceiling.derivation { resolve( @@ -714,13 +732,20 @@ pub fn validate_sealed( // The EnB object itself is sealed evidence (SPEC §4.3, §5.1.3): a ceiling // whose baseline cannot be resolved is unanchored. resolve(&receipt.enb_ref, &[Demotion::CeilingUnanchored], &mut ok); - if let Some(anchor) = &receipt.energy_anchor { + let anchor_resolved = receipt.energy_anchor.as_ref().map(|anchor| { let mut a_ok = true; resolve(anchor, &[], &mut a_ok); - if !a_ok && f.max_energy == EnergyClass::ModelBased { - f.demotions.push(Demotion::Unaccounted); - f.max_energy = EnergyClass::Unaccounted; - } + a_ok + }); + // A `Metered` tag whose meter attestation does not resolve falls to the + // class its remaining evidence supports; then a `ModelBased` figure whose + // anchor does not resolve falls to `Unaccounted`. + if meter_unresolved && f.max_energy == EnergyClass::Metered { + f.max_energy = metered_unattested_class(receipt, &mut f.demotions); + } + if anchor_resolved == Some(false) && f.max_energy == EnergyClass::ModelBased { + f.demotions.push(Demotion::Unaccounted); + f.max_energy = EnergyClass::Unaccounted; } if evidence_declared && !evidence_sealed { @@ -1152,6 +1177,28 @@ mod tests { } let v = validate(&c, &r).unwrap(); assert!(v.demotions.contains(&Demotion::MeteredUnattested)); + // No metered-baseline anchor is sealed, so nothing supports a model. + assert!(v.demotions.contains(&Demotion::Unaccounted)); + assert_eq!(v.max_profile.energy, EnergyClass::Unaccounted); + } + + /// An unbound `Metered` tag falls to `ModelBased` only where the receipt + /// seals the metered-baseline anchor that class is defined by. + #[test] + fn an_unattested_metered_tag_is_model_based_only_with_its_anchor() { + let c = contract(); + let mut r = full_receipt(&c); + r.meter = None; + r.energy_anchor = None; + let v = validate(&c, &r).unwrap(); + assert!(v.demotions.contains(&Demotion::MeteredUnattested)); + assert!(v.demotions.contains(&Demotion::Unaccounted)); + assert_eq!(v.max_profile.energy, EnergyClass::Unaccounted); + + r.energy_anchor = Some(ContentAddress::of_bytes(b"metered baseline for a comparable workload")); + let v = validate(&c, &r).unwrap(); + assert!(v.demotions.contains(&Demotion::MeteredUnattested)); + assert!(!v.demotions.contains(&Demotion::Unaccounted)); assert_eq!(v.max_profile.energy, EnergyClass::ModelBased); } -- 2.54.0 (Apple Git-157) From 24ba03db5537ea481fc50cf9a1b1ef617c4e6f7c Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sun, 11 Oct 2026 22:57:23 -0400 Subject: [PATCH 2/2] wai: ModelBased means a model calibrated on the host it describes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The ModelBased class was defined as "a calibrated per-operation model (e.g. wall time × a power constant)", and the example licensed any constant. The family's metering ladder grades only a host-calibrated model ModelBased; a nominal TDP or typical draw is an estimate however it is multiplied. The definition in energy_class.rs and the energy extension's class table now say so. No conformance vector carries the definition, and none changes. Co-Authored-By: Claude Opus 5.5 --- wai/extensions/energy-measurement.md | 2 +- wai/wai-rs/src/energy_class.rs | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/wai/extensions/energy-measurement.md b/wai/extensions/energy-measurement.md index 9f8f7a156..1e826e4a2 100644 --- a/wai/extensions/energy-measurement.md +++ b/wai/extensions/energy-measurement.md @@ -117,7 +117,7 @@ only where §1 says it does. |---|---|---| | `CalibratedInstrument` | Read from an instrument external to the measured device — a shunt, a power analyser, a metering socket — that holds a current calibration covering the range and conditions it was used in. | a present, non-zero measurement; a declared uncertainty (§2.3); a calibration reference (§2.5) | | `OnChipCounter` | Read from an energy counter the measured silicon keeps about itself — RAPL, NVML, SMC, IOReport (§2.9) — or from any other instrument whose uncertainty is not traceable to a current calibration (§2.2). | a present, non-zero measurement; a declared uncertainty (§2.3); the counter's filtering state (§2.4) | -| `ModelBased` | Computed from a calibrated per-operation model (e.g. wall time × a power constant). A real number, honestly labelled as derived. | — | +| `ModelBased` | Computed from a model calibrated on the host it describes (e.g. wall time × an active power measured on that host). A real number, honestly labelled as derived. A constant nobody calibrated there — a nominal TDP, a typical draw — is `Estimator`, however it is multiplied. | — | | `Estimator` | A coarse constant or load estimator. | — | | `HwShunt` *(legacy)* | Read from a hardware energy interface, sub-class unspecified, no uncertainty declared. Accepted in receipts sealed before the hardware class was refined; never emitted (§2.6). | a present, non-zero measurement | diff --git a/wai/wai-rs/src/energy_class.rs b/wai/wai-rs/src/energy_class.rs index e8a160930..8d3037404 100644 --- a/wai/wai-rs/src/energy_class.rs +++ b/wai/wai-rs/src/energy_class.rs @@ -240,8 +240,11 @@ pub enum EnergyProvenance { HwShunt is only for reading receipts sealed before the split" )] HwShunt, - /// Computed from a calibrated per-operation model (e.g. wall time × a power - /// constant). A real number, honestly labelled as derived. + /// Computed from a model calibrated on the host it describes (e.g. wall + /// time × an active power measured on that host). A real number, honestly + /// labelled as derived. A constant nobody calibrated there — a nominal + /// TDP, a typical draw — is an [`EnergyProvenance::Estimator`], however it is + /// multiplied. ModelBased, /// A coarse constant or load estimator. Estimator, -- 2.54.0 (Apple Git-157)