code wiki / (root) / nx_zstd_lit_gate.nx

nx_zstd_lit_gate.nx

buildroot/runtime/nx_zstd_lit_gate.nx

9040 B193 linesdepth 5pulls 5 transitivereach 0 importersview sourcekind gate/prooftopic zstd
docsdependenciesstructsconstsfunctions

about

nx_zstd_lit_gate.nx -- proves the zstd literals section. T2 pins the NON-BYTE-ALIGNED size fields. Two bits of block type and two of size format share byte 0 with the TOP of the regenerated size, so every size read starts at bit 4 and runs on little-endian. Reading whole bytes instead yields a value wrong by a factor of 16 -- loud on a large block, silent on a small one. The test uses hand-built headers at every size format and asserts the decoded size exactly. T3 pins the DOUBLE MEANING of the format field. For Raw and RLE, formats 0 and 2 are the SAME one-byte form. For Compressed and Treeless the same two values mean different things -- 0 is ONE stream, 1 is FOUR, both with 10-bit sizes. One field, two interpretations, decided by the block type. T5 decodes Huffman literals end-to-end through the table built by nx_zstd_huf: header -> table -> backward stream -> literal bytes. It reuses the hand-assembled stream whose symbol sequence is derived in the huf gate, so the expected output is known independently of this code. license_tier: ORIGINAL

dependencies 4 imports · 0 importers

nx_syscalls.nx nx_zstd_bits.nx nx_zstd_huf.nx nx_zstd_lit.nx nx_zstd_lit_gate.nx

imports: nx_syscalls.nxnx_zstd_bits.nxnx_zstd_huf.nxnx_zstd_lit.nx

imported by: nobody (leaf or entry point)

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

main sys_mmap nx_zstd_lit_header_write nx_zstd_lit_header nx_lit_at nx_zstd_lit_raw nx_zstd_lit_rle nx_zstd_huf_build sys_mmap ↻ nx_zstd_lit_huf nx_zstd_bits_init nx_zb_at nx_zb_highbit8 sys_mmap ↻ nx_zstd_huf_decode nx_zstd_bits_peek nx_zb_at ↻ nx_zstd_huf_symbol_at nx_zstd_huf_nbits_at nx_zstd_bits_skip 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