nx_legal_store_gate.nx source

1// nx_legal_store_gate.nx -- GATE for LEGAL D7 (nx_legal_store), the ENGINEER verify. 2// 3// Composes a REAL D1 vault store + the persistence layer and asserts the durable- 4// state contract, each with a negative control: 5// T1 ROUND-TRIP : a 3-version vault saved + loaded into a FRESH array is 6// byte-identical (every record field), as after a restart. 7// T2 SURVIVES-RESTART: the reloaded array still satisfies the vault invariants 8// (version_count=3, chain OK, current=v3) -- real state, not bytes. 9// T3 TENANT ISOLATION: ls_path rejects '../x' / 'a/b' / '' (no traversal); a 10// different tenant's path is a different file -> can't load it. 11// T4 ABSENT + CORRUPT: load of a missing file -> -1; a wrong-magic file -> -MAGIC 12// (never silent garbage). 13// T5 STRIDE GUARD : a vault file (stride 8) loaded as stride 9 -> -STRIDE 14// (a vault can never be misread as an envelope). 15// T6 IDEMPOTENT : saving twice then loading yields the identical store (#10). 16// 17// Evidence -> knowledge/status/legal_store.log 18// license_tier: ORIGINAL 19import "nx_legal_store.nx" 20import "nx_doc_vault.nx" 21import "nx_syscalls.nx" 22import "nx_gate_verdict.nx" 23 24const LST_LOG: *u8 = "knowledge/status/legal_store.log" 25const LST_BASE: *u8 = "/tmp/nx_ls_" 26 27func ew(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 } 28func ewn(fd: i64, v: i64) -> i64 { 29 let bb: *u8 = sys_mmap(28); var m: i64 = v 30 if m < 0 { m = 0 - m; sys_write(fd, "-" as *u8, 1) } 31 let t: *u8 = sys_mmap(28); var k: i64 = 0 32 if m == 0 { t[0] = 48; k = 1 } 33 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 34 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 } 35 sys_write(fd, bb, k); return 0 36} 37 38func main() -> i64 { 39 var ok: i64 = 1 40 let cap: i64 = 16 41 let flat1: *i64 = sys_mmap(cap * VF_STRIDE * 8) as *i64 42 let flat2: *i64 = sys_mmap(cap * VF_STRIDE * 8) as *i64 43 let path: *u8 = sys_mmap(512) 44 let pathB: *u8 = sys_mmap(512) 45 46 // ---- build a real 3-version vault store ---- 47 var count: i64 = 0 48 count = nx_vault_add(flat1, count, cap, 7001, 1001, 500, 100) 49 count = nx_vault_add(flat1, count, cap, 7001, 1002, 510, 200) 50 count = nx_vault_add(flat1, count, cap, 7001, 1003, 520, 300) 51 52 // ---- T1: save + load into a FRESH array, byte-identical ---- 53 var t1: i64 = 1 54 if ls_path(path, LST_BASE, "clientA" as *u8, "vault" as *u8) < 0 { t1 = 0 } 55 if ls_save(flat1, count, VF_STRIDE, path) != LS_OK { t1 = 0 } 56 let lc: i64 = ls_load(flat2, cap, VF_STRIDE, path) 57 if lc != count { t1 = 0 } 58 var i: i64 = 0 59 while i < count * VF_STRIDE { 60 if flat2[i] != flat1[i] { t1 = 0 } 61 i = i + 1 62 } 63 if t1 != 1 { ok = 0 } 64 65 // ---- T2: the reloaded store still satisfies the vault invariants ---- 66 var t2: i64 = 1 67 if nx_vault_version_count(flat2, lc, 7001) != 3 { t2 = 0 } 68 if nx_vault_verify_chain(flat2, lc, 7001) != VAULT_OK { t2 = 0 } 69 let cur: i64 = nx_vault_current_idx(flat2, lc, 7001) 70 if cur < 0 { t2 = 0 } 71 if flat2[cur * VF_STRIDE + VF_VER] != 3 { t2 = 0 } 72 if t2 != 1 { ok = 0 } 73 74 // ---- T3: tenant isolation ---- 75 // (a genuine zeroed empty string -- the bare "" literal can alias another 76 // literal in the string pool, so build the empty tenant explicitly.) 77 var t3: i64 = 1 78 let empty: *u8 = sys_mmap(8); empty[0] = 0 as u8 79 if ls_path(path, LST_BASE, "../etc" as *u8, "vault" as *u8) != (0 - 1) { t3 = 0 } 80 if ls_path(path, LST_BASE, "a/b" as *u8, "vault" as *u8) != (0 - 1) { t3 = 0 } 81 if ls_path(path, LST_BASE, empty, "vault" as *u8) != (0 - 1) { t3 = 0 } 82 // clientB's path is a DIFFERENT file -> loading it finds nothing (no cross-tenant) 83 if ls_path(pathB, LST_BASE, "clientB" as *u8, "vault" as *u8) < 0 { t3 = 0 } 84 if ls_load(flat2, cap, VF_STRIDE, pathB) != (0 - 1) { t3 = 0 } 85 if t3 != 1 { ok = 0 } 86 87 // ---- T4: absent + corrupt ---- 88 var t4: i64 = 1 89 let pmiss: *u8 = sys_mmap(512) 90 if ls_path(pmiss, LST_BASE, "nobody" as *u8, "vault" as *u8) < 0 { t4 = 0 } 91 if ls_load(flat2, cap, VF_STRIDE, pmiss) != (0 - 1) { t4 = 0 } 92 // write a wrong-magic file, then load -> -LS_ERR_MAGIC 93 let pbad: *u8 = sys_mmap(512) 94 if ls_path(pbad, LST_BASE, "corrupt" as *u8, "vault" as *u8) < 0 { t4 = 0 } 95 let bfd: i64 = sys_openat_wr(pbad, 420) 96 if bfd < 0 { t4 = 0 } else { 97 let bh: *i64 = sys_mmap(32) as *i64 98 bh[0] = 0xDEADBEEF; bh[1] = VF_STRIDE; bh[2] = 0 99 sys_write(bfd, bh as *u8, 24) 100 sys_close(bfd) 101 } 102 if ls_load(flat2, cap, VF_STRIDE, pbad) != (0 - LS_ERR_MAGIC) { t4 = 0 } 103 if t4 != 1 { ok = 0 } 104 105 // ---- T5: stride guard (a vault file is not an envelope file) ---- 106 var t5: i64 = 1 107 // path still points at clientA's saved vault (stride 8); load expecting stride 9 -> refused 108 if ls_path(path, LST_BASE, "clientA" as *u8, "vault" as *u8) < 0 { t5 = 0 } 109 if ls_load(flat2, cap, 9, path) != (0 - LS_ERR_STRIDE) { t5 = 0 } 110 if t5 != 1 { ok = 0 } 111 112 // ---- T6: idempotent re-save ---- 113 var t6: i64 = 1 114 if ls_save(flat1, count, VF_STRIDE, path) != LS_OK { t6 = 0 } 115 if ls_save(flat1, count, VF_STRIDE, path) != LS_OK { t6 = 0 } 116 let lc2: i64 = ls_load(flat2, cap, VF_STRIDE, path) 117 if lc2 != count { t6 = 0 } 118 var j: i64 = 0 119 while j < count * VF_STRIDE { 120 if flat2[j] != flat1[j] { t6 = 0 } 121 j = j + 1 122 } 123 if t6 != 1 { ok = 0 } 124 125 // ---- evidence ---- 126 var fd: i64 = 1 127 while fd >= 1 { 128 ew(fd, "LEGALSTOREGATE authored=organ composes=D1 roundtrip=" as *u8); ewn(fd, t1) 129 ew(fd, " survives_restart=" as *u8); ewn(fd, t2) 130 ew(fd, " tenant_isolation=" as *u8); ewn(fd, t3) 131 ew(fd, " absent_corrupt=" as *u8); ewn(fd, t4) 132 ew(fd, " stride_guard=" as *u8); ewn(fd, t5) 133 ew(fd, " idempotent_resave=" as *u8); ewn(fd, t6) 134 if ok == 1 { ew(fd, " verdict=GREEN\n" as *u8) } else { ew(fd, " verdict=RED\n" as *u8) } 135 if fd == 1 { 136 let lf: i64 = sys_openat_append(LST_LOG, 420) 137 if lf >= 1 { fd = lf } else { fd = 0 } 138 } else { 139 sys_close(fd); fd = 0 140 } 141 } 142 143 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 144 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 145 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 146 let ctr__dry: *i64 = gv_ctr() 147 ctr__dry[0] = ok 148 ctr__dry[1] = 1 149 let rc__dry: i64 = gv_verdict("LEGAL-STORE-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 150 sys_exit(rc__dry) 151 return rc__dry 152}