Skip to content

Commit 11bc8a6

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(fault-tolerance): health monitoring, NeSy validation, fallback SLA
Integrates the in-flight/fault-tolerance-2026-04-25 branch (8 commits): - dispatch.rs: circuit-breaker health recording at prove exits; record_prover_result flows into HealthStatus for per-prover degradation tracking - server.rs: ProverDispatcher wired into AppState alongside MetaController/stats; prove_handler now records health on success and failure paths - diagnostics: add nesy_validation (GNN–symbolic agreement rate, can_claim_gnn_verified), fallback_monitor (FallbackSLAConfig, FallbackInvocation, cosine fallback SLA), CircuitBreakerStateSnapshot; gnn_training + proof_failure from main retained - repl: diagnostics module enabled (DiagnosticsREPL) - tests: full_health_system_test, prove_handler_health_integration_test Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 0830053 commit 11bc8a6

17 files changed

Lines changed: 3362 additions & 10 deletions

‎examples/.simple_proof.aux‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
COQAUX1 b6e86f4cbeae9f778c619e89f35ea3c2 /var/mnt/eclipse/repos/echidna/examples/simple_proof.v
2+
0 0 VernacProof "tac:no using:no"
3+
671 675 proof_build_time "0.005"
4+
0 0 add_comm "0.005"
5+
658 670 context_used ""
6+
671 675 proof_check_time "0.001"
7+
0 0 VernacProof "tac:no using:no"
8+
940 944 proof_build_time "0.003"
9+
0 0 add_assoc "0.003"
10+
927 939 context_used ""
11+
940 944 proof_check_time "0.001"
12+
0 0 VernacProof "tac:no using:no"
13+
1120 1124 proof_build_time "0.003"
14+
0 0 add_0_r "0.003"
15+
1107 1119 context_used ""
16+
1120 1124 proof_check_time "0.001"
17+
0 0 VernacProof "tac:no using:no"

‎examples/simple_proof.glob‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
DIGEST b6e86f4cbeae9f778c619e89f35ea3c2
2+
Fsimple_proof
3+
R275:279 Stdlib.Arith.Arith <> <> lib
4+
prf 324:331 <> add_comm
5+
R348:350 Corelib.Init.Datatypes <> nat ind
6+
binder 342:342 <> n:1
7+
binder 344:344 <> m:2
8+
R360:362 Corelib.Init.Logic <> ::type_scope:x_'='_x not
9+
R356:358 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
10+
R355:355 simple_proof <> n:1 var
11+
R359:359 simple_proof <> m:2 var
12+
R364:366 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
13+
R363:363 simple_proof <> m:2 var
14+
R367:367 simple_proof <> n:1 var
15+
R529:536 Corelib.Init.Peano <> plus_n_O thm
16+
R529:536 Corelib.Init.Peano <> plus_n_O thm
17+
R529:536 Corelib.Init.Peano <> plus_n_O thm
18+
R643:651 Corelib.Init.Peano <> plus_n_Sm thm
19+
R643:651 Corelib.Init.Peano <> plus_n_Sm thm
20+
R643:651 Corelib.Init.Peano <> plus_n_Sm thm
21+
prf 718:726 <> add_assoc
22+
R745:747 Corelib.Init.Datatypes <> nat ind
23+
binder 737:737 <> n:3
24+
binder 739:739 <> m:4
25+
binder 741:741 <> p:5
26+
R763:765 Corelib.Init.Logic <> ::type_scope:x_'='_x not
27+
R752:752 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
28+
R758:761 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
29+
R754:756 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
30+
R753:753 simple_proof <> n:3 var
31+
R757:757 simple_proof <> m:4 var
32+
R762:762 simple_proof <> p:5 var
33+
R767:770 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
34+
R776:776 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
35+
R766:766 simple_proof <> n:3 var
36+
R772:774 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
37+
R771:771 simple_proof <> m:4 var
38+
R775:775 simple_proof <> p:5 var
39+
prf 978:984 <> add_0_r
40+
R999:1001 Corelib.Init.Datatypes <> nat ind
41+
binder 995:995 <> n:6
42+
R1011:1013 Corelib.Init.Logic <> ::type_scope:x_'='_x not
43+
R1007:1009 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
44+
R1006:1006 simple_proof <> n:6 var
45+
R1014:1014 simple_proof <> n:6 var
46+
prf 1156:1164 <> mult_dist
47+
R1183:1185 Corelib.Init.Datatypes <> nat ind
48+
binder 1175:1175 <> n:7
49+
binder 1177:1177 <> m:8
50+
binder 1179:1179 <> p:9
51+
R1201:1203 Corelib.Init.Logic <> ::type_scope:x_'='_x not
52+
R1191:1194 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not
53+
R1200:1200 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not
54+
R1190:1190 simple_proof <> n:7 var
55+
R1196:1198 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
56+
R1195:1195 simple_proof <> m:8 var
57+
R1199:1199 simple_proof <> p:9 var
58+
R1209:1211 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not
59+
R1205:1207 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not
60+
R1204:1204 simple_proof <> n:7 var
61+
R1208:1208 simple_proof <> m:8 var
62+
R1213:1215 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not
63+
R1212:1212 simple_proof <> n:7 var
64+
R1216:1216 simple_proof <> p:9 var

