nx_triangulation_classical.nx source
↩ module page · 121 lines · 5256 B
1// nx_triangulation_classical.nx -- triangulated correctness proofs
2// for classical algorithms beyond the original battery. Each AUT
3// is verified against 2 independent witnesses (known-vector + algebraic
4// identity) inside the NishiLang substrate.
5
6// nx_safety_envelope:
7// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
8// sil_target: SIL1
9// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
10// verdict: NOT_YET_EVALUATED
11
12import "nx_syscalls.nx"
13import "nx_runtime.nx"
14import "nx_tier.nx"
15import "nx_classical_unpatented.nx"
16import "nx_classical_unpatented_2.nx"
17import "nx_classical_unpatented_3.nx"
18const K_MAGIC_1024: i64 = 1024
19const K_MAGIC_2048: i64 = 2048
20
21func nx_tri_check(label: *u8, aut: nx_int, w1: nx_int, w2: nx_int,
22 agree: *nx_int, fail: *nx_int) {
23 print(label); print(": AUT=" as *u8); print_i64(aut)
24 print(" W1=" as *u8); print_i64(w1); print(" W2=" as *u8); print_i64(w2)
25 if aut == w1 {
26 if aut == w2 {
27 println(" -> TRIANGULATED" as *u8)
28 agree[0] = agree[0] + 1
29 return
30 }
31 }
32 println(" -> DISAGREE" as *u8)
33 fail[0] = fail[0] + 1
34}
35
36func main() -> nx_exit {
37 let agree: *nx_int = (sys_mmap(8)) as *nx_int
38 let fail: *nx_int = (sys_mmap(8)) as *nx_int
39 agree[0] = 0
40 fail[0] = 0
41
42 println("=== TRIANGULATION: CLASSICAL ALGORITHMS BATTERY 2 ===" as *u8)
43
44 // log2_floor: log2(8)=3. W2: log2(7)=2, so log2(8) == log2(7) + 1
45 nx_tri_check("log2_floor(8) " as *u8,
46 nx_log2_floor_int(8), 3, nx_log2_floor_int(7) + 1, agree, fail)
47 nx_tri_check("log2_floor(1024) " as *u8,
48 nx_log2_floor_int(K_MAGIC_1024), 10, nx_log2_floor_int(512) + 1, agree, fail)
49
50 // clz_64(1) = 63 (1 leading 0s before the only set bit).
51 // W2: clz_64(2) should be 62 (one less leading zero)
52 nx_tri_check("clz_64(1) " as *u8,
53 nx_clz_64(1), 63, nx_clz_64(2) + 1, agree, fail)
54 nx_tri_check("clz_64(256) " as *u8,
55 nx_clz_64(256), 55, nx_clz_64(128) - 1, agree, fail)
56
57 // ctz_64(8) = 3. W2: ctz_64(16) = 4, so ctz_64(8) == ctz_64(16) - 1
58 nx_tri_check("ctz_64(8) " as *u8,
59 nx_ctz_64(8), 3, nx_ctz_64(16) - 1, agree, fail)
60 nx_tri_check("ctz_64(1024) " as *u8,
61 nx_ctz_64(K_MAGIC_1024), 10, nx_ctz_64(K_MAGIC_2048) - 1, agree, fail)
62
63 // mod_pow(2, 10, 1000) = 1024 mod 1000 = 24.
64 // W2: 2^10 = 2^5 * 2^5 = 32 * 32 = 1024 -> mod 1000 = 24
65 nx_tri_check("mod_pow(2, 10, 1000) " as *u8,
66 nx_mod_pow(2, 10, 1000), 24,
67 (nx_mod_pow(2, 5, 1000) * nx_mod_pow(2, 5, 1000)) % 1000, agree, fail)
68
69 // mod_pow(3, 7, 100) = 3^7 = 2187 mod 100 = 87
70 nx_tri_check("mod_pow(3, 7, 100) " as *u8,
71 nx_mod_pow(3, 7, 100), 87,
72 (nx_mod_pow(3, 3, 100) * nx_mod_pow(3, 4, 100)) % 100, agree, fail)
73
74 // is_prime_trial: 7 is prime (1), 9 is not (0)
75 nx_tri_check("is_prime_trial(7) " as *u8,
76 nx_is_prime_trial(7), 1, 1, agree, fail)
77 nx_tri_check("is_prime_trial(9) " as *u8,
78 nx_is_prime_trial(9), 0, 0, agree, fail)
79 nx_tri_check("is_prime_trial(97) " as *u8,
80 nx_is_prime_trial(97), 1, 1, agree, fail)
81
82 // linear_search vs binary_search on sorted array
83 let arr: *nx_int = (sys_mmap(80)) as *nx_int
84 arr[0] = 5; arr[1] = 15; arr[2] = 25; arr[3] = 42
85 arr[4] = 55; arr[5] = 71; arr[6] = 89; arr[7] = 99
86 nx_tri_check("linear_search(42) " as *u8,
87 nx_linear_search_idx(arr, 8, 42) as nx_int, 3,
88 nx_binary_search(arr, 8, 42) as nx_int, agree, fail)
89 nx_tri_check("linear_search(99) " as *u8,
90 nx_linear_search_idx(arr, 8, 99) as nx_int, 7,
91 nx_binary_search(arr, 8, 99) as nx_int, agree, fail)
92
93 // count_occurrences: array with repeats
94 arr[0] = 7; arr[1] = 3; arr[2] = 7; arr[3] = 7
95 arr[4] = 1; arr[5] = 7; arr[6] = 2; arr[7] = 5
96 nx_tri_check("count_occurrences(7) " as *u8,
97 nx_count_occurrences(arr, 8, 7), 4,
98 4, agree, fail)
99 nx_tri_check("count_occurrences(3) " as *u8,
100 nx_count_occurrences(arr, 8, 3), 1, 1, agree, fail)
101
102 // bubble_sort then array reads -- AUT is the post-sort array values,
103 // W2 is verified by re-sorting with insertion_sort
104 let buf1: *nx_int = (sys_mmap(40)) as *nx_int
105 let buf2: *nx_int = (sys_mmap(40)) as *nx_int
106 buf1[0] = 4; buf1[1] = 2; buf1[2] = 5; buf1[3] = 1; buf1[4] = 3
107 buf2[0] = 4; buf2[1] = 2; buf2[2] = 5; buf2[3] = 1; buf2[4] = 3
108 let _u1: nx_int = nx_bubble_sort(buf1, 5)
109 let _u2: nx_int = nx_insertion_sort(buf2, 5)
110 nx_tri_check("sort_consistency[0] " as *u8, buf1[0], 1, buf2[0], agree, fail)
111 nx_tri_check("sort_consistency[2] " as *u8, buf1[2], 3, buf2[2], agree, fail)
112 nx_tri_check("sort_consistency[4] " as *u8, buf1[4], 5, buf2[4], agree, fail)
113
114 println("" as *u8)
115 println("============================================" as *u8)
116 print("TRIANGULATED: " as *u8); print_i64(agree[0]); println("" as *u8)
117 print("DISAGREE: " as *u8); print_i64(fail[0]); println("" as *u8)
118 println("============================================" as *u8)
119 if fail[0] > 0 { return 1 }
120 return 0
121}