`nx_tstp_emit.nx` source

↩ module page · 110 lines · 4510 B
1// nx_tstp_emit.nx -- TSTP-format proof serializer.
2//
3// Walks the ProofLog + clause set and emits the proof in TSTP format:
4//
5//   cnf(c0, axiom, p(a)).
6//   cnf(c1, axiom, ~p(a)).
7//   cnf(c2, plain, $false, inference(resolution, [], [c0, c1])).
8//
9// Required for CASC submission output.  Closes the substrate-side of
10// the BLOCKED_ON_PROOF_HISTORY_TRACKING axis once integrated with the
11// saturation loop (this commit ships the standalone serializer; loop
12// integration is a follow-up).
13//
14// Output discipline: each clause emitted exactly once in proof order
15// (transitive ancestors of the empty clause first, then the empty
16// derivation last).  The caller can pre-walk via nx_proof_walk_ancestors
17// to determine the minimal proof support.
18
19// nx_safety_envelope:
20//   intended_use:       AUTO_APPLIED -- primitive-specific tuning queued
21//   sil_target:         SIL1
22//   evidence:           [bulk_applied_2026-05-16, see-file-comment-for-detail]
23//   verdict:            NOT_YET_EVALUATED
24
25import "nx_syscalls.nx"
26import "nx_runtime.nx"
27import "nx_tier.nx"
28import "nx_str.nx"
29import "nx_result.nx"
30import "nx_unify.nx"
31import "nx_resolution.nx"
32import "nx_tptp_symtab.nx"
33import "nx_tptp_emit.nx"
34import "nx_proof_log.nx"
35
36// Forward decl for the int->decimal helper from nx_tptp_emit (used
37// for clause name generation "c0", "c1", ...).  Defined there.
38func nx_int_to_decimal(n: nx_int, out: *u8) -> nx_int;
39
40// Emit one clause in TSTP form, with role + inference annotation.
41// Returns 1 on success, -1 on capacity overflow.
42func nx_tstp_emit_clause(c: *Clause, idx: nx_int, log: *ProofLog,
43                         symtab: *TptpSymtab, eq_sym: nx_int,
44                         buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int {
45    // "cnf(c<idx>, "
46    if nx_emit_str("cnf(c" as *u8, buf, pos, cap) < 0 { return 0 - 1 }
47    let idx_buf: *u8 = sys_mmap(32)
48    let _il: nx_int = nx_int_to_decimal(idx, idx_buf)
49    if nx_emit_str(idx_buf, buf, pos, cap) < 0 { return 0 - 1 }
50    if nx_emit_str(", " as *u8, buf, pos, cap) < 0 { return 0 - 1 }
51
52    // Role: "axiom" for INPUT, "plain" otherwise.  $false body for
53    // empty clauses.
54    let entry: *ProofEntry = nx_proof_log_get(log, idx)
55    var is_input: nx_int = 0
56    if (entry as nx_int) != 0 {
57        if entry.rule == NX_PROOF_RULE_INPUT { is_input = 1 }
58    }
59    if is_input == 1 {
60        if nx_emit_str("axiom, " as *u8, buf, pos, cap) < 0 { return 0 - 1 }
61    }
62    if is_input == 0 {
63        if nx_emit_str("plain, " as *u8, buf, pos, cap) < 0 { return 0 - 1 }
64    }
65
66    // Body
67    if nx_emit_clause_body(c, symtab, eq_sym, buf, pos, cap) < 0 { return 0 - 1 }
68
69    // Inference annotation (only for non-input)
70    if is_input == 0 {
71        if nx_emit_str(", inference(" as *u8, buf, pos, cap) < 0 { return 0 - 1 }
72        let rule_name: *u8 = nx_proof_rule_name(entry.rule)
73        if nx_emit_str(rule_name, buf, pos, cap) < 0 { return 0 - 1 }
74        if nx_emit_str(", [], [" as *u8, buf, pos, cap) < 0 { return 0 - 1 }
75        // First parent
76        if entry.parent_a >= 0 {
77            if nx_emit_str("c" as *u8, buf, pos, cap) < 0 { return 0 - 1 }
78            let pa_buf: *u8 = sys_mmap(32)
79            let _pl: nx_int = nx_int_to_decimal(entry.parent_a, pa_buf)
80            if nx_emit_str(pa_buf, buf, pos, cap) < 0 { return 0 - 1 }
81        }
82        if entry.parent_b >= 0 {
83            if nx_emit_str(", c" as *u8, buf, pos, cap) < 0 { return 0 - 1 }
84            let pb_buf: *u8 = sys_mmap(32)
85            let _pl2: nx_int = nx_int_to_decimal(entry.parent_b, pb_buf)
86            if nx_emit_str(pb_buf, buf, pos, cap) < 0 { return 0 - 1 }
87        }
88        if nx_emit_str("])" as *u8, buf, pos, cap) < 0 { return 0 - 1 }
89    }
90
91    if nx_emit_str(").\n" as *u8, buf, pos, cap) < 0 { return 0 - 1 }
92    return 1
93}
94
95// Emit the full proof: walk every entry in the log up to + including
96// the empty-clause derivation, in order.  `clauses` is the parallel
97// clause array; clauses[i] is the clause produced by inference log[i].
98func nx_tstp_emit_proof(clauses: *Clause, n_clauses: nx_int, log: *ProofLog,
99                        symtab: *TptpSymtab, eq_sym: nx_int,
100                        buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int {
101    var i: nx_int = 0
102    while i < n_clauses {
103        let c: *Clause = ((clauses as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
104        if nx_tstp_emit_clause(c, i, log, symtab, eq_sym, buf, pos, cap) < 0 {
105            return 0 - 1
106        }
107        i = i + 1
108    }
109    return 1
110}
nx_tstp_emit.nx source

`nx_tstp_emit.nx` source
