code wiki / (root) / nx_flatstore_flip_gate.nx

nx_flatstore_flip_gate.nx

buildroot/runtime/nx_flatstore_flip_gate.nx

3615 B67 linesdepth 4pulls 4 transitivereach 0 importersview sourcekind gate/proof
docsdependenciesstructsconstsfunctions

about

nx_flatstore_flip_gate.nx -- proves the GENERIC store-law flip primitive (nx_flatstore_flip) works on a planted fixture: writes a temp .conf (3 data rows + comments + a blank line), flips it to a temp seg_store, and checks migrate byte-exactness (ver==tot==3), round-trip (fsf_count==3), reader reconstruction (fsf_read_all = 3 lines, row 0 == the first data line), + neg-controls (no phantom row past the end; the byte compare has teeth). Run standalone (CWD=nxc2; fixture + store live under /tmp). license_tier: ORIGINAL

dependencies 2 imports · 0 importers

nx_flatstore_flip.nx nx_syscalls.nx nx_flatstore_flip_gate.nx

imports: nx_flatstore_flip.nxnx_syscalls.nx

imported by: nobody (leaf or entry point)

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

main gp sys_write sys_openat_wr gred gp ↻ sys_exit sys_write ↻ sys_close sys_mmap fsf_migrate sys_mmap ↻ ss_readall sys_openat_rd sys_lseek sys_mmap ↻ sys_read sys_close ↻ ss_begin ss_begin_cap sys_mmap ↻ fsf_key sys_mmap ↻ ss_add ss_add2 ss_w32 ss_len ss_commit ss_segid_ok sys_mmap ↻ ss_cat ss_catn sys_mmap ↻ sys_write ↻ ss_write_seg ss_segid_ok ↻ sys_mmap ↻ ss_cat ↻ ss_catn ↻ sys_write ↻

structs

none

consts

19const FX_CONF: *u8 = "/tmp/fsf_fixture.conf"
20const FX_STORE: *u8 = "/tmp/fsf_store"
21const FX_KEY: *u8 = "fsftest:row:"

functions

9func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
called by 2: gredmain calls 1: sys_write
10func gn(v: i64) -> i64
called by 1: main calls 2: sys_mmapsys_write
16func gred(msg: *u8) -> i64 { gp(" RED: " as *u8); gp(msg); gp("\n" as *u8); sys_exit(1); return 1 }
called by 1: main calls 2: gpsys_exit
17func gstreq(a: *u8, b: *u8) -> i64 { var i: i64=0; while a[i]!=(0 as u8){ if a[i]!=b[i]{return 0} i=i+1 } if b[i]!=(0 as u8){return 0} return 1 }
called by 1: main
23func main() -> i64