nx_ctrl_same.nx source

1// nx_procchurn_gate.nx -- proves the four pure predicates of nx_procchurn_lib, BOTH POLARITIES. 2// 3// Non-vacuity discipline (seq395 / the quality ruler): every policy cell is a gv_bite -- it must FIRE on 4// the crafted-bad input AND stay SILENT on the crafted-good one. A cell that is green before the defect 5// exists proves nothing. The value cells are pinned to the ACTUAL 2026-07-30 field measurement so the 6// gate would have caught the live fork-storm, not merely compiled. 7// license_tier: ORIGINAL expect_exit: 0 No hw writes (Rule 26). 8import "nx_procchurn_lib.nx" 9import "nx_gate_verdict.nx" 10 11const PG_BUF: i64 = 2048 12const PG_OUT_BYTES: i64 = 256 13// the real numbers measured on the NAS 2026-07-30 (two /proc/stat samples 117s apart) 14const PG_FIELD_FORKS: i64 = 9164 15const PG_FIELD_MS: i64 = 117000 16const PG_FIELD_FORKS_PS: i64 = 78 17const PG_FIELD_SYS_J: i64 = 21639 18const PG_FIELD_USR_J: i64 = 9163 19const PG_FIELD_RATIO: i64 = 2361 20const PG_FIELD_CTXSW_PS: i64 = 91718 21// thresholds under test (the shipped defaults) 22const PG_F_AMBER: i64 = 20 23const PG_F_RED: i64 = 50 24const PG_R_AMBER: i64 = 1000 25const PG_R_RED: i64 = 1500 26const PG_C_AMBER: i64 = 20000 27const PG_C_RED: i64 = 50000 28 29func pg_cpy(d: *u8, s: *u8) -> i64 { 30 var i: i64 = 0 31 while s[i] != (0 as u8) { d[i] = s[i]; i = i + 1 } 32 d[i] = 0 as u8 33 return i 34} 35func pg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 36 37func main() -> i64 { 38 let ctr: *i64 = gv_ctr() 39 gv_head("nx_procchurn_gate -- process-churn predicates, pinned to the 2026-07-30 field data" as *u8) 40 41 gv_check("T1 pc_rate reproduces the field measurement 9164 forks / 117000ms = 78/s" as *u8, 42 pg_eq(pc_rate(PG_FIELD_FORKS, PG_FIELD_MS), PG_FIELD_FORKS_PS), ctr) 43 gv_bite("T2 pc_rate refuses a zero-length window" as *u8, 44 pg_eq(pc_rate(PG_FIELD_FORKS, 0), 0 - 1), 45 pg_eq(pc_rate(PG_FIELD_FORKS, PG_FIELD_MS), 0 - 1), ctr) 46 gv_bite("T3 pc_rate refuses a BACKWARD counter (wrap/reboot between samples)" as *u8, 47 pg_eq(pc_rate(0 - 5, PG_FIELD_MS), 0 - 1), 48 pg_eq(pc_rate(5, PG_FIELD_MS), 0 - 1), ctr) 49 50 gv_check("T4 pc_ratio_permil reproduces the field kernel:user 21639:9163 = 2361 permil" as *u8, 51 pg_eq(pc_ratio_permil(PG_FIELD_SYS_J, PG_FIELD_USR_J), PG_FIELD_RATIO), ctr) 52 gv_bite("T5 pc_ratio_permil saturates on zero userspace instead of reading as parity" as *u8, 53 pg_eq(pc_ratio_permil(100, 0), PC_RATIO_SAT), 54 pg_eq(pc_ratio_permil(100, 100), PC_RATIO_SAT), ctr) 55 56 gv_check("T6 pc_verdict is GREEN when every axis is quiet" as *u8, 57 pg_eq(pc_verdict(1, 100, 100, PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 0), ctr) 58 gv_bite("T7 the FORK axis alone raises RED" as *u8, 59 pg_eq(pc_verdict(60, 100, 100, PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 2), 60 pg_eq(pc_verdict(10, 100, 100, PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 2), ctr) 61 gv_bite("T8 the KERNEL:USER axis alone raises RED" as *u8, 62 pg_eq(pc_verdict(1, 1600, 100, PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 2), 63 pg_eq(pc_verdict(1, 900, 100, PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 2), ctr) 64 gv_bite("T9 the CONTEXT-SWITCH axis alone raises RED" as *u8, 65 pg_eq(pc_verdict(1, 100, 60000, PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 2), 66 pg_eq(pc_verdict(1, 100, 100, PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 2), ctr) 67 gv_check("T10 RED dominates AMBER (amber-only input stays 1)" as *u8, 68 pg_eq(pc_verdict(25, 900, 100, PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 1), ctr) 69 70 let buf: *u8 = sys_mmap(PG_BUF) 71 let out: *i64 = sys_mmap(PG_OUT_BYTES) as *i64 72 let n: i64 = pg_cpy(buf, "cpu0 999 999 999\ncpu 11 22 33 44 55 66 77 88 99 1010\nprocesses 4153147\nctxt 5007810360\n" as *u8) 73 let cnt: i64 = pc_line_ints(buf, n, "cpu " as *u8, out, 10) 74 gv_check("T11 pc_line_ints reads all 10 jiffy fields off the aggregate cpu line" as *u8, pg_eq(cnt, 10), ctr) 75 var t12: i64 = 0 76 if out[0] == 11 { if out[2] == 33 { if out[9] == 1010 { t12 = 1 } } } 77 gv_check("T12 PREFIX DISCIPLINE: cpu-space takes the aggregate line, NOT cpu0 decoy 999s" as *u8, t12, ctr) 78 let pcnt: i64 = pc_line_ints(buf, n, "processes " as *u8, out, 1) 79 var t13: i64 = 0 80 if pcnt == 1 { if out[0] == 4153147 { t13 = 1 } } 81 gv_check("T13 pc_line_ints reads the scalar processes fork counter" as *u8, t13, ctr) 82 gv_bite("T14 pc_line_ints is FAIL-CLOSED on an absent key (-1, never a silent 0)" as *u8, 83 pg_eq(pc_line_ints(buf, n, "nosuchkey " as *u8, out, 1), 0 - 1), 84 pg_eq(pc_line_ints(buf, n, "ctxt " as *u8, out, 1), 0 - 1), ctr) 85 86 gv_check("T15 the REAL 2026-07-30 numbers (78/s, 2361 permil, 91718 ctxsw/s) verdict RED" as *u8, 87 pg_eq(pc_verdict(PG_FIELD_FORKS_PS, PG_FIELD_RATIO, PG_FIELD_CTXSW_PS, 88 PG_F_AMBER, PG_F_RED, PG_R_AMBER, PG_R_RED, PG_C_AMBER, PG_C_RED), 2), ctr) 89 90 // ---- the append-only journal frame: proven BYTE-FOR-BYTE without touching a filesystem ---- 91 let fb: *u8 = sys_mmap(PG_BUF) 92 let eb: *u8 = sys_mmap(PG_BUF) 93 let frmn: i64 = pc_frame(fb, 1785433000, 3000, 18, 81480, 47557, 2361, 98, 231, 351, 2) 94 let expn: i64 = pg_cpy(eb, "ts=1785433000 window_ms=3000 forks_ps=18 ctxsw_ps=81480 intr_ps=47557 ku_permil=2361 usr_permil=98 sys_permil=231 busy_permil=351 sev=2\n" as *u8) 95 var t16: i64 = 0 96 if frmn == expn { 97 var q: i64 = 0 98 var same: i64 = 1 99 while q < frmn { if fb[q] != eb[q] { same = 0 } q = q + 1 } 100 t16 = same 101 } 102 gv_check("T16 pc_frame emits the journal frame BYTE-FOR-BYTE (parseable trend line)" as *u8, t16, ctr) 103 104 // An UNMEASURED axis is -1. If pc_catn dropped the sign it would land in the journal as a huge 105 // positive number and read as a catastrophic measurement instead of an absent one. 106 let nb: *u8 = sys_mmap(PG_BUF) 107 let nb2: *u8 = sys_mmap(PG_BUF) 108 let nn1: i64 = pc_catn(nb, 0, 0 - 1) 109 var neg_ok: i64 = 0 110 if nn1 == 2 { if nb[0] == (45 as u8) { if nb[1] == (49 as u8) { neg_ok = 1 } } } 111 pc_catn(nb2, 0, 1) 112 var pos_signed: i64 = 0 113 if nb2[0] == (45 as u8) { pos_signed = 1 } 114 gv_bite("T17 pc_catn keeps the sign on -1 (UNMEASURED stays visible, never wraps huge)" as *u8, 115 neg_ok, pos_signed, ctr) 116 117 let rc: i64 = gv_verdict("PROCCHURN-GATE" as *u8, ctr, "process-churn predicates proven both polarities on field data" as *u8) 118 sys_exit(rc) 119 return rc 120}