nx_proof_log_test.nx source
↩ module page · 91 lines · 4298 B
1// nx_proof_log_test.nx -- proof history tracking smoke.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_result.nx"
7import "nx_proof_log.nx"
8
9func main() -> nx_exit {
10 println("=== Proof history log smoke ===" as *u8)
11 var fails: nx_int = 0
12
13 // Build a minimal proof log:
14 // 0: input {p}
15 // 1: input {~p, q}
16 // 2: input {~q}
17 // 3: RES(0, 1) -> {q}
18 // 4: RES(2, 3) -> empty
19 let log: *ProofLog = nx_proof_log_new(16)
20
21 let i0: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
22 let i1: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
23 let i2: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
24 let i3: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_RES, i0, i1)
25 let i4: nx_int = nx_proof_log_add(log, NX_PROOF_RULE_RES, i2, i3)
26
27 // ---------- Test 1: indices ascend -------------------------
28 if i0 == 0 {
29 if i4 == 4 { println(" 1. 5 entries 0..4 PASS" as *u8) }
30 else { println(" 1. wrong tail idx FAIL" as *u8); fails = fails + 1 }
31 } else { println(" 1. wrong head idx FAIL" as *u8); fails = fails + 1 }
32
33 // ---------- Test 2: rule lookup ----------------------------
34 let e3: *ProofEntry = nx_proof_log_get(log, i3)
35 if e3.rule == NX_PROOF_RULE_RES {
36 if e3.parent_a == i0 {
37 if e3.parent_b == i1 {
38 println(" 2. RES entry (rule + 2 parents) PASS" as *u8)
39 } else { println(" 2. parent_b wrong FAIL" as *u8); fails = fails + 1 }
40 } else { println(" 2. parent_a wrong FAIL" as *u8); fails = fails + 1 }
41 } else { println(" 2. rule wrong FAIL" as *u8); fails = fails + 1 }
42
43 // ---------- Test 3: ancestor walk from empty ---------------
44 // Walk from i4 (empty); should visit all 5 entries: i4, i2, i3, i0, i1.
45 let visited: *nx_int = (sys_mmap((16 * 8) as i64)) as *nx_int
46 let count: nx_int = nx_proof_walk_ancestors(log, i4, visited)
47 print(" 3. ancestor walk from empty -> " as *u8); print_i64(count); print(" entries; visited[0..4] = " as *u8)
48 print_i64(visited[0]); print(" " as *u8)
49 print_i64(visited[1]); print(" " as *u8)
50 print_i64(visited[2]); print(" " as *u8)
51 print_i64(visited[3]); print(" " as *u8)
52 print_i64(visited[4]); println("" as *u8)
53 if count == 5 {
54 if visited[0] == 1 {
55 if visited[1] == 1 {
56 if visited[2] == 1 {
57 if visited[3] == 1 {
58 if visited[4] == 1 {
59 println(" all 5 ancestors visited PASS" as *u8)
60 } else { println(" i4 missed FAIL" as *u8); fails = fails + 1 }
61 } else { println(" i3 missed FAIL" as *u8); fails = fails + 1 }
62 } else { println(" i2 missed FAIL" as *u8); fails = fails + 1 }
63 } else { println(" i1 missed FAIL" as *u8); fails = fails + 1 }
64 } else { println(" i0 missed FAIL" as *u8); fails = fails + 1 }
65 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
66
67 // ---------- Test 4: rule name lookup -----------------------
68 let r_name: *u8 = nx_proof_rule_name(NX_PROOF_RULE_PARAMOD)
69 print(" 4. rule_name(PARAMOD) -> '" as *u8); print(r_name); println("'" as *u8)
70 if r_name[0] == 112 {
71 if r_name[1] == 97 { println(" PASS" as *u8) }
72 else { println(" FAIL" as *u8); fails = fails + 1 }
73 } else { println(" FAIL" as *u8); fails = fails + 1 }
74
75 // ---------- Test 5: capacity overflow returns -1 -----------
76 let small: *ProofLog = nx_proof_log_new(2)
77 let _o0: nx_int = nx_proof_log_add(small, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
78 let _o1: nx_int = nx_proof_log_add(small, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
79 let o2: nx_int = nx_proof_log_add(small, NX_PROOF_RULE_INPUT, 0 - 1, 0 - 1)
80 if o2 == 0 - 1 {
81 println(" 5. capacity overflow -> -1 PASS" as *u8)
82 } else { println(" 5. cap not enforced FAIL" as *u8); fails = fails + 1 }
83
84 println("" as *u8)
85 if fails == 0 {
86 println("=== ALL 5 proof-log tests PASS ===" as *u8)
87 return 0
88 }
89 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
90 return 1
91}