code wiki / (root) / nx_toolreg_reap_gate.nx

nx_toolreg_reap_gate.nx

buildroot/runtime/nx_toolreg_reap_gate.nx

6666 B135 linesdepth 2pulls 2 transitivereach 0 importersview sourcekind gate/prooftopic toolreg

docs dependencies structs consts functions

about

nx_toolreg_reap_gate.nx -- proof that the reaper removes what it should and REFUSES what it must not. The teeth that matter are the NEGATIVE ones. A reaper that removes everything asked of it is a registry-deletion oracle; the whole safety claim is that it discriminates by TARGET SHAPE, so T2 (a live .elf row survives an explicit reap request) and T4 (unrelated rows byte-preserved) are what make T1 mean anything. T5 checks the no-op path writes NOTHING -- rewriting a shared conf to change nothing is how a concurrent reader gets a truncated read for no reason. license_tier: ORIGINAL expect_exit: 0

dependencies 1 imports · 0 importers

imports: nx_syscalls.nx

imported by: nobody (leaf or entry point)

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

structs

none

consts

none

functions

11	func rg_w(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 1: main calls 1: sys_write
12	func rg_slen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } called by 2: rg_wfile rg_has
13	func rg_wn(v: i64) -> i64 called by 1: main calls 2: sys_mmap sys_write
19	func rg_wfile(path: u8, content: u8) -> i64 called by 1: main calls 4: sys_openat_wr sys_write rg_slen sys_close
26	func rg_read(path: u8, buf: u8, cap: i64) -> i64 called by 1: main calls 3: sys_openat_rd sys_read sys_close
39	func rg_has(b: u8, n: i64, s: u8) -> i64 called by 1: main calls 1: rg_slen
52	func rg_run(elf: u8, dir: u8, a1: u8, a2: u8) -> i64 called by 1: main calls 6: sys_fork sys_chdir sys_mmap sys_execve sys_exit sys_wait4
70	func main(argc: i64, argv: *i64) -> i64 calls 9: rg_w sys_mkdir rg_wfile rg_run sys_mmap rg_read+3