nx_ctxtop_gate.nx source

1// nx_ctxtop_gate.nx -- the gate nx_ctxtop and nx_memvel SHIPPED WITHOUT. Closing my own gap. 2// 3// Both organs went live on the strength of 'it compiled and printed plausible numbers' -- which is 4// exactly the vacuous-green class this ecosystem bans. Their shared core (top-k, pid join, share, and 5// the new admission check) is pure and was never proven. T5/T6 are the load-bearing cells: a top-k that 6// evicts the WRONG entry silently truncates the biggest producer, and that is the silent-truncation 7// defect (L011) hiding inside a tool built to FIND producers. 8// license_tier: ORIGINAL expect_exit: 0 No hw writes (Rule 26). 9import "nx_ctxtop_lib.nx" 10import "nx_gate_verdict.nx" 11 12const CG_ARR: i64 = 256 13const CG_BUF: i64 = 128 14const CG_K: i64 = 3 15const CG_MAXLOAD: i64 = 800 16 17func cg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 18func cg_cpy(d: *u8, s: *u8) -> i64 { 19 var i: i64 = 0 20 while s[i] != (0 as u8) { d[i] = s[i]; i = i + 1 } 21 d[i] = 0 as u8 22 return i 23} 24 25func main() -> i64 { 26 let ctr: *i64 = gv_ctr() 27 gv_head("nx_ctxtop_gate -- the shared core of nx_ctxtop + nx_memvel, finally proven" as *u8) 28 29 // ---- ct_find ---- 30 let ids: *i64 = sys_mmap(CG_ARR) as *i64 31 ids[0] = 111 32 ids[1] = 222 33 ids[2] = 333 34 gv_check("T1 ct_find locates a pid by value" as *u8, cg_eq(ct_find(ids, 3, 222), 1), ctr) 35 gv_bite("T2 ct_find REFUSES an absent pid (-1, never index 0)" as *u8, 36 cg_eq(ct_find(ids, 3, 999), 0 - 1), 37 cg_eq(ct_find(ids, 3, 111), 0 - 1), ctr) 38 39 // ---- ct_topk_insert: descending order + correct eviction ---- 40 let tp: *i64 = sys_mmap(CG_ARR) as *i64 41 let tr: *i64 = sys_mmap(CG_ARR) as *i64 42 var used: i64 = 0 43 used = ct_topk_insert(tp, tr, CG_K, used, 1, 10) 44 used = ct_topk_insert(tp, tr, CG_K, used, 2, 20) 45 used = ct_topk_insert(tp, tr, CG_K, used, 3, 30) 46 var t3: i64 = 0 47 if used == 3 { if tr[0] == 30 { if tr[1] == 20 { if tr[2] == 10 { t3 = 1 } } } } 48 gv_check("T3 the table is kept sorted DESCENDING as entries arrive out of order" as *u8, t3, ctr) 49 50 // a LATE-ARRIVING BIG entry must displace the smallest incumbent, not be dropped 51 used = ct_topk_insert(tp, tr, CG_K, used, 4, 25) 52 var t4: i64 = 0 53 if used == 3 { if tr[0] == 30 { if tr[1] == 25 { if tr[2] == 20 { t4 = 1 } } } } 54 gv_bite("T4 a late BIG producer evicts the SMALLEST, never itself (silent-truncation class)" as *u8, 55 t4, cg_eq(tr[1], 20), ctr) 56 57 // a genuinely small entry against a full table must be dropped, leaving the table untouched 58 let before: i64 = tr[2] 59 used = ct_topk_insert(tp, tr, CG_K, used, 5, 1) 60 var t5: i64 = 0 61 if used == 3 { if tr[2] == before { t5 = 1 } } 62 gv_check("T5 a below-threshold entry is dropped and the full table is left intact" as *u8, t5, ctr) 63 64 // TEST-DESIGN FIX (this cell FAILED as a FALSE-POSITIVE on first run and the bite tooth caught it): 65 // against a FULL table `used` stays k whether the insert happened or not, so comparing to `used` 66 // could not distinguish REFUSE from ACCEPT. Use an EMPTY table where the count actually moves. 67 // ★LAW: an assertion whose two outcomes produce the SAME observable is not an assertion. 68 let fp: *i64 = sys_mmap(CG_ARR) as *i64 69 let fr: *i64 = sys_mmap(CG_ARR) as *i64 70 gv_bite("T6 ct_topk_insert REFUSES a negative rate (an UNMEASURED axis cannot rank)" as *u8, 71 cg_eq(ct_topk_insert(fp, fr, CG_K, 0, 6, 0 - 5), 0), 72 cg_eq(ct_topk_insert(fp, fr, CG_K, 0, 7, 99), 0), ctr) 73 74 // ---- ct_share_permil ---- 75 gv_check("T7 ct_share_permil computes a permil share" as *u8, cg_eq(ct_share_permil(250, 1000), 250), ctr) 76 gv_bite("T8 ct_share_permil REFUSES a zero total instead of dividing by it" as *u8, 77 cg_eq(ct_share_permil(5, 0), 0 - 1), 78 cg_eq(ct_share_permil(5, 10), 0 - 1), ctr) 79 80 // ---- ct_load_centi: the REAL /proc/loadavg line measured on this NAS ---- 81 // TEST-DESIGN FIX (T11 also FAILED as a FALSE-POSITIVE first run -- BUFFER ALIASING): one shared 82 // buffer was overwritten three times, so the bite's good-leg read "garbage" using the FIRST string's 83 // length. Separate buffers per fixture. ★LAW: a fixture that a later fixture can overwrite is not a 84 // fixture -- and note T9 PASSED on the same buffer, so the alias was invisible until a cell re-read it. 85 let lb: *u8 = sys_mmap(CG_BUF) 86 let lb2: *u8 = sys_mmap(CG_BUF) 87 let lb3: *u8 = sys_mmap(CG_BUF) 88 let n1: i64 = cg_cpy(lb, "4.02 4.02 4.30 8/1836 3111" as *u8) 89 let n2: i64 = cg_cpy(lb2, "16.75 12.00 9.31 3/900 42" as *u8) 90 let n3: i64 = cg_cpy(lb3, "garbage" as *u8) 91 gv_check("T9 parses the REAL measured loadavg 4.02 as 402 centi" as *u8, 92 cg_eq(ct_load_centi(lb, n1), 402), ctr) 93 gv_check("T10 parses a two-digit whole part (16.75 -> 1675)" as *u8, 94 cg_eq(ct_load_centi(lb2, n2), 1675), ctr) 95 gv_bite("T11 ct_load_centi REFUSES an unparseable loadavg" as *u8, 96 cg_eq(ct_load_centi(lb3, n3), 0 - 1), 97 cg_eq(ct_load_centi(lb, n1), 0 - 1), ctr) 98 99 // ---- ct_admit: the whole point -- refuse to add load to a saturated box ---- 100 gv_check("T12 admits on a quiet box (402 centi under an 800 ceiling)" as *u8, 101 cg_eq(ct_admit(402, CG_MAXLOAD), 1), ctr) 102 gv_bite("T13 REFUSES on a saturated box (1675 centi over the ceiling)" as *u8, 103 cg_eq(ct_admit(1675, CG_MAXLOAD), 0), 104 cg_eq(ct_admit(402, CG_MAXLOAD), 0), ctr) 105 gv_bite("T14 FAIL-CLOSED: an unreadable loadavg REFUSES (cannot tell = do not add to it)" as *u8, 106 cg_eq(ct_admit(0 - 1, CG_MAXLOAD), 0), 107 cg_eq(ct_admit(402, CG_MAXLOAD), 0), ctr) 108 109 let rc: i64 = gv_verdict("CTXTOP-GATE" as *u8, ctr, "shared core of nx_ctxtop + nx_memvel proven, incl. admission control" as *u8) 110 sys_exit(rc) 111 return rc 112}