code wiki / _hdl_build / nx_pub_obs_gate.nx
nx_pub_obs_gate.nx source
↩ module page · 95 lines · 7552 B
1// nx_pub_obs_gate.nx -- R10 PROOF: STATUS snapshot + DRY-RUN plan (zero side-effects) vs the wet run.
2//
3// Seeds a known queue (5 real requests via pub_submit_to: 3 ready, 1 held=outward-unapproved, 1 idempotent-skip),
4// pre-seeds the ledger so one is a skip, approves one outward request, then asserts:
5// STATUS -- the snapshot counts are exact (pending/published/ready/held/skip).
6// DRY-RUN -- the plan counts are exact AND it touches NOTHING (ledger byte-identical, live dir not written).
7// WET -- a real pub_run_governed publishes EXACTLY what dry-run predicted (wet==dryrun==3) and the ledger
8// grows by exactly 3 -- proving both the prediction's accuracy and that dry-run's no-write was real.
9// Liar-kill: dry-run must be the REAL predicate (3 ready, NOT a naive count-all of 5). File-based (no forks).
10// license_tier: ORIGINAL expect_exit: 0
11import "nx_syscalls.nx"
12import "nx_publisher.nx"
13import "nx_runpath.nx"
14
15func 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 }
16func g_n(v: i64) -> i64 { var m: i64=v; if m<0{g_w("-" as *u8);m=0-m} let t:*u8=sys_mmap(24); var k:i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} var i:i64=0; let o:*u8=sys_mmap(24); while i<k{o[i]=t[k-1-i];i=i+1} sys_write(1,o,k); return 0 }
17func g_row(id: *u8, ok: i64, pass: *i64) -> i64 { g_w(" " as *u8); g_w(id); g_w(": " as *u8); if ok==1 { g_w("OK\n" as *u8); pass[0]=pass[0]+1 } else { g_w("FAIL\n" as *u8) } return 0 }
18func sv_write(path: *u8, content: *u8) -> i64 { let fd: i64 = sys_openat_wr(path, 0x1a4); if fd<0 { return 0 } var n: i64=0; while content[n]!=(0 as u8){n=n+1} sys_write(fd, content, n); sys_close(fd); return 1 }
19func g_unlink(path: *u8) -> i64 { __syscall(87, path as i64, 0, 0, 0, 0, 0); return 0 }
20
21func main() -> i64 {
22 let pass: *i64 = sys_mmap(8) as *i64; pass[0]=0
23 g_w("=== NX-PUB-OBS GATE (status snapshot + dry-run plan with zero side-effects, vs the wet run) ===\n" as *u8)
24 let wsid: *u8 = sys_mmap(64); rp_wsid(wsid); rp_ensure(wsid)
25 let D: *u8 = sys_mmap(512); rp_path(wsid, "pob" as *u8, D); __syscall(83, D as i64, 493, 0, 0, 0, 0)
26
27 let qpath: *u8 = sys_mmap(700); pub_join(D, "queue.tsv" as *u8, qpath)
28 let ledpath: *u8 = sys_mmap(700); pub_join(D, "ledger.tsv" as *u8, ledpath)
29 let approval: *u8 = sys_mmap(700); pub_join(D, "approvals" as *u8, approval); __syscall(83, approval as i64, 493, 0, 0, 0, 0)
30 let stageroot: *u8 = sys_mmap(700); pub_join(D, "stage" as *u8, stageroot); __syscall(83, stageroot as i64, 493, 0, 0, 0, 0)
31 let liveroot: *u8 = sys_mmap(700); pub_join(D, "live" as *u8, liveroot); __syscall(83, liveroot as i64, 493, 0, 0, 0, 0)
32
33 // reset queue + ledger for an idempotent re-run; clear stale live deploys from a prior run.
34 // NOTE: reset by UNLINK, not sv_write(path,""): in NishiLang an empty string literal "" aliases adjacent
35 // rodata (it wrote "a.html" into both files), so the first append landed after garbage. Unlink => clean slate.
36 g_unlink(qpath)
37 g_unlink(ledpath)
38 let liveA: *u8 = sys_mmap(700); pub_join(liveroot, "a.html" as *u8, liveA); g_unlink(liveA)
39 let liveB: *u8 = sys_mmap(700); pub_join(liveroot, "b.html" as *u8, liveB); g_unlink(liveB)
40 let liveC: *u8 = sys_mmap(700); pub_join(liveroot, "c.html" as *u8, liveC); g_unlink(liveC)
41
42 // distinct src files (pub_submit_to computes the real content sha)
43 let s1: *u8 = sys_mmap(700); pub_join(D, "s1.src" as *u8, s1); sv_write(s1, "AAA-one\n" as *u8)
44 let s2: *u8 = sys_mmap(700); pub_join(D, "s2.src" as *u8, s2); sv_write(s2, "BBB-two\n" as *u8)
45 let s3: *u8 = sys_mmap(700); pub_join(D, "s3.src" as *u8, s3); sv_write(s3, "CCC-three\n" as *u8)
46 let s4: *u8 = sys_mmap(700); pub_join(D, "s4.src" as *u8, s4); sv_write(s4, "DDD-four\n" as *u8)
47 let s5: *u8 = sys_mmap(700); pub_join(D, "s5.src" as *u8, s5); sv_write(s5, "EEE-five\n" as *u8)
48
49 pub_submit_to(qpath, s1, "a.html" as *u8, "games" as *u8, "wsA" as *u8, "internal" as *u8) // ready
50 pub_submit_to(qpath, s2, "b.html" as *u8, "games" as *u8, "wsB" as *u8, "internal" as *u8) // ready
51 pub_submit_to(qpath, s3, "c.html" as *u8, "site" as *u8, "wsC" as *u8, "outward" as *u8) // ready (approved below)
52 pub_submit_to(qpath, s4, "d.html" as *u8, "site" as *u8, "wsD" as *u8, "outward" as *u8) // held (unapproved)
53 pub_submit_to(qpath, s5, "e.html" as *u8, "games" as *u8, "wsE" as *u8, "internal" as *u8) // idempotent-skip
54
55 let sha3: *u8 = sys_mmap(72); pub_sha_file(s3, sha3); pub_approve(sha3, approval) // approve the outward one
56 let sha5: *u8 = sys_mmap(72); pub_sha_file(s5, sha5); pub_record_ledger(ledpath, sha5, "e.html" as *u8, "games" as *u8) // pre-publish s5
57
58 // ---- STATUS snapshot ----
59 let stat: *i64 = sys_mmap(64) as *i64
60 pub_status(qpath, ledpath, approval, stat)
61 let st_ok: i64 = ((stat[0]==5) as i64) & ((stat[1]==1) as i64) & ((stat[2]==3) as i64) & ((stat[3]==1) as i64) & ((stat[4]==1) as i64)
62
63 // ---- DRY-RUN + no-side-effect proof ----
64 let ledsha_before: *u8 = sys_mmap(72); pub_sha_file(ledpath, ledsha_before)
65 let plan: *i64 = sys_mmap(64) as *i64
66 let dr: i64 = pub_dryrun(qpath, ledpath, approval, plan)
67 let ledsha_after: *u8 = sys_mmap(72); pub_sha_file(ledpath, ledsha_after)
68 let no_mut: i64 = pub_streq(ledsha_before, ledsha_after)
69 let live_untouched: i64 = (pub_exists(liveA)==0) as i64
70 let dr_ok: i64 = ((dr==3) as i64) & ((plan[1]==3) as i64) & ((plan[2]==1) as i64) & ((plan[3]==1) as i64)
71 let r3: i64 = no_mut & live_untouched
72
73 // ---- WET contrast: the real run must match the prediction exactly ----
74 let lockres: *u8 = sys_mmap(128); pub_pcat("pob_pub_" as *u8, wsid, lockres)
75 let wet: i64 = pub_run_governed(qpath, ledpath, stageroot, liveroot, lockres, approval)
76 let ledcount: i64 = pub_count_ledger(ledpath)
77 let wet_ok: i64 = ((wet==3) as i64) & ((dr==wet) as i64) & ((ledcount==4) as i64)
78 let live_now: i64 = pub_exists(liveA)
79 let real_predicate: i64 = ((dr < stat[0]) as i64) & ((dr==3) as i64)
80
81 g_w(" STATUS pending=" as *u8); g_n(stat[0]); g_w(" published=" as *u8); g_n(stat[1]); g_w(" ready=" as *u8); g_n(stat[2]); g_w(" held=" as *u8); g_n(stat[3]); g_w(" skip=" as *u8); g_n(stat[4]); g_w("\n" as *u8)
82 g_w(" DRYRUN ready=" as *u8); g_n(plan[1]); g_w(" held=" as *u8); g_n(plan[2]); g_w(" skip=" as *u8); g_n(plan[3]); g_w(" no_mut=" as *u8); g_n(no_mut); g_w(" live_untouched=" as *u8); g_n(live_untouched); g_w("\n" as *u8)
83 g_w(" WET published=" as *u8); g_n(wet); g_w(" ledger_now=" as *u8); g_n(ledcount); g_w(" live_now=" as *u8); g_n(live_now); g_w("\n" as *u8)
84
85 g_row("STATUS snapshot exact (pending5 / published1 / ready3 / held1 / skip1)" as *u8, st_ok, pass)
86 g_row("DRYRUN plan exact (ready3 / held1 / skip1)" as *u8, dr_ok, pass)
87 g_row("DRYRUN zero side-effects (ledger byte-identical + live untouched)" as *u8, r3, pass)
88 g_row("WET run == dry-run prediction (wet==dr==3) AND ledger grew by exactly 3 (1->4)" as *u8, wet_ok, pass)
89 g_row("LIAR-KILL: dry-run is the REAL predicate (3=ready, NOT naive count-all 5)" as *u8, real_predicate, pass)
90 g_row("WET actually deployed to live (proves dry-run's no-write was real, not a no-op)" as *u8, live_now, pass)
91
92 g_w("NX-PUB-OBS rows=6 pass=" as *u8); g_n(pass[0])
93 if pass[0]==6 { g_w(" verdict=GREEN\n" as *u8); sys_exit(0); return 0 }
94 g_w(" verdict=RED\n" as *u8); sys_exit(1); return 1
95}