`nx_ctrl_fn.nx` source

↩ module page · 120 lines · 6732 B
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 fn: i64 = pc_frame(fb, 1785433000, 3000, 18, 81480, 47557, 2361, 98, 231, 351, 2)
94    let en: 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 fn == en {
97        var q: i64 = 0
98        var same: i64 = 1
99        while q < fn { 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}
nx_ctrl_fn.nx source

`nx_ctrl_fn.nx` source
