Transaction-Science/open-standards
Watch
1
0
Fork
You've already forked open-standards
 0
Code Issues Pull requests 7 Projects Releases Packages Wiki Activity Actions 1

wai: attested OTT video workflow + machine-checked totality proofs over the rANS core #82

Open
dcharlot wants to merge 18 commits from feat/wai-video-workflow into main
pull from: feat/wai-video-workflow
merge into: Transaction-Science:main
Conversation 0 Commits 18 Files changed 20 +3227 -14
dcharlot commented 2026-09-07 03:45:52 -04:00
Owner
Copy link

Two related strands, 14 commits.

OTT video workflow — five capabilities covering the ingest spec: wai.video.manifest (attested per-session manifest, §1), .ssai (attested ad insertion + per-impression receipt), .keys (attested content-key release, §3), .package (deterministic packaging + attested SegmentMap) and .channel (linear/FAST assembly, program-as-run chain, §5). Plus a browser sink live at /video-ott and energy meters that make the provenance ladder mechanical rather than asserted.

Formal verification — machine-checked proofs over the integer rANS core, which found four real defects in the bypass escape (fixed here, not just documented). Also proves softmax normalisation, matmul + layernorm totality, and that the scale→bucket primitive is total and monotone. A CI job and SPEC §7 keep the totality half checked on every push.

The proofs are recorded honestly: each commit notes where the technique stops and what it does not cover, including a latent inconsistency the softmax work exposed and the SSAI decision policy being separated specifically so it can be checked.

Co-Authored-By: Claude Opus 5 [email protected]

