nx_meet_store_gate.nx source

1// nx_meet_store_gate.nx -- liar-kill gate for P4 (durable member/application store over the seg-store). Proves 2// store -> read-back byte-exact, the meet:ids index tracks ids, an UPDATE (latest-value-wins) reflects the new 3// record (PENDING -> MEMBER), an absent id reads -1, and a never-stored id is not indexed (teeth). Idempotent-safe 4// on a persistent store. expect_exit: 0 5import "nx_syscalls.nx" 6import "nx_meet_lib.nx" 7import "nx_meet_store.nx" 8import "nx_gate_verdict.nx" 9 10func eq_n(buf: *u8, len: i64, exp: *u8) -> i64 { 11 if len != mlen(exp) { return 0 } 12 var i: i64 = 0 13 while i < len { if buf[i] != exp[i] { return 0 } i = i + 1 } 14 return 1 15} 16 17func main() -> i64 { 18 mputs("=== nx_meet_store_gate: durable member store (seg-store, NO TSV) ===\n" as *u8) 19 let r1: *u8 = "kind: apply\nname: Jane Doe\nstatus: SCREENED" as *u8 20 let r1b: *u8 = "kind: apply\nname: Jane Doe\nstatus: MEMBER" as *u8 21 let r2: *u8 = "kind: hire\nname: Acme Inc\nstatus: SCREENED" as *u8 22 let pq: *i64 = sys_mmap(16) as *i64 23 let lq: *i64 = sys_mmap(16) as *i64 24 25 var pass: i64 = 0; var fail: i64 = 0 26 // put + read back byte-exact 27 if meet_store_put("m-gate-001" as *u8, r1) == 0 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL put-1\n" as *u8) } 28 if meet_store_get("m-gate-001" as *u8, pq, lq) == 1 { if eq_n(pq[0] as *u8, lq[0], r1) == 1 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL roundtrip-1\n" as *u8) } } else { fail=fail+1; mputs(" FAIL get-1-absent\n" as *u8) } 29 if meet_store_indexed("m-gate-001" as *u8) == 1 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL not-indexed-1\n" as *u8) } 30 // a second member 31 if meet_store_put("m-gate-002" as *u8, r2) == 0 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL put-2\n" as *u8) } 32 if meet_store_get("m-gate-002" as *u8, pq, lq) == 1 { if eq_n(pq[0] as *u8, lq[0], r2) == 1 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL roundtrip-2\n" as *u8) } } else { fail=fail+1; mputs(" FAIL get-2-absent\n" as *u8) } 33 // UPDATE m-001 (latest-value-wins: SCREENED -> MEMBER) 34 if meet_store_put("m-gate-001" as *u8, r1b) == 0 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL update-1\n" as *u8) } 35 if meet_store_get("m-gate-001" as *u8, pq, lq) == 1 { if eq_n(pq[0] as *u8, lq[0], r1b) == 1 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL update-not-latest\n" as *u8) } } else { fail=fail+1; mputs(" FAIL get-1b-absent\n" as *u8) } 36 // index stays consistent after the idempotent update 37 if meet_store_indexed("m-gate-001" as *u8) == 1 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL index-lost-after-update\n" as *u8) } 38 // TEETH: an absent id reads -1, and a never-stored id is not indexed 39 if meet_store_get("m-gate-nope" as *u8, pq, lq) == 0 - 1 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL absent-not--1\n" as *u8) } 40 if meet_store_indexed("m-gate-nope" as *u8) == 0 { pass=pass+1 } else { fail=fail+1; mputs(" FAIL phantom-indexed\n" as *u8) } 41 42 mputs("MEET-STORE-GATE pass=" as *u8); mnum(pass); mputs(" fail=" as *u8); mnum(fail) 43 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 44 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 45 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 46 let ctr__dry: *i64 = gv_ctr() 47 ctr__dry[0] = pass 48 ctr__dry[1] = pass + fail 49 let rc__dry: i64 = gv_verdict("MEET-STORE-GATE" as *u8, ctr__dry, "durable member store: roundtrip + index + latest-wins update, sovereign seg-store no-TSV)" as *u8) 50 sys_exit(rc__dry) 51 return rc__dry 52}