code wiki / (root) / nx_model_lane_gate.nx

nx_model_lane_gate.nx

buildroot/runtime/nx_model_lane_gate.nx

4141 B79 linesdepth 4pulls 5 transitivereach 0 importersview sourcekind gate/prooftopic model
docsdependenciesstructsconstsfunctions

about

nx_model_lane_gate.nx -- gate for the sovereign model-lane lease. Deterministic, tiny-RAM, test lease path only (never touches the real lane). Proves: T1 claim -> free -> re-claim (lifecycle; pid=1 init = always alive) T2 second claimant REFUSED while held (rc=10) -- the anti-OOM tooth T3 stale holder (dead pid) is REAPED and the lane re-claimed (crash recovery) T4 NEG headroom: absurd est_mb DENIED (rc=11) even though the lane is FREE T5 NEG corrupt lease: garbage bytes -> claim REFUSES rc=14 (fail-loud, never steals) T6 NEG free-by-non-holder REFUSED (rc=13) license_tier: ORIGINAL expect_exit: 0

dependencies 2 imports · 0 importers

nx_model_lane_core.nx nx_gate_verdict.nx nx_model_lane_gate.nx

imports: nx_model_lane_core.nxnx_gate_verdict.nx

imported by: nobody (leaf or entry point)

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

main std_putln std_puts std_slen sys_write ml_unlink ml_claim ml_meminfo_avail_mb sys_mmap sys_openat_rd sys_read sys_close std_slen ↻ std_putln ↻ std_puts ↻ std_pdec sys_mmap ↻ std_itoa sys_mmap ↻ sys_write ↻ ml_try_create sys_mmap ↻ std_itoa ↻ sys_now_us sys_mmap ↻ sys_clock_gettime_mono sys_write ↻ sys_close ↻ ml_unlink ↻ sys_mmap ↻ sys_openat_rd ↻ sys_read ↻ sys_close ↻ ml_parse ml_pid_alive sys_mmap ↻ std_itoa ↻ sys_openat_rd ↻ sys_close ↻ sys_now_us ↻

structs

none

consts

none

functions

13func mg_write_raw(path: *u8, s: *u8) -> i64
called by 1: main calls 2: sys_openat_wrstd_slen
22func main(argc: i64, argv: *i64) -> i64
calls 9: std_putlnml_unlinkml_claimml_freestd_putsstd_pdec+3