code wiki / _hdl_build / nx_apistack_idempotency_gate.nx

nx_apistack_idempotency_gate.nx source

↩ module page · 110 lines · 8211 B

1import "nx_gate_gn.nx" 2import "nx_gate_base.nx" 3// nx_apistack_idempotency_gate.nx -- hermetic gate for CAP-API-IDEMPOTENCY. Proves a keyed write is exactly-once: 4// a new key executes, a seen key returns the CACHED result (no re-execute), distinct keys are independent, and the 5// first result wins (a retry can't overwrite). Sovereign: nx_syscalls + nx_apistack_idempotency. expect_exit: 0 6// T5-T11 (2026-09-16, debt 1789503583): malformed rows are QUARANTINED not poisonous, the sought key still fails closed 7// under a malformed or torn row, the quarantine is counted and its first line named, and the READ lock is SHARED. 8import "nx_syscalls.nx" 9import "nx_apistack_idempotency.nx" 10import "nx_gate_verdict.nx" 11 12func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 13" as *u8); return ok } 14func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 15func g_eq(a: *u8, b: *u8, n: i64) -> i64 { var i: i64=0; while i<n { if a[i]!=b[i] { return 0 } i=i+1 } return 1 } 16// fixture bytes are assembled from named pieces and byte constants, never from lexer escapes 17func g_puts_fd(fd: i64, s: *u8) -> i64 { let n: i64 = g_slen(s); sys_write(fd, s, n); return n } 18func g_putb_fd(fd: i64, b: i64) -> i64 { let t: *u8 = sys_mmap(1); t[0] = b as u8; sys_write(fd, t, 1); return 1 } 19const GB_TAB: i64 = 9 20const GB_NL: i64 = 10 21const GB_CR: i64 = 13 22 23func main(argc: i64, argv: *i64) -> i64 { 24 gp("=== nx_apistack_idempotency_gate (exactly-once writes over /api) ===\n" as *u8) 25 let L: *u8 = "/tmp/id_ledger.tsv" as *u8 26 // fresh slate: truncate the ledger 27 let fd: i64 = sys_openat_wr(L, 0x1a4); if fd >= 0 { sys_close(fd) } 28 let K1: *u8 = "deploy-2026-07-01-abc" as *u8; let K1n: i64 = g_slen(K1) 29 let K2: *u8 = "restart-xyz" as *u8; let K2n: i64 = g_slen(K2) 30 var pass: i64 = 0; var fail: i64 = 0 31 32 // T1 new key -> not seen (must execute) 33 if id_seen(L, K1, K1n) == 0 { pass=pass+1; gp(" T1 new key -> NOT seen (executes) PASS\n" as *u8) } else { fail=fail+1; gp(" T1 FAIL\n" as *u8) } 34 35 // T2 record result -> now seen + cached result returned 36 id_record(L, K1, K1n, "{\"action\":\"DEPLOY\",\"rc\":0}" as *u8, g_slen("{\"action\":\"DEPLOY\",\"rc\":0}" as *u8)) 37 let s2: i64 = id_seen(L, K1, K1n) 38 let rb: *u8 = sys_mmap(256); let rl: i64 = id_lookup(L, K1, K1n, rb, 256) 39 if s2 == 1 { if g_eq(rb, "{\"action\":\"DEPLOY\",\"rc\":0}" as *u8, rl) == 1 { pass=pass+1; gp(" T2 seen -> returns CACHED result (no re-execute) PASS\n" as *u8) } else { fail=fail+1; gp(" T2 FAIL cached content\n" as *u8) } } else { fail=fail+1; gp(" T2 FAIL not seen\n" as *u8) } 40 41 // T3 distinct key -> independent (not seen) 42 if id_seen(L, K2, K2n) == 0 { pass=pass+1; gp(" T3 distinct key -> independent (not seen) PASS\n" as *u8) } else { fail=fail+1; gp(" T3 FAIL\n" as *u8) } 43 44 // T4 first-write-wins: a retry recording a DIFFERENT result does not overwrite the cached one 45 id_record(L, K1, K1n, "{\"action\":\"DEPLOY\",\"rc\":99}" as *u8, g_slen("{\"action\":\"DEPLOY\",\"rc\":99}" as *u8)) 46 let rb2: *u8 = sys_mmap(256); let rl2: i64 = id_lookup(L, K1, K1n, rb2, 256) 47 if g_eq(rb2, "{\"action\":\"DEPLOY\",\"rc\":0}" as *u8, rl2) == 1 { pass=pass+1; gp(" T4 first-write-wins (retry can't overwrite) PASS\n" as *u8) } else { fail=fail+1; gp(" T4 FAIL overwrote\n" as *u8) } 48 49 // QUARANTINE FIXTURE: good K1 row, a two-TAB row, a CR row, good K2 row, then a torn tail (no trailing newline) 50 let L2: *u8 = "/tmp/id_ledger_q.tsv" as *u8 51 let f2: i64 = sys_openat_wr(L2, 0x1a4) 52 g_puts_fd(f2, K1); g_putb_fd(f2, GB_TAB); g_puts_fd(f2, "ok1" as *u8); g_putb_fd(f2, GB_NL) 53 g_puts_fd(f2, "twotab" as *u8); g_putb_fd(f2, GB_TAB); g_puts_fd(f2, "x" as *u8); g_putb_fd(f2, GB_TAB); g_puts_fd(f2, "y" as *u8); g_putb_fd(f2, GB_NL) 54 g_puts_fd(f2, "crkey" as *u8); g_putb_fd(f2, GB_TAB); g_puts_fd(f2, "v" as *u8); g_putb_fd(f2, GB_CR); g_putb_fd(f2, GB_NL) 55 g_puts_fd(f2, K2); g_putb_fd(f2, GB_TAB); g_puts_fd(f2, "ok2" as *u8); g_putb_fd(f2, GB_NL) 56 g_puts_fd(f2, "torn" as *u8); g_putb_fd(f2, GB_TAB); g_puts_fd(f2, "partial" as *u8) 57 sys_close(f2) 58 let q: *i64 = sys_mmap(16) as *i64 59 60 // T5 a good row BEFORE the malformed rows is found (the old reader refused the whole ledger) 61 let rb5: *u8 = sys_mmap(256); let rl5: i64 = id_lookup_q(L2, K1, K1n, rb5, 256, q) 62 var t5: i64 = 0; if rl5 == 3 { if g_eq(rb5, "ok1" as *u8, 3) == 1 { t5 = 1 } } 63 if t5 == 1 { pass=pass+1; gp(" T5 quarantine: good row before malformed rows still FOUND PASS\n" as *u8) } else { fail=fail+1; gp(" T5 FAIL rl=" as *u8); gn(rl5); gp("\n" as *u8) } 64 65 // T6 a good row AFTER the malformed rows is found too 66 let rb6: *u8 = sys_mmap(256); let rl6: i64 = id_lookup(L2, K2, K2n, rb6, 256) 67 var t6: i64 = 0; if rl6 == 3 { if g_eq(rb6, "ok2" as *u8, 3) == 1 { t6 = 1 } } 68 if t6 == 1 { pass=pass+1; gp(" T6 quarantine: good row after malformed rows still FOUND PASS\n" as *u8) } else { fail=fail+1; gp(" T6 FAIL rl=" as *u8); gn(rl6); gp("\n" as *u8) } 69 70 // T7 the quarantine is COUNTED (three bad rows) and its FIRST LINE is named (line 2) 71 gp(" quarantined=" as *u8); gn(q[0]); gp(" first_bad_line=" as *u8); gn(q[1]); gp("\n" as *u8) 72 if q[0] == 3 { if q[1] == 2 { pass=pass+1; gp(" T7 quarantine counted and first bad line named PASS\n" as *u8) } else { fail=fail+1; gp(" T7 FAIL line\n" as *u8) } } else { fail=fail+1; gp(" T7 FAIL count\n" as *u8) } 73 74 // T8 FAIL-CLOSED KEPT: a malformed row whose key field IS the sought key is not NEW (neg-control of the quarantine) 75 let rb8: *u8 = sys_mmap(256); let rl8: i64 = id_lookup(L2, "twotab" as *u8, g_slen("twotab" as *u8), rb8, 256) 76 if rl8 == ID_EVIDENCE_ERROR { pass=pass+1; gp(" T8 neg-control-malformed-row-under-the-sought-key-fails-closed PASS\n" as *u8) } else { fail=fail+1; gp(" T8 FAIL rl=" as *u8); gn(rl8); gp("\n" as *u8) } 77 78 // T9 a torn tail under the sought key is a torn append, not NEW 79 let rb9: *u8 = sys_mmap(256); let rl9: i64 = id_lookup(L2, "torn" as *u8, g_slen("torn" as *u8), rb9, 256) 80 if rl9 == ID_EVIDENCE_ERROR { pass=pass+1; gp(" T9 neg-control-torn-tail-under-the-sought-key-fails-closed PASS\n" as *u8) } else { fail=fail+1; gp(" T9 FAIL rl=" as *u8); gn(rl9); gp("\n" as *u8) } 81 82 // T10 a key absent from the ledger reads NOT FOUND despite the quarantined rows (they are skipped, not fatal) 83 let rb10: *u8 = sys_mmap(256); let rl10: i64 = id_lookup(L2, "absent-key" as *u8, g_slen("absent-key" as *u8), rb10, 256) 84 if rl10 == ID_NOT_FOUND { pass=pass+1; gp(" T10 absent key reads NOT FOUND beside quarantined rows PASS\n" as *u8) } else { fail=fail+1; gp(" T10 FAIL rl=" as *u8); gn(rl10); gp("\n" as *u8) } 85 86 // T11 SHARED READ LOCK: with LOCK_SH held on another open description of the ledger, a lookup still succeeds 87 // (the old reader took LOCK_EX|LOCK_NB and answered EVIDENCE_UNAVAILABLE here -- the 2026-09-15 rollback) 88 let fdl: i64 = __syscall(257, AT_FDCWD, L, 0, 0, 0, 0) 89 var t11: i64 = 0 90 if fdl >= 0 { 91 if sys_flock(fdl, SYS_LOCK_SH) == 0 { 92 let rb11: *u8 = sys_mmap(256); let rl11: i64 = id_lookup(L, K1, K1n, rb11, 256) 93 if rl11 > 0 { t11 = 1 } 94 sys_flock(fdl, SYS_LOCK_UN) 95 } 96 sys_close(fdl) 97 } 98 if t11 == 1 { pass=pass+1; gp(" T11 shared read lock: lookup succeeds while another reader holds LOCK_SH PASS\n" as *u8) } else { fail=fail+1; gp(" T11 FAIL\n" as *u8) } 99 100 gp("RESULT pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail) 101 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 102 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 103 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 104 let ctr__dry: *i64 = gv_ctr() 105 ctr__dry[0] = pass 106 ctr__dry[1] = pass + fail 107 let rc__dry: i64 = gv_verdict("APISTACK-IDEMPOTENCY-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 108 sys_exit(rc__dry) 109 return rc__dry 110}