nx_netscope_heal_loop_test.nx source

1// nx_netscope_heal_loop_test.nx -- 1:1 KAT for the live MAPE-K loop safety 2// brain (nx_netscope_heal_loop.nx). Pure + deterministic: backoff stays 3// in its Full-Jitter bound, the circuit breaker trips/opens/half-opens, 4// the retry budget exhausts + refills, and the composed step gates 5// act/wait/give-up so the loop CONVERGES instead of thrashing. 6// 7// expect_exit: 0 8// license_tier: ORIGINAL 9 10import "nx_netscope_heal_loop.nx" 11 12func main() -> i64 { 13 let w: *i64 = sys_mmap(8) as *i64 14 15 // ---- T1: Full-Jitter backoff stays within [0, min(cap, base<<attempt)] ---- 16 let base: i64 = 100 17 let cap: i64 = 2000 18 var att: i64 = 0 19 while att <= 6 { 20 let bo: i64 = heal_backoff_ms(base, cap, att, 12345) 21 var ceil: i64 = base 22 var a: i64 = 0 23 while a < att { 24 ceil = ceil * 2 25 if ceil >= cap { ceil = cap; a = att } else { a = a + 1 } 26 } 27 if ceil > cap { ceil = cap } 28 if bo < 0 { return 1 } 29 if bo > ceil { return 2 } 30 att = att + 1 31 } 32 33 // ---- T2: circuit breaker closed -> open(threshold) -> halfopen(after open_ms) -> closed ---- 34 let cb: *HealCircuit = sys_mmap(HEAL_CIRCUIT_BYTES) as *HealCircuit 35 heal_cb_init(cb) 36 if heal_cb_allow(cb, 0, 1000) != 1 { return 3 } // closed -> allow 37 heal_cb_on_fail(cb, 0, 3); heal_cb_on_fail(cb, 0, 3); heal_cb_on_fail(cb, 0, 3) // 3 fails / thr 3 -> OPEN 38 if heal_cb_allow(cb, 10, 1000) != 0 { return 4 } // open, within window -> deny 39 if heal_cb_allow(cb, 1010, 1000) != 1 { return 5 } // window elapsed -> half-open, allow one 40 heal_cb_on_success(cb) 41 if heal_cb_allow(cb, 2000, 1000) != 1 { return 6 } // closed again 42 43 // ---- T3: retry budget exhausts then refills ---- 44 let b: *HealBudget = sys_mmap(HEAL_BUDGET_BYTES) as *HealBudget 45 heal_budget_init(b, 2) 46 if heal_budget_try(b, 0, 100000, 2) != 1 { return 7 } // spend 1 (2->1) 47 if heal_budget_try(b, 1, 100000, 2) != 1 { return 8 } // spend 1 (1->0) 48 if heal_budget_try(b, 2, 100000, 2) != 0 { return 9 } // empty -> deny 49 if heal_budget_try(b, 100002, 100000, 2) != 1 { return 10 } // refill window elapsed -> 1 token -> spend 50 51 // ---- T4: composed step gates act / wait / give-up ---- 52 let cb2: *HealCircuit = sys_mmap(HEAL_CIRCUIT_BYTES) as *HealCircuit 53 heal_cb_init(cb2) 54 let bud2: *HealBudget = sys_mmap(HEAL_BUDGET_BYTES) as *HealBudget 55 heal_budget_init(bud2, 5) 56 if heal_loop_next(HEAL_KEEP, cb2, bud2, 0, 0, base, cap, 1000, 100000, 5, 1, w) != HLOOP_STABLE { return 11 } 57 if heal_loop_next(HEAL_GIVEUP, cb2, bud2, 0, 0, base, cap, 1000, 100000, 5, 1, w) != HLOOP_GIVEUP { return 12 } 58 if heal_loop_next(HEAL_SWITCH, cb2, bud2, 0, 0, base, cap, 1000, 100000, 5, 1, w) != HLOOP_ACT { return 13 } 59 heal_cb_on_fail(cb2, 0, 1) // threshold 1 -> open now 60 if heal_loop_next(HEAL_SWITCH, cb2, bud2, 2, 5, base, cap, 1000, 100000, 5, 1, w) != HLOOP_WAIT { return 14 } 61 if *w < 0 { return 15 } 62 if *w > cap { return 16 } // backoff bounded by cap 63 64 // ---- T5: budget-exhausted SWITCH -> GIVEUP (no thrash) ---- 65 let cb3: *HealCircuit = sys_mmap(HEAL_CIRCUIT_BYTES) as *HealCircuit 66 heal_cb_init(cb3) 67 let bud3: *HealBudget = sys_mmap(HEAL_BUDGET_BYTES) as *HealBudget 68 heal_budget_init(bud3, 1) 69 if heal_loop_next(HEAL_SWITCH, cb3, bud3, 0, 0, base, cap, 1000, 100000, 1, 1, w) != HLOOP_ACT { return 17 } 70 if heal_loop_next(HEAL_SWITCH, cb3, bud3, 1, 1, base, cap, 1000, 100000, 1, 1, w) != HLOOP_GIVEUP { return 18 } 71 72 // ---- T6: convergence -- a candidate that keeps failing burns EXACTLY 73 // the retry budget (3 ACTs) then converges to safe GIVEUP (no thrash) ---- 74 var acts: i64 = 0 75 var attempt: i64 = 0 76 var outcome: i64 = HLOOP_ACT 77 let cbx: *HealCircuit = sys_mmap(HEAL_CIRCUIT_BYTES) as *HealCircuit 78 heal_cb_init(cbx) // candidate allowed (closed) 79 let budx: *HealBudget = sys_mmap(HEAL_BUDGET_BYTES) as *HealBudget 80 heal_budget_init(budx, 3) 81 while attempt < 100 { 82 outcome = heal_loop_next(HEAL_SWITCH, cbx, budx, attempt, attempt, base, cap, 1000, 100000, 3, 7, w) 83 if outcome == HLOOP_ACT { acts = acts + 1; attempt = attempt + 1 } else { attempt = 100 } 84 } 85 if outcome != HLOOP_GIVEUP { return 19 } // must converge to safe give-up 86 if acts != 3 { return 20 } // exactly the retry budget, then stop 87 88 sys_write(1, "NETSCOPE HEAL-LOOP KAT PASS (backoff bound + circuit breaker + retry budget + act/wait/giveup gate)\n", 99) 89 return 0 90}