nx_theorem_card_test.nx source
↩ module page · 47 lines · 1987 B
1// nx_theorem_card_test.nx -- smoke for TheoremCard primitive.
2
3import "syscalls.nx"
4import "nx_theorem_card.nx"
5
6func main() -> i64 {
7 // Default card -> wobbly.
8 let blank: *TheoremCard = nx_card_alloc()
9 if blank.wobbly_flag != 1 { return 10 }
10 if blank.completeness_score_ppb != 0 { return 11 }
11 if nx_card_check_or_refuse(blank) != 0 { return 12 } // refuses dispatch
12
13 // Pythagorean card -> all 8 axes populated, score = 1e9, wobbly=0.
14 let py: *TheoremCard = nx_card_build_pythagorean()
15 if py.wobbly_flag != 0 { return 20 }
16 if py.completeness_score_ppb != 1000000000 { return 21 }
17 if nx_card_check_or_refuse(py) != 1 { return 22 } // allows dispatch
18 if py.n_genealogy < 2 { return 23 }
19 if py.n_lineage < 3 { return 24 }
20 if py.smoke_pass != 1 { return 25 }
21 if py.cross_check_status != NX_XCHECK_MATCHES_INDEPENDENT { return 26 }
22 if py.determinism_status != NX_DETERMINISM_BIT_IDENTICAL { return 27 }
23 if py.foundation_reach != NX_FOUNDATION_SUFFICIENT { return 28 }
24
25 // Partially-populated card -> wobbly (missing some axes).
26 let p: *TheoremCard = nx_card_alloc()
27 p.theorem_id = 99
28 p.name = "partial"
29 p.n_genealogy = 1
30 let lin: *i64 = (sys_mmap(8)) as *i64
31 lin[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
32 p.lineage_axiom_codes = lin
33 p.n_lineage = 1
34 p.smoke_pass = 1
35 // Missing: perf, xcheck, det, foundation
36 nx_card_compute_completeness(p)
37 if p.wobbly_flag != 1 { return 30 } // still wobbly
38 // Should have 4 axes filled: genealogy + lineage + smoke + (axis 7 fails
39 // because foundation_reach is TBD). So score should be < 1e9.
40 if p.completeness_score_ppb >= 1000000000 { return 31 }
41 if nx_card_check_or_refuse(p) != 0 { return 32 } // refused
42
43 // Emit cards to stderr to verify JSON serialization runs.
44 nx_card_emit(2, py)
45 nx_card_emit(2, blank)
46 return 0
47}