code wiki / _hdl_build / nx_livemap_fast_gate.nx

nx_livemap_fast_gate.nx source

↩ module page · 115 lines · 5460 B

1// nx_livemap_fast_gate.nx -- prove the LINEAR live-doc map is byte-identical to the quadratic one. 2// 3// ss_open2 already built the authoritative maps at h[1 + 8*ns + s] using the existing O(keys x 4// segments) shadow scan. This gate rebuilds the same maps using the newest-first hash table from 5// nx_livemap_fast and compares EVERY BYTE. Any difference is a correctness failure, not a perf note: 6// these maps decide which documents are visible, so a faster map that is subtly different does not 7// make search quick, it makes search WRONG. 8// 9// Run against the REAL shard, not a fixture. A synthetic 2-segment store would not exercise the 10// shadow logic that only appears with many overlapping segments, and this session already learned 11// that a gate is only as honest as its ugliest input. 12// license_tier: ORIGINAL No hw writes (Rule 26). 13import "nx_livemap_fast.nx" 14import "nx_gate_verdict.nx" 15 16func lg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 17 18func main(argc: i64, argv: *i64) -> i64 { 19 let ctr: *i64 = gv_ctr() 20 gv_head("nx_livemap_fast -- linear live-doc map must be BYTE-IDENTICAL to the quadratic one on the real shard" as *u8) 21 22 var prefix: *u8 = "knowledge/store/dp-web-pub-" as *u8 23 if argc >= 2 { prefix = argv[1] as *u8 } 24 25 let h: *i64 = ss_open2(prefix, 1) 26 var t1: i64 = 0 27 if (h as i64) != 0 { t1 = 1 } 28 gv_check("T1 the shard opens (nothing below means anything if it does not)" as *u8, t1, ctr) 29 if t1 == 0 { 30 let rcx: i64 = gv_verdict("LIVEMAPFAST" as *u8, ctr, "linear live-doc map equivalence" as *u8) 31 sys_exit(rcx) 32 return rcx 33 } 34 35 let ns: i64 = h[0] 36 gv_puts(" segments=" as *u8); gv_num(ns); gv_puts("\n" as *u8) 37 gv_check("T2 the shard has MULTIPLE segments, so the shadow path is actually exercised" as *u8, lg_eq(ns > 1, 1), ctr) 38 39 let total: i64 = lmf_total_keys(h, ns) 40 gv_puts(" total key entries=" as *u8); gv_num(total); gv_puts("\n" as *u8) 41 let cap: i64 = lmf_pow2(total * LMF_LOAD_NUM + 16) 42 let tbl_seg: *i64 = sys_mmap(8 * cap) as *i64 43 let tbl_eo: *i64 = sys_mmap(8 * cap) as *i64 44 let ins: i64 = lmf_build(h, ns, tbl_seg, tbl_eo, cap) 45 gv_puts(" distinct keys inserted=" as *u8); gv_num(ins); gv_puts("\n" as *u8) 46 gv_check("T3 the table inserted at least one key and no more than the total entry count" as *u8, lg_eq(ins > 0, 1), ctr) 47 gv_check("T4 distinct keys cannot exceed total entries (a table that over-counts is broken)" as *u8, lg_eq(ins <= total, 1), ctr) 48 49 // Rebuild each segment's live map with the LINEAR shadow test and diff against ss_open2's. 50 var mismatched_bytes: i64 = 0 51 var compared_bytes: i64 = 0 52 var segs_done: i64 = 0 53 var s: i64 = 0 54 while s < ns { 55 let kb: *u8 = h[1 + 8 * s] as *u8 56 let ksz: i64 = h[2 + 8 * s] 57 let pb: *u8 = h[7 + 8 * s] as *u8 58 let dsz: i64 = h[4 + 8 * s] 59 let want: *u8 = h[1 + 8 * ns + s] as *u8 60 let ndoc: i64 = dsz / 9 + 16 61 let got: *u8 = sys_mmap(ndoc) 62 var z: i64 = 0 63 while z < ndoc { got[z] = 0 as u8; z = z + 1 } 64 if ksz >= 8 { if h[8 + 8 * s] >= 8 { 65 let nd9: i64 = ss_r32(pb, 4) 66 let m9: i64 = ss_r32(kb, 4) 67 var e9: i64 = 0 68 while e9 < m9 { 69 let eo: i64 = 8 + 4 * m9 + ss_r32(kb, 8 + 4 * e9) 70 let kind9: i64 = kb[eo] 71 let kl9: i64 = ss_r32(kb, eo + 1) 72 let vof: i64 = ss_r32(kb, eo + 5 + kl9) 73 if kind9 == 1 { if kl9 < 500 { 74 let newest: i64 = lmf_lookup(h, tbl_seg, tbl_eo, cap, kb, eo) 75 var shadowed: i64 = 0 76 if newest > s { shadowed = 1 } 77 if shadowed == 0 { 78 let ioff: i64 = vof - 9 - kl9 79 var lo9: i64 = 0 80 var hi9: i64 = nd9 - 1 81 while lo9 <= hi9 { 82 let mid9: i64 = (lo9 + hi9) / 2 83 let dv: i64 = ss_r32(pb, 8 + 4 * mid9) 84 if dv == ioff { got[mid9] = 1 as u8; lo9 = hi9 + 1 } else { 85 if dv < ioff { lo9 = mid9 + 1 } else { hi9 = mid9 - 1 } 86 } 87 } 88 } 89 } } 90 e9 = e9 + 1 91 } 92 } } 93 var b: i64 = 0 94 while b < ndoc { 95 compared_bytes = compared_bytes + 1 96 if got[b] != want[b] { mismatched_bytes = mismatched_bytes + 1 } 97 b = b + 1 98 } 99 sys_munmap(got, ndoc) 100 segs_done = segs_done + 1 101 s = s + 1 102 } 103 104 gv_puts(" segments compared=" as *u8); gv_num(segs_done) 105 gv_puts(" bytes compared=" as *u8); gv_num(compared_bytes) 106 gv_puts(" MISMATCHED=" as *u8); gv_num(mismatched_bytes); gv_puts("\n" as *u8) 107 108 gv_check("T5 every segment was compared, none skipped" as *u8, lg_eq(segs_done, ns), ctr) 109 gv_check("T6 a non-trivial number of bytes was actually compared (a zero-byte diff proves nothing)" as *u8, lg_eq(compared_bytes > 0, 1), ctr) 110 gv_check("T7 BYTE-IDENTICAL to the quadratic implementation across the whole shard" as *u8, lg_eq(mismatched_bytes, 0), ctr) 111 112 let rc: i64 = gv_verdict("LIVEMAPFAST" as *u8, ctr, "linear live-doc map is byte-identical to the quadratic one on the real shard" as *u8) 113 sys_exit(rc) 114 return rc 115}