nx_hol_stream_ingest_test.nx source
↩ module page · 46 lines · 1615 B
1// nx_hol_stream_ingest_test.nx -- HOL Light parser -> defense stack.
2
3import "nx_syscalls.nx"
4import "nx_tier.nx"
5import "nx_hol_ingest.nx"
6import "nx_ingest_runner.nx"
7import "nx_hol_stream_ingest.nx"
8import "nx_bloom_capacity.nx"
9
10func main() -> nx_exit {
11 let prefix: *u8 = "/tmp/nx_hol_si_t1" as *u8
12 let ckpt: *u8 = "/tmp/nx_hol_si_t1.checkpoint" as *u8
13
14 let corpus: *u8 = sys_mmap(512)
15 var i: nx_int = 0
16 while i < 512 { corpus[i] = 0; i = i + 1 }
17 let src: *u8 = "let REAL_ADD_ASSOC = prove (`x + (y + z) = (x + y) + z`, ARITH_TAC);; let new_axiom INFINITY = new_axiom `~FINITE UNIV`;;" as *u8
18 var k: nx_int = 0
19 while src[k] != 0 { corpus[k] = src[k]; k = k + 1 }
20 let corpus_len: nx_int = k
21
22 let db: *HolDb = nx_hol_ingest_corpus(corpus, corpus_len)
23 if db.n_decls < 1 { return 11 }
24
25 let run: *NxIngestRun = nx_ingest_run_new(
26 prefix,
27 100000 as nx_size, 4096 as nx_size,
28 100, NX_BLOOM_PROFILE_1PCT,
29 ckpt, 60000)
30 if run == (0 as *NxIngestRun) { return 21 }
31
32 let row_buf: *u8 = sys_mmap(512)
33 let n1: nx_int = nx_hol_stream_offer_all(db, run, row_buf)
34 if n1 != db.n_decls { return 22 }
35 if nx_ingest_run_n_emitted(run) != db.n_decls { return 23 }
36
37 let n2: nx_int = nx_hol_stream_offer_all(db, run, row_buf)
38 if n2 != 0 { return 31 }
39 if nx_ingest_run_n_duplicate(run) != db.n_decls { return 32 }
40
41 if nx_ingest_run_n_shards(run) < 1 { return 41 }
42 nx_ingest_run_close(run)
43 let cp: *NxCheckpoint = nx_checkpoint_open(ckpt)
44 if nx_checkpoint_get(cp) != db.n_decls { return 51 }
45 return 0
46}