code wiki / _hdl_build / nx_proc_snapshot_gate.nx

nx_proc_snapshot_gate.nx

buildroot/runtime/_hdl_build/nx_proc_snapshot_gate.nx

10135 B198 linesdepth 3pulls 3 transitivereach 0 importersview sourcekind gate/prooftopic proc
docsdependenciesstructsconstsfunctions

about

nx_proc_snapshot_gate.nx -- proves the seq1318 fix is CORRECT (same answers) and ACTUALLY O(P) (one walk serves many questions). Every tooth fires on the BAD state and is silent on the good one. The two teeth that matter, and why they are not vacuous: T5 EQUIVALENCE vs THE ORACLE: for a battery of names -- present, absent, and every name this supervisor actually guards -- snapshot answer MUST equal the direct per-name /proc scan. The oracle is the pre-existing implementation, so this proves "no behaviour changed", not "the new code agrees with itself". T6 THE O(P) PROPERTY ITSELF: 25 queries after one refresh must leave the BUILD COUNTER at 1. A correctness-only gate would pass even if the fix silently rebuilt per query -- i.e. if the defect were still there. This measures the fix, not just its output. license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0

dependencies 2 imports · 0 importers

nx_proc_snapshot.nx nx_syscalls.nx nx_proc_snapshot_gate.nx

imports: nx_proc_snapshot.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 ps_refresh ps_build ps_init sys_mmap sys_openat_rd sys_mmap ↻ sys_getdents64 dirent_reclen dirent_name ps_read_cmdline sys_openat_rd ↻ sys_read sys_close sys_close ↻ sys_munmap sys_now_realtime_ms sys_mmap ↻ sys_clock_gettime_real gt_bite gt_puts sys_write gt_slen ps_valid ps_init ↻ ps_age_ms ps_init ↻ sys_now_realtime_ms ↻ ps_alive_snap ps_fresh ps_init ↻ sys_now_realtime_ms ↻ ps_build ↻ ps_contains ps_slen sys_mmap ↻ ps_alive_direct ps_slen ↻ sys_openat_rd ↻ sys_mmap ↻

structs

none

consts

16const GT_QUERIES: i64 = 25 // the ~25 guarded services of the real poll
17const GT_SPANCAP: i64 = 512
18const GT_STDOUT: i64 = 1

functions

20func gt_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
called by 1: gt_puts
21func gt_puts(s: *u8) -> i64 { sys_write(GT_STDOUT, s, gt_slen(s)); return 0 }
called by 2: gt_bitemain calls 2: sys_writegt_slen
22func gt_putn(v: i64) -> i64
called by 1: main calls 2: sys_mmapsys_write
34func gt_bite(bad: i64, id: *u8, why: *u8) -> i64
called by 1: main calls 1: gt_puts
40func main(argc: i64, argv: *i64) -> i64
calls 17: ps_refreshgt_biteps_validps_age_msps_alive_snapsys_mmap+11