nx_zstd_fse_dec_gate.nx source
↩ module page · 231 lines · 10197 B
1// nx_zstd_fse_dec_gate.nx -- proves the FSE decoding state machine.
2//
3// T3 is the invariant that matters most: over a long decode the state must
4// ALWAYS stay inside the table and the symbol must always be one the
5// distribution actually contains. An FSE decoder whose newState baseline or
6// nbBits is off produces in-range garbage for a while and then walks out of
7// the table -- so a single decode proves nothing and a long run proves a lot.
8//
9// T4 pins that nbBits of ZERO is legal. High-probability symbols cost no bits
10// to advance from; a decoder that treats zero as an error, or reads a bit
11// anyway, desynchronises on the first such state. The test asserts at least
12// one zero-cost state exists in a skewed distribution and that advancing from
13// it consumes nothing.
14//
15// T5 pins DETERMINISM: the same stream and table must produce the same symbol
16// sequence every time. That is what makes an entropy decoder usable at all.
17//
18// NOT PROVEN HERE, DELIBERATELY: the predefined distributions for literal
19// lengths, match lengths and offsets. Those are spec DATA and are not in the
20// module -- transcribing them from memory would yield a decoder that looks
21// right and disagrees with every other implementation.
22//
23// license_tier: ORIGINAL
24import "nx_syscalls.nx"
25import "nx_zstd_fse.nx"
26import "nx_zstd_bits.nx"
27import "nx_zstd_fse_dec.nx"
28
29func g_puts(s: *u8) -> i64 {
30 var i: i64 = 0
31 while s[i] != (0 as u8) { i = i + 1 }
32 sys_write(1, s, i)
33 return i
34}
35
36func g_putn(v: i64) -> i64 {
37 let buf: *u8 = sys_mmap(32)
38 var x: i64 = v
39 if x < 0 { g_puts("-" as *u8); x = 0 - x }
40 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
41 let tmp: *u8 = sys_mmap(32)
42 var d: i64 = 0
43 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
44 var i: i64 = 0
45 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
46 sys_write(1, buf, d)
47 return d
48}
49
50func main() -> i64 {
51 var fails: i64 = 0
52 var mark: i64 = 0
53 var i: i64 = 0
54
55 // ---- build a table from a known distribution: 16/8/8 at log 5 ----
56 let norm: *i64 = sys_mmap(NX_FSE_MAX_SYMBOL * 8 + 64) as *i64
57 i = 0
58 while i < NX_FSE_MAX_SYMBOL { norm[i] = 0; i = i + 1 }
59 norm[0] = 16; norm[1] = 8; norm[2] = 8
60 let t: *NxFseTable = nx_fse_build_dtable(norm, 2, 5)
61 if t == (0 as *NxFseTable) { fails = fails + 1 }
62 if fails > 0 { if mark == 0 { mark = 0 - 1 } }
63
64 // ---- T1: state init reads exactly tableLog bits ----
65 let d: *u8 = sys_mmap(256)
66 i = 0
67 while i < 32 { d[i] = ((i * 53 + 17) & 255) as u8; i = i + 1 }
68 d[31] = 0x80 as u8 // sentinel at the top of the final byte
69 let b: *NxZstdBits = nx_zstd_bits_init(d, 32)
70 if b == (0 as *NxZstdBits) { fails = fails + 1 } else {
71 let before: i64 = nx_zstd_bits_remaining(b)
72 let s0: i64 = nx_zstd_fse_state_init(t, b)
73 if s0 < 0 { fails = fails + 1 }
74 if s0 >= 32 { fails = fails + 1 }
75 if nx_zstd_bits_remaining(b) != (before - 5) { fails = fails + 1 }
76 }
77 if fails > 0 { if mark == 0 { mark = 1 } }
78
79 // ---- T2: the symbol is read at the CURRENT state ----
80 // every table index must name a symbol the distribution contains
81 var bad: i64 = 0
82 i = 0
83 while i < 32 {
84 let s: i64 = nx_zstd_fse_state_symbol(t, i)
85 if s < 0 { bad = bad + 1 }
86 if s > 2 { bad = bad + 1 }
87 i = i + 1
88 }
89 if bad != 0 { fails = fails + 1 }
90 // out-of-range states report -1 rather than a plausible symbol
91 if nx_zstd_fse_state_symbol(t, 32) != (0 - 1) { fails = fails + 1 }
92 if nx_zstd_fse_state_symbol(t, 0 - 1) != (0 - 1) { fails = fails + 1 }
93 if fails > 0 { if mark == 0 { mark = 2 } }
94
95 // ---- T3: a LONG decode stays inside the table throughout ----
96 let b2: *NxZstdBits = nx_zstd_bits_init(d, 32)
97 var state: i64 = nx_zstd_fse_state_init(t, b2)
98 var steps: i64 = 0
99 var range_bad: i64 = 0
100 var sym_bad: i64 = 0
101 var seen0: i64 = 0
102 var seen1: i64 = 0
103 var seen2: i64 = 0
104 var go: i64 = 1
105 while go == 1 {
106 if state < 0 { range_bad = range_bad + 1; go = 0 } else {
107 let s: i64 = nx_zstd_fse_state_symbol(t, state)
108 if s < 0 { sym_bad = sym_bad + 1 } else {
109 if s == 0 { seen0 = seen0 + 1 }
110 if s == 1 { seen1 = seen1 + 1 }
111 if s == 2 { seen2 = seen2 + 1 }
112 if s > 2 { sym_bad = sym_bad + 1 }
113 }
114 let cost: i64 = nx_zstd_fse_state_cost(t, state)
115 if cost < 0 { range_bad = range_bad + 1; go = 0 } else {
116 if nx_zstd_bits_remaining(b2) < cost { go = 0 } else {
117 state = nx_zstd_fse_state_next(t, b2, state)
118 steps = steps + 1
119 if steps > 500 { go = 0 }
120 }
121 }
122 }
123 }
124 if range_bad != 0 { fails = fails + 1 }
125 if sym_bad != 0 { fails = fails + 1 }
126 // the walk must have actually gone somewhere
127 if steps < 20 { fails = fails + 1 }
128 // and it must have visited more than one symbol -- a decoder stuck on one
129 // state would pass the range checks while decoding nothing
130 var distinct: i64 = 0
131 if seen0 > 0 { distinct = distinct + 1 }
132 if seen1 > 0 { distinct = distinct + 1 }
133 if seen2 > 0 { distinct = distinct + 1 }
134 if distinct < 2 { fails = fails + 1 }
135 if fails > 0 { if mark == 0 { mark = 3 } }
136
137 // ---- T4: nbBits of ZERO is legal and consumes nothing ----
138 // A zero-cost state needs a symbol dominant enough that its next-state
139 // reaches the TABLE SIZE: nb = tableLog - highbit(nextState), so nb hits 0
140 // only when nextState >= 2^tableLog. With 16/8/8 the minimum is ONE bit --
141 // that distribution has no zero-cost state at all. 24/4/4 does: symbol 0's
142 // next-states run 24..47, and the 16 of them at 32 and above cost nothing.
143 let norm2: *i64 = sys_mmap(NX_FSE_MAX_SYMBOL * 8 + 64) as *i64
144 i = 0
145 while i < NX_FSE_MAX_SYMBOL { norm2[i] = 0; i = i + 1 }
146 norm2[0] = 24; norm2[1] = 4; norm2[2] = 4
147 let t0: *NxFseTable = nx_fse_build_dtable(norm2, 2, 5)
148 if t0 == (0 as *NxFseTable) { fails = fails + 1 } else {
149 var zero_states: i64 = 0
150 i = 0
151 while i < 32 {
152 if nx_zstd_fse_state_cost(t0, i) == 0 { zero_states = zero_states + 1 }
153 i = i + 1
154 }
155 if zero_states == 0 { fails = fails + 1 } else {
156 // and the 16/8/8 table must have NONE, which is what made the
157 // first version of this test wrong -- assert both directions
158 var flat_zero: i64 = 0
159 i = 0
160 while i < 32 {
161 if nx_zstd_fse_state_cost(t, i) == 0 { flat_zero = flat_zero + 1 }
162 i = i + 1
163 }
164 if flat_zero != 0 { fails = fails + 1 }
165
166 var zs: i64 = 0 - 1
167 i = 0
168 while i < 32 {
169 if zs < 0 { if nx_zstd_fse_state_cost(t0, i) == 0 { zs = i } }
170 i = i + 1
171 }
172 let b3: *NxZstdBits = nx_zstd_bits_init(d, 32)
173 let r0: i64 = nx_zstd_bits_remaining(b3)
174 let ns: i64 = nx_zstd_fse_state_next(t0, b3, zs)
175 if ns < 0 { fails = fails + 1 }
176 if ns >= 32 { fails = fails + 1 }
177 if nx_zstd_bits_remaining(b3) != r0 { fails = fails + 1 }
178 }
179 }
180 if fails > 0 { if mark == 0 { mark = 4 } }
181
182 // ---- T5: DETERMINISM -- same stream, same table, same symbols ----
183 let ba: *NxZstdBits = nx_zstd_bits_init(d, 32)
184 let bb: *NxZstdBits = nx_zstd_bits_init(d, 32)
185 var sa: i64 = nx_zstd_fse_state_init(t, ba)
186 var sb: i64 = nx_zstd_fse_state_init(t, bb)
187 var mismatch: i64 = 0
188 i = 0
189 while i < 40 {
190 if nx_zstd_fse_state_symbol(t, sa) != nx_zstd_fse_state_symbol(t, sb) { mismatch = mismatch + 1 }
191 if sa != sb { mismatch = mismatch + 1 }
192 let c: i64 = nx_zstd_fse_state_cost(t, sa)
193 if nx_zstd_bits_remaining(ba) < c { i = 40 } else {
194 sa = nx_zstd_fse_state_next(t, ba, sa)
195 sb = nx_zstd_fse_state_next(t, bb, sb)
196 i = i + 1
197 }
198 }
199 if mismatch != 0 { fails = fails + 1 }
200 if fails > 0 { if mark == 0 { mark = 5 } }
201
202 // ---- T6 NEG: refusals ----
203 if nx_zstd_fse_state_init(0 as *NxFseTable, b) != (0 - 1) { fails = fails + 1 }
204 if nx_zstd_fse_state_init(t, 0 as *NxZstdBits) != (0 - 1) { fails = fails + 1 }
205 if nx_zstd_fse_state_next(0 as *NxFseTable, b, 0) != (0 - 1) { fails = fails + 1 }
206 if nx_zstd_fse_state_next(t, 0 as *NxZstdBits, 0) != (0 - 1) { fails = fails + 1 }
207 if nx_zstd_fse_state_next(t, b, 32) != (0 - 1) { fails = fails + 1 }
208 if nx_zstd_fse_state_next(t, b, 0 - 1) != (0 - 1) { fails = fails + 1 }
209 if nx_zstd_fse_state_cost(t, 99) != (0 - 1) { fails = fails + 1 }
210 // an exhausted stream cannot init a state
211 let tiny: *u8 = sys_mmap(64)
212 tiny[0] = 0x01 as u8
213 let bt: *NxZstdBits = nx_zstd_bits_init(tiny, 1)
214 if bt != (0 as *NxZstdBits) {
215 if nx_zstd_fse_state_init(t, bt) != (0 - 1) { fails = fails + 1 }
216 }
217 if fails > 0 { if mark == 0 { mark = 6 } }
218
219 if fails == 0 {
220 g_puts("GATE nx_zstd_fse_dec verdict=GREEN pass=6/6 (state init consumes exactly tableLog bits; every table index names a symbol in the distribution and out-of-range states report -1; a LONG walk stays inside the table for its whole run and visits MORE THAN ONE symbol so a stuck decoder cannot pass; nbBits of ZERO is legal -- proven BOTH ways: a 24/4/4 table HAS zero-cost states and advancing from one consumes NOTHING, while 16/8/8 has NONE (nb hits 0 only when nextState reaches the table size); DETERMINISM -- two readers over the same stream agree on state and symbol for 40 steps; NEG null table/null reader/out-of-range state/exhausted stream refused. Predefined LL/ML/OF distributions deliberately NOT included -- spec data, not derivable)\n" as *u8)
221 sys_exit(0)
222 return 0
223 }
224 g_puts("GATE nx_zstd_fse_dec verdict=RED fails=" as *u8)
225 g_putn(fails)
226 g_puts(" first_stage=" as *u8)
227 g_putn(mark)
228 g_puts("\n" as *u8)
229 sys_exit(1)
230 return 1
231}