proofs(Layer 3 follow-up): port proven SafePath + SafeUrl into panic-attack

[hyperpolymath]

Context

The 2026-06-02 hyperpolymath/proven cross-fit survey (recorded in PROOF-PROGRAMME.md) identified two leaf-validator modules as semantic-equivalent + perf-neutral candidates:

#	Swap	Where in panic-attack	How
1	SafePath::has_traversal + sanitize_filename	src/abduct/mod.rs:123,266; src/main.rs:2314,2377 (fs::canonicalize(..).unwrap_or_else)	port-to-Rust + proptest invariants against proven's Idris2 reference
2	SafeUrl::parse	src/storage/mod.rs:1071 VERISIMDB_URL (currently raw String, no scheme/host validation before HTTP POST)	port-to-Rust wrapping url::Url + proptest scheme-required invariant

NOT via FFI — libproven.so dylib build dep too heavy for cargo install panic-attack's distribution model.

Why these two

Both are leaves with clear soundness statements (traversal-rejection + RFC-3986 scheme/host parse) AND clear panic-attack failure modes (silent fallback on canonicalize fail; unvalidated env-var concatenated into POST URL).

The skip list (semantic mismatch or already-total): SafeJson (serde already total + typed), SafeRegex (regex is RE2-lineage), SafeDateTime (chrono total on emit), SafeCommand (Command::new doesn't shell-interpolate), SafeEnv (env keys are compile-time literals), SafeUUID (we use deterministic-timestamp UUIDs by design).

Acceptance per swap

• New Rust module under src/safe/ or similar.
• proptest suite verifying the invariant against proven's Idris2 reference (read the Idris2 source — proven repo src/Proven/SafePath.idr / SafeUrl.idr).
• Call sites migrated.
• No new dylib deps. No libproven.so link.
• Benchmark showing zero perf regression on the relevant hot path.

Refs

• PROOF-PROGRAMME.md §Proven cross-fit + row 3 of the sequencing
• PR docs(proof): PROOF-PROGRAMME.md — first-principles 3-layer landscape #104 (PROOF-PROGRAMME with the verdict)
• hyperpolymath/proven repo (the reference)

[hyperpolymath]

Part 1 of 2 — SafePath landed via #120

SafePath ported as pure-Rust at src/safe_path.rs (merged 2026-06-02 19:22Z):

• has_traversal(path: &str) -> bool mirrors proven::Operations::containsTraversal
• sanitize_filename(filename: &str) -> String mirrors proven::Operations::sanitizeSegment
• 23 tests including 5 proptest invariants matching proven's Idris2 reference lemmas
• Wire-in: src/main.rs:2360 (BridgeAction::Triage) + src/main.rs:2423 (BridgeAction::Status) — both now reject .. segments BEFORE any disk I/O, replacing the prior canonicalize().unwrap_or_else(|_| dir.clone()) silent-fallback pattern.
• The src/abduct/mod.rs canonicalize sites (lines 123 + 266) were already safe (use with_context + ?); left untouched.

Part 2 of 2 — SafeUrl still open

SafeUrl::parse for src/storage/mod.rs:1071 VERISIMDB_URL is still pending. Needs more careful audit because:

• The URL flows through unvalidated into HTTP POST construction.
• Migration must preserve compatibility with the localhost-default behaviour (default http://localhost:8080 when env unset).
• proven's SafeUrl parser is an RFC-3986 scheme/host/port/path/query/fragment splitter; the Rust port can wrap url::Url from the url crate + add proptest scheme-required invariants against proven's reference.

Keeping this issue open as the SafeUrl tracker.