‎reports/blitz-2026-04-25-late/crates.json‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
{
2+
"program_path": "crates",
3+
"language": "rust",
4+
"frameworks": [],
5+
"weak_points": [],
6+
"statistics": {
7+
"total_lines": 2272,
8+
"unsafe_blocks": 0,
9+
"panic_sites": 0,
10+
"unwrap_calls": 3,
11+
"allocation_sites": 26,
12+
"io_operations": 1,
13+
"threading_constructs": 0
14+
},
15+
"file_statistics": [
16+
{
17+
"file_path": "typed_wasm/src/lib.rs",
18+
"lines": 1030,
19+
"unsafe_blocks": 0,
20+
"panic_sites": 0,
21+
"unwrap_calls": 2,
22+
"allocation_sites": 10,
23+
"io_operations": 0,
24+
"threading_constructs": 0
25+
},
26+
{
27+
"file_path": "echidna-mcp/src/main.rs",
28+
"lines": 308,
29+
"unsafe_blocks": 0,
30+
"panic_sites": 0,
31+
"unwrap_calls": 0,
32+
"allocation_sites": 6,
33+
"io_operations": 1,
34+
"threading_constructs": 0
35+
},
36+
{
37+
"file_path": "echidna-wire/build.rs",
38+
"lines": 12,
39+
"unsafe_blocks": 0,
40+
"panic_sites": 0,
41+
"unwrap_calls": 1,
42+
"allocation_sites": 0,
43+
"io_operations": 0,
44+
"threading_constructs": 0
45+
},
46+
{
47+
"file_path": "echidna-core/src/types.rs",
48+
"lines": 478,
49+
"unsafe_blocks": 0,
50+
"panic_sites": 0,
51+
"unwrap_calls": 0,
52+
"allocation_sites": 10,
53+
"io_operations": 0,
54+
"threading_constructs": 0
55+
}
56+
],
57+
"recommended_attacks": [
58+
"memory",
59+
"cpu"
60+
],
61+
"dependency_graph": {
62+
"edges": []
63+
},
64+
"taint_matrix": {
65+
"rows": []
66+
}
67+
}

‎reports/blitz-2026-04-25-late/src-abi.json‎

