nx_ot_replay.nx
buildroot/runtime/nx_ot_replay.nx
about
nx_ot_replay.nx -- OpenTheory replay engine.
Per user 2026-05-15: "world class". Per the comparison-engine
commit's named improvement for library_size LOSE_BIG vs HOL Light.
OpenTheory is the kernel-independent proof-exchange format from
gilith.com/opentheory/article.html. HOL kernels (HOL Light, HOL4,
ProofPower, Isabelle/HOL) export their proofs as a list of stack
machine instructions; any HOL-compatible kernel can replay them
and re-derive each theorem natively.
THIS ENGINE: a stack-based interpreter that executes OpenTheory-
style instructions. Each opcode that produces a Theorem dispatches
to a v2 kernel emitter, so every replayed theorem becomes a real
kernel-checked chain in our K2Chain. No third-party trust: the
source is the input, OUR kernel is the verifier.
Every successful `thm` opcode registers an entry in the supplied
LemmaLib with NX_LEMMA_PROVED_NATIVE_REPLAYED status. This is the
honest framing per [[feedback-no-third-party-trust-native-or-nothing]]:
the proof BODY was replayed natively; the SOURCE is preserved as
provenance metadata.
What this commit ships:
- Stack machine + 8 opcodes (num, term, axiom, refl, mp, assume,
imp_intro, thm)
- Programmatic replay (caller assembles an instruction array)
Named follow-up:
- .ot file parser (read ASCII OpenTheory format from file)
- Full opcode coverage (absTerm, appTerm, defineConst, subst,
deductAntisym, eqMp, etc. -- ~30 total)
dependencies 1 imports · 1 importers
imports: nx_lemma_import.nx
imported by: nx_ot_replay_test.nx
structs
| 56 | struct OTInstr |
| 71 | struct OTValue |
| 87 | struct OTStack |
consts
| 42 | const NX_OT_OP_NUM: nx_int = 1 |
| 43 | const NX_OT_OP_TERM: nx_int = 2 |
| 44 | const NX_OT_OP_AXIOM: nx_int = 3 |
| 45 | const NX_OT_OP_REFL: nx_int = 4 |
| 46 | const NX_OT_OP_MP: nx_int = 5 |
| 47 | const NX_OT_OP_ASSUME: nx_int = 6 |
| 48 | const NX_OT_OP_IMP_INTRO: nx_int = 7 |
| 49 | const NX_OT_OP_AND_INTRO: nx_int = 8 |
| 50 | const NX_OT_OP_THM: nx_int = 9 |
| 51 | const NX_OT_OP_NAME: nx_int = 10 |
| 63 | const NX_OT_INSTR_BYTES: nx_int = 40 |
| 78 | const NX_OT_VAL_BYTES: nx_int = 40 |
| 80 | const NX_OT_VAL_NUM: nx_int = 1 |
| 81 | const NX_OT_VAL_TERM: nx_int = 2 |
| 82 | const NX_OT_VAL_THM: nx_int = 3 |
| 83 | const NX_OT_VAL_NAME: nx_int = 4 |
| 85 | const NX_OT_STACK_CAP: nx_int = 256 |
| 92 | const NX_OT_STACK_BYTES: nx_int = 24 |
| 151 | const NX_OT_OK: nx_int = 0 |
| 152 | const NX_OT_ERR_STACK: nx_int = -1 |
| 153 | const NX_OT_ERR_BAD_OP: nx_int = -2 |
| 154 | const NX_OT_ERR_KIND: nx_int = -3 |
| 155 | const NX_OT_ERR_KERNEL: nx_int = -4 |
functions
| 65 | func nx_ot_instr_at(prog: *OTInstr, i: nx_int) -> *OTInstr |
| 94 | func nx_ot_stack_new() -> *OTStack called by 1: nx_ot_replay |
| 102 | func nx_ot_stack_at(s: *OTStack, i: nx_int) -> *OTValue |
| 106 | func nx_ot_stack_push_num(s: *OTStack, n: nx_int) -> nx_int |
| 115 | func nx_ot_stack_push_term(s: *OTStack, t: *Term) -> nx_int |
| 124 | func nx_ot_stack_push_thm(s: *OTStack, chain_idx: nx_int) -> nx_int |
| 133 | func nx_ot_stack_push_name(s: *OTStack, name: *u8, name_len: nx_int) -> nx_int |
| 143 | func nx_ot_stack_pop(s: *OTStack) -> *OTValue |
| 157 | func nx_ot_step( |
| 268 | func nx_ot_replay( |