code wiki / _hdl_build / nx_frontier_store_gate.nx

nx_frontier_store_gate.nx

buildroot/runtime/_hdl_build/nx_frontier_store_gate.nx

2922 B59 linesdepth 6pulls 7 transitivereach 0 importersview sourcekind gate/prooftopic frontier
docsdependenciesstructsconstsfunctions

about

nx_frontier_store_gate.nx -- F-201 (store-law) verification with a NEGATIVE CONTROL. Proves the frontier backlog round-trips through the SOVEREIGN seg-store: frs_seed a fixture into an ISOLATED /tmp store -> frs_load reconstructs the exact rows; a re-seed with a changed row is REFLECTED (live store read, not cached); a never-seeded prefix loads empty. Exit 0 = GREEN. license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0

dependencies 2 imports · 0 importers

nx_frontier_store.nx nx_syscalls.nx nx_frontier_store_gate.nx

imports: nx_frontier_store.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 sys_mmap frs_seed sts_seed ss_begin_cap sys_mmap ↻ sts_mm sys_mmap ↻ sts_werr sys_write sys_exit sts_rowkey ss_catn sys_mmap ↻ ss_add ss_add2 ss_w32 ss_len ss_catn ↻ ss_commit ss_segid_ok sys_mmap ↻ ss_cat ss_catn ↻ sys_write ↻ ss_write_seg ss_segid_ok ↻ sys_mmap ↻ ss_cat ↻ ss_catn ↻ sys_write ↻ ss_segname ss_cat ↻ ss_catn ↻ ss_writefile sys_openat_wr sys_write ↻ sys_close sys_fsync sys_renameat

structs

none

consts

9const G_PFX: *u8 = "/tmp/frtest-a-"
10const G_PFX_FRESH: *u8 = "/tmp/frtest-never-"
11const G_CAP: i64 = 65536
12const G_NROWS: i64 = 2 // fixture has 2 real rows

functions

14func g_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
called by 3: g_wg_findmain
15func g_w(s: *u8) -> i64 { sys_write(1, s, g_slen(s)); return 0 }
called by 2: g_failmain calls 2: sys_writeg_slen
17func g_find(h: *u8, hn: i64, needle: *u8) -> i64
called by 1: main calls 1: g_slen
30func g_fail(s: *u8) -> i64 { g_w("VERDICT RED -- " as *u8); g_w(s); g_w("\n" as *u8); sys_exit(1); return 1 }
called by 1: main calls 2: g_wsys_exit
32func main() -> i64