nx_zstd_huf_gate.nx source
↩ module page · 187 lines · 8481 B
1// nx_zstd_huf_gate.nx -- proves the zstd Huffman decode table.
2//
3// T2 pins the EXACT table layout for a known weight set, index by index.
4// Weights {2,1,4,3,1} at tableLog 4 must tile 16 entries as:
5// 0..7 symbol 2, 1 bit (weight 4, the shortest code, LOWEST indices)
6// 8..11 symbol 3, 2 bits
7// 12..13 symbol 0, 3 bits
8// 14 symbol 1, 4 bits
9// 15 symbol 4, 4 bits
10// Laying ranks out in SYMBOL order instead of DESCENDING WEIGHT produces a
11// table that decodes self-consistently and disagrees with every other zstd
12// implementation -- a file only this decoder can read. Asserting the indices
13// directly is the only way to catch that.
14//
15// T3 requires the slots to TILE EXACTLY. A weight set that sums to 15 of 16
16// leaves an entry no symbol ever claims, and a peek landing there would decode
17// as symbol 0 forever. The build refuses rather than leaving the hole.
18//
19// T5 decodes a hand-assembled backward stream. Bits were placed so the reader
20// emits 0 | 10 | 110 | 1111, which must come out as symbols 2, 3, 0, 4 --
21// four codes of four different lengths, so a decoder that consumes tableLog
22// bits per symbol instead of the code's true length fails on the second one.
23//
24// license_tier: ORIGINAL
25import "nx_syscalls.nx"
26import "nx_zstd_bits.nx"
27import "nx_zstd_huf.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 let w: *i64 = sys_mmap(512 * 8) as *i64
56
57 // ---- T1: the table builds and has the right shape ----
58 w[0] = 2; w[1] = 1; w[2] = 4; w[3] = 3; w[4] = 1
59 let t: *NxZstdHuf = nx_zstd_huf_build(w, 5, 4)
60 if t == (0 as *NxZstdHuf) { fails = fails + 1 } else {
61 if t.table_log != 4 { fails = fails + 1 }
62 if t.table_size != 16 { fails = fails + 1 }
63 }
64 if fails > 0 { if mark == 0 { mark = 1 } }
65
66 // ---- T2: the EXACT layout, heaviest weight at the LOWEST indices ----
67 // indices 0..7 -> symbol 2 at 1 bit
68 i = 0
69 while i < 8 {
70 if nx_zstd_huf_symbol_at(t, i) != 2 { fails = fails + 1 }
71 if nx_zstd_huf_nbits_at(t, i) != 1 { fails = fails + 1 }
72 i = i + 1
73 }
74 // 8..11 -> symbol 3 at 2 bits
75 i = 8
76 while i < 12 {
77 if nx_zstd_huf_symbol_at(t, i) != 3 { fails = fails + 1 }
78 if nx_zstd_huf_nbits_at(t, i) != 2 { fails = fails + 1 }
79 i = i + 1
80 }
81 // 12..13 -> symbol 0 at 3 bits
82 if nx_zstd_huf_symbol_at(t, 12) != 0 { fails = fails + 1 }
83 if nx_zstd_huf_symbol_at(t, 13) != 0 { fails = fails + 1 }
84 if nx_zstd_huf_nbits_at(t, 12) != 3 { fails = fails + 1 }
85 // 14 -> symbol 1, 15 -> symbol 4, both at 4 bits
86 if nx_zstd_huf_symbol_at(t, 14) != 1 { fails = fails + 1 }
87 if nx_zstd_huf_symbol_at(t, 15) != 4 { fails = fails + 1 }
88 if nx_zstd_huf_nbits_at(t, 14) != 4 { fails = fails + 1 }
89 if nx_zstd_huf_nbits_at(t, 15) != 4 { fails = fails + 1 }
90 if fails > 0 { if mark == 0 { mark = 2 } }
91
92 // ---- T3: every symbol occupies exactly 2^(weight-1) slots ----
93 let seen: *i64 = sys_mmap(64 * 8) as *i64
94 i = 0
95 while i < 8 { seen[i] = 0; i = i + 1 }
96 i = 0
97 while i < 16 {
98 let s: i64 = nx_zstd_huf_symbol_at(t, i)
99 if s < 0 { fails = fails + 1 } else { seen[s] = seen[s] + 1 }
100 i = i + 1
101 }
102 if seen[0] != 2 { fails = fails + 1 } // weight 2 -> 2 slots
103 if seen[1] != 1 { fails = fails + 1 } // weight 1 -> 1 slot
104 if seen[2] != 8 { fails = fails + 1 } // weight 4 -> 8 slots
105 if seen[3] != 4 { fails = fails + 1 } // weight 3 -> 4 slots
106 if seen[4] != 1 { fails = fails + 1 } // weight 1 -> 1 slot
107 // out-of-range accessors report -1 rather than reading past the table
108 if nx_zstd_huf_symbol_at(t, 16) != (0 - 1) { fails = fails + 1 }
109 if nx_zstd_huf_symbol_at(t, 0 - 1) != (0 - 1) { fails = fails + 1 }
110 if fails > 0 { if mark == 0 { mark = 3 } }
111
112 // ---- T4: peek does NOT move the cursor; skip does ----
113 let pd: *u8 = sys_mmap(64)
114 pd[0] = 0x6f as u8; pd[1] = 0x05 as u8
115 let pb: *NxZstdBits = nx_zstd_bits_init(pd, 2)
116 if pb == (0 as *NxZstdBits) { fails = fails + 1 } else {
117 if nx_zstd_bits_remaining(pb) != 10 { fails = fails + 1 }
118 let a: i64 = nx_zstd_bits_peek(pb, 4)
119 if nx_zstd_bits_remaining(pb) != 10 { fails = fails + 1 }
120 let b: i64 = nx_zstd_bits_peek(pb, 4)
121 if a != b { fails = fails + 1 }
122 nx_zstd_bits_skip(pb, 3)
123 if nx_zstd_bits_remaining(pb) != 7 { fails = fails + 1 }
124 }
125 if fails > 0 { if mark == 0 { mark = 4 } }
126
127 // ---- T5: decode a hand-assembled stream -> symbols 2, 3, 0, 4 ----
128 // bits emitted in read order: 0 | 10 | 110 | 1111
129 // placed so the sentinel sits at absolute bit 10 (byte1 bit 2 = 0x05)
130 let sd: *u8 = sys_mmap(64)
131 sd[0] = 0x6f as u8; sd[1] = 0x05 as u8
132 let sb: *NxZstdBits = nx_zstd_bits_init(sd, 2)
133 if sb == (0 as *NxZstdBits) { fails = fails + 1 } else {
134 if nx_zstd_huf_decode(t, sb) != 2 { fails = fails + 1 }
135 if nx_zstd_bits_remaining(sb) != 9 { fails = fails + 1 }
136 if nx_zstd_huf_decode(t, sb) != 3 { fails = fails + 1 }
137 if nx_zstd_bits_remaining(sb) != 7 { fails = fails + 1 }
138 if nx_zstd_huf_decode(t, sb) != 0 { fails = fails + 1 }
139 if nx_zstd_bits_remaining(sb) != 4 { fails = fails + 1 }
140 if nx_zstd_huf_decode(t, sb) != 4 { fails = fails + 1 }
141 if nx_zstd_bits_remaining(sb) != 0 { fails = fails + 1 }
142 }
143 if fails > 0 { if mark == 0 { mark = 5 } }
144
145 // ---- T6: a two-symbol table, the degenerate but legal case ----
146 w[0] = 1; w[1] = 1
147 let t2: *NxZstdHuf = nx_zstd_huf_build(w, 2, 1)
148 if t2 == (0 as *NxZstdHuf) { fails = fails + 1 } else {
149 if t2.table_size != 2 { fails = fails + 1 }
150 if nx_zstd_huf_symbol_at(t2, 0) != 0 { fails = fails + 1 }
151 if nx_zstd_huf_symbol_at(t2, 1) != 1 { fails = fails + 1 }
152 if nx_zstd_huf_nbits_at(t2, 0) != 1 { fails = fails + 1 }
153 }
154 if fails > 0 { if mark == 0 { mark = 6 } }
155
156 // ---- T7 NEG: the slots must TILE EXACTLY ----
157 // {2,1,4,3} without the inferred last weight sums to 15 of 16 -> REFUSED
158 w[0] = 2; w[1] = 1; w[2] = 4; w[3] = 3
159 if nx_zstd_huf_build(w, 4, 4) != (0 as *NxZstdHuf) { fails = fails + 1 }
160 // over-tiling is refused too
161 w[0] = 4; w[1] = 4; w[2] = 4
162 if nx_zstd_huf_build(w, 3, 4) != (0 as *NxZstdHuf) { fails = fails + 1 }
163 // a weight larger than the table log cannot be represented
164 w[0] = 5; w[1] = 1
165 if nx_zstd_huf_build(w, 2, 4) != (0 as *NxZstdHuf) { fails = fails + 1 }
166 // bad table logs and counts
167 w[0] = 1; w[1] = 1
168 if nx_zstd_huf_build(w, 2, 0) != (0 as *NxZstdHuf) { fails = fails + 1 }
169 if nx_zstd_huf_build(w, 2, 13) != (0 as *NxZstdHuf) { fails = fails + 1 }
170 if nx_zstd_huf_build(w, 0, 4) != (0 as *NxZstdHuf) { fails = fails + 1 }
171 // decoding through a null table reports -1 rather than a plausible symbol
172 if nx_zstd_huf_decode(0 as *NxZstdHuf, sb) != (0 - 1) { fails = fails + 1 }
173 if fails > 0 { if mark == 0 { mark = 7 } }
174
175 if fails == 0 {
176 g_puts("GATE nx_zstd_huf verdict=GREEN pass=7/7 (table builds at log 4; EXACT layout asserted index by index -- heaviest weight at the LOWEST indices, 0-7 sym2/1bit, 8-11 sym3/2bit, 12-13 sym0/3bit, 14 sym1, 15 sym4; every symbol holds exactly 2^(w-1) slots and every entry is written; peek does NOT move the cursor, skip does; hand-assembled backward stream decodes to 2,3,0,4 across FOUR different code lengths so a fixed-width consumer fails at the second symbol; degenerate 2-symbol table; NEG under-tiling 15-of-16 and over-tiling and weight>log and bad log/count and null table all refused)\n" as *u8)
177 sys_exit(0)
178 return 0
179 }
180 g_puts("GATE nx_zstd_huf verdict=RED fails=" as *u8)
181 g_putn(fails)
182 g_puts(" first_stage=" as *u8)
183 g_putn(mark)
184 g_puts("\n" as *u8)
185 sys_exit(1)
186 return 1
187}