nx_embfeat_gate.nx source
↩ module page · 99 lines · 7253 B
1// nx_embfeat_gate.nx -- GATE for the embedding-feature library (nx_embfeat_lib), driven IN-PROCESS on a PLANTED pair of
2// models under /tmp/nx_embfeat_gate: a four-word PPMI vocabulary written through nx_wordclust's fixture writer (the
3// canonical NXPPMI1 shape) and a four-row NXEMB1 table written by the library's own fixture writer in the same sorted-hash
4// order. Proves: the pair loads, header fields read back, the scale is derived from the table (RMS then a half step),
5// a known word resolves to its own planted row and an unknown word reads -1, the bucket arithmetic (zero, one step,
6// minus one step, a clamp on both sides), the two-byte spelling, determinism across two loads, and the fail-closed
7// controls (a missing table, a table with a wrong magic). Every fixture asserts its own condition first. No network.
8// license_tier: ORIGINAL No hw writes (Rule 26).
9import "nx_syscalls.nx"
10import "nx_gatekit_lib.nx"
11import "nx_reviewmine_lib.nx"
12import "nx_wordclust.nx"
13import "nx_embfeat_lib.nx"
14import "nx_gate_verdict.nx"
15
16const G_ROOT: *u8 = "/tmp/nx_embfeat_gate"
17const G_PPMI: *u8 = "/tmp/nx_embfeat_gate/mini.ppmi"
18const G_EMB: *u8 = "/tmp/nx_embfeat_gate/mini.emb"
19const G_BADEMB: *u8 = "/tmp/nx_embfeat_gate/bad.emb"
20const G_MISSING: *u8 = "/tmp/nx_embfeat_gate/absent.emb"
21const G_I64: i64 = 8
22const G_NW: i64 = 4
23const G_DIM: i64 = 3
24const G_TABLE_BYTES: i64 = 120 // 24 + 4*3*8
25// planted rows (Q10): battery (1024, 0, -512) screen (0, 2048, 512) waiter (-1024, 0, 0) food (512, -512, 1024)
26// sum of squares = 1310720 + 4456448 + 1048576 + 1572864 = 8388608 over 12 coordinates -> mean 699050 -> integer root 836
27const G_EXPECT_RMS: i64 = 836
28const G_EXPECT_STEP: i64 = 418
29const G_CH_ZERO: i64 = 48
30const G_CH_AT: i64 = 64
31
32func main() -> i64 {
33 gv_head("=== nx_embfeat_gate -- dense embedding features from a planted PPMI vocabulary and NXEMB1 table ===" as *u8)
34 let c: *i64 = gv_ctr()
35 gk_mkdir(G_ROOT)
36 let wb: *u8 = sys_mmap(64)
37 let wo: *i64 = sys_mmap(G_NW * G_I64) as *i64
38 let wl: *i64 = sys_mmap(G_NW * G_I64) as *i64
39 let wx: *i64 = sys_mmap(G_NW * G_I64) as *i64
40 var w: i64 = 0
41 wo[0] = w; wl[0] = 7; wx[0] = 0; w = rm_catn(wb, w, "battery" as *u8, 7)
42 wo[1] = w; wl[1] = 6; wx[1] = 1; w = rm_catn(wb, w, "screen" as *u8, 6)
43 wo[2] = w; wl[2] = 6; wx[2] = 2; w = rm_catn(wb, w, "waiter" as *u8, 6)
44 wo[3] = w; wl[3] = 4; wx[3] = 3; w = rm_catn(wb, w, "food" as *u8, 4)
45 gv_check_eq("fixture-reached-the-condition: the planted PPMI vocabulary was written" as *u8, wc_plant_model(G_PPMI, wb, wo, wl, wx, G_NW), 1, c)
46 let vecs: *i64 = sys_mmap(G_NW * G_DIM * G_I64) as *i64
47 vecs[0] = 1024; vecs[1] = 0; vecs[2] = 0 - 512
48 vecs[3] = 0; vecs[4] = 2048; vecs[5] = 512
49 vecs[6] = 0 - 1024; vecs[7] = 0; vecs[8] = 0
50 vecs[9] = 512; vecs[10] = 0 - 512; vecs[11] = 1024
51 gv_check_eq("fixture-reached-the-condition: the planted embedding table was written" as *u8, ef_plant(G_EMB, wb, wo, wl, vecs, G_NW, G_DIM), 1, c)
52 gv_check_eq("fixture-reached-the-condition: the table has the format's exact byte count" as *u8, gk_size(G_EMB), G_TABLE_BYTES, c)
53 gv_check_eq("the-pair-loads" as *u8, ef_load(G_PPMI, G_EMB), 1, c)
54 gv_check_eq("header-nv-reads-back" as *u8, ef_nv_of(), G_NW, c)
55 gv_check_eq("header-dim-reads-back" as *u8, ef_dim_of(), G_DIM, c)
56 gv_check_eq("scale-is-derived-from-the-table: rms" as *u8, ef_rms_of(), G_EXPECT_RMS, c)
57 gv_check_eq("scale-is-derived-from-the-table: step is half the rms" as *u8, ef_step_of(), G_EXPECT_STEP, c)
58 let wbat: i64 = ef_wid("battery" as *u8, 7)
59 let wscr: i64 = ef_wid("screen" as *u8, 6)
60 gv_check("known-words-resolve" as *u8, ((wbat >= 0) & (wscr >= 0) & (wbat != wscr)) as i64, c)
61 gv_check_eq("a-known-word-reads-its-own-planted-row (battery coordinate 0)" as *u8, ef_coord(wbat, 0), 1024, c)
62 gv_check_eq("a-known-word-reads-its-own-planted-row (battery coordinate 2)" as *u8, ef_coord(wbat, 2), 0 - 512, c)
63 gv_check_eq("a-known-word-reads-its-own-planted-row (screen coordinate 1)" as *u8, ef_coord(wscr, 1), 2048, c)
64 gv_check_eq("neg-control-an-unknown-word-reads-minus-one" as *u8, ef_wid("zzzq" as *u8, 4), EF_NONE, c)
65 gv_check_eq("lookups-are-counted (three)" as *u8, ef_lookup_count(), 3, c)
66 gv_check_eq("hits-are-counted (two)" as *u8, ef_hit_count(), 2, c)
67 // bucket arithmetic at the derived step
68 gv_check_eq("bucket(0) = 0" as *u8, ef_bucket(0), 0, c)
69 gv_check_eq("bucket(step) = 1" as *u8, ef_bucket(G_EXPECT_STEP), 1, c)
70 gv_check_eq("bucket(-step) = -1" as *u8, ef_bucket(0 - G_EXPECT_STEP), 0 - 1, c)
71 gv_check_eq("bucket(2048) = 4 (2048 / 418 = 4.9, truncated)" as *u8, ef_bucket(2048), 4, c)
72 gv_check_eq("bucket-clamps-above (100 steps read the maximum)" as *u8, ef_bucket(100 * G_EXPECT_STEP), EF_BUCKET_MAX, c)
73 gv_check_eq("bucket-clamps-below" as *u8, ef_bucket(0 - 100 * G_EXPECT_STEP), 0 - EF_BUCKET_MAX, c)
74 // spelling
75 let sb: *u8 = sys_mmap(4)
76 gv_check_eq("spell-writes-two-bytes" as *u8, ef_spell(wbat, 0, sb), 2, c)
77 gv_check_eq("spell-first-byte-is-the-dimension" as *u8, sb[0] as i64, G_CH_ZERO, c)
78 gv_check_eq("spell-second-byte-is-the-bucket-offset-by-the-maximum (1024 / 418 = 2 -> '6')" as *u8, sb[1] as i64, G_CH_ZERO + EF_BUCKET_MAX + 2, c)
79 ef_spell(EF_NONE, 2, sb)
80 gv_check_eq("spell-of-an-unknown-word-is-the-dimension-and-an-at" as *u8, sb[1] as i64, G_CH_AT, c)
81 gv_check_eq("spell-of-an-unknown-word-keeps-the-dimension-byte" as *u8, sb[0] as i64, G_CH_ZERO + 2, c)
82 // determinism across two loads
83 let step1: i64 = ef_step_of()
84 gv_check_eq("second-load-succeeds" as *u8, ef_load(G_PPMI, G_EMB), 1, c)
85 gv_check_eq("second-load-derives-the-same-step" as *u8, ef_step_of(), step1, c)
86 gv_check_eq("second-load-resolves-battery-to-the-same-row" as *u8, ef_wid("battery" as *u8, 7), wbat, c)
87 // fail-closed controls
88 gv_check_eq("neg-control-missing-table-refuses-to-load" as *u8, ef_load(G_PPMI, G_MISSING), 0, c)
89 gv_check_eq("neg-control-after-a-refused-load-nothing-resolves" as *u8, ef_wid("battery" as *u8, 7), EF_NONE, c)
90 // a table with the wrong magic: the PPMI file itself has a different magic, so it is the wrong-magic control
91 gv_check_eq("neg-control-wrong-magic-refuses-to-load" as *u8, ef_load(G_PPMI, G_PPMI), 0, c)
92 gv_values_head()
93 gv_kv("nv" as *u8, G_NW)
94 gv_kv("dim" as *u8, G_DIM)
95 gv_kv("rms_q10" as *u8, G_EXPECT_RMS)
96 gv_kv("step_q10" as *u8, G_EXPECT_STEP)
97 gv_kv("battery_row" as *u8, wbat)
98 return gv_verdict("nx_embfeat_gate" as *u8, c, "the embedding-feature library proven on a planted PPMI vocabulary and NXEMB1 table: the pair loads, header fields read back, the scale is derived from the table (the rms of every coordinate, then a half step; the teeth print both), known words resolve to their own rows and an unknown reads -1 with lookups and hits counted, bucket arithmetic at the derived step with clamps both sides, the two-byte spelling with '@' for an unknown word, determinism across two loads, and three fail-closed controls (missing table, wrong magic, nothing resolves after a refusal); every fixture asserts its own condition first" as *u8)
99}