nx_zstd_block_gate.nx source
↩ module page · 204 lines · 9519 B
1// nx_zstd_block_gate.nx -- proves zstd compressed-block decompression.
2//
3// T3 is the payoff: a complete Compressed block with HUFFMAN-CODED literals,
4// assembled byte by byte -- literals header, Huffman tree description, coded
5// stream, sequences header -- decompressed to its exact bytes. Every layer
6// below is exercised in one call: header parsing, weight decoding, weight
7// completion, table build, backward reading, symbol decode.
8//
9// T5 pins the DISTINCT refusal codes. A block carrying sequences must NOT
10// quietly emit its literals: that produces output of the right LENGTH and the
11// wrong BYTES, which a length check passes. FSE sequences, FSE weights and
12// four-stream literals each get their own code so a caller can tell
13// 'unsupported' from 'corrupt' from 'wrong shape'.
14//
15// T4 pins that the tree description lives INSIDE compressed_size. Treating
16// compressed_size as the stream alone over-reads by the description length
17// and desynchronises the sequences section that follows -- which is why the
18// sequences byte is asserted to land where it does.
19//
20// license_tier: ORIGINAL
21import "nx_syscalls.nx"
22import "nx_zstd_fse.nx"
23import "nx_zstd_bits.nx"
24import "nx_zstd_huf.nx"
25import "nx_zstd_lit.nx"
26import "nx_zstd_seq.nx"
27import "nx_zstd_fse_dec.nx"
28import "nx_zstd_seqtab.nx"
29import "nx_zstd_seqdec.nx"
30import "nx_zstd_block.nx"
31
32func g_puts(s: *u8) -> i64 {
33 var i: i64 = 0
34 while s[i] != (0 as u8) { i = i + 1 }
35 sys_write(1, s, i)
36 return i
37}
38
39func g_putn(v: i64) -> i64 {
40 let buf: *u8 = sys_mmap(32)
41 var x: i64 = v
42 if x < 0 { g_puts("-" as *u8); x = 0 - x }
43 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
44 let tmp: *u8 = sys_mmap(32)
45 var d: i64 = 0
46 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
47 var i: i64 = 0
48 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
49 sys_write(1, buf, d)
50 return d
51}
52
53func main() -> i64 {
54 var fails: i64 = 0
55 var mark: i64 = 0
56 var i: i64 = 0
57
58 let blk: *u8 = sys_mmap(4096)
59 let out: *u8 = sys_mmap(4096)
60
61 // ---- T1: RAW literals, zero sequences ----
62 // byte0 = type 0 | regen 20 << 3 = 0xA0 ; 20 literals ; then nbSeq = 0
63 blk[0] = 0xa0 as u8
64 i = 0
65 while i < 20 { blk[1 + i] = ((i * 7 + 3) & 255) as u8; i = i + 1 }
66 blk[21] = 0x00 as u8
67 let g1: i64 = nx_zstd_block_decompress(blk, 22, out, 4096)
68 if g1 != 20 { fails = fails + 1 } else {
69 var bad: i64 = 0
70 i = 0
71 while i < 20 {
72 if (out[i] as i64 & 255) != ((i * 7 + 3) & 255) { bad = bad + 1 }
73 i = i + 1
74 }
75 if bad != 0 { fails = fails + 1 }
76 }
77 if fails > 0 { if mark == 0 { mark = 1 } }
78
79 // ---- T2: RLE literals, zero sequences ----
80 // byte0 = type 1 | regen 25 << 3 = 0xC9 ; one byte ; then nbSeq = 0
81 blk[0] = 0xc9 as u8
82 blk[1] = 0x5a as u8
83 blk[2] = 0x00 as u8
84 let g2: i64 = nx_zstd_block_decompress(blk, 3, out, 4096)
85 if g2 != 25 { fails = fails + 1 } else {
86 var bad2: i64 = 0
87 i = 0
88 while i < 25 {
89 if (out[i] as i64 & 255) != 0x5a { bad2 = bad2 + 1 }
90 i = i + 1
91 }
92 if bad2 != 0 { fails = fails + 1 }
93 }
94 if fails > 0 { if mark == 0 { mark = 2 } }
95
96 // ---- T3: a COMPRESSED block with HUFFMAN literals, end to end ----
97 // literals header, format 0 (one stream, 10-bit sizes, 3 bytes):
98 // regen 4, compressed 5 -> v = 4 | (5 << 10) = 5124
99 blk[0] = ((NX_LIT_COMP) | ((5124 & 15) << 4)) as u8 // 0x42
100 blk[1] = ((5124 >> 4) & 255) as u8 // 0x40
101 blk[2] = ((5124 >> 12) & 255) as u8 // 0x01
102 // tree description: header 3 means FOUR stored weights {2,1,4,3},
103 // packed high nibble first; the fifth weight (1) is INFERRED
104 blk[3] = 0x03 as u8
105 blk[4] = 0x21 as u8
106 blk[5] = 0x43 as u8
107 // the coded stream, proven in the huf gate to decode to symbols 2,3,0,4
108 blk[6] = 0x6f as u8
109 blk[7] = 0x05 as u8
110 // sequences header: zero sequences
111 blk[8] = 0x00 as u8
112
113 let g3: i64 = nx_zstd_block_decompress(blk, 9, out, 4096)
114 if g3 != 4 { fails = fails + 1 } else {
115 if (out[0] as i64 & 255) != 2 { fails = fails + 1 }
116 if (out[1] as i64 & 255) != 3 { fails = fails + 1 }
117 if (out[2] as i64 & 255) != 0 { fails = fails + 1 }
118 if (out[3] as i64 & 255) != 4 { fails = fails + 1 }
119 }
120 if fails > 0 { if mark == 0 { mark = 3 } }
121
122 // ---- T4: the tree description is INSIDE compressed_size ----
123 // it is 3 bytes (1 header + 2 packed weights), so the stream is 5-3 = 2,
124 // and the sequences byte therefore lands at offset 3 + 5 = 8. If the
125 // decoder treated compressed_size as the stream alone it would look for
126 // sequences at offset 11 -- past the block -- and fail.
127 let tslot: *i64 = sys_mmap(64) as *i64
128 if nx_zstd_block_tree(blk, 9, 3, tslot) != 3 { fails = fails + 1 }
129 if tslot[0] == 0 { fails = fails + 1 }
130 if fails > 0 { if mark == 0 { mark = 4 } }
131
132 // ---- T5: DISTINCT refusal codes, never a quiet literals-only answer ----
133 // the error codes must differ from each other
134 if NX_BLK_ERR_FSE_SEQ == NX_BLK_ERR_MALFORMED { fails = fails + 1 }
135 if NX_BLK_ERR_FSE_WEIGHTS == NX_BLK_ERR_MALFORMED { fails = fails + 1 }
136 if NX_BLK_ERR_STREAMS4 == NX_BLK_ERR_MALFORMED { fails = fails + 1 }
137 if NX_BLK_ERR_FSE_SEQ == NX_BLK_ERR_FSE_WEIGHTS { fails = fails + 1 }
138
139 // a block whose sequences use a NON-PREDEFINED mode must refuse: those
140 // carry a table description this layer does not read, and decoding them
141 // against the predefined tables would give the right length and wrong bytes
142 blk[0] = 0xa0 as u8
143 i = 0
144 while i < 20 { blk[1 + i] = 0x41 as u8; i = i + 1 }
145 blk[21] = 5 as u8
146 blk[22] = (NX_SEQ_MODE_FSE << 6) as u8 // literal lengths FSE-coded
147 blk[23] = 0x80 as u8
148 if nx_zstd_block_decompress(blk, 24, out, 4096) != NX_BLK_ERR_FSE_SEQ { fails = fails + 1 }
149 blk[22] = (NX_SEQ_MODE_RLE << 4) as u8 // offsets RLE-coded
150 if nx_zstd_block_decompress(blk, 24, out, 4096) != NX_BLK_ERR_FSE_SEQ { fails = fails + 1 }
151 blk[22] = (NX_SEQ_MODE_REPEAT << 2) as u8 // match lengths repeat
152 if nx_zstd_block_decompress(blk, 24, out, 4096) != NX_BLK_ERR_FSE_SEQ { fails = fails + 1 }
153
154 // with ALL THREE predefined the path is now WIRED -- it runs the real
155 // sequence decoder. The stream here is arbitrary bytes, so the only sound
156 // assertions are that it never crashes, never exceeds the output buffer,
157 // and either produces a bounded length or refuses. A real .zst fixture is
158 // needed to prove the bytes; that is stated rather than implied.
159 blk[22] = 0x00 as u8 // all three PREDEFINED
160 let r: i64 = nx_zstd_block_decompress(blk, 24, out, 4096)
161 if r > 4096 { fails = fails + 1 }
162 if r < NX_BLK_ERR_STREAMS4 { fails = fails + 1 }
163
164 // FSE-compressed Huffman weights get their own code
165 blk[0] = ((NX_LIT_COMP) | ((5124 & 15) << 4)) as u8
166 blk[1] = ((5124 >> 4) & 255) as u8
167 blk[2] = ((5124 >> 12) & 255) as u8
168 blk[3] = 200 as u8 // header >= 128 means FSE-coded weights
169 if nx_zstd_block_decompress(blk, 9, out, 4096) != NX_BLK_ERR_FSE_WEIGHTS { fails = fails + 1 }
170
171 // four-stream literals get their own code rather than misreading stream one
172 // format 1 = four streams, same 10-bit sizes
173 blk[0] = ((NX_LIT_COMP) | (1 << 2) | ((5124 & 15) << 4)) as u8
174 blk[3] = 0x03 as u8
175 if nx_zstd_block_decompress(blk, 9, out, 4096) != NX_BLK_ERR_STREAMS4 { fails = fails + 1 }
176 if fails > 0 { if mark == 0 { mark = 5 } }
177
178 // ---- T6 NEG: malformed blocks ----
179 // a literals header whose payload runs past the block
180 blk[0] = 0xf8 as u8 // raw, regen 31, but only a few bytes present
181 if nx_zstd_block_decompress(blk, 4, out, 4096) != NX_BLK_ERR_MALFORMED { fails = fails + 1 }
182 // an output buffer too small for the literals
183 blk[0] = 0xa0 as u8
184 i = 0
185 while i < 20 { blk[1 + i] = 0x42 as u8; i = i + 1 }
186 blk[21] = 0x00 as u8
187 if nx_zstd_block_decompress(blk, 22, out, 5) != NX_BLK_ERR_MALFORMED { fails = fails + 1 }
188 // an empty block
189 if nx_zstd_block_decompress(blk, 0, out, 4096) != NX_BLK_ERR_MALFORMED { fails = fails + 1 }
190 if fails > 0 { if mark == 0 { mark = 6 } }
191
192 if fails == 0 {
193 g_puts("GATE nx_zstd_block verdict=GREEN pass=6/6 (RAW literals block 20B exact; RLE literals block 25B exact; a COMPLETE COMPRESSED BLOCK with HUFFMAN literals assembled byte by byte -- header, tree description, coded stream, sequences header -- decompressed end to end through every layer below; the tree description proven to live INSIDE compressed_size so the sequences byte lands where the spec says; DISTINCT refusal codes for FSE-sequences, FSE-weights and four-stream literals so a sequenced block is never answered with literals-only output of the right length and wrong bytes; all three NON-PREDEFINED sequence modes refused while all-predefined runs the REAL sequence decoder bounded; NEG payload-past-block/small-output/empty refused. NOTE: the sequenced path is wired and bounded but its BYTES are not yet proven -- that needs a real .zst fixture)\n" as *u8)
194 sys_exit(0)
195 return 0
196 }
197 g_puts("GATE nx_zstd_block verdict=RED fails=" as *u8)
198 g_putn(fails)
199 g_puts(" first_stage=" as *u8)
200 g_putn(mark)
201 g_puts("\n" as *u8)
202 sys_exit(1)
203 return 1
204}