wai: attested OTT video workflow + machine-checked totality proofs over the rANS core #82
20 changed files with 3227 additions and 14 deletions
92
.github/workflows/wai-formal-verification.yml
vendored
Normal file
92
.github/workflows/wai-formal-verification.yml
vendored
Normal file
|
|
@ -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
|
||||
48
wai/SPEC.md
48
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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
229
wai/wai-rs/src/energy_meter.rs
Normal file
229
wai/wai-rs/src/energy_meter.rs
Normal file
|
|
@ -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<EnergyProvenance>) {
|
||||
(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<EnergyProvenance>) {
|
||||
(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<EnergyReading>;
|
||||
/// 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<dyn FnMut() -> Option<u64>>,
|
||||
wrap_at: u64,
|
||||
start: Option<u64>,
|
||||
}
|
||||
|
||||
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<u64> + '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<CounterMeter> {
|
||||
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<u64> {
|
||||
std::fs::read_to_string(path).ok()?.trim().parse::<u64>().ok()
|
||||
}
|
||||
|
||||
impl Meter for CounterMeter {
|
||||
fn start(&mut self) {
|
||||
self.start = (self.read)();
|
||||
}
|
||||
|
||||
fn stop(&mut self) -> Option<EnergyReading> {
|
||||
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<dyn FnMut() -> u64>,
|
||||
milliwatts: u64,
|
||||
t0: Option<u64>,
|
||||
}
|
||||
|
||||
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<EnergyReading> {
|
||||
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<Option<u64>>) -> impl FnMut() -> Option<u64> {
|
||||
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<u64>) -> 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());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -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::*;
|
||||
|
|
|
|||
|
|
@ -63,7 +63,23 @@ pub fn softmax(x: &[i64], frac: u32) -> Vec<i64> {
|
|||
|
||||
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<<PROB_FRAC)/n)` is `1<<PROB_FRAC`
|
||||
// only when `n` divides it: for n = 3 it is 65_535, not 65_536. A
|
||||
// denormalised distribution here becomes a denormalised CDF, and the
|
||||
// entropy decode then selects the wrong interval and desyncs the rest
|
||||
// of the stream — the exact failure SPEC §7 exists to prevent.
|
||||
//
|
||||
// So the invariant currently holds by unreachability rather than by
|
||||
// construction. Any change to the exp reduction that lets this fire
|
||||
// must distribute the remainder here the way the tail of this function
|
||||
// does.
|
||||
return vec![(1i64 << PROB_FRAC) / n as i64; n];
|
||||
}
|
||||
let mut probs: Vec<i64> = exps
|
||||
|
|
@ -79,6 +95,66 @@ pub fn softmax(x: &[i64], frac: u32) -> Vec<i64> {
|
|||
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
|
||||
|
|
|
|||
|
|
@ -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),
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
336
wai/wai-rs/src/wai_video_channel.rs
Normal file
336
wai/wai-rs/src/wai_video_channel.rs
Normal file
|
|
@ -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<u64> {
|
||||
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<ScheduleEntry>,
|
||||
pub window_start_ms: u64,
|
||||
pub window_end_ms: u64,
|
||||
/// Schedule indices on air in the window — recomputed in verify().
|
||||
pub aired: Vec<u64>,
|
||||
pub work_schedule_ops: u64,
|
||||
pub joules_micro: u64,
|
||||
pub energy_provenance: Option<EnergyProvenance>,
|
||||
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<u8> {
|
||||
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<String>,
|
||||
channel_id: impl Into<String>,
|
||||
schedule: Vec<ScheduleEntry>,
|
||||
window_start_ms: u64,
|
||||
window_end_ms: u64,
|
||||
joules_micro: u64,
|
||||
energy_provenance: Option<EnergyProvenance>,
|
||||
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<ScheduleEntry> {
|
||||
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::<Vec<_>>(), ["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");
|
||||
}
|
||||
}
|
||||
363
wai/wai-rs/src/wai_video_keys.rs
Normal file
363
wai/wai-rs/src/wai_video_keys.rs
Normal file
|
|
@ -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<EnergyProvenance>,
|
||||
/// 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<u8> {
|
||||
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<String>,
|
||||
key_id: [u8; 16],
|
||||
content_id: impl Into<String>,
|
||||
drm: DrmSystem,
|
||||
required_entitlement: impl Into<String>,
|
||||
issued_epoch: u64,
|
||||
expiry_epoch: u64,
|
||||
released_key: &[u8],
|
||||
joules_micro: u64,
|
||||
energy_provenance: Option<EnergyProvenance>,
|
||||
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());
|
||||
}
|
||||
}
|
||||
503
wai/wai-rs/src/wai_video_manifest.rs
Normal file
503
wai/wai-rs/src/wai_video_manifest.rs
Normal file
|
|
@ -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<String>,
|
||||
}
|
||||
|
||||
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<String>,
|
||||
/// 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<Segment>,
|
||||
/// 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<EnergyProvenance>,
|
||||
/// 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<u8> {
|
||||
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<String>,
|
||||
class: SessionClass,
|
||||
segments: Vec<Segment>,
|
||||
viewers_served: u64,
|
||||
joules_micro: u64,
|
||||
energy_provenance: Option<EnergyProvenance>,
|
||||
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<Segment> {
|
||||
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());
|
||||
}
|
||||
}
|
||||
368
wai/wai-rs/src/wai_video_package.rs
Normal file
368
wai/wai-rs/src/wai_video_package.rs
Normal file
|
|
@ -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<SegmentEntry> {
|
||||
let mut out = Vec::new();
|
||||
let mut cur: Vec<Gop> = Vec::new();
|
||||
let mut dur = 0u64;
|
||||
let mut bytes = 0u64;
|
||||
let mut close = |cur: &mut Vec<Gop>, dur: &mut u64, bytes: &mut u64, out: &mut Vec<SegmentEntry>| {
|
||||
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<SegmentEntry>,
|
||||
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<EnergyProvenance>,
|
||||
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<u8> {
|
||||
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<String>,
|
||||
asset_id: impl Into<String>,
|
||||
segments: Vec<SegmentEntry>,
|
||||
joules_micro: u64,
|
||||
energy_provenance: Option<EnergyProvenance>,
|
||||
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::<u64>() {
|
||||
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<Gop<'static>> {
|
||||
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");
|
||||
}
|
||||
}
|
||||
142
wai/wai-rs/src/wai_video_policy.rs
Normal file
142
wai/wai-rs/src/wai_video_policy.rs
Normal file
|
|
@ -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<Impression> {
|
||||
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");
|
||||
}
|
||||
324
wai/wai-rs/src/wai_video_ssai.rs
Normal file
324
wai/wai-rs/src/wai_video_ssai.rs
Normal file
|
|
@ -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<Impression>,
|
||||
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<EnergyProvenance>,
|
||||
/// 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<u8> {
|
||||
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<String>,
|
||||
avail_id: impl Into<String>,
|
||||
manifest_hash: [u8; 32],
|
||||
pod_hash: [u8; 32],
|
||||
impressions: Vec<Impression>,
|
||||
work_decide_ops: u64,
|
||||
joules_micro: u64,
|
||||
energy_provenance: Option<EnergyProvenance>,
|
||||
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<AdCandidate> {
|
||||
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::<Vec<_>>(), ["ad-a", "ad-b"]);
|
||||
assert_eq!(a.iter().map(|i| i.price_micros).sum::<u64>(), 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");
|
||||
}
|
||||
}
|
||||
7
wai/wai-verify/Cargo.lock
generated
Normal file
7
wai/wai-verify/Cargo.lock
generated
Normal file
|
|
@ -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"
|
||||
18
wai/wai-verify/Cargo.toml
Normal file
18
wai/wai-verify/Cargo.toml
Normal file
|
|
@ -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.
|
||||
37
wai/wai-verify/src/lib.rs
Normal file
37
wai/wai-verify/src/lib.rs
Normal file
|
|
@ -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;
|
||||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
270
wai/wai-web/src/video_ott.rs
Normal file
270
wai/wai-web/src/video_ott.rs
Normal file
|
|
@ -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<Segment> {
|
||||
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<String> = 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<String> = self
|
||||
.receipt
|
||||
.impressions
|
||||
.iter()
|
||||
.map(|i| format!("[{},\"{}\",{},{}]", i.slot, i.ad_id, i.price_micros, i.quartiles_reached))
|
||||
.collect();
|
||||
format!("[{}]", rows.join(","))
|
||||
}
|
||||
}
|
||||
Loading…
Reference in a new issue