code wiki / (root) / nx_zstd_frame_gate.nx

nx_zstd_frame_gate.nx

buildroot/runtime/nx_zstd_frame_gate.nx

8945 B199 linesdepth 3pulls 3 transitivereach 0 importersview sourcekind gate/prooftopic zstd
docsdependenciesstructsconstsfunctions

about

nx_zstd_frame_gate.nx -- proves the zstd frame and block layer. T3 pins the 2-BYTE FRAME_CONTENT_SIZE BIAS. A two-byte size stores (size - 256), so a naive reader reports every such frame exactly 256 bytes short. The affected range is 256..65791 bytes, which is where small test files live -- so this bug hides in exactly the frames a developer checks by hand. The test asserts a stored 0 means 256. T2 pins the IRREGULAR field-size tables. Neither FCS nor Dictionary_ID size is the flag value: FCS goes 0/2/4/8 (or 1 when Single_Segment is set with flag 0) and DID goes 0/1/2/4. Treating either as the raw flag mis-sizes the header and every byte after it. T6 proves a real end-to-end decode: a frame of raw and RLE blocks IS a valid zstd file, and this decodes one to exact bytes. T7 proves the honest refusal: a Compressed block returns a DISTINCT code rather than passing undecoded bytes through as if they were output. license_tier: ORIGINAL

dependencies 2 imports · 0 importers

nx_syscalls.nx nx_zstd_frame.nx nx_zstd_frame_gate.nx

imports: nx_syscalls.nxnx_zstd_frame.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_frame_write nx_zstd_le_w nx_zstd_fcs_size nx_zstd_did_size nx_zstd_frame_parse nx_zstd_le nx_zstd_at nx_zstd_at ↻ nx_zstd_window_size nx_zstd_did_size ↻ nx_zstd_fcs_size ↻ nx_zstd_window_size ↻ nx_zstd_block_write nx_zstd_le_w ↻ nx_zstd_decode sys_mmap ↻ nx_zstd_frame_parse ↻ nx_zstd_block_parse nx_zstd_le ↻ nx_zstd_le_w ↻ g_puts sys_write sys_exit g_putn sys_mmap ↻ g_puts ↻ sys_write ↻

structs

none

consts

none

functions

24func g_puts(s: *u8) -> i64
called by 2: g_putnmain calls 1: sys_write
31func g_putn(v: i64) -> i64
called by 1: main calls 3: sys_mmapg_putssys_write
45func main() -> i64