code wiki / (root) / nx_auto_verify_test.nx

nx_auto_verify_test.nx

buildroot/runtime/nx_auto_verify_test.nx

3095 B80 linesdepth 6pulls 8 transitivereach 0 importersview sourcekind gate/prooftopic auto
docsdependenciesstructsconstsfunctions

about

nx_auto_verify_test.nx -- smoke for autonomous bulk verification.

dependencies 5 imports · 0 importers

syscalls.nx nx_axioms.nx nx_qed_db.nx nx_prover.nx nx_auto_verify.nx nx_auto_verify_test.nx

imports: syscalls.nxnx_axioms.nxnx_qed_db.nxnx_prover.nxnx_auto_verify.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main nx_qed_db_alloc nx_qed_insert nx_qed_entry_at nx_verify_stats_alloc nx_auto_verify_bulk nx_qed_entry_at ↻ nx_auto_verify_entry nx_auto_try_prove nx_prover_state_alloc nx_prover_add_axiom nx_axiom_is_valid nx_prover_fact_at nx_prover_search nx_prover_has_target nx_prover_fact_at ↻ nx_prover_step_mp nx_prover_has_stmt nx_prover_fact_at ↻ nx_prover_add_inferred nx_qed_entry_at ↻ nx_verify_emit_stats av_str av_i64 av_putc av_i64 ↻

structs

none

consts

none

functions

9func main() -> i64 {
calls 6: nx_qed_db_allocnx_qed_insertnx_verify_stats_allocnx_auto_verify_bulknx_qed_entry_atnx_verify_emit_stats