code wiki / (root) / nx_zstd_seq_gate.nx

nx_zstd_seq_gate.nx

buildroot/runtime/nx_zstd_seq_gate.nx

10958 B235 linesdepth 3pulls 3 transitivereach 0 importersview sourcekind gate/prooftopic zstd
docsdependenciesstructsconstsfunctions

about

nx_zstd_seq_gate.nx -- proves zstd sequence execution and code tables. T4 is the one that matters. An offset SMALLER than the match length is legal and common -- it is how zstd encodes runs -- and the copy is REQUIRED to read bytes it wrote moments earlier in the same operation. The test uses offset 3 with match length 4 (the fourth byte read is one this copy just wrote) and offset 1 with match length 5 (a pure run). A bulk move that snapshots the source region gives the right answer for the first `offset` bytes and garbage after, so both cases are needed: the offset-1 run fails loudly, the offset-3 overlap fails on exactly one byte. T1 pins the DISCONTINUOUS sequence count: the byte itself below 128, a two-byte form below 255, and an escape to three bytes at exactly 255 biased by 0x7F00. A plain varint reading mis-sizes the header and every table after it. T2/T3 pin the code tables, including that match lengths start at THREE and that the literal-length baselines are the value itself only up to 15. license_tier: ORIGINAL

dependencies 2 imports · 0 importers

nx_syscalls.nx nx_zstd_seq.nx nx_zstd_seq_gate.nx

imports: nx_syscalls.nxnx_zstd_seq.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_seq_header nx_seq_at nx_zstd_ll_base nx_zstd_ll_extra nx_zstd_ml_base nx_zstd_ml_extra nx_zstd_of_base nx_zstd_of_extra nx_zstd_seq_execute 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