code wiki / _hdl_build / nx_intlog_gate.nx

nx_intlog_gate.nx source

↩ module page · 125 lines · 7622 B

1// nx_intlog_gate.nx -- KAT gate for the integer log2 / IDF / tf-saturation primitives (the BM25 rung's 2// math floor) and the S1 crossover side. Exact on powers of two, tight (+-2/1024) between them, monotonic, 3// overflow-safe at the top of the domain, the derived idf/tfsat behaviors the ranking depends on, and the 4// corpus-scale side decision with its planted-other-side control. MIGRATED onto nx_gate_verdict 2026-09-14: 5// /api/promote refused the hand-rolled verdict (D001) because nothing outside the gate could read it. 6// license_tier: ORIGINAL expect_exit: 0 7import "nx_intlog.nx" 8import "nx_gate_verdict.nx" 9// T9 fixture values, NAMED because the build ratchet counts inline literal sites (it refused T9c for adding three) 10const GI_CROSSOVER_TOKENS: i64 = 10000000 // the published crossover the conf carries, planted here as the threshold 11const GI_ONE_UNDER: i64 = 9999999 // one token under the crossover reads BELOW 12const GI_WEB_TOKENS: i64 = 376066000 // a web-sized corpus, far above 13const GI_TWICE: i64 = 20000000 // twice the crossover, the planted other side 14const GI_ONE_TOKEN: i64 = 1 // a one-token corpus, the planted BELOW 15const GI_UNMEASURED: i64 = 0 // an unmeasured corpus or threshold 16 17func main() -> i64 { 18 gv_puts("=== nx_intlog gate (integer log2 Q10 + idf + tf-saturation KATs + crossover side) ===\n" as *u8) 19 let ctr: *i64 = gv_ctr() 20 21 // T1 exact powers of two 22 var t1: i64 = 1 23 if ilog2_1024(1) != 0 { t1 = 0 } 24 if ilog2_1024(2) != 1024 { t1 = 0 } 25 if ilog2_1024(1024) != 10240 { t1 = 0 } 26 if ilog2_1024(1048576) != 20480 { t1 = 0 } 27 gv_check("T1 exact on powers of two (1,2,2^10,2^20)" as *u8, t1, ctr) 28 29 // T2 tight between powers: log2(3)=1.58496 -> 1623.0; accept +-2 30 let l3: i64 = ilog2_1024(3) 31 var t2: i64 = 0 32 if l3 >= 1621 { if l3 <= 1625 { t2 = 1 } } 33 gv_check("T2 log2(3) within +-2/1024 of 1623" as *u8, t2, ctr) 34 35 // T3 monotonic over a sweep 36 var t3: i64 = 1 37 var prev: i64 = 0 - 1 38 var x: i64 = 1 39 while x < 5000 { 40 let v: i64 = ilog2_1024(x) 41 if v < prev { t3 = 0 } 42 prev = v 43 x = x + 7 44 } 45 gv_check("T3 monotonic (1..5000 step 7)" as *u8, t3, ctr) 46 47 // T4 large-domain safety: 2^46 exact, no overflow 48 var t4: i64 = 0 49 if ilog2_1024(70368744177664) == 47104 { t4 = 1 } 50 gv_check("T4 2^46 -> 46*1024 (top-of-domain, overflow-safe)" as *u8, t4, ctr) 51 52 // T5 idf behavior: rare >> common; everywhere-term ~0 and never negative 53 let rare: i64 = idf_q10(1000, 1) 54 let common: i64 = idf_q10(1000, 500) 55 let all: i64 = idf_q10(1000, 1000) 56 var t5: i64 = 0 57 if rare > common { if common > all { if all >= 0 { if all <= 4 { t5 = 1 } } } } 58 gv_check("T5 idf: rare>common>everywhere~=0, floored at 0" as *u8, t5, ctr) 59 60 // T6 tf saturation: increasing, capped near (k1+1)=2252, tf1 = 2252*1024/(1024+1228)=1024ish 61 let s1: i64 = tfsat_q10(1) 62 let s5: i64 = tfsat_q10(5) 63 let s50: i64 = tfsat_q10(50) 64 var t6: i64 = 0 65 if s1 >= 1020 { if s1 <= 1028 { if s5 > s1 { if s50 > s5 { if s50 <= 2252 { if tfsat_q10(0) == 0 { t6 = 1 } } } } } } 66 gv_check("T6 tf-saturation: tf1~=1024, increasing, bounded by 2252, tf0=0" as *u8, t6, ctr) 67 68 // T7 length-norm: at average length it reduces EXACTLY to tfsat (b=0 stays a pinned special case) 69 var t7: i64 = 1 70 if tfnorm_q10(1, 1024) != tfsat_q10(1) { t7 = 0 } 71 if tfnorm_q10(7, 1024) != tfsat_q10(7) { t7 = 0 } 72 gv_check("T7 tfnorm at avg length == tfsat (b=0 special case pinned)" as *u8, t7, ctr) 73 74 // T8 verbosity correction: longer doc scores lower, shorter higher; bounds hold 75 var t8: i64 = 0 76 let sshort: i64 = tfnorm_q10(2, 512) 77 let savg: i64 = tfnorm_q10(2, 1024) 78 let slong: i64 = tfnorm_q10(2, 4096) 79 if sshort > savg { if savg > slong { if slong > 0 { if sshort <= 2252 { t8 = 1 } } } } 80 gv_check("T8 tfnorm: shorter>avg>longer, bounded" as *u8, t8, ctr) 81 82 // T9 crossover side (S1): the crossover tier itself is ABOVE, one token under it is BELOW, a web corpus is ABOVE 83 var t9: i64 = 1 84 if cs_crossover(GI_CROSSOVER_TOKENS, GI_CROSSOVER_TOKENS) != CS_SIDE_ABOVE { t9 = 0 } 85 if cs_crossover(GI_ONE_UNDER, GI_CROSSOVER_TOKENS) != CS_SIDE_BELOW { t9 = 0 } 86 if cs_crossover(GI_WEB_TOKENS, GI_CROSSOVER_TOKENS) != CS_SIDE_ABOVE { t9 = 0 } 87 gv_check("T9 crossover side: the crossover tier and above read ABOVE, one token under reads BELOW" as *u8, t9, ctr) 88 // T9b neg-control: a planted corpus on the OTHER side of the same crossover must answer the other side 89 var t9b: i64 = 0 90 if cs_crossover(GI_ONE_TOKEN, GI_CROSSOVER_TOKENS) == CS_SIDE_BELOW { if cs_crossover(GI_TWICE, GI_CROSSOVER_TOKENS) == CS_SIDE_ABOVE { t9b = 1 } } 91 gv_check("T9b neg-control-a-planted-corpus-on-the-other-side answers the other side" as *u8, t9b, ctr) 92 // T9c the third state (2026-09-14, folded in from nx_qrels_bench's own copy of this ruler): an unmeasured corpus or 93 // threshold abstains as UNMEASURED and never reads BELOW -- abstain, never acquit 94 var t9c: i64 = 0 95 if cs_crossover(GI_UNMEASURED, GI_CROSSOVER_TOKENS) == CS_SIDE_UNMEASURED { if cs_crossover(GI_ONE_TOKEN, GI_UNMEASURED) == CS_SIDE_UNMEASURED { if cs_crossover(GI_ONE_TOKEN, GI_CROSSOVER_TOKENS) == CS_SIDE_BELOW { t9c = 1 } } } 96 gv_check("T9c an unmeasured corpus or threshold abstains as UNMEASURED, never BELOW" as *u8, t9c, ctr) 97 98 // T10 S5 BM25Q query-side saturation (2026-09-15): qtf=1 is EXACTLY 1024 (a term seen once weighs what plain BM25 99 // gives it, the pre-declared anti-vacuity control), increasing, bounded by k+1, zero at zero; idf_bm25q returns the 100 // caller's idf UNCHANGED at qtf=1 for every idf in a doubling sweep, and a repeated term never weighs qtf times 101 gv_check_eq("T10 qtfsat_q10(1) is exactly 1024" as *u8, qtfsat_q10(1), 1024, ctr) 102 var t10a: i64 = 0 103 if qtfsat_q10(2) > qtfsat_q10(1) { if qtfsat_q10(10) > qtfsat_q10(2) { if qtfsat_q10(1000) > qtfsat_q10(10) { if qtfsat_q10(1000) <= 1024 + BM25Q_K_Q10 { if qtfsat_q10(0) == 0 { t10a = 1 } } } } } 104 gv_check("T10a qtf saturation: increasing, bounded by k+1, zero at zero" as *u8, t10a, ctr) 105 var t10b: i64 = 1 106 var sw: i64 = 1 107 while sw <= 4096 { if idf_bm25q(sw, 1) != sw { t10b = 0 } sw = sw * 2 } 108 gv_check("T10b idf_bm25q at qtf=1 returns every idf in a doubling sweep UNCHANGED (the anti-vacuity control)" as *u8, t10b, ctr) 109 var t10c: i64 = 0 110 if idf_bm25q(1024, 2) > 1024 { if idf_bm25q(1024, 2) < idf_bm25q(1024, 5) { if idf_bm25q(1024, 5) <= 2252 { if idf_bm25q(1024, 0) == 0 { t10c = 1 } } } } 111 gv_check("T10c idf_bm25q grows with qtf below (k+1) x idf and is zero at qtf=0" as *u8, t10c, ctr) 112 gv_check("neg-control-T10d a repeated term does NOT weigh qtf times: idf_bm25q(1024,2) is under 2048" as *u8, (idf_bm25q(1024, 2) < 2048) as i64, ctr) 113 // the values behind the teeth, so a second method can contradict a number and not only a PASS 114 gv_values_head() 115 gv_kv("ilog2_1024_of_3" as *u8, l3) 116 gv_kv("idf_q10_rare_1_of_1000" as *u8, rare) 117 gv_kv("idf_q10_everywhere" as *u8, all) 118 gv_kv("tfsat_q10_tf1" as *u8, s1) 119 gv_kv("tfnorm_q10_tf2_short" as *u8, sshort) 120 gv_kv("tfnorm_q10_tf2_long" as *u8, slong) 121 gv_kv("qtfsat_q10_qtf2" as *u8, qtfsat_q10(2)) 122 gv_kv("idf_bm25q_1024_qtf10" as *u8, idf_bm25q(1024, 10)) 123 124 return gv_verdict("NX-INTLOG-GATE" as *u8, ctr, "the integer log2 floor the BM25 rung stands on, its idf and tf-saturation behaviours, and the S1 crossover side, each pinned by a KAT" as *u8) 125}