nx_zstd_lit_gate.nx source
↩ module page · 193 lines · 9040 B
1// nx_zstd_lit_gate.nx -- proves the zstd literals section.
2//
3// T2 pins the NON-BYTE-ALIGNED size fields. Two bits of block type and two of
4// size format share byte 0 with the TOP of the regenerated size, so every size
5// read starts at bit 4 and runs on little-endian. Reading whole bytes instead
6// yields a value wrong by a factor of 16 -- loud on a large block, silent on a
7// small one. The test uses hand-built headers at every size format and
8// asserts the decoded size exactly.
9//
10// T3 pins the DOUBLE MEANING of the format field. For Raw and RLE, formats 0
11// and 2 are the SAME one-byte form. For Compressed and Treeless the same two
12// values mean different things -- 0 is ONE stream, 1 is FOUR, both with 10-bit
13// sizes. One field, two interpretations, decided by the block type.
14//
15// T5 decodes Huffman literals end-to-end through the table built by
16// nx_zstd_huf: header -> table -> backward stream -> literal bytes. It reuses
17// the hand-assembled stream whose symbol sequence is derived in the huf gate,
18// so the expected output is known independently of this code.
19//
20// license_tier: ORIGINAL
21import "nx_syscalls.nx"
22import "nx_zstd_bits.nx"
23import "nx_zstd_huf.nx"
24import "nx_zstd_lit.nx"
25
26func g_puts(s: *u8) -> i64 {
27 var i: i64 = 0
28 while s[i] != (0 as u8) { i = i + 1 }
29 sys_write(1, s, i)
30 return i
31}
32
33func g_putn(v: i64) -> i64 {
34 let buf: *u8 = sys_mmap(32)
35 var x: i64 = v
36 if x < 0 { g_puts("-" as *u8); x = 0 - x }
37 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
38 let tmp: *u8 = sys_mmap(32)
39 var d: i64 = 0
40 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
41 var i: i64 = 0
42 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
43 sys_write(1, buf, d)
44 return d
45}
46
47func main() -> i64 {
48 var fails: i64 = 0
49 var mark: i64 = 0
50 var i: i64 = 0
51
52 let d: *u8 = sys_mmap(4096)
53 let out: *u8 = sys_mmap(4096)
54 let fld: *i64 = sys_mmap(128) as *i64
55
56 // ---- T1: the one-byte Raw header, 5-bit size ----
57 // type 0, format 0, regenerated size 20 -> byte = 0 | (20 << 3) = 0xA0
58 if nx_zstd_lit_header_write(d, 4096, 0, NX_LIT_RAW, 20) != 1 { fails = fails + 1 }
59 if (d[0] as i64 & 255) != 0xa0 { fails = fails + 1 }
60 i = 0
61 while i < 20 { d[1 + i] = ((i * 7 + 3) & 255) as u8; i = i + 1 }
62 if nx_zstd_lit_header(d, 4096, 0, fld) != 1 { fails = fails + 1 } else {
63 if fld[NX_LIT_FLD_TYPE] != NX_LIT_RAW { fails = fails + 1 }
64 if fld[NX_LIT_FLD_REGEN] != 20 { fails = fails + 1 }
65 if fld[NX_LIT_FLD_HDRLEN] != 1 { fails = fails + 1 }
66 if fld[NX_LIT_FLD_STREAMS] != 1 { fails = fails + 1 }
67 }
68 if fails > 0 { if mark == 0 { mark = 1 } }
69
70 // ---- T2: sizes start at BIT 4, not at a byte boundary ----
71 // Raw, format 1: 2-byte header, 12-bit size. size 1000 = 0x3E8
72 // byte0 = type(0) | fmt(1)<<2 | (size & 15) << 4 ; byte1 = size >> 4
73 d[0] = ((1 << 2) | ((1000 & 15) << 4)) as u8
74 d[1] = ((1000 >> 4) & 255) as u8
75 if nx_zstd_lit_header(d, 4096, 0, fld) != 1 { fails = fails + 1 } else {
76 if fld[NX_LIT_FLD_REGEN] != 1000 { fails = fails + 1 }
77 if fld[NX_LIT_FLD_HDRLEN] != 2 { fails = fails + 1 }
78 }
79 // Raw, format 3: 3-byte header, 20-bit size. size 100000
80 d[0] = ((3 << 2) | ((100000 & 15) << 4)) as u8
81 d[1] = ((100000 >> 4) & 255) as u8
82 d[2] = ((100000 >> 12) & 255) as u8
83 if nx_zstd_lit_header(d, 200000, 0, fld) != 1 { fails = fails + 1 } else {
84 if fld[NX_LIT_FLD_REGEN] != 100000 { fails = fails + 1 }
85 if fld[NX_LIT_FLD_HDRLEN] != 3 { fails = fails + 1 }
86 }
87 if fails > 0 { if mark == 0 { mark = 2 } }
88
89 // ---- T3: the format field means DIFFERENT things per block type ----
90 // Raw with format 2 is the SAME one-byte form as format 0
91 d[0] = ((NX_LIT_RAW) | (2 << 2) | (7 << 3)) as u8
92 if nx_zstd_lit_header(d, 4096, 0, fld) != 1 { fails = fails + 1 } else {
93 if fld[NX_LIT_FLD_HDRLEN] != 1 { fails = fails + 1 }
94 }
95 // Compressed format 0 -> ONE stream, 10-bit sizes, 3-byte header
96 // regen 300, comp 200 -> v = 300 | (200 << 10) = 300 + 204800 = 205100
97 d[0] = ((NX_LIT_COMP) | (0 << 2) | ((205100 & 15) << 4)) as u8
98 d[1] = ((205100 >> 4) & 255) as u8
99 d[2] = ((205100 >> 12) & 255) as u8
100 if nx_zstd_lit_header(d, 4096, 0, fld) != 1 { fails = fails + 1 } else {
101 if fld[NX_LIT_FLD_REGEN] != 300 { fails = fails + 1 }
102 if fld[NX_LIT_FLD_COMPSIZE] != 200 { fails = fails + 1 }
103 if fld[NX_LIT_FLD_STREAMS] != 1 { fails = fails + 1 }
104 if fld[NX_LIT_FLD_HDRLEN] != 3 { fails = fails + 1 }
105 }
106 // Compressed format 1 -> the SAME sizes but FOUR streams
107 d[0] = ((NX_LIT_COMP) | (1 << 2) | ((205100 & 15) << 4)) as u8
108 if nx_zstd_lit_header(d, 4096, 0, fld) != 1 { fails = fails + 1 } else {
109 if fld[NX_LIT_FLD_REGEN] != 300 { fails = fails + 1 }
110 if fld[NX_LIT_FLD_STREAMS] != 4 { fails = fails + 1 }
111 }
112 if fails > 0 { if mark == 0 { mark = 3 } }
113
114 // ---- T4: raw and RLE payloads ----
115 let src: *u8 = sys_mmap(1024)
116 i = 0
117 while i < 64 { src[i] = ((i * 11 + 5) & 255) as u8; i = i + 1 }
118 if nx_zstd_lit_raw(src, 64, 0, 64, out, 4096) != 64 { fails = fails + 1 } else {
119 var bad: i64 = 0
120 i = 0
121 while i < 64 {
122 if (out[i] as i64 & 255) != (src[i] as i64 & 255) { bad = bad + 1 }
123 i = i + 1
124 }
125 if bad != 0 { fails = fails + 1 }
126 }
127 let one: *u8 = sys_mmap(64)
128 one[0] = 0x5a as u8
129 if nx_zstd_lit_rle(one, 1, 0, 300, out, 4096) != 300 { fails = fails + 1 } else {
130 var bad2: i64 = 0
131 i = 0
132 while i < 300 {
133 if (out[i] as i64 & 255) != 0x5a { bad2 = bad2 + 1 }
134 i = i + 1
135 }
136 if bad2 != 0 { fails = fails + 1 }
137 }
138 if fails > 0 { if mark == 0 { mark = 4 } }
139
140 // ---- T5: Huffman literals, end to end through the built table ----
141 // the same weight set and stream proven in the huf gate: the stream
142 // decodes to symbols 2, 3, 0, 4
143 let w: *i64 = sys_mmap(512 * 8) as *i64
144 w[0] = 2; w[1] = 1; w[2] = 4; w[3] = 3; w[4] = 1
145 let t: *NxZstdHuf = nx_zstd_huf_build(w, 5, 4)
146 if t == (0 as *NxZstdHuf) { fails = fails + 1 } else {
147 let sd: *u8 = sys_mmap(64)
148 sd[0] = 0x6f as u8; sd[1] = 0x05 as u8
149 if nx_zstd_lit_huf(t, sd, 2, 0, 2, 4, out, 4096) != 4 { fails = fails + 1 } else {
150 if (out[0] as i64 & 255) != 2 { fails = fails + 1 }
151 if (out[1] as i64 & 255) != 3 { fails = fails + 1 }
152 if (out[2] as i64 & 255) != 0 { fails = fails + 1 }
153 if (out[3] as i64 & 255) != 4 { fails = fails + 1 }
154 }
155 // asking for MORE literals than the stream holds must REFUSE, not
156 // return a partial buffer the caller cannot distinguish from a full one
157 if nx_zstd_lit_huf(t, sd, 2, 0, 2, 40, out, 4096) != (0 - 1) { fails = fails + 1 }
158 }
159 if fails > 0 { if mark == 0 { mark = 5 } }
160
161 // ---- T6 NEG: refusals ----
162 // a header whose declared payload runs past the buffer
163 d[0] = ((NX_LIT_RAW) | (31 << 3)) as u8
164 if nx_zstd_lit_header(d, 4, 0, fld) != 0 { fails = fails + 1 }
165 // a 2-byte header with only one byte available
166 d[0] = (1 << 2) as u8
167 if nx_zstd_lit_header(d, 1, 0, fld) != 0 { fails = fails + 1 }
168 // an offset at or past the end
169 if nx_zstd_lit_header(d, 10, 10, fld) != 0 { fails = fails + 1 }
170 // raw and RLE payload bounds
171 if nx_zstd_lit_raw(src, 64, 0, 100, out, 4096) != (0 - 1) { fails = fails + 1 }
172 if nx_zstd_lit_raw(src, 64, 0, 64, out, 10) != (0 - 1) { fails = fails + 1 }
173 if nx_zstd_lit_rle(one, 1, 0, 300, out, 10) != (0 - 1) { fails = fails + 1 }
174 // a null Huffman table
175 if nx_zstd_lit_huf(0 as *NxZstdHuf, src, 64, 0, 8, 4, out, 4096) != (0 - 1) { fails = fails + 1 }
176 // the writer refuses sizes the one-byte form cannot hold
177 if nx_zstd_lit_header_write(d, 4096, 0, NX_LIT_RAW, 32) != 0 { fails = fails + 1 }
178 if nx_zstd_lit_header_write(d, 4096, 0, NX_LIT_COMP, 10) != 0 { fails = fails + 1 }
179 if fails > 0 { if mark == 0 { mark = 6 } }
180
181 if fails == 0 {
182 g_puts("GATE nx_zstd_lit verdict=GREEN pass=6/6 (one-byte Raw header 5-bit size; sizes start at BIT 4 not a byte boundary -- 12-bit 1000 and 20-bit 100000 decoded exactly; the format field means DIFFERENT things per block type -- Raw fmt 2 is the one-byte form while Compressed fmt 0 is ONE stream and fmt 1 is FOUR with the same 10-bit sizes; raw and RLE payloads byte-exact; HUFFMAN LITERALS END-TO-END header->table->backward stream->bytes 2,3,0,4 and an over-long request REFUSED rather than returning a partial buffer; NEG payload-past-buffer/short-header/bad-offset/bounds/null-table/unencodable-size refused)\n" as *u8)
183 sys_exit(0)
184 return 0
185 }
186 g_puts("GATE nx_zstd_lit verdict=RED fails=" as *u8)
187 g_putn(fails)
188 g_puts(" first_stage=" as *u8)
189 g_putn(mark)
190 g_puts("\n" as *u8)
191 sys_exit(1)
192 return 1
193}