nx_lean_stream_ingest_test.nx source
↩ module page · 58 lines · 1979 B
1// nx_lean_stream_ingest_test.nx -- Lean parser -> defense stack.
2
3import "nx_syscalls.nx"
4import "nx_tier.nx"
5import "nx_lean_ingest.nx"
6import "nx_ingest_runner.nx"
7import "nx_lean_stream_ingest.nx"
8import "nx_bloom_capacity.nx"
9
10func main() -> nx_exit {
11 let prefix: *u8 = "/tmp/nx_lean_si_t1" as *u8
12 let ckpt: *u8 = "/tmp/nx_lean_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 = "axiom A1 theorem T1 def helper theorem T2 lemma L1" 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: *LeanDb = nx_lean_ingest_corpus(corpus, corpus_len)
23 if db.n_decls < 4 { return 11 }
24 if nx_lean_count_kind(db, NX_LEAN_TOK_AXIOM) != 1 { return 12 }
25 if nx_lean_count_kind(db, NX_LEAN_TOK_THEOREM) != 2 { return 13 }
26 if nx_lean_count_kind(db, NX_LEAN_TOK_LEMMA) != 1 { return 14 }
27
28 let run: *NxIngestRun = nx_ingest_run_new(
29 prefix,
30 100000 as nx_size,
31 4096 as nx_size,
32 100,
33 NX_BLOOM_PROFILE_1PCT,
34 ckpt,
35 60000
36 )
37 if run == (0 as *NxIngestRun) { return 21 }
38
39 let row_buf: *u8 = sys_mmap(512)
40 let n1: nx_int = nx_lean_stream_offer_all(db, run, row_buf)
41 if (n1 as nx_int) != db.n_decls { return 22 }
42 if nx_ingest_run_n_emitted(run) != db.n_decls { return 23 }
43 if nx_ingest_run_n_duplicate(run) != 0 { return 24 }
44
45 let n2: nx_int = nx_lean_stream_offer_all(db, run, row_buf)
46 if n2 != 0 { return 31 }
47 if nx_ingest_run_n_duplicate(run) != db.n_decls { return 32 }
48 if nx_ingest_run_n_emitted(run) != db.n_decls { return 33 }
49
50 if nx_ingest_run_n_shards(run) < 1 { return 41 }
51 if nx_ingest_run_disk_used_bytes(run) < 50 { return 42 }
52
53 nx_ingest_run_close(run)
54 let cp: *NxCheckpoint = nx_checkpoint_open(ckpt)
55 if nx_checkpoint_get(cp) != db.n_decls { return 51 }
56
57 return 0
58}