nx_cr_exec_proof.nx source
↩ module page · 77 lines · 4958 B
1// nx_cr_exec_proof.nx -- PROVE (not assert) that code_review_gate is runnable end-to-end over the execution
2// allowlist path (the /mcp tools/call machinery), using a TEST allowlist conf so the operator-curated
3// production tool_allowlist.conf is never touched. Composes tea_run_from (nx_tool_exec_allow) against a written
4// test conf + nx_cr_gate.elf (the single-arg entry point). Demonstrates: a GREEN-allowlisted code_review_gate
5// resolves + runs + returns the gate verdict (dirty->1, clean->0); a RED row is refused; a ghost name is
6// refused (fail-closed). So the operator's remaining step is exactly ONE proven line in tool_allowlist.conf.
7// license_tier: ORIGINAL expect_exit: 0
8import "nx_tool_exec_allow.nx" // tea_run_from + TEA_* codes (transitively nx_tool_run + nx_syscalls)
9import "nx_itoa_lib.nx" // shared MSB-first emitter (zero-alloc)
10const K_MAGIC_262144: i64 = 262144
11
12func p_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
13// MIGRATED to the shared emitter (debt 1785563586). The old body mmapped a scratch buffer
14// per call and never freed it. At PAGE granularity that is 4096B leaked PER CALL -- the
15// defect that took 28.5GB of a 36GB host in nx_ts_lumadiff (2MB input, ~3.66M calls).
16// nxi_* is MSB-first, allocates NOTHING, and emits identical bytes including the sign.
17func p_putn(v: i64) -> i64 { nxi_out(v); return 0 }
18
19func write_conf(path: *u8, content: *u8) -> i64 {
20 let fd: i64 = sys_openat_wr(path, 420)
21 if fd < 0 { return 0 - 1 }
22 var n: i64 = 0
23 while content[n] != (0 as u8) { n = n + 1 }
24 sys_write(fd, content, n)
25 sys_close(fd)
26 return 0
27}
28
29func main() -> i64 {
30 p_puts("=== nx_cr_exec_proof -- code_review_gate runnable over the exec allowlist (TEST conf; prod untouched) ===\n" as *u8)
31 // TEST allowlist: code_review_gate=GREEN (runnable) + blocked_tool=RED (present, refused). TAB=\x09 NL=\x0a.
32 let conf: *u8 = "/tmp/cr_exec_test.conf\x00" as *u8
33 write_conf(conf, "code_review_gate\x09_offc/nx_cr_gate.elf\x09GREEN\x0ablocked_tool\x09_offc/nx_cr_gate.elf\x09RED\x0a\x00" as *u8)
34
35 let out: *u8 = sys_mmap(K_MAGIC_262144)
36 let outlen: *i64 = sys_mmap(16) as *i64
37 let rc: *i64 = sys_mmap(16) as *i64
38
39 // T1: GREEN-allowlisted tool on a DIRTY file -> resolves (rc=TEA_OK=1) + runs + gate exit 1
40 let e1: i64 = tea_run_from(conf, "code_review_gate\x00" as *u8, 16, "runtime/nx_ml_dsa_65.nx\x00" as *u8, out, K_MAGIC_262144, outlen, rc)
41 let r1: i64 = rc[0]
42 p_puts(" T1 code_review_gate(dirty): resolve_rc=" as *u8); p_putn(r1); p_puts(" (want 1=TEA_OK) gate_exit=" as *u8); p_putn(e1); p_puts(" (want 1=RED)\n" as *u8)
43
44 // T2: GREEN-allowlisted tool on a CLEAN file -> resolves + runs + gate exit 0
45 let e2: i64 = tea_run_from(conf, "code_review_gate\x00" as *u8, 16, "runtime/nx_ecdsa_p256.nx\x00" as *u8, out, K_MAGIC_262144, outlen, rc)
46 let r2: i64 = rc[0]
47 p_puts(" T2 code_review_gate(clean): resolve_rc=" as *u8); p_putn(r2); p_puts(" (want 1=TEA_OK) gate_exit=" as *u8); p_putn(e2); p_puts(" (want 0=GREEN)\n" as *u8)
48
49 // T3: a present-but-RED row -> refused (TEA_BLOCKED=0), never runs
50 let e3: i64 = tea_run_from(conf, "blocked_tool\x00" as *u8, 12, "runtime/nx_ecdsa_p256.nx\x00" as *u8, out, K_MAGIC_262144, outlen, rc)
51 let r3: i64 = rc[0]
52 p_puts(" T3 blocked_tool(RED status): resolve_rc=" as *u8); p_putn(r3); p_puts(" (want 0=TEA_BLOCKED, refused)\n" as *u8)
53
54 // T4: a name NOT in the allowlist -> refused (TEA_NOTFOUND=-1), fail-closed
55 let e4: i64 = tea_run_from(conf, "ghost_tool_zzz\x00" as *u8, 14, "x\x00" as *u8, out, K_MAGIC_262144, outlen, rc)
56 let r4: i64 = rc[0]
57 p_puts(" T4 ghost_tool_zzz(absent): resolve_rc=" as *u8); p_putn(r4); p_puts(" (want -1=TEA_NOTFOUND, refused)\n" as *u8)
58
59 var ok: i64 = 1
60 if r1 != 1 { ok = 0 } // dirty resolved GREEN
61 if e1 != 1 { ok = 0 } // dirty gate = RED exit 1
62 if r2 != 1 { ok = 0 } // clean resolved GREEN
63 if e2 != 0 { ok = 0 } // clean gate = GREEN exit 0
64 if r3 != 0 { ok = 0 } // RED row refused (TEA_BLOCKED)
65 if r4 != (0 - 1) { ok = 0 } // ghost refused (TEA_NOTFOUND)
66
67 p_puts("\n" as *u8)
68 if ok == 1 {
69 p_puts("NX-CR-EXEC-PROOF GREEN: code_review_gate resolves + runs over the allowlist (dirty->RED, clean->GREEN) AND fail-closed holds (RED + ghost refused).\n" as *u8)
70 p_puts(" OPERATOR STEP (the only thing left to make it live over /mcp) = ONE curated line in tool_allowlist.conf:\n" as *u8)
71 p_puts(" code_review_gate\x09_offc/nx_cr_gate.elf\x09GREEN\n" as *u8)
72 p_puts(" then issue a cap token for the caller. Discovery already live; execution stays fail-closed until that line exists.\n" as *u8)
73 sys_exit(0); return 0
74 }
75 p_puts("NX-CR-EXEC-PROOF RED: path did not behave as required (see wants above)\n" as *u8)
76 sys_exit(1); return 1
77}