nx_zstd_seq_gate.nx source
↩ module page · 235 lines · 10958 B
1// nx_zstd_seq_gate.nx -- proves zstd sequence execution and code tables.
2//
3// T4 is the one that matters. An offset SMALLER than the match length is legal
4// and common -- it is how zstd encodes runs -- and the copy is REQUIRED to
5// read bytes it wrote moments earlier in the same operation. The test uses
6// offset 3 with match length 4 (the fourth byte read is one this copy just
7// wrote) and offset 1 with match length 5 (a pure run). A bulk move that
8// snapshots the source region gives the right answer for the first `offset`
9// bytes and garbage after, so both cases are needed: the offset-1 run fails
10// loudly, the offset-3 overlap fails on exactly one byte.
11//
12// T1 pins the DISCONTINUOUS sequence count: the byte itself below 128, a
13// two-byte form below 255, and an escape to three bytes at exactly 255 biased
14// by 0x7F00. A plain varint reading mis-sizes the header and every table
15// after it.
16//
17// T2/T3 pin the code tables, including that match lengths start at THREE and
18// that the literal-length baselines are the value itself only up to 15.
19//
20// license_tier: ORIGINAL
21import "nx_syscalls.nx"
22import "nx_zstd_seq.nx"
23
24func g_puts(s: *u8) -> i64 {
25 var i: i64 = 0
26 while s[i] != (0 as u8) { i = i + 1 }
27 sys_write(1, s, i)
28 return i
29}
30
31func g_putn(v: i64) -> i64 {
32 let buf: *u8 = sys_mmap(32)
33 var x: i64 = v
34 if x < 0 { g_puts("-" as *u8); x = 0 - x }
35 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
36 let tmp: *u8 = sys_mmap(32)
37 var d: i64 = 0
38 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
39 var i: i64 = 0
40 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
41 sys_write(1, buf, d)
42 return d
43}
44
45func main() -> i64 {
46 var fails: i64 = 0
47 var mark: i64 = 0
48 var i: i64 = 0
49
50 let d: *u8 = sys_mmap(256)
51 let fld: *i64 = sys_mmap(128) as *i64
52
53 // ---- T1: the DISCONTINUOUS sequence count ----
54 // zero sequences: one byte, and NO mode byte follows
55 d[0] = 0 as u8
56 if nx_zstd_seq_header(d, 4, 0, fld) != 1 { fails = fails + 1 } else {
57 if fld[NX_SEQ_FLD_COUNT] != 0 { fails = fails + 1 }
58 if fld[NX_SEQ_FLD_HDRLEN] != 1 { fails = fails + 1 }
59 }
60 // below 128: the byte itself, then a mode byte
61 d[0] = 100 as u8
62 d[1] = 0x00 as u8
63 if nx_zstd_seq_header(d, 4, 0, fld) != 1 { fails = fails + 1 } else {
64 if fld[NX_SEQ_FLD_COUNT] != 100 { fails = fails + 1 }
65 if fld[NX_SEQ_FLD_HDRLEN] != 2 { fails = fails + 1 }
66 }
67 // 128..254: two bytes, ((b0-128) << 8) + b1
68 d[0] = 130 as u8
69 d[1] = 50 as u8
70 d[2] = 0x00 as u8
71 if nx_zstd_seq_header(d, 4, 0, fld) != 1 { fails = fails + 1 } else {
72 if fld[NX_SEQ_FLD_COUNT] != 562 { fails = fails + 1 }
73 if fld[NX_SEQ_FLD_HDRLEN] != 3 { fails = fails + 1 }
74 }
75 // exactly 255: escape to three bytes, biased by 0x7F00
76 d[0] = 255 as u8
77 d[1] = 0x10 as u8
78 d[2] = 0x01 as u8
79 d[3] = 0x00 as u8
80 if nx_zstd_seq_header(d, 5, 0, fld) != 1 { fails = fails + 1 } else {
81 // 0x10 + (0x01 << 8) + 32512 = 16 + 256 + 32512 = 32784
82 if fld[NX_SEQ_FLD_COUNT] != 32784 { fails = fails + 1 }
83 if fld[NX_SEQ_FLD_HDRLEN] != 4 { fails = fails + 1 }
84 }
85 if fails > 0 { if mark == 0 { mark = 1 } }
86
87 // ---- T2: the compression-mode field and its reserved bits ----
88 d[0] = 10 as u8
89 // ll=2 (FSE), of=1 (RLE), ml=3 (Repeat), reserved 0
90 d[1] = ((2 << 6) | (1 << 4) | (3 << 2)) as u8
91 if nx_zstd_seq_header(d, 4, 0, fld) != 1 { fails = fails + 1 } else {
92 if fld[NX_SEQ_FLD_LLMODE] != NX_SEQ_MODE_FSE { fails = fails + 1 }
93 if fld[NX_SEQ_FLD_OFMODE] != NX_SEQ_MODE_RLE { fails = fails + 1 }
94 if fld[NX_SEQ_FLD_MLMODE] != NX_SEQ_MODE_REPEAT { fails = fails + 1 }
95 }
96 // the low two bits are reserved: a non-zero value must be REFUSED
97 d[1] = ((2 << 6) | 1) as u8
98 if nx_zstd_seq_header(d, 4, 0, fld) != 0 { fails = fails + 1 }
99 if fails > 0 { if mark == 0 { mark = 2 } }
100
101 // ---- T3: the code tables ----
102 // literal lengths: the value itself up to 15, then the table jumps
103 if nx_zstd_ll_base(0) != 0 { fails = fails + 1 }
104 if nx_zstd_ll_base(15) != 15 { fails = fails + 1 }
105 if nx_zstd_ll_extra(15) != 0 { fails = fails + 1 }
106 if nx_zstd_ll_base(16) != 16 { fails = fails + 1 }
107 if nx_zstd_ll_extra(16) != 1 { fails = fails + 1 }
108 if nx_zstd_ll_base(24) != 48 { fails = fails + 1 }
109 if nx_zstd_ll_extra(24) != 4 { fails = fails + 1 }
110 if nx_zstd_ll_base(35) != 65536 { fails = fails + 1 }
111 if nx_zstd_ll_extra(35) != 16 { fails = fails + 1 }
112 if nx_zstd_ll_base(36) != (0 - 1) { fails = fails + 1 }
113 // match lengths start at THREE, not zero
114 if nx_zstd_ml_base(0) != 3 { fails = fails + 1 }
115 if nx_zstd_ml_base(31) != 34 { fails = fails + 1 }
116 if nx_zstd_ml_extra(31) != 0 { fails = fails + 1 }
117 if nx_zstd_ml_base(32) != 35 { fails = fails + 1 }
118 if nx_zstd_ml_extra(32) != 1 { fails = fails + 1 }
119 if nx_zstd_ml_base(52) != 65539 { fails = fails + 1 }
120 if nx_zstd_ml_extra(52) != 16 { fails = fails + 1 }
121 if nx_zstd_ml_base(53) != (0 - 1) { fails = fails + 1 }
122 // offsets: baseline 2^N with N extra bits
123 if nx_zstd_of_base(0) != 1 { fails = fails + 1 }
124 if nx_zstd_of_base(5) != 32 { fails = fails + 1 }
125 if nx_zstd_of_extra(5) != 5 { fails = fails + 1 }
126 if nx_zstd_of_base(32) != (0 - 1) { fails = fails + 1 }
127 if fails > 0 { if mark == 0 { mark = 3 } }
128
129 // ---- T4: THE OVERLAPPING MATCH COPY ----
130 let lit: *u8 = sys_mmap(256)
131 let out: *u8 = sys_mmap(4096)
132 let seqs: *i64 = sys_mmap(256 * 8) as *i64
133
134 // literals "abcdef"; one sequence ll=3 ml=4 off=3
135 lit[0] = 0x61 as u8; lit[1] = 0x62 as u8; lit[2] = 0x63 as u8
136 lit[3] = 0x64 as u8; lit[4] = 0x65 as u8; lit[5] = 0x66 as u8
137 seqs[0] = 3; seqs[1] = 4; seqs[2] = 3
138 let got: i64 = nx_zstd_seq_execute(lit, 6, seqs, 1, out, 4096)
139 // "abc" + match from offset 3 for 4 bytes = a,b,c,a (the 4th reads a byte
140 // this very copy wrote) + tail literals "def" -> "abcabcadef", 10 bytes
141 if got != 10 { fails = fails + 1 } else {
142 if (out[0] as i64 & 255) != 0x61 { fails = fails + 1 }
143 if (out[1] as i64 & 255) != 0x62 { fails = fails + 1 }
144 if (out[2] as i64 & 255) != 0x63 { fails = fails + 1 }
145 if (out[3] as i64 & 255) != 0x61 { fails = fails + 1 }
146 if (out[4] as i64 & 255) != 0x62 { fails = fails + 1 }
147 if (out[5] as i64 & 255) != 0x63 { fails = fails + 1 }
148 // THE overlap byte: reads out[3], written earlier in this same copy
149 if (out[6] as i64 & 255) != 0x61 { fails = fails + 1 }
150 if (out[7] as i64 & 255) != 0x64 { fails = fails + 1 }
151 if (out[8] as i64 & 255) != 0x65 { fails = fails + 1 }
152 if (out[9] as i64 & 255) != 0x66 { fails = fails + 1 }
153 }
154
155 // offset 1 with match length 5 is a pure RUN -- a bulk move gives one byte
156 lit[0] = 0x78 as u8
157 seqs[0] = 1; seqs[1] = 5; seqs[2] = 1
158 let run: i64 = nx_zstd_seq_execute(lit, 1, seqs, 1, out, 4096)
159 if run != 6 { fails = fails + 1 } else {
160 var bad: i64 = 0
161 i = 0
162 while i < 6 {
163 if (out[i] as i64 & 255) != 0x78 { bad = bad + 1 }
164 i = i + 1
165 }
166 if bad != 0 { fails = fails + 1 }
167 }
168 if fails > 0 { if mark == 0 { mark = 4 } }
169
170 // ---- T5: multiple sequences, and the literal tail ----
171 i = 0
172 while i < 20 { lit[i] = (0x41 + i) as u8; i = i + 1 }
173 // seq1: 4 literals, match 3 at offset 4 ; seq2: 2 literals, match 6 at offset 2
174 seqs[0] = 4; seqs[1] = 3; seqs[2] = 4
175 seqs[3] = 2; seqs[4] = 6; seqs[5] = 2
176 let m: i64 = nx_zstd_seq_execute(lit, 20, seqs, 2, out, 4096)
177 // 4 + 3 + 2 + 6 + 14 remaining literals = 29
178 if m != 29 { fails = fails + 1 } else {
179 // ABCD then match offset 4 -> ABC
180 if (out[0] as i64 & 255) != 0x41 { fails = fails + 1 }
181 if (out[4] as i64 & 255) != 0x41 { fails = fails + 1 }
182 if (out[5] as i64 & 255) != 0x42 { fails = fails + 1 }
183 if (out[6] as i64 & 255) != 0x43 { fails = fails + 1 }
184 // then literals E,F at 7,8
185 if (out[7] as i64 & 255) != 0x45 { fails = fails + 1 }
186 if (out[8] as i64 & 255) != 0x46 { fails = fails + 1 }
187 // then match offset 2 length 6 -> E,F,E,F,E,F
188 if (out[9] as i64 & 255) != 0x45 { fails = fails + 1 }
189 if (out[10] as i64 & 255) != 0x46 { fails = fails + 1 }
190 if (out[11] as i64 & 255) != 0x45 { fails = fails + 1 }
191 if (out[14] as i64 & 255) != 0x46 { fails = fails + 1 }
192 // the tail literals resume at G
193 if (out[15] as i64 & 255) != 0x47 { fails = fails + 1 }
194 }
195 if fails > 0 { if mark == 0 { mark = 5 } }
196
197 // ---- T6: zero sequences means the literals ARE the output ----
198 let z: i64 = nx_zstd_seq_execute(lit, 20, seqs, 0, out, 4096)
199 if z != 20 { fails = fails + 1 } else {
200 if (out[0] as i64 & 255) != 0x41 { fails = fails + 1 }
201 if (out[19] as i64 & 255) != 0x54 { fails = fails + 1 }
202 }
203 if fails > 0 { if mark == 0 { mark = 6 } }
204
205 // ---- T7 NEG: refusals ----
206 // an offset reaching before the START of the output
207 seqs[0] = 2; seqs[1] = 4; seqs[2] = 10
208 if nx_zstd_seq_execute(lit, 20, seqs, 1, out, 4096) != (0 - 1) { fails = fails + 1 }
209 // an offset of zero is never valid
210 seqs[0] = 2; seqs[1] = 4; seqs[2] = 0
211 if nx_zstd_seq_execute(lit, 20, seqs, 1, out, 4096) != (0 - 1) { fails = fails + 1 }
212 // a literal run longer than the literals available
213 seqs[0] = 50; seqs[1] = 3; seqs[2] = 1
214 if nx_zstd_seq_execute(lit, 20, seqs, 1, out, 4096) != (0 - 1) { fails = fails + 1 }
215 // an output buffer too small
216 seqs[0] = 4; seqs[1] = 3; seqs[2] = 4
217 if nx_zstd_seq_execute(lit, 20, seqs, 1, out, 5) != (0 - 1) { fails = fails + 1 }
218 // a header whose count field runs past the buffer
219 d[0] = 200 as u8
220 if nx_zstd_seq_header(d, 1, 0, fld) != 0 { fails = fails + 1 }
221 if fails > 0 { if mark == 0 { mark = 7 } }
222
223 if fails == 0 {
224 g_puts("GATE nx_zstd_seq verdict=GREEN pass=7/7 (DISCONTINUOUS count -- 0 with no mode byte, byte-itself below 128, two-byte below 255, three-byte escape at 255 biased 0x7F00; mode field with reserved bits ENFORCED; LL baselines value-itself only to 15 then jumping, ML starting at THREE, offsets 2^N; OVERLAPPING MATCH COPY proven twice -- offset 3 length 4 reads a byte this copy just wrote, offset 1 length 5 is a pure run a bulk move cannot produce; two sequences plus literal tail = 29 bytes exact; zero sequences yields the literals verbatim; NEG offset-before-start/offset-zero/over-long-literal-run/small-output/short-header refused)\n" as *u8)
225 sys_exit(0)
226 return 0
227 }
228 g_puts("GATE nx_zstd_seq verdict=RED fails=" as *u8)
229 g_putn(fails)
230 g_puts(" first_stage=" as *u8)
231 g_putn(mark)
232 g_puts("\n" as *u8)
233 sys_exit(1)
234 return 1
235}