nx_ot_replay.nx source

1// nx_ot_replay.nx -- OpenTheory replay engine. 2// 3// Per user 2026-05-15: "world class". Per the comparison-engine 4// commit's named improvement for library_size LOSE_BIG vs HOL Light. 5// 6// OpenTheory is the kernel-independent proof-exchange format from 7// gilith.com/opentheory/article.html. HOL kernels (HOL Light, HOL4, 8// ProofPower, Isabelle/HOL) export their proofs as a list of stack 9// machine instructions; any HOL-compatible kernel can replay them 10// and re-derive each theorem natively. 11// 12// THIS ENGINE: a stack-based interpreter that executes OpenTheory- 13// style instructions. Each opcode that produces a Theorem dispatches 14// to a v2 kernel emitter, so every replayed theorem becomes a real 15// kernel-checked chain in our K2Chain. No third-party trust: the 16// source is the input, OUR kernel is the verifier. 17// 18// Every successful `thm` opcode registers an entry in the supplied 19// LemmaLib with NX_LEMMA_PROVED_NATIVE_REPLAYED status. This is the 20// honest framing per [[feedback-no-third-party-trust-native-or-nothing]]: 21// the proof BODY was replayed natively; the SOURCE is preserved as 22// provenance metadata. 23// 24// What this commit ships: 25// - Stack machine + 8 opcodes (num, term, axiom, refl, mp, assume, 26// imp_intro, thm) 27// - Programmatic replay (caller assembles an instruction array) 28// Named follow-up: 29// - .ot file parser (read ASCII OpenTheory format from file) 30// - Full opcode coverage (absTerm, appTerm, defineConst, subst, 31// deductAntisym, eqMp, etc. -- ~30 total) 32 33// nx_safety_envelope: 34// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 35// sil_target: SIL1 36// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 37// verdict: NOT_YET_EVALUATED 38 39import "nx_lemma_import.nx" 40 41// ===== Sealed opcode enum ========================================== 42const NX_OT_OP_NUM: nx_int = 1 43const NX_OT_OP_TERM: nx_int = 2 44const NX_OT_OP_AXIOM: nx_int = 3 45const NX_OT_OP_REFL: nx_int = 4 46const NX_OT_OP_MP: nx_int = 5 47const NX_OT_OP_ASSUME: nx_int = 6 48const NX_OT_OP_IMP_INTRO: nx_int = 7 49const NX_OT_OP_AND_INTRO: nx_int = 8 50const NX_OT_OP_THM: nx_int = 9 51const NX_OT_OP_NAME: nx_int = 10 52 53// ===== One instruction ============================================= 54// Caller-built array. arg_term and arg_str unused for opcodes that 55// only need the integer arg. 56struct OTInstr { 57 op: nx_int, 58 arg_int: nx_int, 59 arg_term: *Term, 60 arg_str: *u8, 61 arg_str_len: nx_int, 62} 63const NX_OT_INSTR_BYTES: nx_int = 40 64 65func nx_ot_instr_at(prog: *OTInstr, i: nx_int) -> *OTInstr { 66 return ((prog as nx_int) + (i * NX_OT_INSTR_BYTES)) as *OTInstr 67} 68 69// ===== Stack value ================================================= 70// kind = 1 (number), 2 (term), 3 (chain-index of a thm), 4 (name). 71struct OTValue { 72 kind: nx_int, 73 n: nx_int, 74 t: *Term, 75 name: *u8, 76 name_len: nx_int, 77} 78const NX_OT_VAL_BYTES: nx_int = 40 79 80const NX_OT_VAL_NUM: nx_int = 1 81const NX_OT_VAL_TERM: nx_int = 2 82const NX_OT_VAL_THM: nx_int = 3 83const NX_OT_VAL_NAME: nx_int = 4 84 85const NX_OT_STACK_CAP: nx_int = 256 86 87struct OTStack { 88 entries: *OTValue, 89 n: nx_int, 90 cap: nx_int, 91} 92const NX_OT_STACK_BYTES: nx_int = 24 93 94func nx_ot_stack_new() -> *OTStack { 95 let s: *OTStack = (sys_mmap(NX_OT_STACK_BYTES as i64)) as *OTStack 96 s.entries = (sys_mmap((NX_OT_STACK_CAP * NX_OT_VAL_BYTES) as i64)) as *OTValue 97 s.n = 0 98 s.cap = NX_OT_STACK_CAP 99 return s 100} 101 102func nx_ot_stack_at(s: *OTStack, i: nx_int) -> *OTValue { 103 return ((s.entries as nx_int) + (i * NX_OT_VAL_BYTES)) as *OTValue 104} 105 106func nx_ot_stack_push_num(s: *OTStack, n: nx_int) -> nx_int { 107 if s.n >= s.cap { return 0 - 1 } 108 let v: *OTValue = nx_ot_stack_at(s, s.n) 109 v.kind = NX_OT_VAL_NUM 110 v.n = n 111 s.n = s.n + 1 112 return s.n 113} 114 115func nx_ot_stack_push_term(s: *OTStack, t: *Term) -> nx_int { 116 if s.n >= s.cap { return 0 - 1 } 117 let v: *OTValue = nx_ot_stack_at(s, s.n) 118 v.kind = NX_OT_VAL_TERM 119 v.t = t 120 s.n = s.n + 1 121 return s.n 122} 123 124func nx_ot_stack_push_thm(s: *OTStack, chain_idx: nx_int) -> nx_int { 125 if s.n >= s.cap { return 0 - 1 } 126 let v: *OTValue = nx_ot_stack_at(s, s.n) 127 v.kind = NX_OT_VAL_THM 128 v.n = chain_idx 129 s.n = s.n + 1 130 return s.n 131} 132 133func nx_ot_stack_push_name(s: *OTStack, name: *u8, name_len: nx_int) -> nx_int { 134 if s.n >= s.cap { return 0 - 1 } 135 let v: *OTValue = nx_ot_stack_at(s, s.n) 136 v.kind = NX_OT_VAL_NAME 137 v.name = name 138 v.name_len = name_len 139 s.n = s.n + 1 140 return s.n 141} 142 143func nx_ot_stack_pop(s: *OTStack) -> *OTValue { 144 if s.n <= 0 { return 0 as *OTValue } 145 s.n = s.n - 1 146 return nx_ot_stack_at(s, s.n) 147} 148 149// ===== Engine: replay one instruction ============================== 150// Returns 0 on success, negative error code on failure. 151const NX_OT_OK: nx_int = 0 152const NX_OT_ERR_STACK: nx_int = -1 153const NX_OT_ERR_BAD_OP: nx_int = -2 154const NX_OT_ERR_KIND: nx_int = -3 155const NX_OT_ERR_KERNEL: nx_int = -4 156 157func nx_ot_step( 158 instr: *OTInstr, 159 s: *OTStack, 160 ch: *K2Chain, 161 lib: *LemmaLib 162) -> nx_int { 163 if instr.op == NX_OT_OP_NUM { 164 let r: nx_int = nx_ot_stack_push_num(s, instr.arg_int) 165 if r < 0 { return NX_OT_ERR_STACK } 166 return NX_OT_OK 167 } 168 if instr.op == NX_OT_OP_TERM { 169 let r: nx_int = nx_ot_stack_push_term(s, instr.arg_term) 170 if r < 0 { return NX_OT_ERR_STACK } 171 return NX_OT_OK 172 } 173 if instr.op == NX_OT_OP_NAME { 174 let r: nx_int = nx_ot_stack_push_name(s, instr.arg_str, instr.arg_str_len) 175 if r < 0 { return NX_OT_ERR_STACK } 176 return NX_OT_OK 177 } 178 if instr.op == NX_OT_OP_AXIOM { 179 // Pop top term -> emit axiom -> push thm. 180 let v: *OTValue = nx_ot_stack_pop(s) 181 if (v as nx_int) == 0 { return NX_OT_ERR_STACK } 182 if v.kind != NX_OT_VAL_TERM { return NX_OT_ERR_KIND } 183 let idx: nx_int = nx_k2_axiom(ch, v.t) 184 if idx < 0 { return NX_OT_ERR_KERNEL } 185 let _r: nx_int = nx_ot_stack_push_thm(s, idx) 186 return NX_OT_OK 187 } 188 if instr.op == NX_OT_OP_REFL { 189 let v: *OTValue = nx_ot_stack_pop(s) 190 if (v as nx_int) == 0 { return NX_OT_ERR_STACK } 191 if v.kind != NX_OT_VAL_TERM { return NX_OT_ERR_KIND } 192 let idx: nx_int = nx_k2_refl(ch, v.t) 193 if idx < 0 { return NX_OT_ERR_KERNEL } 194 let _r: nx_int = nx_ot_stack_push_thm(s, idx) 195 return NX_OT_OK 196 } 197 if instr.op == NX_OT_OP_ASSUME { 198 let v: *OTValue = nx_ot_stack_pop(s) 199 if (v as nx_int) == 0 { return NX_OT_ERR_STACK } 200 if v.kind != NX_OT_VAL_TERM { return NX_OT_ERR_KIND } 201 let idx: nx_int = nx_k2_assume(ch, v.t) 202 if idx < 0 { return NX_OT_ERR_KERNEL } 203 let _r: nx_int = nx_ot_stack_push_thm(s, idx) 204 return NX_OT_OK 205 } 206 if instr.op == NX_OT_OP_MP { 207 // Stack: ..., (P=>Q)_thm, P_thm -- pop P_thm then imp_thm 208 let v_a: *OTValue = nx_ot_stack_pop(s) 209 if (v_a as nx_int) == 0 { return NX_OT_ERR_STACK } 210 let v_imp: *OTValue = nx_ot_stack_pop(s) 211 if (v_imp as nx_int) == 0 { return NX_OT_ERR_STACK } 212 if v_a.kind != NX_OT_VAL_THM { return NX_OT_ERR_KIND } 213 if v_imp.kind != NX_OT_VAL_THM { return NX_OT_ERR_KIND } 214 let idx: nx_int = nx_k2_modus_ponens(ch, v_imp.n, v_a.n) 215 if idx < 0 { return NX_OT_ERR_KERNEL } 216 let _r: nx_int = nx_ot_stack_push_thm(s, idx) 217 return NX_OT_OK 218 } 219 if instr.op == NX_OT_OP_IMP_INTRO { 220 // Stack: ..., assumption_thm, body_thm -- pop body then assume 221 let v_b: *OTValue = nx_ot_stack_pop(s) 222 if (v_b as nx_int) == 0 { return NX_OT_ERR_STACK } 223 let v_a: *OTValue = nx_ot_stack_pop(s) 224 if (v_a as nx_int) == 0 { return NX_OT_ERR_STACK } 225 if v_b.kind != NX_OT_VAL_THM { return NX_OT_ERR_KIND } 226 if v_a.kind != NX_OT_VAL_THM { return NX_OT_ERR_KIND } 227 let idx: nx_int = nx_k2_imp_intro(ch, v_a.n, v_b.n) 228 if idx < 0 { return NX_OT_ERR_KERNEL } 229 let _r: nx_int = nx_ot_stack_push_thm(s, idx) 230 return NX_OT_OK 231 } 232 if instr.op == NX_OT_OP_AND_INTRO { 233 let v_b: *OTValue = nx_ot_stack_pop(s) 234 if (v_b as nx_int) == 0 { return NX_OT_ERR_STACK } 235 let v_a: *OTValue = nx_ot_stack_pop(s) 236 if (v_a as nx_int) == 0 { return NX_OT_ERR_STACK } 237 if v_b.kind != NX_OT_VAL_THM { return NX_OT_ERR_KIND } 238 if v_a.kind != NX_OT_VAL_THM { return NX_OT_ERR_KIND } 239 let idx: nx_int = nx_k2_and_intro(ch, v_a.n, v_b.n) 240 if idx < 0 { return NX_OT_ERR_KERNEL } 241 let _r: nx_int = nx_ot_stack_push_thm(s, idx) 242 return NX_OT_OK 243 } 244 if instr.op == NX_OT_OP_THM { 245 // Stack: ..., name, thm. Pop both; register in lib with 246 // PROVED_NATIVE_REPLAYED status + provenance = HOL_LIGHT (the 247 // canonical OpenTheory source). 248 let v_thm: *OTValue = nx_ot_stack_pop(s) 249 if (v_thm as nx_int) == 0 { return NX_OT_ERR_STACK } 250 if v_thm.kind != NX_OT_VAL_THM { return NX_OT_ERR_KIND } 251 let v_name: *OTValue = nx_ot_stack_pop(s) 252 if (v_name as nx_int) == 0 { return NX_OT_ERR_STACK } 253 if v_name.kind != NX_OT_VAL_NAME { return NX_OT_ERR_KIND } 254 let thm: *K2Thm = nx_k2_at(ch, v_thm.n) 255 let _i: nx_int = nx_lemma_import( 256 lib, ch, NX_LEMMA_SRC_HOL_LIGHT, 257 v_name.name, v_name.name_len, 258 thm.stmt, NX_LEMMA_PROVED_NATIVE_REPLAYED) 259 return NX_OT_OK 260 } 261 return NX_OT_ERR_BAD_OP 262} 263 264// Replay an entire program. Returns # of `thm` opcodes successfully 265// committed (= number of new lemmas added to lib), or negative on 266// any kernel-rejection (which means the source proof was malformed -- 267// fail loud per the no-third-party-trust cardinal). 268func nx_ot_replay( 269 prog: *OTInstr, n_instr: nx_int, 270 ch: *K2Chain, lib: *LemmaLib 271) -> nx_int { 272 let s: *OTStack = nx_ot_stack_new() 273 let lib_n_before: nx_int = lib.n 274 var i: nx_int = 0 275 while i < n_instr { 276 let r: nx_int = nx_ot_step(nx_ot_instr_at(prog, i), s, ch, lib) 277 if r != NX_OT_OK { return r } 278 i = i + 1 279 } 280 return lib.n - lib_n_before 281}