nx_triangulation_graph.nx source
↩ module page · 139 lines · 5698 B
1// nx_triangulation_graph.nx -- battery 5: graph algorithms.
2//
3// Triangulates nx_graph_bfs_count, nx_graph_is_connected,
4// nx_graph_degree, nx_graph_edge_count on a few well-known small
5// graphs (path, cycle, star, complete). Cross-witnesses use
6// graph-theory identities:
7//
8// - For ANY connected graph with n vertices and starting vertex v:
9// bfs_count(v) == n
10// - For ANY graph: sum(degree(v)) == 2 * edge_count
11// - Cycle Cn: every vertex has degree 2 (a deterministic property)
12// - Path Pn: 2 endpoints have degree 1, internal vertices have degree 2
13
14// nx_safety_envelope:
15// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
16// sil_target: SIL1
17// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
18// verdict: NOT_YET_EVALUATED
19
20import "nx_syscalls.nx"
21import "nx_runtime.nx"
22import "nx_tier.nx"
23import "nx_graph.nx"
24
25func nx_tri_check(label: *u8, aut: nx_int, w1: nx_int, w2: nx_int,
26 agree: *nx_int, fail: *nx_int) {
27 print(label); print(": AUT=" as *u8); print_i64(aut)
28 print(" W1=" as *u8); print_i64(w1); print(" W2=" as *u8); print_i64(w2)
29 if aut == w1 {
30 if aut == w2 {
31 println(" -> TRIANGULATED" as *u8)
32 agree[0] = agree[0] + 1
33 return
34 }
35 }
36 println(" -> DISAGREE" as *u8)
37 fail[0] = fail[0] + 1
38}
39
40// Build a small adjacency matrix. Convention: adj is n*n nx_int array,
41// adj[i*n+j] = 1 if edge i--j (undirected), 0 otherwise.
42func nx_set_edge(adj: *nx_int, n: nx_int, u: nx_int, v: nx_int) {
43 adj[u * n + v] = 1
44 adj[v * n + u] = 1
45}
46
47func main() -> nx_exit {
48 let agree: *nx_int = (sys_mmap(8)) as *nx_int
49 let fail: *nx_int = (sys_mmap(8)) as *nx_int
50 agree[0] = 0
51 fail[0] = 0
52
53 println("=== TRIANGULATION: GRAPH ALGORITHMS BATTERY ===" as *u8)
54
55 // ===== Graph 1: cycle C5 (5 vertices, edges 0-1, 1-2, 2-3, 3-4, 4-0)
56 let n_c5: nx_int = 5
57 let adj_c5: *nx_int = (sys_mmap(200)) as *nx_int // 5*5*8 bytes
58 var i: nx_int = 0
59 while i < n_c5 * n_c5 { adj_c5[i] = 0; i = i + 1 }
60 nx_set_edge(adj_c5, n_c5, 0, 1)
61 nx_set_edge(adj_c5, n_c5, 1, 2)
62 nx_set_edge(adj_c5, n_c5, 2, 3)
63 nx_set_edge(adj_c5, n_c5, 3, 4)
64 nx_set_edge(adj_c5, n_c5, 4, 0)
65
66 // C5 is connected. bfs_count from any vertex == 5.
67 let bfs_c5_v0: nx_int = nx_graph_bfs_count(adj_c5, n_c5, 0) as nx_int
68 let bfs_c5_v2: nx_int = nx_graph_bfs_count(adj_c5, n_c5, 2) as nx_int
69 let connected_c5: nx_int = nx_graph_is_connected(adj_c5, n_c5) as nx_int
70 nx_tri_check("C5: bfs(v0) == n == bfs(v2) " as *u8,
71 bfs_c5_v0, n_c5 as nx_int, bfs_c5_v2, agree, fail)
72 nx_tri_check("C5: connected (bfs/is_conn) " as *u8,
73 connected_c5, 1, 1, agree, fail)
74
75 // C5: every vertex has degree 2 (cycle property)
76 let deg_c5_v0: nx_int = nx_graph_degree(adj_c5, n_c5, 0) as nx_int
77 let deg_c5_v3: nx_int = nx_graph_degree(adj_c5, n_c5, 3) as nx_int
78 nx_tri_check("C5: deg(v0)==deg(v3)==2 " as *u8,
79 deg_c5_v0, 2, deg_c5_v3, agree, fail)
80
81 // C5: edge_count == 5 (cycle has n edges)
82 let e_c5: nx_int = nx_graph_edge_count(adj_c5, n_c5) as nx_int
83 nx_tri_check("C5: edge_count == n " as *u8,
84 e_c5, 5, 5, agree, fail)
85
86 // ===== Graph 2: disconnected (two components, 4 vertices)
87 let n_d: nx_int = 4
88 let adj_d: *nx_int = (sys_mmap(128)) as *nx_int
89 i = 0
90 while i < n_d * n_d { adj_d[i] = 0; i = i + 1 }
91 // Component 1: 0-1
92 // Component 2: 2-3
93 nx_set_edge(adj_d, n_d, 0, 1)
94 nx_set_edge(adj_d, n_d, 2, 3)
95
96 let bfs_d_v0: nx_int = nx_graph_bfs_count(adj_d, n_d, 0) as nx_int
97 let connected_d: nx_int = nx_graph_is_connected(adj_d, n_d) as nx_int
98 // bfs_count from v0 reaches 2 (just 0 and 1). Not connected.
99 nx_tri_check("disconn: bfs(v0)<n " as *u8,
100 bfs_d_v0, 2, 2, agree, fail)
101 nx_tri_check("disconn: is_connected=0 " as *u8,
102 connected_d, 0, 0, agree, fail)
103
104 // ===== Graph 3: path P5 (0-1-2-3-4 linearly)
105 let n_p5: nx_int = 5
106 let adj_p5: *nx_int = (sys_mmap(200)) as *nx_int
107 i = 0
108 while i < n_p5 * n_p5 { adj_p5[i] = 0; i = i + 1 }
109 nx_set_edge(adj_p5, n_p5, 0, 1)
110 nx_set_edge(adj_p5, n_p5, 1, 2)
111 nx_set_edge(adj_p5, n_p5, 2, 3)
112 nx_set_edge(adj_p5, n_p5, 3, 4)
113
114 // P5: bfs_count from any vertex == 5; edge_count == 4 (path Pn has n-1 edges)
115 let bfs_p5_v0: nx_int = nx_graph_bfs_count(adj_p5, n_p5, 0) as nx_int
116 let bfs_p5_v4: nx_int = nx_graph_bfs_count(adj_p5, n_p5, 4) as nx_int
117 let e_p5: nx_int = nx_graph_edge_count(adj_p5, n_p5) as nx_int
118 nx_tri_check("P5: bfs(v0)==n==bfs(v4) " as *u8,
119 bfs_p5_v0, 5, bfs_p5_v4, agree, fail)
120 nx_tri_check("P5: edge_count == n-1 " as *u8,
121 e_p5, 4, 4, agree, fail)
122
123 // P5: endpoints have degree 1, internal vertices have degree 2
124 let deg_p5_v0: nx_int = nx_graph_degree(adj_p5, n_p5, 0) as nx_int
125 let deg_p5_v2: nx_int = nx_graph_degree(adj_p5, n_p5, 2) as nx_int
126 let deg_p5_v4: nx_int = nx_graph_degree(adj_p5, n_p5, 4) as nx_int
127 nx_tri_check("P5: deg(endpoints) == 1 " as *u8,
128 deg_p5_v0, 1, deg_p5_v4, agree, fail)
129 nx_tri_check("P5: deg(internal) == 2 " as *u8,
130 deg_p5_v2, 2, 2, agree, fail)
131
132 println("" as *u8)
133 println("============================================" as *u8)
134 print("TRIANGULATED: " as *u8); print_i64(agree[0]); println("" as *u8)
135 print("DISAGREE: " as *u8); print_i64(fail[0]); println("" as *u8)
136 println("============================================" as *u8)
137 if fail[0] > 0 { return 1 }
138 return 0
139}