|
| 1 | +# Echidna Chunked panic-attack Sweep — 2026-04-25 |
| 2 | + |
| 3 | +Single full-repo `panic-attack assail .` had timed out at 180s. |
| 4 | +This sweep splits the tree into 14 per-subdir chunks, each completing |
| 5 | +in < 30s for a combined wall time well under the prior single-run cap. |
| 6 | + |
| 7 | +## Per-chunk totals (severity counts) |
| 8 | + |
| 9 | +| Chunk | Critical | High | Medium | Total | |
| 10 | +| ------------------------------ | -------: | ---: | -----: | ----: | |
| 11 | +| `src/rust` | 26 | 6 | 2 | 34 | |
| 12 | +| `src/interfaces` | 0 | 6 | 0 | 6 | |
| 13 | +| `src/zig` | 0 | 1 | 0 | 1 | |
| 14 | +| `src/zig_ffi` | 0 | 1 | 0 | 1 | |
| 15 | +| `src/abi` | 1 | 0 | 0 | 1 | |
| 16 | +| `crates/echidna-mcp` | 0 | 1 | 0 | 1 | |
| 17 | +| `crates/echidna-core` | 0 | 0 | 0 | 0 | |
| 18 | +| `crates/echidna-wire` | 0 | 0 | 0 | 0 | |
| 19 | +| `crates/typed_wasm` | 0 | 0 | 0 | 0 | |
| 20 | +| `src/julia` | 0 | 0 | 0 | 0 | |
| 21 | +| `src/idris` | 0 | 0 | 0 | 0 | |
| 22 | +| `src/ada` | 0 | 0 | 0 | 0 | |
| 23 | +| `src/rescript` | 0 | 0 | 0 | 0 | |
| 24 | +| `src/ui` | 0 | 0 | 0 | 0 | |
| 25 | +| `src/chapel` | – | – | – | – | |
| 26 | +| **Total** | **27** | **15** | **2** | **44** | |
| 27 | + |
| 28 | +Note: `src/chapel` returned "Could not detect language" — panic-attack |
| 29 | +has no Chapel detector. Track separately. |
| 30 | + |
| 31 | +## Classification (per `feedback_panic_attack_*` memory rules) |
| 32 | + |
| 33 | +### Structural / expected (do not chase counts) |
| 34 | + |
| 35 | +- **26× Critical UnboundedAllocation in `src/rust/provers/*.rs`** — |
| 36 | + one per prover backend, file-level aggregation of `Vec::new()` / |
| 37 | + `String` allocations across 600+ LoC parsers. This is the |
| 38 | + PanicPath-is-file-level pattern: one finding per file, not one per |
| 39 | + site. The 26 backends with the highest Vec/parse density flag here. |
| 40 | + Investigation required per backend before any structural rewrite — |
| 41 | + most allocations are in error-message construction or proof-script |
| 42 | + parsing, both bounded in practice by `ProverConfig::timeout`. |
| 43 | + |
| 44 | +- **6× High UnsafeCode in `src/interfaces/*/ffi_wrapper.rs`** — two |
| 45 | + per FFI wrapper × three interfaces (rest, grpc, graphql). All |
| 46 | + calls into the Zig FFI shim's `extern "C"` surface plus `CStr::from_ptr`. |
| 47 | + These cannot be eliminated without dropping the FFI boundary; per |
| 48 | + `feedback_panic_attack_unsafe_blocks_meaning.md` this is the |
| 49 | + legitimate-FFI-try/catch class, not the banned partial-cast class. |
| 50 | + |
| 51 | +- **2× High UnsafeFFI in zig bridges** (`chapel_bridge.zig`, |
| 52 | + `ffi/axiom_spark_bridge.zig`) — required for cross-language FFI. |
| 53 | + |
| 54 | +- **1× Critical ProofDrift in `src/abi/echidnaabi.ipkg`** — flagged |
| 55 | + per `feedback_panic_attack_proofdrift_parameter_pattern.md`. The |
| 56 | + `.ipkg` is an Idris2 package manifest; the rule's "free Parameter |
| 57 | + unless inside designated Section Carriers" pattern doesn't quite |
| 58 | + fit a config file. Worth re-reading the rule's scope; likely a |
| 59 | + detector false-positive on `.ipkg` files. |
| 60 | + |
| 61 | +- **2× High UnsafeCode in `src/rust/proof_search.rs`** — Chapel FFI |
| 62 | + boundary; behind `--features chapel` cargo feature. Same class as |
| 63 | + the interface FFI wrappers. |
| 64 | + |
| 65 | +- **3× High UnsafeCode + 1× High ResourceLeak in `src/rust/ffi/`** — |
| 66 | + same FFI-boundary class. |
| 67 | + |
| 68 | +### Actionable today (low cost, structural fixes) |
| 69 | + |
| 70 | +- **1× High SupplyChain `crates/echidna-mcp/Cargo.toml`** — needs |
| 71 | + inspection. May be an unpinned dep version or a permissive feature |
| 72 | + set. |
| 73 | + |
| 74 | +- **1× Medium PanicPath `src/rust/provers/z3.rs`** — single panic site |
| 75 | + in a hot prover. Easy to convert to anyhow::Result. |
| 76 | + |
| 77 | +- **1× Medium InsecureProtocol `src/rust/provers/uppaal.rs`** — |
| 78 | + probably an `http://` URL in a comment or test fixture; quick |
| 79 | + audit. |
| 80 | + |
| 81 | +## Conclusion |
| 82 | + |
| 83 | +Chunked sweep replaces the 180s timeout with 14 fast per-subdir runs. |
| 84 | +Of 44 findings: ~41 are structural / FFI / file-level aggregation |
| 85 | +classes that the memory rules say not to chase by count, and 3 are |
| 86 | +genuinely actionable in a follow-up (1 SupplyChain, 1 PanicPath, |
| 87 | +1 InsecureProtocol). No new criticals discovered — all in the |
| 88 | +expected places (FFI surfaces and prover wrappers). |
| 89 | + |
| 90 | +Reports retained at `reports/panic-attack-chunks/*.json`. |
0 commit comments