Split Rust/FFI/proof safety alerts by runtime, memory, proof, and test-only risk

[hyperpolymath]

Failure type

echidna has mixed Rust/FFI/proof safety alerts that need triage by risk class, not a single generic code-safety bucket.

Evidence

On 2026-06-06, open Hypatia code-safety alerts include:

• 22 unwrap_without_check
• 10 unwrap_dangerous_default
• 9 expect_in_hot_path
• 7 unsafe_block
• 7 as_ptr
• 3 zig_ptr_cast
• 3 lock_unwrap
• 2 from_raw
• 2 agda_postulate
• 1 panic_macro
• 1 mem_forget

Examples touch production-looking Rust server/prover/FFI paths as well as tests and proof/FFI boundary code.

Expected behavior

Split into sub-buckets:

• runtime crash/availability: unwrap, expect, panic, lock unwrap;
• FFI memory safety: unsafe blocks, raw pointers, from_raw, mem_forget, Zig pointer casts;
• proof soundness: Agda postulates and proof bypasses;
• test-only idioms: should be downgraded or suppressed if clearly test fixtures.

Route

• panicbot: runtime crash/availability review.
• echidnabot: proof/FFI soundness review.
• rhodibot: mechanical refactors only after tests prove behavior.

Safety notes

No estate-wide auto-rewrite. Replacing unwrap() with default values can silently corrupt proof/prover behavior. Each production finding should either propagate an error, prove invariant preconditions, or carry a local suppression rationale.

Acceptance criteria

• Findings include precise line numbers where possible.
• Test-only code is downgraded or suppressed with rationale.
• Production FFI/proof findings are reviewed by the right bot route.
• Fixes preserve behavior and are covered by targeted tests.