nx_zstd_fse_gate.nx source
↩ module page · 135 lines · 5351 B
1// nx_zstd_fse_gate.nx -- proves the FSE (tANS) decoding-table build.
2//
3// An FSE table is not verifiable by eyeballing one cell -- it is verifiable by
4// its INVARIANTS, and those invariants are exactly what a bad spread breaks:
5// * every cell receives a symbol (a stride that is not coprime with the
6// table size silently overwrites cells and leaves holes)
7// * each symbol occupies exactly its normalized count of cells
8// * nb_bits and new_state stay inside the table
9// T4/T5 are the ones that catch the classic defect: with table_log 3 the
10// stride is 8 and 8 & 7 == 0, so the walk never advances and one symbol eats
11// the whole table. We refuse that log outright, and T9 proves it.
12//
13// NON-VACUITY: T8..T12 are negative controls -- counts that do not fill the
14// table, a log below the minimum, a log above the maximum, and out-of-range
15// state lookups must each be REFUSED.
16//
17// license_tier: ORIGINAL
18import "nx_syscalls.nx"
19import "nx_zstd_fse.nx"
20
21func g_puts(s: *u8) -> i64 {
22 var i: i64 = 0
23 while s[i] != (0 as u8) { i = i + 1 }
24 sys_write(1, s, i)
25 return i
26}
27
28func main() -> i64 {
29 var fails: i64 = 0
30
31 // ---- T1: highbit is the MSB index, and 0 has none ----
32 if nx_fse_highbit(1) != 0 { fails = fails + 1 }
33 if nx_fse_highbit(2) != 1 { fails = fails + 1 }
34 if nx_fse_highbit(3) != 1 { fails = fails + 1 }
35 if nx_fse_highbit(255) != 7 { fails = fails + 1 }
36 if nx_fse_highbit(256) != 8 { fails = fails + 1 }
37 if nx_fse_highbit(0) != (0 - 1) { fails = fails + 1 }
38
39 // ---- T2: the spread stride ----
40 if nx_fse_step(32) != 23 { fails = fails + 1 }
41 if nx_fse_step(64) != 43 { fails = fails + 1 }
42
43 // ---- T3: a well-formed table of 32 cells builds ----
44 let norm: *i64 = sys_mmap(NX_FSE_MAX_SYMBOL * 8 + 64) as *i64
45 var i: i64 = 0
46 while i < NX_FSE_MAX_SYMBOL { norm[i] = 0; i = i + 1 }
47 norm[0] = 16
48 norm[1] = 8
49 norm[2] = 8
50 let t: *NxFseTable = nx_fse_build_dtable(norm, 2, 5)
51 if t == (0 as *NxFseTable) { fails = fails + 1 } else {
52 if t.table_size != 32 { fails = fails + 1 }
53
54 // ---- T4: every cell holds a symbol in range, no holes ----
55 var c0: i64 = 0
56 var c1: i64 = 0
57 var c2: i64 = 0
58 var bad: i64 = 0
59 i = 0
60 while i < 32 {
61 let s: i64 = nx_fse_cell_symbol(t, i)
62 if s == 0 { c0 = c0 + 1 } else {
63 if s == 1 { c1 = c1 + 1 } else {
64 if s == 2 { c2 = c2 + 1 } else { bad = bad + 1 } } }
65 i = i + 1
66 }
67 if bad != 0 { fails = fails + 1 }
68
69 // ---- T5: each symbol got exactly its normalized count ----
70 if c0 != 16 { fails = fails + 1 }
71 if c1 != 8 { fails = fails + 1 }
72 if c2 != 8 { fails = fails + 1 }
73
74 // ---- T6/T7: transitions stay inside the table ----
75 var badbits: i64 = 0
76 var badstate: i64 = 0
77 i = 0
78 while i < 32 {
79 let nb: i64 = nx_fse_cell_nbbits(t, i)
80 let ns: i64 = nx_fse_cell_newstate(t, i)
81 if nb < 0 { badbits = badbits + 1 }
82 if nb > 5 { badbits = badbits + 1 }
83 if ns < 0 { badstate = badstate + 1 }
84 if ns >= 32 { badstate = badstate + 1 }
85 i = i + 1
86 }
87 if badbits != 0 { fails = fails + 1 }
88 if badstate != 0 { fails = fails + 1 }
89 }
90
91 // ---- T8 NEG: counts that do not fill the table are REFUSED ----
92 let short_n: *i64 = sys_mmap(NX_FSE_MAX_SYMBOL * 8 + 64) as *i64
93 i = 0
94 while i < NX_FSE_MAX_SYMBOL { short_n[i] = 0; i = i + 1 }
95 short_n[0] = 16
96 short_n[1] = 8
97 short_n[2] = 7
98 if nx_fse_build_dtable(short_n, 2, 5) != (0 as *NxFseTable) { fails = fails + 1 }
99
100 // ---- T9 NEG: table_log 3 has a degenerate stride -> REFUSED ----
101 let tiny: *i64 = sys_mmap(NX_FSE_MAX_SYMBOL * 8 + 64) as *i64
102 i = 0
103 while i < NX_FSE_MAX_SYMBOL { tiny[i] = 0; i = i + 1 }
104 tiny[0] = 8
105 if nx_fse_build_dtable(tiny, 0, 3) != (0 as *NxFseTable) { fails = fails + 1 }
106
107 // ---- T10 NEG: a log above the maximum is REFUSED ----
108 if nx_fse_build_dtable(norm, 2, 13) != (0 as *NxFseTable) { fails = fails + 1 }
109
110 // ---- T11: low-probability (-1) symbols sit at the TOP of the table ----
111 let lowp: *i64 = sys_mmap(NX_FSE_MAX_SYMBOL * 8 + 64) as *i64
112 i = 0
113 while i < NX_FSE_MAX_SYMBOL { lowp[i] = 0; i = i + 1 }
114 lowp[0] = 30
115 lowp[1] = 1
116 lowp[2] = 0 - 1
117 let t2: *NxFseTable = nx_fse_build_dtable(lowp, 2, 5)
118 if t2 == (0 as *NxFseTable) { fails = fails + 1 } else {
119 if nx_fse_cell_symbol(t2, 31) != 2 { fails = fails + 1 }
120 }
121
122 // ---- T12 NEG: out-of-range state lookups report -1, never a cell ----
123 if nx_fse_cell_symbol(t, 32) != (0 - 1) { fails = fails + 1 }
124 if nx_fse_cell_symbol(t, 0 - 1) != (0 - 1) { fails = fails + 1 }
125 if nx_fse_cell_nbbits(0 as *NxFseTable, 0) != (0 - 1) { fails = fails + 1 }
126
127 if fails == 0 {
128 g_puts("GATE nx_zstd_fse verdict=GREEN pass=12/12 (highbit; stride 23/43; 32-cell table builds; no holes; exact per-symbol counts 16/8/8; nb_bits+new_state in range; low-prob symbol at top; NEG underfilled/log-3-degenerate/log-13/out-of-range refused)\n" as *u8)
129 sys_exit(0)
130 return 0
131 }
132 g_puts("GATE nx_zstd_fse verdict=RED\n" as *u8)
133 sys_exit(1)
134 return 1
135}