nx_heavyio_gate.nx source

1// nx_heavyio_gate.nx -- proves nx_heavyio_lib, THE HEAVY-I/O CONCURRENCY BOUND, and RATCHETS ITS ADOPTION. 2// 3// THE DEFECT (measured 2026-09-02): the storm ruler is instantaneous and per-caller, so independent launch 4// surfaces each pass it and collectively storm the box; the fix is a bound over what is RUNNING across all 5// surfaces, composed from nx_poolgov (width) + nx_ioadmit_lib (storm witness). This gate proves the conf 6// reader, the PURE decision (every conjunct and every unobservable input), the live-box wrappers (width in 7// range, the counter that counts nothing when nothing matches and fires on a process that IS running -- 8// this gate itself), the ratchet arithmetic (a floor that only rises), and -- the maintenance mechanism -- 9// an ADOPTION RATCHET over the real conf: how many declared producers import the lib, floor persisted in 10// knowledge/status/heavyio_adopt.ratchet, every unadopted producer NAMED (a count without a worklist is 11// not actionable). Fixtures live in /tmp/nx_heavyio_gate/ (fixture-ratchet law), created at setup. 12// nx_heavyio_gate (no args) 13// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 14import "nx_syscalls.nx" 15import "nx_gate_verdict.nx" 16import "nx_gatekit_lib.nx" 17import "nx_heavyio_lib.nx" 18 19const HG_FX: *u8 = "/tmp/nx_heavyio_gate" 20const HG_FX_CONF: *u8 = "/tmp/nx_heavyio_gate/heavyio.conf" 21const HG_FX_HALF: *u8 = "/tmp/nx_heavyio_gate/half.conf" 22const HG_FX_SELF: *u8 = "/tmp/nx_heavyio_gate/self.conf" 23const HG_FX_ABSENT: *u8 = "/tmp/nx_heavyio_gate/does-not-exist.conf" 24const HG_REAL_A: *u8 = "knowledge/heavyio.conf" 25const HG_REAL_B: *u8 = "../knowledge/heavyio.conf" 26const HG_RATCHET_A: *u8 = "knowledge/status/heavyio_adopt.ratchet" 27const HG_RATCHET_B: *u8 = "../knowledge/status/heavyio_adopt.ratchet" 28const HG_IMPORT_LINE: *u8 = "import \"nx_heavyio_lib.nx\"" 29const HG_PATHCAP: i64 = 512 30const HG_RBUF: i64 = 64 31// fixture numbers, named for what they test (rule 11): width bounds and a load ceiling any box clears 32const HG_FX_SLOTS: i64 = 1 33const HG_FX_FLOOR: i64 = 2 34const HG_FX_MAXC: i64 = 800 35const HG_FX_WMIN: i64 = 1 36const HG_FX_WMAX: i64 = 4 37// pure-decision fixtures 38const HG_D_RUN_LOW: i64 = 1 39const HG_D_RUN_AT: i64 = 2 40const HG_D_RUN_OVER: i64 = 3 41const HG_D_WIDTH: i64 = 2 42const HG_D_STORM_OK: i64 = 3 43const HG_D_STORM_LINE: i64 = 0 44const HG_D_UNOBS: i64 = 0 - 1 45// ---- THE K-SLOT POOL fixtures (2026-09-03): a fixture lease root under /tmp (never the production knowledge/lease), 46// three CWD roots for the root probe, and a GHOST pid beyond pid_max (4194304) that can never be alive. 47// ★THE LEASE ROOT IS UNIQUE PER RUN (pid-suffixed). Lock dirs are never removed and carry g<N> generation dirs; 48// a planted stamp in a root with history can gate its takeover on a generation dir that ALREADY EXISTS (measured 49// 2026-09-03: a stale g2 made the dead-holder reclaim read as a genuine failure). A fixture that persists state 50// between runs measures its own history, not the code. 51const HG_FX_RUN_PFX: *u8 = "/tmp/nx_heavyio_gate/run-" 52const HG_FX_LEASE_LEAF: *u8 = "lease/" 53const HG_FX_SLOT0_LEAF: *u8 = "heavyio-slot-0.lock" 54const HG_FX_STAMP_LEAF: *u8 = "/stamp" 55const HG_FX_ROOTA: *u8 = "/tmp/nx_heavyio_gate/rootA" 56const HG_FX_ROOTA_K: *u8 = "/tmp/nx_heavyio_gate/rootA/knowledge" 57const HG_FX_ROOTA_C: *u8 = "/tmp/nx_heavyio_gate/rootA/knowledge/heavyio.conf" 58const HG_FX_ROOTB: *u8 = "/tmp/nx_heavyio_gate/rootB" 59const HG_FX_ROOTB_K: *u8 = "/tmp/nx_heavyio_gate/rootB/knowledge" 60const HG_FX_ROOTB_C: *u8 = "/tmp/nx_heavyio_gate/rootB/knowledge/heavyio.conf" 61const HG_FX_ROOTB_SUB: *u8 = "/tmp/nx_heavyio_gate/rootB/sub" 62const HG_FX_ROOTN: *u8 = "/tmp/nx_heavyio_gate/rootN" 63const HG_FX_ANN: *u8 = "/tmp/nx_heavyio_gate/announce.txt" 64const HG_FX_LROOT_BAD: *u8 = "/proc/nx-no-such-dir/lease/" 65const HG_P_WIDTH: i64 = 2 66const HG_P_ONE: i64 = 1 67const HG_P_TTL: i64 = 60 68const HG_P_SLOT_A: i64 = 0 69const HG_P_SLOT_B: i64 = 1 70const HG_P_NONE: i64 = 0 - 1 71const HG_P_STORM_OK: i64 = 1 72const HG_P_ANN_SLOT: i64 = 5 73const HG_GHOST_PID: i64 = 4000000000 74const HG_TAB: i64 = 9 75const HG_NL: i64 = 10 76const HG_STAMPCAP: i64 = 256 77const HG_SLOT0_NAME: *u8 = "heavyio-slot-0" 78const HG_ROOT_KIND_A: i64 = 1 79const HG_ROOT_KIND_B: i64 = 2 80const HG_ROOT_KIND_NONE: i64 = 0 81 82func hg_atoi(b: *u8, n: i64) -> i64 { var v: i64 = 0; var i: i64 = 0; var seen: i64 = 0; while i < n { let c: i64 = b[i] as i64; if c >= 48 { if c <= 57 { v = v * 10 + (c - 48); seen = 1; i = i + 1 } else { i = n } } else { i = n } } if seen == 0 { return 0 - 1 } return v } 83func hg_streq(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 } 84// does <root><name>.nx import the lib? tries runtime/ then runtime/_hdl_build/ under both CWD roots 85func hg_adopted(name: *u8, pbuf: *u8) -> i64 { 86 var o: i64 = 0 87 o = gk_cat(pbuf, 0, "runtime/" as *u8); o = gk_cat(pbuf, o, name); o = gk_cat(pbuf, o, ".nx" as *u8); pbuf[o] = 0 as u8 88 if gk_exists(pbuf) == 1 { return gk_contains(pbuf, HG_IMPORT_LINE) } 89 o = gk_cat(pbuf, 0, "runtime/_hdl_build/" as *u8); o = gk_cat(pbuf, o, name); o = gk_cat(pbuf, o, ".nx" as *u8); pbuf[o] = 0 as u8 90 if gk_exists(pbuf) == 1 { return gk_contains(pbuf, HG_IMPORT_LINE) } 91 o = gk_cat(pbuf, 0, "buildroot/runtime/" as *u8); o = gk_cat(pbuf, o, name); o = gk_cat(pbuf, o, ".nx" as *u8); pbuf[o] = 0 as u8 92 if gk_exists(pbuf) == 1 { return gk_contains(pbuf, HG_IMPORT_LINE) } 93 o = gk_cat(pbuf, 0, "buildroot/runtime/_hdl_build/" as *u8); o = gk_cat(pbuf, o, name); o = gk_cat(pbuf, o, ".nx" as *u8); pbuf[o] = 0 as u8 94 if gk_exists(pbuf) == 1 { return gk_contains(pbuf, HG_IMPORT_LINE) } 95 return 0 - 1 96} 97 98// plant a HELD, unexpired stamp for slot 0 under the fixture lease root, owned by <owner> with holder pid <pid> 99static g_hg_rootdir: *u8 100static g_hg_lroot: *u8 101static g_hg_lock0: *u8 102static g_hg_stamp0: *u8 103func hg_fx_paths() -> i64 { 104 g_hg_rootdir = sys_mmap(HG_PATHCAP) 105 var r: i64 = hio_cat(g_hg_rootdir, 0, HG_FX_RUN_PFX) 106 r = hio_catn(g_hg_rootdir, r, ls_pid()) 107 g_hg_rootdir[r] = 47 as u8; r = r + 1 108 g_hg_rootdir[r] = 0 as u8 109 g_hg_lroot = sys_mmap(HG_PATHCAP) 110 var o: i64 = hio_cat(g_hg_lroot, 0, g_hg_rootdir) 111 o = hio_cat(g_hg_lroot, o, HG_FX_LEASE_LEAF) 112 g_hg_lroot[o] = 0 as u8 113 g_hg_lock0 = sys_mmap(HG_PATHCAP) 114 var p: i64 = hio_cat(g_hg_lock0, 0, g_hg_lroot) 115 p = hio_cat(g_hg_lock0, p, HG_FX_SLOT0_LEAF) 116 g_hg_lock0[p] = 0 as u8 117 g_hg_stamp0 = sys_mmap(HG_PATHCAP) 118 var q: i64 = hio_cat(g_hg_stamp0, 0, g_hg_lock0) 119 q = hio_cat(g_hg_stamp0, q, HG_FX_STAMP_LEAF) 120 g_hg_stamp0[q] = 0 as u8 121 return 0 122} 123func hg_plant_slot0(pid: i64) -> i64 { 124 gk_mkdir(g_hg_lock0) 125 let b: *u8 = sys_mmap(HG_STAMPCAP) 126 var o: i64 = hio_cat(b, 0, "held" as *u8) 127 b[o] = HG_TAB as u8; o = o + 1 128 o = hio_cat(b, o, "pid" as *u8) 129 o = hio_catn(b, o, pid) 130 b[o] = HG_TAB as u8; o = o + 1 131 o = hio_catn(b, o, sys_now_realtime_sec()) 132 b[o] = HG_TAB as u8; o = o + 1 133 o = hio_catn(b, o, HG_P_TTL) 134 b[o] = HG_TAB as u8; o = o + 1 135 o = hio_catn(b, o, sys_now_realtime_sec()) // a generation no g<N> dir in a FRESH root can collide with 136 b[o] = HG_NL as u8; o = o + 1 137 b[o] = 0 as u8 138 gk_write(g_hg_stamp0, b) 139 return 0 140} 141func main(argc: i64, argv: *i64) -> i64 { 142 gv_head("nx_heavyio_gate -- the heavy-I/O concurrency bound: conf, PURE decision, live wrappers, THE K-SLOT POOL (bound, reclaim, root), ratchet, ADOPTION" as *u8) 143 let ctr: *i64 = gv_ctr() 144 gk_mkdir(HG_FX) 145 hg_fx_paths() 146 gk_mkdir(g_hg_rootdir) 147 gk_mkdir(g_hg_lroot) 148 gk_write(HG_FX_CONF, "# fixture\nproducer nx_zz_alpha\nproducer nx_zz_beta\nslots_per_cpu 1\nfloor 2\nmax_centi 800\nwmin 1\nwmax 4\n" as *u8) 149 gk_write(HG_FX_HALF, "producer nx_zz_alpha\nslots_per_cpu 1\nfloor 2\nmax_centi 800\nwmin 1\n" as *u8) 150 gk_write(HG_FX_SELF, "producer nx_heavyio_gate\nslots_per_cpu 1\nfloor 2\nmax_centi 800\nwmin 1\nwmax 4\n" as *u8) 151 gk_rm(HG_FX_ABSENT) 152 gv_check("fixture-reached-condition: fixture conf present and the absent path absent" as *u8, gk_exists(HG_FX_CONF) * (1 - gk_exists(HG_FX_ABSENT)), ctr) 153 154 // ---- conf reader ---- 155 let cfg: *i64 = sys_mmap(HIO_C_BYTES) as *i64 156 let names: *u8 = sys_mmap(HIO_MAXP * HIO_NAMEW) 157 let rd: i64 = hio_conf_read(HG_FX_CONF, cfg, names) 158 gv_check("conf: reads and returns 1" as *u8, rd, ctr) 159 gv_check("conf: two producer rows counted" as *u8, (cfg[HIO_C_NPROD] == 2) as i64, ctr) 160 gv_check("conf: first needle is nx_zz_alpha (exact)" as *u8, hg_streq(hio_slot(names, 0), "nx_zz_alpha" as *u8), ctr) 161 gv_check("conf: sizing keys parsed slots=1 floor=2 max_centi=800 wmin=1 wmax=4" as *u8, 162 ((cfg[HIO_C_SLOTS] == HG_FX_SLOTS) as i64) * ((cfg[HIO_C_FLOOR] == HG_FX_FLOOR) as i64) * ((cfg[HIO_C_MAXC] == HG_FX_MAXC) as i64) * ((cfg[HIO_C_WMIN] == HG_FX_WMIN) as i64) * ((cfg[HIO_C_WMAX] == HG_FX_WMAX) as i64), ctr) 163 let cfg2: *i64 = sys_mmap(HIO_C_BYTES) as *i64 164 let names2: *u8 = sys_mmap(HIO_MAXP * HIO_NAMEW) 165 gv_check("neg-control-absent-conf-reads-0 (the caller reports UNOBSERVABLE)" as *u8, (hio_conf_read(HG_FX_ABSENT, cfg2, names2) == 0) as i64, ctr) 166 let cfgh: *i64 = sys_mmap(HIO_C_BYTES) as *i64 167 let namesh: *u8 = sys_mmap(HIO_MAXP * HIO_NAMEW) 168 hio_conf_read(HG_FX_HALF, cfgh, namesh) 169 gv_check("neg-control-half-conf-cannot-size-the-pool: missing wmax -> width -1" as *u8, (hio_width(cfgh) == (0 - 1)) as i64, ctr) 170 171 // ---- PURE decision ---- 172 gv_check("decide: under width, storm ok -> ADMIT" as *u8, (hio_decide(HG_D_RUN_LOW, HG_D_WIDTH, HG_D_STORM_OK) == HIO_ADMIT) as i64, ctr) 173 gv_check("decide: AT width (self counted) -> ADMIT" as *u8, (hio_decide(HG_D_RUN_AT, HG_D_WIDTH, HG_D_STORM_OK) == HIO_ADMIT) as i64, ctr) 174 gv_check("neg-control-over-width-defers" as *u8, (hio_decide(HG_D_RUN_OVER, HG_D_WIDTH, HG_D_STORM_OK) == HIO_DEFER) as i64, ctr) 175 gv_check("neg-control-storm-line-defers-even-under-width (second conjunct is load-bearing)" as *u8, (hio_decide(HG_D_RUN_LOW, HG_D_WIDTH, HG_D_STORM_LINE) == HIO_DEFER) as i64, ctr) 176 gv_check("decide: unobservable running -> UNOBSERVABLE, never a verdict" as *u8, (hio_decide(HG_D_UNOBS, HG_D_WIDTH, HG_D_STORM_OK) == HIO_UNOBSERVABLE) as i64, ctr) 177 gv_check("decide: unobservable width -> UNOBSERVABLE" as *u8, (hio_decide(HG_D_RUN_LOW, HG_D_UNOBS, HG_D_STORM_OK) == HIO_UNOBSERVABLE) as i64, ctr) 178 gv_check("decide: unobservable storm -> UNOBSERVABLE" as *u8, (hio_decide(HG_D_RUN_LOW, HG_D_WIDTH, HG_D_UNOBS) == HIO_UNOBSERVABLE) as i64, ctr) 179 gv_bite("bite: the same decision DEFERS over width and ADMITS under it" as *u8, 180 (hio_decide(HG_D_RUN_OVER, HG_D_WIDTH, HG_D_STORM_OK) == HIO_DEFER) as i64, 181 (hio_decide(HG_D_RUN_LOW, HG_D_WIDTH, HG_D_STORM_OK) == HIO_DEFER) as i64, ctr) 182 183 // ---- live-box wrappers ---- 184 let w: i64 = hio_width(cfg) 185 gv_check("live: derived width lies within [wmin, wmax] on this box" as *u8, ((w >= HG_FX_WMIN) as i64) * ((w <= HG_FX_WMAX) as i64), ctr) 186 gv_check("live: counter counts NOTHING for needles nothing runs (not -1, not a phantom)" as *u8, (hio_running(cfg, names) == 0) as i64, ctr) 187 let cfgs: *i64 = sys_mmap(HIO_C_BYTES) as *i64 188 let namess: *u8 = sys_mmap(HIO_MAXP * HIO_NAMEW) 189 hio_conf_read(HG_FX_SELF, cfgs, namess) 190 gv_check("neg-control-counter-fires-on-a-running-process (this gate counts itself >= 1)" as *u8, (hio_running(cfgs, namess) >= 1) as i64, ctr) 191 gv_check("live: storm witness observable on this box (budget >= 0)" as *u8, (hio_storm_budget() >= 0) as i64, ctr) 192 let outv: *i64 = sys_mmap(32) as *i64 193 let av: i64 = hio_admit_conf_root(g_hg_rootdir, HG_FX_CONF, outv) 194 gv_check("live: hio_admit on the fixture class yields a real verdict (ADMIT or DEFER), never UNOBSERVABLE here" as *u8, (av != HIO_UNOBSERVABLE) as i64, ctr) 195 hio_announce(1, av, outv) 196 hio_pool_release(g_hg_lroot, outv[HIO_O_SLOT]) 197 gv_check("live: hio_admit on an ABSENT conf yields UNOBSERVABLE" as *u8, (hio_admit_conf(HG_FX_ABSENT, outv) == HIO_UNOBSERVABLE) as i64, ctr) 198 199 // ---- THE K-SLOT POOL (the TOCTOU fix): PURE table, then the bound itself on a fixture lease root ---- 200 gv_check("pool-decide: storm ok + slot held -> ADMIT" as *u8, (hio_decide_pool(HG_P_WIDTH, HG_P_STORM_OK, HG_P_SLOT_A) == HIO_ADMIT) as i64, ctr) 201 gv_check("neg-control-pool-decide-no-slot-defers (every slot held)" as *u8, (hio_decide_pool(HG_P_WIDTH, HG_P_STORM_OK, HG_P_NONE) == HIO_DEFER) as i64, ctr) 202 gv_check("neg-control-pool-decide-storm-first (a slot in hand still DEFERS on the storm line)" as *u8, (hio_decide_pool(HG_P_WIDTH, HG_D_STORM_LINE, HG_P_SLOT_A) == HIO_DEFER) as i64, ctr) 203 gv_check("neg-control-pool-io-is-UNOBSERVABLE-not-DEFER (an unwritable lease root must announce, never stall a producer)" as *u8, 204 ((hio_pool_acquire(HG_FX_LROOT_BAD, HG_P_WIDTH, HG_P_TTL) == HIO_POOL_IO) as i64) * ((hio_decide_pool(HG_P_WIDTH, HG_P_STORM_OK, HIO_POOL_IO) == HIO_UNOBSERVABLE) as i64), ctr) 205 gv_check("pool-decide: unobservable width or storm -> UNOBSERVABLE, never a verdict" as *u8, 206 ((hio_decide_pool(HG_D_UNOBS, HG_P_STORM_OK, HG_P_SLOT_A) == HIO_UNOBSERVABLE) as i64) * ((hio_decide_pool(HG_P_WIDTH, HG_D_UNOBS, HG_P_SLOT_A) == HIO_UNOBSERVABLE) as i64), ctr) 207 let s0: i64 = hio_pool_acquire(g_hg_lroot, HG_P_WIDTH, HG_P_TTL) 208 let s1: i64 = hio_pool_acquire(g_hg_lroot, HG_P_WIDTH, HG_P_TTL) 209 let s2: i64 = hio_pool_acquire(g_hg_lroot, HG_P_WIDTH, HG_P_TTL) 210 gv_check("pool: first acquire takes slot 0, second takes slot 1 (K=2)" as *u8, ((s0 == HG_P_SLOT_A) as i64) * ((s1 == HG_P_SLOT_B) as i64), ctr) 211 let rel0: i64 = hio_pool_release(g_hg_lroot, HG_P_SLOT_A) 212 let s3: i64 = hio_pool_acquire(g_hg_lroot, HG_P_WIDTH, HG_P_TTL) 213 gv_bite("bite: the K+1-th acquire is REFUSED while K are held, and admitted again after ONE release (the bound is real)" as *u8, 214 (s2 == HG_P_NONE) as i64, (s3 == HG_P_NONE) as i64, ctr) 215 gv_check("pool: release returns 0 and the RELEASED slot (0) is the one retaken, not a new one" as *u8, ((rel0 == 0) as i64) * ((s3 == HG_P_SLOT_A) as i64), ctr) 216 hio_pool_release(g_hg_lroot, HG_P_SLOT_A) 217 hio_pool_release(g_hg_lroot, HG_P_SLOT_B) 218 // dead-holder reclaim: a HELD, unexpired stamp whose holder pid cannot exist is reclaimed at once 219 hg_plant_slot0(HG_GHOST_PID) 220 gv_check("fixture-reached-condition: ghost stamp planted and its holder pid reads back dead" as *u8, 221 ((gk_exists(g_hg_stamp0)) as i64) * ((hio_pid_alive(HG_GHOST_PID) == 0) as i64), ctr) 222 let g: i64 = hio_pool_acquire(g_hg_lroot, HG_P_ONE, HG_P_TTL) 223 gv_check("pool: a slot held by a DEAD pid is reclaimed at once by liveness (not by waiting out the ttl)" as *u8, (g == HG_P_SLOT_A) as i64, ctr) 224 hio_pool_release(g_hg_lroot, HG_P_SLOT_A) 225 // neg-control: the SAME shape with an ALIVE holder (this gate's own pid under a foreign owner) must NOT be reclaimed 226 hg_plant_slot0(ls_pid()) 227 let a: i64 = hio_pool_acquire(g_hg_lroot, HG_P_ONE, HG_P_TTL) 228 gv_check("neg-control-pool-alive-holder-is-NOT-reclaimed (a stamp owned by pid<this gate> is alive; liveness discriminates; width 1 -> no slot)" as *u8, (a == HG_P_NONE) as i64, ctr) 229 let me: *u8 = sys_mmap(HIO_PATHCAP) 230 hio_owner(me) 231 ls_release_root(g_hg_lroot, HG_SLOT0_NAME, me) 232 // root resolution: the pool root follows the conf, from THREE CWDs (host root, buildroot-like child, neither) 233 gk_mkdir(HG_FX_ROOTA); gk_mkdir(HG_FX_ROOTA_K); gk_write(HG_FX_ROOTA_C, "producer nx_zz_alpha\n" as *u8) 234 gk_mkdir(HG_FX_ROOTB); gk_mkdir(HG_FX_ROOTB_K); gk_mkdir(HG_FX_ROOTB_SUB); gk_write(HG_FX_ROOTB_C, "producer nx_zz_alpha\n" as *u8) 235 gk_mkdir(HG_FX_ROOTN) 236 let cwd: *u8 = sys_mmap(HG_PATHCAP) 237 sys_getcwd(cwd, HG_PATHCAP) 238 let rr: *u8 = sys_mmap(HIO_PATHCAP) 239 var ka: i64 = 0 - 1 240 var kb: i64 = 0 - 1 241 var kn: i64 = 0 - 1 242 var ka_path: i64 = 0 243 var kb_path: i64 = 0 244 if sys_chdir(HG_FX_ROOTA) == 0 { ka = hio_root(rr); ka_path = hg_streq(rr, HIO_ROOT_A) } 245 if sys_chdir(HG_FX_ROOTB_SUB) == 0 { kb = hio_root(rr); kb_path = hg_streq(rr, HIO_ROOT_B) } 246 if sys_chdir(HG_FX_ROOTN) == 0 { kn = hio_root(rr) } 247 sys_chdir(cwd) 248 gv_check("root: a CWD with knowledge/heavyio.conf resolves kind 1 = knowledge/" as *u8, ((ka == HG_ROOT_KIND_A) as i64) * ka_path, ctr) 249 gv_check("root: a CWD whose conf lives at ../knowledge resolves kind 2 = ../knowledge/ (buildroot producers share the host pool)" as *u8, ((kb == HG_ROOT_KIND_B) as i64) * kb_path, ctr) 250 gv_check("neg-control-root-neither-resolves-0 (UNOBSERVABLE, never a guessed pool)" as *u8, (kn == HG_ROOT_KIND_NONE) as i64, ctr) 251 // the announce line carries the slot so a log reader can see WHICH slot a producer held 252 let outa: *i64 = sys_mmap(HIO_C_BYTES) as *i64 253 outa[HIO_O_RUNNING] = 0; outa[HIO_O_WIDTH] = HG_P_WIDTH; outa[HIO_O_STORM] = HG_P_STORM_OK; outa[HIO_O_SLOT] = HG_P_ANN_SLOT 254 gk_rm(HG_FX_ANN) 255 let afd: i64 = sys_openat_wr(HG_FX_ANN, 0x1a4) 256 if afd >= 0 { hio_announce(afd, HIO_ADMIT, outa); sys_close(afd) } 257 gv_check("announce: the HEAVYIO line carries slot=<n> beside the verdict" as *u8, gk_contains(HG_FX_ANN, " slot=5 verdict=ADMIT" as *u8), ctr) 258 259 // ---- ratchet arithmetic (PURE) ---- 260 gv_check("ratchet: first sight baselines (floor -1, adopters 3 -> 3)" as *u8, (hio_ratchet_next(0 - 1, 3) == 3) as i64, ctr) 261 gv_check("ratchet: rises (3 -> 5)" as *u8, (hio_ratchet_next(3, 5) == 5) as i64, ctr) 262 gv_check("ratchet: holds (3 -> 3)" as *u8, (hio_ratchet_next(3, 3) == 3) as i64, ctr) 263 gv_check("neg-control-ratchet-refuses-to-lower (5 -> 3 is -1, baseline NOT rewritten)" as *u8, (hio_ratchet_next(5, 3) == (0 - 1)) as i64, ctr) 264 265 // ---- ADOPTION RATCHET over the real conf: the maintenance mechanism ---- 266 var real: *u8 = HG_REAL_A 267 var rat: *u8 = HG_RATCHET_A 268 if gk_exists(real) == 0 { real = HG_REAL_B; rat = HG_RATCHET_B } 269 let have_real: i64 = gk_exists(real) 270 gv_need("real knowledge/heavyio.conf present (adoption tooth abstains without it)" as *u8, have_real, ctr) 271 if have_real == 1 { 272 let rc: *i64 = sys_mmap(HIO_C_BYTES) as *i64 273 let rn: *u8 = sys_mmap(HIO_MAXP * HIO_NAMEW) 274 hio_conf_read(real, rc, rn) 275 let np: i64 = rc[HIO_C_NPROD] 276 let pbuf: *u8 = sys_mmap(HG_PATHCAP) 277 var adopters: i64 = 0 278 var unresolved: i64 = 0 279 var i: i64 = 0 280 while i < np { 281 let a: i64 = hg_adopted(hio_slot(rn, i), pbuf) 282 gv_puts(" producer " as *u8); gv_puts(hio_slot(rn, i)) 283 if a == 1 { adopters = adopters + 1; gv_puts(": ADOPTED\n" as *u8) } 284 if a == 0 { gv_puts(": UNADOPTED (does not import nx_heavyio_lib.nx)\n" as *u8) } 285 if a < 0 { unresolved = unresolved + 1; gv_puts(": SOURCE-UNRESOLVED (no .nx under either root)\n" as *u8) } 286 i = i + 1 287 } 288 let rb: *u8 = sys_mmap(HG_RBUF) 289 var floor: i64 = 0 - 1 290 let rl: i64 = gk_read(rat, rb, HG_RBUF - 1) 291 if rl > 0 { floor = hg_atoi(rb, rl) } 292 let nxt: i64 = hio_ratchet_next(floor, adopters) 293 gv_puts(" ADOPTION producers=" as *u8); gv_num(np); gv_puts(" adopters=" as *u8); gv_num(adopters); gv_puts(" unresolved=" as *u8); gv_num(unresolved); gv_puts(" floor=" as *u8); gv_num(floor); gv_puts("\n" as *u8) 294 gv_check("adoption-ratchet: adopters >= persisted floor (a drop is RED and the floor is NOT rewritten)" as *u8, (nxt >= 0) as i64, ctr) 295 gv_check("adoption: every declared producer resolves to a source under some root" as *u8, (unresolved == 0) as i64, ctr) 296 if nxt > floor { 297 let wb: *u8 = sys_mmap(HG_RBUF) 298 var wo: i64 = gk_catn(wb, 0, nxt); wo = gk_cat(wb, wo, "\n" as *u8); wb[wo] = 0 as u8 299 gk_write(rat, wb) 300 gv_puts(" ADOPTION-RATCHET tightened to " as *u8); gv_num(nxt); gv_puts("\n" as *u8) 301 } 302 } 303 304 return gv_verdict("nx_heavyio_gate" as *u8, ctr, 305 "conf reader, PURE decision over every conjunct and unobservable input, live width/counter/storm wrappers on this box, ratchet arithmetic, and the adoption ratchet over the real conf naming every unadopted producer" as *u8) 306}