nx_handoff_gate_proof.nx source

1// nx_handoff_gate_proof.nx -- GATE proving the shared deep-gate library (runtime/, see the import below). 2// NOTE: the lib filename appears ONLY in the import line -- nx_gate_mutation_probe splices that line to 3// point at a mutated copy; a second textual occurrence would eat the splice and false-GREEN the probe. 4// 5// Oracle = TRUTH TABLES (math ground truth -- the correct external judge for pure logic, same class as 6// RFC/NIST KAT vectors): every primitive is exercised on cases whose right answer is known a priori, 7// including the ADVERSARY cases (a gamed 9999 score MUST be caught by the neg-control; a backslid count 8// MUST trip the regression guard; an absent baseline/evidence file MUST report absent, never fabricate). 9// T1 hg_neg_control -- honest wrong-input score passes; GAMED high score is CAUGHT (liar-killer). 10// T2 hg_monotonic_* -- monotone passes, a reversal is caught (physics invariant). 11// T3 hg_invariant_le/ge -- bound truth table incl equality edge. 12// T4 hg_parse_ints -- mixed tab/space/newline ints parse exactly; empty buffer = 0. 13// T5 hg_no_backslide/worsen-- equal holds; a single worse value = REGRESSION caught. 14// T6 hg_baseline_load -- ABSENT file => -1 (evidence-grounding: never fabricated). 15// T7 hg_evidence_file -- real file (this gate itself) opens=1; fake path=0 (liar-kill). 16// T8 telemetry chain -- per-stage handoff report; fail count, worst-quality-drop + max-time 17// LOCALIZERS correct; deterministic on re-run. 18// Read-only, bounded, deterministic (never-brick). GREEN iff ALL pass. Run with CWD=nxc2 root. 19// Sovereign nx_cc->nxasm (no gcc). expect_exit: 0 license_tier: ORIGINAL 20import "syscalls.nx" 21import "runtime.nx" 22import "nx_handoff_gate.nx" 23const K_MAGIC_9999: i64 = 9999 24const K_MAGIC_3675: i64 = 3675 25const K_MAGIC_4096: i64 = 4096 26 27func check(label: *u8, got: i64, want: i64, pass: *i64, total: *i64) -> i64 { 28 total[0] = total[0] + 1 29 if got == want { 30 pass[0] = pass[0] + 1 31 print(" [PASS] " as *u8) 32 } else { 33 print(" [FAIL] " as *u8) 34 } 35 print(label) 36 print(" got=" as *u8) 37 print_i64(got) 38 print(" want=" as *u8) 39 print_i64(want) 40 print("\n" as *u8) 41 return 0 42} 43 44func main() -> i64 { 45 print("=== nx_handoff_gate_proof: truth-table gate over the shared deep-gate library ===\n" as *u8) 46 let pass: *i64 = sys_mmap(8) as *i64 47 let total: *i64 = sys_mmap(8) as *i64 48 pass[0] = 0 49 total[0] = 0 50 51 // ---------- T1 neg-control (liar-killer) ---------- 52 check("T1a neg-control honest (50<=100)" as *u8, hg_neg_control(50, 100), 1, pass, total) 53 check("T1b neg-control edge (100<=100)" as *u8, hg_neg_control(100, 100), 1, pass, total) 54 check("T1c neg-control CATCHES GAMED 9999" as *u8, hg_neg_control(K_MAGIC_9999, 100), 0, pass, total) 55 56 // ---------- T2 monotonicity (physics invariant) ---------- 57 let mv: *i64 = sys_mmap(8 * 8) as *i64 58 mv[0] = 1 59 mv[1] = 2 60 mv[2] = 2 61 mv[3] = 9 62 check("T2a nondec [1,2,2,9]" as *u8, hg_monotonic_nondec(mv, 4), 1, pass, total) 63 mv[2] = 1 64 check("T2b nondec catches reversal [1,2,1,9]" as *u8, hg_monotonic_nondec(mv, 4), 0, pass, total) 65 mv[0] = 9 66 mv[1] = 3 67 mv[2] = 3 68 mv[3] = 1 69 check("T2c noninc [9,3,3,1]" as *u8, hg_monotonic_noninc(mv, 4), 1, pass, total) 70 mv[2] = 4 71 check("T2d noninc catches rise [9,3,4,1]" as *u8, hg_monotonic_noninc(mv, 4), 0, pass, total) 72 check("T2e n=1 trivially monotone" as *u8, hg_monotonic_nondec(mv, 1), 1, pass, total) 73 74 // ---------- T3 bound invariants ---------- 75 check("T3a le(3,5)" as *u8, hg_invariant_le(3, 5), 1, pass, total) 76 check("T3b le(5,5) edge" as *u8, hg_invariant_le(5, 5), 1, pass, total) 77 check("T3c le(6,5) caught" as *u8, hg_invariant_le(6, 5), 0, pass, total) 78 check("T3d ge(5,3)" as *u8, hg_invariant_ge(5, 3), 1, pass, total) 79 check("T3e ge(2,3) caught" as *u8, hg_invariant_ge(2, 3), 0, pass, total) 80 81 // ---------- T4 parse_ints ---------- 82 let pbuf: *u8 = "3675\t1093 472\n44 216x9" as *u8 83 var plen: i64 = 0 84 while pbuf[plen] != (0 as u8) { plen = plen + 1 } 85 let pv: *i64 = sys_mmap(8 * 8) as *i64 86 let pn: i64 = hg_parse_ints(pbuf, plen, pv, 8) 87 check("T4a parse count (mixed seps)" as *u8, pn, 6, pass, total) 88 check("T4b parse v0" as *u8, pv[0], K_MAGIC_3675, pass, total) 89 check("T4c parse v3" as *u8, pv[3], 44, pass, total) 90 check("T4d parse v5 (x-split)" as *u8, pv[5], 9, pass, total) 91 check("T4e empty buffer = 0" as *u8, hg_parse_ints(pbuf, 0, pv, 8), 0, pass, total) 92 93 // ---------- T5 regression guards ---------- 94 let cur: *i64 = sys_mmap(8 * 4) as *i64 95 let bas: *i64 = sys_mmap(8 * 4) as *i64 96 cur[0] = 5 97 cur[1] = 5 98 cur[2] = 5 99 bas[0] = 5 100 bas[1] = 5 101 bas[2] = 5 102 check("T5a no_backslide equal holds" as *u8, hg_no_backslide(cur, bas, 3), 1, pass, total) 103 cur[1] = 4 104 check("T5b no_backslide CATCHES drop" as *u8, hg_no_backslide(cur, bas, 3), 0, pass, total) 105 cur[1] = 5 106 check("T5c no_worsen equal holds" as *u8, hg_no_worsen(cur, bas, 3), 1, pass, total) 107 cur[1] = 6 108 check("T5d no_worsen CATCHES rise" as *u8, hg_no_worsen(cur, bas, 3), 0, pass, total) 109 110 // ---------- T6 baseline evidence-grounding ---------- 111 let ab: *i64 = sys_mmap(8 * 4) as *i64 112 let absent: i64 = hg_baseline_load("knowledge/status/__hg_no_such_baseline_zzqq.tsv" as *u8, ab, 4) 113 check("T6 absent baseline => -1 (never fabricated)" as *u8, absent, 0 - 1, pass, total) 114 115 // ---------- T7 evidence file (liar-kill on artifacts) ---------- 116 check("T7a real artifact opens (this gate)" as *u8, 117 hg_evidence_file("runtime/_hdl_build/nx_handoff_gate_proof.nx" as *u8), 1, pass, total) 118 check("T7b fake artifact = absent" as *u8, 119 hg_evidence_file("runtime/_hdl_build/__hg_fake_zzqq.nx" as *u8), 0, pass, total) 120 121 // ---------- T8 handoff telemetry + localizers ---------- 122 let stages: *HgStage = sys_mmap(HG_STAGE_BYTES * 4) as *HgStage 123 hg_stage_set(stages, 0, "capture" as *u8, 1000, K_MAGIC_4096, 10, 0) 124 hg_stage_set(stages, 1, "encode" as *u8, 990, 900, 500, 1) 125 hg_stage_set(stages, 2, "transport" as *u8, 400, 900, 20, 0) 126 let fails: i64 = hg_chain_report("demo" as *u8, stages, 3) 127 check("T8a chain fail count" as *u8, fails, 1, pass, total) 128 check("T8b worst-drop LOCALIZES handoff 2 (990->400)" as *u8, hg_chain_worst_drop(stages, 3), 2, pass, total) 129 check("T8c max-time LOCALIZES stage 1 (500us)" as *u8, hg_chain_max_time(stages, 3), 1, pass, total) 130 let w2: i64 = hg_chain_worst_drop(stages, 3) 131 let t2: i64 = hg_chain_max_time(stages, 3) 132 var det: i64 = 0 133 if w2 == 2 { if t2 == 1 { det = 1 } } 134 check("T8d deterministic re-run" as *u8, det, 1, pass, total) 135 check("T8e worst-drop n<2 => -1" as *u8, hg_chain_worst_drop(stages, 1), 0 - 1, pass, total) 136 137 // ---------- verdict ---------- 138 print("=== nx_handoff_gate_proof " as *u8) 139 print_i64(pass[0]) 140 print("/" as *u8) 141 print_i64(total[0]) 142 if pass[0] == total[0] { 143 print(" GREEN (shared liar-killer + regression + telemetry primitives truth-table-proven; retrofit = import + a few lines)\n" as *u8) 144 sys_exit(0) 145 return 0 146 } 147 print(" RED\n" as *u8) 148 sys_exit(1) 149 return 1 150}