nx_nofloat_prefix_cache_gate.nx source
↩ module page · 124 lines · 6010 B
1// nx_nofloat_prefix_cache_gate.nx -- proves the PREFIX-KV-CACHE speed optimization is BIT-EXACT + measures the
2// prefill-step savings (operator 2026-07-15: attack the ~2.4 tok/s prefill wall; coordinated with S2 = the
3// compiler owns the per-matmul 4.2x, this owns the ~10x FEWER prefill matmuls for the forge's fixed crib).
4//
5// The forge re-prefills a FIXED crib (~130 tok) on EVERY task. nsv_generate_pfx snapshots the crib's KV rows
6// once and restores them per task, prefilling only the task suffix. This gate proves the load-bearing property:
7// restore-snapshot + suffix-only-prefill produces output BYTE-IDENTICAL to a full prefill (bit-exactness is the
8// whole point of no-float). Same prompt, two paths:
9// A = full prefill, no cache (prefill = nprompt steps)
10// B = full prefill + snapshot rows 0..P (builds the cache)
11// C = restore rows 0..P + prefill [P..nprompt) (prefill = nprompt-P steps)
12// Teeth: T1 output(A) == output(C) BYTE-EXACT (the cache reuse is lossless) T2 cached prefill < baseline
13// T3 savings ratio reported (forge: crib~130 + task~15 => ~10x fewer prefill matmuls)
14// expect_exit: 0 license_tier: ORIGINAL
15import "nx_nofloat_serve_core.nx"
16import "nx_gate_verdict.nx"
17import "nx_stage_path.nx"
18
19func gw(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
20func gn(v: i64) -> i64 {
21 var m: i64 = v
22 if m < 0 { gw("-" as *u8); m = 0 - m }
23 let t: *u8 = sys_mmap(24)
24 var k: i64 = 0
25 if m == 0 { t[0] = 48 as u8; k = 1 }
26 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
27 let o: *u8 = sys_mmap(24)
28 var i: i64 = 0
29 while i < k { o[i] = t[k - 1 - i]; i = i + 1 }
30 sys_write(1, o, k)
31 return 0
32}
33
34func main() -> i64 {
35 gw("=== NX-NOFLOAT-PREFIX-CACHE -- prove KV-prefix reuse is BIT-EXACT + measure prefill savings ===\n" as *u8)
36 let mpath: *u8 = sp_path("nx_coder_model.gguf" as *u8, sys_mmap(SP_PATH_MAX))
37 sp_skip_unless("NOFLOAT-PREFIX-CACHE-GATE" as *u8, mpath)
38 let ir: i64 = nsv_init(mpath)
39 if ir != 0 { gw(" nsv_init FAILED rc=" as *u8); gn(ir); gw("\n" as *u8); return 2 }
40 gw(" model ready\n\n" as *u8)
41
42 let prompt: *u8 = "NishiLang program: write a function that returns the larger of two integers a and b." as *u8
43 var plen: i64 = 0
44 while prompt[plen] != (0 as u8) { plen = plen + 1 }
45
46 let outA: *u8 = sys_mmap(8192)
47 let outC: *u8 = sys_mmap(8192)
48 let meta: *i64 = sys_mmap(8*8) as *i64
49 let gp: *i64 = sys_mmap(16*8) as *i64
50 gp[1] = plen
51 gp[2] = 24 // max_new
52 gp[3] = 1 // mode 1 = i8 fast (deterministic; A and C share it)
53 gp[6] = meta as i64
54 gp[7] = 0 // no stream
55 gp[8] = 0 // greedy
56 gp[9] = 0
57 gp[10] = 0
58 gp[11] = 12345 // fixed seed
59 gp[12] = 0 // not chatml
60
61 // --- A: baseline full prefill, NO cache ---
62 gp[0] = prompt as i64
63 gp[4] = outA as i64
64 gp[5] = 8192
65 let na: i64 = nsv_generate_pfx(gp, 0, 0)
66 let nprompt: i64 = meta[0]
67 let msA: i64 = meta[2]
68
69 var P: i64 = nprompt - 4 // prefix = all but the last 4 tokens (the "crib")
70 if P < 1 { P = 1 }
71
72 // --- B: full prefill + SNAPSHOT rows 0..P-1 (build the cache) ---
73 gp[4] = outC as i64
74 gp[5] = 8192
75 nsv_generate_pfx(gp, P, 0)
76
77 // --- C: RESTORE rows 0..P-1 + prefill only [P..nprompt) ---
78 gp[4] = outC as i64
79 gp[5] = 8192
80 let nc: i64 = nsv_generate_pfx(gp, P, 1)
81 let msC: i64 = meta[2]
82
83 // bit-exact compare A vs C
84 var same: i64 = 1
85 if na != nc { same = 0 }
86 if same == 1 {
87 var k: i64 = 0
88 while k < na { if outA[k] != outC[k] { same = 0; k = na } else { k = k + 1 } }
89 }
90
91 gw(" prompt tokens (nprompt)=" as *u8); gn(nprompt)
92 gw(" prefix P=" as *u8); gn(P); gw(" suffix=" as *u8); gn(nprompt - P); gw("\n" as *u8)
93 gw(" PREFILL STEPS baseline=" as *u8); gn(nprompt); gw(" cached=" as *u8); gn(nprompt - P)
94 gw(" (saved " as *u8); gn(P); gw(" matmul passes/req)\n" as *u8)
95 gw(" wall ms baseline=" as *u8); gn(msA); gw(" cached=" as *u8); gn(msC); gw("\n" as *u8)
96 gw(" output bytes A=" as *u8); gn(na); gw(" C=" as *u8); gn(nc); gw("\n" as *u8)
97 // projected forge speedup (fixed crib ~130 tok + task ~15 tok)
98 let proj: i64 = (145 * 100) / 15 // baseline 145 prefill / cached 15 => ~9.6x
99 gw(" PROJECTED forge (crib 130 + task 15): prefill " as *u8); gn(145); gw(" -> " as *u8); gn(15)
100 gw(" steps = ~" as *u8); gn(proj / 100); gw("x fewer prefill matmuls (compounds with S2's 4.2x kernel)\n\n" as *u8)
101
102 var pass: i64 = 0
103 var ttl: i64 = 0
104 ttl = ttl + 1
105 gw(" T1 BIT-EXACT: restore+suffix-prefill output == full-prefill output (lossless cache): " as *u8)
106 if same == 1 { pass = pass + 1; gw("PASS\n" as *u8) } else { gw("FAIL (cache changed the output!)\n" as *u8) }
107 ttl = ttl + 1
108 gw(" T2 SAVINGS: cached prefill steps < baseline prefill steps: " as *u8)
109 if (nprompt - P) < nprompt { pass = pass + 1; gw("PASS\n" as *u8) } else { gw("FAIL\n" as *u8) }
110 ttl = ttl + 1
111 gw(" T3 NON-TRIVIAL: >= 1 output token produced (the run is real, not empty): " as *u8)
112 if na > 0 { pass = pass + 1; gw("PASS\n" as *u8) } else { gw("FAIL\n" as *u8) }
113
114 gw("NX-NOFLOAT-PREFIX-CACHE-GATE passed " as *u8); gn(pass); gw("/" as *u8); gn(ttl)
115 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
116 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
117 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
118 let ctr__dry: *i64 = gv_ctr()
119 ctr__dry[0] = pass
120 ctr__dry[1] = ttl
121 let rc__dry: i64 = gv_verdict("NOFLOAT-PREFIX-CACHE-GATE" as *u8, ctr__dry, "prefix-KV-cache is bit-exact + cuts prefill matmuls -- the forge's fixed-crib speed lever)" as *u8)
122 sys_exit_group(rc__dry)
123 return rc__dry
124}