Lines changed: 151 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,151 @@
1+
{
2+
"program_path": "src/abi",
3+
"language": "idris",
4+
"frameworks": [],
5+
"weak_points": [],
6+
"statistics": {
7+
"total_lines": 7652,
8+
"unsafe_blocks": 204,
9+
"panic_sites": 0,
10+
"unwrap_calls": 0,
11+
"allocation_sites": 0,
12+
"io_operations": 0,
13+
"threading_constructs": 0
14+
},
15+
"file_statistics": [
16+
{
17+
"file_path": "Boj/Foreign.idr",
18+
"lines": 271,
19+
"unsafe_blocks": 19,
20+
"panic_sites": 0,
21+
"unwrap_calls": 0,
22+
"allocation_sites": 0,
23+
"io_operations": 0,
24+
"threading_constructs": 0
25+
},
26+
{
27+
"file_path": "BojForeign.idr",
28+
"lines": 271,
29+
"unsafe_blocks": 19,
30+
"panic_sites": 0,
31+
"unwrap_calls": 0,
32+
"allocation_sites": 0,
33+
"io_operations": 0,
34+
"threading_constructs": 0
35+
},
36+
{
37+
"file_path": "EchidnaABI/Foreign.idr",
38+
"lines": 217,
39+
"unsafe_blocks": 12,
40+
"panic_sites": 0,
41+
"unwrap_calls": 0,
42+
"allocation_sites": 0,
43+
"io_operations": 0,
44+
"threading_constructs": 0
45+
},
46+
{
47+
"file_path": "Foreign.idr",
48+
"lines": 217,
49+
"unsafe_blocks": 12,
50+
"panic_sites": 0,
51+
"unwrap_calls": 0,
52+
"allocation_sites": 0,
53+
"io_operations": 0,
54+
"threading_constructs": 0
55+
},
56+
{
57+
"file_path": "Overlay/Foreign.idr",
58+
"lines": 522,
59+
"unsafe_blocks": 34,
60+
"panic_sites": 0,
61+
"unwrap_calls": 0,
62+
"allocation_sites": 0,
63+
"io_operations": 0,
64+
"threading_constructs": 0
65+
},
66+
{
67+
"file_path": "OverlayForeign.idr",
68+
"lines": 522,
69+
"unsafe_blocks": 34,
70+
"panic_sites": 0,
71+
"unwrap_calls": 0,
72+
"allocation_sites": 0,
73+
"io_operations": 0,
74+
"threading_constructs": 0
75+
},
76+
{
77+
"file_path": "Tentacles/Foreign.idr",
78+
"lines": 350,
79+
"unsafe_blocks": 20,
80+
"panic_sites": 0,
81+
"unwrap_calls": 0,
82+
"allocation_sites": 0,
83+
"io_operations": 0,
84+
"threading_constructs": 0
85+
},
86+
{
87+
"file_path": "TentaclesForeign.idr",
88+
"lines": 350,
89+
"unsafe_blocks": 20,
90+
"panic_sites": 0,
91+
"unwrap_calls": 0,
92+
"allocation_sites": 0,
93+
"io_operations": 0,
94+
"threading_constructs": 0
95+
},
96+
{
97+
"file_path": "TypeLL/Foreign.idr",
98+
"lines": 262,
99+
"unsafe_blocks": 17,
100+
"panic_sites": 0,
101+
"unwrap_calls": 0,
102+
"allocation_sites": 0,
103+
"io_operations": 0,
104+
"threading_constructs": 0
105+
},
106+
{
107+
"file_path": "TypeLLForeign.idr",
108+
"lines": 262,
109+
"unsafe_blocks": 17,
110+
"panic_sites": 0,
111+
"unwrap_calls": 0,
112+
"allocation_sites": 0,
113+
"io_operations": 0,
114+
"threading_constructs": 0
115+
}
116+
],
117+
"recommended_attacks": [
118+
"cpu"
119+
],
120+
"dependency_graph": {
121+
"edges": [
122+
{
123+
"from": "BojForeign.idr",
124+
"to": "Foreign.idr",
125+
"relation": "shared_dir:",
126+
"weight": 1.0
127+
},
128+
{
129+
"from": "Foreign.idr",
130+
"to": "OverlayForeign.idr",
131+
"relation": "shared_dir:",
132+
"weight": 1.0
133+
},
134+
{
135+
"from": "OverlayForeign.idr",
136+
"to": "TentaclesForeign.idr",
137+
"relation": "shared_dir:",
138+
"weight": 1.0
139+
},
140+
{
141+
"from": "TentaclesForeign.idr",
142+
"to": "TypeLLForeign.idr",
143+
"relation": "shared_dir:",
144+
"weight": 1.0
145+
}
146+
]
147+
},
148+
"taint_matrix": {
149+
"rows": []
150+
}
151+
}

0 commit comments

Comments
 (0)