nx_ot_replay_test.nx
buildroot/runtime/nx_ot_replay_test.nx
about
nx_ot_replay_test.nx -- exercise the OpenTheory replay engine.
Each scenario assembles a small program of OT-style instructions
and asserts the engine produces the expected number of corpus
entries with kernel-checked semantics.
dependencies 1 imports · 0 importers
imports: nx_ot_replay.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| 8 | const SYM_P: nx_int = 1001 |
| 9 | const SYM_Q: nx_int = 1002 |
| 10 | const SYM_R: nx_int = 1003 |
functions
| 13 | func set_instr(prog: *OTInstr, i: nx_int, op: nx_int, arg_int: nx_int, called by 5: t1_axiom_onlyt2_mpt3_kernel_rejects_bad_replayt4_hyp_syllogismt5_refl calls 1: nx_ot_instr_at |
| 25 | func t1_axiom_only() -> nx_int called by 1: main calls 6: nx_k2_chain_newnx_lemma_lib_newnx_term_constset_instrnx_ot_replaynx_lemma_lib_at |
| 45 | func t2_mp() -> nx_int called by 1: main calls 8: nx_k2_chain_newnx_lemma_lib_newnx_term_constnx_k2_impset_instrnx_ot_replay+2 |
| 90 | func t3_kernel_rejects_bad_replay() -> nx_int called by 1: main calls 6: nx_k2_chain_newnx_lemma_lib_newnx_term_constnx_k2_impset_instrnx_ot_replay |
| 114 | func t4_hyp_syllogism() -> nx_int called by 1: main calls 8: nx_k2_chain_newnx_lemma_lib_newnx_term_constnx_k2_impset_instrnx_ot_replay+2 |
| 156 | func t5_refl() -> nx_int called by 1: main calls 6: nx_k2_chain_newnx_lemma_lib_newnx_term_constset_instrnx_ot_replaynx_lemma_lib_at |
| 173 | func main() -> nx_exit |