nx_atp_to_derive.nx source
↩ module page · 97 lines · 4666 B
1// nx_atp_to_derive.nx -- bridge from ATP saturation proofs to
2// kernel-checkable nx_derive natural-deduction chains.
3//
4// Closes the gap between the substrate's two QED layers:
5// - Vampire-displacement: AUTOMATIC proof search via saturation
6// (resolution + paramod + factor + ...)
7// - nx_derive (kernel): verifies HUMAN-WRITTEN derivation chains
8// in natural deduction (modus ponens, etc.)
9//
10// This bridge takes an ATP-discovered proof (ProofLog) and emits a
11// DerivationChain the kernel can verify. Result: machine-discovered
12// derivations that are ALSO certificate-emittable. Few real provers
13// do both -- Vampire emits TSTP traces but no LCF-style certificate;
14// Coq/Lean check certificates but don't auto-discover proofs. This
15// substrate does both because the foundation supports it.
16//
17// Structural mapping (saturation rule -> closest natural-deduction
18// rule with matching arity):
19//
20// ATP rule -> nx_derive rule (arity)
21// -------- -- ----------- -----
22// INPUT (0-ary) -> AXIOM_CITATION (0)
23// RES (binary) -> CONTRADICTION (2)
24// FACTOR (unary) -> ALGEBRA_REWRITE (1)
25// PARAMOD (binary) -> SUBSTITUTION (2)
26// DEMOD (binary) -> SUBSTITUTION (2)
27// HYPERRES (>= binary) -> CONTRADICTION (2) [first 2 parents]
28// EQ_FACTOR (binary) -> SUBSTITUTION (2)
29// INST_GEN (binary) -> UNIVERSAL_INSTANT (1) [first parent]
30// DEDUP (unary) -> ALGEBRA_REWRITE (1)
31// AVATAR_SPLIT (unary) -> CONJUNCTION_ELIM (1)
32//
33// Caller supplies axiom_codes[i] for each INPUT entry (-1 if no
34// specific axiom applies; bridge then emits a placeholder NX_AX_PEANO_PA1
35// citation, kernel still verifies STRUCTURE).
36//
37// Bits-up nx_int.
38
39// nx_safety_envelope:
40// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
41// sil_target: SIL1
42// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
43// verdict: NOT_YET_EVALUATED
44
45import "nx_syscalls.nx"
46import "nx_runtime.nx"
47import "nx_tier.nx"
48import "nx_result.nx"
49import "nx_axioms.nx"
50import "nx_derive.nx"
51import "nx_proof_log.nx"
52
53// Map ATP rule code -> nx_derive rule code. Returns -1 for INPUT
54// (which uses the axiom-citation code path, not the step code path).
55func nx_atp_rule_to_drule(atp_rule: nx_int) -> nx_int {
56 if atp_rule == NX_PROOF_RULE_INPUT { return 0 - 1 }
57 if atp_rule == NX_PROOF_RULE_RES { return NX_DRULE_CONTRADICTION }
58 if atp_rule == NX_PROOF_RULE_FACTOR { return NX_DRULE_ALGEBRA_REWRITE }
59 if atp_rule == NX_PROOF_RULE_PARAMOD { return NX_DRULE_SUBSTITUTION }
60 if atp_rule == NX_PROOF_RULE_DEMOD { return NX_DRULE_SUBSTITUTION }
61 if atp_rule == NX_PROOF_RULE_HYPERRES { return NX_DRULE_CONTRADICTION }
62 if atp_rule == NX_PROOF_RULE_EQ_FACTOR { return NX_DRULE_SUBSTITUTION }
63 if atp_rule == NX_PROOF_RULE_INST_GEN { return NX_DRULE_UNIVERSAL_INSTANT }
64 if atp_rule == NX_PROOF_RULE_DEDUP { return NX_DRULE_ALGEBRA_REWRITE }
65 if atp_rule == NX_PROOF_RULE_AVATAR_SPLIT { return NX_DRULE_CONJ_ELIM }
66 return NX_DRULE_ALGEBRA_REWRITE // defensive: closest rewrite-class
67}
68
69// Convert a ProofLog into a DerivationChain. axiom_codes[] supplies
70// per-INPUT-entry axiom code (use NX_AX_* from nx_axioms or a
71// placeholder). Returns count of nodes emitted, or -1 on failure.
72func nx_atp_to_derive(log: *ProofLog, axiom_codes: *nx_int,
73 chain: *DerivationChain) -> nx_int {
74 var i: nx_int = 0
75 while i < log.n {
76 let entry: *ProofEntry = nx_proof_log_get(log, i)
77 if entry.rule == NX_PROOF_RULE_INPUT {
78 // Axiom citation. Caller-supplied axiom code; falls back
79 // to PEANO_PA1 if -1.
80 var ax: nx_int = axiom_codes[i]
81 if ax < 0 { ax = NX_AX_PEANO_PA1_ZERO_EXISTS }
82 let _id: i64 = nx_deriv_add_axiom(chain, i as i64, ax as i64)
83 } else {
84 // Internal step.
85 let drule: nx_int = nx_atp_rule_to_drule(entry.rule)
86 let arity: i64 = nx_drule_arity(drule as i64)
87 // Map premises per arity.
88 var pa: i64 = entry.parent_a as i64
89 var pb: i64 = entry.parent_b as i64
90 if arity == 1 { pb = 0 - 1 }
91 // arity 2 keeps both
92 let _id: i64 = nx_deriv_add_step(chain, i as i64, drule as i64, pa, pb)
93 }
94 i = i + 1
95 }
96 return chain.n_nodes as nx_int
97}