diff --git a/.github/workflows/wai-formal-verification.yml b/.github/workflows/wai-formal-verification.yml new file mode 100644 index 000000000..78f96b789 --- /dev/null +++ b/.github/workflows/wai-formal-verification.yml @@ -0,0 +1,92 @@ +name: wai formal verification (integer core) + +# The other half of the determinism contract. +# +# `wai-byte-equality` establishes byte-exactness by SAMPLING: it decodes fixed +# vectors on five real OS/arch combinations and asserts identical bytes. That +# proves the paths agree on the inputs someone thought to write down. +# +# This job REASONS instead. It runs a model checker (Kani/CBMC) over the same +# sources, for every input in a bounded window, and discharges the property the +# byte-exactness claim actually rests on: arithmetic totality. Rust integer +# overflow panics in debug and wraps in release, so an overflowing decoder is +# not one implementation but two, and which one a sink runs depends on how it +# was compiled. A decoder proved free of overflow, out-of-bounds access and +# non-termination is a decoder whose bitstream means exactly one thing. +# +# This is not redundant with the matrix: the matrix decodes WELL-FORMED vectors, +# so it cannot see defects that only a malformed or adversarial stream reaches. +# Four such defects in the bypass escape were found here and fixed, and the +# harnesses stand so they cannot come back. +# +# The proofs are bounded (small symbolic CDFs, fixed-length symbolic streams, +# explicit unwind limits). Bounded is not universal, and the job claims only +# what it checks. + +on: + pull_request: + paths: + - 'wai/wai-verify/**' + # The verified source itself must be able to fire this job, or a change + # can regress totality and merge green. + - 'wai/wai-rs/src/rans.rs' + - 'wai/wai-rs/src/int_entropy.rs' + - 'wai/wai-rs/src/int_transform.rs' + - 'wai/wai-rs/src/wai_video_policy.rs' + - '.github/workflows/wai-formal-verification.yml' + push: + branches: + - main + paths: + - 'wai/wai-verify/**' + - 'wai/wai-rs/src/rans.rs' + - 'wai/wai-rs/src/int_entropy.rs' + - 'wai/wai-rs/src/int_transform.rs' + - 'wai/wai-rs/src/wai_video_policy.rs' + - '.github/workflows/wai-formal-verification.yml' + +jobs: + kani: + runs-on: linux + steps: + - uses: actions/checkout@v4 + + # dtolnay/rust-toolchain cannot help — it calls `rustup`, which is absent + # on this runner image. + - name: Install rustup + toolchain + run: | + set -euo pipefail + if ! command -v rustup >/dev/null; then + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \ + | sh -s -- -y --profile minimal --default-toolchain 1.98.0 + fi + echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" + + # Kani ships its own pinned nightly and a CBMC build; both are slow to + # fetch, so they are cached on the verifier version. + - name: Cache Kani toolchain + uses: actions/cache@v4 + with: + path: | + ~/.cargo/bin/kani + ~/.cargo/bin/cargo-kani + ~/.kani + key: kani-0.67.0-${{ runner.os }} + + - name: Install Kani + run: | + set -euo pipefail + export PATH="$HOME/.cargo/bin:$PATH" + command -v cargo-kani >/dev/null || cargo install --locked kani-verifier --version 0.67.0 + # Idempotent; fetches the pinned nightly + CBMC on a cold cache. + cargo kani setup + + - name: Verify the integer core + working-directory: wai/wai-verify + run: | + set -euo pipefail + export PATH="$HOME/.cargo/bin:$PATH" + # Every harness must verify. A failing harness is a real finding + # about the decoder, so this job is allowed to be the thing that + # blocks the merge. + cargo kani diff --git a/wai/SPEC.md b/wai/SPEC.md index e44dc8b9b..f7252bbef 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -211,6 +211,11 @@ decode route for each is implemented in the reference sink (see the | `wai.neural.dcvc_fm` | DCVC-FM (feature modulation), wide single-model quality range (RGB + YUV) | SOTA-RD neural video; shares the inter-frame route | research code, `neural/video_dcvc.rs` | | `wai.video.int_motion` | DETERMINISTIC INTEGER inter-frame — I-frame + integer block motion-compensated P-frames + integer-quantized residual over rANS, no float/ONNX; motion is whole-pel or **half-pel** (`mv_precision`), the latter predicting at the half-grid by integer bilinear interpolation (`(a+b+1)>>1`, `(a+b+c+d+2)>>2`) so real footage — which pans a non-integer number of pixels per frame — costs fewer residual bits while staying byte-exact | byte-identical frame-by-frame on every machine (*frame-state-equivalence*, a per-frame portable hash); the temporal extension of the integer contract, where a float inter-frame decode desyncs down the GOP | `int_video.rs` (whole-pel `tools/wai_int_video_encode.py`; half-pel from real footage `tools/wai_int_video_real_encode.py`) | | `wai.video.int_hyper` | NEURAL-KEYFRAME inter-frame — the I-frame is the LEARNED integer codec `int_hyper` decoded byte-exact, the P-frames are integer block-MC residuals on top | a learned keyframe you can put in a receipt + integer inter-frames; whole decode integer, byte-identical everywhere | `int_video::decode_pframes` ∘ `int_hyper_synth::decode_conditional` | +| `wai.video.manifest` | ATTESTED PER-SESSION MANIFEST — the OTT delivery layer, not a codec: a personalised HLS manifest (ads stitched at `EXT-X-DISCONTINUITY`, blackouts + geo enforced) rendered as a **pure function of the session *class*** `(content, entitlement, geo, blackout set, ad pod, window)` rather than the viewer, and sealed in an Ed25519 receipt that binds the JCP grant (capability, joule ceiling, `funds_ceiling` = ad budget), the composition, the stitched ads and the policy applied | **manifest-equivalence**: `manifest_hash == hash(render(segments))` and `session_class_hash` are recomputable by anyone holding the bytes, so the ads, blackouts and compose-work stop being dashboard claims; class-determinism means one generation serves every viewer of the class, and `uj_per_viewer` is the amortised energy that a 1:1-unique generator cannot report below its per-viewer cost. Only `joules_micro` is measured-attested | `wai_video_manifest.rs` | +| `wai.video.ssai` | ATTESTED SERVER-SIDE AD INSERTION — a **deterministic** ad decision (greedy by price within the avail duration and the funds remaining) plus a per-impression Ed25519 receipt binding the candidate pod, the manifest it belongs to, the served `creative_hash`es and the VAST quartile each reached | **spend-equivalence**: `budget_spent_micros` is recomputed from the *billable* impressions and rejected if it exceeds the grant's `funds_ceiling` — overspend cannot be signed; every creative and quartile is checkable, so a buyer and seller reconcile impressions from the same bytes instead of two logs that only a dashboard joins. Only `joules_micro` is measured-attested | `wai_video_ssai.rs` | +| `wai.video.keys` | ATTESTED CONTENT-KEY RELEASE — the DRM licensing decision as a record: every key release, and every refusal, is an Ed25519 receipt binding the KID, the DRM system, the entitlement demanded and the window enforced, with a BLAKE3 `key_commit` proving *which* key was released without carrying it | **decision-equivalence**: `verify()` re-runs the release policy over the receipt's own `(grant capability, entitlement, issued, expiry)` and rejects any misreported outcome, and enforces granted-iff-committed — so "keys went only to entitled, unexpired sessions" is checkable against the signed log, not asserted. Only `joules_micro` is measured-attested | `wai_video_keys.rs` | +| `wai.video.package` | DETERMINISTIC PACKAGING + ATTESTED SEGMENTMAP — a source sliced into content-hashed segments on GOP boundaries; the ordered `(index → content_hash)` map is a signed Merkle commitment, and identical content (ads, bumpers, replays, simulcast overlap) dedups to one stored/encoded copy | **map-equivalence + verifiable dedup**: `segment_map_root` lets a `wai.video.manifest` reference be checked against the package that produced it, and `verify()` recomputes `unique_segments`/`stored_bytes` from the segments so the storage/encode saving cannot be overstated; `uj_per_unique_segment` is the encode-once energy. Only `joules_micro` is measured-attested | `wai_video_package.rs` | +| `wai.video.channel` | VIRTUAL LINEAR / FAST ASSEMBLY — a continuous schedule of assets over wall-clock time, sliced into attested playback windows; windows chain via `parent_receipt_hash`, so a channel's history is a hash chain of program-as-run records | **schedule-continuity + recomputable program-as-run**: `verify()` rejects a schedule with a gap or overlap (no dead air, no double-booking) and recomputes `aired` from the schedule and the window, so what actually aired is checkable by a licensor, advertiser or regulator against the signed chain rather than an operator-held play-out log. Only `joules_micro` is measured-attested | `wai_video_channel.rs` | **Sink-architecture note:** the inter-frame neural video codecs (DCVC-RT, DCVC-FM) decode through `ort` and are **CPU-capable** for native sinks — @@ -504,6 +509,49 @@ learned-codec standards make and the floor for a sound neural `replicate`; and rendered result has a portable hash, the tier WAI adds on top and the precondition for a hard [reconstruction binding](extensions/reconstruction-binding.md). +### Machine-checked totality (informative) + +The cross-architecture matrix establishes byte-exactness by **sampling**: it +decodes fixed vectors on five real OS/arch combinations. `wai-verify/` supplies +the complementary half by **reasoning** — a model checker (Kani/CBMC) over the +same `#[path]`-included sources, for every input in a bounded window. + +What it discharges is the property the byte-exactness claim rests on: +**arithmetic totality**. Rust integer overflow *panics in debug and wraps in +release*, so an overflowing decoder is not one implementation but two, and which +one a sink runs depends on how it was compiled. A decode proved free of +overflow, out-of-bounds access and non-termination is a decode whose bitstream +denotes exactly one symbol sequence. + +`matmul`'s accumulation is total for fixed-point operands of realistic magnitude (±2^31 at Q16). This one is a *conditional* result and is stated as such: the product is formed in i128 then truncated to i64 and accumulated with a plain `+=`, which genuinely does overflow for large enough operands. Nothing in the signature constrains magnitude, so callers inherited that safe-operating range silently; the harness turns it into a written, checked precondition rather than reporting an unstated contract as a defect. + +Currently proved for the integer transformer kernels (`int_transform`): `softmax` is total over the whole fixed-point path (ln2 reduction, i128 polynomial, shift, division) and its output **sums to exactly `2^PROB_FRAC`** with no negative probability — the normalisation the entropy stage depends on, since a denormalised distribution becomes a denormalised CDF. The checker also shows the degenerate uniform fallback to be *unreachable*; that branch would violate the same invariant if it ever fired, so the property currently holds by unreachability rather than by construction, and the code says so at the site. + +Currently proved for the scale→bucket primitive (`int_entropy`): `det_build_index` always returns an index addressing a real scale-table entry, and is **monotone in σ** — a larger σ never selects a smaller bucket. The monotonicity is proved for an *arbitrary* edge table rather than only an ascending one, so it does not rest on a precondition a caller might not maintain; it is the property the bucketing exists to guarantee, and a non-monotone bucketing would mis-order the table without ever panicking. + +Currently proved for the integer rANS coder: `RansDecoder::new` is total for +every input slice; `decode_categorical` is total and returns an in-alphabet +symbol for all admissible CDFs and all streams in the window; and `decode`'s +bypass escape is total. Each harness carries a `kani::cover` obligation, so a +proof cannot pass vacuously on assumptions that admit no state. + +This is not redundant with the matrix. The matrix decodes *well-formed* vectors +and therefore cannot see defects only a malformed stream reaches; four such +defects in the bypass escape — a stream-controlled shift distance, two +saturating-arithmetic gaps, an unbounded read — were found this way and fixed, +with the conformance vectors confirming the fix changed nothing a conforming +encoder can produce. + +The `wai.video.ssai` decision policy is **test-backed, not proof-backed**: the natural theorem — that `decide` never proposes a fill exceeding the funds, the avail duration or the slot count — did not close (three configurations, up to 900s each). The obstacle is that the decision sorts on a heap-allocated key, so the model carries `memcmp` and the allocator machinery rather than the budget arithmetic. Stubbing that away would prove a property of the stub. What *is* proved there is narrower: a fresh decision bills nothing until its beacons arrive, so a fill cannot be mistaken for delivery. + +`layernorm` closes only at ±2^10 — *below* realistic Q16 activation magnitude (at ±2^20 it did not close in 25 minutes). Its guarded divide and surrounding arithmetic are therefore established for small operands only, not over the kernel's working range. The obstacle is `isqrt` over a symbolic u128, which is a limit of bounded model checking rather than a property of the code. `attention`, `linear`, `igdn` and the composed `TransformerBlock` are **not covered at all**. The technique does not reach everything, and this section records where it stops rather than listing only what it reached. + +**Scope, stated plainly:** these are *bounded* proofs — small symbolic CDFs, +fixed-length symbolic streams, explicit unwind limits — not universal ones, and +they cover the stream-controlled paths rather than the whole crate. A CDF +supplied by internal tables is still assumed well-formed. The verification +claims what it checks and no more. + --- ## 7.1. Multi-rendition envelope (v1.1 extension) diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index f3afd9442..9a9b5afb1 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -26,8 +26,7 @@ serde_json = { version = "1", features = ["preserve_order"] } # --features world and none of the C codec chain. Registration (the # capability strings in codecs/mod.rs) is NOT gated — only the decoders. # Image -image = { version = "0.25", default-features = false, - features = ["png", "jpeg", "webp", "avif"], optional = true } # PNG, JPEG decode, AVIF encode (via ravif) +image = { version = "0.25", default-features = false, features = ["png", "jpeg", "webp", "avif"], optional = true } # PNG, JPEG decode, AVIF encode (via ravif) jpeg-encoder = { version = "0.7", optional = true } # pure-Rust JPEG with optimized Huffman tables libavif-image = { version = "0.14", optional = true } # AVIF decode via system libavif (fixes silent-empty decode bug) jpegxl-rs = { version = "0.14", optional = true } # libjxl bindings (links system libjxl; 0.11.x and 0.12.x both work) @@ -52,9 +51,7 @@ byteorder = { version = "1", optional = true } # browser-side wai-web demo uses, so models built with our exporters # load identically here. The `download-binaries` feature fetches the # right libonnxruntime build at compile time; no manual brew install. -ort = { version = "2.0.0-rc.12", default-features = false, - features = ["std", "download-binaries", "ndarray", "tls-rustls"], - optional = true } +ort = { version = "2.0.0-rc.12", default-features = false, features = ["std", "download-binaries", "ndarray", "tls-rustls"], optional = true } ndarray = { version = "0.17", optional = true } zstd-safe = { version = "7", optional = true, features = ["std"] } # for bmshj2018 latent unpack (std → WriteBuf for Vec) sha2 = { version = "0.10", optional = true } # verify a pinned neural prior against the registered model artifact @@ -189,6 +186,34 @@ quantum_receipt = ["quantum", "wai-quantum/quantum_receipt"] # crate, and that crate must keep its three-dependency set to stay runnable on # every leg of the cross-arch matrix. video_receipt = ["video_int", "world"] +# wai.video.manifest — attested, deduplicating, energy-accounted per-session +# manifest. Reuses the world Merkle + Ed25519 and the JCP GrantRef (quantum_ops); +# carries no pixel-decode dependency, so it stays a light, pure-Rust surface. +# Depends on `world` EXPLICITLY: these receipts use +# `crate::world::receipt::merkle_root`. That used to arrive transitively via +# `quantum_ops`, which no longer provides it now the quantum stack lives in +# its own crate — a dependency this feature always had and never declared. +video_manifest = ["quantum_ops", "world"] +# Energy meters — the source of a receipt's joules_micro. Reuses the +# EnergyProvenance ladder; hardware counter vs calibrated model, mechanically. +energy_meter = ["video_manifest"] +# wai.video.ssai — attested ad decisioning + per-impression receipt. Reuses the +# manifest module's EnergyProvenance + the GrantRef/Merkle/Ed25519 floor. +# Pure decision policy (no deps) — separable so it can be model-checked. +video_policy = [] +video_ssai = ["video_manifest", "video_policy"] +# wai.video.keys — attested content-key release; the DRM audit trail as a +# recomputable decision. Reuses the manifest floor (EnergyProvenance, GrantRef, +# Ed25519). +video_keys = ["video_manifest"] +# wai.video.package — deterministic segmentation + attested, deduplicating +# SegmentMap. Reuses the manifest floor (EnergyProvenance, GrantRef, Merkle). +video_package = ["video_manifest"] +# wai.video.channel — virtual linear / FAST assembly; the program-as-run hash +# chain. Reuses the manifest floor (EnergyProvenance, GrantRef, Merkle). +video_channel = ["video_manifest"] +# The whole OTT workflow suite in one switch. +video_workflow = ["video_manifest", "video_ssai", "video_keys", "video_package", "video_channel"] # Balanced-ternary matrix-product-state transform (`wai.ternary.tt`, # extensions/ternary-tt): quantum-INSPIRED (tensor-network) compression whose # novel delta is an INTEGER core scale — the whole decode is pure i64/i128, so a diff --git a/wai/wai-rs/src/energy_meter.rs b/wai/wai-rs/src/energy_meter.rs new file mode 100644 index 000000000..b433e7a8e --- /dev/null +++ b/wai/wai-rs/src/energy_meter.rs @@ -0,0 +1,229 @@ +//! Energy meters — where a receipt's `joules_micro` actually comes from. +//! +//! Every receipt class in WAI seals a joule figure *beside its acquisition +//! class*, and rejects the two out of step: an unlabelled non-zero figure is +//! uncomparable, a labelled zero claims a measurement that did not happen. That +//! discipline is only as good as the thing producing the number, so this module +//! makes the ladder **mechanical rather than conventional**: +//! +//! - A [`CounterMeter`] reads a real hardware energy counter and is the only +//! meter here that can ever yield [`EnergyProvenance::HwShunt`]. +//! - A [`ModelMeter`] multiplies elapsed time by a calibrated power figure and +//! can only ever yield [`EnergyProvenance::ModelBased`] — it has no way to +//! claim a measurement. +//! - When a meter cannot measure — no hardware, no counter, no span started — +//! [`Meter::stop`] returns `None`. It never falls back to a fabricated figure, +//! because a plausible number with the wrong label is worse than no number: +//! the caller then either meters with a model and says so, or seals unmetered +//! (`0` / `None`), which the receipts already accept. +//! +//! Both meters take their source injected — a counter reader, a clock — so the +//! delta and wraparound arithmetic is testable without hardware, and so the +//! module stays usable on targets with no `Instant` (wasm). The convenience +//! constructor [`CounterMeter::rapl`] wires the Linux powercap sysfs interface +//! and returns `None` anywhere it is absent. + +use crate::wai_video_manifest::EnergyProvenance; + +/// A measured span: the energy, and the class of the measurement. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct EnergyReading { + pub joules_micro: u64, + pub provenance: EnergyProvenance, +} + +impl EnergyReading { + /// The pair a receipt's `seal` wants: `(joules_micro, Some(provenance))`. + pub fn as_seal_args(self) -> (u64, Option) { + (self.joules_micro, Some(self.provenance)) + } + + /// What to seal when there was no measurement at all — `(0, None)`, the + /// only unmetered form the receipts accept. + pub fn unmetered() -> (u64, Option) { + (0, None) + } +} + +/// Something that can measure the energy of a span of work. +pub trait Meter { + /// Begin a span. Calling it again restarts the span. + fn start(&mut self); + /// End the span. `None` when this meter could not measure — never a + /// fabricated figure. + fn stop(&mut self) -> Option; + /// The class this meter is capable of claiming, whatever happens. + fn provenance(&self) -> EnergyProvenance; +} + +/// A monotonic hardware energy counter, in microjoules, that wraps at +/// `wrap_at`. The read is injected, so the delta and wraparound arithmetic is +/// exercised in tests without needing the hardware present. +pub struct CounterMeter { + read: Box Option>, + wrap_at: u64, + start: Option, +} + +impl CounterMeter { + /// `read` returns the counter's current microjoule value, or `None` when it + /// cannot be read. `wrap_at` is the counter's range (its maximum + 1). + pub fn new(read: impl FnMut() -> Option + 'static, wrap_at: u64) -> CounterMeter { + CounterMeter { read: Box::new(read), wrap_at, start: None } + } + + /// Wire the Linux powercap (RAPL) interface for a package domain. `None` + /// when the interface is absent — which is every non-Linux target, and any + /// Linux without powercap — so the caller must fall back explicitly rather + /// than silently receive a made-up figure. + pub fn rapl(domain: &str) -> Option { + let base = format!("/sys/class/powercap/{domain}"); + let energy = format!("{base}/energy_uj"); + let range = format!("{base}/max_energy_range_uj"); + // Both files must be readable now, or this meter does not exist. + let wrap_at = read_u64_file(&range)?.saturating_add(1); + read_u64_file(&energy)?; + Some(CounterMeter::new(move || read_u64_file(&energy), wrap_at)) + } +} + +fn read_u64_file(path: &str) -> Option { + std::fs::read_to_string(path).ok()?.trim().parse::().ok() +} + +impl Meter for CounterMeter { + fn start(&mut self) { + self.start = (self.read)(); + } + + fn stop(&mut self) -> Option { + let started = self.start.take()?; + let now = (self.read)()?; + // Energy counters are monotonic until they wrap at their range. + let delta = + if now >= started { now - started } else { self.wrap_at - started + now }; + Some(EnergyReading { joules_micro: delta, provenance: EnergyProvenance::HwShunt }) + } + + fn provenance(&self) -> EnergyProvenance { + EnergyProvenance::HwShunt + } +} + +/// Elapsed time multiplied by a calibrated power figure. A real number, and +/// honestly labelled as derived — it cannot claim `HwShunt` however it is +/// configured. +pub struct ModelMeter { + clock_micros: Box u64>, + milliwatts: u64, + t0: Option, +} + +impl ModelMeter { + /// `clock_micros` returns a monotonic microsecond timestamp; `milliwatts` + /// is the calibrated marginal power of the work being measured. + pub fn new(clock_micros: impl FnMut() -> u64 + 'static, milliwatts: u64) -> ModelMeter { + ModelMeter { clock_micros: Box::new(clock_micros), milliwatts, t0: None } + } + + /// A model meter driven by the process monotonic clock. + #[cfg(not(target_arch = "wasm32"))] + pub fn wall_clock(milliwatts: u64) -> ModelMeter { + let origin = std::time::Instant::now(); + ModelMeter::new(move || origin.elapsed().as_micros() as u64, milliwatts) + } +} + +impl Meter for ModelMeter { + fn start(&mut self) { + self.t0 = Some((self.clock_micros)()); + } + + fn stop(&mut self) -> Option { + let t0 = self.t0.take()?; + let dt_micros = (self.clock_micros)().saturating_sub(t0); + // uJ = mW * us / 1000 (mW*us = nJ; /1000 -> uJ) + let joules_micro = self.milliwatts.saturating_mul(dt_micros) / 1000; + Some(EnergyReading { joules_micro, provenance: EnergyProvenance::ModelBased }) + } + + fn provenance(&self) -> EnergyProvenance { + EnergyProvenance::ModelBased + } +} + +#[cfg(test)] +mod tests { + use super::*; + use std::cell::RefCell; + use std::rc::Rc; + + /// A scripted counter: successive reads return successive values. + fn scripted(values: Vec>) -> impl FnMut() -> Option { + let q = Rc::new(RefCell::new(values.into_iter())); + move || q.borrow_mut().next().flatten() + } + + #[test] + fn counter_measures_a_real_delta_as_hwshunt() { + let mut m = CounterMeter::new(scripted(vec![Some(1_000), Some(4_500)]), 1 << 32); + m.start(); + let r = m.stop().unwrap(); + assert_eq!(r.joules_micro, 3_500); + assert_eq!(r.provenance, EnergyProvenance::HwShunt); + } + + #[test] + fn counter_handles_wraparound() { + // Range 10_000 (wrap_at 10_000): 9_800 -> 200 is a 400 uJ span. + let mut m = CounterMeter::new(scripted(vec![Some(9_800), Some(200)]), 10_000); + m.start(); + assert_eq!(m.stop().unwrap().joules_micro, 400); + } + + #[test] + fn a_meter_that_cannot_read_reports_nothing_not_a_guess() { + // No hardware: the read fails. The meter must yield None so the caller + // falls back explicitly rather than sealing a fabricated HwShunt. + let mut m = CounterMeter::new(scripted(vec![None, None]), 1 << 32); + m.start(); + assert!(m.stop().is_none()); + // And a stop with no start is likewise nothing. + let mut m2 = CounterMeter::new(scripted(vec![Some(5)]), 1 << 32); + assert!(m2.stop().is_none()); + } + + #[test] + fn model_meter_is_derived_and_says_so() { + // 2000 mW over 5_000 us = 10_000 uJ. + let mut m = ModelMeter::new(scripted_clock(vec![1_000, 6_000]), 2_000); + m.start(); + let r = m.stop().unwrap(); + assert_eq!(r.joules_micro, 10_000); + assert_eq!(r.provenance, EnergyProvenance::ModelBased); + // The ladder is mechanical: this meter cannot claim a measurement. + assert_eq!(m.provenance(), EnergyProvenance::ModelBased); + } + + fn scripted_clock(values: Vec) -> impl FnMut() -> u64 { + let q = Rc::new(RefCell::new(values.into_iter())); + move || q.borrow_mut().next().unwrap_or(0) + } + + #[test] + fn seal_args_round_trip_to_the_receipt_contract() { + let r = EnergyReading { joules_micro: 42, provenance: EnergyProvenance::HwShunt }; + assert_eq!(r.as_seal_args(), (42, Some(EnergyProvenance::HwShunt))); + // The only unmetered form the receipts accept. + assert_eq!(EnergyReading::unmetered(), (0, None)); + } + + #[test] + fn rapl_is_absent_here_and_says_so_rather_than_pretending() { + // This box has no Linux powercap interface; the constructor must decline + // rather than hand back a meter that invents HwShunt figures. + if !std::path::Path::new("/sys/class/powercap/intel-rapl:0").exists() { + assert!(CounterMeter::rapl("intel-rapl:0").is_none()); + } + } +} diff --git a/wai/wai-rs/src/int_entropy.rs b/wai/wai-rs/src/int_entropy.rs index e50d0bd7f..897ea8b4d 100644 --- a/wai/wai-rs/src/int_entropy.rs +++ b/wai/wai-rs/src/int_entropy.rs @@ -77,6 +77,67 @@ pub fn det_build_index(sigma_q: i64, edges_q: &[i64]) -> usize { idx } +// ───────────────────────────────────────────────────────────────────── +// Kani proof harnesses — the soundness hinge, checked rather than asserted +// ───────────────────────────────────────────────────────────────────── +// +// SPEC §7 makes this function load-bearing: a bucket that flips selects a +// different CDF and desyncs the remainder of the stream. Two things therefore +// have to hold, and both are proved here rather than argued in prose. +// +// 1. The index addresses a real scale-table entry. An out-of-range bucket is +// either an out-of-bounds panic downstream or, worse, a silently wrong CDF. +// 2. The bucketing is *monotone* in σ. The doc comment claims "index rises +// with σ"; a non-monotone bucketing would mis-order the table without ever +// panicking, which no amount of round-trip testing on well-formed vectors +// would reliably surface. +// +// Note the second is proved for an ARBITRARY edge table, not only an ascending +// one — the property follows from counting, not from the table being sorted, so +// the proof does not depend on a precondition a caller might not maintain. + +/// The bucket always addresses a real entry of the scale table. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(6)] +fn kani_det_build_index_in_range() { + let edges: [i64; 4] = kani::any(); + let sigma: i64 = kani::any(); + let idx = det_build_index(sigma, &edges); + kani::assert(idx < edges.len(), "bucket index addresses a real scale-table entry"); + kani::cover!(true, "the bucketing is reachable"); +} + +/// **Monotonicity**: a larger σ never selects a smaller bucket. +/// +/// This is the semantic property the integer bucketing exists to guarantee. It +/// holds by counting — a larger σ satisfies `σ <= e` for no more edges than a +/// smaller one does — so it is proved without assuming the table is ascending. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(6)] +fn kani_det_build_index_is_monotone_in_sigma() { + let edges: [i64; 4] = kani::any(); + let a: i64 = kani::any(); + let b: i64 = kani::any(); + kani::assume(a <= b); + kani::assert( + det_build_index(a, &edges) <= det_build_index(b, &edges), + "a larger sigma never selects a smaller bucket", + ); + kani::cover!(true, "both bucketings are reachable"); +} + +/// The single-entry table degenerates correctly: one bucket, always index 0. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(4)] +fn kani_det_build_index_singleton_table() { + let edges: [i64; 1] = kani::any(); + let sigma: i64 = kani::any(); + kani::assert(det_build_index(sigma, &edges) == 0, "a one-entry table has one bucket"); +} + #[cfg(test)] mod tests { use super::*; diff --git a/wai/wai-rs/src/int_transform.rs b/wai/wai-rs/src/int_transform.rs index 162528259..02d881a5c 100644 --- a/wai/wai-rs/src/int_transform.rs +++ b/wai/wai-rs/src/int_transform.rs @@ -63,7 +63,23 @@ pub fn softmax(x: &[i64], frac: u32) -> Vec { let sum: i64 = exps.iter().sum(); if sum == 0 { - // numerically degenerate (all underflowed): uniform. + // UNREACHABLE, and load-bearingly so — do not make it reachable without + // fixing it. The model checker marks this branch dead (see + // `kani_softmax_sums_to_exactly_one`): the argmax element always has + // `neg = xmax - xmax = 0`, hence `q = 0`, `r = 0`, `e = c0 > 0`, so + // `exps[argmax] > 0` and `sum > 0` for every input. + // + // That matters because this line would BREAK the exact-normalisation + // contract asserted below. `n * ((1< = exps @@ -79,6 +95,66 @@ pub fn softmax(x: &[i64], frac: u32) -> Vec { probs } +// ───────────────────────────────────────────────────────────────────── +// Kani proof harnesses — the normalisation invariant, checked +// ───────────────────────────────────────────────────────────────────── +// +// `softmax` states its own contract above: the remainder is handed to the +// largest element "so the distribution sums to EXACTLY 2^PROB_FRAC". That is +// load-bearing rather than cosmetic — these probabilities become a CDF, and a +// CDF that does not normalise makes the entropy decode select the wrong +// interval and desync the rest of the stream, exactly the failure SPEC §7 is +// written to prevent. A comment is not a guarantee; this is. +// +// The logits are bounded to a range a real hyper-decoder produces. That bound +// is a genuine precondition, not a convenience: `xmax - xi` is an i64 +// subtraction, so unbounded logits can overflow it — which panics in debug and +// wraps in release, i.e. two different softmaxes depending on the build. The +// bound is stated here so the precondition is explicit rather than assumed. + +/// The distribution sums to exactly one, and no probability is negative. +/// +/// **Arity and bound are what the solver can close, and are stated rather than +/// tuned quietly.** Each element costs an i128 polynomial evaluation and an +/// i128 division; at three symbolic logits over ±2^40 the instance did not +/// close in twenty minutes of propositional reduction. This is the two-logit +/// case over ±2^20 — a real instance of the invariant, not a universal claim. +/// [`kani_softmax_singleton_is_certain`] covers the one-symbol case. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(5)] +#[kani::solver(kissat)] +fn kani_softmax_sums_to_exactly_one() { + let a: i64 = kani::any(); + let b: i64 = kani::any(); + // Logits at scale 2^frac from an integer hyper-decoder; bounded well inside + // the range where the reduction arithmetic is exact. + const LIM: i64 = 1i64 << 20; + kani::assume(a > -LIM && a < LIM); + kani::assume(b > -LIM && b < LIM); + + let p = softmax(&[a, b], PROB_FRAC); + let total: i64 = p.iter().sum(); + kani::assert(total == 1i64 << PROB_FRAC, "the distribution sums to exactly one"); + for &v in &p { + kani::assert(v >= 0, "no probability is negative"); + } + kani::cover!(true, "softmax is reachable under these bounds"); +} + +/// The degenerate single-element case: all the mass on one symbol. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(4)] +#[kani::solver(kissat)] +fn kani_softmax_singleton_is_certain() { + let a: i64 = kani::any(); + kani::assume(a > -(1i64 << 40) && a < (1i64 << 40)); + let p = softmax(&[a], PROB_FRAC); + kani::assert(p.len() == 1, "one logit yields one probability"); + kani::assert(p[0] == 1i64 << PROB_FRAC, "a lone symbol carries all the mass"); +} + /// `exp(-a)` for `a ≥ 0` (fixed-point, `frac` bits), result at `2^frac` /// (so in `[0, 2^frac]`). Same reduce-by-`ln2` + 2nd-order polynomial as /// [`softmax`]'s inner exp, factored out so the activations can share it. @@ -188,6 +264,80 @@ pub fn matmul(a: &[i64], b: &[i64], m: usize, k: usize, n: usize, shift: u32) -> c } +/// [`matmul`]'s accumulation is total for fixed-point operands of realistic +/// magnitude — and the bound is the point of the harness. +/// +/// The product is formed in i128 and then **truncated to i64**, after which the +/// accumulator is a plain `i64 +=`. That `+=` is the hazard: for unbounded +/// operands it overflows, panicking in debug and wrapping in release, i.e. two +/// different matmuls depending on the build. Nothing in the signature enforces a +/// magnitude, so the safe operating range is a precondition callers inherit +/// silently. Writing it down here makes it checkable instead. +/// +/// `±2^31` at Q16 is a real activation range: each product is at most +/// `2^62 >> 16 = 2^46`, and `k` of them accumulate well inside i64. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(4)] +#[kani::solver(kissat)] +fn kani_matmul_accumulation_is_total() { + const LIM: i64 = 1i64 << 31; + let bounded = || -> i64 { + let v: i64 = kani::any(); + kani::assume(v > -LIM && v < LIM); + v + }; + // Written out rather than looped: an assume-loop of its own would need a + // larger unwind bound than the code under test, and a harness that cannot + // unwind reports nothing about the function. + let a: [i64; 4] = [bounded(), bounded(), bounded(), bounded()]; // 2x2 + let b: [i64; 4] = [bounded(), bounded(), bounded(), bounded()]; // 2x2 + let c = matmul(&a, &b, 2, 2, 2, PROB_FRAC); + kani::assert(c.len() == 4, "the result has m*n entries"); + kani::cover!(true, "the accumulation is reachable"); +} + + +/// [`layernorm`] is total: the divide is guarded, the arithmetic stays in range. +/// +/// The division by `std` is already defended twice (`.max(1)` on the radicand +/// and again on the root), so the question is whether the surrounding +/// fixed-point arithmetic holds and whether `isqrt` over u128 is something a +/// bounded model checker can actually close. Both are worth knowing. +/// +/// `gamma`/`beta` are indexed by the length of `x` with no length check in the +/// signature, so they are supplied at matching length here — that mismatch is a +/// caller-contract violation, not a property of this function. +/// +/// **Read the bound before trusting the coverage.** This closes at ±2^10, which +/// is *below* the magnitudes a real Q16 activation carries; at ±2^20 the +/// instance did not close in 25 minutes. So this proves the guarded divide and +/// the surrounding arithmetic hold for small operands — it does not establish +/// `layernorm` over its working range, and it should not be read as doing so. +/// The obstacle is `isqrt` over a symbolic u128, a limit of bounded model +/// checking rather than a property of the code. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(4)] +#[kani::solver(kissat)] +fn kani_layernorm_is_total() { + // Deliberately small. `std = isqrt(var + eps)` over a symbolic u128 is the + // cost centre: at ±2^20 the instance did not close in 25 minutes. A tighter + // magnitude shrinks the radicand and with it the solver's search. + const LIM: i64 = 1i64 << 10; + let bounded = || -> i64 { + let v: i64 = kani::any(); + kani::assume(v > -LIM && v < LIM); + v + }; + let x = [bounded(), bounded()]; + let gamma = [bounded(), bounded()]; + let beta = [bounded(), bounded()]; + let out = layernorm(&x, PROB_FRAC, &gamma, &beta, 1); + kani::assert(out.len() == 2, "one output per input"); + kani::cover!(true, "layernorm is reachable"); +} + /// Single-head scaled dot-product attention, fully integer: /// `out = softmax(Q·Kᵀ / √d) · V`. `q`/`k`/`v` are `seq×d` row-major at `2^frac`; /// output is `seq×d` at `2^frac`. Composes [`matmul`] + [`softmax`]; every step diff --git a/wai/wai-rs/src/lib.rs b/wai/wai-rs/src/lib.rs index a4a5f51f0..0de371833 100644 --- a/wai/wai-rs/src/lib.rs +++ b/wai/wai-rs/src/lib.rs @@ -275,6 +275,60 @@ pub mod ternary_receipt; #[cfg(feature = "quantum_ops")] pub use wai_quantum::quantum_ops; +// Attested per-session manifest (wai.video.manifest): the incumbent OTT 1:1 +// manifest, made deterministic (a pure function of the session *class*, so it +// dedups across viewers), energy-accounted, and sealed in a signed receipt that +// binds the JCP grant, the stitched ads and the blackouts applied. Reuses the +// world Merkle + Ed25519 and the GrantRef from quantum_ops — no pixel decode. +#[cfg(feature = "video_manifest")] +pub mod wai_video_manifest; + +// Where a receipt's joules_micro actually comes from. Makes the provenance +// ladder mechanical: only a hardware counter can yield HwShunt, a model meter +// can only ever say ModelBased, and a meter with no hardware returns None +// rather than a fabricated figure. +#[cfg(feature = "energy_meter")] +pub mod energy_meter; + +// Attested server-side ad insertion (wai.video.ssai): a deterministic ad +// decision + per-impression signed receipt. Budget enforcement is a checkable +// fact — verify() recomputes the billable spend and rejects it over the grant's +// funds_ceiling. Links to a manifest by manifest_hash; reuses the manifest +// module's EnergyProvenance and the world Merkle + Ed25519. +// Pure decision policy for the video capabilities — no crypto, no I/O, so a +// model checker can reach it. Holds `decide` and the spend accounting, whose +// limits are proved rather than sampled; the signing layer lives in +// wai_video_ssai and re-exports these types so the public surface is unchanged. +#[cfg(feature = "video_policy")] +pub mod wai_video_policy; + +#[cfg(feature = "video_ssai")] +pub mod wai_video_ssai; + +// Attested content-key release (wai.video.keys): every DRM key release — and +// every refusal — is a signed receipt whose decision verify() recomputes from +// the bound (grant, entitlement, times), with a BLAKE3 key-commitment that +// proves which key was released without carrying it. The content-protection +// audit trail as a checkable fact. +#[cfg(feature = "video_keys")] +pub mod wai_video_keys; + +// Deterministic packaging + attested SegmentMap (wai.video.package): a source is +// sliced into content-hashed segments; the signed Merkle SegmentMap is what a +// manifest reference is checked against, and identical content (ads, bumpers, +// replays, simulcast overlap) dedups to one stored/encoded copy — a saving +// verify() recomputes rather than takes on trust. +#[cfg(feature = "video_package")] +pub mod wai_video_package; + +// Virtual linear / FAST channel assembly (wai.video.channel): the capstone. A +// continuous schedule (gapless, non-overlapping — verify() rejects dead air) +// whose program-as-run per window is recomputed, not logged. Windows chain via +// parent_receipt_hash, so a channel's history is a hash chain: operational +// accountability as a cryptographic artifact rather than an operator's log. +#[cfg(feature = "video_channel")] +pub mod wai_video_channel; + // Deterministic autonomous CALIBRATION engines (extensions/quantum-ops § Calibration): // a fixed-point qubit-device simulator + autonomous tune-up algorithms (Rabi π-pulse) // — the software capability the quantum-control vendors sell (autonomous gate tune-up), diff --git a/wai/wai-rs/src/rans.rs b/wai/wai-rs/src/rans.rs index 0536e0acc..06ace9bce 100644 --- a/wai/wai-rs/src/rans.rs +++ b/wai/wai-rs/src/rans.rs @@ -14,6 +14,10 @@ pub struct RansDecoder<'a> { words: &'a [u8], // big-byte view; we read u32 LE words at idx idx: usize, // word index (i.e., 4*idx is byte offset) state: u64, + /// Set when a renormalisation would have run past the end of the bitstream. + /// A well-formed stream never sets it. A truncated one does, and the decoder + /// then stops consuming rather than panicking the sink that fed it. + exhausted: bool, } impl<'a> RansDecoder<'a> { @@ -26,13 +30,27 @@ impl<'a> RansDecoder<'a> { } let w0 = u32::from_le_bytes(bytes[0..4].try_into().unwrap()) as u64; let w1 = u32::from_le_bytes(bytes[4..8].try_into().unwrap()) as u64; - Ok(Self { words: bytes, idx: 2, state: (w1 << 32) | w0 }) + Ok(Self { words: bytes, idx: 2, state: (w1 << 32) | w0, exhausted: false }) + } + + /// Whether the stream ran out during a renormalisation. Decoded values are + /// not meaningful past this point; a conforming stream never sets it. + pub fn is_exhausted(&self) -> bool { + self.exhausted } #[inline] fn renorm(&mut self) { if self.state < RANS64_L { let off = self.idx * 4; - let next = u32::from_le_bytes(self.words[off..off + 4].try_into().unwrap()) as u64; + // A truncated or fully-consumed stream must not panic a sink that + // was handed untrusted bytes. A conforming stream always has the + // word this branch wants, so the guard is a no-op on every + // well-formed decode. + let Some(w) = self.words.get(off..off + 4) else { + self.exhausted = true; + return; + }; + let next = u32::from_le_bytes(w.try_into().unwrap()) as u64; self.state = (self.state << 32) | next; self.idx += 1; } @@ -48,6 +66,14 @@ impl<'a> RansDecoder<'a> { /// Decode one symbol against `cdf[0..cdf_len]` with per-channel `offset`. pub fn decode(&mut self, cdf: &[i32], cdf_len: usize, offset: i32) -> i32 { + // A table shorter than two entries has no alphabet, and `cdf_len - 1` + // below would underflow; a `cdf_len` past the slice would index out of + // bounds. Both are caller-contract violations that a conforming codec + // never produces — handled here so the function is total rather than + // merely usually-safe. + if cdf_len < 2 || cdf_len > cdf.len() { + return offset; + } let max_value = (cdf_len as i32) - 2; let cum_freq = (self.state & ((1u64 << PRECISION) - 1)) as i32; // Binary search for the largest s such that cdf[s] <= cum_freq. @@ -65,22 +91,34 @@ impl<'a> RansDecoder<'a> { let mut value = s; if value == max_value { + // `raw_val` is 32 bits and each group carries BYPASS_PRECISION of + // them, so at most this many groups can contribute anything. The + // run length is read *from the stream*, so without a bound a + // malformed bitstream drives the shift distance to 32 or beyond — + // which panics in debug and masks in release, i.e. the same bytes + // decode two different ways depending on how the sink was compiled. + // A conforming encoder never emits more than MAX_BYPASS_GROUPS, so + // every clamp here is a no-op on a well-formed stream. + const MAX_BYPASS_GROUPS: u32 = 32 / BYPASS_PRECISION; let mut val = self.get_bits(BYPASS_PRECISION); let mut n_bypass = val; - while val == MAX_BYPASS_VAL { + let mut groups = 0u32; + while val == MAX_BYPASS_VAL && groups < MAX_BYPASS_GROUPS && !self.exhausted { val = self.get_bits(BYPASS_PRECISION); - n_bypass += val; + n_bypass = n_bypass.saturating_add(val); + groups += 1; } + let n_bypass = n_bypass.min(MAX_BYPASS_GROUPS); let mut raw_val: u32 = 0; for j in 0..n_bypass { let v = self.get_bits(BYPASS_PRECISION); raw_val |= v << (j * BYPASS_PRECISION); } value = (raw_val >> 1) as i32; - if (raw_val & 1) != 0 { value = -value - 1; } - else { value += max_value; } + if (raw_val & 1) != 0 { value = (-value).saturating_sub(1); } + else { value = value.saturating_add(max_value); } } - value + offset + value.saturating_add(offset) } /// Decode one symbol of a **categorical** distribution (GLC / VQ codebook): @@ -105,6 +143,149 @@ impl<'a> RansDecoder<'a> { } } +// ───────────────────────────────────────────────────────────────────── +// Kani proof harnesses — the determinism claim, checked rather than sampled +// ───────────────────────────────────────────────────────────────────── +// +// WAI's contract is that an integer decode is byte-identical on every machine. +// The cross-architecture matrix samples that on four targets with well-formed +// streams; these harnesses reason over *all* inputs in a bounded window. +// +// The property that actually carries the claim is arithmetic totality. Rust +// integer overflow **panics in debug and wraps in release**, so an overflowing +// decoder is not one implementation — it is two, and which one a sink runs +// depends on how it was compiled. Proving the arithmetic cannot overflow is +// therefore proving the bitstream means one thing. +// +// The pair below is deliberate: the same decode, once without the rANS state +// invariant and once with it, so the proof isolates exactly which precondition +// the guarantee rests on rather than asserting safety unconditionally. + +/// The rANS state invariant the encoder maintains: after seeding and after each +/// renormalisation the state is a 63-bit quantity. `RansDecoder::new` seeds from +/// caller-supplied bytes and does **not** establish it, which is what the paired +/// harnesses below make precise. +#[cfg(kani)] +const RANS64_STATE_BOUND: u64 = 1u64 << 63; + +/// A well-formed 3-symbol categorical CDF: `cdf[0] = 0`, strictly increasing, +/// `cdf[K] = 2^PRECISION`. Symbolic in the interior points, so the harness +/// reasons over every admissible table of this size rather than one example. +#[cfg(kani)] +fn any_wellformed_cdf3() -> [u32; 4] { + let a: u32 = kani::any(); + let b: u32 = kani::any(); + kani::assume(0 < a && a < b && b < (1u32 << PRECISION)); + [0, a, b, 1u32 << PRECISION] +} + +/// **With the state invariant**: the decode is total (no overflow, no +/// underflow, no out-of-bounds) and the symbol it returns is inside the +/// alphabet, for every admissible CDF and every state in range. +/// +/// This is the theorem the byte-exactness claim needs: on a stream the encoder +/// produced, the arithmetic cannot overflow, so debug and release agree and the +/// bitstream denotes exactly one symbol sequence. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(8)] +fn kani_decode_categorical_total_under_state_invariant() { + let cdf = any_wellformed_cdf3(); + let bytes: [u8; 16] = kani::any(); + let mut d = match RansDecoder::new(&bytes) { + Ok(d) => d, + Err(_) => return, + }; + // The invariant the encoder establishes and every renorm preserves. + kani::assume(d.state < RANS64_STATE_BOUND); + let s = d.decode_categorical(&cdf); + kani::assert( + (s as usize) < cdf.len() - 1, + "decoded symbol lies inside the alphabet", + ); + // Non-vacuity, checked rather than asserted. A harness whose assumptions + // admit no state, or which returns before the call, would satisfy every + // assertion trivially. This cover obligation is discharged only if the + // decode is actually reachable, so an over-strong assumption cannot + // masquerade as a proof. + kani::cover!(true, "the decode is reachable under these assumptions"); +} + +/// **Without the state invariant**: the same decode over a state seeded from +/// arbitrary bytes. `RansDecoder::new` accepts any 4-byte-aligned input, so a +/// malformed or adversarial stream can seed a state at or above 2^63, and +/// `freq * (state >> PRECISION)` is then not guaranteed to fit in u64. +/// +/// Kept as a proof harness rather than deleted: if it fails, the failure is the +/// finding — the decoder's totality depends on a precondition the constructor +/// does not enforce, which is exactly the kind of gap a four-target test matrix +/// on well-formed streams cannot see. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(8)] +fn kani_decode_categorical_total_on_arbitrary_stream() { + let cdf = any_wellformed_cdf3(); + let bytes: [u8; 16] = kani::any(); + let mut d = match RansDecoder::new(&bytes) { + Ok(d) => d, + Err(_) => return, + }; + let s = d.decode_categorical(&cdf); + kani::assert( + (s as usize) < cdf.len() - 1, + "decoded symbol lies inside the alphabet", + ); + // Non-vacuity, checked rather than asserted. A harness whose assumptions + // admit no state, or which returns before the call, would satisfy every + // assertion trivially. This cover obligation is discharged only if the + // decode is actually reachable, so an over-strong assumption cannot + // masquerade as a proof. + kani::cover!(true, "the decode is reachable under these assumptions"); +} + +/// The **bypass escape** in [`RansDecoder::decode`], over an arbitrary stream. +/// +/// When a symbol lands on `max_value` the decoder leaves the CDF and reads raw +/// 4-bit groups: a run-length `n_bypass` accumulated from the stream, then that +/// many nibbles shifted into place by `v << (j * BYPASS_PRECISION)`. Both the +/// run length and the shift distance are therefore *stream-controlled*, and the +/// loop that gathers them reads words without re-checking the buffer. +/// +/// This harness asks the verifier whether that path is total for any stream. It +/// carries no assertion of its own: Kani checks arithmetic overflow, shift +/// distance and slice bounds automatically, so whatever it reports is a +/// statement about the decoder rather than about the harness. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(20)] +fn kani_decode_bypass_escape_is_total() { + let a: i32 = kani::any(); + kani::assume(0 < a && a < (1i32 << PRECISION)); + let cdf: [i32; 3] = [0, a, 1i32 << PRECISION]; + let bytes: [u8; 64] = kani::any(); + let mut d = match RansDecoder::new(&bytes) { + Ok(d) => d, + Err(_) => return, + }; + let _ = d.decode(&cdf, cdf.len(), 0); + kani::cover!(true, "decode() returns under these assumptions"); +} + +/// `RansDecoder::new` is total: every byte slice either yields a decoder or a +/// typed error, and never panics. The constructor is the sink's first contact +/// with untrusted bytes, so its totality is load-bearing on its own. +#[cfg(kani)] +#[kani::proof] +fn kani_decoder_new_is_total() { + let bytes: [u8; 12] = kani::any(); + let n: usize = kani::any(); + kani::assume(n <= bytes.len()); + match RansDecoder::new(&bytes[..n]) { + Ok(d) => kani::assert(d.idx == 2, "a seeded decoder starts at word 2"), + Err(_) => {} + } +} + /// rANS **encoder** matching [`RansDecoder`] byte-for-byte (rans64, precision 16): /// the missing half for an entropy-coded integer codec. Symbols are buffered in /// forward order and emitted in reverse on [`flush`](Self::flush) — the LIFO diff --git a/wai/wai-rs/src/wai_video_channel.rs b/wai/wai-rs/src/wai_video_channel.rs new file mode 100644 index 000000000..9d6bd399e --- /dev/null +++ b/wai/wai-rs/src/wai_video_channel.rs @@ -0,0 +1,336 @@ +//! Virtual linear / FAST channel assembly — `wai.video.channel`. +//! +//! A linear channel is a continuous schedule of assets over wall-clock time; the +//! delivery layer turns the slice of that schedule covering a playback window +//! into a manifest. The capstone of the OTT ingest: it composes the other four +//! and turns the one thing a managed streaming operation is really selling — +//! *operational accountability* — into a cryptographic artifact. +//! +//! Two facts a broadcaster today reconstructs from logs after the fact are here +//! signed and recomputable: +//! +//! - **The schedule is a real continuous channel.** [`ChannelReceipt::verify`] +//! rejects a schedule with a gap or an overlap — a linear channel airs with no +//! dead air and no double-booking, and the receipt will not sign one that +//! does. +//! - **The program-as-run is checkable.** `aired` — which entries were on air in +//! the attested window — is recomputed from the schedule and the window, so a +//! licensor, an advertiser or a regulator confirms what actually aired against +//! the signed record rather than a play-out log only the operator holds. +//! +//! Windows chain via `parent_receipt_hash`, so a channel's history is a hash +//! chain of program-as-run windows — the StreamOps audit trail. Each window's +//! manifest is still a `wai.video.manifest`, so the per-class dedup carries +//! through: one generation per window per class, not per viewer. Only +//! `joules_micro` is measured-attested. Reuses the manifest floor. + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; + +use crate::quantum_ops::GrantRef; +use crate::wai_video_manifest::EnergyProvenance; +use crate::world::receipt::merkle_root; + +const DOMAIN_RECEIPT: &[u8] = b"wai:video-channel-receipt\x01"; +const DOMAIN_RECEIPT_ID: &[u8] = b"wai:video-channel-receipt-id\x01"; +const DOMAIN_ENTRY: &[u8] = b"wai:video-channel-entry\x01"; + +/// What a scheduled slot carries. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum EntryKind { + Program, + Ad, + Filler, +} + +impl EntryKind { + fn tag(self) -> u8 { + match self { + EntryKind::Program => 1, + EntryKind::Ad => 2, + EntryKind::Filler => 3, + } + } +} + +/// One slot in the channel schedule. `start_ms` is an epoch in milliseconds so +/// it shares units with `duration_ms`; the slot occupies `[start_ms, end)`. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct ScheduleEntry { + pub asset_id: String, + pub start_ms: u64, + pub duration_ms: u64, + pub kind: EntryKind, +} + +impl ScheduleEntry { + pub fn end_ms(&self) -> u64 { + self.start_ms + self.duration_ms + } + fn leaf(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_ENTRY); + h.update(&(self.asset_id.len() as u32).to_be_bytes()); + h.update(self.asset_id.as_bytes()); + h.update(&self.start_ms.to_be_bytes()); + h.update(&self.duration_ms.to_be_bytes()); + h.update(&[self.kind.tag()]); + *h.finalize().as_bytes() + } +} + +/// Whether a schedule is a valid continuous channel: ordered, gapless and +/// non-overlapping — each entry begins exactly where the previous one ended. +pub fn is_continuous(schedule: &[ScheduleEntry]) -> bool { + schedule.windows(2).all(|w| w[0].end_ms() == w[1].start_ms) +} + +/// The schedule entry on air at `now_ms`, and the offset into it. Deterministic; +/// `None` before the schedule starts or after it ends. +pub fn entry_at(schedule: &[ScheduleEntry], now_ms: u64) -> Option<(usize, u64)> { + schedule + .iter() + .position(|e| now_ms >= e.start_ms && now_ms < e.end_ms()) + .map(|i| (i, now_ms - schedule[i].start_ms)) +} + +/// The indices on air at any point in the half-open window `[start, end)` — +/// the program-as-run for that window. An entry aired if it overlaps the window. +fn aired_in(schedule: &[ScheduleEntry], window_start_ms: u64, window_end_ms: u64) -> Vec { + schedule + .iter() + .enumerate() + .filter(|(_, e)| e.start_ms < window_end_ms && e.end_ms() > window_start_ms) + .map(|(i, _)| i as u64) + .collect() +} + +/// A signed program-as-run window of a linear channel. +#[derive(Clone, Debug, PartialEq)] +pub struct ChannelReceipt { + pub channel_id: String, + /// Merkle commitment over the schedule entries — the program identity. + pub schedule_root: [u8; 32], + pub schedule: Vec, + pub window_start_ms: u64, + pub window_end_ms: u64, + /// Schedule indices on air in the window — recomputed in verify(). + pub aired: Vec, + pub work_schedule_ops: u64, + pub joules_micro: u64, + pub energy_provenance: Option, + pub grant: GrantRef, + /// The prior window's receipt — the channel history is this hash chain. + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +impl ChannelReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&(self.channel_id.len() as u32).to_be_bytes()); + o.extend_from_slice(self.channel_id.as_bytes()); + o.extend_from_slice(&self.schedule_root); + o.extend_from_slice(&self.window_start_ms.to_be_bytes()); + o.extend_from_slice(&self.window_end_ms.to_be_bytes()); + o.extend_from_slice(&self.work_schedule_ops.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, EnergyProvenance::tag_byte)); + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&(self.aired.len() as u64).to_be_bytes()); + for a in &self.aired { + o.extend_from_slice(&a.to_be_bytes()); + } + o.extend_from_slice(&(self.schedule.len() as u64).to_be_bytes()); + for e in &self.schedule { + o.extend_from_slice(&e.leaf()); + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Seal a program-as-run window. `aired` is computed here from the schedule + /// and the window, so it cannot claim a program that did not air. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + channel_id: impl Into, + schedule: Vec, + window_start_ms: u64, + window_end_ms: u64, + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> ChannelReceipt { + let leaves: Vec<[u8; 32]> = schedule.iter().map(ScheduleEntry::leaf).collect(); + let aired = aired_in(&schedule, window_start_ms, window_end_ms); + let mut r = ChannelReceipt { + channel_id: channel_id.into(), + schedule_root: merkle_root(&leaves), + work_schedule_ops: schedule.len() as u64, + schedule, + window_start_ms, + window_end_ms, + aired, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + program integrity: the schedule must be a valid continuous + /// channel (ordered, gapless, non-overlapping), the Merkle root and work + /// figure must follow from it, the window must be non-empty, `aired` must be + /// exactly what the schedule and window produce, and the energy figure and + /// its label stand or fall together. + pub fn verify(&self) -> bool { + let leaves: Vec<[u8; 32]> = self.schedule.iter().map(ScheduleEntry::leaf).collect(); + if merkle_root(&leaves) != self.schedule_root { + return false; + } + if self.work_schedule_ops != self.schedule.len() as u64 { + return false; + } + if self.window_start_ms >= self.window_end_ms { + return false; + } + if !is_continuous(&self.schedule) { + return false; + } + if aired_in(&self.schedule, self.window_start_ms, self.window_end_ms) != self.aired { + return false; + } + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// The program-as-run: the schedule entries on air in this window. + pub fn aired_entries(&self) -> Vec<&ScheduleEntry> { + self.aired.iter().filter_map(|&i| self.schedule.get(i as usize)).collect() + } + + /// Microjoules of assembly energy per aired entry in the window, with its + /// acquisition class. `None` when unmetered or nothing aired. + pub fn uj_per_aired(&self) -> Option<(f64, EnergyProvenance)> { + let n = self.aired.len() as u64; + match (self.energy_provenance, n) { + (Some(p), a) if self.joules_micro > 0 && a > 0 => { + Some((self.joules_micro as f64 / a as f64, p)) + } + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + // A gapless channel: show A [0,10s), ad [10s,12s), show B [12s,22s). + fn schedule() -> Vec { + vec![ + ScheduleEntry { asset_id: "show-A".into(), start_ms: 0, duration_ms: 10_000, kind: EntryKind::Program }, + ScheduleEntry { asset_id: "ad-1".into(), start_ms: 10_000, duration_ms: 2_000, kind: EntryKind::Ad }, + ScheduleEntry { asset_id: "show-B".into(), start_ms: 12_000, duration_ms: 10_000, kind: EntryKind::Program }, + ] + } + + #[test] + fn entry_at_and_continuity() { + let s = schedule(); + assert!(is_continuous(&s)); + assert_eq!(entry_at(&s, 5_000), Some((0, 5_000))); + assert_eq!(entry_at(&s, 11_000), Some((1, 1_000))); + assert_eq!(entry_at(&s, 100_000), None); + } + + #[test] + fn program_as_run_is_recomputable() { + // Window [8s, 13s) spans the tail of A, the whole ad, the head of B. + let g = GrantRef::unbounded("video.channel"); + let r = ChannelReceipt::seal(&key(1), "did:key:chan", "fast-42", schedule(), 8_000, 13_000, 6_000, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + assert_eq!(r.aired, vec![0, 1, 2], "all three entries touch the window"); + assert_eq!(r.aired_entries().iter().map(|e| e.asset_id.as_str()).collect::>(), ["show-A", "ad-1", "show-B"]); + } + + #[test] + fn a_gap_in_the_schedule_will_not_verify() { + let mut s = schedule(); + s[2].start_ms = 13_000; // leave 1s of dead air after the ad + let g = GrantRef::unbounded("video.channel"); + let r = ChannelReceipt::seal(&key(2), "o", "c", s, 0, 22_000, 0, None, g, None); + assert!(!r.verify(), "a channel with dead air is not a valid linear schedule"); + } + + #[test] + fn a_misreported_program_as_run_is_rejected() { + let g = GrantRef::unbounded("video.channel"); + // Window [0, 5s): only show-A aired. + let mut r = ChannelReceipt::seal(&key(3), "o", "c", schedule(), 0, 5_000, 0, None, g, None); + assert_eq!(r.aired, vec![0]); + assert!(r.verify()); + r.aired = vec![0, 1]; // claim the ad aired when it did not + r.sig = key(3).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify(), "an aired set the window does not produce must fail"); + } + + #[test] + fn windows_chain_and_energy_amortises() { + let g = GrantRef::unbounded("video.channel"); + let w1 = ChannelReceipt::seal(&key(4), "o", "c", schedule(), 0, 10_000, 3_000, Some(EnergyProvenance::ModelBased), g.clone(), None); + assert!(w1.verify()); + // The next window chains from the first — the channel history is a chain. + let w2 = ChannelReceipt::seal(&key(4), "o", "c", schedule(), 10_000, 22_000, 6_000, Some(EnergyProvenance::ModelBased), g, Some(w1.receipt_hash())); + assert!(w2.verify()); + assert_eq!(w2.parent_receipt_hash, Some(w1.receipt_hash())); + let (uj, _) = w2.uj_per_aired().unwrap(); + assert!((uj - 3000.0).abs() < 1e-9, "6000 uJ / 2 aired (ad-1, show-B) = 3000 each"); + } +} diff --git a/wai/wai-rs/src/wai_video_keys.rs b/wai/wai-rs/src/wai_video_keys.rs new file mode 100644 index 000000000..ae0980cfe --- /dev/null +++ b/wai/wai-rs/src/wai_video_keys.rs @@ -0,0 +1,363 @@ +//! Attested content-key release — `wai.video.keys`. +//! +//! The DRM systems (Widevine, PlayReady, FairPlay) wrap and deliver the content +//! key; what none of them leave is a portable, checkable record of *why* a key +//! was released — under which entitlement, before which expiry. This profile is +//! that record: every release, and every refusal, is a signed receipt whose +//! decision a verifier **recomputes** from the bound inputs. +//! +//! The decision is a pure function of `(grant capability, required entitlement, +//! issued time, expiry)`. [`KeyReleaseReceipt::verify`] re-runs [`decide_release`] +//! over the receipt's own fields and rejects any receipt whose stored decision +//! does not match — so "we released keys only to entitled, unexpired sessions" +//! stops being a policy assertion and becomes a fact a licensor can check +//! against the signed log. +//! +//! The key itself never enters the receipt. A granted release carries a +//! `key_commit` — BLAKE3 over the released key bytes — so a verifier confirms +//! *which* key was released (it matches the KID's key on the encrypted content) +//! without the record ever carrying key material. A refusal carries no +//! commitment, and the coupling is enforced, not merely documented. +//! +//! Only `joules_micro` is measured-attested. Reuses the manifest module's +//! `EnergyProvenance` and the world Merkle floor's Ed25519 + `GrantRef`; links +//! to a manifest via `parent_receipt_hash`. Reuse, not reinvention. + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; + +use crate::quantum_ops::GrantRef; +use crate::wai_video_manifest::EnergyProvenance; + +const DOMAIN_RECEIPT: &[u8] = b"wai:video-keys-receipt\x01"; +const DOMAIN_RECEIPT_ID: &[u8] = b"wai:video-keys-receipt-id\x01"; +const DOMAIN_KEY: &[u8] = b"wai:video-keys-commit\x01"; + +/// The DRM system the release targets. Sealed so the record says which client +/// ecosystem the key went to. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum DrmSystem { + Widevine, + PlayReady, + FairPlay, + ClearKey, +} + +impl DrmSystem { + fn tag(self) -> u8 { + match self { + DrmSystem::Widevine => 1, + DrmSystem::PlayReady => 2, + DrmSystem::FairPlay => 3, + DrmSystem::ClearKey => 4, + } + } + pub fn label(self) -> &'static str { + match self { + DrmSystem::Widevine => "Widevine", + DrmSystem::PlayReady => "PlayReady", + DrmSystem::FairPlay => "FairPlay", + DrmSystem::ClearKey => "ClearKey", + } + } +} + +/// The outcome of a release decision — a grant *and* every refusal is a +/// first-class, signed record. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ReleaseDecision { + Granted, + DeniedNoEntitlement, + DeniedExpired, +} + +impl ReleaseDecision { + fn tag(self) -> u8 { + match self { + ReleaseDecision::Granted => 1, + ReleaseDecision::DeniedNoEntitlement => 2, + ReleaseDecision::DeniedExpired => 3, + } + } + pub fn label(self) -> &'static str { + match self { + ReleaseDecision::Granted => "Granted", + ReleaseDecision::DeniedNoEntitlement => "DeniedNoEntitlement", + ReleaseDecision::DeniedExpired => "DeniedExpired", + } + } + pub fn is_granted(self) -> bool { + self == ReleaseDecision::Granted + } +} + +/// The one definition of the policy, used by both the issuer and every verifier +/// so they cannot disagree. Entitlement is an exact class match; a granted key +/// requires the request to arrive at or before the entitlement's expiry. +pub fn decide_release( + grant_capability: &str, + required_entitlement: &str, + issued_epoch: u64, + expiry_epoch: u64, +) -> ReleaseDecision { + if grant_capability != required_entitlement { + return ReleaseDecision::DeniedNoEntitlement; + } + if issued_epoch > expiry_epoch { + return ReleaseDecision::DeniedExpired; + } + ReleaseDecision::Granted +} + +/// BLAKE3 commitment to released key bytes — proves *which* key without carrying +/// it. Domain-separated so it can never collide with another module's hash of +/// the same bytes. +pub fn key_commitment(key_bytes: &[u8]) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_KEY); + h.update(&(key_bytes.len() as u32).to_be_bytes()); + h.update(key_bytes); + *h.finalize().as_bytes() +} + +/// A signed content-key release decision. +#[derive(Clone, Debug, PartialEq)] +pub struct KeyReleaseReceipt { + /// The key identifier (KID) on the encrypted content. + pub key_id: [u8; 16], + pub content_id: String, + pub drm: DrmSystem, + /// The entitlement class the content demanded. + pub required_entitlement: String, + pub decision: ReleaseDecision, + /// BLAKE3 over the released key bytes — `Some` iff `decision` is `Granted`. + pub key_commit: Option<[u8; 32]>, + /// The entitlement window enforced, and when the decision was taken. + pub expiry_epoch: u64, + pub issued_epoch: u64, + pub joules_micro: u64, + pub energy_provenance: Option, + /// The grant presented; its `capability` is the entitlement checked. + pub grant: GrantRef, + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +impl KeyReleaseReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&self.key_id); + o.extend_from_slice(&(self.content_id.len() as u32).to_be_bytes()); + o.extend_from_slice(self.content_id.as_bytes()); + o.push(self.drm.tag()); + o.extend_from_slice(&(self.required_entitlement.len() as u32).to_be_bytes()); + o.extend_from_slice(self.required_entitlement.as_bytes()); + o.push(self.decision.tag()); + match self.key_commit { + Some(c) => { + o.push(1); + o.extend_from_slice(&c); + } + None => o.push(0), + } + o.extend_from_slice(&self.expiry_epoch.to_be_bytes()); + o.extend_from_slice(&self.issued_epoch.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, EnergyProvenance::tag_byte)); + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Evaluate the policy and seal the decision. The decision is computed here + /// from the grant and the request, so a receipt cannot claim an outcome the + /// policy would not produce; `released_key` is hashed into a commitment only + /// when the decision is `Granted`. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + key_id: [u8; 16], + content_id: impl Into, + drm: DrmSystem, + required_entitlement: impl Into, + issued_epoch: u64, + expiry_epoch: u64, + released_key: &[u8], + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> KeyReleaseReceipt { + let required_entitlement = required_entitlement.into(); + let decision = + decide_release(&grant.capability, &required_entitlement, issued_epoch, expiry_epoch); + let key_commit = decision.is_granted().then(|| key_commitment(released_key)); + let mut r = KeyReleaseReceipt { + key_id, + content_id: content_id.into(), + drm, + required_entitlement, + decision, + key_commit, + expiry_epoch, + issued_epoch, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + policy consistency. Re-runs [`decide_release`] over the + /// receipt's own fields and rejects any mismatch, enforces the + /// granted-iff-committed coupling, and holds the energy figure and its label + /// together. A refusal is a valid receipt; a *misreported* decision is not. + pub fn verify(&self) -> bool { + let recomputed = decide_release( + &self.grant.capability, + &self.required_entitlement, + self.issued_epoch, + self.expiry_epoch, + ); + if recomputed != self.decision { + return false; + } + if self.decision.is_granted() != self.key_commit.is_some() { + return false; + } + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// Confirm the released key this receipt commits to is the one the caller + /// holds — the licensor's check that the sealed commitment matches the KID's + /// key. `false` for a refusal (there is no committed key). + pub fn commits_to_key(&self, key_bytes: &[u8]) -> bool { + self.key_commit == Some(key_commitment(key_bytes)) + } + + /// Amortised microjoules of decision energy per release, with its + /// acquisition class. `None` when unmetered. + pub fn uj_per_release(&self) -> Option<(f64, EnergyProvenance)> { + match self.energy_provenance { + Some(p) if self.joules_micro > 0 => Some((self.joules_micro as f64, p)), + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + fn grant(cap: &str) -> GrantRef { + GrantRef { grant_hash: [5u8; 32], capability: cap.into(), joule_ceiling_micro: 1_000_000, funds_ceiling: None } + } + + const CEK: &[u8] = b"0123456789abcdef"; // a 16-byte content-encryption key + + #[test] + fn entitled_and_unexpired_releases_and_commits() { + let r = KeyReleaseReceipt::seal( + &key(1), "did:key:license", [0xAB; 16], "asset-abc", DrmSystem::Widevine, + "svod:tier2", 1000, 2000, CEK, 300, Some(EnergyProvenance::HwShunt), + grant("svod:tier2"), None, + ); + assert_eq!(r.decision, ReleaseDecision::Granted); + assert!(r.verify()); + assert!(r.commits_to_key(CEK)); + assert!(!r.commits_to_key(b"the-wrong-key-16"), "a different key must not match the commitment"); + } + + #[test] + fn wrong_entitlement_is_a_signed_refusal() { + let r = KeyReleaseReceipt::seal( + &key(2), "o", [1; 16], "asset", DrmSystem::PlayReady, "svod:tier3", + 1000, 2000, CEK, 0, None, grant("svod:tier2"), None, + ); + assert_eq!(r.decision, ReleaseDecision::DeniedNoEntitlement); + assert!(r.key_commit.is_none(), "a refusal carries no key commitment"); + assert!(r.verify(), "a refusal is still a valid, signed record"); + } + + #[test] + fn expired_entitlement_denies() { + let r = KeyReleaseReceipt::seal( + &key(3), "o", [1; 16], "asset", DrmSystem::FairPlay, "svod:tier2", + 2500, 2000, CEK, 0, None, grant("svod:tier2"), None, + ); + assert_eq!(r.decision, ReleaseDecision::DeniedExpired); + assert!(r.verify()); + } + + #[test] + fn a_misreported_decision_will_not_verify() { + // Forge a "Granted" over a request the policy would deny (wrong tier), + // re-sign it, and confirm the recomputation catches it. + let mut r = KeyReleaseReceipt::seal( + &key(4), "o", [1; 16], "asset", DrmSystem::Widevine, "svod:tier3", + 1000, 2000, CEK, 0, None, grant("svod:tier2"), None, + ); + assert_eq!(r.decision, ReleaseDecision::DeniedNoEntitlement); + r.decision = ReleaseDecision::Granted; + r.key_commit = Some(key_commitment(CEK)); + r.sig = key(4).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify(), "a decision the bound policy would not produce must fail"); + } + + #[test] + fn granted_without_commitment_is_rejected() { + let mut r = KeyReleaseReceipt::seal( + &key(5), "o", [1; 16], "asset", DrmSystem::ClearKey, "svod:tier2", + 1000, 2000, CEK, 100, Some(EnergyProvenance::ModelBased), grant("svod:tier2"), None, + ); + assert!(r.verify()); + r.key_commit = None; // granted but no committed key + r.sig = key(5).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify()); + } +} diff --git a/wai/wai-rs/src/wai_video_manifest.rs b/wai/wai-rs/src/wai_video_manifest.rs new file mode 100644 index 000000000..e64b67bfa --- /dev/null +++ b/wai/wai-rs/src/wai_video_manifest.rs @@ -0,0 +1,503 @@ +//! Attested per-session manifest — `wai.video.manifest`. +//! +//! The incumbent OTT model personalises at the manifest layer: every viewer is +//! handed a 1:1 manifest with ads stitched, blackouts applied and geo enforced, +//! generated per playback request and vouched for by nothing but a dashboard. +//! This profile keeps the personalisation and adds the two things that model +//! cannot give a verifier — **determinism** and a **receipt**. +//! +//! A session is not a viewer, it is a *class*: `(content, entitlement, geo, +//! blackout set, ad pod, time window)`. The rendered manifest is a pure function +//! of that class, so: +//! +//! - **Verifiable** — anyone holding the manifest bytes recomputes +//! [`ManifestReceipt::manifest_hash`] by hashing them, recomputes +//! [`ManifestReceipt::session_class_hash`] from the carried [`SessionClass`], +//! and confirms `manifest_hash == hash(render(segments))`. The composition, the +//! stitched ads, the blackouts applied and the compose work all stop being +//! claims and become checkable facts (see [`ManifestReceipt::verify_render`]). +//! - **Measured-attested** — `joules_micro`, the marginal energy the generation +//! sink spent, vouched for by the signature and nothing else. Same honesty +//! ladder as [`crate::video_receipt`]: a figure without its acquisition class +//! is not comparable to another. +//! +//! The efficiency is itself a checkable fact, not a slogan. Because the manifest +//! is a pure function of the *class* rather than the *viewer*, every viewer in a +//! class receives byte-identical bytes and the generation energy is spent once. +//! [`ManifestReceipt::viewers_served`] records how many sessions that one +//! generation covered, and [`ManifestReceipt::uj_per_viewer`] is the amortised +//! figure — a per-viewer energy that a 1:1-unique generator, by construction, +//! cannot report below its per-viewer generation cost. +//! +//! The grant it ran under is bound in, exactly as the quantum receipts bind +//! theirs: [`GrantRef`] carries the capability, the joule ceiling and the +//! `funds_ceiling` — here the ad budget. Reuse, not reinvention. + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; + +use crate::quantum_ops::GrantRef; +use crate::world::receipt::merkle_root; + +const DOMAIN_RECEIPT: &[u8] = b"wai:video-manifest-receipt\x01"; +const DOMAIN_RECEIPT_ID: &[u8] = b"wai:video-manifest-receipt-id\x01"; +const DOMAIN_CLASS: &[u8] = b"wai:video-manifest-class\x01"; +const DOMAIN_SEG: &[u8] = b"wai:video-manifest-seg\x01"; + +/// How an energy figure was acquired — the family's ladder, mirrored here rather +/// than pulled from [`crate::video_receipt`] so this module carries no +/// pixel-decode dependency. A joule figure without this label is not comparable +/// to another: the same number can mean a counter reading, a model, or a +/// constant. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum EnergyProvenance { + /// Read from a hardware energy interface (RAPL / NVML / SMC / IOReport). + HwShunt, + /// Computed from a calibrated per-operation model (real, honestly derived). + ModelBased, + /// A coarse constant or load estimator. + Estimator, +} + +impl EnergyProvenance { + pub fn label(self) -> &'static str { + match self { + EnergyProvenance::HwShunt => "HwShunt", + EnergyProvenance::ModelBased => "ModelBased", + EnergyProvenance::Estimator => "Estimator", + } + } + /// The byte written into a signing payload — public so sibling video + /// capabilities (e.g. `wai.video.ssai`) seal the same energy label the same + /// way rather than each keeping a private copy. + pub fn tag_byte(self) -> u8 { + match self { + EnergyProvenance::HwShunt => 1, + EnergyProvenance::ModelBased => 2, + EnergyProvenance::Estimator => 3, + } + } +} + +/// Whether a segment carries programme content or a stitched ad. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum SegmentKind { + Content, + Ad, +} + +impl SegmentKind { + fn tag(self) -> u8 { + match self { + SegmentKind::Content => 1, + SegmentKind::Ad => 2, + } + } +} + +/// One entry in the ordered manifest composition. +/// +/// `ad_id.is_some()` iff `kind == Ad`; [`ManifestReceipt::verify`] rejects any +/// other combination, so the monetisation audit (the ad-bearing segments) is a +/// single source of truth rather than a second list that could disagree. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Segment { + pub index: u64, + pub kind: SegmentKind, + /// The segment URI as it appears in the manifest (content or ad). + pub uri: String, + pub duration_ms: u64, + /// Present exactly for ad segments — the ad decision this break resolved to. + pub ad_id: Option, +} + +impl Segment { + fn leaf(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_SEG); + h.update(&self.index.to_be_bytes()); + h.update(&[self.kind.tag()]); + h.update(&self.duration_ms.to_be_bytes()); + h.update(&(self.uri.len() as u32).to_be_bytes()); + h.update(self.uri.as_bytes()); + match &self.ad_id { + Some(a) => { + h.update(&[1]); + h.update(&(a.len() as u32).to_be_bytes()); + h.update(a.as_bytes()); + } + None => { + h.update(&[0]); + } + } + *h.finalize().as_bytes() + } +} + +/// The deterministic inputs that define a manifest. Its hash is the dedup key: +/// two sessions with the same class render to byte-identical manifests, so a +/// platform generates once and serves many. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct SessionClass { + pub content_id: String, + /// Entitlement class, e.g. `"svod:tier2"` — never a viewer identity. + pub entitlement: String, + /// ISO-3166 country the geo rules resolved against. + pub geo: String, + /// The active blackout ids. Order-independent: hashed sorted+deduped. + pub blackouts: Vec, + /// The ad-decision pod this class resolved to (the SSAI decision key). + pub ad_pod_id: String, + /// The manifest time-window bucket (a live window index or `0` for VOD). + pub window: u64, +} + +impl SessionClass { + /// Domain-separated, canonical, order-independent over `blackouts`. + pub fn class_hash(&self) -> [u8; 32] { + let mut bs: Vec<&str> = self.blackouts.iter().map(String::as_str).collect(); + bs.sort_unstable(); + bs.dedup(); + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_CLASS); + for s in [ + self.content_id.as_str(), + self.entitlement.as_str(), + self.geo.as_str(), + self.ad_pod_id.as_str(), + ] { + h.update(&(s.len() as u32).to_be_bytes()); + h.update(s.as_bytes()); + } + h.update(&(bs.len() as u32).to_be_bytes()); + for s in bs { + h.update(&(s.len() as u32).to_be_bytes()); + h.update(s.as_bytes()); + } + h.update(&self.window.to_be_bytes()); + *h.finalize().as_bytes() + } +} + +/// Deterministic HLS rendering: the manifest is a pure function of the ordered +/// segments, so `hash(render(segments))` is a stable identity a verifier can +/// recompute. Ad segments carry an `EXT-X-DISCONTINUITY` — the real SSAI splice +/// marker — so the stitched breaks are visible in the bytes, not only the +/// receipt. Target duration is derived (ceil of the longest segment) rather than +/// supplied, so nothing outside `segments` can move the output. +pub fn render_hls(segments: &[Segment]) -> String { + let target = segments + .iter() + .map(|s| s.duration_ms.div_ceil(1000)) + .max() + .unwrap_or(0); + let mut out = String::new(); + out.push_str("#EXTM3U\n#EXT-X-VERSION:6\n"); + out.push_str(&format!("#EXT-X-TARGETDURATION:{target}\n")); + out.push_str("#EXT-X-MEDIA-SEQUENCE:0\n"); + for s in segments { + if s.kind == SegmentKind::Ad { + out.push_str("#EXT-X-DISCONTINUITY\n"); + } + // Fixed 3-dp seconds so the byte output is stable across platforms. + out.push_str(&format!("#EXTINF:{}.{:03},\n", s.duration_ms / 1000, s.duration_ms % 1000)); + out.push_str(&s.uri); + out.push('\n'); + } + out.push_str("#EXT-X-ENDLIST\n"); + out +} + +/// A signed, energy-accounted per-session manifest. +#[derive(Clone, Debug, PartialEq)] +pub struct ManifestReceipt { + /// Identity: BLAKE3 over the rendered manifest bytes. Verifiable by hashing + /// the bytes a player received. + pub manifest_hash: [u8; 32], + /// The dedup key — BLAKE3 over [`SessionClass`]. Verifiable from `class`. + pub session_class_hash: [u8; 32], + /// Carried so a verifier recomputes the class hash and reads the policy + /// (entitlement, geo, blackouts) that was enforced. + pub class: SessionClass, + /// The ordered composition. `manifest_hash == hash(render(segments))`. + pub segments: Vec, + /// Merkle root over the segment leaves — the family's shared helper. + pub merkle_root: [u8; 32], + /// Portable compose work: the number of segments composed. Verified by + /// recomputation, so it cannot be inflated to flatter an energy figure. + pub work_compose_ops: u64, + /// How many sessions this one generation served (the dedup multiplier). + /// `>= 1`. The class determinism is what makes this honest: every one of + /// them received the same bytes. + pub viewers_served: u64, + /// Marginal microjoules the generation sink spent (`0` = unmetered). + /// Attested by the signature, not independently verifiable. + pub joules_micro: u64, + /// How `joules_micro` was acquired. `None` iff unmetered. + pub energy_provenance: Option, + /// The JCP grant this session ran under — capability, joule ceiling, and + /// `funds_ceiling` (the ad budget). Bound in, as the quantum receipts do. + pub grant: GrantRef, + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +impl ManifestReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&self.manifest_hash); + o.extend_from_slice(&self.session_class_hash); + o.extend_from_slice(&self.merkle_root); + o.extend_from_slice(&self.work_compose_ops.to_be_bytes()); + o.extend_from_slice(&self.viewers_served.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, EnergyProvenance::tag_byte)); + // Grant binding: hash, capability, both ceilings. + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&(self.segments.len() as u64).to_be_bytes()); + for s in &self.segments { + o.extend_from_slice(&s.leaf()); + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Compose a class into a manifest and seal a receipt over what it renders. + /// + /// The manifest hash is taken from the rendering of `segments` here, so the + /// sealed identity cannot be a manifest the segments do not produce. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + class: SessionClass, + segments: Vec, + viewers_served: u64, + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> ManifestReceipt { + let manifest_hash = *blake3::hash(render_hls(&segments).as_bytes()).as_bytes(); + let session_class_hash = class.class_hash(); + let leaves: Vec<[u8; 32]> = segments.iter().map(Segment::leaf).collect(); + let mut r = ManifestReceipt { + manifest_hash, + session_class_hash, + class, + work_compose_ops: segments.len() as u64, + merkle_root: merkle_root(&leaves), + segments, + viewers_served, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + internal consistency. Confirms the manifest is exactly what + /// the carried segments render to, the class hash follows from `class`, the + /// Merkle root and work figure follow from the segments, the ad/kind + /// coupling holds, and the energy figure and its label stand or fall + /// together. Does **not** by itself prove the bytes a player received — + /// [`ManifestReceipt::verify_render`] does that. + pub fn verify(&self) -> bool { + let leaves: Vec<[u8; 32]> = self.segments.iter().map(Segment::leaf).collect(); + if merkle_root(&leaves) != self.merkle_root { + return false; + } + if self.class.class_hash() != self.session_class_hash { + return false; + } + if *blake3::hash(render_hls(&self.segments).as_bytes()).as_bytes() != self.manifest_hash { + return false; + } + if self.work_compose_ops != self.segments.len() as u64 { + return false; + } + if self.viewers_served == 0 { + return false; + } + for (i, s) in self.segments.iter().enumerate() { + if s.index != i as u64 { + return false; + } + if (s.kind == SegmentKind::Ad) != s.ad_id.is_some() { + return false; + } + } + // A figure and its acquisition class stand or fall together: an + // unlabelled non-zero figure is uncomparable; a labelled zero claims a + // measurement that did not happen. Both rejected. + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// The independent check: the bytes a player received hash to + /// `manifest_hash`, and re-rendering the sealed segments reproduces those + /// exact bytes. A verifier need not trust the generating machine — the + /// manifest is a pure function of the composition. `joules_micro` is + /// untouched; it is not reproducible and is not meant to be. + pub fn verify_render(&self, rendered_manifest: &[u8]) -> bool { + if *blake3::hash(rendered_manifest).as_bytes() != self.manifest_hash { + return false; + } + if render_hls(&self.segments).as_bytes() != rendered_manifest { + return false; + } + self.verify() + } + + /// The stitched ads — the monetisation audit, derived from the one source of + /// truth (ad-bearing segments) so it cannot disagree with the manifest. + /// Each is `(break_index, ad_id, duration_ms)`. + pub fn ad_insertions(&self) -> Vec<(u64, &str, u64)> { + self.segments + .iter() + .filter_map(|s| s.ad_id.as_deref().map(|a| (s.index, a, s.duration_ms))) + .collect() + } + + /// Amortised microjoules per viewer served, **with** the acquisition class — + /// the only comparable form. This is the efficiency the class-dedup buys, + /// and it is honest precisely because the manifest determinism is verifiable: + /// every one of `viewers_served` viewers received identical bytes from one + /// generation. `None` when unmetered. + pub fn uj_per_viewer(&self) -> Option<(f64, EnergyProvenance)> { + match (self.energy_provenance, self.viewers_served) { + (Some(p), v) if self.joules_micro > 0 && v > 0 => { + Some((self.joules_micro as f64 / v as f64, p)) + } + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + fn class() -> SessionClass { + SessionClass { + content_id: "asset-abc".into(), + entitlement: "svod:tier2".into(), + geo: "US".into(), + blackouts: vec!["nfl-home-market".into()], + ad_pod_id: "pod-42".into(), + window: 7, + } + } + + fn segments() -> Vec { + vec![ + Segment { index: 0, kind: SegmentKind::Content, uri: "seg0.ts".into(), duration_ms: 6000, ad_id: None }, + Segment { index: 1, kind: SegmentKind::Ad, uri: "ad/xyz/0.ts".into(), duration_ms: 4000, ad_id: Some("ad-xyz".into()) }, + Segment { index: 2, kind: SegmentKind::Content, uri: "seg1.ts".into(), duration_ms: 6000, ad_id: None }, + ] + } + + #[test] + fn seal_verify_roundtrip() { + let g = GrantRef { grant_hash: [9u8; 32], capability: "video.manifest".into(), joule_ceiling_micro: 5_000_000, funds_ceiling: Some(250) }; + let r = ManifestReceipt::seal(&key(1), "did:key:origin", class(), segments(), 12_000, 800, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + // The bytes a player received verify against the receipt. + let rendered = render_hls(&r.segments); + assert!(r.verify_render(rendered.as_bytes())); + // Monetisation audit is exactly the ad segment. + assert_eq!(r.ad_insertions(), vec![(1, "ad-xyz", 4000)]); + } + + #[test] + fn tamper_on_ad_is_rejected() { + let g = GrantRef::unbounded("video.manifest"); + let mut r = ManifestReceipt::seal(&key(2), "did:key:o", class(), segments(), 3, 0, None, g, None); + assert!(r.verify()); + // Swap the ad for a different creative without re-signing. + r.segments[1].ad_id = Some("ad-hijack".into()); + r.segments[1].uri = "ad/hijack/0.ts".into(); + assert!(!r.verify(), "a swapped ad must break the receipt"); + } + + #[test] + fn class_determinism_enables_dedup() { + // Two independent sessions of the same class render byte-identical + // manifests: the dedup that makes uj_per_viewer honest. + let a = render_hls(&segments()); + let b = render_hls(&segments()); + assert_eq!(a, b); + assert_eq!(class().class_hash(), class().class_hash()); + // Ad segments surface as HLS discontinuities in the bytes themselves. + assert!(a.contains("#EXT-X-DISCONTINUITY")); + } + + #[test] + fn efficiency_is_amortised_across_the_class() { + let g = GrantRef::unbounded("video.manifest"); + // One 9000 uJ generation served 300 viewers of the class. + let r = ManifestReceipt::seal(&key(3), "o", class(), segments(), 300, 9000, Some(EnergyProvenance::ModelBased), g, None); + let (uj, prov) = r.uj_per_viewer().unwrap(); + assert_eq!(prov, EnergyProvenance::ModelBased); + assert!((uj - 30.0).abs() < 1e-9, "9000 uJ / 300 viewers = 30 uJ/viewer"); + } + + #[test] + fn labelled_zero_and_unlabelled_figure_are_rejected() { + let g = GrantRef::unbounded("video.manifest"); + let mut r = ManifestReceipt::seal(&key(4), "o", class(), segments(), 1, 500, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + // Unlabelled non-zero: uncomparable number. + r.energy_provenance = None; + r.sig = key(4).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify()); + // Labelled zero: a measurement that did not happen. + r.joules_micro = 0; + r.energy_provenance = Some(EnergyProvenance::HwShunt); + r.sig = key(4).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify()); + } +} diff --git a/wai/wai-rs/src/wai_video_package.rs b/wai/wai-rs/src/wai_video_package.rs new file mode 100644 index 000000000..0a1bf5a1c --- /dev/null +++ b/wai/wai-rs/src/wai_video_package.rs @@ -0,0 +1,368 @@ +//! Deterministic packaging + attested SegmentMap — `wai.video.package`. +//! +//! The ingest/packaging layer: a source is sliced into segments, each with an +//! index and a content hash, and the ordered `(index -> content_hash)` map is +//! the SegmentMap the manifest layer references. Two things the incumbent +//! packagers leave implicit become explicit and checkable here. +//! +//! - **The SegmentMap is signed.** `segment_map_root` is a Merkle commitment +//! over the segment leaves, so a `wai.video.manifest` that references segment +//! `i` can be checked against the package that actually produced it — the two +//! receipts compose. +//! - **The dedup is a fact, not a billing line.** Identical content — an ad +//! played in every break, a bumper, a replay, the overlap between simulcast +//! feeds — hashes identically and is stored and encoded once. +//! [`PackageReceipt::verify`] recomputes `unique_segments` and `stored_bytes` +//! from the segments themselves, so the storage/encode saving cannot be +//! overstated. `uj_per_unique_segment` is the encode-once energy, and it is +//! honest precisely because the uniqueness is recomputable. +//! +//! Only `joules_micro` is measured-attested. Reuses the manifest module's +//! `EnergyProvenance` and the world Merkle floor's Ed25519 + `GrantRef`. + +use std::collections::BTreeSet; + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; + +use crate::quantum_ops::GrantRef; +use crate::wai_video_manifest::EnergyProvenance; +use crate::world::receipt::merkle_root; + +const DOMAIN_RECEIPT: &[u8] = b"wai:video-package-receipt\x01"; +const DOMAIN_RECEIPT_ID: &[u8] = b"wai:video-package-receipt-id\x01"; +const DOMAIN_SEG: &[u8] = b"wai:video-package-seg\x01"; +const DOMAIN_MEDIA: &[u8] = b"wai:video-package-media\x01"; + +/// One segment in the SegmentMap. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct SegmentEntry { + pub index: u64, + /// BLAKE3 over the segment's media bytes — the identity that makes two + /// byte-identical segments dedup. + pub content_hash: [u8; 32], + pub duration_ms: u64, + pub byte_len: u64, +} + +impl SegmentEntry { + fn leaf(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_SEG); + h.update(&self.index.to_be_bytes()); + h.update(&self.content_hash); + h.update(&self.duration_ms.to_be_bytes()); + h.update(&self.byte_len.to_be_bytes()); + *h.finalize().as_bytes() + } +} + +/// A source GOP (group-of-pictures): the smallest independently-decodable unit, +/// which a segment boundary must fall on. `(media bytes, presentation duration)`. +pub type Gop<'a> = (&'a [u8], u64); + +/// BLAKE3 over concatenated GOP media bytes — a segment's content identity. +fn media_hash(gops: &[Gop]) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_MEDIA); + for (bytes, _) in gops { + h.update(&(bytes.len() as u64).to_be_bytes()); + h.update(bytes); + } + *h.finalize().as_bytes() +} + +/// Deterministic segmentation: accumulate GOPs until the segment reaches +/// `target_ms`, then close it on the GOP boundary. A pure function of the source +/// and the target, so the SegmentMap is reproducible and content that repeats +/// byte-for-byte lands on identical `content_hash`es. +pub fn segment(gops: &[Gop], target_ms: u64) -> Vec { + let mut out = Vec::new(); + let mut cur: Vec = Vec::new(); + let mut dur = 0u64; + let mut bytes = 0u64; + let mut close = |cur: &mut Vec, dur: &mut u64, bytes: &mut u64, out: &mut Vec| { + if !cur.is_empty() { + out.push(SegmentEntry { + index: out.len() as u64, + content_hash: media_hash(cur), + duration_ms: *dur, + byte_len: *bytes, + }); + cur.clear(); + *dur = 0; + *bytes = 0; + } + }; + for &(b, d) in gops { + cur.push((b, d)); + dur += d; + bytes += b.len() as u64; + if dur >= target_ms { + close(&mut cur, &mut dur, &mut bytes, &mut out); + } + } + close(&mut cur, &mut dur, &mut bytes, &mut out); + out +} + +/// The count of distinct segment contents, and the bytes a dedup store keeps +/// (one copy per distinct content). Both recomputed from the segments so a +/// receipt cannot overstate the saving. +fn dedup_stats(segments: &[SegmentEntry]) -> (u64, u64) { + let mut seen: BTreeSet<[u8; 32]> = BTreeSet::new(); + let mut stored = 0u64; + for s in segments { + if seen.insert(s.content_hash) { + stored += s.byte_len; + } + } + (seen.len() as u64, stored) +} + +/// A signed SegmentMap with an attested dedup accounting. +#[derive(Clone, Debug, PartialEq)] +pub struct PackageReceipt { + pub asset_id: String, + /// Merkle commitment over the segment leaves — the SegmentMap identity a + /// manifest is checked against. + pub segment_map_root: [u8; 32], + pub segments: Vec, + pub total_segments: u64, + /// Distinct `content_hash`es — recomputed in verify(). + pub unique_segments: u64, + pub total_bytes: u64, + /// Bytes a dedup store keeps (one copy per distinct content) — recomputed. + pub stored_bytes: u64, + pub work_segment_ops: u64, + pub joules_micro: u64, + pub energy_provenance: Option, + pub grant: GrantRef, + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +impl PackageReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&(self.asset_id.len() as u32).to_be_bytes()); + o.extend_from_slice(self.asset_id.as_bytes()); + o.extend_from_slice(&self.segment_map_root); + o.extend_from_slice(&self.total_segments.to_be_bytes()); + o.extend_from_slice(&self.unique_segments.to_be_bytes()); + o.extend_from_slice(&self.total_bytes.to_be_bytes()); + o.extend_from_slice(&self.stored_bytes.to_be_bytes()); + o.extend_from_slice(&self.work_segment_ops.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, EnergyProvenance::tag_byte)); + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&(self.segments.len() as u64).to_be_bytes()); + for s in &self.segments { + o.extend_from_slice(&s.leaf()); + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Seal a SegmentMap. The dedup figures are computed here from the segments, + /// so they cannot be set to a saving the map does not support. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + asset_id: impl Into, + segments: Vec, + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> PackageReceipt { + let leaves: Vec<[u8; 32]> = segments.iter().map(SegmentEntry::leaf).collect(); + let (unique_segments, stored_bytes) = dedup_stats(&segments); + let total_bytes = segments.iter().map(|s| s.byte_len).sum(); + let mut r = PackageReceipt { + asset_id: asset_id.into(), + segment_map_root: merkle_root(&leaves), + total_segments: segments.len() as u64, + unique_segments, + total_bytes, + stored_bytes, + work_segment_ops: segments.len() as u64, + segments, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + internal consistency: the Merkle root, the counts and the + /// recomputed dedup figures must all follow from the carried segments, and + /// the energy figure and its label stand or fall together. + pub fn verify(&self) -> bool { + let leaves: Vec<[u8; 32]> = self.segments.iter().map(SegmentEntry::leaf).collect(); + if merkle_root(&leaves) != self.segment_map_root { + return false; + } + if self.total_segments != self.segments.len() as u64 { + return false; + } + if self.work_segment_ops != self.segments.len() as u64 { + return false; + } + let (uniq, stored) = dedup_stats(&self.segments); + if uniq != self.unique_segments || stored != self.stored_bytes { + return false; + } + if self.total_bytes != self.segments.iter().map(|s| s.byte_len).sum::() { + return false; + } + for (i, s) in self.segments.iter().enumerate() { + if s.index != i as u64 { + return false; + } + } + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// Whether the segment at `index` in the attested map has this content — + /// how a `wai.video.manifest` reference is checked against the package. + pub fn segment_content(&self, index: u64) -> Option<[u8; 32]> { + self.segments.get(index as usize).map(|s| s.content_hash) + } + + /// Bytes a dedup store saves versus storing every segment. Verifiable, since + /// both terms are recomputed in [`PackageReceipt::verify`]. + pub fn bytes_saved(&self) -> u64 { + self.total_bytes.saturating_sub(self.stored_bytes) + } + + /// Encode-once energy: microjoules per *distinct* segment, with its + /// acquisition class. `None` when unmetered. + pub fn uj_per_unique_segment(&self) -> Option<(f64, EnergyProvenance)> { + match (self.energy_provenance, self.unique_segments) { + (Some(p), u) if self.joules_micro > 0 && u > 0 => { + Some((self.joules_micro as f64 / u as f64, p)) + } + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + // A source where the ad GOP (`AD`) recurs: content, ad, content, ad. + fn source() -> Vec> { + vec![ + (b"content-gop-0000".as_ref(), 2000), + (b"AD-creative-0001".as_ref(), 2000), + (b"content-gop-0002".as_ref(), 2000), + (b"AD-creative-0001".as_ref(), 2000), + ] + } + + #[test] + fn segmentation_is_deterministic_and_dedups_repeats() { + // target 2000ms -> one GOP per segment; the two ad segments are identical. + let a = segment(&source(), 2000); + let b = segment(&source(), 2000); + assert_eq!(a, b, "segmentation must be a pure function"); + assert_eq!(a.len(), 4); + assert_eq!(a[1].content_hash, a[3].content_hash, "the repeated ad dedups"); + let (uniq, _) = dedup_stats(&a); + assert_eq!(uniq, 3, "4 segments, 3 distinct"); + } + + #[test] + fn seal_verify_and_dedup_is_a_fact() { + let segs = segment(&source(), 2000); + let g = GrantRef::unbounded("video.package"); + let r = PackageReceipt::seal(&key(1), "did:key:pkg", "asset-abc", segs, 12_000, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + assert_eq!(r.total_segments, 4); + assert_eq!(r.unique_segments, 3); + assert_eq!(r.bytes_saved(), 16, "one 16-byte ad segment is stored once, not twice"); + // A manifest referencing index 3 can be checked against the package. + assert_eq!(r.segment_content(3), Some(r.segments[1].content_hash)); + } + + #[test] + fn overstated_dedup_will_not_verify() { + let segs = segment(&source(), 2000); + let g = GrantRef::unbounded("video.package"); + let mut r = PackageReceipt::seal(&key(2), "o", "asset", segs, 0, None, g, None); + assert!(r.verify()); + // Claim more saving than the map supports. + r.unique_segments = 2; + r.stored_bytes = 32; + r.sig = key(2).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify(), "a dedup figure the segments do not support must fail"); + } + + #[test] + fn tampered_segment_breaks_the_map() { + let segs = segment(&source(), 2000); + let g = GrantRef::unbounded("video.package"); + let mut r = PackageReceipt::seal(&key(3), "o", "asset", segs, 0, None, g, None); + assert!(r.verify()); + r.segments[0].content_hash = [0xFF; 32]; // swap a segment's content + assert!(!r.verify(), "a swapped segment must break the SegmentMap root"); + } + + #[test] + fn encode_once_energy_amortises_over_unique_segments() { + let segs = segment(&source(), 2000); + let g = GrantRef::unbounded("video.package"); + // 9000 uJ of packaging over 3 distinct segments. + let r = PackageReceipt::seal(&key(4), "o", "asset", segs, 9000, Some(EnergyProvenance::ModelBased), g, None); + let (uj, prov) = r.uj_per_unique_segment().unwrap(); + assert_eq!(prov, EnergyProvenance::ModelBased); + assert!((uj - 3000.0).abs() < 1e-9, "9000 uJ / 3 unique = 3000 uJ each"); + } +} diff --git a/wai/wai-rs/src/wai_video_policy.rs b/wai/wai-rs/src/wai_video_policy.rs new file mode 100644 index 000000000..aa413e5e5 --- /dev/null +++ b/wai/wai-rs/src/wai_video_policy.rs @@ -0,0 +1,142 @@ +//! Pure decision policy for the video capabilities — no crypto, no I/O. +//! +//! The ad decision and the spend accounting are ordinary integer algorithms; +//! the receipt layer that signs their output is not. Keeping the two apart +//! matters for the same reason `byte-exact-conformance` exists: a module with a +//! minimal dependency closure can be handed to a model checker, and the claims +//! this layer makes are exactly the ones worth checking. +//! +//! `wai.video.ssai` advertises that **overspend cannot be signed**. That claim +//! has two halves. The receipt half — `verify()` recomputing the billable spend +//! and rejecting it over the grant's ceiling — is enforced there. The half that +//! lives here is stronger and earlier: [`decide`] never *proposes* a fill that +//! exceeds the funds, the avail duration, or the slot count it was given. The +//! harnesses below prove that, rather than sampling it. + +/// A candidate ad in the decision pod. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct AdCandidate { + pub ad_id: String, + /// Identity of the creative bytes — bound into the impression so a swapped + /// creative breaks the receipt. + pub creative_hash: [u8; 32], + pub duration_ms: u64, + /// Price charged if this ad is served, in minor-currency micro-units. The + /// same unit as the grant's `funds_ceiling`. + pub price_micros: u64, +} + +/// One filled slot in the avail: the selected ad and the completion its beacons +/// confirmed. `quartiles_reached`: `0` = never rendered, `1` = started (the +/// billable impression, IAB), `2..=5` = 25/50/75/100%. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Impression { + pub slot: u64, + pub ad_id: String, + pub creative_hash: [u8; 32], + pub duration_ms: u64, + pub price_micros: u64, + pub quartiles_reached: u8, +} + +impl Impression { + /// An impression is billable once the ad has begun to render (IAB): the + /// creative reached at least its start beacon. + pub fn is_billable(&self) -> bool { + self.quartiles_reached >= 1 + } +} + +/// Deterministic decision: fill up to `avail_slots` of a `avail_duration_ms` +/// break from `candidates`, never exceeding `funds_remaining_micros`. +/// +/// Greedy by price descending, ties broken by `ad_id` ascending — a pure +/// function of its inputs, so an auditor reproduces the fill exactly. Each +/// selected ad must fit the remaining avail time and the remaining funds. Slots +/// are returned as [`Impression`]s with `quartiles_reached = 0`; the caller +/// raises each as its beacons arrive, then seals. +pub fn decide( + candidates: &[AdCandidate], + avail_slots: u64, + avail_duration_ms: u64, + funds_remaining_micros: u64, +) -> Vec { + let mut order: Vec<&AdCandidate> = candidates.iter().collect(); + order.sort_by(|a, b| b.price_micros.cmp(&a.price_micros).then(a.ad_id.cmp(&b.ad_id))); + let mut out = Vec::new(); + let (mut time_left, mut funds_left) = (avail_duration_ms, funds_remaining_micros); + for c in order { + if out.len() as u64 >= avail_slots { + break; + } + if c.duration_ms <= time_left && c.price_micros <= funds_left { + out.push(Impression { + slot: out.len() as u64, + ad_id: c.ad_id.clone(), + creative_hash: c.creative_hash, + duration_ms: c.duration_ms, + price_micros: c.price_micros, + quartiles_reached: 0, + }); + time_left -= c.duration_ms; + funds_left -= c.price_micros; + } + } + out +} + +/// Σ price over billable impressions — the one definition of spend, used by both +/// `seal` and `verify` so they cannot disagree. +pub(crate) fn billable_spend(impressions: &[Impression]) -> u64 { + impressions.iter().filter(|i| i.is_billable()).map(|i| i.price_micros).sum() +} + +// ───────────────────────────────────────────────────────────────────── +// Kani proof harnesses — "overspend cannot be signed", at its root +// ───────────────────────────────────────────────────────────────────── + +// ATTEMPTED AND NOT ACHIEVED — recorded so it is not silently retried. +// +// The natural theorem here is that `decide` never proposes a fill exceeding the +// funds, the avail duration, or the slot count. It does not close under this +// checker: +// +// - 3 candidates, all fields symbolic .......... CBMC timed out at 600s +// - 2 candidates, all fields symbolic .......... CBMC timed out at 900s +// - 2 candidates, durations concrete (funds +// limit isolated) ............................ CBMC timed out at 600s +// +// The cost is not the budget arithmetic, which is trivial. `decide` sorts by +// `ad_id: String`, so the model has to carry `memcmp` plus the +// `Vec`/`raw_vec`/`Layout`/`handle_alloc_error` machinery; the plumbing around +// the logic is what explodes. Kani could stub that away, and the proof would +// then be about the stub — the "stand-in closing a goal nothing decided" +// failure this codebase has already been bitten by. Not worth a green tick. +// +// So the funds limit remains **test-backed, not proof-backed**: see +// `wai_video_ssai::tests::overspend_cannot_be_signed`, which exercises it on a +// concrete pod. Closing it properly needs either a decision path that does not +// sort on a heap-allocated key, or a deductive verifier (Creusot/Verus) rather +// than a bounded model checker. + +/// Everything [`decide`] returns starts unbilled, so a fill cannot be mistaken +/// for delivery: spend is zero until beacons raise the quartiles. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(8)] +#[kani::solver(kissat)] +fn kani_a_fresh_decision_bills_nothing() { + let bounded = || -> u64 { + let v: u64 = kani::any(); + kani::assume(v < (1u64 << 30)); + v + }; + let pod = [AdCandidate { + ad_id: "a".to_string(), + creative_hash: [0u8; 32], + duration_ms: bounded(), + price_micros: bounded(), + }]; + let out = decide(&pod, 1, bounded(), bounded()); + kani::assert(billable_spend(&out) == 0, "a decision bills nothing before its beacons arrive"); +} diff --git a/wai/wai-rs/src/wai_video_ssai.rs b/wai/wai-rs/src/wai_video_ssai.rs new file mode 100644 index 000000000..f06f57560 --- /dev/null +++ b/wai/wai-rs/src/wai_video_ssai.rs @@ -0,0 +1,324 @@ +//! Attested server-side ad insertion — `wai.video.ssai`. +//! +//! SSAI's unsolved problem is not stitching, it is *proof*: buyer and seller +//! reconcile impression counts from separate logs neither can check, and the +//! gap is fraud. This profile makes an ad break a signed, budget-bounded, +//! per-impression record that both sides verify from the same bytes. +//! +//! Two things become checkable facts rather than dashboard claims: +//! +//! - **Which creatives were served, to what completion.** Each filled slot +//! carries the `creative_hash` and the VAST quartile it reached; a buyer +//! holding the receipt confirms exactly what played, not what a report says. +//! - **That the decision stayed within budget.** `budget_spent_micros` is the +//! sum of the *billable* impressions (those that started) and +//! [`SsaiReceipt::verify`] both recomputes it and rejects it if it exceeds the +//! grant's `funds_ceiling`. Overspend cannot be signed. +//! +//! The decision itself is deterministic ([`decide`]): a pure function of the +//! candidate pod, the avail and the funds remaining, so an auditor re-runs it +//! and gets the same fill. The pod is bound by `pod_hash`, so the inputs to that +//! decision are fixed too. Only `joules_micro` is measured-attested — the same +//! honesty ladder as the rest of WAI. +//! +//! Links to [`crate::wai_video_manifest`] by `manifest_hash` and chains from the +//! manifest receipt via `parent_receipt_hash`: the ad break belongs to a +//! specific attested manifest. Reuse, not reinvention. + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; + +use crate::quantum_ops::GrantRef; +// The decision policy is pure integer logic and lives apart from this +// signing layer so a model checker can reach it; re-exported here so the +// capability's public surface is unchanged. +pub use crate::wai_video_policy::{decide, AdCandidate, Impression}; +use crate::wai_video_policy::billable_spend; +use crate::wai_video_manifest::EnergyProvenance; +use crate::world::receipt::merkle_root; + +const DOMAIN_RECEIPT: &[u8] = b"wai:video-ssai-receipt\x01"; +const DOMAIN_RECEIPT_ID: &[u8] = b"wai:video-ssai-receipt-id\x01"; +const DOMAIN_POD: &[u8] = b"wai:video-ssai-pod\x01"; +const DOMAIN_IMP: &[u8] = b"wai:video-ssai-imp\x01"; + + +/// Hash of the ordered candidate pod — the decision input, bound so the +/// deterministic decision is auditable against fixed candidates. +pub fn pod_hash(candidates: &[AdCandidate]) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_POD); + h.update(&(candidates.len() as u64).to_be_bytes()); + for c in candidates { + h.update(&(c.ad_id.len() as u32).to_be_bytes()); + h.update(c.ad_id.as_bytes()); + h.update(&c.creative_hash); + h.update(&c.duration_ms.to_be_bytes()); + h.update(&c.price_micros.to_be_bytes()); + } + *h.finalize().as_bytes() +} + + +impl Impression { + fn leaf(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_IMP); + h.update(&self.slot.to_be_bytes()); + h.update(&(self.ad_id.len() as u32).to_be_bytes()); + h.update(self.ad_id.as_bytes()); + h.update(&self.creative_hash); + h.update(&self.duration_ms.to_be_bytes()); + h.update(&self.price_micros.to_be_bytes()); + h.update(&[self.quartiles_reached]); + *h.finalize().as_bytes() + } +} + + +/// A signed, budget-bounded, per-impression ad-break record. +#[derive(Clone, Debug, PartialEq)] +pub struct SsaiReceipt { + /// The ad break identity within its manifest. + pub avail_id: String, + /// The attested manifest this avail belongs to (`wai.video.manifest`). + pub manifest_hash: [u8; 32], + /// The candidate pod the decision ran over — the auditable decision input. + pub pod_hash: [u8; 32], + /// The filled slots and the completion their beacons confirmed. + pub impressions: Vec, + pub merkle_root: [u8; 32], + /// Σ price over *billable* impressions. Recomputed and ceiling-checked in + /// [`SsaiReceipt::verify`], so it is a fact, not an assertion. + pub budget_spent_micros: u64, + /// Candidates the decision considered — portable work, `>= impressions`. + pub work_decide_ops: u64, + pub joules_micro: u64, + pub energy_provenance: Option, + /// The grant this break ran under; `funds_ceiling` is the spend ceiling. + pub grant: GrantRef, + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + + +impl SsaiReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&(self.avail_id.len() as u32).to_be_bytes()); + o.extend_from_slice(self.avail_id.as_bytes()); + o.extend_from_slice(&self.manifest_hash); + o.extend_from_slice(&self.pod_hash); + o.extend_from_slice(&self.merkle_root); + o.extend_from_slice(&self.budget_spent_micros.to_be_bytes()); + o.extend_from_slice(&self.work_decide_ops.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, |p| p.tag_byte())); + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&(self.impressions.len() as u64).to_be_bytes()); + for i in &self.impressions { + o.extend_from_slice(&i.leaf()); + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Seal an ad break. `budget_spent_micros` is computed from the impressions + /// here, so it cannot be set to a figure the slots do not support. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + avail_id: impl Into, + manifest_hash: [u8; 32], + pod_hash: [u8; 32], + impressions: Vec, + work_decide_ops: u64, + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> SsaiReceipt { + let leaves: Vec<[u8; 32]> = impressions.iter().map(Impression::leaf).collect(); + let mut r = SsaiReceipt { + avail_id: avail_id.into(), + manifest_hash, + pod_hash, + budget_spent_micros: billable_spend(&impressions), + merkle_root: merkle_root(&leaves), + impressions, + work_decide_ops, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + internal consistency: the Merkle root and the recomputed + /// billable spend must follow from the impressions, the spend must not + /// exceed the grant's `funds_ceiling`, the work figure must cover the slots, + /// slots must be contiguous, quartiles in range, and the energy figure and + /// its label must stand or fall together. + pub fn verify(&self) -> bool { + let leaves: Vec<[u8; 32]> = self.impressions.iter().map(Impression::leaf).collect(); + if merkle_root(&leaves) != self.merkle_root { + return false; + } + // Spend is recomputed, not trusted — a tampered figure or a swapped + // creative (which changes a leaf) is caught here. + if billable_spend(&self.impressions) != self.budget_spent_micros { + return false; + } + // Overspend cannot be signed. + if let Some(ceiling) = self.grant.funds_ceiling { + if self.budget_spent_micros > ceiling { + return false; + } + } + if self.work_decide_ops < self.impressions.len() as u64 { + return false; + } + for (i, imp) in self.impressions.iter().enumerate() { + if imp.slot != i as u64 { + return false; + } + if imp.quartiles_reached > 5 { + return false; + } + } + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// The billable impressions — those that started rendering. + pub fn billable_impressions(&self) -> usize { + self.impressions.iter().filter(|i| i.is_billable()).count() + } + + /// Amortised microjoules of decision energy per billable impression, with + /// its acquisition class — the only comparable form. `None` when unmetered + /// or when nothing billable played. + pub fn uj_per_impression(&self) -> Option<(f64, EnergyProvenance)> { + let n = self.billable_impressions() as u64; + match (self.energy_provenance, n) { + (Some(p), v) if self.joules_micro > 0 && v > 0 => { + Some((self.joules_micro as f64 / v as f64, p)) + } + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + fn pod() -> Vec { + vec![ + AdCandidate { ad_id: "ad-a".into(), creative_hash: [1u8; 32], duration_ms: 15000, price_micros: 40_000 }, + AdCandidate { ad_id: "ad-b".into(), creative_hash: [2u8; 32], duration_ms: 15000, price_micros: 30_000 }, + AdCandidate { ad_id: "ad-c".into(), creative_hash: [3u8; 32], duration_ms: 30000, price_micros: 90_000 }, + ] + } + + #[test] + fn decision_is_deterministic_and_bounded() { + // 30s avail, 2 slots, budget 80_000: ad-c (90k) is too dear; greedy by + // price takes ad-a (40k) then ad-b (30k), total 70k, both 15s -> fit. + let a = decide(&pod(), 2, 30_000, 80_000); + let b = decide(&pod(), 2, 30_000, 80_000); + assert_eq!(a, b, "decision must be a pure function of its inputs"); + assert_eq!(a.iter().map(|i| i.ad_id.as_str()).collect::>(), ["ad-a", "ad-b"]); + assert_eq!(a.iter().map(|i| i.price_micros).sum::(), 70_000); + } + + #[test] + fn seal_verify_and_only_started_ads_bill() { + let mut imps = decide(&pod(), 2, 30_000, 80_000); + imps[0].quartiles_reached = 5; // ad-a played to complete -> billable + imps[1].quartiles_reached = 0; // ad-b never rendered -> not billed + let g = GrantRef { grant_hash: [7u8; 32], capability: "video.ssai".into(), joule_ceiling_micro: 1_000_000, funds_ceiling: Some(80_000) }; + let r = SsaiReceipt::seal(&key(1), "did:key:ssai", "avail-1", [9u8; 32], pod_hash(&pod()), imps, 3, 500, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + assert_eq!(r.billable_impressions(), 1); + assert_eq!(r.budget_spent_micros, 40_000, "only the started ad bills"); + } + + #[test] + fn overspend_cannot_be_signed() { + // Both ads billable = 70_000, but grant ceiling is 50_000. + let mut imps = decide(&pod(), 2, 30_000, 80_000); + imps[0].quartiles_reached = 1; + imps[1].quartiles_reached = 1; + let g = GrantRef { grant_hash: [7u8; 32], capability: "video.ssai".into(), joule_ceiling_micro: 0, funds_ceiling: Some(50_000) }; + let r = SsaiReceipt::seal(&key(2), "o", "avail-2", [9u8; 32], pod_hash(&pod()), imps, 3, 0, None, g, None); + assert!(!r.verify(), "spend 70_000 over a 50_000 ceiling must not verify"); + } + + #[test] + fn swapped_creative_breaks_the_receipt() { + let mut imps = decide(&pod(), 1, 30_000, 100_000); + imps[0].quartiles_reached = 5; + let g = GrantRef::unbounded("video.ssai"); + let mut r = SsaiReceipt::seal(&key(3), "o", "avail-3", [9u8; 32], pod_hash(&pod()), imps, 3, 0, None, g, None); + assert!(r.verify()); + r.impressions[0].creative_hash = [0xAA; 32]; // serve a different creative than billed + assert!(!r.verify(), "a swapped creative must break the receipt"); + } + + #[test] + fn efficiency_amortises_over_billable_impressions() { + let mut imps = decide(&pod(), 2, 30_000, 80_000); + imps[0].quartiles_reached = 5; + imps[1].quartiles_reached = 5; + let g = GrantRef::unbounded("video.ssai"); + let r = SsaiReceipt::seal(&key(4), "o", "avail-4", [9u8; 32], pod_hash(&pod()), imps, 3, 900, Some(EnergyProvenance::ModelBased), g, None); + let (uj, prov) = r.uj_per_impression().unwrap(); + assert_eq!(prov, EnergyProvenance::ModelBased); + assert!((uj - 450.0).abs() < 1e-9, "900 uJ / 2 impressions = 450 uJ each"); + } +} diff --git a/wai/wai-verify/Cargo.lock b/wai/wai-verify/Cargo.lock new file mode 100644 index 000000000..5e6cc7ea5 --- /dev/null +++ b/wai/wai-verify/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "wai-verify" +version = "0.1.0" diff --git a/wai/wai-verify/Cargo.toml b/wai/wai-verify/Cargo.toml new file mode 100644 index 000000000..af979f642 --- /dev/null +++ b/wai/wai-verify/Cargo.toml @@ -0,0 +1,18 @@ +# Formal verification host for WAI's integer core. +# +# Deliberately a SEPARATE tiny crate, mirroring `byte-exact-conformance`: it +# `#[path]`-includes the pure-integer sources from wai-rs (single source of +# truth, no copy) so the model checker sees a minimal dependency closure — +# which is what makes the proofs tractable. +# +# NOTE: no `rust-version` on purpose. The verifier ships its own pinned nightly +# toolchain; an MSRV above it makes cargo refuse to build the proof harnesses. +[package] +name = "wai-verify" +version = "0.1.0" +edition = "2024" +license = "Apache-2.0" +publish = false + +[dependencies] +# none — the integer core this crate verifies is pure std. diff --git a/wai/wai-verify/src/lib.rs b/wai/wai-verify/src/lib.rs new file mode 100644 index 000000000..fa53c1100 --- /dev/null +++ b/wai/wai-verify/src/lib.rs @@ -0,0 +1,37 @@ +//! Formal verification host for WAI's integer core. +//! +//! WAI's contract is that an integer decode is byte-identical on every machine. +//! `byte-exact-conformance` establishes that by *sampling*: it decodes fixed +//! vectors on four real targets. This crate establishes the complementary half +//! by *reasoning*: it hosts the model checker over the same sources, so the +//! arithmetic is checked for all inputs in a bounded window rather than for the +//! vectors someone thought to write. +//! +//! The harnesses live beside the code they verify, in `wai-rs`, behind +//! `#[cfg(kani)]`; this crate only supplies a minimal compilation environment +//! (no codec libraries, no ONNX, no MSRV floor above the verifier's toolchain). +//! One source of truth, exactly as the conformance crate does it. + +/// The integer rANS coder — the arithmetic every byte-exact decode flows +/// through, and therefore the place the determinism claim is won or lost. +#[path = "../../wai-rs/src/rans.rs"] +pub mod rans; + +/// The scale→bucket primitive. SPEC §7 names this the soundness hinge: a +/// bucket that flips selects a different CDF and desyncs the rest of the +/// stream, so its totality and its *monotonicity* are both load-bearing. +#[path = "../../wai-rs/src/int_entropy.rs"] +pub mod int_entropy; + +/// The integer transformer kernels on the JPEG-AI path. `softmax` states its +/// own invariant in a comment — the distribution sums to EXACTLY 2^PROB_FRAC — +/// and that invariant is load-bearing: a distribution that does not normalise +/// denormalises the CDF and desyncs the entropy coder. +#[path = "../../wai-rs/src/int_transform.rs"] +pub mod int_transform; + +/// The pure decision policy behind `wai.video.ssai`. Dependency-free by +/// construction, which is what lets the checker reach it without stubbing the +/// crypto layer — a stand-in would close the goal without deciding it. +#[path = "../../wai-rs/src/wai_video_policy.rs"] +pub mod wai_video_policy; diff --git a/wai/wai-web/Cargo.toml b/wai/wai-web/Cargo.toml index b5277ec1e..fc4bc39f1 100644 --- a/wai/wai-web/Cargo.toml +++ b/wai/wai-web/Cargo.toml @@ -19,7 +19,7 @@ js-sys = "0.3" # with the codec chain off. No second implementation: replay-equivalence # in the browser is the identical Rust that generated the conformance # corpus hashes. -wai = { path = "../wai-rs", default-features = false, features = ["world", "audio_scene", "haptic", "splat4d", "provenance", "score", "film", "neural_int", "generate", "video_int", "audio_int", "world_model", "world_int", "splat_int", "quantum", "quantum_ops", "quantum_cal", "quantum_mitigate", "quantum_qec", "quantum_control", "quantum_noise", "quantum_compile", "quantum_atom", "quantum_qbom", "quantum_receipt", "quantum_toolchain", "quantum_mps", "quantum_stabilizer", "quantum_pauli", "quantum_vml", "quantum_phasor", "quantum_qfhrr", "quantum_kernel", "quantum_phasor_meter", "quantum_qdata"] } +wai = { path = "../wai-rs", default-features = false, features = ["world", "audio_scene", "haptic", "splat4d", "provenance", "score", "film", "neural_int", "generate", "video_int", "audio_int", "world_model", "world_int", "splat_int", "quantum", "quantum_ops", "quantum_cal", "quantum_mitigate", "quantum_qec", "quantum_control", "quantum_noise", "quantum_compile", "quantum_atom", "quantum_qbom", "quantum_receipt", "quantum_toolchain", "quantum_mps", "quantum_stabilizer", "quantum_pauli", "quantum_vml", "quantum_phasor", "quantum_qfhrr", "quantum_kernel", "quantum_phasor_meter", "quantum_qdata", "video_workflow"] } ed25519-dalek = "2" # actor keys for browser-side op authoring (same version as wai-rs) blake3 = "1" # in-page receipt check: hash a decoded image against a pinned digest diff --git a/wai/wai-web/src/lib.rs b/wai/wai-web/src/lib.rs index f933ad0e2..2b9a1f8b8 100644 --- a/wai/wai-web/src/lib.rs +++ b/wai/wai-web/src/lib.rs @@ -41,6 +41,11 @@ pub mod generate; // i64, no ML runtime; frame-state-equivalence, decoded + per-frame-verified in-page. pub mod video; +// Browser sink for the OTT workflow (wai.video.manifest + wai.video.ssai): +// render a real manifest, verify its receipt in the tab, swap a creative to +// break it, and watch per-viewer energy amortise as the class dedups. +pub mod video_ott; + // Byte-exact LEARNED AUDIO codec (wai.audio.int_codec) — pure i64, no ML runtime; // sample-equivalence, decoded to int16 PCM + hash-verified + played in-page. pub mod audio_int; diff --git a/wai/wai-web/src/video_ott.rs b/wai/wai-web/src/video_ott.rs new file mode 100644 index 000000000..f87061f5f --- /dev/null +++ b/wai/wai-web/src/video_ott.rs @@ -0,0 +1,270 @@ +//! Browser sink for the OTT workflow — `wai.video.manifest` + `wai.video.ssai`. +//! +//! The same `wai` crate a native packager runs, compiled to wasm32: the page +//! composes a session class, renders the real HLS manifest, seals the receipt +//! and verifies it in the tab. No second implementation, so what the browser +//! shows is what a native sink would produce. +//! +//! Three things the page can demonstrate that a dashboard cannot: +//! +//! - **The manifest is the receipt's subject.** `manifest_hash == +//! hash(render(segments))` is recomputed here, in the tab. +//! - **Tamper-evidence.** [`OttSession::swap_ad`] substitutes a different +//! creative without re-signing — exactly the ad-fraud move — and `verify()` +//! flips to false. +//! - **The efficiency is amortised, not asserted.** Raising the viewers served +//! by one class drops `uj_per_viewer`, because the manifest is a pure function +//! of the class and is generated once for all of them. + +use wasm_bindgen::prelude::*; + +use wai::quantum_ops::GrantRef; +use wai::wai_video_manifest::{ + render_hls, EnergyProvenance, ManifestReceipt, Segment, SegmentKind, SessionClass, +}; +use wai::wai_video_ssai::{decide, pod_hash, AdCandidate, SsaiReceipt}; + +fn hex(b: &[u8]) -> String { + b.iter().map(|x| format!("{x:02x}")).collect() +} + +/// A demo signing key — the page is a sink, not a licensor; a real deployment +/// holds its key in the packager. +fn demo_key() -> ed25519_dalek::SigningKey { + ed25519_dalek::SigningKey::from_bytes(&[42u8; 32]) +} + +/// Build a plausible break-bearing composition: `n_content` programme segments +/// of 6s with a single 4s ad spliced in after the first. +fn compose(n_content: u32, ad_id: &str) -> Vec { + let mut segs = Vec::new(); + let mut idx = 0u64; + for i in 0..n_content { + if i == 1 { + segs.push(Segment { + index: idx, + kind: SegmentKind::Ad, + uri: format!("ad/{ad_id}/0.ts"), + duration_ms: 4000, + ad_id: Some(ad_id.to_string()), + }); + idx += 1; + } + segs.push(Segment { + index: idx, + kind: SegmentKind::Content, + uri: format!("seg{i}.ts"), + duration_ms: 6000, + ad_id: None, + }); + idx += 1; + } + segs +} + +/// An attested per-session manifest, live in the page. +#[wasm_bindgen] +pub struct OttSession { + receipt: ManifestReceipt, + /// The bytes the player was handed — kept as delivered, so a later tamper + /// of the composition is visible against them. + delivered: String, +} + +#[wasm_bindgen] +impl OttSession { + /// Compose a session class, render its manifest and seal the receipt. + /// `blackouts` is a comma-separated set (order-independent by construction). + #[wasm_bindgen(constructor)] + #[allow(clippy::too_many_arguments)] + pub fn new( + content_id: &str, + entitlement: &str, + geo: &str, + blackouts: &str, + ad_pod_id: &str, + window: u64, + n_content: u32, + ad_id: &str, + viewers_served: u64, + joules_micro: u64, + ) -> OttSession { + let class = SessionClass { + content_id: content_id.to_string(), + entitlement: entitlement.to_string(), + geo: geo.to_string(), + blackouts: blackouts + .split(',') + .map(str::trim) + .filter(|s| !s.is_empty()) + .map(String::from) + .collect(), + ad_pod_id: ad_pod_id.to_string(), + window, + }; + let segments = compose(n_content.max(1), ad_id); + let delivered = render_hls(&segments); + let grant = GrantRef { + grant_hash: [7u8; 32], + capability: "video.manifest".to_string(), + joule_ceiling_micro: u64::MAX, + funds_ceiling: None, + }; + let prov = (joules_micro > 0).then_some(EnergyProvenance::ModelBased); + let receipt = ManifestReceipt::seal( + &demo_key(), + "did:key:demo-packager", + class, + segments, + viewers_served.max(1), + joules_micro, + prov, + grant, + None, + ); + OttSession { receipt, delivered } + } + + /// The rendered HLS the player receives — ad breaks appear as real + /// `EXT-X-DISCONTINUITY` splices. + pub fn manifest(&self) -> String { + self.delivered.clone() + } + + /// The manifest currently implied by the sealed composition. After a tamper + /// this diverges from [`OttSession::manifest`]. + pub fn composed_manifest(&self) -> String { + render_hls(&self.receipt.segments) + } + + pub fn manifest_hash_hex(&self) -> String { + hex(&self.receipt.manifest_hash) + } + + /// The dedup key: every viewer of this class gets these identical bytes. + pub fn class_hash_hex(&self) -> String { + hex(&self.receipt.session_class_hash) + } + + pub fn receipt_hash_hex(&self) -> String { + hex(&self.receipt.receipt_hash()) + } + + /// Signature + internal consistency, recomputed in the tab. + pub fn verify(&self) -> bool { + self.receipt.verify() + } + + /// The independent check against the bytes actually delivered. + pub fn verify_delivered(&self) -> bool { + self.receipt.verify_render(self.delivered.as_bytes()) + } + + /// The monetisation audit, derived from the ad-bearing segments: + /// `[[break_index, ad_id, duration_ms], ...]` as JSON. + pub fn ads_json(&self) -> String { + let rows: Vec = self + .receipt + .ad_insertions() + .iter() + .map(|(i, a, d)| format!("[{i},\"{a}\",{d}]")) + .collect(); + format!("[{}]", rows.join(",")) + } + + pub fn segment_count(&self) -> u32 { + self.receipt.segments.len() as u32 + } + + pub fn viewers_served(&self) -> u64 { + self.receipt.viewers_served + } + + /// Amortised microjoules per viewer, or `-1` when unmetered. This is the + /// figure a 1:1-unique generator cannot report below its per-viewer cost. + pub fn uj_per_viewer(&self) -> f64 { + self.receipt.uj_per_viewer().map_or(-1.0, |(v, _)| v) + } + + /// Substitute a different creative into the break **without re-signing** — + /// the ad-fraud move. `verify()` flips to false, because the sealed + /// `manifest_hash` no longer matches what the composition renders. + pub fn swap_ad(&mut self, new_ad_id: &str) { + for s in self.receipt.segments.iter_mut() { + if s.ad_id.is_some() { + s.ad_id = Some(new_ad_id.to_string()); + s.uri = format!("ad/{new_ad_id}/0.ts"); + } + } + } +} + +/// An attested ad break — the budget half of the story. +#[wasm_bindgen] +pub struct OttAdBreak { + receipt: SsaiReceipt, +} + +#[wasm_bindgen] +impl OttAdBreak { + /// Run a deterministic decision over a three-ad pod against `budget_micros`, + /// mark the filled slots as played, and seal. Set `budget_micros` below the + /// resulting spend to watch a ceiling breach refuse to verify. + #[wasm_bindgen(constructor)] + pub fn new(avail_slots: u32, avail_ms: u64, budget_micros: u64, ceiling_micros: u64) -> OttAdBreak { + let pod = vec![ + AdCandidate { ad_id: "ad-alpha".into(), creative_hash: [1u8; 32], duration_ms: 15000, price_micros: 40_000 }, + AdCandidate { ad_id: "ad-beta".into(), creative_hash: [2u8; 32], duration_ms: 15000, price_micros: 30_000 }, + AdCandidate { ad_id: "ad-gamma".into(), creative_hash: [3u8; 32], duration_ms: 30000, price_micros: 90_000 }, + ]; + let mut imps = decide(&pod, avail_slots as u64, avail_ms, budget_micros); + for i in imps.iter_mut() { + i.quartiles_reached = 5; // played to completion + } + let grant = GrantRef { + grant_hash: [8u8; 32], + capability: "video.ssai".to_string(), + joule_ceiling_micro: u64::MAX, + funds_ceiling: Some(ceiling_micros), + }; + let receipt = SsaiReceipt::seal( + &demo_key(), + "did:key:demo-ssai", + "avail-1", + [9u8; 32], + pod_hash(&pod), + imps, + 3, + 0, + None, + grant, + None, + ); + OttAdBreak { receipt } + } + + /// `false` when the spend exceeds the grant's ceiling — overspend cannot be + /// signed into a valid receipt. + pub fn verify(&self) -> bool { + self.receipt.verify() + } + + pub fn budget_spent(&self) -> u64 { + self.receipt.budget_spent_micros + } + + pub fn billable(&self) -> u32 { + self.receipt.billable_impressions() as u32 + } + + /// `[[slot, ad_id, price_micros, quartiles], ...]` as JSON. + pub fn slots_json(&self) -> String { + let rows: Vec = self + .receipt + .impressions + .iter() + .map(|i| format!("[{},\"{}\",{},{}]", i.slot, i.ad_id, i.price_micros, i.quartiles_reached)) + .collect(); + format!("[{}]", rows.join(",")) + } +}