Two related strands, 14 commits. **OTT video workflow** — five capabilities covering the ingest spec: `wai.video.manifest` (attested per-session manifest, §1), `.ssai` (attested ad insertion + per-impression receipt), `.keys` (attested content-key release, §3), `.package` (deterministic packaging + attested SegmentMap) and `.channel` (linear/FAST assembly, program-as-run chain, §5). Plus a browser sink live at `/video-ott` and energy meters that make the provenance ladder mechanical rather than asserted. **Formal verification** — machine-checked proofs over the integer rANS core, which found **four real defects** in the bypass escape (fixed here, not just documented). Also proves softmax normalisation, matmul + layernorm totality, and that the scale→bucket primitive is total and monotone. A CI job and SPEC §7 keep the totality half checked on every push. The proofs are recorded honestly: each commit notes where the technique stops and what it does not cover, including a latent inconsistency the softmax work exposed and the SSAI decision policy being separated specifically so it can be checked. Co-Authored-By: Claude Opus 5 <[email protected]> 
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 <[email protected]>
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 <[email protected]>
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 <[email protected]>
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 <[email protected]>
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) <[email protected]>
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) <[email protected]>
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) <[email protected]>
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) <[email protected]>
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) <[email protected]>
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) <[email protected]>
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) <[email protected]>
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<<PROB_FRAC)/n) equals 1<<PROB_FRAC only when n divides it (n = 3
gives 65_535, not 65_536). The checker marks the branch UNREACHABLE (the argmax
element always has neg = 0, so exps[argmax] = c0 > 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) <[email protected]>
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 <[email protected]>
verify(wai): separate the ssai decision policy so it can be checked — and record what would not close
Some checks failed
standards workspaces build + test / eoc-rs (pull_request) Successful in 2m19s
Details
standards workspaces build + test / aac-rs (pull_request) Successful in 1m3s
Details
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m13s
Details
standards workspaces build + test / joule-code-rs (pull_request) Successful in 57s
Details
standards workspaces build + test / proof-rs (pull_request) Successful in 1m11s
Details
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m2s
Details
standards workspaces build + test / jouleclaw-rs (pull_request) Successful in 3m55s
Details
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 46s
Details
standards workspaces build + test / map-rs (pull_request) Successful in 40s
Details
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 2m32s
Details
wai cross-architecture byte-equality / linux-x86_64 (pull_request) Successful in 14s
Details
standards workspaces build + test / mesh-rs (pull_request) Successful in 34s
Details
WAI conformance / cargo-class corpora · linux (pull_request) Successful in 30s
Details
WAI conformance / cross-arch byte-equality · linux (pull_request) Successful in 14s
Details
standards workspaces build + test / openpay (pull_request) Successful in 2m19s
Details
wai cross-architecture byte-equality / linux-aarch64 (pull_request) Successful in 24s
Details
WAI conformance / cargo-class corpora · linux-arm64 (pull_request) Successful in 58s
Details
WAI conformance / cross-arch byte-equality · linux-arm64 (pull_request) Successful in 23s
Details
wai formal verification (integer core) / kani (pull_request) Successful in 3m28s
Details
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 10m32s
Details
standards workspaces build + test / arl-rs (pull_request) Failing after 38m8s
Details
standards workspaces build + test / jouledesk-rs (pull_request) Has been cancelled
Details
standards workspaces build + test / joulehook-rs (pull_request) Successful in 9m38s
Details
standards workspaces build + test / sense-rs (pull_request) Successful in 9m11s
Details
wai cross-architecture byte-equality / macos-arm64 (reference) (pull_request) Successful in 17s
Details
WAI conformance / cargo-class corpora · macos (pull_request) Successful in 58s
Details
WAI conformance / cross-arch byte-equality · macos (pull_request) Successful in 19s
Details
wai cross-architecture byte-equality / windows-x86_64 (pull_request) Has been cancelled
Details
WAI conformance / cargo-class corpora · windows (pull_request) Has been cancelled
Details
WAI conformance / cross-arch byte-equality · windows (pull_request) Has been cancelled
Details
fa69ab5ec2 
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 <[email protected]>
fix(wai): declare the world dependency video_manifest always had
Some checks failed
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 36s
Details
standards workspaces build + test / map-rs (pull_request) Successful in 33s
Details
standards workspaces build + test / mesh-rs (pull_request) Successful in 29s
Details
jouleclaw public surface must stay documented / Public-surface audit (jouleclaw-rs) (pull_request) Successful in 59s
Details
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 3s
Details
standards workspaces build + test / openpay (pull_request) Successful in 1m20s
Details
wai cross-architecture byte-equality / linux-aarch64 (pull_request) Successful in 21s
Details
WAI conformance / cargo-class corpora · linux-arm64 (pull_request) Successful in 37s
Details
WAI conformance / cross-arch byte-equality · linux-arm64 (pull_request) Successful in 19s
Details
standards workspaces build + test / eoc-rs (pull_request) Successful in 1m47s
Details
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m14s
Details
standards workspaces build + test / proof-rs (pull_request) Successful in 1m12s
Details
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m0s
Details
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 2m34s
Details
wai cross-architecture byte-equality / linux-x86_64 (pull_request) Successful in 14s
Details
WAI conformance / cargo-class corpora · linux (pull_request) Successful in 30s
Details
WAI conformance / cross-arch byte-equality · linux (pull_request) Successful in 14s
Details
WAI conformance / C2PA manifest emission · signed, read back, validated (pull_request) Successful in 40s
Details
wai formal verification (integer core) / kani (pull_request) Successful in 3m52s
Details
standards workspaces build + test / arl-rs (pull_request) Successful in 10m5s
Details
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 10m24s
Details
standards workspaces build + test / jouledesk-rs (pull_request) Successful in 9m55s
Details
standards workspaces build + test / joulehook-rs (pull_request) Successful in 10m8s
Details
standards workspaces build + test / sense-rs (pull_request) Successful in 10m31s
Details
wai cross-architecture byte-equality / macos-arm64 (reference) (pull_request) Successful in 32s
Details
WAI conformance / cargo-class corpora · macos (pull_request) Successful in 1m15s
Details
WAI conformance / cross-arch byte-equality · macos (pull_request) Successful in 19s
Details
wai cross-architecture byte-equality / windows-x86_64 (pull_request) Has been cancelled
Details
WAI conformance / cargo-class corpora · windows (pull_request) Has been cancelled
Details
WAI conformance / cross-arch byte-equality · windows (pull_request) Has been cancelled
Details
090d97b415 
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:🧾: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 <[email protected]>
Merge remote-tracking branch 'origin/main' into feat/wai-video-workflow
Some checks failed
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 38s
Details
standards workspaces build + test / map-rs (pull_request) Successful in 32s
Details
standards workspaces build + test / mesh-rs (pull_request) Successful in 28s
Details
standards workspaces build + test / openpay (pull_request) Successful in 1m38s
Details
wai cross-architecture byte-equality / linux-aarch64 (pull_request) Successful in 21s
Details
WAI conformance / cargo-class corpora · linux-arm64 (pull_request) Successful in 55s
Details
WAI conformance / cross-arch byte-equality · linux-arm64 (pull_request) Successful in 20s
Details
jouleclaw public surface must stay documented / Public-surface audit (jouleclaw-rs) (pull_request) Successful in 1m0s
Details
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 4s
Details
standards workspaces build + test / eoc-rs (pull_request) Successful in 1m53s
Details
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m20s
Details
standards workspaces build + test / proof-rs (pull_request) Successful in 1m15s
Details
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m9s
Details
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 2m43s
Details
wai cross-architecture byte-equality / linux-x86_64 (pull_request) Successful in 17s
Details
WAI conformance / cargo-class corpora · linux (pull_request) Successful in 41s
Details
WAI conformance / cross-arch byte-equality · linux (pull_request) Successful in 16s
Details
WAI conformance / C2PA manifest emission · signed, read back, validated (pull_request) Successful in 1m3s
Details
wai formal verification (integer core) / kani (pull_request) Successful in 4m50s
Details
standards workspaces build + test / arl-rs (pull_request) Successful in 2m22s
Details
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 2m12s
Details
standards workspaces build + test / jouledesk-rs (pull_request) Successful in 2m30s
Details
standards workspaces build + test / joulehook-rs (pull_request) Successful in 2m15s
Details
standards workspaces build + test / sense-rs (pull_request) Successful in 2m7s
Details
wai cross-architecture byte-equality / macos-arm64 (reference) (pull_request) Successful in 13s
Details
WAI conformance / cargo-class corpora · macos (pull_request) Successful in 46s
Details
WAI conformance / cross-arch byte-equality · macos (pull_request) Successful in 15s
Details
wai cross-architecture byte-equality / windows-x86_64 (pull_request) Has been cancelled
Details
WAI conformance / cargo-class corpora · windows (pull_request) Has been cancelled
Details
WAI conformance / cross-arch byte-equality · windows (pull_request) Has been cancelled
Details
2b9de9595f 
# Conflicts:
#	wai/wai-rs/Cargo.lock
Merge remote-tracking branch 'origin/main' into feat/wai-video-workflow
Some checks failed
standards workspaces build + test / jouleclaw-rs (pull_request) Successful in 2m5s
Details
standards workspaces build + test / aac-rs (pull_request) Successful in 38s
Details
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m17s
Details
standards workspaces build + test / joule-code-rs (pull_request) Successful in 39s
Details
standards workspaces build + test / arl-rs (pull_request) Successful in 3m31s
Details
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 35s
Details
standards workspaces build + test / proof-rs (pull_request) Successful in 1m10s
Details
standards workspaces build + test / map-rs (pull_request) Successful in 31s
Details
standards workspaces build + test / mesh-rs (pull_request) Successful in 25s
Details
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m6s
Details
standards workspaces build + test / openpay (pull_request) Successful in 1m31s
Details
wai cross-architecture byte-equality / linux-aarch64 (pull_request) Successful in 21s
Details
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 3m22s
Details
WAI conformance / cargo-class corpora · linux-arm64 (pull_request) Successful in 48s
Details
WAI conformance / cross-arch byte-equality · linux-arm64 (pull_request) Successful in 16s
Details
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 2m34s
Details
wai cross-architecture byte-equality / linux-x86_64 (pull_request) Successful in 14s
Details
WAI conformance / cargo-class corpora · linux (pull_request) Successful in 34s
Details
WAI conformance / cross-arch byte-equality · linux (pull_request) Successful in 14s
Details
standards workspaces build + test / jouledesk-rs (pull_request) Successful in 3m17s
Details
WAI conformance / C2PA manifest emission · signed, read back, validated (pull_request) Successful in 41s
Details
wai formal verification (integer core) / kani (pull_request) Successful in 4m15s
Details
standards workspaces build + test / joulehook-rs (pull_request) Successful in 9m16s
Details
standards workspaces build + test / sense-rs (pull_request) Successful in 5m41s
Details
wai cross-architecture byte-equality / macos-arm64 (reference) (pull_request) Successful in 16s
Details
WAI conformance / cargo-class corpora · macos (pull_request) Successful in 57s
Details
WAI conformance / cross-arch byte-equality · macos (pull_request) Successful in 15s
Details
wai cross-architecture byte-equality / windows-x86_64 (pull_request) Has been cancelled
Details
WAI conformance / cargo-class corpora · windows (pull_request) Has been cancelled
Details
WAI conformance / cross-arch byte-equality · windows (pull_request) Has been cancelled
Details
25a0b2ce70
Some checks failed
no-vanity-metrics / Scan committed Markdown for vanity metrics (pull_request) Successful in 3s
Details
standards workspaces build + test / eoc-rs (pull_request) Successful in 1m50s
Details
standards workspaces build + test / jouleclaw-rs (pull_request) Successful in 2m5s
Details
standards workspaces build + test / aac-rs (pull_request) Successful in 38s
Details
standards workspaces build + test / jcp-rs (pull_request) Successful in 1m17s
Details
standards workspaces build + test / joule-code-rs (pull_request) Successful in 39s
Details
standards workspaces build + test / arl-rs (pull_request) Successful in 3m31s
Details
standards workspaces build + test / joulecontract-rs (pull_request) Successful in 35s
Details
standards workspaces build + test / proof-rs (pull_request) Successful in 1m10s
Details
standards workspaces build + test / map-rs (pull_request) Successful in 31s
Details
standards workspaces build + test / mesh-rs (pull_request) Successful in 25s
Details
standards workspaces build + test / sandbox-rs (pull_request) Successful in 2m6s
Details
standards workspaces build + test / openpay (pull_request) Successful in 1m31s
Details
wai cross-architecture byte-equality / linux-aarch64 (pull_request) Successful in 21s
Details
standards workspaces build + test / joule-ui-rs (pull_request) Successful in 3m22s
Details
WAI conformance / cargo-class corpora · linux-arm64 (pull_request) Successful in 48s
Details
WAI conformance / cross-arch byte-equality · linux-arm64 (pull_request) Successful in 16s
Details
standards workspaces build + test / smart-byte-rs (pull_request) Successful in 2m34s
Details
wai cross-architecture byte-equality / linux-x86_64 (pull_request) Successful in 14s
Details
WAI conformance / cargo-class corpora · linux (pull_request) Successful in 34s
Details
WAI conformance / cross-arch byte-equality · linux (pull_request) Successful in 14s
Details
standards workspaces build + test / jouledesk-rs (pull_request) Successful in 3m17s
Details
WAI conformance / C2PA manifest emission · signed, read back, validated (pull_request) Successful in 41s
Details
wai formal verification (integer core) / kani (pull_request) Successful in 4m15s
Details
standards workspaces build + test / joulehook-rs (pull_request) Successful in 9m16s
Details
standards workspaces build + test / sense-rs (pull_request) Successful in 5m41s
Details
wai cross-architecture byte-equality / macos-arm64 (reference) (pull_request) Successful in 16s
Details
WAI conformance / cargo-class corpora · macos (pull_request) Successful in 57s
Details
WAI conformance / cross-arch byte-equality · macos (pull_request) Successful in 15s
Details
wai cross-architecture byte-equality / windows-x86_64 (pull_request) Has been cancelled
Details
WAI conformance / cargo-class corpora · windows (pull_request) Has been cancelled
Details
WAI conformance / cross-arch byte-equality · windows (pull_request) Has been cancelled
Details
This pull request can be merged automatically.
This branch is out-of-date with the base branch
You are not authorized to merge this pull request.
View command line instructions

Checkout

From your project repository, check out a new branch and test the changes.
git fetch -u origin feat/wai-video-workflow:feat/wai-video-workflow
git switch feat/wai-video-workflow

Merge

Merge the changes and update on Forgejo.

Warning: The "Autodetect manual merge" setting is not enabled for this repository, you will have to mark this pull request as manually merged afterwards.

git switch main
git merge --no-ff feat/wai-video-workflow
git switch feat/wai-video-workflow
git rebase main
git switch main
git merge --ff-only feat/wai-video-workflow
git switch feat/wai-video-workflow
git rebase main
git switch main
git merge --no-ff feat/wai-video-workflow
git switch main
git merge --squash feat/wai-video-workflow
git switch main
git merge --ff-only feat/wai-video-workflow
git switch main
git merge feat/wai-video-workflow
git push origin main
Sign in to join this conversation.
Reviewers
No reviewers
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
Transaction-Science/open-standards!82
No description provided.