nx_av1_ec_gate.nx

nx_av1_ec_gate.nx -- proves the AV1/AV2 multi-symbol CDF arithmetic decoder. This gate exists because writing this module produced a real bug: the first draft mixed libaom's INVERTED cdf convention with the spec's FORWARD one and wrote the adaptation as a bare `if i == symbol` instead of the spec's running threshold. Both mistakes still decode -- they drift. T7/T8/T9 pin the adaptation DIRECTION and MAGNITUDE against hand-computed spec values, so the convention cannot silently flip again. T13 is the one that matters most for liveness: the terminator cdf[N-1] must stay exactly 32768 forever. update_cdf only walks i < N-1 precisely so it cannot touch it. If it ever drifts below, f never reaches 0, cur never reaches 0, and decode_symbol walks off the end of every distribution. NON-VACUITY: T11/T12 are negative controls -- out-of-range symbols, tiny alphabets and a null coder must each be REFUSED. license_tier: ORIGINAL