nx_vecexec_gate.nx source
↩ module page · 95 lines · 4599 B
1// nx_vecexec_gate.nx -- proves the vectorized operators are CORRECT (identical to a scalar reference) and
2// that they run over the zero-copy colframe. Correctness is deterministic and lives here; THROUGHPUT is
3// nondeterministic and is reported by the organ's `bench` verb, never faked in the gate. Hand-computed
4// known answers on a tiny frame + a cross-check against the scalar path on a larger random frame.
5// D001 verdict via nx_gate_verdict. expect_exit: 0 license_tier: ORIGINAL
6import "nx_gate_verdict.nx"
7import "nx_vecexec.nx"
8
9func vg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 }
10
11// build a colframe from two i64 arrays; returns the frame buffer
12func vg_frame2(a: *i64, b: *i64, na: *u8, nb: *u8, n: i64) -> *u8 {
13 let cols: *i64 = sys_mmap(8 * 2) as *i64
14 let names: *i64 = sys_mmap(8 * 2) as *i64
15 cols[0] = a as i64
16 cols[1] = b as i64
17 names[0] = na as i64
18 names[1] = nb as i64
19 let tot: i64 = cf_encoded_bytes(names, 2, n)
20 let f: *u8 = sys_mmap(tot + 64)
21 cf_encode(cols, names, 2, n, f)
22 return f
23}
24
25func main() -> i64 {
26 let ctr: *i64 = gv_ctr()
27 gv_head("nx_vecexec_gate -- vectorized operators, correct to the last integer, over the zero-copy frame" as *u8)
28
29 // ---- tiny hand-computed frame: key=[50,150,80,200,120], val=[1,2,3,4,5] ----------------------
30 let key: *i64 = sys_mmap(8 * 5) as *i64
31 let val: *i64 = sys_mmap(8 * 5) as *i64
32 key[0] = 50
33 key[1] = 150
34 key[2] = 80
35 key[3] = 200
36 key[4] = 120
37 val[0] = 1
38 val[1] = 2
39 val[2] = 3
40 val[3] = 4
41 val[4] = 5
42 let f: *u8 = vg_frame2(val, key, "val" as *u8, "key" as *u8, 5)
43
44 // SUM(val) = 15
45 gv_check("T1 vx_sum(val) == 15 (whole-column vectorized reduction)" as *u8, vg_eq(vx_sum(f, 0), 15), ctr)
46 // COUNT key>=100 -> rows 1(150),3(200),4(120) => 3
47 gv_check("T2 vx_count_ge(key,100) == 3" as *u8, vg_eq(vx_count_ge(f, 1, 100), 3), ctr)
48 // FILTER key>=100 -> sel = [1,3,4]; SUM(val over sel) = 2+4+5 = 11
49 let sel: *i64 = sys_mmap(8 * 8) as *i64
50 let ns: i64 = vx_filter_ge(f, 1, 100, sel)
51 gv_check("T3 vx_filter_ge(key,100) selects 3 rows" as *u8, vg_eq(ns, 3), ctr)
52 var selok: i64 = 0
53 if sel[0] == 1 { if sel[1] == 3 { if sel[2] == 4 { selok = 1 } } }
54 gv_check("T4 the selection vector holds the RIGHT row indices in order [1,3,4]" as *u8, selok, ctr)
55 gv_check("T5 SUM(val) WHERE key>=100 == 11 (filter->select->gather, hand-computed)" as *u8, vg_eq(vx_sum_where_ge(f, 0, 1, 100, sel), 11), ctr)
56
57 // ---- edges: empty and all-pass --------------------------------------------------------------
58 gv_check("T6 threshold above max -> empty selection, sum 0" as *u8, vg_eq(vx_sum_where_ge(f, 0, 1, 9999, sel), 0), ctr)
59 gv_check("T7 threshold below min -> all rows pass (count 5)" as *u8, vg_eq(vx_count_ge(f, 1, 0), 5), ctr)
60
61 // ---- CROSS-CHECK vs the scalar tuple-at-a-time reference on a LARGER random frame ------------
62 // this crosses the batch boundary (N > VX_VEC) so it exercises multi-vector execution.
63 let N: i64 = 5000
64 let bk: *i64 = sys_mmap(8 * N) as *i64
65 let bv: *i64 = sys_mmap(8 * N) as *i64
66 var s: i64 = 999
67 var i: i64 = 0
68 while i < N {
69 s = (s * 1103515245 + 12345) & 0x7fffffff
70 bk[i] = s % 200
71 bv[i] = s % 1000
72 i = i + 1
73 }
74 let bf: *u8 = vg_frame2(bv, bk, "val" as *u8, "key" as *u8, N)
75 let bsel: *i64 = sys_mmap(8 * N) as *i64
76 let vec: i64 = vx_sum_where_ge(bf, 0, 1, 137, bsel)
77 let scl: i64 = vx_scalar_sum_where_ge(bf, 0, 1, 137)
78 gv_check("T8 vectorized == scalar on a 5000-row frame across MANY vectors (SUM(val) WHERE key>=137)" as *u8, vg_eq(vec, scl), ctr)
79 // whole-column vectorized sum == a plain reference sum
80 var ref: i64 = 0
81 i = 0
82 while i < N { ref = ref + bv[i]; i = i + 1 }
83 gv_check("T9 vx_sum over 5000 rows == the plain reference total (batch reduction is exact)" as *u8, vg_eq(vx_sum(bf, 0), ref), ctr)
84
85 // ---- it genuinely runs over the ZERO-COPY frame (composes nx_colframe): the operator read the
86 // column via cf_col, so mutating the SOURCE arrays after encode must not change the result -------
87 bv[0] = 777777
88 bk[0] = 0
89 let vec2: i64 = vx_sum_where_ge(bf, 0, 1, 137, bsel)
90 gv_check("T10 the operators read the FRAME (snapshot), not the mutated source arrays" as *u8, vg_eq(vec2, vec), ctr)
91
92 let rc: i64 = gv_verdict("VECEXEC-GATE" as *u8, ctr, "vectorized filter/aggregate operators, integer-exact vs scalar, over the zero-copy columnar frame" as *u8)
93 sys_exit(rc)
94 return rc
95}