nx_proof_log.nx source

1// nx_proof_log.nx -- inference history tracking. 2// 3// Side table recording, per derived clause, the inference rule + parent 4// clause indices. Foundation for TSTP-format proof certificate 5// emission required by CASC submissions (LOSE -> WIN on the 6// "proof certificate output" axis of the honest CASC verdict). 7// 8// API: 9// nx_proof_log_new(cap) -> *ProofLog 10// nx_proof_log_add(log, rule, parent_a, parent_b) -> entry_idx 11// nx_proof_log_walk_unsat(log, empty_idx, visited[]) -> count 12// (transitive parent walk from the empty clause back to inputs -- 13// the "minimal proof support" set) 14// 15// Caller threading is the saturation loop's responsibility. A clause 16// index in `log` corresponds 1:1 to its index in the clause set the 17// loop manages. Input clauses get NX_PROOF_RULE_INPUT with parents -1. 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_result.nx" 29 30// Sealed rule enum. 31const NX_PROOF_RULE_INPUT: nx_int = 0 32const NX_PROOF_RULE_RES: nx_int = 1 // binary resolution 33const NX_PROOF_RULE_FACTOR: nx_int = 2 34const NX_PROOF_RULE_PARAMOD: nx_int = 3 35const NX_PROOF_RULE_DEMOD: nx_int = 4 36const NX_PROOF_RULE_HYPERRES: nx_int = 5 // N-electron hyperresolution 37const NX_PROOF_RULE_EQ_FACTOR: nx_int = 6 38const NX_PROOF_RULE_INST_GEN: nx_int = 7 39const NX_PROOF_RULE_DEDUP: nx_int = 8 // literal dedup (preprocessing) 40const NX_PROOF_RULE_AVATAR_SPLIT: nx_int = 9 41 42func nx_proof_rule_name(r: nx_int) -> *u8 { 43 if r == NX_PROOF_RULE_INPUT { return "input" as *u8 } 44 if r == NX_PROOF_RULE_RES { return "resolution" as *u8 } 45 if r == NX_PROOF_RULE_FACTOR { return "factoring" as *u8 } 46 if r == NX_PROOF_RULE_PARAMOD { return "paramodulation" as *u8 } 47 if r == NX_PROOF_RULE_DEMOD { return "demodulation" as *u8 } 48 if r == NX_PROOF_RULE_HYPERRES { return "hyperresolution" as *u8 } 49 if r == NX_PROOF_RULE_EQ_FACTOR { return "equality_factoring" as *u8 } 50 if r == NX_PROOF_RULE_INST_GEN { return "instance_generation" as *u8 } 51 if r == NX_PROOF_RULE_DEDUP { return "literal_dedup" as *u8 } 52 if r == NX_PROOF_RULE_AVATAR_SPLIT { return "avatar_split" as *u8 } 53 return "?" as *u8 54} 55 56struct ProofEntry { 57 rule: nx_int, 58 parent_a: nx_int, // -1 if not applicable (e.g. INPUT) 59 parent_b: nx_int, // -1 if unary inference 60} 61const NX_PROOF_ENTRY_BYTES: nx_int = 24 62 63struct ProofLog { 64 entries: *ProofEntry, 65 n: nx_int, 66 cap: nx_int, 67} 68const NX_PROOF_LOG_BYTES: nx_int = 24 69 70func nx_proof_log_new(cap: nx_int) -> *ProofLog { 71 let log: *ProofLog = (sys_mmap(NX_PROOF_LOG_BYTES as i64)) as *ProofLog 72 log.entries = (sys_mmap((cap * NX_PROOF_ENTRY_BYTES) as i64)) as *ProofEntry 73 log.n = 0 74 log.cap = cap 75 return log 76} 77 78// Append an entry; returns its index in the log or -1 on overflow. 79func nx_proof_log_add(log: *ProofLog, rule: nx_int, 80 parent_a: nx_int, parent_b: nx_int) -> nx_int { 81 if log.n >= log.cap { return 0 - 1 } 82 let slot: *ProofEntry = ((log.entries as nx_int) + (log.n * NX_PROOF_ENTRY_BYTES)) as *ProofEntry 83 slot.rule = rule 84 slot.parent_a = parent_a 85 slot.parent_b = parent_b 86 let idx: nx_int = log.n 87 log.n = log.n + 1 88 return idx 89} 90 91func nx_proof_log_get(log: *ProofLog, i: nx_int) -> *ProofEntry { 92 if i < 0 { return 0 as *ProofEntry } 93 if i >= log.n { return 0 as *ProofEntry } 94 return ((log.entries as nx_int) + (i * NX_PROOF_ENTRY_BYTES)) as *ProofEntry 95} 96 97// Walk transitively from `start_idx` upward through parent_a/parent_b, 98// marking every ancestor in `visited[]` (caller-allocated bitfield 99// sized at least log.cap). Returns the count of distinct ancestors 100// visited. Used to compute the "proof support" -- the minimal set of 101// input clauses + intermediate derivations needed to justify the empty 102// clause. 103func nx_proof_walk_ancestors(log: *ProofLog, start_idx: nx_int, 104 visited: *nx_int) -> nx_int { 105 if start_idx < 0 { return 0 } 106 if start_idx >= log.n { return 0 } 107 if visited[start_idx] == 1 { return 0 } 108 visited[start_idx] = 1 109 110 let e: *ProofEntry = nx_proof_log_get(log, start_idx) 111 var count: nx_int = 1 112 if (e as nx_int) != 0 { 113 if e.parent_a >= 0 { 114 count = count + nx_proof_walk_ancestors(log, e.parent_a, visited) 115 } 116 if e.parent_b >= 0 { 117 count = count + nx_proof_walk_ancestors(log, e.parent_b, visited) 118 } 119 } 120 return count 121}