wai: D2c O8 + M7b — JPEG AI's networks written in jpegai-int/1 and run through wai-ops/1, goldens unchanged #315
Loading…
Reference in a new issue
No description provided.
Delete branch "wai/d2c-m7b"
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 O8 and M7b:
wai.image.jpegai's hyper decoders, context stages and synthesis are now written out asWHG1graphs in integer-operators §13.6.2. That section is now normative, and the decoder runs these networks throughwai-ops/1. Every committed and pinned golden is unchanged: theSynthesisstage hash and the RGB SHA-256 among them.The branch was built on #308 (M8, which carried #298, M7a). Both have landed, and
origin/mainis merged in (938582b3). Main's other changes since are outsidewai/, so the diff against main is this work alone.O8: what the text now says
(a) The graphs.
jpegai-int/1writes six graphs, in §13.0's role order:hs_y,hs_uv,rec_y,rec_uv,syn_y,syn_uv. The two scale graphs (§13.6.1) are unchanged. The four new ones (§13.6.2) are written in §13.0's canonical numbering, from the bundle's eight weight files:rec_y/rec_uv: a plane's hyper decoder ψ (thez·2^16lift,conv1, the 4×4 transposedconv2, ReLU6,conv3, ReLU6,conv4to4C).subpos_splitof the residual in the order(0,0), (1,1), (0,1), (1,0); per stage,split(ψ), the context (conv.0,conv.1in groups of 5,concat) and the three fusion convolutions; thenaddandsubpos_merge.z [C,4,4]and the dequantised residual[C,16,16]. Output:ŷ.syn_y/syn_uv: the synthesis, built from blocks the text defines:C(conv),T(transposed conv),R(residual block),G(gatex·(f(x)+1)),CABandTAB(layer norm, the three attention convolutions,l2norm,gram, the per-head temperature,softmax,apply, then the feed-forward half witheluand its product),pixel_shuffle, andD(denormalisation,clamp [0, 255·2^16]);conv:dims, awof prod(dims) integers that fit i64,mult, andshiftin0..=127;q16:v;model_mismatch). So is the certificate meetingacc64.(b) The floating-point→Q16 boundary. Every input except the hyper-latent is checked within i32 (
A32 = check [−2^31, 2^31 − 1]). So is the output of every operator that can grow a value: convolution, transposed convolution,add, Q16mul,layernorm_c,gram,apply, and the scalerescales. With those checks, every sum is bounded by the weights alone. The new refusals (field_range), each named in §13.6.2 and in §15.3 item 4:rec_*;syn_*;The direct decoder computed on in each of these cases: in i64, or i128 for the transposed convolutions, and it wrapped or panicked past them. On the test codestream every input stays within 21 bits and every activation within 24, so no committed decode reaches a check.
Why one uniform range rather than per-tensor admissible ranges (§8.4): an admissible range depends on the other inputs of its consumers. In a residual block,
add(x, conv(conv(x))), and in a gate,mul(x, f(x) + 1), the other input is a function of the tensor being ranged, so the ranges would have to be found jointly. The gate's product also binds any uniform range at2^31.5(mul.pisacc-class). Checking every growable activation within i32 leaves every sum certifiable from the weights, at 42 to 60 bits onjpegai/v1.(c) The accumulator class, measured.
tests/jpegai_nets_ops.rsruns the four graphs on the test codestream through the interpreter, withwai_ops::bounds::Withinholding every value to its certified interval (about 19.5 billion values, none outside). The largest magnitudes, in bits (certified bits in brackets):conv.accconvT.accmul.pgram.accapply.accrec_yrec_uvsyn_ysyn_uvThe largest real sum is 106,184,428,047 (37 bits,
syn_uv). No real or certified sum reaches 2^63, so the class isacc64, and O8'sacc128fallback is not needed. Theproductintermediates reach 53 bits (rq.p), whichacc64holds in 128 bits.§1's claim widens: an implementation of the text reproduces the integers of
wai.image.jpegai's integer stages, the networks' outputs for their inputs among them.The verdict and the profiles
The
jpegai/v1certificate (3e243dc1…, committed by digest) now holds six graphs. Its verdict isacc64, and itsacc32_first_failureisrec_ynode 1 (conv.acc, 42 bits). The scale graphs still meetacc32on every node. So that the set can meetacc64while its scale path keepsacc32(M7a's decision, for D3b), §11 gainsrole_profiles.{ wai-ops/1, acc64, full, jpegai-int/1, role_profiles: { hs_y: acc32, hs_uv: acc32 } }. Its schema is regenerated, androle_profilesrequiresprofile.--role-profile ROLE=PROFILE, and the external-set check readsexternal.json'srole_profiles.wai-jpegai-e2e.ymlcertifies with--profile acc64 --role-profile hs_y=acc32 --role-profile hs_uv=acc32.The independent checker
tools/wai_ops_check.pygained §13.6.2's lowering. A separate session wrote it from §13.6.2's text alone, without reading the Rust. It reproduces every lowered graph and certificate byte for byte:ops-conformance: 19 sets, 34 graphs, 19 certificates;jpegai/v1, throughcertify --checkand--external jpegai/v1=DIR.Its readings made two member rules explicit in the text, and both implementations now refuse what the text refuses: a duplicate name at any depth, and a
wthat does not hold prod(dims) values each fitting i64. Its other choices (the operator order within the steps, operand order, and thataddandmulneed equal channel counts) matched the committed bytes.Gates, each red once and restored
96f5468e(on08b5ac25,f44a37ab)prep_data.conv1'sthe_committed_bundle_lowers_to_its_committed_networks: "the lowering of the bytes differs from the committed syn_y.whg1";wai-verify vectors verify, 5 failures. The pinned certificate stays identical (everyjpegai/v1shift is 31) and the Python checker stays green (it is independent)6bed5fa4i mod 4, not by headthe_networks_decode_through_the_lowering_as_directly: "Y through syn_y differs from the direct synthesis";the_whole_decode_through_the_networks_is_the_pinned_decode(the stages). The committed synthetic set, with one channel per head, and the pre-switch file goldens stay greenopsmemberb9663685A32's upper end one past (2^31)a_value_past_its_range_is_refused_field_range: "rec_y: input 1 holding 2147483648", refused atOp(13), notInput(1)f97757a3jpegai_nets_opstest green (8 of 8, pinned bundle);jpegai_random_networks_reconstruct_alike: "the parsed networks lower as their bytes", seed 3372 (chroma)c26b3ce0,cbc4caf7every_kernel_policy_runs_the_networks_alike("rec_y Policy { path: Fast, threads: 1 }: the outputs differ from the interpreter alone") and the golden equality. The first run left the unit test green: every committed vector of the four graphs refused pastA32.cbc4caf7keeps the synthetic networks' magnitudes, so every rec/syn vector now decodes, and requires a completed decode per graph; run again, the unit test is red with the same messagef4de2c78half_upjpegai_cross_platform"differs from the pinned decode, first atlatent_y", every stage fromlatent_yon (synthesis aaba532d…,rgb 1b351a7b…, against the pinnedd5669572…anddbc494a5…)jpegai_memory: "the decode through the operator set held 653409531 bytes; the direct decode held 175465380"2d64a57djpegai_cross_platform,jpegai_e2e_full,jpegai_reconstruction_binding, and the lowering, refusal and policy tests); the comparisons red:the_networks_decode_through_the_lowering_as_directly, the whole decode against the direct one,jpegai_random_synthesis_networks_decode_alike(seed 15111065706836451375)Each fault was applied in the worktree only, run on the build host, and restored with git. The gate's tests then ran green on the committed tree.
Goldens, unchanged
tests/jpegai_cross_platform.rs: all nine pinned hashes, after the switch. That includes theSynthesisstaged56695726bb6ebed403199f60a79a5698734eef1e5ca2813859d490c0882d2a4andrgbdbc494a5a670914edf55c07c48afc0dd348cd05d3a82fff293bf384b2bb69ea3, withlatent_yandlatent_uv(whichrec_*produce) and every post-filter stage.wai-jpegai-e2e.ymlpins:jpegai_reconstruction_binding"matches the pinned WAI_JPEGAI_EXPECT_SHA256";jpegai_e2e_fullmax|Δ| = 1 on 4.446% of samples, as before.rec_y(40,960 values) andrec_uv(24,576), and Y (65,536) and U, V (131,072) throughsyn_yandsyn_uv, equal the direct networks' values, bit for bit as the floats the decode reports.jpegai_ops9 of 9, after the switch.What changes in the code
wai-ops:lower::jpegai_nets:parse_ptq,parse_nets,rec,syn_y,syn_uv,nets,nets_loaded;lower::jpegaiwrites the six roles,lower::jpegai_scalethe scale path alone, andJpegaiBytesnames the members;Builder::ops(an operator with several outputs);1bc0daae…), with graph vectors for the multi-input graphs.wai-rs:jpegai_ops::Networks(load_networks,load_networks_bytes,reconstruct,synthesize_y,synthesize_uv); the store keeps it asResident;jpegai_decodedecodes every integer stage through the operator set;decode_loaded(data, icci, norm, scale path, networks, observe);Result<_, BadMember>;IntNetkeeps only well-formed tensors;acc64. It parses only the eICCI net besides, and reportsmodel_mismatchorfield_rangewithout falling back.a_refused_exact_decode_does_not_fall_backgains a non-integer network weight and a mistyped eICCI field;decodeJpegAiFullreports a mistyped member.jpegai_memory, on the test codestream): the decode through the operator set holds at most 72,752,387 bytes at once, where the direct decode held 175,465,380. Lowering and loading the networks peaks at 89,727,913 bytes; the loaded networks hold 55,530,900.legacy_int):int_transformer,jpegai_synthesis' networks,jpegai_pipeline::reconstruct_yhat(_uv), andint_kernels'par_map,par_zip,conv_acc_i64. The tests that run them requirelegacy_int.wai_decode_bench's JPEG-AI cases now run the graphs the decode runs.tests/jpegai_nets_ops.rsruns in both fast-kernel steps ofwai-conformance.yml, where its pinned cases skip;wai-jpegai-e2e.ymlthat requires 8 tests by name with no skip banner. The job's timeout goes to 60 minutes, because the measured-maxima test takes about 5 minutes on the build host;scripts/check-tests-in-ci.pyis clean. Gate 7 made seven direct-network tests requirelegacy_intinCargo.toml, ande6453a95gates their files the same way, as the check requires.Planned breaks (integer-operators §15.3 item 4, SPEC §8)
On the exact decoder:
acc64:model_mismatch, where the loaders panicked or the decoder computed with what the files held;field_range, where it computed on.No committed bundle or codestream reaches either.
The refusal order: the codestream's scope, then the bundle (its scale path, then its networks), then the streams, then the networks' ranges as each runs.
Results (build host, through
rb, under memguard)Every run went through the build host's runner, under its memory guard at 64 GB. Each script writes cargo's output to a log on the host and greps it. Exit statuses:
gate.sh), at2d64a57d: GREEN. Build, library tests,carriage, the corpus loop (21 of 21), the fast-kernel step,byte-exact-conformance,wai-webon wasm32, and the neural gates, each exit 0.938582b3(whosewai/, workflows and scripts equale6453a95's): the D2c gate GREEN again, every step exit 0 and the corpus loop 21 of 21;check-tests-in-ci.py0;registry export --check0, up to date; nothing pulled back, soinclude/wai.his unchanged.2d64a57d:registry export --check: 0, up to date;jpegai_nets_opson the pinned bundle: 0, 8 of 8 passed (256 s);cargo kani --lib --only-codegeninwai-verify: 0;include/wai.his unchanged.e6453a95:check-tests-in-ci.py: 0, clean;jpegai_e2e_synthesis,jpegai_reconstruct_calibration,jpegai_ops(9) andjpegai_nets_ops(8, pinned cases skipped) underneural_int,legacy_int: 0;int_kernels_geometryunder the fast-kernel step's features: 0, 6 passed;neural,legacy_int: 0 (each returns without its fixture, as NOT-IN-CI.txt says).96f5468e):wai-opstests: 0;wai-verifybuild and tests: 0;bounds --check: 0, identical;--role-profile syn_y=acc32: 1, as it should be;jpegai_opsandjpegai_nets_ops: 0.wai-verify vectors verifyexited 1 here: the external set's registry member still saidacc32. Gate 3 gives itacc64withrole_profiles, and it has passed since.b9663685):registry export0,--check0, the registry tests 0 (14 passed), the differential 0,wai-verify vectors verify0, the Python checker with--external jpegai/v10, thewai-opstests 0.f97757a3): the differential's two new tests 0, in release:A32, and 5 broken networks (1 member missing, 2 with shift 128, 2 with a shortw), each refused alike by both;A32.5d3a0ea9):the_networks_keep_to_their_certificate_on_the_test_codestream: 0 (295 s, about 19.5 billion values held to their intervals).cbc4caf7): the Python checker 0,wai-verify vectors verify0, thewai-opstests 0,jpegai_opsandjpegai_nets_ops0, the fast-kernel unit test 0.f4de2c78):jpegai_e2e_full,jpegai_reconstruction_bindingandjpegai_cross_platform, with the pinned SHA-256: 0;jpegai_ops,jpegai_nets_opsandjpegai_memory: 0;jpegai_decode_symbols: 0;wai-webtests: 0 (32 passed), and its wasm32 check: 0.2d64a57d):cargo checkof the library underneural_intand underneural, and of the tests underlegacy_int: 0;wai_decode_bench's build and its JPEG-AI cases: 0;int_kernels_geometry: 0;jpegai_opsandjpegai_nets_ops: 0;byte-exact-conformance: 0;wai-verifybuild: 0.certify --checkon the pinned bundle: 0.Kani
No harness changed.
wai-verify's library compileswai-ops'lowermodule, which this branch extends (Builder::ops,lower::jpegai_nets), andwai-rs'int_kernels.rs, whose direct-network helpers are now gated onlegacy_int.cargo kani --lib --only-codegen: 0. Every harness builds under the verifier's toolchain.planshard (--harness proofs::plan::, the one that reaches the lowerings' predicates): 0. Its 6 enabled harnesses all verified: K12largest,p_convandp_leaky; K15; and K16pixel_shuffleandpixel_unshuffle. The run had a time limit of 900 s per harness and 2,400 s overall, under the 64 GB guard.kani_openon main and stay that way here, as do K27's two totality harnesses (k27_mans_sgm_is_total,k27_mans_fac_is_total).Left
WAI_JPEGAI_FRONTEND_FIXTURE,WAI_JPEGAI_HYPERSCALE_IO, and the calibration tests' fixtures that NOT-IN-CI.txt lists) are still rebuilt only from the reference software's local dumps.run_decode_*hook.py) that wrap the reference decoder and record each stage's inputs and outputs on the test codestream. The scripts and their dumps sit with the exported reference assets, outside the repository (jpegai-vm-assets/is ignored).jpegai/v1is already published. The notice also says that it grants no patent rights; the fixtures are values of the decode, asjpegai/v1's weights are.jpegai/v1on the models root, pinned intools/jpegai-e2e-v1.sha256, with the notice, is feasible.wai-jpegai-e2e.ymlcould then runjpegai_e2e_frontend,jpegai_e2e_chromaandjpegai_hyperscale_calibration.acc64-only (layer norm, attention and the Q16 activations, §7.3), so a GPU leg for them would emulate 64-bit arithmetic or leave them to the CPU. The scale path stays D3b'sacc32target./jpegaipage picks up the change with its next wasm build:decodeJpegAiFullnow decodes the networks through the operator set and reports a mistyped member.Notes
rbon the build host. Logs are under$RB_ROOT/logs/d2c-m7b/.08b5ac25), and each falsification's fault was restored with git before the next step.cargo fmt, nogit stash, and no cargo output piped intoheadortailas the only copy. No history was rewritten.include/wai.his unchanged.🤖 Generated with Claude Code
- jpegai_decode::decode_networks runs the whole decode with every integer stage through the operator set: the scale path and entropy decodes (§13.6.1), and the hyper decoders, context stages and synthesis through rec_y, rec_uv, syn_y and syn_uv (§13.6.2). The decode's default is unchanged until the switch (gate 6). - tests/jpegai_nets_ops.rs, on jpegai/v1 and the test codestream (build host, release, WAI_REQUIRE_SOTA_VECTORS=1): - the_networks_decode_through_the_lowering_as_directly: ŷ through rec_y (40960 values) and rec_uv (24576) equals the direct hyper decoder and context stages; Y (65536) and U, V (131072) through syn_y and syn_uv equal the direct synthesis, bit for bit as the float values the decode reports; - the_whole_decode_through_the_networks_is_the_pinned_decode: every stage hash equals the direct decode's and the pinned values of tests/jpegai_cross_platform.rs: the Synthesis stage d56695726bb6ebed…, the RGB SHA-256 dbc494a5a670914e…, both unchanged. - wai-jpegai-e2e.yml requires the new test by name. Co-Authored-By: Claude Opus 5.5 <[email protected]>- Refusal parity (tests/jpegai_nets_ops.rs): - every_load_check_of_the_networks_refuses_model_mismatch: 19 breaks of §13.6.2's load checks in the committed networks (a member missing or of the other kind, dims, counts, groups other than 4 or 5, a kernel not the topology's, a bias short, shifts of 128 and -1, a non-integer weight, a multiplier past i64, three temperatures, ψ of other than 4C channels, a luma synthesis of two planes, an odd feed-forward width, a mistyped member, a sum past i64 under A32) are refused model_mismatch from the files' bytes, 15 of them from the parsed networks too (the rest the direct parser cannot read); and two members of one name, from the bytes; - a_value_past_its_range_is_refused_field_range: a residual or a latent one past A32 at either end is refused field_range at its input by every graph that reads it; on the test codestream a residual at either end of A32, where the mean keeps the sum within it, decodes through rec_y and rec_uv as the direct decode does, and one past it is refused where the direct decode computed on (integer-operators §15.3 item 4). - Registry: wai.image.jpegai's ops member is { wai-ops/1, acc64, full, jpegai-int/1, role_profiles: { hs_y: acc32, hs_uv: acc32 } } (§11); the schema gains role_profiles (it requires profile); registry/capabilities.json and its schema regenerated by `wai registry export`. - SPEC §5 (the row's refusals and its reference implementation), §7 (NeuralEntropyExact names the profiles; the networks lie outside the claim), §8 (the networks' planned breaks). - CHANGELOG: a truncated sentence of the WIV1/WIR1 entry completed. Co-Authored-By: Claude Opus 5.5 <[email protected]>- jpegai_decode::{decode, decode_with_stages} load the bundle's networks (load_networks, under acc64) beside its scale path and run the hyper decoders, context stages and synthesis through rec_y, rec_uv, syn_y and syn_uv; decode_loaded(data, icci, norm, scale path, networks, observe) decodes with both loaded once. The direct networks are reached only from jpegai_decode::legacy (Front::Direct, Back::Direct, test-only, legacy_int). - The loaders no longer panic: Weights::from_json, IntNet::from_json and IcciNet::from_json return Result<_, BadMember>; a mistyped member is model_mismatch. IntNet keeps only well-formed tensors, so a member §13.6.1 reads that is mistyped is missing, as the lowering of the bytes refuses it. - The neural sink lowers and loads the networks from their eight files' bytes through the store of loaded sets (keyed by their listing, at acc64), parses only the eICCI net besides, and reports a refusal (model_mismatch, field_range) without falling back: a_refused_exact_decode_does_not_fall_back gains a non-integer network weight and a mistyped eICCI field. - The browser crate's decodeJpegAiFull reports a mistyped member. - Goldens, unchanged (build host, release): jpegai_cross_platform's nine pinned hashes, the Synthesis stage d56695726bb6ebed… among them; the decoded RGB SHA-256 dbc494a5a670914e… (jpegai_reconstruction_binding with WAI_JPEGAI_EXPECT_SHA256, jpegai_e2e_full: max|Δ| = 1 on 4.446%). - Memory (jpegai_memory, reference kernels): with the scale path and the networks loaded beforehand the decode holds 72,752,387 bytes, the direct decode 175,465,380; the networks take 89,727,913 to load and hold 55,530,900. - Also green: clippy's disallowed-methods guard and jpegai_decode_symbols, the sink's three dispatch tests, wai-web's tests and its wasm32 build; include/wai.h unchanged. - CHANGELOG: the M7b entry. Co-Authored-By: Claude Opus 5.5 <[email protected]>