nx_av1_ec_gate.nx source
↩ module page · 154 lines · 6364 B
1// nx_av1_ec_gate.nx -- proves the AV1/AV2 multi-symbol CDF arithmetic decoder.
2//
3// This gate exists because writing this module produced a real bug: the first
4// draft mixed libaom's INVERTED cdf convention with the spec's FORWARD one and
5// wrote the adaptation as a bare `if i == symbol` instead of the spec's
6// running threshold. Both mistakes still decode -- they drift. T7/T8/T9 pin
7// the adaptation DIRECTION and MAGNITUDE against hand-computed spec values, so
8// the convention cannot silently flip again.
9//
10// T13 is the one that matters most for liveness: the terminator cdf[N-1] must
11// stay exactly 32768 forever. update_cdf only walks i < N-1 precisely so it
12// cannot touch it. If it ever drifts below, f never reaches 0, cur never
13// reaches 0, and decode_symbol walks off the end of every distribution.
14//
15// NON-VACUITY: T11/T12 are negative controls -- out-of-range symbols, tiny
16// alphabets and a null coder must each be REFUSED.
17//
18// license_tier: ORIGINAL
19import "nx_syscalls.nx"
20import "nx_bitstream.nx"
21import "nx_av1_ec.nx"
22
23func g_puts(s: *u8) -> i64 {
24 var i: i64 = 0
25 while s[i] != (0 as u8) { i = i + 1 }
26 sys_write(1, s, i)
27 return i
28}
29
30func main() -> i64 {
31 var fails: i64 = 0
32
33 // ---- T1: FloorLog2 ----
34 if nx_av1_floor_log2(1) != 0 { fails = fails + 1 }
35 if nx_av1_floor_log2(2) != 1 { fails = fails + 1 }
36 if nx_av1_floor_log2(3) != 1 { fails = fails + 1 }
37 if nx_av1_floor_log2(32768) != 15 { fails = fails + 1 }
38 if nx_av1_floor_log2(0) != (0 - 1) { fails = fails + 1 }
39
40 // ---- T2: a uniform 4-symbol CDF is FORWARD and terminates at 32768 ----
41 let c4: *i64 = nx_av1_cdf_uniform(4)
42 if c4 == (0 as *i64) { fails = fails + 1 } else {
43 if c4[0] != 8192 { fails = fails + 1 }
44 if c4[1] != 16384 { fails = fails + 1 }
45 if c4[2] != 24576 { fails = fails + 1 }
46 if c4[3] != 32768 { fails = fails + 1 }
47 if c4[4] != 0 { fails = fails + 1 }
48 }
49
50 // ---- T3: the 2-symbol case ----
51 let c2: *i64 = nx_av1_cdf_uniform(2)
52 if c2[0] != 16384 { fails = fails + 1 }
53 if c2[1] != 32768 { fails = fails + 1 }
54 if c2[2] != 0 { fails = fails + 1 }
55
56 // ---- T4: init primes range to the full window ----
57 let data: *u8 = sys_mmap(64)
58 var k: i64 = 0
59 while k < 16 { data[k] = 0x5a as u8; k = k + 1 }
60 let bs: *NxBitStream = nx_bitstream_alloc(data, 16)
61 let ec: *NxAv1Ec = nx_av1_ec_init(bs, 16)
62 if ec == (0 as *NxAv1Ec) { fails = fails + 1 } else {
63 if ec.range != 32768 { fails = fails + 1 }
64 }
65
66 // ---- T5/T6: every decoded symbol is in range, and range renormalises ----
67 var bad_sym: i64 = 0
68 var bad_range: i64 = 0
69 var d: i64 = 0
70 while d < 20 {
71 let s: i64 = nx_av1_decode_symbol(ec, c4, 4)
72 if s < 0 { bad_sym = bad_sym + 1 }
73 if s > 3 { bad_sym = bad_sym + 1 }
74 if ec.range < 32768 { bad_range = bad_range + 1 }
75 if ec.range >= 65536 { bad_range = bad_range + 1 }
76 d = d + 1
77 }
78 if bad_sym != 0 { fails = fails + 1 }
79 if bad_range != 0 { fails = fails + 1 }
80
81 // ---- T7: adapting toward symbol 0 RAISES cdf[0] by the spec amount ----
82 // n=2, fresh uniform: rate = 3 + 0 + 0 + min(FloorLog2(2),2) = 4
83 // i=0 is the symbol -> tmp=32768 -> cdf[0] += (32768-16384)>>4 = 1024
84 let a1: *i64 = nx_av1_cdf_uniform(2)
85 nx_av1_update_cdf(a1, 0, 2)
86 if a1[0] != 17408 { fails = fails + 1 }
87 if a1[2] != 1 { fails = fails + 1 }
88
89 // ---- T8: adapting toward symbol 1 LOWERS cdf[0] by the same amount ----
90 // i=0 is not the symbol -> tmp stays 0 -> cdf[0] -= (16384-0)>>4 = 1024
91 let a2: *i64 = nx_av1_cdf_uniform(2)
92 nx_av1_update_cdf(a2, 1, 2)
93 if a2[0] != 15360 { fails = fails + 1 }
94
95 // ---- T9: the running threshold across a 3-symbol alphabet ----
96 // uniform = 10922, 21845, 32768; symbol 1, rate 4
97 // i=0: tmp=0 -> cdf[0] -= 10922>>4 = 682 -> 10240
98 // i=1: tmp=32768 -> cdf[1] += (32768-21845)>>4 = 682 -> 22527
99 let a3: *i64 = nx_av1_cdf_uniform(3)
100 if a3[0] != 10922 { fails = fails + 1 }
101 if a3[1] != 21845 { fails = fails + 1 }
102 nx_av1_update_cdf(a3, 1, 3)
103 if a3[0] != 10240 { fails = fails + 1 }
104 if a3[1] != 22527 { fails = fails + 1 }
105 // symbol 1's interval must have WIDENED: was 10923, now 12287
106 if (a3[1] - a3[0]) <= 10923 { fails = fails + 1 }
107
108 // ---- T10: repeated adaptation converges upward, never past full ----
109 let a4: *i64 = nx_av1_cdf_uniform(2)
110 var prev: i64 = a4[0]
111 var mono: i64 = 0
112 var over: i64 = 0
113 var r: i64 = 0
114 while r < 40 {
115 nx_av1_update_cdf(a4, 0, 2)
116 if a4[0] < prev { mono = mono + 1 }
117 if a4[0] > 32768 { over = over + 1 }
118 prev = a4[0]
119 r = r + 1
120 }
121 if mono != 0 { fails = fails + 1 }
122 if over != 0 { fails = fails + 1 }
123 // the usage counter saturates at 32
124 if a4[2] != 32 { fails = fails + 1 }
125
126 // ---- T13: the terminator NEVER drifts -- liveness depends on it ----
127 let a5: *i64 = nx_av1_cdf_uniform(4)
128 var t: i64 = 0
129 while t < 50 {
130 nx_av1_update_cdf(a5, t % 4, 4)
131 t = t + 1
132 }
133 if a5[3] != 32768 { fails = fails + 1 }
134
135 // ---- T11 NEG: malformed adaptation calls are REFUSED ----
136 if nx_av1_update_cdf(a1, 2, 2) != 0 { fails = fails + 1 }
137 if nx_av1_update_cdf(a1, 0 - 1, 2) != 0 { fails = fails + 1 }
138 if nx_av1_update_cdf(a1, 0, 1) != 0 { fails = fails + 1 }
139
140 // ---- T12 NEG: malformed decode calls are REFUSED ----
141 if nx_av1_decode_symbol(0 as *NxAv1Ec, c4, 4) != (0 - 1) { fails = fails + 1 }
142 if nx_av1_decode_symbol(ec, c4, 1) != (0 - 1) { fails = fails + 1 }
143 if nx_av1_cdf_uniform(1) != (0 as *i64) { fails = fails + 1 }
144 if nx_av1_ec_init(bs, 0) != (0 as *NxAv1Ec) { fails = fails + 1 }
145
146 if fails == 0 {
147 g_puts("GATE nx_av1_ec verdict=GREEN pass=13/13 (FloorLog2; forward uniform CDF 4+2+3 sym; init range 32768; 20 decodes in-range with range renormalised to [32768,65536); adaptation up/down at spec magnitude 1024; running threshold widens the chosen interval; 40x converges monotonic, counter saturates 32; terminator holds 32768 over 50 updates; NEG bad symbol/alphabet/null-coder/zero-size refused)\n" as *u8)
148 sys_exit(0)
149 return 0
150 }
151 g_puts("GATE nx_av1_ec verdict=RED\n" as *u8)
152 sys_exit(1)
153 return 1
154}