nx_vp8_gate.nx

nx_vp8_gate.nx -- proves the VP8 boolean decoder and keyframe header. T2 is the one that validates the whole entropy engine without needing an encoder: at probability 128 the split lands exactly at the midpoint, so the coder degenerates to reading the stream MSB-first. Decoding 128 prob-128 bits must therefore reproduce the raw bits of the input bytes EXACTLY. Any error in the shift, the carry or the 8-bit byte refill breaks it on the first refill boundary. T3 asserts the RANGE INVARIANT after every single decode: 128 <= range <= 255. A renormalisation loop that under- or over-shifts returns plausible bits for a while and then diverges, so checking the invariant per call catches it at the first bit rather than the thousandth. T6 pins the mandatory start code. Without it a corrupt or non-VP8 payload decodes as a frame with dimensions read out of arbitrary bytes. license_tier: ORIGINAL