nx_autoformalize_cap_probe.nx source
↩ module page · 46 lines · 2184 B
1// nx_autoformalize_cap_probe.nx -- what does the 8-token cap in af_parse ACTUALLY do?
2//
3// Debt 1785521261 claimed it produces a WELL-FORMED FORMALIZATION OF A WEAKER STATEMENT (silently
4// dropping trailing constraints). Reading the consumer suggests otherwise: it accepts ONLY nt==3 or
5// nt==5 and returns 0 for anything else, so a 9+ token sentence truncated to 8 should match NEITHER
6// shape and REFUSE. This probe settles which is true by RUNNING it, because a wrong debt is worse than
7// no debt -- it sends the next person to fix something that is not broken.
8// expect_exit: 0 license_tier: ORIGINAL
9
10import "nx_syscalls.nx"
11import "nx_autoformalize_lib.nx"
12
13func ac_w(s: *u8) -> i64 {
14 var n: i64 = 0
15 while s[n] != (0 as u8) { n = n + 1 }
16 sys_write(1, s, n)
17 return 0
18}
19
20func main() -> i64 {
21 let res: *u8 = sys_mmap(64)
22
23 // 3-token form: "5 is 5" -> should PARSE (rc=1).
24 let ok3: i64 = af_parse("5 is 5" as *u8, res)
25 if ok3 != 1 { ac_w("T1 FAIL: 3-token form did not parse\n" as *u8); return 1 }
26 ac_w("T1 three_token PASS a 3-token sentence formalizes (rc=1)\n" as *u8)
27
28 // 5-token form: "2 plus 3 is 5" -> should PARSE.
29 let ok5: i64 = af_parse("2 plus 3 is 5" as *u8, res)
30 if ok5 != 1 { ac_w("T2 FAIL: 5-token form did not parse\n" as *u8); return 2 }
31 ac_w("T2 five_token PASS a 5-token sentence formalizes (rc=1)\n" as *u8)
32
33 // OVER-CAP: 11 semantic tokens. Truncated to 8, it matches neither nt==3 nor nt==5.
34 // If the cap REFUSES (rc=0) the debt's premise is wrong; if it returns 1 the debt was right.
35 let over: i64 = af_parse("2 plus 3 plus 4 plus 5 plus 6 is 20" as *u8, res)
36 if over == 1 {
37 ac_w("T3 over_cap FOUND: over-cap sentence FORMALIZED anyway -- debt 1785521261 CONFIRMED\n" as *u8)
38 return 3
39 }
40 ac_w("T3 over_cap PASS over-cap sentence REFUSED (rc=0), not silently weakened\n" as *u8)
41
42 ac_w("\nVERDICT: the 8-token cap FAILS CLOSED via the nt==3 / nt==5 shape check.\n" as *u8)
43 ac_w("Truncation cannot produce a weaker-but-valid formalization here.\n" as *u8)
44 ac_w("AUTOFORMALIZE-CAP-PROBE OK\n" as *u8)
45 return 0
46}