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}