wai: D2c M8 — WIV1 and WIR1 through wai-ops/1's stage operators, goldens unchanged #308
Loading…
Reference in a new issue
No description provided.
Delete branch "wai/d2c-m8"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
D2c M8:
WIV1(wai.video.int_motion, and the P-frames ofwai.video.int_hyper) andWIR1(wai.{image,video,audio,splat}.int_refine) decode through the integer operator setwai-ops/1, by its stage operators alone (integer-operators §13.5). No arithmetic changes, and every committed golden is unchanged.Stacked on #298 (M7a): this branch starts from
wai/d2c-m7aat3bc90f02, and its diff against main includes #298's commits until #298 merges. #298's newer heads are merged in, with no conflict:a1e007b9(origin/main with #296; CHANGELOG both sides) as88e4735f, and the pusheda6cd06d7(origin/main atea84f7e2) asf01eb197, which changes no file underwai/,.github/orscripts/.What changes
WIV1: one E1rans64_decode(t4097,lenient,canonical) over the clip's stream; the prediction 128 for frame 0 under keyframe 0, otherwise E10mc_predicton the previous decoded frame; E9residual_stepon[0, 255].WIR1: per unit, one E1 decode of its stream; the prediction from the element below (identity), E11up2_predictor E12rate_predict; E9 on[0, 255]or[−32768, 32767].wai-ops. E1 decodes a symbol against a table in whatever width a payload's parser keeps it (Rans::symbol_in;table_okreads its entries likewise). E10, E11 and E12 gain per-element forms (mc_predict_at,up2_at,rate_at) that read a frame, a picture or source samples in the driver's own layout, so a decode forms no copy:int_payload_cost's bound (a keyframe-0 clip holds its declared working bytes to within 4096) holds unchanged.mc_predict,up2_predictandrate_predictare those forms over aTensor; their vectors are unchanged.int_video::opsandstaged::wir1::ops, each with its stage form (stages: the operands each operator takes), its decode, andWIR1's stream check. A.4 step 1 (a unit's geometry) is shared with the direct decode.int_video::{decode_typed, decode_pframes_typed},staged::wir1::apply_unitandWir1::check_streamsdecode through the drivers, so the integer-payload decode, the staged sink, the video receipts and the browser crate do. The direct decodes areint_video::legacyandstaged::wir1::legacy, test-only (legacy_int).wai-ops' E9 32-bit form (stage::residual_step_i32,i32_form_fits, andresidual_step_by_i32fori64operands) is behind the newi32_formsfeature, and compiled for its own tests and for K29 under the model checker.wai-rs'i32_formsdecodes both payloads through it (int_video::ops::{decode_typed_i32, decode_pframes_typed_i32},staged::wir1::ops::apply_unit_i32). byte-exact-conformance turns it on by default, so the matrix holds the 32-bit form to the pinned digests on every leg.wir1_arith's saturating step) runs only in the test-only decode.int_video::predictis E10 on an RGB8 frame, which the encoder predicts with; theWIR1encoder predicts with the decode's E11 or E12 (ops::prediction) and steps with E9; the staged-measurement and staged-corpus tools callops::{up2_prediction, rate_prediction}.staged::predict'sup2_at,rate_at,rate_indexandrdiv, andwir1_arith, are test-only (andcfg(kani));rate_len, the rate predictor's geometry, stays. The predictors' proofs move to the operators a decode runs:e11_up2_between_its_neighbours,e12_rdiv_matches_its_definitionande12_rate_at_reads_only_source_samples, in the stage shard.wai.video.int_motionand the fourint_refinecapabilities register anopsmember with no graph,{ "set": "wai-ops/1", "stage": { "rans64": { t4097, lenient, canonical } } }: with no parameter set there is no profile, subset or lowering.OpsMember's three are optional, and the schema requiresset, the three together, and a lowering or a stage.registry/capabilities.jsonand its schema regenerated.WIV1andWIR1drivers and their widths; the status note names the stage-only capabilities; §15.3 item 5 (none). integer-payloads §3 and §12 and staged-delivery A.4 cite the stage operators. SPEC §5 (theint_motionandint_hyperrows, the refinement table), §7 (StandardDefined) and §8 (no planned break). CHANGELOG.tests/int_video_ops.rsandtests/wir1_ops.rsin both fast-kernel steps ofwai-conformance.yml, which carryi32_forms(appended, sogate.sh's grep still finds the steps); the differential's two new halves run there for a fixed count and nightly inwai-ops-differential.yml, whose features gainvideo_int,staged; the moved harnesses inwai-formal-verification.yml's stage shard.Planned breaks
None. integer-operators §15.3 item 5 and SPEC §8 say so: the decodes through the stage operators give the output and the refusal of the decoders they replaced, on every input. The differential's oracle is equality, with no exemption.
Gates, each red once and restored
19c4f407,a0db84b9,582a643ct4097length bound widened to 4098int_video_opsandwir1_ops,e1s_table_rule_is_the_payloads: "4098 entries: the decode's checks and E1 disagree";wai-verify vectors verify,stage/rans64_decode.jsonlline 433. (A first run left theWIV1case green: its 4098-entry table was not strictly increasing, so it broke two rules; fixed in582a643cand run red again.)840b7961,ac203e85,768e8798+1int_video_ops: video_real differs (the whole-pel clips, the 65 staged bases and video_nk alike); byte-exactwiv1_through_the_stage_operators_is_golden, video_real frame 2; the file-based goldens stay green (pre-switch);stage/mc_predict.jsonlline 17rdivrounding halves toward zerowir1_ops:audio_flac_rate_ladderL1 unit 0 (−272 against −273); byte-exactstaged_sets_through_the_stage_operators_are_byte_exact, the audio set;stage/rate_predict.jsonlline 1opsmembersee2fc134,c00b656c,f0c2b4b9canonicalend accepts an unread wordint_video_ops: "wiv1_unread_word: through the stage operators None, directly Some(…does not end canonically…)";wir1_ops:stream_noncanonical/L1.waichecked Ok;stage/rans64_decode.jsonlline 45c84ca0ec,11af3852w / block(only a grid with a partial last column reaches it; every committed clip's sides are multiples of its block)int_video_random_clips_decode_alike, "the two decodes differ", seed 3372 (h 5, w 3, block 4)44686569Rone short ((hi − lo)/q)residual_identity_holds;wir1_ops32-bit test (image_up2_from_int_hyperL1, element 2966: 254 against 255); byte-exactstaged_sets_through_the_32bit_form_are_byte_exact; both differential halves. The exact paths stay green, and so do theWIV132-bit golden and test: no committed clip has a residual past⌊255/q⌋9a377f9bwiv1_keyframe_0_payloads_are_byte_identical,int_video_real_footage_exercises_the_half_pel_predictor,staged_audio_rate_ladder_is_byte_exact; wai-rsint_video_halfpel;wai_int_payload_vectors verify(FAIL video_real) andwai_staged_vectors verify(the generator's encoder checks its reconstruction against the decode).staged_verify.pyandint_payload_verify.py, which share no code with the decoder, stay greenint_payload_cost: "int_video: the decode held 42524 bytes, over the declared 35612"f2513980,ca6c0544legacy::predictwithout its+1,wir1_arith::stepwithout its clamp)int_video_ops,wir1_ops(attested_across_drop L1, element 24: 255 through the operator set, 7 directly; the refusal sweep), both differential halvesEvery fault was restored with git, and the gate's tests run green again on the committed tree.
Goldens, unchanged
Every golden M8's row names, byte for byte:
int_video_golden: the synthetic clip (clip FNV27573cdba1ad6628, SHA-2565afd6477…) and the half-pel real footage (1ec1f0fa7da0d70f,e6724ca2…), every frame; through the stage operators, through the 32-bit form, and as the sink decodes (byte-exact on the matrix's legs;int_video,int_video_halfpel,int_video_keyframein wai-rs).WIV1payloads of int-payload-conformance (int_video, video_real, video_nk4a81f0c9…) and every refusal fixture's code (wai_int_payload_vectors verify,tests/int_payload.rs,int_payload_verify.py).staged-conformance(wai_staged_vectors verify, which regenerates every file and compares byte for byte),staged_verify.py, the wasm32 sink (69 of 69 cases, 146 unit stage hashes equal the native ones), and byte-exact's pinned stage digests of the video, image and audio sets, through the stage operators and the 32-bit form.ops-conformance/stage/), unchanged and reproduced by both certifiers.Results
All on the build host, on the merged head
88e4735f;f01eb197has the samewai/,.github/andscripts/trees.gate.sh d2c-m8-merged: GREEN. The build, the lib tests, carriage, the corpus loop (21 of 21), the fast kernels, byte-exact, wai-web wasm32 and the neural gates. Also GREEN on the switched tree (d2c-m8-g6) and after gate 7 (d2c-m8-g7).i32_forms): 37 test binaries, 0 failures,int_payload_costat the 2^30-byte clip among them;wai registry export --check;cargo test --locked, debug and release;wai-verify vectors verify(every file verifies);tools/wai_ops_check.py ops-conformance(every vector file, lowered graph and certificate rewritten byte for byte);staged_verify.py(69 cases, 0 failures) andint_payload_verify.py;legacy_int,splat_int,audio_int,world_int,video_int,staged);verify_int_payload_wasm(int_video5afd6477…, video_reale6724ca2…, video_nk4a81f0c9…) andverify_staged_wasm(69 of 69 cases, 146 unit stage hashes equal the native ones);check-lockfiles.shwith 1.98.0 (38 lockfiles current),check-public-names.shwith the host's list,pr-touches-paths-selftest.sh;include/wai.his as committed.q40,mv_precision36, the vector count 26, a short stream 13, an I-frame a byte short 12); layers: units applied alike 5743,geometry_mismatch188,stream_exhausted15,stream_noncanonical15, refused at parse 6, no layer drawn 21.i32_forms(the fast-kernel steps), every case also through the 32-bit form, alike.WIV1payloads and 132WIR1layers (237 units) through the stage operators as directly; 4 committed decode fixtures, 21 per-rule fixtures and 682 changed streams ofWIV1, and 25 geometry fixtures and 765 changed streams ofWIR1, refused alike; 618 clips and 501 units through the 32-bit form as through the exact form.int_payload_costholds unchanged: a keyframe-0 clip holds its declared working bytes to within 4096, andstaged_resourcesandint_video_enc_memorypass.Kani
The moved harnesses, and those the change touches, under memguard at 48 GB and a 45-minute budget: 8 of 8 verified, 0 failures.
e12_rate_at_reads_only_source_samples7.4 s,e12_rdiv_matches_its_definition13.7 s,e11_up2_between_its_neighbours2.8 s (new in wai-ops, in the stage shard);k29_residual_step_32bit_identity_registered_ranges137.9 s (its functions are now behindi32_forms, and compiled undercfg(kani));staged_predict::{rate_index_in_bounds, rdiv_matches_spec, up2_bounded}andstaged_wir1_arith::step_in_range64.8 s, which still compile under their newcfg.k29_residual_step_32bit_identity_every_range(the stage-long shard) was not rerun: its code is unchanged, only gated. No harness is leftkani_openby this PR.Decisions
WIV1payloads, 132WIR1layers), and that E1'st4097rule is each payload's table rule, edit for edit. The operators' own vectors areops-conformance/stage/, which both certifiers reproduce byte for byte.opsmember of a stage-only capability names no profile. A profile is what a parameter set's certificate meets; these capabilities have no set. Their widths are §7.4's per operator (E1 a 64-bit state, E12 64-bit arithmetic, E9i32by its identity), which §13.5 now states.int_video::checkandWIR1's parser keep their table checks, codes and order; gate 1 shows E1's rule admits exactly the tables they admit.staged_predict::,staged_wir1_arith::in the integer-core shard): they prove the reference the differential holds the operator set to.Left for D3b, and for M7b/O8
i32_formsfeature: E9's 32-bit form for the integer GPU legs, with its parity tests and byte-equality goldens. E10 and E11 fiti32as they are; E1 needs a 64-bit state and E12 64-bit arithmetic on any fabric (§7.4), so a GPU leg for these payloads emulates both or leaves them to the CPU.Notes
rb, under memguard; logs are under$RB_ROOT/logs/d2c-m8/andlogs/land/d2c-m8-*.cargo fmt, nogit stash, no cargo output piped intoheadortail. No history rewritten; WIP-labelled commits were committed before their runs, and each gate's results are in its later commits' messages.🤖 Generated with Claude Code
The compile fix of the gate's WIP commit (a payload helper with two borrowed inputs needs its lifetime named), and gate 2's results. Results (build host, release; pinned jpegai/v1 inputs fetched and checked against tools/jpegai-e2e-v1.sha256; the reference-decoder stage fixtures rebuilt from the local assets' dumps and checked by the unchanged tests first): - tests/jpegai_ops.rs 4 passed, no skip: both planes' z, v, mask, likely, rvs, σ_idx and y_q through the lowering equal the direct computation's; the whole decode through the operator set equals the direct decode at all 7 stages and matches WAI_JPEGAI_EXPECT_SHA256. - jpegai_hyperscale_calibration, luma and chroma: the scale graph (acc32) vs the reference I_s, 40960/40960 and 24576/24576 exact, max|Δ| = 0. - jpegai_mans_golden 12 passed: E8's tables (4 golden, 32 normative), the reference encoder's sgm and fac streams, codestream → E8, the 258-call replay, the scale graph on both planes, the sigma chain through the stage operators. - byte-exact jpegai_golden 3 passed (E8 on the reference stream). - jpegai_e2e_frontend and jpegai_e2e_chroma: y_q through the operator set 40960/40960 and 24576/24576 exact; every later stage as before (U,V 3.377%, Y 1.398% at 1 LSB). - The file-based goldens (jpegai_e2e_full, jpegai_reconstruction_binding, jpegai_cross_platform's 9 hashes) unchanged; wai-ops 35 + 7 + 3 + 4 + 2 + 1 + 1 tests. Falsified (Part 3.5): - Chroma's fac decode skips the 160 luma rows' reads (a fresh decoder over only its own 96 rows). Red: jpegai_ops 2 of 4 (the planes test, Refusal { StreamExhausted, Symbol(711) }; the whole decode, Ops(StreamExhausted)), jpegai_e2e_chroma (the same refusal). The file-based goldens stay green: the switch is gate 6. Restored: green. - B_y read as signed in E8. Every M7a golden stays green: no reference stream decodes an escape at a distribution whose bound is 128 or more, so the prediction that jpegai_mans_golden carries this row is corrected. Red: wai-verify vectors verify, stage/mans_decode.jsonl line 12 (a vector with a bound of 128). Restored: green. Co-Authored-By: Claude Opus 5.5 <[email protected]>jpegai_decode::{decode, decode_with_stages} decode through the integer operator set and return Result<Rgb, Refusal>; load and decode_loaded run a scale path loaded once. The direct decode is jpegai_decode::legacy and jpegai_ops::legacy, test-only (legacy_int). The neural sink's exact path lowers and loads the scale path from the members' bytes through the store of loaded sets (int_set_cache, keyed by the listing of norm.json and weights/hs_{y,uv}.json); a refusal of the exact decode (model_mismatch, stream_exhausted, or set_incomplete for a member the set lacks) is the decode's result and does not fall back to the float decode (O9). Only an absent bundle, or a target or floating-point environment the float stages cannot run in, takes the float decode. The float decode path (neural::jpegai) runs its scale path and entropy decodes through the same driver (jpegai_ops::plane, O10), from its own bundle's members; one whose hyper-latent offsets are not 31, or that fails a load check, is refused. The browser crate's decodeJpegAiMans decodes through E8 (jpegai_ops::latent_span) and throws on a refusal; decodeJpegAiFull reports the decode's refusal. Co-Authored-By: Claude Opus 5.5 <[email protected]>Results (build host, release, pinned inputs, no skip): tests/jpegai_ops.rs 9 passed; the CI trio (jpegai_e2e_full, jpegai_reconstruction_binding, jpegai_cross_platform: all 9 hashes and WAI_JPEGAI_EXPECT_SHA256); jpegai_e2e_frontend and jpegai_e2e_chroma; jpegai_hyperscale_calibration on both planes (max|Δ| = 0); jpegai_mans_golden 12 passed on E8 alone; the neural dispatch 3; the float path (jpegai_e2e, jpegai_live 5/196608 at 1 LSB, jpegai_scope_ort); byte-exact jpegai_golden 2; wai-ops' bundle tests 2; jpegai_memory (front half luma 2,114,160 against 2,218,884, chroma 1,290,864 against 1,357,586); the differential, 1,500 cases, no disagreement. Each build's cargo check (neural_int; neural_int,legacy_int,provenance; neural; the differential's features; the default features with neural; wai-web; the byte-equality crate) adds no warning. Falsified: the test-only direct mANS port refills its window to 48 bits instead of 56. Production green (the CI trio, byte-exact's E8 golden); the comparisons red: jpegai_ops 4 of 9 (the planes, the whole decode, both stream-parity tests), byte-exact's direct-port golden, the differential ("Luma: the two decodes differ", seed 10208061212434326836). Restored: green. Co-Authored-By: Claude Opus 5.5 <[email protected]>- wai-ops: E1's symbol decode takes its table in any width (Rans::symbol_in; symbol is it over a Table); E10, E11 and E12 gain their per-element forms, mc_predict_at, up2_at and rate_at, which read a frame, a picture or the source samples in whatever layout the driver holds them, so a decode forms no copy. mc_predict, up2_predict and rate_predict are them over a Tensor. - int_video::ops::{decode_typed, decode_pframes_typed}: one E1 decode of the residual stream (t4097, lenient, canonical), GREY or E10 for the prediction, E9 on [0, 255]. The direct decode moves, unchanged, into int_video::legacy; decode_typed and decode_pframes_typed still call it (the switch is gate 6). - staged::wir1::ops::{apply_unit, check_streams}: E1 per unit, identity, E11 or E12 for the prediction, E9 on the kind's range. The direct decode moves, unchanged, into wir1::legacy; A.4 step 1 (the unit's geometry) is shared. - Goldens: tests/int_video_ops.rs, every committed WIV1 payload (the staged bases among them) through the stage operators as directly, and the three vectors and the keyframe-0 JSON forms to every committed digest; tests/wir1_ops.rs, every committed WIR1 layer's every unit as directly, and each layer's stream check; byte-exact-conformance, wiv1_through_the_stage_operators_is_golden and staged_sets_through_the_stage_operators_are_byte_exact, with the pinned constants. Co-Authored-By: Claude Opus 5.5 <[email protected]>- Refusal parity. tests/int_video_ops.rs: every committed WIV1 fixture the decode refuses (int-payload-conformance), refused alike by both decodes with its code and by the sink; one fixture per refusal of the decode in its order; the stream cut at every word, and bytes changed across it. tests/wir1_ops.rs: every committed layer's streams checked alike (the corpus's stream_exhausted and stream_noncanonical cases with their codes); A.4 step 1 broken once per rule for each predictor; a coded layer of each kind and predictor cut at every word, a word appended, every byte changed. - Registry: wai.video.int_motion and the four int_refine capabilities carry an ops member with no graph, { wai-ops/1, stage: rans64 t4097 lenient canonical }. OpsMember's profile, subset and lowering are optional; the schema requires set, the three together, and a lowering or a stage. - Text: integer-operators §11 (a member with no graph), SPEC §5 (the int_motion and int_hyper rows, the refinement table) and §7 (StandardDefined), CHANGELOG. Co-Authored-By: Claude Opus 5.5 <[email protected]>A stage-only decode has no fast kernel behind an interpreter. What a faster fabric runs instead is E9's 32-bit form (§5E E9, Width): the form D3b's integer GPU legs take. Gate 5 holds it to the exact form. - wai-ops: residual_step_i32 and i32_form_fits behind the new i32_forms feature (and cfg(test), cfg(kani), so the unit tests and K29 keep them); residual_step_by_i32, E9 through its 32-bit form for a driver whose operands are i64. wai-verify declares the feature name its included sources test. - wai-rs i32_forms: int_video::ops::{decode_typed_i32, decode_pframes_typed_i32} and staged::wir1::ops::apply_unit_i32, the drivers with E9 as a parameter. - Parity: every committed clip and layer through the 32-bit form as through the exact form (tests/int_video_ops.rs, tests/wir1_ops.rs), changed streams too; the differential compares the 32-bit form on every random case; byte-exact-conformance (i32_forms on by default) decodes WIV1 and the staged sets through it to the pinned digests on every leg. - CI: the fast-kernel steps carry i32_forms, appended so gate.sh's grep still finds them. Gate 4's falsification, for the record: ops::frame's block grid taken as w / block, which only a grid with a partial last column reaches (every committed clip's sides are multiples of its block). Gates 1 to 3 stayed green (int_video_ops 5, wir1_ops 5); int_video_random_clips_decode_alike failed at seed 3372 (h 5, w 3, block 4). Timed 300 s, seed 20261017: debug 2,402,935 clips and 408,439 layers, release 11,948,953 and 3,322,036, alike. Co-Authored-By: Claude Opus 5.5 <[email protected]>- int_video::{decode_typed, decode_pframes_typed} decode through int_video::ops (E1, E10, E9); staged::wir1::apply_unit and Wir1::check_streams through staged::wir1::ops (E1, E11 or E12, E9). The int_payload decode, the staged sink, the receipts and the browser crate reach them through these. The direct decodes, int_video::legacy and staged::wir1::legacy, are test-only (legacy_int). - integer-operators: §5E writes E10, E11 and E12 out; §13.5 the WIV1 and WIR1 drivers (no graph, the step and the predictions, and their widths); the status note names the stage-only capabilities; §15.3 item 5: none. - integer-payloads §3 and §12 and staged-delivery A.4 cite the stage operators; SPEC §8: no planned break; CHANGELOG. Co-Authored-By: Claude Opus 5.5 <[email protected]>The arithmetic guards of the direct decodes (their own predictors, and the saturating step of wir1_arith) no longer run outside the test-only decode; the stage operators carry them now. - int_video::predict is E10 on an RGB8 frame (the encoder predicts with it, as the decode does); the direct predictor, verbatim, is int_video::legacy::predict, test-only. - staged::wir1: the direct decode's pred_at and step are legacy's. The encoder predicts with the decode's E11, E12 or the element below (ops::prediction) and steps with E9; it refuses a stage below of the wrong shape or element type up front. ops::{up2_prediction, rate_prediction} are E11 and E12 on the interleaved layouts, which the staged-measurement and staged-corpus tools now call. - staged::predict's up2_at, rate_at, rate_index and rdiv, and the wir1_arith module, are test-only (legacy_int; and cfg(kani), for the harnesses that still prove them); rate_len, the rate predictor's geometry, stays. wai-verify declares legacy_int. - The predictors' proofs move to the operators a decode runs: wai-ops' e11_up2_between_its_neighbours, e12_rdiv_matches_its_definition and e12_rate_at_reads_only_source_samples, in the stage shard. Gate 6's results, for the record (the switch at9a377f9b): gate.sh GREEN; the release fast-kernel step; staged_verify.py and int_payload_verify.py; wai-web native 32 and wasm32, verify_int_payload_wasm and verify_staged_wasm (69 of 69 cases, 146 unit stage hashes equal the native ones); include/wai.h unchanged. Falsified with the switch live: E10's half-pel rounding without its +1 and E12's rdiv halves toward zero turn the file-based goldens red (byte-exact wiv1_keyframe_0_payloads_are_byte_identical, video_real frame 2; int_video_real_footage_exercises_the_half_pel_predictor; staged_audio_rate_ladder_is_byte_exact; wai-rs int_video_halfpel), and the corpora (wai_int_payload_vectors verify, FAIL video_real; wai_staged_vectors verify, the encoder's reconstruction differs from the decode); the Python verifiers stay green. The decode cloning the previous frame for E10 turns int_payload_cost red: int_video held 42524 bytes against 35612 declared. Co-Authored-By: Claude Opus 5.5 <[email protected]>