nx_zstd_fse_gate.nx
buildroot/runtime/nx_zstd_fse_gate.nx
about
nx_zstd_fse_gate.nx -- proves the FSE (tANS) decoding-table build.
An FSE table is not verifiable by eyeballing one cell -- it is verifiable by
its INVARIANTS, and those invariants are exactly what a bad spread breaks:
* every cell receives a symbol (a stride that is not coprime with the
table size silently overwrites cells and leaves holes)
* each symbol occupies exactly its normalized count of cells
* nb_bits and new_state stay inside the table
T4/T5 are the ones that catch the classic defect: with table_log 3 the
stride is 8 and 8 & 7 == 0, so the walk never advances and one symbol eats
the whole table. We refuse that log outright, and T9 proves it.
NON-VACUITY: T8..T12 are negative controls -- counts that do not fill the
table, a log below the minimum, a log above the maximum, and out-of-range
state lookups must each be REFUSED.
license_tier: ORIGINAL
dependencies 2 imports · 0 importers
imports: nx_syscalls.nxnx_zstd_fse.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| none |
functions
| 21 | func g_puts(s: *u8) -> i64 |
| 28 | func main() -> i64 |