code wiki / (root) / nx_zstd_bits_gate.nx

nx_zstd_bits_gate.nx

buildroot/runtime/nx_zstd_bits_gate.nx

9743 B210 linesdepth 3pulls 3 transitivereach 0 importersview sourcekind gate/prooftopic zstd
docsdependenciesstructsconstsfunctions

about

nx_zstd_bits_gate.nx -- proves zstd's BACKWARD reader and Huffman weights. T2 pins the SENTINEL. zstd streams carry no length: the final byte's highest SET bit marks the end of the data, and everything above it is padding. The test uses two last bytes with the marker at OPPOSITE ends -- 0x81 (marker at bit 7, so almost nothing is padding) and 0x01 (marker at bit 0, so the whole final byte is consumed by the sentinel). A reader that assumes a fixed padding width passes one and fails the other. T3 is the clean identity: with a final byte of 0x01 the readable data is exactly the preceding bytes, so reading 8 bits must return that byte's own value. Bits are packed LSB-first within a byte but the stream is walked HIGH-to-LOW overall; only getting both right reproduces the byte. T6 pins the INFERRED LAST WEIGHT via KRAFT EQUALITY. zstd never stores the final Huffman weight -- it is whatever completes the set to an exact power of two. The check is that after completion, sum of 2^(tableLog - length) over all present symbols equals 2^tableLog EXACTLY. A decoder that reads only the stored weights builds a table missing its last symbol, decodes most literals correctly, and produces one wrong byte wherever that symbol appears. license_tier: ORIGINAL

dependencies 2 imports · 0 importers

nx_syscalls.nx nx_zstd_bits.nx nx_zstd_bits_gate.nx

imports: nx_syscalls.nxnx_zstd_bits.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main nx_zb_highbit8 sys_mmap nx_zstd_bits_init nx_zb_at nx_zb_highbit8 ↻ sys_mmap ↻ nx_zstd_bits_remaining nx_zstd_bits_read nx_zb_at ↻ nx_zstd_weights_direct nx_zb_at ↻ nx_zstd_weights_complete nx_zstd_weights_tablelog nx_zstd_weights_to_lengths g_puts sys_write sys_exit g_putn sys_mmap ↻ g_puts ↻ sys_write ↻

structs

none

consts

none

functions

26func g_puts(s: *u8) -> i64
called by 2: g_putnmain calls 1: sys_write
33func g_putn(v: i64) -> i64
called by 1: main calls 3: sys_mmapg_putssys_write
47func main() -> i64