nx_loop_gate.nx source

1// nx_loop_gate.nx -- GATE for nx_loop (the bounded-loop discipline primitive; JPL Power-of-10 rule 2). 2// Flagged by the HONESTY SYSTEM 2026-07-16: reach=421, 50 direct children, ZERO direct validation -- 3// the loop-safety layer itself was unproven. Gate proves: verdict enum validity (+NEG), success/failure 4// split, settle transitions, frame budget exhaustion (exactly N steps), and break-stops-immediately. 5// license_tier: ORIGINAL expect_exit:0 6import "nx_syscalls.nx" 7import "nx_loop.nx" 8 9func lw2(s: *u8) -> i64 { var n:i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 10func ln2(v: i64) -> i64 { let b:*u8=sys_mmap(24); var m:i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m} let t:*u8=sys_mmap(24); var k:i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} var j:i64=0; while j<k{b[j]=t[k-1-j];j=j+1} sys_write(1,b,k); return 0 } 11 12func main() -> i64 { 13 var pass: i64 = 0 14 15 // T1: verdict validity for all 5 + NEG for 99 and -1 16 var ok1: i64 = 1 17 if nx_loop_verdict_is_valid(NX_LOOP_RUNNING) != 1 { ok1 = 0 } 18 if nx_loop_verdict_is_valid(NX_LOOP_DONE_SUCCESS) != 1 { ok1 = 0 } 19 if nx_loop_verdict_is_valid(NX_LOOP_DONE_EXIT) != 1 { ok1 = 0 } 20 if nx_loop_verdict_is_valid(NX_LOOP_BUDGET_EXHAUSTED) != 1 { ok1 = 0 } 21 if nx_loop_verdict_is_valid(NX_LOOP_ABORTED) != 1 { ok1 = 0 } 22 if nx_loop_verdict_is_valid(99) != 0 { ok1 = 0 } 23 if nx_loop_verdict_is_valid(0 - 1) != 0 { ok1 = 0 } 24 if ok1 == 1 { pass = pass + 1; lw2("T1 verdict-valid PASS\n" as *u8) } else { lw2("T1 FAIL\n" as *u8) } 25 26 // T2: success/failure split 27 var ok2: i64 = 1 28 if nx_loop_is_success(NX_LOOP_DONE_SUCCESS) != 1 { ok2 = 0 } 29 if nx_loop_is_success(NX_LOOP_DONE_EXIT) != 1 { ok2 = 0 } 30 if nx_loop_is_failure(NX_LOOP_BUDGET_EXHAUSTED) != 1 { ok2 = 0 } 31 if nx_loop_is_failure(NX_LOOP_ABORTED) != 1 { ok2 = 0 } 32 if nx_loop_is_success(NX_LOOP_ABORTED) != 0 { ok2 = 0 } 33 if ok2 == 1 { pass = pass + 1; lw2("T2 success-split PASS\n" as *u8) } else { lw2("T2 FAIL\n" as *u8) } 34 35 // T3: settle is POST-loop resolution (documented contract): terminal verdicts pass through; 36 // RUNNING at budget -> BUDGET_EXHAUSTED (safe default); RUNNING under budget (defensive 37 // "shouldn't happen" fall-out) -> DONE_SUCCESS. It NEVER returns RUNNING. 38 var ok3: i64 = 1 39 if nx_loop_settle(NX_LOOP_DONE_EXIT, 2, 10) != NX_LOOP_DONE_EXIT { ok3 = 0 } 40 if nx_loop_settle(NX_LOOP_ABORTED, 2, 10) != NX_LOOP_ABORTED { ok3 = 0 } 41 if nx_loop_settle(NX_LOOP_RUNNING, 10, 10) != NX_LOOP_BUDGET_EXHAUSTED { ok3 = 0 } 42 if nx_loop_settle(NX_LOOP_RUNNING, 3, 10) != NX_LOOP_DONE_SUCCESS { ok3 = 0 } 43 if nx_loop_settle(NX_LOOP_RUNNING, 3, 10) == NX_LOOP_RUNNING { ok3 = 0 } 44 if ok3 == 1 { pass = pass + 1; lw2("T3 settle PASS\n" as *u8) } else { lw2("T3 FAIL\n" as *u8) } 45 46 // T4: frame budget -- begin(5): step yields 1 exactly 5 times, then 0 47 let lp: *NxLoopFrame = nx_loop_begin(5) 48 var steps: i64 = 0 49 var guard: i64 = 0 50 while guard < 20 { 51 if nx_loop_step(lp) == 1 { steps = steps + 1 } else { guard = 20 } 52 guard = guard + 1 53 } 54 if steps == 5 { pass = pass + 1; lw2("T4 budget-5 PASS\n" as *u8) } else { lw2("T4 FAIL steps=" as *u8); ln2(steps); lw2("\n" as *u8) } 55 56 // T5: break stops the frame immediately 57 let lp2: *NxLoopFrame = nx_loop_begin(10) 58 nx_loop_step(lp2) 59 nx_loop_step(lp2) 60 nx_loop_break(lp2) 61 if nx_loop_step(lp2) == 0 { pass = pass + 1; lw2("T5 break PASS\n" as *u8) } else { lw2("T5 FAIL step after break\n" as *u8) } 62 63 // T6: settle_counted -- reaching the required count is SUCCESS-class 64 let sc: i64 = nx_loop_settle_counted(NX_LOOP_RUNNING, 10, 10) 65 if nx_loop_verdict_is_valid(sc) == 1 { if sc != NX_LOOP_RUNNING { pass = pass + 1; lw2("T6 settle-counted PASS\n" as *u8) } else { lw2("T6 FAIL still RUNNING at count\n" as *u8) } } else { lw2("T6 FAIL invalid verdict\n" as *u8) } 66 67 lw2("NX-LOOP GATE " as *u8); ln2(pass); lw2("/6" as *u8) 68 if pass == 6 { lw2(" GREEN\n" as *u8); return 0 } 69 lw2(" RED\n" as *u8) 70 return 1 71}