code wiki / _hdl_build / nx_wiki_publish_gate.nx
nx_wiki_publish_gate.nx source
↩ module page · 172 lines · 10055 B
1// nx_wiki_publish_gate.nx -- TEETH for A3, the guarded publish wrapper (nx_wiki_publish pub_publish_ex).
2// Proves THE safety property: a guard-REJECTED page can NEVER reach the push path. HERMETIC -- every case
3// is called with do_push_flag=0, so the gate NEVER touches the network/vault/SSH; it asserts the verdict
4// AND that push_invoked==0 exactly where it must be.
5//
6// Cases (each asserts the EXACT machine-readable result, not merely "rejected"/"allowed"):
7// (i) page missing freshness stamp -> status=PUB_REJECTED, code=PG_REJECT_NO_FRESHNESS, push_invoked=0
8// (ii) page with a dead /wiki link -> status=PUB_REJECTED, code=PG_REJECT_DEAD_LINK, push_invoked=0
9// (iii) well-formed page (do_push=0) -> status=PUB_ALLOW_NOPUSH, code=PG_ALLOW, push_invoked=0
10// (iii) proves the ALLOW path is REACHED -- verdict=ALLOW -- while push_invoked=0 confirms that
11// with do_push_flag=0 nothing is pushed. (i)+(ii) prove push_invoked=0 on REJECT = the core
12// safety property: a bad page is fail-closed BEFORE the push path.
13//
14// The ALLOW case PLANTS a real resolvable citation (ss_begin -> war_archive_page -> ss_commit) into a
15// fresh per-run archive store and embeds [[cite:<that cid>]] -- so the guard's archive resolution is
16// exercised end-to-end through the wrapper, not mocked. The page is written to a per-run /tmp file so
17// pub_publish_ex reads it exactly as in production. Appends a PASS line to
18// knowledge/status/wiki_publish_gate.log on all-pass. Exit 0 iff all pass (no fake-green).
19// license_tier: ORIGINAL
20import "nx_wiki_publish.nx"
21import "nx_syscalls.nx"
22
23func g_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
24func g_num(v: i64) -> i64 {
25 let bb: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m }
26 let t: *u8 = sys_mmap(28); var k: i64 = 0
27 if m == 0 { t[0] = 48 as u8; k = 1 }
28 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
29 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
30 sys_write(1, bb, k); return 0
31}
32func g_cat(dst: *u8, off: i64, s: *u8) -> i64 { var o: i64 = off; var k: i64 = 0; while s[k] != (0 as u8) { dst[o] = s[k]; o = o + 1; k = k + 1 } return o }
33func g_catnum(dst: *u8, off: i64, v: i64) -> i64 {
34 var o: i64 = off; let t: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m }
35 var k: i64 = 0; if m == 0 { t[0] = 48 as u8; k = 1 }
36 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
37 var i: i64 = 0; while i < k { dst[o] = t[k - 1 - i]; o = o + 1; i = i + 1 } return o
38}
39func g_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
40
41func g_codename(v: i64) -> *u8 {
42 if v == PG_ALLOW { return "ALLOW" as *u8 }
43 if v == PG_REJECT_NO_FRESHNESS { return "REJECT NO_FRESHNESS" as *u8 }
44 if v == PG_REJECT_DANGLING_CITE { return "REJECT DANGLING_CITE" as *u8 }
45 if v == PG_REJECT_DEAD_LINK { return "REJECT DEAD_LINK" as *u8 }
46 if v == PG_REJECT_PLACEHOLDER { return "REJECT PLACEHOLDER" as *u8 }
47 return "UNKNOWN" as *u8
48}
49
50// emit one row asserting the FULL result triple (status, code, push_invoked). pass iff all three match.
51func g_row(id: i64, what: *u8,
52 got_status: i64, want_status: i64,
53 got_code: i64, want_code: i64,
54 got_pi: i64, want_pi: i64) -> i64 {
55 var ok: i64 = 1
56 if got_status != want_status { ok = 0 }
57 if got_code != want_code { ok = 0 }
58 if got_pi != want_pi { ok = 0 }
59 g_w("PUBROW " as *u8); g_num(id); g_w(" " as *u8)
60 if ok == 1 { g_w("PASS " as *u8) } else { g_w("FAIL " as *u8) }
61 g_w(what)
62 g_w(" [status want=" as *u8); g_w(pub_status_name(want_status)); g_w(" got=" as *u8); g_w(pub_status_name(got_status))
63 g_w(" | code want=" as *u8); g_w(g_codename(want_code)); g_w(" got=" as *u8); g_w(g_codename(got_code))
64 g_w(" | push_invoked want=" as *u8); g_num(want_pi); g_w(" got=" as *u8); g_num(got_pi); g_w("]\n" as *u8)
65 return ok
66}
67
68// write buf to a per-run /tmp file so pub_publish_ex reads it exactly like a production page.
69func g_stage_page(path: *u8, buf: *u8, n: i64) -> i64 {
70 let fd: i64 = sys_openat_wr(path, 0x1a4)
71 if fd < 0 { return 0 - 1 }
72 sys_write(fd, buf, n)
73 sys_close(fd)
74 return 0
75}
76
77func main() -> i64 {
78 // ---- a fresh per-run archive store prefix (flat files in /tmp; no mkdir needed) ----
79 let prefix: *u8 = sys_mmap(128)
80 var po: i64 = 0
81 po = ss_cat(prefix, po, "/tmp/pubds" as *u8)
82 po = ss_catn(prefix, po, sys_now_us())
83 po = ss_cat(prefix, po, "-" as *u8)
84 prefix[po] = 0 as u8
85
86 // ---- PLANT a real resolvable source for the ALLOW case ----
87 let srcbody: *u8 = "NIST SP 800-207: zero-trust denies by default; evidence-cited publishing." as *u8
88 let srcn: i64 = g_slen(srcbody)
89 let goodcid: *u8 = sys_mmap(80)
90 let w: *i64 = ss_begin()
91 let ar: i64 = war_archive_page(w, "src_a3" as *u8, srcbody, srcn, goodcid)
92 if ar != 0 { g_w("PUBGATE FATAL: archive add failed\n" as *u8); sys_exit(2); return 2 }
93 let cr: i64 = ss_commit(prefix, w, 1)
94 if cr != 0 { g_w("PUBGATE FATAL: archive commit failed\n" as *u8); sys_exit(2); return 2 }
95 let pp: *i64 = sys_mmap(16) as *i64
96 let chk: i64 = war_get_by_cid(prefix, goodcid, pp, PG_SCAN_CAP)
97 if chk <= 0 { g_w("PUBGATE FATAL: planted cid did not resolve\n" as *u8); sys_exit(2); return 2 }
98
99 // ---- corpus set ----
100 let cs_ptr: *i64 = sys_mmap(8 * 8) as *i64
101 let cs_len: *i64 = sys_mmap(8 * 8) as *i64
102 cs_ptr[0] = "start" as *u8 as i64; cs_len[0] = 5
103 cs_ptr[1] = "charter" as *u8 as i64; cs_len[1] = 7
104 cs_ptr[2] = "nist_stem" as *u8 as i64; cs_len[2] = 9
105 let ncorpus: i64 = 3
106
107 var pass: i64 = 0
108 var rows: i64 = 0
109 let res: *PubResult = sys_mmap(64) as *PubResult
110
111 // ============================================================================================
112 // (i) REJECT: page missing freshness -> PUB_REJECTED / NO_FRESHNESS / push_invoked=0
113 // ============================================================================================
114 let p_nofresh: *u8 = sys_mmap(2048)
115 var nf: i64 = 0
116 nf = g_cat(p_nofresh, nf, "<h1>Zero Trust</h1><p>no stamp here</p>" as *u8)
117 nf = g_cat(p_nofresh, nf, "<p>See <a href=\"/wiki/charter.html\">charter</a>.</p>" as *u8)
118 let f_nofresh: *u8 = "/tmp/a3_nofresh.html" as *u8
119 if g_stage_page(f_nofresh, p_nofresh, nf) != 0 { g_w("PUBGATE FATAL: stage nofresh failed\n" as *u8); sys_exit(2); return 2 }
120 pub_publish_ex(prefix, f_nofresh, "nofresh" as *u8, cs_ptr, cs_len, ncorpus, 0, res)
121 rows = rows + 1
122 pass = pass + g_row(0, "REJECT no-freshness never reaches push" as *u8,
123 res.status, PUB_REJECTED, res.code, PG_REJECT_NO_FRESHNESS, res.push_invoked, 0)
124
125 // ============================================================================================
126 // (ii) REJECT: dead /wiki link -> PUB_REJECTED / DEAD_LINK / push_invoked=0
127 // ============================================================================================
128 let p_dead: *u8 = sys_mmap(2048)
129 var dd: i64 = 0
130 dd = g_cat(p_dead, dd, "<h1>Zero Trust</h1><p>epoch=1781730256</p>" as *u8)
131 dd = g_cat(p_dead, dd, "<p>See <a href=\"/wiki/ghost_page.html\">a missing page</a>.</p>" as *u8)
132 let f_dead: *u8 = "/tmp/a3_deadlink.html" as *u8
133 if g_stage_page(f_dead, p_dead, dd) != 0 { g_w("PUBGATE FATAL: stage deadlink failed\n" as *u8); sys_exit(2); return 2 }
134 pub_publish_ex(prefix, f_dead, "deadlink" as *u8, cs_ptr, cs_len, ncorpus, 0, res)
135 rows = rows + 1
136 pass = pass + g_row(1, "REJECT dead-link never reaches push" as *u8,
137 res.status, PUB_REJECTED, res.code, PG_REJECT_DEAD_LINK, res.push_invoked, 0)
138
139 // ============================================================================================
140 // (iii) ALLOW path reached (do_push=0): PUB_ALLOW_NOPUSH / PG_ALLOW / push_invoked=0
141 // fresh + a RESOLVABLE cite + only corpus links + real body.
142 // ============================================================================================
143 let p_good: *u8 = sys_mmap(4096)
144 var go: i64 = 0
145 go = g_cat(p_good, go, "<h1>Zero Trust</h1><p class=\"fresh\">epoch=1781730256</p>" as *u8)
146 go = g_cat(p_good, go, "<p>See <a href=\"/wiki/charter.html\">the charter</a> and " as *u8)
147 go = g_cat(p_good, go, "<a href=\"/wiki/start.html#tasks\">tasks</a>.</p>" as *u8)
148 go = g_cat(p_good, go, "<p>Evidence: [[cite:" as *u8)
149 go = g_cat(p_good, go, goodcid)
150 go = g_cat(p_good, go, "]]</p>" as *u8)
151 let f_good: *u8 = "/tmp/a3_good.html" as *u8
152 if g_stage_page(f_good, p_good, go) != 0 { g_w("PUBGATE FATAL: stage good failed\n" as *u8); sys_exit(2); return 2 }
153 pub_publish_ex(prefix, f_good, "good" as *u8, cs_ptr, cs_len, ncorpus, 0, res)
154 rows = rows + 1
155 pass = pass + g_row(2, "ALLOW path reached, do_push=0 so nothing pushed" as *u8,
156 res.status, PUB_ALLOW_NOPUSH, res.code, PG_ALLOW, res.push_invoked, 0)
157
158 // ---- verdict ----
159 g_w("NX-WIKI-PUBLISH-GATE rows=" as *u8); g_num(rows); g_w(" pass=" as *u8); g_num(pass); g_w("\n" as *u8)
160 if pass == rows {
161 let line: *u8 = sys_mmap(256)
162 var off: i64 = g_cat(line, 0, "WIKIPUBLISH row=nx_wiki_publish guarded-wrapper rows=" as *u8)
163 off = g_catnum(line, off, rows); off = g_cat(line, off, " pass=" as *u8); off = g_catnum(line, off, pass)
164 off = g_cat(line, off, " safety=push_invoked-0-on-REJECT verdict=PASS\n" as *u8)
165 let gf: i64 = sys_openat_append("knowledge/status/wiki_publish_gate.log" as *u8, 0x1a4)
166 if gf >= 0 { sys_write(gf, line, off); sys_close(gf) }
167 g_w("NX-WIKI-PUBLISH-GATE verdict=PASS -- guarded publish wrapper recorded in wiki_publish_gate.log\n" as *u8)
168 sys_exit(0); return 0
169 }
170 g_w("NX-WIKI-PUBLISH-GATE verdict=FAIL -- NOT recorded (no fake-green)\n" as *u8)
171 sys_exit(1); return 1
172}