wai: integer-operators (Draft), the operator set wai-ops/1, with its payload text in integer-payloads #202
Loading…
Reference in a new issue
No description provided.
Delete branch "wai/d2a-operators-text"
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?
Adds
wai/extensions/integer-operators.md(Draft):wai-ops/1, the integer operator set the integer-exact capabilities decode through. It also adds tointeger-payloads.mdthe payload text the operator set depends on. Text only: no code, vector or registry change.What lands
1.
integer-operators.md, status Draft. It covers:derived,clamporcheck;acc64andacc32profiles;wai-ops/1-npu;WHG1graph form;wai.image.jpegaiscale path (§13.6.1);int_synth.json,WHM1,WAM1andWMB1toWHG1;The status block says that the
wai-opscrate, thewai-verify boundstool and theops-conformancecorpus come after this Draft. Until they land, each capability's reference is the decoder its payload extension names.2.
integer-payloads.md.entropy.json. Its sentence on the layers' arithmetic now cites integer-operators §13.2 and §13.3.wai.neural.int_synthpayload andint_synth.json.WIM1and theWMB1bundle. It states that every element ofynot yet decoded is 0 when it enters the entropy network, and that the three networks and the tables share oneafracin1..=30.Every statement in these sections was checked against the decoders:
CondEntropy::try_from_value,int_synth::decode_from_spec,int_mlicpp::{parse_header, from_bundle, decode_inner}. They match, with one exception.int_synthdoes not yet make these checks: a reserved byte of 0,C ≥ 1, the caps,k ≥ 1,stride ≥ 1, a shift of at most 127, and the certificate. These are planned changes that take effect with the capability's lowering. §13 lists them as checks that wait for the lowering, and integer-operators §15.3 says each change takes effect then. Every committedint_synthpayload and set already passes the syntactic ones.3. The README names the extension, and the CHANGELOG records it. No file enumerates the extensions directory apart from the section-refs check, which picks the new file up by itself. Wire identifiers in the registry cover delivery identifiers only, and they do not list the integer payload magics, so none is added.
Edits to the drafted text
The first commit is the text as drafted. The second commit reconciles it with what lands beside it:
WIA1andWIS1rows now cite integer-payloads §5 and §6; before, they pointed at this text's own §5 and §6.[1, C, 1, 1], not[C];Check (a): E8 and §13.6.1 against
jpegai_mans.rs, on the committed vectorMethod.
sgmandfac, the scale graph and the stage operators.jpegai_mans.rsagainst E8 line by line, andjpegai_decode::decode_plane,decode_hyper_scaleand thejpegai_pipelinederivations against §13.6.1.wai-rsdumped what the code computes ontests/vectors/jpegai/test256.bin, the committed codestream. It used the pinnedjpegai/v1membersnorm.json,hs_y.jsonandhs_uv.json, and their SHA-256 values matchedtools/jpegai-e2e-v1.sha256.Results. All match:
test256.bin. Both planes, luma at 160 channels and chroma at 96, give identical integers at every stage:z,I_s, the mask,likely,rvs,σ_idxandy_q. That covers 703 and 537 coded latent positions, three of them decoded through the escape, and 4,096 hyper-latent symbols, seven of them through theread(6)escape. The 32 × 256 latent tables are identical too.test256.bin's, and the hyper-latent symbols of both planes, every span'sσ_idxand mask, and every span's symbols are identical. This also confirms the chroma plane's 160 discarded luma rows.sgmspan matches, 12 positions of it escaped.facrows of 96 match, four symbols of them escaped.stream_exhausted) exactly where the code panicked;Falsifying the checker. Each mutation went into a copy of the Python, not the repository:
B_yas signed failed the fuzz (94 mismatches);mod 2^8from the state update failed both;test256.bin.Findings.
test256.bincodesσ_idx≤ 20 for luma and ≤ 10 for chroma, and the golden streams use bounds 4–11. So a decoder that readsB_yas signed passes every existing jpegai test. Only the fuzz above tells the two readings apart, and the synthetic vector §14.1 item 7 calls for has to carry the check.T_zcarry rule: every committed row ends at 255.sgmgroup reads at most 49 between refills even with its flush moved after the outbound reads. Moving thesgmgroup flush after the outbound reads left every fuzz case unchanged, refusals included. Only the point at which a refusal fires could depend on it.Check (b): Lemma L1, and the 512-bit sufficiency of §8.1
Lemma L1, re-derived.
d_c² ≤ T < C·(V + 1), and(r + 1)² > V + ε ≥ V + 1, so|d_c| < √C·(r + 1).k ≤ 2^32/randr ≥ r0, this gives|d_c·k| < isqrt_ceil(C)·2^32·(r0 + 1)/r0.Y = isqrt_ceil(C)·2^16·(r0 + 1)/r0. Thenn_c < Y. On the negative side the floor adds at most 1, so|n_c| < Y + 1, and therefore|n_c| ≤ ⌈Y⌉ ≤ ⌊Y⌋ + 1 = N_max.ln.nandln.dkrules needs the mean in[l, h]. It is: the mean isS/Crounded half away from zero, andS/Clies between the integerslandh.Trying to break it. I implemented
layernorm_cexactly as §5.7 and §2 define it, and asserted that every value it forms lies in its §8.3 interval. That covers every partial sum ofln.Sandln.T, and each ofln.m,ln.d,ln.v,ln.k,ln.dk,ln.n,ln.ngand the output. Inputs:Cfrom 1 to 4, small ranges, and 14 values ofεfrom 1 to 2^64 − 1;|n|/N_max, withCup to 64, ranges up to 2^62 andγat the i32 extremes;layernorm_cstages, each stage's input range the previous stage's producer result.There was no counterexample. The
ln.dkbound is attained exactly: withC = 2andx = (l, l + 1),|d·k| = ⌊2^32/r0⌋. The largest|n|/N_maxseen was 0.984.512 bits, re-derived. After saturation, every operand lies within ±2^255. So a product lies within ±2^510, a sum within ±2^256, and every other primitive within its operands' range. A signed 512-bit integer holds that, with nothing to spare:
igdn.x2on an input at ±2^255 forms 2^510. The text now says so.Trying to break it. An engine computed every primitive exactly, asserted that each operand lay within ±2^255 and each result within signed 512 bits, then saturated. It ran 20,000 random chains of up to 11 operators with extreme parameters:
convwith ±2^63 weights and post biases;rqat shift 127 in every rounding mode;mul;igdnwithγandβat the i64 extremes;layernorm_catε = 2^64 − 1andC = 2^26;l2normandgramatL = 2^26;leakyata = −2^63;addandsoftmax.Those chains formed 120,626 nodes, 13,291 of them saturated. No operand fell outside ±2^255, and no exact result needed more than 512 bits.
Finding, fixed in the text. §8.1 fixed the order of a
Σbut not that of a product of three or more factors written without one. A zero factor makes the saturated flag depend on the order:2^200·2^100·0. Every such product in §8.3 is safe:C·(h − l)²,L·X²andisqrt_ceil(C)·2^32·(r0 + 1). Either no factor can be 0, or a 0 makes every partial product 0. All 42 extreme cases agree in every order. So no certificate changes, and the text now fixes a left fold as written.R_roundis evaluated as §2 writes it. The half-up addend it forms is the onerq.palready forms on the same node, so this cannot change a flag either.Review fixes (commits 3 to 5)
A review of the D2a crate and corpus against this text found rules that only the crate and the corpus README stated, and two width claims that do not hold. Each is now in the text. The crate PR carries the matching code and a vector for each rule.
model_mismatch,field_rangefor E2, andgeometry_mismatchfor the shapes E11 and E12 read. E5, E6, E7 and E10 now state their conditions. E8's table and bound checks aremodel_mismatch; only its window refusals arestream_exhausted.hi − lo ≤ 65535,lo − 131070andhi + 131070also fit. Atlo = 2^31 − 65536,hi = 2^31 − 1,q = 65535,pred = hiandr = 2, it formshi + 131070.(b − a)·ρreaches65535·(2^32 − 2), just under 2^48, and rdiv's2|n| + dpasses 2^48. Every value fits i50, not 47 bits.max_elems.cout·uh·uw.subpos_mergetakes the hull of its inputs' intervals, andcrop_totakes its first input's interval.chscale'sm_bytesandlayernorm_c'sg_bytesare 4 or 8.derived. The crate gave such a tensorcheck [−2^63, I64], so three committed lowered graphs did not follow the text. The crate PR regenerates them.modes, the predictors' fields and CHW layouts, andcoding_order's indices are now normative.atis now defined, includingmans_decode's position rule for a flush that belongs to no single position.profiles.Checks run
scripts/check-wai-section-refs.py: clean. It now checks the references to integer-payloads §13 and §14, integer-operators §13.0, §13.2, §13.3 and §15.3, and determinism-tiers §5.check-public-names.shandcheck-comparative-prose.sh, one file at a time, on both extension texts, the README and this body: clean, and again on integer-operators after the review fixes. The CHANGELOG's hits are historical lines only.check-no-vanity-metrics.sh: clean.integer-payloads.md. #197, #199 and #200 also add CHANGELOG entries at the top, so whichever lands second has a one-hunk conflict there.🤖 Generated with Claude Code
profilestoo