nx_autoformalize_lib.nx
buildroot/runtime/nx_autoformalize_lib.nx
about
nx_autoformalize_lib.nx -- the CANONICAL autoformalization library (pure funcs, no main), extracted
2026-07-15 from nx_autoformalize.nx so other organs can compose the verifier (the propose->verify loop:
an LLM PROPOSES, this kernel-backed checker DISPOSES). Same code, zero behavior change; the organ's own
gate battery re-proves it after the split.
af_decide(claim, vb) -> 1 PROVED · 2 REFUTED · 3 UNSUPPORTED · 5 NO-SOLUTION · -1 kernel failure
Grammar: "<n|what> [plus|times <n|what>] =|equals|is|<|under|<= <n>", digits or words zero..twelve;
plus operands <= 12, times operands <= 6, rhs <= 144. Everything derives through the LCF v2 kernel
(nx_k2_verify checks the whole chain; a wrong claim CANNOT certify -- soundness by construction).
license_tier: ORIGINAL (lib: no main -- build standalone gives rc=102 by design)
dependencies 1 imports · 3 importers
imports: nx_arith.nx
imported by: nx_autoformalize.nxnx_autoformalize_cap_probe.nxnx_propose_verify_lib.nx
structs
| none |
consts
| none |
functions
| 12 | func af_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } |
| 13 | func af_n(v: i64) -> i64 |
| 26 | func af_streq(a: *u8, b: *u8) -> i64 { var i: i64 = 0; while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 } if b[i] != (0 as u8) { return 0 } return 1 } |
| 29 | func af_tok_num(t: *u8) -> i64 |
| 53 | func af_tok_plus(t: *u8) -> i64 { if af_streq(t, "+" as *u8) == 1 { return 1 } if af_streq(t, "plus" as *u8) == 1 { return 1 } return 0 } |
| 54 | func af_tok_times(t: *u8) -> i64 { if af_streq(t, "*" as *u8) == 1 { return 1 } if af_streq(t, "times" as *u8) == 1 { return 1 } return 0 } |
| 55 | func af_tok_eqw(t: *u8) -> i64 { if af_streq(t, "=" as *u8) == 1 { return 1 } if af_streq(t, "equals" as *u8) == 1 { return 1 } if af_streq(t, "is" as *u8) == 1 { return 1 } return 0 } |
| 56 | func af_tok_lt(t: *u8) -> i64 { if af_streq(t, "<" as *u8) == 1 { return 1 } if af_streq(t, "under" as *u8) == 1 { return 1 } return 0 } |
| 57 | func af_tok_unknown(t: *u8) -> i64 { if af_streq(t, "what" as *u8) == 1 { return 1 } if af_streq(t, "x" as *u8) == 1 { return 1 } return 0 } |
| 58 | func af_tok_le(t: *u8) -> i64 { if af_streq(t, "<=" as *u8) == 1 { return 1 } return 0 } |
| 66 | func af_parse(s: *u8, res: *i64) -> i64 called by 3: mainaf_decidepvx_route calls 7: af_tok_numaf_tok_plusaf_tok_timesaf_tok_leaf_tok_ltaf_tok_unknown+1 |
| 160 | func af_rel_term(sym: i64, x: *Term, y: *Term) -> *Term |
| 172 | func af_derive_lt(ch: *K2Chain, u: i64, v: i64, stepsbox: *i64) -> i64 called by 2: af_derive_leaf_decide calls 8: af_derive_sumnx_k2_axiomnx_k2_impnx_k2_eqnx_arith_plusnx_arith_nat+2 |
| 190 | func af_derive_le(ch: *K2Chain, u: i64, v: i64, stepsbox: *i64) -> i64 |
| 216 | func af_derive_sum(ch: *K2Chain, a: i64, b: i64, stepsbox: *i64) -> i64 |
| 252 | func af_derive_mult(ch: *K2Chain, a: i64, b: i64, stepsbox: *i64) -> i64 called by 1: af_decide calls 10: nx_arith_natnx_k2_axiomnx_k2_eqnx_arith_multnx_arith_zeronx_arith_plus+4 |
| 286 | func af_decide(claim: *u8, vb: i64) -> i64 called by 7: mainmainmainmainmainpvx_case+1 calls 21: af_parseaf_wnx_k2_chain_newnx_arith_natnx_arith_plusnx_arith_mult+15 |