nx_propose_verify_lib.nx source
↩ module page · 176 lines · 7435 B
1// nx_propose_verify_lib.nx -- the PROPOSE->VERIFY primitive as a reusable LIBRARY (2026-07-15): few-shot
2// templating + greedy no-float generation (through the PRODUCTION serve core) + first-integer proposal
3// parse + concrete-claim building for kernel certification. Composes nx_nofloat_serve_core (the PROPOSER)
4// and nx_autoformalize_lib (the DISPOSER: af_decide -- a wrong proposal cannot certify, soundness by
5// construction). This is the autonomous-building safety primitive: generator proposes, sound checker
6// disposes, nothing unverified is trusted. Consumers: nx_propose_verify (organ/CLI) + the probe gates
7// nx_nofloat_propose_verify_gate / nx_nofloat_propose_solve_gate (single source of truth for the templates:
8// the gates measure EXACTLY the code path the organ serves).
9// Caller must nsv_init(<gguf path>) ONCE before pvl_generate (and RETURN from main -- pool-worker reap).
10// license_tier: ORIGINAL (lib: no main -- build standalone gives rc=102 by design)
11import "nx_nofloat_serve_core.nx"
12import "nx_autoformalize_lib.nx"
13
14// first unsigned-integer run in s[0,n) -> res[0]=found(0/1) res[1]=value. Returns res[0].
15func pvl_first_uint(s: *u8, n: i64, res: *i64) -> i64 {
16 res[0] = 0
17 res[1] = 0
18 var i: i64 = 0
19 var v: i64 = 0
20 var inrun: i64 = 0
21 while i < n {
22 let c: i64 = s[i] as i64
23 var isd: i64 = 0
24 if c >= 48 { if c <= 57 { isd = 1 } }
25 if isd == 1 {
26 inrun = 1
27 if v < 1000000 { v = v * 10 + (c - 48) }
28 i = i + 1
29 } else {
30 if inrun == 1 { i = n } else { i = i + 1 }
31 }
32 }
33 if inrun == 1 { res[0] = 1; res[1] = v }
34 return res[0]
35}
36
37// COMPLETION prompt: 3-shot few-shot, question ends at "equals" -> the model proposes c.
38func pvl_prompt_complete(dst: *u8, a: i64, b: i64, op: i64) -> i64 {
39 var o: i64 = 0
40 if op == 1 { o = nsv_cat(dst, o, "2 plus 2 equals 4. 3 plus 5 equals 8. 10 plus 1 equals 11. " as *u8) } else { o = nsv_cat(dst, o, "2 times 3 equals 6. 4 times 2 equals 8. 5 times 3 equals 15. " as *u8) }
41 o = nsv_catn(dst, o, a)
42 if op == 1 { o = nsv_cat(dst, o, " plus " as *u8) } else { o = nsv_cat(dst, o, " times " as *u8) }
43 o = nsv_catn(dst, o, b)
44 o = nsv_cat(dst, o, " equals" as *u8)
45 dst[o] = 0 as u8
46 return o
47}
48
49// SOLVE prompt: 3-shot inversion, question ends with '?' -> the model proposes the unknown x.
50// slot 1 = unknown first ("what plus k equals c?"), slot 2 = unknown second ("k plus what equals c?").
51func pvl_prompt_solve(dst: *u8, k: i64, c: i64, op: i64, slot: i64) -> i64 {
52 var o: i64 = 0
53 if op == 1 {
54 if slot == 1 { o = nsv_cat(dst, o, "what plus 4 equals 6? 2. what plus 6 equals 13? 7. what plus 3 equals 12? 9. what plus " as *u8) } else { o = nsv_cat(dst, o, "2 plus what equals 5? 3. 7 plus what equals 10? 3. 5 plus what equals 13? 8. " as *u8) }
55 } else {
56 if slot == 1 { o = nsv_cat(dst, o, "what times 2 equals 6? 3. what times 3 equals 12? 4. what times 5 equals 10? 2. what times " as *u8) } else { o = nsv_cat(dst, o, "2 times what equals 10? 5. 4 times what equals 8? 2. 3 times what equals 9? 3. " as *u8) }
57 }
58 if slot == 1 {
59 o = nsv_catn(dst, o, k)
60 o = nsv_cat(dst, o, " equals " as *u8)
61 o = nsv_catn(dst, o, c)
62 o = nsv_cat(dst, o, "?" as *u8)
63 } else {
64 o = nsv_catn(dst, o, k)
65 if op == 1 { o = nsv_cat(dst, o, " plus what equals " as *u8) } else { o = nsv_cat(dst, o, " times what equals " as *u8) }
66 o = nsv_catn(dst, o, c)
67 o = nsv_cat(dst, o, "?" as *u8)
68 }
69 dst[o] = 0 as u8
70 return o
71}
72
73// greedy i32 raw generation through the production serve path. Returns generated-text length (-1 err).
74// mt = the nsv meta out ([0]=n_prompt [1]=n_gen [2]=ms_total [3]=ms/tok [4]=eos [5]=err).
75func pvl_generate(pb: *u8, plen: i64, tx: *u8, mt: *i64, max_new: i64) -> i64 {
76 let gp: *i64 = sys_mmap(16 * 8) as *i64
77 gp[0] = pb as i64
78 gp[1] = plen
79 gp[2] = max_new
80 gp[3] = 0
81 gp[4] = tx as i64
82 gp[5] = 4000
83 gp[6] = mt as i64
84 gp[7] = 0 - 1
85 gp[8] = 0
86 gp[9] = 0
87 gp[10] = 0
88 gp[11] = 0
89 gp[12] = 0
90 return nsv_generate(gp)
91}
92
93// LAST unsigned-integer run in s[0,n) -> res[0]=found(0/1) res[1]=value. Returns res[0]. The chat-instrument
94// (v2) extraction: instruct models answer in sentences ("The number is 7 - 3 = 4.") where the FINAL integer
95// is the answer position -- first-int mis-extracts operands. Use with EOS-complete generation (max_new high
96// enough that the reply finishes) so the final integer is really final.
97func pvl_last_uint(s: *u8, n: i64, res: *i64) -> i64 {
98 res[0] = 0
99 res[1] = 0
100 var i: i64 = 0
101 var v: i64 = 0
102 var inrun: i64 = 0
103 var found: i64 = 0
104 var lastv: i64 = 0
105 while i < n {
106 let c: i64 = s[i] as i64
107 var isd: i64 = 0
108 if c >= 48 { if c <= 57 { isd = 1 } }
109 if isd == 1 {
110 if inrun == 0 { v = 0 }
111 inrun = 1
112 if v < 1000000 { v = v * 10 + (c - 48) }
113 } else {
114 if inrun == 1 { found = 1; lastv = v }
115 inrun = 0
116 }
117 i = i + 1
118 }
119 if inrun == 1 { found = 1; lastv = v }
120 if found == 1 { res[0] = 1; res[1] = lastv }
121 return res[0]
122}
123
124// CHAT-mode SOLVE prompt: a natural-language question for the serve's ChatML path (nsv_chatml_ids wraps it
125// in <|im_start|>user ... <|im_end|><|im_start|>assistant turn structure -- the instruct-tuned surface).
126// slot 1: "What number plus k equals c?" slot 2: "k plus what number equals c?" Both end with the
127// answer-format instruction so the reply parses as a bare integer.
128func pvl_prompt_solve_chat(dst: *u8, k: i64, c: i64, op: i64, slot: i64) -> i64 {
129 var o: i64 = 0
130 if slot == 1 {
131 o = nsv_cat(dst, o, "What number " as *u8)
132 if op == 1 { o = nsv_cat(dst, o, "plus " as *u8) } else { o = nsv_cat(dst, o, "times " as *u8) }
133 o = nsv_catn(dst, o, k)
134 o = nsv_cat(dst, o, " equals " as *u8)
135 o = nsv_catn(dst, o, c)
136 } else {
137 o = nsv_catn(dst, o, k)
138 if op == 1 { o = nsv_cat(dst, o, " plus what number equals " as *u8) } else { o = nsv_cat(dst, o, " times what number equals " as *u8) }
139 o = nsv_catn(dst, o, c)
140 }
141 o = nsv_cat(dst, o, "? Answer with only the number." as *u8)
142 dst[o] = 0 as u8
143 return o
144}
145
146// greedy i32 generation through the serve's CHATML path (gp[12]=1) -- identical to pvl_generate otherwise.
147func pvl_generate_chat(pb: *u8, plen: i64, tx: *u8, mt: *i64, max_new: i64) -> i64 {
148 let gp: *i64 = sys_mmap(16 * 8) as *i64
149 gp[0] = pb as i64
150 gp[1] = plen
151 gp[2] = max_new
152 gp[3] = 0
153 gp[4] = tx as i64
154 gp[5] = 4000
155 gp[6] = mt as i64
156 gp[7] = 0 - 1
157 gp[8] = 0
158 gp[9] = 0
159 gp[10] = 0
160 gp[11] = 0
161 gp[12] = 1
162 return nsv_generate(gp)
163}
164
165// build the concrete claim "<x> <plus|times> <y> equals <c>" into dst; prm = [x, y, op, c]. Returns len.
166// Feed the result to af_decide for the kernel verdict (1 PROVED / 2 REFUTED / 3 UNSUPPORTED).
167func pvl_claim(dst: *u8, prm: *i64) -> i64 {
168 var o: i64 = 0
169 o = nsv_catn(dst, o, prm[0])
170 if prm[2] == 1 { o = nsv_cat(dst, o, " plus " as *u8) } else { o = nsv_cat(dst, o, " times " as *u8) }
171 o = nsv_catn(dst, o, prm[1])
172 o = nsv_cat(dst, o, " equals " as *u8)
173 o = nsv_catn(dst, o, prm[3])
174 dst[o] = 0 as u8
175 return o
176}