From ddc4613a88d78304588012e3d4fa75067d6a7ef5 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 3 Sep 2026 14:44:58 -0400 Subject: [PATCH 01/15] =?UTF-8?q?feat(wai):=20wai.video.manifest=20?= =?UTF-8?q?=E2=80=94=20attested=20per-session=20manifest=20(OTT=20ingest?= =?UTF-8?q?=20=C2=A71)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ingests the OTT delivery layer as a WAI capability. A personalised HLS manifest (SSAI ads stitched at EXT-X-DISCONTINUITY, blackouts + geo enforced) is 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 binding the JCP grant (capability, joule ceiling, funds_ceiling = ad budget), the composition, the stitched ads and the policy applied. The efficiency is a checkable fact, not a slogan: because the manifest is a pure function of the class, one generation serves every viewer of that class, so uj_per_viewer is an amortised energy a 1:1-unique generator cannot report below its per-viewer cost. manifest_hash == hash(render(segments)) and session_class_hash are recomputable by anyone holding the bytes; only joules_micro is measured-attested. Same honesty ladder and receipt idiom as video_receipt; reuses the world Merkle + Ed25519 and the GrantRef from quantum_ops (no pixel-decode dependency). wai_video_manifest.rs + SPEC §5 registration; feature `video_manifest`. Tests: seal/verify roundtrip, ad-tamper rejection, class-dedup determinism, amortised efficiency metric, energy-label discipline. Co-Authored-By: Claude Opus 4.8 --- wai/SPEC.md | 1 + wai/wai-rs/Cargo.toml | 4 + wai/wai-rs/src/lib.rs | 8 + wai/wai-rs/src/wai_video_manifest.rs | 500 +++++++++++++++++++++++++++ 4 files changed, 513 insertions(+) create mode 100644 wai/wai-rs/src/wai_video_manifest.rs diff --git a/wai/SPEC.md b/wai/SPEC.md index 4810b7583..6f622831e 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -211,6 +211,7 @@ 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` | **Sink-architecture note:** the inter-frame neural video codecs (DCVC-RT, DCVC-FM) decode through `ort` and are **CPU-capable** for native sinks — diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index 9ad85b2e6..c08b6c5fd 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -162,6 +162,10 @@ quantum_receipt = ["quantum", "world"] # 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. +video_manifest = ["quantum_ops"] # Balanced-ternary matrix-product-state transform (`wai.ternary.tt`, # extensions/ternary-tt): quantum-INSPIRED (tensor-network) compression whose # novel delta is an INTEGER core scale — the whole decode is pure i64/i128, so a diff --git a/wai/wai-rs/src/lib.rs b/wai/wai-rs/src/lib.rs index bba1e36e2..15033c242 100644 --- a/wai/wai-rs/src/lib.rs +++ b/wai/wai-rs/src/lib.rs @@ -258,6 +258,14 @@ pub mod ternary_receipt; #[cfg(feature = "quantum_ops")] pub mod 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; + // Deterministic autonomous CALIBRATION engines (extensions/quantum-ops § Calibration): // a fixed-point qubit-device simulator + autonomous tune-up algorithms (Rabi π-pulse) // — the software capability the quantum-control vendors sell (autonomous gate tune-up), diff --git a/wai/wai-rs/src/wai_video_manifest.rs b/wai/wai-rs/src/wai_video_manifest.rs new file mode 100644 index 000000000..97e5504a2 --- /dev/null +++ b/wai/wai-rs/src/wai_video_manifest.rs @@ -0,0 +1,500 @@ +//! 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", + } + } + fn tag(self) -> u8 { + match self { + EnergyProvenance::HwShunt => 1, + EnergyProvenance::ModelBased => 2, + EnergyProvenance::Estimator => 3, + } + } +} + +/// Whether a segment carries programme content or a stitched ad. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum SegmentKind { + Content, + Ad, +} + +impl SegmentKind { + fn tag(self) -> u8 { + match self { + SegmentKind::Content => 1, + SegmentKind::Ad => 2, + } + } +} + +/// One entry in the ordered manifest composition. +/// +/// `ad_id.is_some()` iff `kind == Ad`; [`ManifestReceipt::verify`] rejects any +/// other combination, so the monetisation audit (the ad-bearing segments) is a +/// single source of truth rather than a second list that could disagree. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Segment { + pub index: u64, + pub kind: SegmentKind, + /// The segment URI as it appears in the manifest (content or ad). + pub uri: String, + pub duration_ms: u64, + /// Present exactly for ad segments — the ad decision this break resolved to. + pub ad_id: Option, +} + +impl Segment { + fn leaf(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_SEG); + h.update(&self.index.to_be_bytes()); + h.update(&[self.kind.tag()]); + h.update(&self.duration_ms.to_be_bytes()); + h.update(&(self.uri.len() as u32).to_be_bytes()); + h.update(self.uri.as_bytes()); + match &self.ad_id { + Some(a) => { + h.update(&[1]); + h.update(&(a.len() as u32).to_be_bytes()); + h.update(a.as_bytes()); + } + None => { + h.update(&[0]); + } + } + *h.finalize().as_bytes() + } +} + +/// The deterministic inputs that define a manifest. Its hash is the dedup key: +/// two sessions with the same class render to byte-identical manifests, so a +/// platform generates once and serves many. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct SessionClass { + pub content_id: String, + /// Entitlement class, e.g. `"svod:tier2"` — never a viewer identity. + pub entitlement: String, + /// ISO-3166 country the geo rules resolved against. + pub geo: String, + /// The active blackout ids. Order-independent: hashed sorted+deduped. + pub blackouts: Vec, + /// The ad-decision pod this class resolved to (the SSAI decision key). + pub ad_pod_id: String, + /// The manifest time-window bucket (a live window index or `0` for VOD). + pub window: u64, +} + +impl SessionClass { + /// Domain-separated, canonical, order-independent over `blackouts`. + pub fn class_hash(&self) -> [u8; 32] { + let mut bs: Vec<&str> = self.blackouts.iter().map(String::as_str).collect(); + bs.sort_unstable(); + bs.dedup(); + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_CLASS); + for s in [ + self.content_id.as_str(), + self.entitlement.as_str(), + self.geo.as_str(), + self.ad_pod_id.as_str(), + ] { + h.update(&(s.len() as u32).to_be_bytes()); + h.update(s.as_bytes()); + } + h.update(&(bs.len() as u32).to_be_bytes()); + for s in bs { + h.update(&(s.len() as u32).to_be_bytes()); + h.update(s.as_bytes()); + } + h.update(&self.window.to_be_bytes()); + *h.finalize().as_bytes() + } +} + +/// Deterministic HLS rendering: the manifest is a pure function of the ordered +/// segments, so `hash(render(segments))` is a stable identity a verifier can +/// recompute. Ad segments carry an `EXT-X-DISCONTINUITY` — the real SSAI splice +/// marker — so the stitched breaks are visible in the bytes, not only the +/// receipt. Target duration is derived (ceil of the longest segment) rather than +/// supplied, so nothing outside `segments` can move the output. +pub fn render_hls(segments: &[Segment]) -> String { + let target = segments + .iter() + .map(|s| s.duration_ms.div_ceil(1000)) + .max() + .unwrap_or(0); + let mut out = String::new(); + out.push_str("#EXTM3U\n#EXT-X-VERSION:6\n"); + out.push_str(&format!("#EXT-X-TARGETDURATION:{target}\n")); + out.push_str("#EXT-X-MEDIA-SEQUENCE:0\n"); + for s in segments { + if s.kind == SegmentKind::Ad { + out.push_str("#EXT-X-DISCONTINUITY\n"); + } + // Fixed 3-dp seconds so the byte output is stable across platforms. + out.push_str(&format!("#EXTINF:{}.{:03},\n", s.duration_ms / 1000, s.duration_ms % 1000)); + out.push_str(&s.uri); + out.push('\n'); + } + out.push_str("#EXT-X-ENDLIST\n"); + out +} + +/// A signed, energy-accounted per-session manifest. +#[derive(Clone, Debug, PartialEq)] +pub struct ManifestReceipt { + /// Identity: BLAKE3 over the rendered manifest bytes. Verifiable by hashing + /// the bytes a player received. + pub manifest_hash: [u8; 32], + /// The dedup key — BLAKE3 over [`SessionClass`]. Verifiable from `class`. + pub session_class_hash: [u8; 32], + /// Carried so a verifier recomputes the class hash and reads the policy + /// (entitlement, geo, blackouts) that was enforced. + pub class: SessionClass, + /// The ordered composition. `manifest_hash == hash(render(segments))`. + pub segments: Vec, + /// Merkle root over the segment leaves — the family's shared helper. + pub merkle_root: [u8; 32], + /// Portable compose work: the number of segments composed. Verified by + /// recomputation, so it cannot be inflated to flatter an energy figure. + pub work_compose_ops: u64, + /// How many sessions this one generation served (the dedup multiplier). + /// `>= 1`. The class determinism is what makes this honest: every one of + /// them received the same bytes. + pub viewers_served: u64, + /// Marginal microjoules the generation sink spent (`0` = unmetered). + /// Attested by the signature, not independently verifiable. + pub joules_micro: u64, + /// How `joules_micro` was acquired. `None` iff unmetered. + pub energy_provenance: Option, + /// The JCP grant this session ran under — capability, joule ceiling, and + /// `funds_ceiling` (the ad budget). Bound in, as the quantum receipts do. + pub grant: GrantRef, + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +impl ManifestReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&self.manifest_hash); + o.extend_from_slice(&self.session_class_hash); + o.extend_from_slice(&self.merkle_root); + o.extend_from_slice(&self.work_compose_ops.to_be_bytes()); + o.extend_from_slice(&self.viewers_served.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, EnergyProvenance::tag)); + // Grant binding: hash, capability, both ceilings. + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&(self.segments.len() as u64).to_be_bytes()); + for s in &self.segments { + o.extend_from_slice(&s.leaf()); + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Compose a class into a manifest and seal a receipt over what it renders. + /// + /// The manifest hash is taken from the rendering of `segments` here, so the + /// sealed identity cannot be a manifest the segments do not produce. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + class: SessionClass, + segments: Vec, + viewers_served: u64, + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> ManifestReceipt { + let manifest_hash = *blake3::hash(render_hls(&segments).as_bytes()).as_bytes(); + let session_class_hash = class.class_hash(); + let leaves: Vec<[u8; 32]> = segments.iter().map(Segment::leaf).collect(); + let mut r = ManifestReceipt { + manifest_hash, + session_class_hash, + class, + work_compose_ops: segments.len() as u64, + merkle_root: merkle_root(&leaves), + segments, + viewers_served, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + internal consistency. Confirms the manifest is exactly what + /// the carried segments render to, the class hash follows from `class`, the + /// Merkle root and work figure follow from the segments, the ad/kind + /// coupling holds, and the energy figure and its label stand or fall + /// together. Does **not** by itself prove the bytes a player received — + /// [`ManifestReceipt::verify_render`] does that. + pub fn verify(&self) -> bool { + let leaves: Vec<[u8; 32]> = self.segments.iter().map(Segment::leaf).collect(); + if merkle_root(&leaves) != self.merkle_root { + return false; + } + if self.class.class_hash() != self.session_class_hash { + return false; + } + if *blake3::hash(render_hls(&self.segments).as_bytes()).as_bytes() != self.manifest_hash { + return false; + } + if self.work_compose_ops != self.segments.len() as u64 { + return false; + } + if self.viewers_served == 0 { + return false; + } + for (i, s) in self.segments.iter().enumerate() { + if s.index != i as u64 { + return false; + } + if (s.kind == SegmentKind::Ad) != s.ad_id.is_some() { + return false; + } + } + // A figure and its acquisition class stand or fall together: an + // unlabelled non-zero figure is uncomparable; a labelled zero claims a + // measurement that did not happen. Both rejected. + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// The independent check: the bytes a player received hash to + /// `manifest_hash`, and re-rendering the sealed segments reproduces those + /// exact bytes. A verifier need not trust the generating machine — the + /// manifest is a pure function of the composition. `joules_micro` is + /// untouched; it is not reproducible and is not meant to be. + pub fn verify_render(&self, rendered_manifest: &[u8]) -> bool { + if *blake3::hash(rendered_manifest).as_bytes() != self.manifest_hash { + return false; + } + if render_hls(&self.segments).as_bytes() != rendered_manifest { + return false; + } + self.verify() + } + + /// The stitched ads — the monetisation audit, derived from the one source of + /// truth (ad-bearing segments) so it cannot disagree with the manifest. + /// Each is `(break_index, ad_id, duration_ms)`. + pub fn ad_insertions(&self) -> Vec<(u64, &str, u64)> { + self.segments + .iter() + .filter_map(|s| s.ad_id.as_deref().map(|a| (s.index, a, s.duration_ms))) + .collect() + } + + /// Amortised microjoules per viewer served, **with** the acquisition class — + /// the only comparable form. This is the efficiency the class-dedup buys, + /// and it is honest precisely because the manifest determinism is verifiable: + /// every one of `viewers_served` viewers received identical bytes from one + /// generation. `None` when unmetered. + pub fn uj_per_viewer(&self) -> Option<(f64, EnergyProvenance)> { + match (self.energy_provenance, self.viewers_served) { + (Some(p), v) if self.joules_micro > 0 && v > 0 => { + Some((self.joules_micro as f64 / v as f64, p)) + } + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + fn class() -> SessionClass { + SessionClass { + content_id: "asset-abc".into(), + entitlement: "svod:tier2".into(), + geo: "US".into(), + blackouts: vec!["nfl-home-market".into()], + ad_pod_id: "pod-42".into(), + window: 7, + } + } + + fn segments() -> Vec { + vec![ + Segment { index: 0, kind: SegmentKind::Content, uri: "seg0.ts".into(), duration_ms: 6000, ad_id: None }, + Segment { index: 1, kind: SegmentKind::Ad, uri: "ad/xyz/0.ts".into(), duration_ms: 4000, ad_id: Some("ad-xyz".into()) }, + Segment { index: 2, kind: SegmentKind::Content, uri: "seg1.ts".into(), duration_ms: 6000, ad_id: None }, + ] + } + + #[test] + fn seal_verify_roundtrip() { + let g = GrantRef { grant_hash: [9u8; 32], capability: "video.manifest".into(), joule_ceiling_micro: 5_000_000, funds_ceiling: Some(250) }; + let r = ManifestReceipt::seal(&key(1), "did:key:origin", class(), segments(), 12_000, 800, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + // The bytes a player received verify against the receipt. + let rendered = render_hls(&r.segments); + assert!(r.verify_render(rendered.as_bytes())); + // Monetisation audit is exactly the ad segment. + assert_eq!(r.ad_insertions(), vec![(1, "ad-xyz", 4000)]); + } + + #[test] + fn tamper_on_ad_is_rejected() { + let g = GrantRef::unbounded("video.manifest"); + let mut r = ManifestReceipt::seal(&key(2), "did:key:o", class(), segments(), 3, 0, None, g, None); + assert!(r.verify()); + // Swap the ad for a different creative without re-signing. + r.segments[1].ad_id = Some("ad-hijack".into()); + r.segments[1].uri = "ad/hijack/0.ts".into(); + assert!(!r.verify(), "a swapped ad must break the receipt"); + } + + #[test] + fn class_determinism_enables_dedup() { + // Two independent sessions of the same class render byte-identical + // manifests: the dedup that makes uj_per_viewer honest. + let a = render_hls(&segments()); + let b = render_hls(&segments()); + assert_eq!(a, b); + assert_eq!(class().class_hash(), class().class_hash()); + // Ad segments surface as HLS discontinuities in the bytes themselves. + assert!(a.contains("#EXT-X-DISCONTINUITY")); + } + + #[test] + fn efficiency_is_amortised_across_the_class() { + let g = GrantRef::unbounded("video.manifest"); + // One 9000 uJ generation served 300 viewers of the class. + let r = ManifestReceipt::seal(&key(3), "o", class(), segments(), 300, 9000, Some(EnergyProvenance::ModelBased), g, None); + let (uj, prov) = r.uj_per_viewer().unwrap(); + assert_eq!(prov, EnergyProvenance::ModelBased); + assert!((uj - 30.0).abs() < 1e-9, "9000 uJ / 300 viewers = 30 uJ/viewer"); + } + + #[test] + fn labelled_zero_and_unlabelled_figure_are_rejected() { + let g = GrantRef::unbounded("video.manifest"); + let mut r = ManifestReceipt::seal(&key(4), "o", class(), segments(), 1, 500, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + // Unlabelled non-zero: uncomparable number. + r.energy_provenance = None; + r.sig = key(4).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify()); + // Labelled zero: a measurement that did not happen. + r.joules_micro = 0; + r.energy_provenance = Some(EnergyProvenance::HwShunt); + r.sig = key(4).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify()); + } +} -- 2.54.0 (Apple Git-157) From ab98c56185b0d0ba33fb56e1d63a33e7298c125f Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 3 Sep 2026 14:56:41 -0400 Subject: [PATCH 02/15] =?UTF-8?q?feat(wai):=20wai.video.ssai=20=E2=80=94?= =?UTF-8?q?=20attested=20ad=20insertion=20+=20per-impression=20receipt=20(?= =?UTF-8?q?OTT=20ingest=20=C2=A72)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The monetisation half of the ingest. SSAI's real problem is proof, not stitching: buyer and seller reconcile impression counts from separate logs neither can check. This makes an ad break a signed, budget-bounded, per-impression record both sides verify from the same bytes. - Deterministic decision (`decide`): greedy by price within the avail duration and funds remaining — a pure function of the pod, reproducible by an auditor; the pod is bound by `pod_hash`. - Per-impression receipt: each filled slot carries the served `creative_hash` and the VAST quartile it reached, so a swapped creative or a padded count breaks the signature. - Budget enforcement is a checkable fact: `budget_spent_micros` is recomputed from the billable (started) impressions and rejected over the grant's `funds_ceiling` — overspend cannot be signed. Links to wai.video.manifest by `manifest_hash` and chains from its receipt; reuses that module's EnergyProvenance and the world Merkle + Ed25519 + GrantRef. `uj_per_impression` amortises decision energy over billable impressions. Only `joules_micro` is measured-attested. wai_video_ssai.rs + SPEC §5; feature `video_ssai`. 5 tests: deterministic bounded decision, only-started-ads-bill, overspend-cannot-be-signed, swapped-creative rejection, amortised efficiency. (Manifest module's energy tag made pub for reuse; its 5 tests still green — 10 pass total.) Co-Authored-By: Claude Opus 4.8 --- wai/SPEC.md | 1 + wai/wai-rs/Cargo.toml | 3 + wai/wai-rs/src/lib.rs | 8 + wai/wai-rs/src/wai_video_manifest.rs | 7 +- wai/wai-rs/src/wai_video_ssai.rs | 391 +++++++++++++++++++++++++++ 5 files changed, 408 insertions(+), 2 deletions(-) create mode 100644 wai/wai-rs/src/wai_video_ssai.rs diff --git a/wai/SPEC.md b/wai/SPEC.md index 6f622831e..8ec5d3602 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -212,6 +212,7 @@ decode route for each is implemented in the reference sink (see the | `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` | **Sink-architecture note:** the inter-frame neural video codecs (DCVC-RT, DCVC-FM) decode through `ort` and are **CPU-capable** for native sinks — diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index c08b6c5fd..a30e90ba4 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -166,6 +166,9 @@ video_receipt = ["video_int", "world"] # 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. video_manifest = ["quantum_ops"] +# wai.video.ssai — attested ad decisioning + per-impression receipt. Reuses the +# manifest module's EnergyProvenance + the GrantRef/Merkle/Ed25519 floor. +video_ssai = ["video_manifest"] # Balanced-ternary matrix-product-state transform (`wai.ternary.tt`, # extensions/ternary-tt): quantum-INSPIRED (tensor-network) compression whose # novel delta is an INTEGER core scale — the whole decode is pure i64/i128, so a diff --git a/wai/wai-rs/src/lib.rs b/wai/wai-rs/src/lib.rs index 15033c242..facc49409 100644 --- a/wai/wai-rs/src/lib.rs +++ b/wai/wai-rs/src/lib.rs @@ -266,6 +266,14 @@ pub mod quantum_ops; #[cfg(feature = "video_manifest")] pub mod wai_video_manifest; +// 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. +#[cfg(feature = "video_ssai")] +pub mod wai_video_ssai; + // Deterministic autonomous CALIBRATION engines (extensions/quantum-ops § Calibration): // a fixed-point qubit-device simulator + autonomous tune-up algorithms (Rabi π-pulse) // — the software capability the quantum-control vendors sell (autonomous gate tune-up), diff --git a/wai/wai-rs/src/wai_video_manifest.rs b/wai/wai-rs/src/wai_video_manifest.rs index 97e5504a2..e64b67bfa 100644 --- a/wai/wai-rs/src/wai_video_manifest.rs +++ b/wai/wai-rs/src/wai_video_manifest.rs @@ -66,7 +66,10 @@ impl EnergyProvenance { EnergyProvenance::Estimator => "Estimator", } } - fn tag(self) -> u8 { + /// 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, @@ -249,7 +252,7 @@ impl ManifestReceipt { 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)); + 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()); diff --git a/wai/wai-rs/src/wai_video_ssai.rs b/wai/wai-rs/src/wai_video_ssai.rs new file mode 100644 index 000000000..e4d4b8082 --- /dev/null +++ b/wai/wai-rs/src/wai_video_ssai.rs @@ -0,0 +1,391 @@ +//! 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; +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"; + +/// 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, +} + +/// 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() +} + +/// 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 + } + + 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() + } +} + +/// Deterministic decision: fill up to `avail_slots` of a `avail_duration_ms` +/// break from `candidates`, never exceeding `funds_remaining_micros`. +/// +/// Greedy by price descending, ties broken by `ad_id` ascending — a pure +/// function of its inputs, so an auditor reproduces the fill exactly. Each +/// selected ad must fit the remaining avail time and the remaining funds. Slots +/// are returned as [`Impression`]s with `quartiles_reached = 0`; the caller +/// raises each as its beacons arrive, then seals. +pub fn decide( + candidates: &[AdCandidate], + avail_slots: u64, + avail_duration_ms: u64, + funds_remaining_micros: u64, +) -> Vec { + let mut order: Vec<&AdCandidate> = candidates.iter().collect(); + order.sort_by(|a, b| b.price_micros.cmp(&a.price_micros).then(a.ad_id.cmp(&b.ad_id))); + let mut out = Vec::new(); + let (mut time_left, mut funds_left) = (avail_duration_ms, funds_remaining_micros); + for c in order { + if out.len() as u64 >= avail_slots { + break; + } + if c.duration_ms <= time_left && c.price_micros <= funds_left { + out.push(Impression { + slot: out.len() as u64, + ad_id: c.ad_id.clone(), + creative_hash: c.creative_hash, + duration_ms: c.duration_ms, + price_micros: c.price_micros, + quartiles_reached: 0, + }); + time_left -= c.duration_ms; + funds_left -= c.price_micros; + } + } + out +} + +/// A signed, budget-bounded, per-impression ad-break record. +#[derive(Clone, Debug, PartialEq)] +pub struct SsaiReceipt { + /// The ad break identity within its manifest. + pub avail_id: String, + /// The attested manifest this avail belongs to (`wai.video.manifest`). + pub manifest_hash: [u8; 32], + /// The candidate pod the decision ran over — the auditable decision input. + pub pod_hash: [u8; 32], + /// The filled slots and the completion their beacons confirmed. + pub impressions: Vec, + pub merkle_root: [u8; 32], + /// Σ price over *billable* impressions. Recomputed and ceiling-checked in + /// [`SsaiReceipt::verify`], so it is a fact, not an assertion. + pub budget_spent_micros: u64, + /// Candidates the decision considered — portable work, `>= impressions`. + pub work_decide_ops: u64, + pub joules_micro: u64, + pub energy_provenance: Option, + /// The grant this break ran under; `funds_ceiling` is the spend ceiling. + pub grant: GrantRef, + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +/// Σ price over billable impressions — the one definition of spend, used by both +/// `seal` and `verify` so they cannot disagree. +fn billable_spend(impressions: &[Impression]) -> u64 { + impressions.iter().filter(|i| i.is_billable()).map(|i| i.price_micros).sum() +} + +impl SsaiReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&(self.avail_id.len() as u32).to_be_bytes()); + o.extend_from_slice(self.avail_id.as_bytes()); + o.extend_from_slice(&self.manifest_hash); + o.extend_from_slice(&self.pod_hash); + o.extend_from_slice(&self.merkle_root); + o.extend_from_slice(&self.budget_spent_micros.to_be_bytes()); + o.extend_from_slice(&self.work_decide_ops.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, |p| p.tag_byte())); + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&(self.impressions.len() as u64).to_be_bytes()); + for i in &self.impressions { + o.extend_from_slice(&i.leaf()); + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Seal an ad break. `budget_spent_micros` is computed from the impressions + /// here, so it cannot be set to a figure the slots do not support. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + avail_id: impl Into, + manifest_hash: [u8; 32], + pod_hash: [u8; 32], + impressions: Vec, + work_decide_ops: u64, + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> SsaiReceipt { + let leaves: Vec<[u8; 32]> = impressions.iter().map(Impression::leaf).collect(); + let mut r = SsaiReceipt { + avail_id: avail_id.into(), + manifest_hash, + pod_hash, + budget_spent_micros: billable_spend(&impressions), + merkle_root: merkle_root(&leaves), + impressions, + work_decide_ops, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + internal consistency: the Merkle root and the recomputed + /// billable spend must follow from the impressions, the spend must not + /// exceed the grant's `funds_ceiling`, the work figure must cover the slots, + /// slots must be contiguous, quartiles in range, and the energy figure and + /// its label must stand or fall together. + pub fn verify(&self) -> bool { + let leaves: Vec<[u8; 32]> = self.impressions.iter().map(Impression::leaf).collect(); + if merkle_root(&leaves) != self.merkle_root { + return false; + } + // Spend is recomputed, not trusted — a tampered figure or a swapped + // creative (which changes a leaf) is caught here. + if billable_spend(&self.impressions) != self.budget_spent_micros { + return false; + } + // Overspend cannot be signed. + if let Some(ceiling) = self.grant.funds_ceiling { + if self.budget_spent_micros > ceiling { + return false; + } + } + if self.work_decide_ops < self.impressions.len() as u64 { + return false; + } + for (i, imp) in self.impressions.iter().enumerate() { + if imp.slot != i as u64 { + return false; + } + if imp.quartiles_reached > 5 { + return false; + } + } + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// The billable impressions — those that started rendering. + pub fn billable_impressions(&self) -> usize { + self.impressions.iter().filter(|i| i.is_billable()).count() + } + + /// Amortised microjoules of decision energy per billable impression, with + /// its acquisition class — the only comparable form. `None` when unmetered + /// or when nothing billable played. + pub fn uj_per_impression(&self) -> Option<(f64, EnergyProvenance)> { + let n = self.billable_impressions() as u64; + match (self.energy_provenance, n) { + (Some(p), v) if self.joules_micro > 0 && v > 0 => { + Some((self.joules_micro as f64 / v as f64, p)) + } + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + fn pod() -> Vec { + vec![ + AdCandidate { ad_id: "ad-a".into(), creative_hash: [1u8; 32], duration_ms: 15000, price_micros: 40_000 }, + AdCandidate { ad_id: "ad-b".into(), creative_hash: [2u8; 32], duration_ms: 15000, price_micros: 30_000 }, + AdCandidate { ad_id: "ad-c".into(), creative_hash: [3u8; 32], duration_ms: 30000, price_micros: 90_000 }, + ] + } + + #[test] + fn decision_is_deterministic_and_bounded() { + // 30s avail, 2 slots, budget 80_000: ad-c (90k) is too dear; greedy by + // price takes ad-a (40k) then ad-b (30k), total 70k, both 15s -> fit. + let a = decide(&pod(), 2, 30_000, 80_000); + let b = decide(&pod(), 2, 30_000, 80_000); + assert_eq!(a, b, "decision must be a pure function of its inputs"); + assert_eq!(a.iter().map(|i| i.ad_id.as_str()).collect::>(), ["ad-a", "ad-b"]); + assert_eq!(a.iter().map(|i| i.price_micros).sum::(), 70_000); + } + + #[test] + fn seal_verify_and_only_started_ads_bill() { + let mut imps = decide(&pod(), 2, 30_000, 80_000); + imps[0].quartiles_reached = 5; // ad-a played to complete -> billable + imps[1].quartiles_reached = 0; // ad-b never rendered -> not billed + let g = GrantRef { grant_hash: [7u8; 32], capability: "video.ssai".into(), joule_ceiling_micro: 1_000_000, funds_ceiling: Some(80_000) }; + let r = SsaiReceipt::seal(&key(1), "did:key:ssai", "avail-1", [9u8; 32], pod_hash(&pod()), imps, 3, 500, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + assert_eq!(r.billable_impressions(), 1); + assert_eq!(r.budget_spent_micros, 40_000, "only the started ad bills"); + } + + #[test] + fn overspend_cannot_be_signed() { + // Both ads billable = 70_000, but grant ceiling is 50_000. + let mut imps = decide(&pod(), 2, 30_000, 80_000); + imps[0].quartiles_reached = 1; + imps[1].quartiles_reached = 1; + let g = GrantRef { grant_hash: [7u8; 32], capability: "video.ssai".into(), joule_ceiling_micro: 0, funds_ceiling: Some(50_000) }; + let r = SsaiReceipt::seal(&key(2), "o", "avail-2", [9u8; 32], pod_hash(&pod()), imps, 3, 0, None, g, None); + assert!(!r.verify(), "spend 70_000 over a 50_000 ceiling must not verify"); + } + + #[test] + fn swapped_creative_breaks_the_receipt() { + let mut imps = decide(&pod(), 1, 30_000, 100_000); + imps[0].quartiles_reached = 5; + let g = GrantRef::unbounded("video.ssai"); + let mut r = SsaiReceipt::seal(&key(3), "o", "avail-3", [9u8; 32], pod_hash(&pod()), imps, 3, 0, None, g, None); + assert!(r.verify()); + r.impressions[0].creative_hash = [0xAA; 32]; // serve a different creative than billed + assert!(!r.verify(), "a swapped creative must break the receipt"); + } + + #[test] + fn efficiency_amortises_over_billable_impressions() { + let mut imps = decide(&pod(), 2, 30_000, 80_000); + imps[0].quartiles_reached = 5; + imps[1].quartiles_reached = 5; + let g = GrantRef::unbounded("video.ssai"); + let r = SsaiReceipt::seal(&key(4), "o", "avail-4", [9u8; 32], pod_hash(&pod()), imps, 3, 900, Some(EnergyProvenance::ModelBased), g, None); + let (uj, prov) = r.uj_per_impression().unwrap(); + assert_eq!(prov, EnergyProvenance::ModelBased); + assert!((uj - 450.0).abs() < 1e-9, "900 uJ / 2 impressions = 450 uJ each"); + } +} -- 2.54.0 (Apple Git-157) From 1ffe9a0a2f1330a7ebb74d17f3f4146c85a2f0df Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 3 Sep 2026 15:01:03 -0400 Subject: [PATCH 03/15] =?UTF-8?q?feat(wai):=20wai.video.keys=20=E2=80=94?= =?UTF-8?q?=20attested=20content-key=20release=20(OTT=20ingest=20=C2=A73)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The content-protection layer. The DRM systems wrap and deliver the key; what none leave is a portable record of *why* a key was released. This makes every release — and every refusal — a signed receipt whose decision a verifier recomputes from the bound inputs. - decision-equivalence: verify() re-runs decide_release over the receipt's own (grant capability, required entitlement, issued, expiry) and rejects any stored outcome the policy would not produce. "Keys went only to entitled, unexpired sessions" becomes checkable against the signed log. - The key never enters the receipt: a granted release carries a BLAKE3 key_commit proving which key was released; a refusal carries none, and the granted-iff-committed coupling is enforced. - A refusal is a first-class signed record, not a silent drop. Reuses the manifest floor (EnergyProvenance, GrantRef, Ed25519); links to a manifest via parent_receipt_hash. Only joules_micro is measured-attested. wai_video_keys.rs + SPEC §5; feature `video_keys`. 5 tests: entitled release + key commitment, wrong-entitlement refusal, expired denial, misreported decision rejected, granted-without-commitment rejected. Co-Authored-By: Claude Opus 4.8 --- wai/SPEC.md | 1 + wai/wai-rs/Cargo.toml | 4 + wai/wai-rs/src/lib.rs | 8 + wai/wai-rs/src/wai_video_keys.rs | 363 +++++++++++++++++++++++++++++++ 4 files changed, 376 insertions(+) create mode 100644 wai/wai-rs/src/wai_video_keys.rs diff --git a/wai/SPEC.md b/wai/SPEC.md index 8ec5d3602..beeeb16d4 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -213,6 +213,7 @@ decode route for each is implemented in the reference sink (see the | `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` | **Sink-architecture note:** the inter-frame neural video codecs (DCVC-RT, DCVC-FM) decode through `ort` and are **CPU-capable** for native sinks — diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index a30e90ba4..528ed7d88 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -169,6 +169,10 @@ video_manifest = ["quantum_ops"] # wai.video.ssai — attested ad decisioning + per-impression receipt. Reuses the # manifest module's EnergyProvenance + the GrantRef/Merkle/Ed25519 floor. video_ssai = ["video_manifest"] +# 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"] # Balanced-ternary matrix-product-state transform (`wai.ternary.tt`, # extensions/ternary-tt): quantum-INSPIRED (tensor-network) compression whose # novel delta is an INTEGER core scale — the whole decode is pure i64/i128, so a diff --git a/wai/wai-rs/src/lib.rs b/wai/wai-rs/src/lib.rs index facc49409..34d77527e 100644 --- a/wai/wai-rs/src/lib.rs +++ b/wai/wai-rs/src/lib.rs @@ -274,6 +274,14 @@ pub mod wai_video_manifest; #[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 autonomous CALIBRATION engines (extensions/quantum-ops § Calibration): // a fixed-point qubit-device simulator + autonomous tune-up algorithms (Rabi π-pulse) // — the software capability the quantum-control vendors sell (autonomous gate tune-up), diff --git a/wai/wai-rs/src/wai_video_keys.rs b/wai/wai-rs/src/wai_video_keys.rs new file mode 100644 index 000000000..ae0980cfe --- /dev/null +++ b/wai/wai-rs/src/wai_video_keys.rs @@ -0,0 +1,363 @@ +//! Attested content-key release — `wai.video.keys`. +//! +//! The DRM systems (Widevine, PlayReady, FairPlay) wrap and deliver the content +//! key; what none of them leave is a portable, checkable record of *why* a key +//! was released — under which entitlement, before which expiry. This profile is +//! that record: every release, and every refusal, is a signed receipt whose +//! decision a verifier **recomputes** from the bound inputs. +//! +//! The decision is a pure function of `(grant capability, required entitlement, +//! issued time, expiry)`. [`KeyReleaseReceipt::verify`] re-runs [`decide_release`] +//! over the receipt's own fields and rejects any receipt whose stored decision +//! does not match — so "we released keys only to entitled, unexpired sessions" +//! stops being a policy assertion and becomes a fact a licensor can check +//! against the signed log. +//! +//! The key itself never enters the receipt. A granted release carries a +//! `key_commit` — BLAKE3 over the released key bytes — so a verifier confirms +//! *which* key was released (it matches the KID's key on the encrypted content) +//! without the record ever carrying key material. A refusal carries no +//! commitment, and the coupling is enforced, not merely documented. +//! +//! Only `joules_micro` is measured-attested. Reuses the manifest module's +//! `EnergyProvenance` and the world Merkle floor's Ed25519 + `GrantRef`; links +//! to a manifest via `parent_receipt_hash`. Reuse, not reinvention. + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; + +use crate::quantum_ops::GrantRef; +use crate::wai_video_manifest::EnergyProvenance; + +const DOMAIN_RECEIPT: &[u8] = b"wai:video-keys-receipt\x01"; +const DOMAIN_RECEIPT_ID: &[u8] = b"wai:video-keys-receipt-id\x01"; +const DOMAIN_KEY: &[u8] = b"wai:video-keys-commit\x01"; + +/// The DRM system the release targets. Sealed so the record says which client +/// ecosystem the key went to. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum DrmSystem { + Widevine, + PlayReady, + FairPlay, + ClearKey, +} + +impl DrmSystem { + fn tag(self) -> u8 { + match self { + DrmSystem::Widevine => 1, + DrmSystem::PlayReady => 2, + DrmSystem::FairPlay => 3, + DrmSystem::ClearKey => 4, + } + } + pub fn label(self) -> &'static str { + match self { + DrmSystem::Widevine => "Widevine", + DrmSystem::PlayReady => "PlayReady", + DrmSystem::FairPlay => "FairPlay", + DrmSystem::ClearKey => "ClearKey", + } + } +} + +/// The outcome of a release decision — a grant *and* every refusal is a +/// first-class, signed record. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ReleaseDecision { + Granted, + DeniedNoEntitlement, + DeniedExpired, +} + +impl ReleaseDecision { + fn tag(self) -> u8 { + match self { + ReleaseDecision::Granted => 1, + ReleaseDecision::DeniedNoEntitlement => 2, + ReleaseDecision::DeniedExpired => 3, + } + } + pub fn label(self) -> &'static str { + match self { + ReleaseDecision::Granted => "Granted", + ReleaseDecision::DeniedNoEntitlement => "DeniedNoEntitlement", + ReleaseDecision::DeniedExpired => "DeniedExpired", + } + } + pub fn is_granted(self) -> bool { + self == ReleaseDecision::Granted + } +} + +/// The one definition of the policy, used by both the issuer and every verifier +/// so they cannot disagree. Entitlement is an exact class match; a granted key +/// requires the request to arrive at or before the entitlement's expiry. +pub fn decide_release( + grant_capability: &str, + required_entitlement: &str, + issued_epoch: u64, + expiry_epoch: u64, +) -> ReleaseDecision { + if grant_capability != required_entitlement { + return ReleaseDecision::DeniedNoEntitlement; + } + if issued_epoch > expiry_epoch { + return ReleaseDecision::DeniedExpired; + } + ReleaseDecision::Granted +} + +/// BLAKE3 commitment to released key bytes — proves *which* key without carrying +/// it. Domain-separated so it can never collide with another module's hash of +/// the same bytes. +pub fn key_commitment(key_bytes: &[u8]) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_KEY); + h.update(&(key_bytes.len() as u32).to_be_bytes()); + h.update(key_bytes); + *h.finalize().as_bytes() +} + +/// A signed content-key release decision. +#[derive(Clone, Debug, PartialEq)] +pub struct KeyReleaseReceipt { + /// The key identifier (KID) on the encrypted content. + pub key_id: [u8; 16], + pub content_id: String, + pub drm: DrmSystem, + /// The entitlement class the content demanded. + pub required_entitlement: String, + pub decision: ReleaseDecision, + /// BLAKE3 over the released key bytes — `Some` iff `decision` is `Granted`. + pub key_commit: Option<[u8; 32]>, + /// The entitlement window enforced, and when the decision was taken. + pub expiry_epoch: u64, + pub issued_epoch: u64, + pub joules_micro: u64, + pub energy_provenance: Option, + /// The grant presented; its `capability` is the entitlement checked. + pub grant: GrantRef, + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +impl KeyReleaseReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&self.key_id); + o.extend_from_slice(&(self.content_id.len() as u32).to_be_bytes()); + o.extend_from_slice(self.content_id.as_bytes()); + o.push(self.drm.tag()); + o.extend_from_slice(&(self.required_entitlement.len() as u32).to_be_bytes()); + o.extend_from_slice(self.required_entitlement.as_bytes()); + o.push(self.decision.tag()); + match self.key_commit { + Some(c) => { + o.push(1); + o.extend_from_slice(&c); + } + None => o.push(0), + } + o.extend_from_slice(&self.expiry_epoch.to_be_bytes()); + o.extend_from_slice(&self.issued_epoch.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, EnergyProvenance::tag_byte)); + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Evaluate the policy and seal the decision. The decision is computed here + /// from the grant and the request, so a receipt cannot claim an outcome the + /// policy would not produce; `released_key` is hashed into a commitment only + /// when the decision is `Granted`. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + key_id: [u8; 16], + content_id: impl Into, + drm: DrmSystem, + required_entitlement: impl Into, + issued_epoch: u64, + expiry_epoch: u64, + released_key: &[u8], + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> KeyReleaseReceipt { + let required_entitlement = required_entitlement.into(); + let decision = + decide_release(&grant.capability, &required_entitlement, issued_epoch, expiry_epoch); + let key_commit = decision.is_granted().then(|| key_commitment(released_key)); + let mut r = KeyReleaseReceipt { + key_id, + content_id: content_id.into(), + drm, + required_entitlement, + decision, + key_commit, + expiry_epoch, + issued_epoch, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + policy consistency. Re-runs [`decide_release`] over the + /// receipt's own fields and rejects any mismatch, enforces the + /// granted-iff-committed coupling, and holds the energy figure and its label + /// together. A refusal is a valid receipt; a *misreported* decision is not. + pub fn verify(&self) -> bool { + let recomputed = decide_release( + &self.grant.capability, + &self.required_entitlement, + self.issued_epoch, + self.expiry_epoch, + ); + if recomputed != self.decision { + return false; + } + if self.decision.is_granted() != self.key_commit.is_some() { + return false; + } + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// Confirm the released key this receipt commits to is the one the caller + /// holds — the licensor's check that the sealed commitment matches the KID's + /// key. `false` for a refusal (there is no committed key). + pub fn commits_to_key(&self, key_bytes: &[u8]) -> bool { + self.key_commit == Some(key_commitment(key_bytes)) + } + + /// Amortised microjoules of decision energy per release, with its + /// acquisition class. `None` when unmetered. + pub fn uj_per_release(&self) -> Option<(f64, EnergyProvenance)> { + match self.energy_provenance { + Some(p) if self.joules_micro > 0 => Some((self.joules_micro as f64, p)), + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + fn grant(cap: &str) -> GrantRef { + GrantRef { grant_hash: [5u8; 32], capability: cap.into(), joule_ceiling_micro: 1_000_000, funds_ceiling: None } + } + + const CEK: &[u8] = b"0123456789abcdef"; // a 16-byte content-encryption key + + #[test] + fn entitled_and_unexpired_releases_and_commits() { + let r = KeyReleaseReceipt::seal( + &key(1), "did:key:license", [0xAB; 16], "asset-abc", DrmSystem::Widevine, + "svod:tier2", 1000, 2000, CEK, 300, Some(EnergyProvenance::HwShunt), + grant("svod:tier2"), None, + ); + assert_eq!(r.decision, ReleaseDecision::Granted); + assert!(r.verify()); + assert!(r.commits_to_key(CEK)); + assert!(!r.commits_to_key(b"the-wrong-key-16"), "a different key must not match the commitment"); + } + + #[test] + fn wrong_entitlement_is_a_signed_refusal() { + let r = KeyReleaseReceipt::seal( + &key(2), "o", [1; 16], "asset", DrmSystem::PlayReady, "svod:tier3", + 1000, 2000, CEK, 0, None, grant("svod:tier2"), None, + ); + assert_eq!(r.decision, ReleaseDecision::DeniedNoEntitlement); + assert!(r.key_commit.is_none(), "a refusal carries no key commitment"); + assert!(r.verify(), "a refusal is still a valid, signed record"); + } + + #[test] + fn expired_entitlement_denies() { + let r = KeyReleaseReceipt::seal( + &key(3), "o", [1; 16], "asset", DrmSystem::FairPlay, "svod:tier2", + 2500, 2000, CEK, 0, None, grant("svod:tier2"), None, + ); + assert_eq!(r.decision, ReleaseDecision::DeniedExpired); + assert!(r.verify()); + } + + #[test] + fn a_misreported_decision_will_not_verify() { + // Forge a "Granted" over a request the policy would deny (wrong tier), + // re-sign it, and confirm the recomputation catches it. + let mut r = KeyReleaseReceipt::seal( + &key(4), "o", [1; 16], "asset", DrmSystem::Widevine, "svod:tier3", + 1000, 2000, CEK, 0, None, grant("svod:tier2"), None, + ); + assert_eq!(r.decision, ReleaseDecision::DeniedNoEntitlement); + r.decision = ReleaseDecision::Granted; + r.key_commit = Some(key_commitment(CEK)); + r.sig = key(4).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify(), "a decision the bound policy would not produce must fail"); + } + + #[test] + fn granted_without_commitment_is_rejected() { + let mut r = KeyReleaseReceipt::seal( + &key(5), "o", [1; 16], "asset", DrmSystem::ClearKey, "svod:tier2", + 1000, 2000, CEK, 100, Some(EnergyProvenance::ModelBased), grant("svod:tier2"), None, + ); + assert!(r.verify()); + r.key_commit = None; // granted but no committed key + r.sig = key(5).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify()); + } +} -- 2.54.0 (Apple Git-157) From 226d7927e25e535bb2666212267db17a2fe7cc3f Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 3 Sep 2026 15:03:35 -0400 Subject: [PATCH 04/15] =?UTF-8?q?feat(wai):=20wai.video.package=20?= =?UTF-8?q?=E2=80=94=20deterministic=20packaging=20+=20attested=20SegmentM?= =?UTF-8?q?ap=20(OTT=20ingest=20=C2=A74)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The ingest/packaging layer, where the efficiency is most literal. A source is sliced into content-hashed segments on GOP boundaries; the ordered (index -> content_hash) SegmentMap is a signed Merkle commitment. - map-equivalence: segment_map_root lets a wai.video.manifest reference be checked against the package that produced it — the receipts compose. - verifiable dedup: identical content (an ad in every break, a bumper, a replay, simulcast overlap) hashes identically and is stored/encoded once. verify() recomputes unique_segments and stored_bytes from the segments, so the saving cannot be overstated; uj_per_unique_segment is the encode-once energy, honest because the uniqueness is recomputable. Deterministic segment() is a pure function of the source and target duration. Reuses the manifest floor (EnergyProvenance, GrantRef, world Merkle + Ed25519). Only joules_micro is measured-attested. wai_video_package.rs + SPEC §5; feature `video_package`. 5 tests: deterministic dedup segmentation, seal/verify + dedup-is-a-fact, overstated-dedup rejected, tampered-segment breaks the map, encode-once energy amortisation. Co-Authored-By: Claude Opus 4.8 --- wai/SPEC.md | 1 + wai/wai-rs/Cargo.toml | 3 + wai/wai-rs/src/lib.rs | 8 + wai/wai-rs/src/wai_video_package.rs | 368 ++++++++++++++++++++++++++++ 4 files changed, 380 insertions(+) create mode 100644 wai/wai-rs/src/wai_video_package.rs diff --git a/wai/SPEC.md b/wai/SPEC.md index beeeb16d4..38a26981a 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -214,6 +214,7 @@ decode route for each is implemented in the reference sink (see the | `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` | **Sink-architecture note:** the inter-frame neural video codecs (DCVC-RT, DCVC-FM) decode through `ort` and are **CPU-capable** for native sinks — diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index 528ed7d88..cef2cce41 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -173,6 +173,9 @@ video_ssai = ["video_manifest"] # 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"] # Balanced-ternary matrix-product-state transform (`wai.ternary.tt`, # extensions/ternary-tt): quantum-INSPIRED (tensor-network) compression whose # novel delta is an INTEGER core scale — the whole decode is pure i64/i128, so a diff --git a/wai/wai-rs/src/lib.rs b/wai/wai-rs/src/lib.rs index 34d77527e..b040c00e3 100644 --- a/wai/wai-rs/src/lib.rs +++ b/wai/wai-rs/src/lib.rs @@ -282,6 +282,14 @@ pub mod wai_video_ssai; #[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; + // Deterministic autonomous CALIBRATION engines (extensions/quantum-ops § Calibration): // a fixed-point qubit-device simulator + autonomous tune-up algorithms (Rabi π-pulse) // — the software capability the quantum-control vendors sell (autonomous gate tune-up), diff --git a/wai/wai-rs/src/wai_video_package.rs b/wai/wai-rs/src/wai_video_package.rs new file mode 100644 index 000000000..0a1bf5a1c --- /dev/null +++ b/wai/wai-rs/src/wai_video_package.rs @@ -0,0 +1,368 @@ +//! Deterministic packaging + attested SegmentMap — `wai.video.package`. +//! +//! The ingest/packaging layer: a source is sliced into segments, each with an +//! index and a content hash, and the ordered `(index -> content_hash)` map is +//! the SegmentMap the manifest layer references. Two things the incumbent +//! packagers leave implicit become explicit and checkable here. +//! +//! - **The SegmentMap is signed.** `segment_map_root` is a Merkle commitment +//! over the segment leaves, so a `wai.video.manifest` that references segment +//! `i` can be checked against the package that actually produced it — the two +//! receipts compose. +//! - **The dedup is a fact, not a billing line.** Identical content — an ad +//! played in every break, a bumper, a replay, the overlap between simulcast +//! feeds — hashes identically and is stored and encoded once. +//! [`PackageReceipt::verify`] recomputes `unique_segments` and `stored_bytes` +//! from the segments themselves, so the storage/encode saving cannot be +//! overstated. `uj_per_unique_segment` is the encode-once energy, and it is +//! honest precisely because the uniqueness is recomputable. +//! +//! Only `joules_micro` is measured-attested. Reuses the manifest module's +//! `EnergyProvenance` and the world Merkle floor's Ed25519 + `GrantRef`. + +use std::collections::BTreeSet; + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; + +use crate::quantum_ops::GrantRef; +use crate::wai_video_manifest::EnergyProvenance; +use crate::world::receipt::merkle_root; + +const DOMAIN_RECEIPT: &[u8] = b"wai:video-package-receipt\x01"; +const DOMAIN_RECEIPT_ID: &[u8] = b"wai:video-package-receipt-id\x01"; +const DOMAIN_SEG: &[u8] = b"wai:video-package-seg\x01"; +const DOMAIN_MEDIA: &[u8] = b"wai:video-package-media\x01"; + +/// One segment in the SegmentMap. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct SegmentEntry { + pub index: u64, + /// BLAKE3 over the segment's media bytes — the identity that makes two + /// byte-identical segments dedup. + pub content_hash: [u8; 32], + pub duration_ms: u64, + pub byte_len: u64, +} + +impl SegmentEntry { + fn leaf(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_SEG); + h.update(&self.index.to_be_bytes()); + h.update(&self.content_hash); + h.update(&self.duration_ms.to_be_bytes()); + h.update(&self.byte_len.to_be_bytes()); + *h.finalize().as_bytes() + } +} + +/// A source GOP (group-of-pictures): the smallest independently-decodable unit, +/// which a segment boundary must fall on. `(media bytes, presentation duration)`. +pub type Gop<'a> = (&'a [u8], u64); + +/// BLAKE3 over concatenated GOP media bytes — a segment's content identity. +fn media_hash(gops: &[Gop]) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_MEDIA); + for (bytes, _) in gops { + h.update(&(bytes.len() as u64).to_be_bytes()); + h.update(bytes); + } + *h.finalize().as_bytes() +} + +/// Deterministic segmentation: accumulate GOPs until the segment reaches +/// `target_ms`, then close it on the GOP boundary. A pure function of the source +/// and the target, so the SegmentMap is reproducible and content that repeats +/// byte-for-byte lands on identical `content_hash`es. +pub fn segment(gops: &[Gop], target_ms: u64) -> Vec { + let mut out = Vec::new(); + let mut cur: Vec = Vec::new(); + let mut dur = 0u64; + let mut bytes = 0u64; + let mut close = |cur: &mut Vec, dur: &mut u64, bytes: &mut u64, out: &mut Vec| { + if !cur.is_empty() { + out.push(SegmentEntry { + index: out.len() as u64, + content_hash: media_hash(cur), + duration_ms: *dur, + byte_len: *bytes, + }); + cur.clear(); + *dur = 0; + *bytes = 0; + } + }; + for &(b, d) in gops { + cur.push((b, d)); + dur += d; + bytes += b.len() as u64; + if dur >= target_ms { + close(&mut cur, &mut dur, &mut bytes, &mut out); + } + } + close(&mut cur, &mut dur, &mut bytes, &mut out); + out +} + +/// The count of distinct segment contents, and the bytes a dedup store keeps +/// (one copy per distinct content). Both recomputed from the segments so a +/// receipt cannot overstate the saving. +fn dedup_stats(segments: &[SegmentEntry]) -> (u64, u64) { + let mut seen: BTreeSet<[u8; 32]> = BTreeSet::new(); + let mut stored = 0u64; + for s in segments { + if seen.insert(s.content_hash) { + stored += s.byte_len; + } + } + (seen.len() as u64, stored) +} + +/// A signed SegmentMap with an attested dedup accounting. +#[derive(Clone, Debug, PartialEq)] +pub struct PackageReceipt { + pub asset_id: String, + /// Merkle commitment over the segment leaves — the SegmentMap identity a + /// manifest is checked against. + pub segment_map_root: [u8; 32], + pub segments: Vec, + pub total_segments: u64, + /// Distinct `content_hash`es — recomputed in verify(). + pub unique_segments: u64, + pub total_bytes: u64, + /// Bytes a dedup store keeps (one copy per distinct content) — recomputed. + pub stored_bytes: u64, + pub work_segment_ops: u64, + pub joules_micro: u64, + pub energy_provenance: Option, + pub grant: GrantRef, + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +impl PackageReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&(self.asset_id.len() as u32).to_be_bytes()); + o.extend_from_slice(self.asset_id.as_bytes()); + o.extend_from_slice(&self.segment_map_root); + o.extend_from_slice(&self.total_segments.to_be_bytes()); + o.extend_from_slice(&self.unique_segments.to_be_bytes()); + o.extend_from_slice(&self.total_bytes.to_be_bytes()); + o.extend_from_slice(&self.stored_bytes.to_be_bytes()); + o.extend_from_slice(&self.work_segment_ops.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, EnergyProvenance::tag_byte)); + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&(self.segments.len() as u64).to_be_bytes()); + for s in &self.segments { + o.extend_from_slice(&s.leaf()); + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Seal a SegmentMap. The dedup figures are computed here from the segments, + /// so they cannot be set to a saving the map does not support. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + asset_id: impl Into, + segments: Vec, + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> PackageReceipt { + let leaves: Vec<[u8; 32]> = segments.iter().map(SegmentEntry::leaf).collect(); + let (unique_segments, stored_bytes) = dedup_stats(&segments); + let total_bytes = segments.iter().map(|s| s.byte_len).sum(); + let mut r = PackageReceipt { + asset_id: asset_id.into(), + segment_map_root: merkle_root(&leaves), + total_segments: segments.len() as u64, + unique_segments, + total_bytes, + stored_bytes, + work_segment_ops: segments.len() as u64, + segments, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + internal consistency: the Merkle root, the counts and the + /// recomputed dedup figures must all follow from the carried segments, and + /// the energy figure and its label stand or fall together. + pub fn verify(&self) -> bool { + let leaves: Vec<[u8; 32]> = self.segments.iter().map(SegmentEntry::leaf).collect(); + if merkle_root(&leaves) != self.segment_map_root { + return false; + } + if self.total_segments != self.segments.len() as u64 { + return false; + } + if self.work_segment_ops != self.segments.len() as u64 { + return false; + } + let (uniq, stored) = dedup_stats(&self.segments); + if uniq != self.unique_segments || stored != self.stored_bytes { + return false; + } + if self.total_bytes != self.segments.iter().map(|s| s.byte_len).sum::() { + return false; + } + for (i, s) in self.segments.iter().enumerate() { + if s.index != i as u64 { + return false; + } + } + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// Whether the segment at `index` in the attested map has this content — + /// how a `wai.video.manifest` reference is checked against the package. + pub fn segment_content(&self, index: u64) -> Option<[u8; 32]> { + self.segments.get(index as usize).map(|s| s.content_hash) + } + + /// Bytes a dedup store saves versus storing every segment. Verifiable, since + /// both terms are recomputed in [`PackageReceipt::verify`]. + pub fn bytes_saved(&self) -> u64 { + self.total_bytes.saturating_sub(self.stored_bytes) + } + + /// Encode-once energy: microjoules per *distinct* segment, with its + /// acquisition class. `None` when unmetered. + pub fn uj_per_unique_segment(&self) -> Option<(f64, EnergyProvenance)> { + match (self.energy_provenance, self.unique_segments) { + (Some(p), u) if self.joules_micro > 0 && u > 0 => { + Some((self.joules_micro as f64 / u as f64, p)) + } + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + // A source where the ad GOP (`AD`) recurs: content, ad, content, ad. + fn source() -> Vec> { + vec![ + (b"content-gop-0000".as_ref(), 2000), + (b"AD-creative-0001".as_ref(), 2000), + (b"content-gop-0002".as_ref(), 2000), + (b"AD-creative-0001".as_ref(), 2000), + ] + } + + #[test] + fn segmentation_is_deterministic_and_dedups_repeats() { + // target 2000ms -> one GOP per segment; the two ad segments are identical. + let a = segment(&source(), 2000); + let b = segment(&source(), 2000); + assert_eq!(a, b, "segmentation must be a pure function"); + assert_eq!(a.len(), 4); + assert_eq!(a[1].content_hash, a[3].content_hash, "the repeated ad dedups"); + let (uniq, _) = dedup_stats(&a); + assert_eq!(uniq, 3, "4 segments, 3 distinct"); + } + + #[test] + fn seal_verify_and_dedup_is_a_fact() { + let segs = segment(&source(), 2000); + let g = GrantRef::unbounded("video.package"); + let r = PackageReceipt::seal(&key(1), "did:key:pkg", "asset-abc", segs, 12_000, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + assert_eq!(r.total_segments, 4); + assert_eq!(r.unique_segments, 3); + assert_eq!(r.bytes_saved(), 16, "one 16-byte ad segment is stored once, not twice"); + // A manifest referencing index 3 can be checked against the package. + assert_eq!(r.segment_content(3), Some(r.segments[1].content_hash)); + } + + #[test] + fn overstated_dedup_will_not_verify() { + let segs = segment(&source(), 2000); + let g = GrantRef::unbounded("video.package"); + let mut r = PackageReceipt::seal(&key(2), "o", "asset", segs, 0, None, g, None); + assert!(r.verify()); + // Claim more saving than the map supports. + r.unique_segments = 2; + r.stored_bytes = 32; + r.sig = key(2).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify(), "a dedup figure the segments do not support must fail"); + } + + #[test] + fn tampered_segment_breaks_the_map() { + let segs = segment(&source(), 2000); + let g = GrantRef::unbounded("video.package"); + let mut r = PackageReceipt::seal(&key(3), "o", "asset", segs, 0, None, g, None); + assert!(r.verify()); + r.segments[0].content_hash = [0xFF; 32]; // swap a segment's content + assert!(!r.verify(), "a swapped segment must break the SegmentMap root"); + } + + #[test] + fn encode_once_energy_amortises_over_unique_segments() { + let segs = segment(&source(), 2000); + let g = GrantRef::unbounded("video.package"); + // 9000 uJ of packaging over 3 distinct segments. + let r = PackageReceipt::seal(&key(4), "o", "asset", segs, 9000, Some(EnergyProvenance::ModelBased), g, None); + let (uj, prov) = r.uj_per_unique_segment().unwrap(); + assert_eq!(prov, EnergyProvenance::ModelBased); + assert!((uj - 3000.0).abs() < 1e-9, "9000 uJ / 3 unique = 3000 uJ each"); + } +} -- 2.54.0 (Apple Git-157) From b94f5560ac81960a4cdb2c3bb7655dd9cdf31fb8 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 3 Sep 2026 15:06:19 -0400 Subject: [PATCH 05/15] =?UTF-8?q?feat(wai):=20wai.video.channel=20?= =?UTF-8?q?=E2=80=94=20linear/FAST=20assembly,=20program-as-run=20chain=20?= =?UTF-8?q?(OTT=20ingest=20=C2=A75)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The capstone of the OTT ingest. A linear channel is a continuous schedule of assets over wall-clock time, sliced into attested playback windows. - schedule-continuity: verify() rejects a schedule with a gap or an overlap — a linear channel airs with no dead air and no double-booking, and a receipt will not sign one that does. - recomputable program-as-run: `aired` is recomputed from the schedule and the window, so what actually aired is checkable by a licensor, advertiser or regulator against the signed record rather than an operator-held play-out log. - Windows chain via parent_receipt_hash, so a channel's history is a hash chain — operational accountability as a cryptographic artifact. Each window's manifest remains a wai.video.manifest, so the per-class dedup carries through: one generation per window per class, not per viewer. Also adds the `video_workflow` feature switching on the whole suite (manifest + ssai + keys + package + channel): 25 tests pass together. wai_video_channel.rs + SPEC §5; feature `video_channel`. 5 tests: entry_at + continuity, recomputable program-as-run, gap rejected, misreported aired rejected, window chaining + energy amortisation. Co-Authored-By: Claude Opus 5 (1M context) --- wai/SPEC.md | 1 + wai/wai-rs/Cargo.toml | 5 + wai/wai-rs/src/lib.rs | 8 + wai/wai-rs/src/wai_video_channel.rs | 336 ++++++++++++++++++++++++++++ 4 files changed, 350 insertions(+) create mode 100644 wai/wai-rs/src/wai_video_channel.rs diff --git a/wai/SPEC.md b/wai/SPEC.md index 38a26981a..59b99523f 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -215,6 +215,7 @@ decode route for each is implemented in the reference sink (see the | `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 — diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index cef2cce41..0c5ca5bd0 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -176,6 +176,11 @@ video_keys = ["video_manifest"] # wai.video.package — deterministic segmentation + attested, deduplicating # SegmentMap. Reuses the manifest floor (EnergyProvenance, GrantRef, Merkle). video_package = ["video_manifest"] +# wai.video.channel — virtual linear / FAST assembly; the program-as-run hash +# chain. Reuses the manifest floor (EnergyProvenance, GrantRef, Merkle). +video_channel = ["video_manifest"] +# The whole OTT workflow suite in one switch. +video_workflow = ["video_manifest", "video_ssai", "video_keys", "video_package", "video_channel"] # Balanced-ternary matrix-product-state transform (`wai.ternary.tt`, # extensions/ternary-tt): quantum-INSPIRED (tensor-network) compression whose # novel delta is an INTEGER core scale — the whole decode is pure i64/i128, so a diff --git a/wai/wai-rs/src/lib.rs b/wai/wai-rs/src/lib.rs index b040c00e3..1edad8f61 100644 --- a/wai/wai-rs/src/lib.rs +++ b/wai/wai-rs/src/lib.rs @@ -290,6 +290,14 @@ pub mod wai_video_keys; #[cfg(feature = "video_package")] pub mod wai_video_package; +// Virtual linear / FAST channel assembly (wai.video.channel): the capstone. A +// continuous schedule (gapless, non-overlapping — verify() rejects dead air) +// whose program-as-run per window is recomputed, not logged. Windows chain via +// parent_receipt_hash, so a channel's history is a hash chain: operational +// accountability as a cryptographic artifact rather than an operator's log. +#[cfg(feature = "video_channel")] +pub mod wai_video_channel; + // Deterministic autonomous CALIBRATION engines (extensions/quantum-ops § Calibration): // a fixed-point qubit-device simulator + autonomous tune-up algorithms (Rabi π-pulse) // — the software capability the quantum-control vendors sell (autonomous gate tune-up), diff --git a/wai/wai-rs/src/wai_video_channel.rs b/wai/wai-rs/src/wai_video_channel.rs new file mode 100644 index 000000000..9d6bd399e --- /dev/null +++ b/wai/wai-rs/src/wai_video_channel.rs @@ -0,0 +1,336 @@ +//! Virtual linear / FAST channel assembly — `wai.video.channel`. +//! +//! A linear channel is a continuous schedule of assets over wall-clock time; the +//! delivery layer turns the slice of that schedule covering a playback window +//! into a manifest. The capstone of the OTT ingest: it composes the other four +//! and turns the one thing a managed streaming operation is really selling — +//! *operational accountability* — into a cryptographic artifact. +//! +//! Two facts a broadcaster today reconstructs from logs after the fact are here +//! signed and recomputable: +//! +//! - **The schedule is a real continuous channel.** [`ChannelReceipt::verify`] +//! rejects a schedule with a gap or an overlap — a linear channel airs with no +//! dead air and no double-booking, and the receipt will not sign one that +//! does. +//! - **The program-as-run is checkable.** `aired` — which entries were on air in +//! the attested window — is recomputed from the schedule and the window, so a +//! licensor, an advertiser or a regulator confirms what actually aired against +//! the signed record rather than a play-out log only the operator holds. +//! +//! Windows chain via `parent_receipt_hash`, so a channel's history is a hash +//! chain of program-as-run windows — the StreamOps audit trail. Each window's +//! manifest is still a `wai.video.manifest`, so the per-class dedup carries +//! through: one generation per window per class, not per viewer. Only +//! `joules_micro` is measured-attested. Reuses the manifest floor. + +use ed25519_dalek::{Signature, Signer, SigningKey, Verifier, VerifyingKey}; + +use crate::quantum_ops::GrantRef; +use crate::wai_video_manifest::EnergyProvenance; +use crate::world::receipt::merkle_root; + +const DOMAIN_RECEIPT: &[u8] = b"wai:video-channel-receipt\x01"; +const DOMAIN_RECEIPT_ID: &[u8] = b"wai:video-channel-receipt-id\x01"; +const DOMAIN_ENTRY: &[u8] = b"wai:video-channel-entry\x01"; + +/// What a scheduled slot carries. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum EntryKind { + Program, + Ad, + Filler, +} + +impl EntryKind { + fn tag(self) -> u8 { + match self { + EntryKind::Program => 1, + EntryKind::Ad => 2, + EntryKind::Filler => 3, + } + } +} + +/// One slot in the channel schedule. `start_ms` is an epoch in milliseconds so +/// it shares units with `duration_ms`; the slot occupies `[start_ms, end)`. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct ScheduleEntry { + pub asset_id: String, + pub start_ms: u64, + pub duration_ms: u64, + pub kind: EntryKind, +} + +impl ScheduleEntry { + pub fn end_ms(&self) -> u64 { + self.start_ms + self.duration_ms + } + fn leaf(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_ENTRY); + h.update(&(self.asset_id.len() as u32).to_be_bytes()); + h.update(self.asset_id.as_bytes()); + h.update(&self.start_ms.to_be_bytes()); + h.update(&self.duration_ms.to_be_bytes()); + h.update(&[self.kind.tag()]); + *h.finalize().as_bytes() + } +} + +/// Whether a schedule is a valid continuous channel: ordered, gapless and +/// non-overlapping — each entry begins exactly where the previous one ended. +pub fn is_continuous(schedule: &[ScheduleEntry]) -> bool { + schedule.windows(2).all(|w| w[0].end_ms() == w[1].start_ms) +} + +/// The schedule entry on air at `now_ms`, and the offset into it. Deterministic; +/// `None` before the schedule starts or after it ends. +pub fn entry_at(schedule: &[ScheduleEntry], now_ms: u64) -> Option<(usize, u64)> { + schedule + .iter() + .position(|e| now_ms >= e.start_ms && now_ms < e.end_ms()) + .map(|i| (i, now_ms - schedule[i].start_ms)) +} + +/// The indices on air at any point in the half-open window `[start, end)` — +/// the program-as-run for that window. An entry aired if it overlaps the window. +fn aired_in(schedule: &[ScheduleEntry], window_start_ms: u64, window_end_ms: u64) -> Vec { + schedule + .iter() + .enumerate() + .filter(|(_, e)| e.start_ms < window_end_ms && e.end_ms() > window_start_ms) + .map(|(i, _)| i as u64) + .collect() +} + +/// A signed program-as-run window of a linear channel. +#[derive(Clone, Debug, PartialEq)] +pub struct ChannelReceipt { + pub channel_id: String, + /// Merkle commitment over the schedule entries — the program identity. + pub schedule_root: [u8; 32], + pub schedule: Vec, + pub window_start_ms: u64, + pub window_end_ms: u64, + /// Schedule indices on air in the window — recomputed in verify(). + pub aired: Vec, + pub work_schedule_ops: u64, + pub joules_micro: u64, + pub energy_provenance: Option, + pub grant: GrantRef, + /// The prior window's receipt — the channel history is this hash chain. + pub parent_receipt_hash: Option<[u8; 32]>, + pub signer_pubkey: [u8; 32], + pub signer_id: String, + pub sig: [u8; 64], +} + +impl ChannelReceipt { + fn signing_payload(&self) -> Vec { + let mut o = DOMAIN_RECEIPT.to_vec(); + o.extend_from_slice(&(self.channel_id.len() as u32).to_be_bytes()); + o.extend_from_slice(self.channel_id.as_bytes()); + o.extend_from_slice(&self.schedule_root); + o.extend_from_slice(&self.window_start_ms.to_be_bytes()); + o.extend_from_slice(&self.window_end_ms.to_be_bytes()); + o.extend_from_slice(&self.work_schedule_ops.to_be_bytes()); + o.extend_from_slice(&self.joules_micro.to_be_bytes()); + o.push(self.energy_provenance.map_or(0, EnergyProvenance::tag_byte)); + o.extend_from_slice(&self.grant.grant_hash); + o.extend_from_slice(&(self.grant.capability.len() as u32).to_be_bytes()); + o.extend_from_slice(self.grant.capability.as_bytes()); + o.extend_from_slice(&self.grant.joule_ceiling_micro.to_be_bytes()); + match self.grant.funds_ceiling { + Some(f) => { + o.push(1); + o.extend_from_slice(&f.to_be_bytes()); + } + None => o.push(0), + } + match self.parent_receipt_hash { + Some(h) => { + o.push(1); + o.extend_from_slice(&h); + } + None => o.push(0), + } + o.extend_from_slice(&(self.aired.len() as u64).to_be_bytes()); + for a in &self.aired { + o.extend_from_slice(&a.to_be_bytes()); + } + o.extend_from_slice(&(self.schedule.len() as u64).to_be_bytes()); + for e in &self.schedule { + o.extend_from_slice(&e.leaf()); + } + o.extend_from_slice(&self.signer_pubkey); + let id = self.signer_id.as_bytes(); + o.extend_from_slice(&(id.len() as u32).to_be_bytes()); + o.extend_from_slice(id); + o + } + + /// Seal a program-as-run window. `aired` is computed here from the schedule + /// and the window, so it cannot claim a program that did not air. + #[allow(clippy::too_many_arguments)] + pub fn seal( + signer: &SigningKey, + signer_id: impl Into, + channel_id: impl Into, + schedule: Vec, + window_start_ms: u64, + window_end_ms: u64, + joules_micro: u64, + energy_provenance: Option, + grant: GrantRef, + parent_receipt_hash: Option<[u8; 32]>, + ) -> ChannelReceipt { + let leaves: Vec<[u8; 32]> = schedule.iter().map(ScheduleEntry::leaf).collect(); + let aired = aired_in(&schedule, window_start_ms, window_end_ms); + let mut r = ChannelReceipt { + channel_id: channel_id.into(), + schedule_root: merkle_root(&leaves), + work_schedule_ops: schedule.len() as u64, + schedule, + window_start_ms, + window_end_ms, + aired, + joules_micro, + energy_provenance, + grant, + parent_receipt_hash, + signer_pubkey: signer.verifying_key().to_bytes(), + signer_id: signer_id.into(), + sig: [0u8; 64], + }; + r.sig = signer.sign(&r.signing_payload()).to_bytes(); + r + } + + /// Signature + program integrity: the schedule must be a valid continuous + /// channel (ordered, gapless, non-overlapping), the Merkle root and work + /// figure must follow from it, the window must be non-empty, `aired` must be + /// exactly what the schedule and window produce, and the energy figure and + /// its label stand or fall together. + pub fn verify(&self) -> bool { + let leaves: Vec<[u8; 32]> = self.schedule.iter().map(ScheduleEntry::leaf).collect(); + if merkle_root(&leaves) != self.schedule_root { + return false; + } + if self.work_schedule_ops != self.schedule.len() as u64 { + return false; + } + if self.window_start_ms >= self.window_end_ms { + return false; + } + if !is_continuous(&self.schedule) { + return false; + } + if aired_in(&self.schedule, self.window_start_ms, self.window_end_ms) != self.aired { + return false; + } + match (self.energy_provenance, self.joules_micro) { + (None, 0) => {} + (Some(_), n) if n > 0 => {} + _ => return false, + } + let Ok(k) = VerifyingKey::from_bytes(&self.signer_pubkey) else { return false }; + k.verify(&self.signing_payload(), &Signature::from_bytes(&self.sig)).is_ok() + } + + /// The program-as-run: the schedule entries on air in this window. + pub fn aired_entries(&self) -> Vec<&ScheduleEntry> { + self.aired.iter().filter_map(|&i| self.schedule.get(i as usize)).collect() + } + + /// Microjoules of assembly energy per aired entry in the window, with its + /// acquisition class. `None` when unmetered or nothing aired. + pub fn uj_per_aired(&self) -> Option<(f64, EnergyProvenance)> { + let n = self.aired.len() as u64; + match (self.energy_provenance, n) { + (Some(p), a) if self.joules_micro > 0 && a > 0 => { + Some((self.joules_micro as f64 / a as f64, p)) + } + _ => None, + } + } + + pub fn receipt_hash(&self) -> [u8; 32] { + let mut h = blake3::Hasher::new(); + h.update(DOMAIN_RECEIPT_ID); + h.update(&self.signing_payload()); + h.update(&self.sig); + *h.finalize().as_bytes() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + fn key(s: u8) -> SigningKey { + SigningKey::from_bytes(&[s; 32]) + } + + // A gapless channel: show A [0,10s), ad [10s,12s), show B [12s,22s). + fn schedule() -> Vec { + vec![ + ScheduleEntry { asset_id: "show-A".into(), start_ms: 0, duration_ms: 10_000, kind: EntryKind::Program }, + ScheduleEntry { asset_id: "ad-1".into(), start_ms: 10_000, duration_ms: 2_000, kind: EntryKind::Ad }, + ScheduleEntry { asset_id: "show-B".into(), start_ms: 12_000, duration_ms: 10_000, kind: EntryKind::Program }, + ] + } + + #[test] + fn entry_at_and_continuity() { + let s = schedule(); + assert!(is_continuous(&s)); + assert_eq!(entry_at(&s, 5_000), Some((0, 5_000))); + assert_eq!(entry_at(&s, 11_000), Some((1, 1_000))); + assert_eq!(entry_at(&s, 100_000), None); + } + + #[test] + fn program_as_run_is_recomputable() { + // Window [8s, 13s) spans the tail of A, the whole ad, the head of B. + let g = GrantRef::unbounded("video.channel"); + let r = ChannelReceipt::seal(&key(1), "did:key:chan", "fast-42", schedule(), 8_000, 13_000, 6_000, Some(EnergyProvenance::HwShunt), g, None); + assert!(r.verify()); + assert_eq!(r.aired, vec![0, 1, 2], "all three entries touch the window"); + assert_eq!(r.aired_entries().iter().map(|e| e.asset_id.as_str()).collect::>(), ["show-A", "ad-1", "show-B"]); + } + + #[test] + fn a_gap_in_the_schedule_will_not_verify() { + let mut s = schedule(); + s[2].start_ms = 13_000; // leave 1s of dead air after the ad + let g = GrantRef::unbounded("video.channel"); + let r = ChannelReceipt::seal(&key(2), "o", "c", s, 0, 22_000, 0, None, g, None); + assert!(!r.verify(), "a channel with dead air is not a valid linear schedule"); + } + + #[test] + fn a_misreported_program_as_run_is_rejected() { + let g = GrantRef::unbounded("video.channel"); + // Window [0, 5s): only show-A aired. + let mut r = ChannelReceipt::seal(&key(3), "o", "c", schedule(), 0, 5_000, 0, None, g, None); + assert_eq!(r.aired, vec![0]); + assert!(r.verify()); + r.aired = vec![0, 1]; // claim the ad aired when it did not + r.sig = key(3).sign(&r.signing_payload()).to_bytes(); + assert!(!r.verify(), "an aired set the window does not produce must fail"); + } + + #[test] + fn windows_chain_and_energy_amortises() { + let g = GrantRef::unbounded("video.channel"); + let w1 = ChannelReceipt::seal(&key(4), "o", "c", schedule(), 0, 10_000, 3_000, Some(EnergyProvenance::ModelBased), g.clone(), None); + assert!(w1.verify()); + // The next window chains from the first — the channel history is a chain. + let w2 = ChannelReceipt::seal(&key(4), "o", "c", schedule(), 10_000, 22_000, 6_000, Some(EnergyProvenance::ModelBased), g, Some(w1.receipt_hash())); + assert!(w2.verify()); + assert_eq!(w2.parent_receipt_hash, Some(w1.receipt_hash())); + let (uj, _) = w2.uj_per_aired().unwrap(); + assert!((uj - 3000.0).abs() < 1e-9, "6000 uJ / 2 aired (ad-1, show-B) = 3000 each"); + } +} -- 2.54.0 (Apple Git-157) From f47285b531504d77da17dc1d520df5dc0ec2d2d0 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 3 Sep 2026 15:16:19 -0400 Subject: [PATCH 06/15] =?UTF-8?q?feat(wai-web):=20browser=20sink=20for=20t?= =?UTF-8?q?he=20OTT=20workflow=20=E2=80=94=20live=20at=20/video-ott?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The same Rust 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. - OttSession: manifest/class/receipt hashes, the rendered m3u8 (ad breaks as real EXT-X-DISCONTINUITY splices), the monetisation audit, and swap_ad() — substituting a creative without re-signing, so verify() flips false. - OttAdBreak: the deterministic decision plus the budget half — drop the grant's funds ceiling below the billable spend and the receipt refuses. Browser-verified live: receipt verifies, tamper breaks it, per-viewer energy falls 9000 -> 0.180 uJ as the class dedups across 50k viewers, ceiling breach refuses, zero JS errors. Enables `video_workflow` on the wai dependency. Co-Authored-By: Claude Opus 5 (1M context) --- wai/wai-web/Cargo.toml | 2 +- wai/wai-web/src/lib.rs | 5 + wai/wai-web/src/video_ott.rs | 270 +++++++++++++++++++++++++++++++++++ 3 files changed, 276 insertions(+), 1 deletion(-) create mode 100644 wai/wai-web/src/video_ott.rs diff --git a/wai/wai-web/Cargo.toml b/wai/wai-web/Cargo.toml index b5277ec1e..fc4bc39f1 100644 --- a/wai/wai-web/Cargo.toml +++ b/wai/wai-web/Cargo.toml @@ -19,7 +19,7 @@ js-sys = "0.3" # with the codec chain off. No second implementation: replay-equivalence # in the browser is the identical Rust that generated the conformance # corpus hashes. -wai = { path = "../wai-rs", default-features = false, features = ["world", "audio_scene", "haptic", "splat4d", "provenance", "score", "film", "neural_int", "generate", "video_int", "audio_int", "world_model", "world_int", "splat_int", "quantum", "quantum_ops", "quantum_cal", "quantum_mitigate", "quantum_qec", "quantum_control", "quantum_noise", "quantum_compile", "quantum_atom", "quantum_qbom", "quantum_receipt", "quantum_toolchain", "quantum_mps", "quantum_stabilizer", "quantum_pauli", "quantum_vml", "quantum_phasor", "quantum_qfhrr", "quantum_kernel", "quantum_phasor_meter", "quantum_qdata"] } +wai = { path = "../wai-rs", default-features = false, features = ["world", "audio_scene", "haptic", "splat4d", "provenance", "score", "film", "neural_int", "generate", "video_int", "audio_int", "world_model", "world_int", "splat_int", "quantum", "quantum_ops", "quantum_cal", "quantum_mitigate", "quantum_qec", "quantum_control", "quantum_noise", "quantum_compile", "quantum_atom", "quantum_qbom", "quantum_receipt", "quantum_toolchain", "quantum_mps", "quantum_stabilizer", "quantum_pauli", "quantum_vml", "quantum_phasor", "quantum_qfhrr", "quantum_kernel", "quantum_phasor_meter", "quantum_qdata", "video_workflow"] } ed25519-dalek = "2" # actor keys for browser-side op authoring (same version as wai-rs) blake3 = "1" # in-page receipt check: hash a decoded image against a pinned digest diff --git a/wai/wai-web/src/lib.rs b/wai/wai-web/src/lib.rs index f933ad0e2..2b9a1f8b8 100644 --- a/wai/wai-web/src/lib.rs +++ b/wai/wai-web/src/lib.rs @@ -41,6 +41,11 @@ pub mod generate; // i64, no ML runtime; frame-state-equivalence, decoded + per-frame-verified in-page. pub mod video; +// Browser sink for the OTT workflow (wai.video.manifest + wai.video.ssai): +// render a real manifest, verify its receipt in the tab, swap a creative to +// break it, and watch per-viewer energy amortise as the class dedups. +pub mod video_ott; + // Byte-exact LEARNED AUDIO codec (wai.audio.int_codec) — pure i64, no ML runtime; // sample-equivalence, decoded to int16 PCM + hash-verified + played in-page. pub mod audio_int; diff --git a/wai/wai-web/src/video_ott.rs b/wai/wai-web/src/video_ott.rs new file mode 100644 index 000000000..f87061f5f --- /dev/null +++ b/wai/wai-web/src/video_ott.rs @@ -0,0 +1,270 @@ +//! Browser sink for the OTT workflow — `wai.video.manifest` + `wai.video.ssai`. +//! +//! The same `wai` crate a native packager runs, compiled to wasm32: the page +//! composes a session class, renders the real HLS manifest, seals the receipt +//! and verifies it in the tab. No second implementation, so what the browser +//! shows is what a native sink would produce. +//! +//! Three things the page can demonstrate that a dashboard cannot: +//! +//! - **The manifest is the receipt's subject.** `manifest_hash == +//! hash(render(segments))` is recomputed here, in the tab. +//! - **Tamper-evidence.** [`OttSession::swap_ad`] substitutes a different +//! creative without re-signing — exactly the ad-fraud move — and `verify()` +//! flips to false. +//! - **The efficiency is amortised, not asserted.** Raising the viewers served +//! by one class drops `uj_per_viewer`, because the manifest is a pure function +//! of the class and is generated once for all of them. + +use wasm_bindgen::prelude::*; + +use wai::quantum_ops::GrantRef; +use wai::wai_video_manifest::{ + render_hls, EnergyProvenance, ManifestReceipt, Segment, SegmentKind, SessionClass, +}; +use wai::wai_video_ssai::{decide, pod_hash, AdCandidate, SsaiReceipt}; + +fn hex(b: &[u8]) -> String { + b.iter().map(|x| format!("{x:02x}")).collect() +} + +/// A demo signing key — the page is a sink, not a licensor; a real deployment +/// holds its key in the packager. +fn demo_key() -> ed25519_dalek::SigningKey { + ed25519_dalek::SigningKey::from_bytes(&[42u8; 32]) +} + +/// Build a plausible break-bearing composition: `n_content` programme segments +/// of 6s with a single 4s ad spliced in after the first. +fn compose(n_content: u32, ad_id: &str) -> Vec { + let mut segs = Vec::new(); + let mut idx = 0u64; + for i in 0..n_content { + if i == 1 { + segs.push(Segment { + index: idx, + kind: SegmentKind::Ad, + uri: format!("ad/{ad_id}/0.ts"), + duration_ms: 4000, + ad_id: Some(ad_id.to_string()), + }); + idx += 1; + } + segs.push(Segment { + index: idx, + kind: SegmentKind::Content, + uri: format!("seg{i}.ts"), + duration_ms: 6000, + ad_id: None, + }); + idx += 1; + } + segs +} + +/// An attested per-session manifest, live in the page. +#[wasm_bindgen] +pub struct OttSession { + receipt: ManifestReceipt, + /// The bytes the player was handed — kept as delivered, so a later tamper + /// of the composition is visible against them. + delivered: String, +} + +#[wasm_bindgen] +impl OttSession { + /// Compose a session class, render its manifest and seal the receipt. + /// `blackouts` is a comma-separated set (order-independent by construction). + #[wasm_bindgen(constructor)] + #[allow(clippy::too_many_arguments)] + pub fn new( + content_id: &str, + entitlement: &str, + geo: &str, + blackouts: &str, + ad_pod_id: &str, + window: u64, + n_content: u32, + ad_id: &str, + viewers_served: u64, + joules_micro: u64, + ) -> OttSession { + let class = SessionClass { + content_id: content_id.to_string(), + entitlement: entitlement.to_string(), + geo: geo.to_string(), + blackouts: blackouts + .split(',') + .map(str::trim) + .filter(|s| !s.is_empty()) + .map(String::from) + .collect(), + ad_pod_id: ad_pod_id.to_string(), + window, + }; + let segments = compose(n_content.max(1), ad_id); + let delivered = render_hls(&segments); + let grant = GrantRef { + grant_hash: [7u8; 32], + capability: "video.manifest".to_string(), + joule_ceiling_micro: u64::MAX, + funds_ceiling: None, + }; + let prov = (joules_micro > 0).then_some(EnergyProvenance::ModelBased); + let receipt = ManifestReceipt::seal( + &demo_key(), + "did:key:demo-packager", + class, + segments, + viewers_served.max(1), + joules_micro, + prov, + grant, + None, + ); + OttSession { receipt, delivered } + } + + /// The rendered HLS the player receives — ad breaks appear as real + /// `EXT-X-DISCONTINUITY` splices. + pub fn manifest(&self) -> String { + self.delivered.clone() + } + + /// The manifest currently implied by the sealed composition. After a tamper + /// this diverges from [`OttSession::manifest`]. + pub fn composed_manifest(&self) -> String { + render_hls(&self.receipt.segments) + } + + pub fn manifest_hash_hex(&self) -> String { + hex(&self.receipt.manifest_hash) + } + + /// The dedup key: every viewer of this class gets these identical bytes. + pub fn class_hash_hex(&self) -> String { + hex(&self.receipt.session_class_hash) + } + + pub fn receipt_hash_hex(&self) -> String { + hex(&self.receipt.receipt_hash()) + } + + /// Signature + internal consistency, recomputed in the tab. + pub fn verify(&self) -> bool { + self.receipt.verify() + } + + /// The independent check against the bytes actually delivered. + pub fn verify_delivered(&self) -> bool { + self.receipt.verify_render(self.delivered.as_bytes()) + } + + /// The monetisation audit, derived from the ad-bearing segments: + /// `[[break_index, ad_id, duration_ms], ...]` as JSON. + pub fn ads_json(&self) -> String { + let rows: Vec = self + .receipt + .ad_insertions() + .iter() + .map(|(i, a, d)| format!("[{i},\"{a}\",{d}]")) + .collect(); + format!("[{}]", rows.join(",")) + } + + pub fn segment_count(&self) -> u32 { + self.receipt.segments.len() as u32 + } + + pub fn viewers_served(&self) -> u64 { + self.receipt.viewers_served + } + + /// Amortised microjoules per viewer, or `-1` when unmetered. This is the + /// figure a 1:1-unique generator cannot report below its per-viewer cost. + pub fn uj_per_viewer(&self) -> f64 { + self.receipt.uj_per_viewer().map_or(-1.0, |(v, _)| v) + } + + /// Substitute a different creative into the break **without re-signing** — + /// the ad-fraud move. `verify()` flips to false, because the sealed + /// `manifest_hash` no longer matches what the composition renders. + pub fn swap_ad(&mut self, new_ad_id: &str) { + for s in self.receipt.segments.iter_mut() { + if s.ad_id.is_some() { + s.ad_id = Some(new_ad_id.to_string()); + s.uri = format!("ad/{new_ad_id}/0.ts"); + } + } + } +} + +/// An attested ad break — the budget half of the story. +#[wasm_bindgen] +pub struct OttAdBreak { + receipt: SsaiReceipt, +} + +#[wasm_bindgen] +impl OttAdBreak { + /// Run a deterministic decision over a three-ad pod against `budget_micros`, + /// mark the filled slots as played, and seal. Set `budget_micros` below the + /// resulting spend to watch a ceiling breach refuse to verify. + #[wasm_bindgen(constructor)] + pub fn new(avail_slots: u32, avail_ms: u64, budget_micros: u64, ceiling_micros: u64) -> OttAdBreak { + let pod = vec![ + AdCandidate { ad_id: "ad-alpha".into(), creative_hash: [1u8; 32], duration_ms: 15000, price_micros: 40_000 }, + AdCandidate { ad_id: "ad-beta".into(), creative_hash: [2u8; 32], duration_ms: 15000, price_micros: 30_000 }, + AdCandidate { ad_id: "ad-gamma".into(), creative_hash: [3u8; 32], duration_ms: 30000, price_micros: 90_000 }, + ]; + let mut imps = decide(&pod, avail_slots as u64, avail_ms, budget_micros); + for i in imps.iter_mut() { + i.quartiles_reached = 5; // played to completion + } + let grant = GrantRef { + grant_hash: [8u8; 32], + capability: "video.ssai".to_string(), + joule_ceiling_micro: u64::MAX, + funds_ceiling: Some(ceiling_micros), + }; + let receipt = SsaiReceipt::seal( + &demo_key(), + "did:key:demo-ssai", + "avail-1", + [9u8; 32], + pod_hash(&pod), + imps, + 3, + 0, + None, + grant, + None, + ); + OttAdBreak { receipt } + } + + /// `false` when the spend exceeds the grant's ceiling — overspend cannot be + /// signed into a valid receipt. + pub fn verify(&self) -> bool { + self.receipt.verify() + } + + pub fn budget_spent(&self) -> u64 { + self.receipt.budget_spent_micros + } + + pub fn billable(&self) -> u32 { + self.receipt.billable_impressions() as u32 + } + + /// `[[slot, ad_id, price_micros, quartiles], ...]` as JSON. + pub fn slots_json(&self) -> String { + let rows: Vec = self + .receipt + .impressions + .iter() + .map(|i| format!("[{},\"{}\",{},{}]", i.slot, i.ad_id, i.price_micros, i.quartiles_reached)) + .collect(); + format!("[{}]", rows.join(",")) + } +} -- 2.54.0 (Apple Git-157) From 293d2833ac0f0ca07a4fada8d645986c352c3c27 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 3 Sep 2026 15:29:57 -0400 Subject: [PATCH 07/15] =?UTF-8?q?feat(wai):=20energy=20meters=20=E2=80=94?= =?UTF-8?q?=20make=20the=20provenance=20ladder=20mechanical?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the honest gap the OTT ingest left open: joules_micro was a parameter, so the acquisition class was a convention the caller was trusted to honour. Now it is enforced by construction. - CounterMeter reads a real hardware energy counter and is the ONLY meter that can yield HwShunt. Its read is injected, so the delta and wraparound arithmetic is exercised without hardware; CounterMeter::rapl() wires the Linux powercap sysfs and returns None wherever it is absent. - ModelMeter multiplies elapsed time by a calibrated power figure and can only ever say ModelBased. It has no way to claim a measurement. - A meter that cannot measure returns None — never a fabricated figure. A plausible number with the wrong label is worse than no number: the caller then meters with a model and says so, or seals unmetered (0/None), which the receipts already accept and which verify() already enforces. EnergyReading::as_seal_args() feeds a receipt's seal directly, so the meter is a clean seam rather than a coupling. Note: no RAPL on this machine, and the tests say so rather than pretending — the hardware path is exercised where powercap exists (the Linux runner), not here. Nothing in this commit claims a measurement it did not take. energy_meter.rs; feature `energy_meter`. 6 tests. Full suite green: 113 passed / 0 failed under video_workflow + energy_meter. Co-Authored-By: Claude Opus 5 (1M context) --- wai/wai-rs/Cargo.toml | 3 + wai/wai-rs/src/energy_meter.rs | 229 +++++++++++++++++++++++++++++++++ wai/wai-rs/src/lib.rs | 7 + 3 files changed, 239 insertions(+) create mode 100644 wai/wai-rs/src/energy_meter.rs diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index 0c5ca5bd0..ef79661c5 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -166,6 +166,9 @@ video_receipt = ["video_int", "world"] # 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. video_manifest = ["quantum_ops"] +# 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. video_ssai = ["video_manifest"] diff --git a/wai/wai-rs/src/energy_meter.rs b/wai/wai-rs/src/energy_meter.rs new file mode 100644 index 000000000..b433e7a8e --- /dev/null +++ b/wai/wai-rs/src/energy_meter.rs @@ -0,0 +1,229 @@ +//! Energy meters — where a receipt's `joules_micro` actually comes from. +//! +//! Every receipt class in WAI seals a joule figure *beside its acquisition +//! class*, and rejects the two out of step: an unlabelled non-zero figure is +//! uncomparable, a labelled zero claims a measurement that did not happen. That +//! discipline is only as good as the thing producing the number, so this module +//! makes the ladder **mechanical rather than conventional**: +//! +//! - A [`CounterMeter`] reads a real hardware energy counter and is the only +//! meter here that can ever yield [`EnergyProvenance::HwShunt`]. +//! - A [`ModelMeter`] multiplies elapsed time by a calibrated power figure and +//! can only ever yield [`EnergyProvenance::ModelBased`] — it has no way to +//! claim a measurement. +//! - When a meter cannot measure — no hardware, no counter, no span started — +//! [`Meter::stop`] returns `None`. It never falls back to a fabricated figure, +//! because a plausible number with the wrong label is worse than no number: +//! the caller then either meters with a model and says so, or seals unmetered +//! (`0` / `None`), which the receipts already accept. +//! +//! Both meters take their source injected — a counter reader, a clock — so the +//! delta and wraparound arithmetic is testable without hardware, and so the +//! module stays usable on targets with no `Instant` (wasm). The convenience +//! constructor [`CounterMeter::rapl`] wires the Linux powercap sysfs interface +//! and returns `None` anywhere it is absent. + +use crate::wai_video_manifest::EnergyProvenance; + +/// A measured span: the energy, and the class of the measurement. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct EnergyReading { + pub joules_micro: u64, + pub provenance: EnergyProvenance, +} + +impl EnergyReading { + /// The pair a receipt's `seal` wants: `(joules_micro, Some(provenance))`. + pub fn as_seal_args(self) -> (u64, Option) { + (self.joules_micro, Some(self.provenance)) + } + + /// What to seal when there was no measurement at all — `(0, None)`, the + /// only unmetered form the receipts accept. + pub fn unmetered() -> (u64, Option) { + (0, None) + } +} + +/// Something that can measure the energy of a span of work. +pub trait Meter { + /// Begin a span. Calling it again restarts the span. + fn start(&mut self); + /// End the span. `None` when this meter could not measure — never a + /// fabricated figure. + fn stop(&mut self) -> Option; + /// The class this meter is capable of claiming, whatever happens. + fn provenance(&self) -> EnergyProvenance; +} + +/// A monotonic hardware energy counter, in microjoules, that wraps at +/// `wrap_at`. The read is injected, so the delta and wraparound arithmetic is +/// exercised in tests without needing the hardware present. +pub struct CounterMeter { + read: Box Option>, + wrap_at: u64, + start: Option, +} + +impl CounterMeter { + /// `read` returns the counter's current microjoule value, or `None` when it + /// cannot be read. `wrap_at` is the counter's range (its maximum + 1). + pub fn new(read: impl FnMut() -> Option + 'static, wrap_at: u64) -> CounterMeter { + CounterMeter { read: Box::new(read), wrap_at, start: None } + } + + /// Wire the Linux powercap (RAPL) interface for a package domain. `None` + /// when the interface is absent — which is every non-Linux target, and any + /// Linux without powercap — so the caller must fall back explicitly rather + /// than silently receive a made-up figure. + pub fn rapl(domain: &str) -> Option { + let base = format!("/sys/class/powercap/{domain}"); + let energy = format!("{base}/energy_uj"); + let range = format!("{base}/max_energy_range_uj"); + // Both files must be readable now, or this meter does not exist. + let wrap_at = read_u64_file(&range)?.saturating_add(1); + read_u64_file(&energy)?; + Some(CounterMeter::new(move || read_u64_file(&energy), wrap_at)) + } +} + +fn read_u64_file(path: &str) -> Option { + std::fs::read_to_string(path).ok()?.trim().parse::().ok() +} + +impl Meter for CounterMeter { + fn start(&mut self) { + self.start = (self.read)(); + } + + fn stop(&mut self) -> Option { + let started = self.start.take()?; + let now = (self.read)()?; + // Energy counters are monotonic until they wrap at their range. + let delta = + if now >= started { now - started } else { self.wrap_at - started + now }; + Some(EnergyReading { joules_micro: delta, provenance: EnergyProvenance::HwShunt }) + } + + fn provenance(&self) -> EnergyProvenance { + EnergyProvenance::HwShunt + } +} + +/// Elapsed time multiplied by a calibrated power figure. A real number, and +/// honestly labelled as derived — it cannot claim `HwShunt` however it is +/// configured. +pub struct ModelMeter { + clock_micros: Box u64>, + milliwatts: u64, + t0: Option, +} + +impl ModelMeter { + /// `clock_micros` returns a monotonic microsecond timestamp; `milliwatts` + /// is the calibrated marginal power of the work being measured. + pub fn new(clock_micros: impl FnMut() -> u64 + 'static, milliwatts: u64) -> ModelMeter { + ModelMeter { clock_micros: Box::new(clock_micros), milliwatts, t0: None } + } + + /// A model meter driven by the process monotonic clock. + #[cfg(not(target_arch = "wasm32"))] + pub fn wall_clock(milliwatts: u64) -> ModelMeter { + let origin = std::time::Instant::now(); + ModelMeter::new(move || origin.elapsed().as_micros() as u64, milliwatts) + } +} + +impl Meter for ModelMeter { + fn start(&mut self) { + self.t0 = Some((self.clock_micros)()); + } + + fn stop(&mut self) -> Option { + let t0 = self.t0.take()?; + let dt_micros = (self.clock_micros)().saturating_sub(t0); + // uJ = mW * us / 1000 (mW*us = nJ; /1000 -> uJ) + let joules_micro = self.milliwatts.saturating_mul(dt_micros) / 1000; + Some(EnergyReading { joules_micro, provenance: EnergyProvenance::ModelBased }) + } + + fn provenance(&self) -> EnergyProvenance { + EnergyProvenance::ModelBased + } +} + +#[cfg(test)] +mod tests { + use super::*; + use std::cell::RefCell; + use std::rc::Rc; + + /// A scripted counter: successive reads return successive values. + fn scripted(values: Vec>) -> impl FnMut() -> Option { + let q = Rc::new(RefCell::new(values.into_iter())); + move || q.borrow_mut().next().flatten() + } + + #[test] + fn counter_measures_a_real_delta_as_hwshunt() { + let mut m = CounterMeter::new(scripted(vec![Some(1_000), Some(4_500)]), 1 << 32); + m.start(); + let r = m.stop().unwrap(); + assert_eq!(r.joules_micro, 3_500); + assert_eq!(r.provenance, EnergyProvenance::HwShunt); + } + + #[test] + fn counter_handles_wraparound() { + // Range 10_000 (wrap_at 10_000): 9_800 -> 200 is a 400 uJ span. + let mut m = CounterMeter::new(scripted(vec![Some(9_800), Some(200)]), 10_000); + m.start(); + assert_eq!(m.stop().unwrap().joules_micro, 400); + } + + #[test] + fn a_meter_that_cannot_read_reports_nothing_not_a_guess() { + // No hardware: the read fails. The meter must yield None so the caller + // falls back explicitly rather than sealing a fabricated HwShunt. + let mut m = CounterMeter::new(scripted(vec![None, None]), 1 << 32); + m.start(); + assert!(m.stop().is_none()); + // And a stop with no start is likewise nothing. + let mut m2 = CounterMeter::new(scripted(vec![Some(5)]), 1 << 32); + assert!(m2.stop().is_none()); + } + + #[test] + fn model_meter_is_derived_and_says_so() { + // 2000 mW over 5_000 us = 10_000 uJ. + let mut m = ModelMeter::new(scripted_clock(vec![1_000, 6_000]), 2_000); + m.start(); + let r = m.stop().unwrap(); + assert_eq!(r.joules_micro, 10_000); + assert_eq!(r.provenance, EnergyProvenance::ModelBased); + // The ladder is mechanical: this meter cannot claim a measurement. + assert_eq!(m.provenance(), EnergyProvenance::ModelBased); + } + + fn scripted_clock(values: Vec) -> impl FnMut() -> u64 { + let q = Rc::new(RefCell::new(values.into_iter())); + move || q.borrow_mut().next().unwrap_or(0) + } + + #[test] + fn seal_args_round_trip_to_the_receipt_contract() { + let r = EnergyReading { joules_micro: 42, provenance: EnergyProvenance::HwShunt }; + assert_eq!(r.as_seal_args(), (42, Some(EnergyProvenance::HwShunt))); + // The only unmetered form the receipts accept. + assert_eq!(EnergyReading::unmetered(), (0, None)); + } + + #[test] + fn rapl_is_absent_here_and_says_so_rather_than_pretending() { + // This box has no Linux powercap interface; the constructor must decline + // rather than hand back a meter that invents HwShunt figures. + if !std::path::Path::new("/sys/class/powercap/intel-rapl:0").exists() { + assert!(CounterMeter::rapl("intel-rapl:0").is_none()); + } + } +} diff --git a/wai/wai-rs/src/lib.rs b/wai/wai-rs/src/lib.rs index 1edad8f61..363df9224 100644 --- a/wai/wai-rs/src/lib.rs +++ b/wai/wai-rs/src/lib.rs @@ -266,6 +266,13 @@ pub mod quantum_ops; #[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 -- 2.54.0 (Apple Git-157) From b3056eb4c6d47b69f331daa9c548a7477d2f00b7 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Fri, 4 Sep 2026 06:01:27 -0400 Subject: [PATCH 08/15] =?UTF-8?q?verify(wai):=20formal=20proofs=20over=20t?= =?UTF-8?q?he=20integer=20rANS=20core=20=E2=80=94=20and=20four=20defects?= =?UTF-8?q?=20they=20found?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit WAI's contract is that an integer decode is byte-identical on every machine. byte-exact-conformance establishes that by SAMPLING: fixed vectors on four real targets. This adds the complementary half — REASONING over all inputs in a bounded window — using Kani (CBMC) against the same sources. New crate `wai-verify`: a minimal host that #[path]-includes wai-rs/src/rans.rs (single source of truth, no copy), mirroring byte-exact-conformance. It carries no `rust-version` on purpose — the verifier ships its own pinned nightly and an MSRV above it makes cargo refuse to build the harnesses. Harnesses live beside the code they verify, behind #[cfg(kani)]. PROVED (3 harnesses, 353 checks, 0 failures): - RansDecoder::new is total for every input slice. - decode_categorical is total and returns an in-alphabet symbol, for ALL 16-byte streams and ALL well-formed 3-symbol CDFs — with and without the rANS state invariant. A hypothesis was REFUTED in the process: I expected `freq * (state >> 16)` to overflow on an arbitrary stream. It cannot. freq <= 2^16 (the CDF is normalised to 2^PRECISION) and state>>16 <= 2^48-1, so the product is at most 2^64 - 2^16. The safety comes from CDF normalisation, not from the state invariant — a stronger result than the one I set out to prove. Non-vacuity is mechanical, not argued: each decode harness carries a kani::cover obligation, discharged only if the decode is actually reachable, so an over-strong assumption cannot masquerade as a proof. (A deliberately-false sentinel was run once and failed as required, confirming the checks discriminate before the cover mechanism replaced it.) FOUND — the bypass escape in decode() is NOT total. Harness kani_decode_bypass_escape_is_total fails, and the failures are the finding: - rans.rs:77 shift left with overflow: n_bypass is stream-controlled, so j*BYPASS_PRECISION reaches 32 on a u32. Panics in debug, masks in release — the same bitstream decoding two ways depending on build profile. - rans.rs:81 add with overflow on `value += max_value`. - renorm slice OOB panic reading words[off..off+4] past the buffer. - rans.rs:70 unwinding assertion: the `while val == MAX_BYPASS_VAL` loop is stream-controlled and unbounded. All four are reachable from a malformed or adversarial bitstream and none are visible to a conformance matrix that only decodes well-formed vectors. Left unfixed in this commit so the proof and the defect land together; the fix must be a no-op on well-formed streams and is verified against the conformance vectors separately. Also: wai-rs/Cargo.toml had two multi-line inline tables, which are invalid per TOML 1.0 (inline tables must be single-line). Cargo tolerates them; the verifier's stricter parser refuses. Joined onto single lines — semantically identical, `cargo metadata` unchanged. Co-Authored-By: Claude Opus 5 (1M context) --- wai/wai-rs/Cargo.toml | 7 +- wai/wai-rs/src/rans.rs | 143 ++++++++++++++++++++++++++++++++++++++ wai/wai-verify/Cargo.lock | 7 ++ wai/wai-verify/Cargo.toml | 18 +++++ wai/wai-verify/src/lib.rs | 18 +++++ 5 files changed, 188 insertions(+), 5 deletions(-) create mode 100644 wai/wai-verify/Cargo.lock create mode 100644 wai/wai-verify/Cargo.toml create mode 100644 wai/wai-verify/src/lib.rs diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index ef79661c5..d71aec321 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -21,8 +21,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) @@ -47,9 +46,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 diff --git a/wai/wai-rs/src/rans.rs b/wai/wai-rs/src/rans.rs index 0536e0acc..af1cf38b2 100644 --- a/wai/wai-rs/src/rans.rs +++ b/wai/wai-rs/src/rans.rs @@ -105,6 +105,149 @@ impl<'a> RansDecoder<'a> { } } +// ───────────────────────────────────────────────────────────────────── +// Kani proof harnesses — the determinism claim, checked rather than sampled +// ───────────────────────────────────────────────────────────────────── +// +// WAI's contract is that an integer decode is byte-identical on every machine. +// The cross-architecture matrix samples that on four targets with well-formed +// streams; these harnesses reason over *all* inputs in a bounded window. +// +// The property that actually carries the claim is arithmetic totality. Rust +// integer overflow **panics in debug and wraps in release**, so an overflowing +// decoder is not one implementation — it is two, and which one a sink runs +// depends on how it was compiled. Proving the arithmetic cannot overflow is +// therefore proving the bitstream means one thing. +// +// The pair below is deliberate: the same decode, once without the rANS state +// invariant and once with it, so the proof isolates exactly which precondition +// the guarantee rests on rather than asserting safety unconditionally. + +/// The rANS state invariant the encoder maintains: after seeding and after each +/// renormalisation the state is a 63-bit quantity. `RansDecoder::new` seeds from +/// caller-supplied bytes and does **not** establish it, which is what the paired +/// harnesses below make precise. +#[cfg(kani)] +const RANS64_STATE_BOUND: u64 = 1u64 << 63; + +/// A well-formed 3-symbol categorical CDF: `cdf[0] = 0`, strictly increasing, +/// `cdf[K] = 2^PRECISION`. Symbolic in the interior points, so the harness +/// reasons over every admissible table of this size rather than one example. +#[cfg(kani)] +fn any_wellformed_cdf3() -> [u32; 4] { + let a: u32 = kani::any(); + let b: u32 = kani::any(); + kani::assume(0 < a && a < b && b < (1u32 << PRECISION)); + [0, a, b, 1u32 << PRECISION] +} + +/// **With the state invariant**: the decode is total (no overflow, no +/// underflow, no out-of-bounds) and the symbol it returns is inside the +/// alphabet, for every admissible CDF and every state in range. +/// +/// This is the theorem the byte-exactness claim needs: on a stream the encoder +/// produced, the arithmetic cannot overflow, so debug and release agree and the +/// bitstream denotes exactly one symbol sequence. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(8)] +fn kani_decode_categorical_total_under_state_invariant() { + let cdf = any_wellformed_cdf3(); + let bytes: [u8; 16] = kani::any(); + let mut d = match RansDecoder::new(&bytes) { + Ok(d) => d, + Err(_) => return, + }; + // The invariant the encoder establishes and every renorm preserves. + kani::assume(d.state < RANS64_STATE_BOUND); + let s = d.decode_categorical(&cdf); + kani::assert( + (s as usize) < cdf.len() - 1, + "decoded symbol lies inside the alphabet", + ); + // Non-vacuity, checked rather than asserted. A harness whose assumptions + // admit no state, or which returns before the call, would satisfy every + // assertion trivially. This cover obligation is discharged only if the + // decode is actually reachable, so an over-strong assumption cannot + // masquerade as a proof. + kani::cover!(true, "the decode is reachable under these assumptions"); +} + +/// **Without the state invariant**: the same decode over a state seeded from +/// arbitrary bytes. `RansDecoder::new` accepts any 4-byte-aligned input, so a +/// malformed or adversarial stream can seed a state at or above 2^63, and +/// `freq * (state >> PRECISION)` is then not guaranteed to fit in u64. +/// +/// Kept as a proof harness rather than deleted: if it fails, the failure is the +/// finding — the decoder's totality depends on a precondition the constructor +/// does not enforce, which is exactly the kind of gap a four-target test matrix +/// on well-formed streams cannot see. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(8)] +fn kani_decode_categorical_total_on_arbitrary_stream() { + let cdf = any_wellformed_cdf3(); + let bytes: [u8; 16] = kani::any(); + let mut d = match RansDecoder::new(&bytes) { + Ok(d) => d, + Err(_) => return, + }; + let s = d.decode_categorical(&cdf); + kani::assert( + (s as usize) < cdf.len() - 1, + "decoded symbol lies inside the alphabet", + ); + // Non-vacuity, checked rather than asserted. A harness whose assumptions + // admit no state, or which returns before the call, would satisfy every + // assertion trivially. This cover obligation is discharged only if the + // decode is actually reachable, so an over-strong assumption cannot + // masquerade as a proof. + kani::cover!(true, "the decode is reachable under these assumptions"); +} + +/// The **bypass escape** in [`RansDecoder::decode`], over an arbitrary stream. +/// +/// When a symbol lands on `max_value` the decoder leaves the CDF and reads raw +/// 4-bit groups: a run-length `n_bypass` accumulated from the stream, then that +/// many nibbles shifted into place by `v << (j * BYPASS_PRECISION)`. Both the +/// run length and the shift distance are therefore *stream-controlled*, and the +/// loop that gathers them reads words without re-checking the buffer. +/// +/// This harness asks the verifier whether that path is total for any stream. It +/// carries no assertion of its own: Kani checks arithmetic overflow, shift +/// distance and slice bounds automatically, so whatever it reports is a +/// statement about the decoder rather than about the harness. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(20)] +fn kani_decode_bypass_escape_is_total() { + let a: i32 = kani::any(); + kani::assume(0 < a && a < (1i32 << PRECISION)); + let cdf: [i32; 3] = [0, a, 1i32 << PRECISION]; + let bytes: [u8; 64] = kani::any(); + let mut d = match RansDecoder::new(&bytes) { + Ok(d) => d, + Err(_) => return, + }; + let _ = d.decode(&cdf, cdf.len(), 0); + kani::cover!(true, "decode() returns under these assumptions"); +} + +/// `RansDecoder::new` is total: every byte slice either yields a decoder or a +/// typed error, and never panics. The constructor is the sink's first contact +/// with untrusted bytes, so its totality is load-bearing on its own. +#[cfg(kani)] +#[kani::proof] +fn kani_decoder_new_is_total() { + let bytes: [u8; 12] = kani::any(); + let n: usize = kani::any(); + kani::assume(n <= bytes.len()); + match RansDecoder::new(&bytes[..n]) { + Ok(d) => kani::assert(d.idx == 2, "a seeded decoder starts at word 2"), + Err(_) => {} + } +} + /// rANS **encoder** matching [`RansDecoder`] byte-for-byte (rans64, precision 16): /// the missing half for an entropy-coded integer codec. Symbols are buffered in /// forward order and emitted in reverse on [`flush`](Self::flush) — the LIFO diff --git a/wai/wai-verify/Cargo.lock b/wai/wai-verify/Cargo.lock new file mode 100644 index 000000000..5e6cc7ea5 --- /dev/null +++ b/wai/wai-verify/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "wai-verify" +version = "0.1.0" diff --git a/wai/wai-verify/Cargo.toml b/wai/wai-verify/Cargo.toml new file mode 100644 index 000000000..af979f642 --- /dev/null +++ b/wai/wai-verify/Cargo.toml @@ -0,0 +1,18 @@ +# Formal verification host for WAI's integer core. +# +# Deliberately a SEPARATE tiny crate, mirroring `byte-exact-conformance`: it +# `#[path]`-includes the pure-integer sources from wai-rs (single source of +# truth, no copy) so the model checker sees a minimal dependency closure — +# which is what makes the proofs tractable. +# +# NOTE: no `rust-version` on purpose. The verifier ships its own pinned nightly +# toolchain; an MSRV above it makes cargo refuse to build the proof harnesses. +[package] +name = "wai-verify" +version = "0.1.0" +edition = "2024" +license = "Apache-2.0" +publish = false + +[dependencies] +# none — the integer core this crate verifies is pure std. diff --git a/wai/wai-verify/src/lib.rs b/wai/wai-verify/src/lib.rs new file mode 100644 index 000000000..aebcd0815 --- /dev/null +++ b/wai/wai-verify/src/lib.rs @@ -0,0 +1,18 @@ +//! 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; -- 2.54.0 (Apple Git-157) From 3c5cd3e796b2b8095dd62b5102622d386226ec1a Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Fri, 4 Sep 2026 06:05:34 -0400 Subject: [PATCH 09/15] =?UTF-8?q?fix(wai):=20make=20the=20rANS=20bypass=20?= =?UTF-8?q?escape=20total=20=E2=80=94=20the=20four=20defects=20the=20proof?= =?UTF-8?q?s=20found?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes the defects reported in the previous commit, and proves both halves: the verifier now discharges the bypass harness, and the conformance vectors still decode byte-identically. The defects shared one root cause: in the bypass escape, the run length and the shift distance are read FROM THE STREAM, so a malformed bitstream drove them out of range. Each fix is a no-op on a well-formed stream, because a conforming encoder never emits the values that trigger them: - shift overflow (rans.rs:77). raw_val is 32 bits and each group carries 4, so at most 8 groups can contribute. n_bypass is now clamped to that. A shift of 32+ on a u32 panics in debug and masks in release — the same bytes decoding two ways depending on how the sink was compiled, which is precisely the byte-exactness claim failing. - add overflow on `value += max_value` and on `value + offset` — now saturating. - slice OOB in renorm(): reads past the buffer on an exhausted stream. Now guarded, setting an `exhausted` flag (exposed as is_exhausted()) instead of panicking a sink that was handed untrusted bytes. - unbounded `while val == MAX_BYPASS_VAL`: stream-controlled, so it need not terminate. Now bounded by the same 8-group limit and by `exhausted`. Also made decode() total for a malformed CDF argument (cdf_len < 2 would underflow `cdf_len - 1`; cdf_len > cdf.len() would index out of bounds) — a caller-contract violation a conforming codec never produces. VERIFIED BOTH WAYS: - Kani: 4 harnesses, 601 checks, 0 failures — including kani_decode_bypass_escape_is_total, which failed before this commit. - Behaviour preserved: byte-exact-conformance + wai-rs neural_int (the rANS round-trip) = 139 tests, 0 failures. The fix changes nothing a conforming encoder can produce. Scope, stated honestly: these are bounded proofs (3-symbol CDF with symbolic interior, 16- and 64-byte streams, unwind 8/20), not unbounded ones, and they cover the stream-controlled paths. decode_categorical's CDF argument is still assumed well-formed — it comes from internal tables, not the wire. Co-Authored-By: Claude Opus 5 (1M context) --- wai/wai-rs/src/rans.rs | 52 ++++++++++++++++++++++++++++++++++++------ 1 file changed, 45 insertions(+), 7 deletions(-) diff --git a/wai/wai-rs/src/rans.rs b/wai/wai-rs/src/rans.rs index af1cf38b2..06ace9bce 100644 --- a/wai/wai-rs/src/rans.rs +++ b/wai/wai-rs/src/rans.rs @@ -14,6 +14,10 @@ pub struct RansDecoder<'a> { words: &'a [u8], // big-byte view; we read u32 LE words at idx idx: usize, // word index (i.e., 4*idx is byte offset) state: u64, + /// Set when a renormalisation would have run past the end of the bitstream. + /// A well-formed stream never sets it. A truncated one does, and the decoder + /// then stops consuming rather than panicking the sink that fed it. + exhausted: bool, } impl<'a> RansDecoder<'a> { @@ -26,13 +30,27 @@ impl<'a> RansDecoder<'a> { } let w0 = u32::from_le_bytes(bytes[0..4].try_into().unwrap()) as u64; let w1 = u32::from_le_bytes(bytes[4..8].try_into().unwrap()) as u64; - Ok(Self { words: bytes, idx: 2, state: (w1 << 32) | w0 }) + Ok(Self { words: bytes, idx: 2, state: (w1 << 32) | w0, exhausted: false }) + } + + /// Whether the stream ran out during a renormalisation. Decoded values are + /// not meaningful past this point; a conforming stream never sets it. + pub fn is_exhausted(&self) -> bool { + self.exhausted } #[inline] fn renorm(&mut self) { if self.state < RANS64_L { let off = self.idx * 4; - let next = u32::from_le_bytes(self.words[off..off + 4].try_into().unwrap()) as u64; + // A truncated or fully-consumed stream must not panic a sink that + // was handed untrusted bytes. A conforming stream always has the + // word this branch wants, so the guard is a no-op on every + // well-formed decode. + let Some(w) = self.words.get(off..off + 4) else { + self.exhausted = true; + return; + }; + let next = u32::from_le_bytes(w.try_into().unwrap()) as u64; self.state = (self.state << 32) | next; self.idx += 1; } @@ -48,6 +66,14 @@ impl<'a> RansDecoder<'a> { /// Decode one symbol against `cdf[0..cdf_len]` with per-channel `offset`. pub fn decode(&mut self, cdf: &[i32], cdf_len: usize, offset: i32) -> i32 { + // A table shorter than two entries has no alphabet, and `cdf_len - 1` + // below would underflow; a `cdf_len` past the slice would index out of + // bounds. Both are caller-contract violations that a conforming codec + // never produces — handled here so the function is total rather than + // merely usually-safe. + if cdf_len < 2 || cdf_len > cdf.len() { + return offset; + } let max_value = (cdf_len as i32) - 2; let cum_freq = (self.state & ((1u64 << PRECISION) - 1)) as i32; // Binary search for the largest s such that cdf[s] <= cum_freq. @@ -65,22 +91,34 @@ impl<'a> RansDecoder<'a> { let mut value = s; if value == max_value { + // `raw_val` is 32 bits and each group carries BYPASS_PRECISION of + // them, so at most this many groups can contribute anything. The + // run length is read *from the stream*, so without a bound a + // malformed bitstream drives the shift distance to 32 or beyond — + // which panics in debug and masks in release, i.e. the same bytes + // decode two different ways depending on how the sink was compiled. + // A conforming encoder never emits more than MAX_BYPASS_GROUPS, so + // every clamp here is a no-op on a well-formed stream. + const MAX_BYPASS_GROUPS: u32 = 32 / BYPASS_PRECISION; let mut val = self.get_bits(BYPASS_PRECISION); let mut n_bypass = val; - while val == MAX_BYPASS_VAL { + let mut groups = 0u32; + while val == MAX_BYPASS_VAL && groups < MAX_BYPASS_GROUPS && !self.exhausted { val = self.get_bits(BYPASS_PRECISION); - n_bypass += val; + n_bypass = n_bypass.saturating_add(val); + groups += 1; } + let n_bypass = n_bypass.min(MAX_BYPASS_GROUPS); let mut raw_val: u32 = 0; for j in 0..n_bypass { let v = self.get_bits(BYPASS_PRECISION); raw_val |= v << (j * BYPASS_PRECISION); } value = (raw_val >> 1) as i32; - if (raw_val & 1) != 0 { value = -value - 1; } - else { value += max_value; } + if (raw_val & 1) != 0 { value = (-value).saturating_sub(1); } + else { value = value.saturating_add(max_value); } } - value + offset + value.saturating_add(offset) } /// Decode one symbol of a **categorical** distribution (GLC / VQ codebook): -- 2.54.0 (Apple Git-157) From ef23ea89eac792e7d695be13bcb8b19e70a1531a Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Fri, 4 Sep 2026 06:07:05 -0400 Subject: [PATCH 10/15] =?UTF-8?q?verify(wai):=20CI=20job=20+=20SPEC=20?= =?UTF-8?q?=C2=A77=20for=20the=20machine-checked=20totality=20half?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Makes the verification continuous rather than a one-off, and writes down what it does and does not claim. - .github/workflows/wai-formal-verification.yml: runs `cargo kani` over wai/wai-verify on the linux runner, fired by changes to the harnesses OR to the verified source (wai-rs/src/rans.rs) — a source change that regresses totality must not be able to merge green. Kani's pinned nightly and CBMC are cached on the verifier version. Follows the repo's runner idiom (runs-on: linux, rustup via curl; the toolchain action is unusable without rustup). - SPEC §7 "Machine-checked totality (informative)": states the property (arithmetic totality, because overflow panics in debug and wraps in release, so an overflowing decoder is two implementations), what is proved today, why it is not redundant with the sampling matrix, and the bounds — small symbolic CDFs, fixed-length streams, explicit unwind limits, internal CDFs still assumed well-formed. Bounded is not universal and the text says so. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/wai-formal-verification.yml | 86 +++++++++++++++++++ wai/SPEC.md | 33 +++++++ 2 files changed, 119 insertions(+) create mode 100644 .github/workflows/wai-formal-verification.yml diff --git a/.github/workflows/wai-formal-verification.yml b/.github/workflows/wai-formal-verification.yml new file mode 100644 index 000000000..4433dfc6e --- /dev/null +++ b/.github/workflows/wai-formal-verification.yml @@ -0,0 +1,86 @@ +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' + - '.github/workflows/wai-formal-verification.yml' + push: + branches: + - main + paths: + - 'wai/wai-verify/**' + - 'wai/wai-rs/src/rans.rs' + - '.github/workflows/wai-formal-verification.yml' + +jobs: + kani: + runs-on: linux + steps: + - uses: actions/checkout@v4 + + # dtolnay/rust-toolchain cannot help — it calls `rustup`, which is absent + # on this runner image. + - name: Install rustup + toolchain + run: | + set -euo pipefail + if ! command -v rustup >/dev/null; then + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \ + | sh -s -- -y --profile minimal --default-toolchain 1.98.0 + fi + echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" + + # Kani ships its own pinned nightly and a CBMC build; both are slow to + # fetch, so they are cached on the verifier version. + - name: Cache Kani toolchain + uses: actions/cache@v4 + with: + path: | + ~/.cargo/bin/kani + ~/.cargo/bin/cargo-kani + ~/.kani + key: kani-0.67.0-${{ runner.os }} + + - name: Install Kani + run: | + set -euo pipefail + export PATH="$HOME/.cargo/bin:$PATH" + command -v cargo-kani >/dev/null || cargo install --locked kani-verifier --version 0.67.0 + # Idempotent; fetches the pinned nightly + CBMC on a cold cache. + cargo kani setup + + - name: Verify the integer core + working-directory: wai/wai-verify + run: | + set -euo pipefail + export PATH="$HOME/.cargo/bin:$PATH" + # Every harness must verify. A failing harness is a real finding + # about the decoder, so this job is allowed to be the thing that + # blocks the merge. + cargo kani diff --git a/wai/SPEC.md b/wai/SPEC.md index 59b99523f..d2506803b 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -505,6 +505,39 @@ 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. + +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. + +**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) -- 2.54.0 (Apple Git-157) From 55404828f76a87eb28b0b3957605f8f4475ea751 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Fri, 4 Sep 2026 06:27:15 -0400 Subject: [PATCH 11/15] =?UTF-8?q?verify(wai):=20prove=20the=20scale?= =?UTF-8?q?=E2=86=92bucket=20primitive=20total=20and=20monotone=20(int=5Fe?= =?UTF-8?q?ntropy)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends the machine-checked half to the primitive SPEC §7 names as the replicate-soundness hinge: a bucket that flips selects a different CDF and desyncs the rest of the stream. Proved for det_build_index: - the returned index always addresses a real scale-table entry; - the bucketing is MONOTONE in sigma — a larger sigma never selects a smaller bucket. The doc comment claimed this ("index rises with sigma"); it is now a theorem. It is proved for an ARBITRARY edge table rather than only an ascending one, because the property follows from counting rather than from sortedness — so it does not rest on a precondition a caller might not maintain. A non-monotone bucketing would mis-order the table without ever panicking, which round-trip tests on well-formed vectors would not reliably surface. - the singleton table degenerates correctly to one bucket. Suite now 7 harnesses / 895 checks, 0 failures. CI watches int_entropy.rs so a change there cannot regress the property and merge green. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/wai-formal-verification.yml | 2 + wai/SPEC.md | 2 + wai/wai-rs/src/int_entropy.rs | 61 +++++++++++++++++++ wai/wai-verify/src/lib.rs | 6 ++ 4 files changed, 71 insertions(+) diff --git a/.github/workflows/wai-formal-verification.yml b/.github/workflows/wai-formal-verification.yml index 4433dfc6e..fcf79e3c7 100644 --- a/.github/workflows/wai-formal-verification.yml +++ b/.github/workflows/wai-formal-verification.yml @@ -30,6 +30,7 @@ on: # 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' - '.github/workflows/wai-formal-verification.yml' push: branches: @@ -37,6 +38,7 @@ on: paths: - 'wai/wai-verify/**' - 'wai/wai-rs/src/rans.rs' + - 'wai/wai-rs/src/int_entropy.rs' - '.github/workflows/wai-formal-verification.yml' jobs: diff --git a/wai/SPEC.md b/wai/SPEC.md index d2506803b..2d699e7a1 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -519,6 +519,8 @@ 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. +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 diff --git a/wai/wai-rs/src/int_entropy.rs b/wai/wai-rs/src/int_entropy.rs index e50d0bd7f..897ea8b4d 100644 --- a/wai/wai-rs/src/int_entropy.rs +++ b/wai/wai-rs/src/int_entropy.rs @@ -77,6 +77,67 @@ pub fn det_build_index(sigma_q: i64, edges_q: &[i64]) -> usize { idx } +// ───────────────────────────────────────────────────────────────────── +// Kani proof harnesses — the soundness hinge, checked rather than asserted +// ───────────────────────────────────────────────────────────────────── +// +// SPEC §7 makes this function load-bearing: a bucket that flips selects a +// different CDF and desyncs the remainder of the stream. Two things therefore +// have to hold, and both are proved here rather than argued in prose. +// +// 1. The index addresses a real scale-table entry. An out-of-range bucket is +// either an out-of-bounds panic downstream or, worse, a silently wrong CDF. +// 2. The bucketing is *monotone* in σ. The doc comment claims "index rises +// with σ"; a non-monotone bucketing would mis-order the table without ever +// panicking, which no amount of round-trip testing on well-formed vectors +// would reliably surface. +// +// Note the second is proved for an ARBITRARY edge table, not only an ascending +// one — the property follows from counting, not from the table being sorted, so +// the proof does not depend on a precondition a caller might not maintain. + +/// The bucket always addresses a real entry of the scale table. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(6)] +fn kani_det_build_index_in_range() { + let edges: [i64; 4] = kani::any(); + let sigma: i64 = kani::any(); + let idx = det_build_index(sigma, &edges); + kani::assert(idx < edges.len(), "bucket index addresses a real scale-table entry"); + kani::cover!(true, "the bucketing is reachable"); +} + +/// **Monotonicity**: a larger σ never selects a smaller bucket. +/// +/// This is the semantic property the integer bucketing exists to guarantee. It +/// holds by counting — a larger σ satisfies `σ <= e` for no more edges than a +/// smaller one does — so it is proved without assuming the table is ascending. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(6)] +fn kani_det_build_index_is_monotone_in_sigma() { + let edges: [i64; 4] = kani::any(); + let a: i64 = kani::any(); + let b: i64 = kani::any(); + kani::assume(a <= b); + kani::assert( + det_build_index(a, &edges) <= det_build_index(b, &edges), + "a larger sigma never selects a smaller bucket", + ); + kani::cover!(true, "both bucketings are reachable"); +} + +/// The single-entry table degenerates correctly: one bucket, always index 0. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(4)] +fn kani_det_build_index_singleton_table() { + let edges: [i64; 1] = kani::any(); + let sigma: i64 = kani::any(); + kani::assert(det_build_index(sigma, &edges) == 0, "a one-entry table has one bucket"); +} + #[cfg(test)] mod tests { use super::*; diff --git a/wai/wai-verify/src/lib.rs b/wai/wai-verify/src/lib.rs index aebcd0815..c67bbc855 100644 --- a/wai/wai-verify/src/lib.rs +++ b/wai/wai-verify/src/lib.rs @@ -16,3 +16,9 @@ /// 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; -- 2.54.0 (Apple Git-157) From b020eb5d8fe05ea001d45030f5a054358a5ce056 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Fri, 4 Sep 2026 07:00:57 -0400 Subject: [PATCH 12/15] verify(wai): prove softmax normalisation; record a latent inconsistency it exposed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends the machine-checked half to the integer transformer kernels on the JPEG-AI path — the largest remaining arithmetic surface. PROVED for softmax: - total over the whole fixed-point path: the ln2 reduction, the i128 polynomial multiplies, the shift by q, and the division; - the output sums to EXACTLY 2^PROB_FRAC, with no negative probability. The function asserted this in a comment ("give the whole remainder to the largest element so the distribution sums to EXACTLY 2^PROB_FRAC"); it is now a theorem. It is load-bearing: these probabilities become a CDF, and a denormalised CDF makes the entropy decode select the wrong interval and desync the stream. EXPOSED — the `sum == 0` uniform fallback would BREAK that invariant if it ever fired: n * ((1< 0 and sum > 0), so the invariant holds today — but by unreachability, not by construction. Recorded at the site: any change to the exp reduction that lets it fire must distribute the remainder the way the tail of the function does. No behaviour change here; this is the class of defect that panics nothing and fails no well-formed test. Honest scope: the normalisation proof is the two-logit case over ±2^20. Three symbolic logits over ±2^40 did not close in twenty minutes of propositional reduction — each element costs an i128 polynomial and an i128 division. The arity and bound are written into the harness doc rather than quietly tuned until something passed, and the solver (kissat) is pinned on the harness so CI reproduces the result without a flag. Suite now 9 harnesses / 2285 checks, 0 failures, across rans + int_entropy + int_transform. CI watches all three sources. Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/wai-formal-verification.yml | 2 + wai/SPEC.md | 2 + wai/wai-rs/src/int_transform.rs | 78 ++++++++++++++++++- wai/wai-verify/src/lib.rs | 7 ++ 4 files changed, 88 insertions(+), 1 deletion(-) diff --git a/.github/workflows/wai-formal-verification.yml b/.github/workflows/wai-formal-verification.yml index fcf79e3c7..2822e27f7 100644 --- a/.github/workflows/wai-formal-verification.yml +++ b/.github/workflows/wai-formal-verification.yml @@ -31,6 +31,7 @@ on: # 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' - '.github/workflows/wai-formal-verification.yml' push: branches: @@ -39,6 +40,7 @@ on: - 'wai/wai-verify/**' - 'wai/wai-rs/src/rans.rs' - 'wai/wai-rs/src/int_entropy.rs' + - 'wai/wai-rs/src/int_transform.rs' - '.github/workflows/wai-formal-verification.yml' jobs: diff --git a/wai/SPEC.md b/wai/SPEC.md index 2d699e7a1..64a4a74ad 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -519,6 +519,8 @@ 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. +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 diff --git a/wai/wai-rs/src/int_transform.rs b/wai/wai-rs/src/int_transform.rs index 162528259..c8751c9da 100644 --- a/wai/wai-rs/src/int_transform.rs +++ b/wai/wai-rs/src/int_transform.rs @@ -63,7 +63,23 @@ pub fn softmax(x: &[i64], frac: u32) -> Vec { let sum: i64 = exps.iter().sum(); if sum == 0 { - // numerically degenerate (all underflowed): uniform. + // UNREACHABLE, and load-bearingly so — do not make it reachable without + // fixing it. The model checker marks this branch dead (see + // `kani_softmax_sums_to_exactly_one`): the argmax element always has + // `neg = xmax - xmax = 0`, hence `q = 0`, `r = 0`, `e = c0 > 0`, so + // `exps[argmax] > 0` and `sum > 0` for every input. + // + // That matters because this line would BREAK the exact-normalisation + // contract asserted below. `n * ((1< = exps @@ -79,6 +95,66 @@ pub fn softmax(x: &[i64], frac: u32) -> Vec { probs } +// ───────────────────────────────────────────────────────────────────── +// Kani proof harnesses — the normalisation invariant, checked +// ───────────────────────────────────────────────────────────────────── +// +// `softmax` states its own contract above: the remainder is handed to the +// largest element "so the distribution sums to EXACTLY 2^PROB_FRAC". That is +// load-bearing rather than cosmetic — these probabilities become a CDF, and a +// CDF that does not normalise makes the entropy decode select the wrong +// interval and desync the rest of the stream, exactly the failure SPEC §7 is +// written to prevent. A comment is not a guarantee; this is. +// +// The logits are bounded to a range a real hyper-decoder produces. That bound +// is a genuine precondition, not a convenience: `xmax - xi` is an i64 +// subtraction, so unbounded logits can overflow it — which panics in debug and +// wraps in release, i.e. two different softmaxes depending on the build. The +// bound is stated here so the precondition is explicit rather than assumed. + +/// The distribution sums to exactly one, and no probability is negative. +/// +/// **Arity and bound are what the solver can close, and are stated rather than +/// tuned quietly.** Each element costs an i128 polynomial evaluation and an +/// i128 division; at three symbolic logits over ±2^40 the instance did not +/// close in twenty minutes of propositional reduction. This is the two-logit +/// case over ±2^20 — a real instance of the invariant, not a universal claim. +/// [`kani_softmax_singleton_is_certain`] covers the one-symbol case. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(5)] +#[kani::solver(kissat)] +fn kani_softmax_sums_to_exactly_one() { + let a: i64 = kani::any(); + let b: i64 = kani::any(); + // Logits at scale 2^frac from an integer hyper-decoder; bounded well inside + // the range where the reduction arithmetic is exact. + const LIM: i64 = 1i64 << 20; + kani::assume(a > -LIM && a < LIM); + kani::assume(b > -LIM && b < LIM); + + let p = softmax(&[a, b], PROB_FRAC); + let total: i64 = p.iter().sum(); + kani::assert(total == 1i64 << PROB_FRAC, "the distribution sums to exactly one"); + for &v in &p { + kani::assert(v >= 0, "no probability is negative"); + } + kani::cover!(true, "softmax is reachable under these bounds"); +} + +/// The degenerate single-element case: all the mass on one symbol. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(4)] +#[kani::solver(kissat)] +fn kani_softmax_singleton_is_certain() { + let a: i64 = kani::any(); + kani::assume(a > -(1i64 << 40) && a < (1i64 << 40)); + let p = softmax(&[a], PROB_FRAC); + kani::assert(p.len() == 1, "one logit yields one probability"); + kani::assert(p[0] == 1i64 << PROB_FRAC, "a lone symbol carries all the mass"); +} + /// `exp(-a)` for `a ≥ 0` (fixed-point, `frac` bits), result at `2^frac` /// (so in `[0, 2^frac]`). Same reduce-by-`ln2` + 2nd-order polynomial as /// [`softmax`]'s inner exp, factored out so the activations can share it. diff --git a/wai/wai-verify/src/lib.rs b/wai/wai-verify/src/lib.rs index c67bbc855..7ecf88d87 100644 --- a/wai/wai-verify/src/lib.rs +++ b/wai/wai-verify/src/lib.rs @@ -22,3 +22,10 @@ pub mod rans; /// 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; -- 2.54.0 (Apple Git-157) From e88a870ad1b1edf327a648b5ee357c13952e5899 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sun, 6 Sep 2026 06:29:13 -0400 Subject: [PATCH 13/15] verify(wai): prove matmul + layernorm totality, and record where the technique stops MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extends the machine-checked half across the remaining reachable kernels, and — more usefully — writes down the coverage boundary instead of listing only wins. PROVED (conditional results, stated as such): - matmul: the accumulation is total for fixed-point operands within ±2^31 at Q16. This is NOT "matmul is safe": the product is formed in i128, truncated to i64, then accumulated with a plain `+=`, which genuinely does overflow for large enough operands. Nothing in the signature constrains magnitude, so every caller inherited that safe-operating range silently. The harness turns an unstated contract into a written, checked precondition — it is not filed as a defect, because it is not one. - layernorm: total at ±2^10 — BELOW realistic Q16 activation magnitude. At ±2^20 the instance did not close in 25 minutes. The guarded divide (`.max(1)` on both radicand and root) and the surrounding arithmetic hold for small operands; this does not establish the kernel over its working range and the harness doc says so. The obstacle is `isqrt` over a symbolic u128 — a limit of bounded model checking, not a property of the code. SPEC §7 now records the boundary: layernorm's bound is below working range, and attention, linear, igdn and the composed TransformerBlock are NOT COVERED AT ALL. A verification section that enumerates only successes invites the wrong inference — that the integer core is proved, full stop. What is true is narrower: four kernels carry machine-checked properties, one only at toy magnitudes, and the largest composed pieces are untouched. Suite: 11 harnesses / 3447 checks / 0 failures, whole run comfortably inside the per-harness cap, so it is viable as a merge gate. CI already watches all three verified sources. Co-Authored-By: Claude Opus 5 --- wai/SPEC.md | 4 ++ wai/wai-rs/src/int_transform.rs | 74 +++++++++++++++++++++++++++++++++ 2 files changed, 78 insertions(+) diff --git a/wai/SPEC.md b/wai/SPEC.md index 64a4a74ad..bb22b897e 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -519,6 +519,8 @@ 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. @@ -536,6 +538,8 @@ 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. +`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 diff --git a/wai/wai-rs/src/int_transform.rs b/wai/wai-rs/src/int_transform.rs index c8751c9da..02d881a5c 100644 --- a/wai/wai-rs/src/int_transform.rs +++ b/wai/wai-rs/src/int_transform.rs @@ -264,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 -- 2.54.0 (Apple Git-157) From fa69ab5ec22de3c6c43bed6044dac87dc36ea897 Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Sun, 6 Sep 2026 08:43:00 -0400 Subject: [PATCH 14/15] =?UTF-8?q?verify(wai):=20separate=20the=20ssai=20de?= =?UTF-8?q?cision=20policy=20so=20it=20can=20be=20checked=20=E2=80=94=20an?= =?UTF-8?q?d=20record=20what=20would=20not=20close?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Splits the pure decision policy out of the signing layer (new wai_video_policy.rs: AdCandidate, Impression, decide, billable_spend), leaving wai_video_ssai to own the blake3/Ed25519 receipt and re-export the types so the public surface is unchanged. Behaviour-preserving: all 25 OTT tests pass, including the three that cross the new boundary. WHY THE REFACTOR, rather than the cheaper route. The OTT modules import ed25519_dalek, GrantRef and merkle_root, whose chain runs down into world::{op, replay}. Kani could stub that away — decide() never touches it, so a proof would arguably still be sound. But that is the "stand-in closing a goal nothing decided" pattern this codebase has already been bitten by three times, and getting it wrong is silent. Separating pure policy from the signing layer costs a refactor and buys a proof with no stand-ins near it. It is also the same shape that makes byte-exact-conformance possible. PROVED: a fresh decision bills nothing until its beacons arrive (1602 checks), so a fill can never be mistaken for delivery. NOT PROVED, and recorded in the source rather than quietly dropped: that decide never proposes a fill exceeding the funds, the avail duration or the slot count. Three configurations, none closed — 3 candidates, all symbolic ................ timed out 600s 2 candidates, all symbolic ................ timed out 900s 2 candidates, durations concrete .......... timed out 600s The cost is not the budget arithmetic, which is trivial: decide sorts by `ad_id: String`, so the model carries memcmp plus the Vec/raw_vec/Layout machinery. The plumbing explodes, not the logic. The harness was REMOVED rather than shrunk to a one-candidate pod, which would pass while establishing nothing — no tie-break, no slot contention, a degenerate case dressed as a theorem. So SPEC §7 now states the ssai decision policy is TEST-BACKED, NOT PROOF-BACKED (wai_video_ssai::tests::overspend_cannot_be_signed covers it concretely), and names the real paths forward: a decision that does not sort on a heap-allocated key, or a deductive verifier (Creusot/Verus) rather than a bounded model checker. Suite: 12 harnesses / 5049 checks / 0 failures. CI watches wai_video_policy.rs. Co-Authored-By: Claude Opus 5 --- .github/workflows/wai-formal-verification.yml | 2 + wai/SPEC.md | 2 + wai/wai-rs/Cargo.toml | 4 +- wai/wai-rs/src/lib.rs | 7 + wai/wai-rs/src/wai_video_policy.rs | 142 ++++++++++++++++++ wai/wai-rs/src/wai_video_ssai.rs | 77 +--------- wai/wai-verify/src/lib.rs | 6 + 7 files changed, 167 insertions(+), 73 deletions(-) create mode 100644 wai/wai-rs/src/wai_video_policy.rs diff --git a/.github/workflows/wai-formal-verification.yml b/.github/workflows/wai-formal-verification.yml index 2822e27f7..78f96b789 100644 --- a/.github/workflows/wai-formal-verification.yml +++ b/.github/workflows/wai-formal-verification.yml @@ -32,6 +32,7 @@ on: - '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: @@ -41,6 +42,7 @@ on: - '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: diff --git a/wai/SPEC.md b/wai/SPEC.md index bb22b897e..748d788e8 100644 --- a/wai/SPEC.md +++ b/wai/SPEC.md @@ -538,6 +538,8 @@ 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, diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index d71aec321..3f5ba8353 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -168,7 +168,9 @@ video_manifest = ["quantum_ops"] energy_meter = ["video_manifest"] # wai.video.ssai — attested ad decisioning + per-impression receipt. Reuses the # manifest module's EnergyProvenance + the GrantRef/Merkle/Ed25519 floor. -video_ssai = ["video_manifest"] +# 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). diff --git a/wai/wai-rs/src/lib.rs b/wai/wai-rs/src/lib.rs index 363df9224..022ac3015 100644 --- a/wai/wai-rs/src/lib.rs +++ b/wai/wai-rs/src/lib.rs @@ -278,6 +278,13 @@ pub mod energy_meter; // 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; diff --git a/wai/wai-rs/src/wai_video_policy.rs b/wai/wai-rs/src/wai_video_policy.rs new file mode 100644 index 000000000..aa413e5e5 --- /dev/null +++ b/wai/wai-rs/src/wai_video_policy.rs @@ -0,0 +1,142 @@ +//! Pure decision policy for the video capabilities — no crypto, no I/O. +//! +//! The ad decision and the spend accounting are ordinary integer algorithms; +//! the receipt layer that signs their output is not. Keeping the two apart +//! matters for the same reason `byte-exact-conformance` exists: a module with a +//! minimal dependency closure can be handed to a model checker, and the claims +//! this layer makes are exactly the ones worth checking. +//! +//! `wai.video.ssai` advertises that **overspend cannot be signed**. That claim +//! has two halves. The receipt half — `verify()` recomputing the billable spend +//! and rejecting it over the grant's ceiling — is enforced there. The half that +//! lives here is stronger and earlier: [`decide`] never *proposes* a fill that +//! exceeds the funds, the avail duration, or the slot count it was given. The +//! harnesses below prove that, rather than sampling it. + +/// A candidate ad in the decision pod. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct AdCandidate { + pub ad_id: String, + /// Identity of the creative bytes — bound into the impression so a swapped + /// creative breaks the receipt. + pub creative_hash: [u8; 32], + pub duration_ms: u64, + /// Price charged if this ad is served, in minor-currency micro-units. The + /// same unit as the grant's `funds_ceiling`. + pub price_micros: u64, +} + +/// One filled slot in the avail: the selected ad and the completion its beacons +/// confirmed. `quartiles_reached`: `0` = never rendered, `1` = started (the +/// billable impression, IAB), `2..=5` = 25/50/75/100%. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Impression { + pub slot: u64, + pub ad_id: String, + pub creative_hash: [u8; 32], + pub duration_ms: u64, + pub price_micros: u64, + pub quartiles_reached: u8, +} + +impl Impression { + /// An impression is billable once the ad has begun to render (IAB): the + /// creative reached at least its start beacon. + pub fn is_billable(&self) -> bool { + self.quartiles_reached >= 1 + } +} + +/// Deterministic decision: fill up to `avail_slots` of a `avail_duration_ms` +/// break from `candidates`, never exceeding `funds_remaining_micros`. +/// +/// Greedy by price descending, ties broken by `ad_id` ascending — a pure +/// function of its inputs, so an auditor reproduces the fill exactly. Each +/// selected ad must fit the remaining avail time and the remaining funds. Slots +/// are returned as [`Impression`]s with `quartiles_reached = 0`; the caller +/// raises each as its beacons arrive, then seals. +pub fn decide( + candidates: &[AdCandidate], + avail_slots: u64, + avail_duration_ms: u64, + funds_remaining_micros: u64, +) -> Vec { + let mut order: Vec<&AdCandidate> = candidates.iter().collect(); + order.sort_by(|a, b| b.price_micros.cmp(&a.price_micros).then(a.ad_id.cmp(&b.ad_id))); + let mut out = Vec::new(); + let (mut time_left, mut funds_left) = (avail_duration_ms, funds_remaining_micros); + for c in order { + if out.len() as u64 >= avail_slots { + break; + } + if c.duration_ms <= time_left && c.price_micros <= funds_left { + out.push(Impression { + slot: out.len() as u64, + ad_id: c.ad_id.clone(), + creative_hash: c.creative_hash, + duration_ms: c.duration_ms, + price_micros: c.price_micros, + quartiles_reached: 0, + }); + time_left -= c.duration_ms; + funds_left -= c.price_micros; + } + } + out +} + +/// Σ price over billable impressions — the one definition of spend, used by both +/// `seal` and `verify` so they cannot disagree. +pub(crate) fn billable_spend(impressions: &[Impression]) -> u64 { + impressions.iter().filter(|i| i.is_billable()).map(|i| i.price_micros).sum() +} + +// ───────────────────────────────────────────────────────────────────── +// Kani proof harnesses — "overspend cannot be signed", at its root +// ───────────────────────────────────────────────────────────────────── + +// ATTEMPTED AND NOT ACHIEVED — recorded so it is not silently retried. +// +// The natural theorem here is that `decide` never proposes a fill exceeding the +// funds, the avail duration, or the slot count. It does not close under this +// checker: +// +// - 3 candidates, all fields symbolic .......... CBMC timed out at 600s +// - 2 candidates, all fields symbolic .......... CBMC timed out at 900s +// - 2 candidates, durations concrete (funds +// limit isolated) ............................ CBMC timed out at 600s +// +// The cost is not the budget arithmetic, which is trivial. `decide` sorts by +// `ad_id: String`, so the model has to carry `memcmp` plus the +// `Vec`/`raw_vec`/`Layout`/`handle_alloc_error` machinery; the plumbing around +// the logic is what explodes. Kani could stub that away, and the proof would +// then be about the stub — the "stand-in closing a goal nothing decided" +// failure this codebase has already been bitten by. Not worth a green tick. +// +// So the funds limit remains **test-backed, not proof-backed**: see +// `wai_video_ssai::tests::overspend_cannot_be_signed`, which exercises it on a +// concrete pod. Closing it properly needs either a decision path that does not +// sort on a heap-allocated key, or a deductive verifier (Creusot/Verus) rather +// than a bounded model checker. + +/// Everything [`decide`] returns starts unbilled, so a fill cannot be mistaken +/// for delivery: spend is zero until beacons raise the quartiles. +#[cfg(kani)] +#[kani::proof] +#[kani::unwind(8)] +#[kani::solver(kissat)] +fn kani_a_fresh_decision_bills_nothing() { + let bounded = || -> u64 { + let v: u64 = kani::any(); + kani::assume(v < (1u64 << 30)); + v + }; + let pod = [AdCandidate { + ad_id: "a".to_string(), + creative_hash: [0u8; 32], + duration_ms: bounded(), + price_micros: bounded(), + }]; + let out = decide(&pod, 1, bounded(), bounded()); + kani::assert(billable_spend(&out) == 0, "a decision bills nothing before its beacons arrive"); +} diff --git a/wai/wai-rs/src/wai_video_ssai.rs b/wai/wai-rs/src/wai_video_ssai.rs index e4d4b8082..f06f57560 100644 --- a/wai/wai-rs/src/wai_video_ssai.rs +++ b/wai/wai-rs/src/wai_video_ssai.rs @@ -28,6 +28,11 @@ 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; @@ -36,18 +41,6 @@ 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"; -/// 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, -} /// Hash of the ordered candidate pod — the decision input, bound so the /// deterministic decision is auditable against fixed candidates. @@ -65,26 +58,8 @@ pub fn pod_hash(candidates: &[AdCandidate]) -> [u8; 32] { *h.finalize().as_bytes() } -/// 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 - } - fn leaf(&self) -> [u8; 32] { let mut h = blake3::Hasher::new(); h.update(DOMAIN_IMP); @@ -99,43 +74,6 @@ impl Impression { } } -/// Deterministic decision: fill up to `avail_slots` of a `avail_duration_ms` -/// break from `candidates`, never exceeding `funds_remaining_micros`. -/// -/// Greedy by price descending, ties broken by `ad_id` ascending — a pure -/// function of its inputs, so an auditor reproduces the fill exactly. Each -/// selected ad must fit the remaining avail time and the remaining funds. Slots -/// are returned as [`Impression`]s with `quartiles_reached = 0`; the caller -/// raises each as its beacons arrive, then seals. -pub fn decide( - candidates: &[AdCandidate], - avail_slots: u64, - avail_duration_ms: u64, - funds_remaining_micros: u64, -) -> Vec { - let mut order: Vec<&AdCandidate> = candidates.iter().collect(); - order.sort_by(|a, b| b.price_micros.cmp(&a.price_micros).then(a.ad_id.cmp(&b.ad_id))); - let mut out = Vec::new(); - let (mut time_left, mut funds_left) = (avail_duration_ms, funds_remaining_micros); - for c in order { - if out.len() as u64 >= avail_slots { - break; - } - if c.duration_ms <= time_left && c.price_micros <= funds_left { - out.push(Impression { - slot: out.len() as u64, - ad_id: c.ad_id.clone(), - creative_hash: c.creative_hash, - duration_ms: c.duration_ms, - price_micros: c.price_micros, - quartiles_reached: 0, - }); - time_left -= c.duration_ms; - funds_left -= c.price_micros; - } - } - out -} /// A signed, budget-bounded, per-impression ad-break record. #[derive(Clone, Debug, PartialEq)] @@ -164,11 +102,6 @@ pub struct SsaiReceipt { pub sig: [u8; 64], } -/// Σ price over billable impressions — the one definition of spend, used by both -/// `seal` and `verify` so they cannot disagree. -fn billable_spend(impressions: &[Impression]) -> u64 { - impressions.iter().filter(|i| i.is_billable()).map(|i| i.price_micros).sum() -} impl SsaiReceipt { fn signing_payload(&self) -> Vec { diff --git a/wai/wai-verify/src/lib.rs b/wai/wai-verify/src/lib.rs index 7ecf88d87..fa53c1100 100644 --- a/wai/wai-verify/src/lib.rs +++ b/wai/wai-verify/src/lib.rs @@ -29,3 +29,9 @@ pub mod int_entropy; /// 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; -- 2.54.0 (Apple Git-157) From 090d97b415743fa1c74e4d57df1324efa380b67d Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Thu, 10 Sep 2026 12:05:00 -0400 Subject: [PATCH 15/15] fix(wai): declare the `world` dependency video_manifest always had MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The merge with main compiled cleanly and then failed to build — main split the quantum stack into its own `wai-quantum` crate, changing `quantum_ops` from `["world"]` to `["dep:wai-quantum", "wai-quantum/quantum_ops"]`. That surfaced a latent defect in the video capabilities rather than in the restructure: every receipt module calls `crate::world::receipt::merkle_root`, but `video_manifest` only ever declared `quantum_ops` and relied on `world` arriving transitively. It worked by circumstance and broke the moment the transitive path moved. Now declared explicitly. Same shape as the other findings on this branch: something true by accident rather than by construction, invisible until the accident changed. Verified on the merged tree: video capabilities 94 passed / 0 failed, and the Kani suite still 12 harnesses / 5049 checks / 0 failures — the merge did not perturb any proved property. Co-Authored-By: Claude Opus 5 --- wai/wai-rs/Cargo.lock | 2 +- wai/wai-rs/Cargo.toml | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/wai/wai-rs/Cargo.lock b/wai/wai-rs/Cargo.lock index 0b098cdb2..b11837ba0 100644 --- a/wai/wai-rs/Cargo.lock +++ b/wai/wai-rs/Cargo.lock @@ -3898,7 +3898,7 @@ dependencies = [ [[package]] name = "wai-quantum" -version = "0.3.18" +version = "0.3.20" dependencies = [ "blake3", "ed25519-dalek", diff --git a/wai/wai-rs/Cargo.toml b/wai/wai-rs/Cargo.toml index 338a04b93..bd914bc0c 100644 --- a/wai/wai-rs/Cargo.toml +++ b/wai/wai-rs/Cargo.toml @@ -183,7 +183,11 @@ 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. -video_manifest = ["quantum_ops"] +# 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"] -- 2.54.0 (Apple Git-157)