nx_zstd_seqdec_gate.nx source
↩ module page · 195 lines · 8404 B
1// nx_zstd_seqdec_gate.nx -- proves zstd's repeat-offset machine and sequence loop.
2//
3// The repeat-offset rules are pure logic with no bitstream involved, so they
4// can be proven EXHAUSTIVELY -- and they are the part of zstd most likely to
5// be subtly wrong, because the spec's behaviour is genuinely surprising:
6//
7// T2 pins the ZERO-LITERAL SLIDE. With literals the mapping is 1->rep1,
8// 2->rep2, 3->rep3. WITHOUT literals it slides: 1->rep2, 2->rep3, and
9// 3->rep1 MINUS ONE BYTE. That last case is not a repeat at all. A decoder
10// missing it is correct until the first zero-literal sequence and wrong
11// forever after -- and those are common in exactly the repetitive data zstd
12// is best at, so it fails on the files that matter.
13//
14// T3 pins that Offset_Value 1 WITH literals does NOT reorder the history,
15// while every other repeat case moves the used value to the front. Reordering
16// on that one too looks harmless and silently desynchronises from the encoder.
17//
18// T4 pins that idx 1 leaves Repeated_Offset3 untouched while idx 2 and 3
19// shift it -- the asymmetry inside the reorder itself.
20//
21// license_tier: ORIGINAL
22import "nx_syscalls.nx"
23import "nx_zstd_fse.nx"
24import "nx_zstd_bits.nx"
25import "nx_zstd_fse_dec.nx"
26import "nx_zstd_seq.nx"
27import "nx_zstd_seqtab.nx"
28import "nx_zstd_seqdec.nx"
29
30func g_puts(s: *u8) -> i64 {
31 var i: i64 = 0
32 while s[i] != (0 as u8) { i = i + 1 }
33 sys_write(1, s, i)
34 return i
35}
36
37func g_putn(v: i64) -> i64 {
38 let buf: *u8 = sys_mmap(32)
39 var x: i64 = v
40 if x < 0 { g_puts("-" as *u8); x = 0 - x }
41 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
42 let tmp: *u8 = sys_mmap(32)
43 var d: i64 = 0
44 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
45 var i: i64 = 0
46 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
47 sys_write(1, buf, d)
48 return d
49}
50
51func main() -> i64 {
52 var fails: i64 = 0
53 var mark: i64 = 0
54
55 let rep: *i64 = sys_mmap(64) as *i64
56
57 // ---- T1: the initial history is 1, 4, 8 ----
58 nx_zstd_rep_init(rep)
59 if rep[0] != 1 { fails = fails + 1 }
60 if rep[1] != 4 { fails = fails + 1 }
61 if rep[2] != 8 { fails = fails + 1 }
62
63 // a normal offset (value > 3) is value-3 and shifts the history back
64 if nx_zstd_rep_apply(rep, 103, 5) != 100 { fails = fails + 1 }
65 if rep[0] != 100 { fails = fails + 1 }
66 if rep[1] != 1 { fails = fails + 1 }
67 if rep[2] != 4 { fails = fails + 1 }
68 if fails > 0 { if mark == 0 { mark = 1 } }
69
70 // ---- T2: THE ZERO-LITERAL SLIDE ----
71 // with literals: 1->rep1, 2->rep2, 3->rep3
72 nx_zstd_rep_init(rep)
73 if nx_zstd_rep_apply(rep, 1, 7) != 1 { fails = fails + 1 }
74 nx_zstd_rep_init(rep)
75 if nx_zstd_rep_apply(rep, 2, 7) != 4 { fails = fails + 1 }
76 nx_zstd_rep_init(rep)
77 if nx_zstd_rep_apply(rep, 3, 7) != 8 { fails = fails + 1 }
78
79 // WITHOUT literals the whole mapping slides by one
80 nx_zstd_rep_init(rep)
81 if nx_zstd_rep_apply(rep, 1, 0) != 4 { fails = fails + 1 } // -> rep2
82 nx_zstd_rep_init(rep)
83 if nx_zstd_rep_apply(rep, 2, 0) != 8 { fails = fails + 1 } // -> rep3
84 nx_zstd_rep_init(rep)
85 // 3 with no literals is NOT a repeat: it is Repeated_Offset1 MINUS ONE.
86 // From the initial history rep1 is 1, so this yields 0 -- not a usable
87 // offset, and REFUSED rather than returned as a zero a caller might copy from
88 if nx_zstd_rep_apply(rep, 3, 0) != (0 - 1) { fails = fails + 1 }
89 // with a larger rep1 the minus-one is a real, usable offset
90 nx_zstd_rep_init(rep)
91 nx_zstd_rep_apply(rep, 53, 5) // rep1 becomes 50
92 if rep[0] != 50 { fails = fails + 1 }
93 if nx_zstd_rep_apply(rep, 3, 0) != 49 { fails = fails + 1 } // 50 - 1
94 if rep[0] != 49 { fails = fails + 1 }
95 if fails > 0 { if mark == 0 { mark = 2 } }
96
97 // ---- T3: Offset_Value 1 WITH literals does NOT reorder ----
98 nx_zstd_rep_init(rep)
99 if nx_zstd_rep_apply(rep, 1, 9) != 1 { fails = fails + 1 }
100 if rep[0] != 1 { fails = fails + 1 }
101 if rep[1] != 4 { fails = fails + 1 }
102 if rep[2] != 8 { fails = fails + 1 }
103
104 // ...whereas Offset_Value 2 DOES move the used value to the front
105 nx_zstd_rep_init(rep)
106 if nx_zstd_rep_apply(rep, 2, 9) != 4 { fails = fails + 1 }
107 if rep[0] != 4 { fails = fails + 1 }
108 if rep[1] != 1 { fails = fails + 1 }
109 if fails > 0 { if mark == 0 { mark = 3 } }
110
111 // ---- T4: the asymmetry INSIDE the reorder ----
112 // idx 1 leaves Repeated_Offset3 alone
113 nx_zstd_rep_init(rep)
114 nx_zstd_rep_apply(rep, 2, 9)
115 if rep[2] != 8 { fails = fails + 1 }
116 // idx 2 shifts Repeated_Offset3
117 nx_zstd_rep_init(rep)
118 if nx_zstd_rep_apply(rep, 3, 9) != 8 { fails = fails + 1 }
119 if rep[0] != 8 { fails = fails + 1 }
120 if rep[1] != 1 { fails = fails + 1 }
121 if rep[2] != 4 { fails = fails + 1 }
122 if fails > 0 { if mark == 0 { mark = 4 } }
123
124 // ---- T5: the history stays consistent over a long mixed run ----
125 nx_zstd_rep_init(rep)
126 var seed: i64 = 31337
127 var bad: i64 = 0
128 var i: i64 = 0
129 while i < 400 {
130 seed = (seed * 1103515245 + 12345) & 0x7fffffff
131 let ov: i64 = 1 + ((seed >> 6) % 200)
132 seed = (seed * 1103515245 + 12345) & 0x7fffffff
133 let ll: i64 = (seed >> 6) % 3
134 let off: i64 = nx_zstd_rep_apply(rep, ov, ll)
135 if off > 0 {
136 // every remembered offset must stay positive and usable
137 if rep[0] < 1 { bad = bad + 1 }
138 if rep[1] < 1 { bad = bad + 1 }
139 if rep[2] < 1 { bad = bad + 1 }
140 }
141 i = i + 1
142 }
143 if bad != 0 { fails = fails + 1 }
144 if fails > 0 { if mark == 0 { mark = 5 } }
145
146 // ---- T6: the loop runs three states over one shared stream ----
147 let tll: *NxFseTable = nx_zstd_seqtab_ll_table()
148 let tml: *NxFseTable = nx_zstd_seqtab_ml_table()
149 let tof: *NxFseTable = nx_zstd_seqtab_of_table()
150 if tll == (0 as *NxFseTable) { fails = fails + 1 }
151 if tml == (0 as *NxFseTable) { fails = fails + 1 }
152 if tof == (0 as *NxFseTable) { fails = fails + 1 }
153
154 let d: *u8 = sys_mmap(256)
155 i = 0
156 while i < 64 { d[i] = ((i * 61 + 29) & 255) as u8; i = i + 1 }
157 d[63] = 0x80 as u8
158 let b: *NxZstdBits = nx_zstd_bits_init(d, 64)
159 let seqs: *i64 = sys_mmap(256 * 8) as *i64
160 if nx_zstd_seq_decode_all(tll, tml, tof, b, 3, seqs) != 1 { fails = fails + 1 } else {
161 // whatever the stream says, every decoded triple must be USABLE:
162 // non-negative lengths, a match of at least 3, a positive offset
163 var t: i64 = 0
164 while t < 3 {
165 if seqs[t * 3] < 0 { fails = fails + 1 }
166 if seqs[t * 3 + 1] < 3 { fails = fails + 1 }
167 if seqs[t * 3 + 2] < 1 { fails = fails + 1 }
168 t = t + 1
169 }
170 }
171 // zero sequences is a valid, trivial decode
172 if nx_zstd_seq_decode_all(tll, tml, tof, b, 0, seqs) != 1 { fails = fails + 1 }
173 if fails > 0 { if mark == 0 { mark = 6 } }
174
175 // ---- T7 NEG: refusals ----
176 nx_zstd_rep_init(rep)
177 if nx_zstd_rep_apply(rep, 0, 5) != (0 - 1) { fails = fails + 1 }
178 if nx_zstd_rep_apply(rep, 0 - 1, 5) != (0 - 1) { fails = fails + 1 }
179 if nx_zstd_rep_apply(rep, 2, 0 - 1) != (0 - 1) { fails = fails + 1 }
180 if nx_zstd_seq_decode_all(tll, tml, tof, b, 0 - 1, seqs) != 0 { fails = fails + 1 }
181 if fails > 0 { if mark == 0 { mark = 7 } }
182
183 if fails == 0 {
184 g_puts("GATE nx_zstd_seqdec verdict=GREEN pass=7/7 (history starts 1/4/8 and a normal offset is value-3 shifting it back; THE ZERO-LITERAL SLIDE proven both ways -- with literals 1/2/3 give rep1/rep2/rep3, without literals they give rep2/rep3/rep1-MINUS-ONE which is not a repeat at all; Offset_Value 1 WITH literals does NOT reorder while 2 and 3 do; the asymmetry inside the reorder -- idx 1 leaves Repeated_Offset3 alone, idx 2 shifts it; 400 mixed applications keep every remembered offset positive; three FSE states run over ONE shared stream with the spec's asymmetric orders -- extra bits offset/match/literal, updates literal/match/offset -- yielding usable triples; NEG offset-value 0 or negative, negative literals length, negative count refused)\n" as *u8)
185 sys_exit(0)
186 return 0
187 }
188 g_puts("GATE nx_zstd_seqdec verdict=RED fails=" as *u8)
189 g_putn(fails)
190 g_puts(" first_stage=" as *u8)
191 g_putn(mark)
192 g_puts("\n" as *u8)
193 sys_exit(1)
194 return 1
195}