Repository navigation
proofs(Layer 3 follow-up): port proven SafePath + SafeUrl into panic-attack #115
Description
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.solink. - 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)
Activity
release(v2.5.5): tag the 11-PR context-awareness cohort (#118)
feat(safe_path): port proven SafePath as pure-Rust + add traversal gu…
hyperpolymath commentedon Jun 2, 2026
Part 1 of 2 — SafePath landed via #120
SafePathported as pure-Rust atsrc/safe_path.rs(merged 2026-06-02 19:22Z):has_traversal(path: &str) -> boolmirrorsproven::Operations::containsTraversalsanitize_filename(filename: &str) -> Stringmirrorsproven::Operations::sanitizeSegmentsrc/main.rs:2360(BridgeAction::Triage) +src/main.rs:2423(BridgeAction::Status) — both now reject..segments BEFORE any disk I/O, replacing the priorcanonicalize().unwrap_or_else(|_| dir.clone())silent-fallback pattern.src/abduct/mod.rscanonicalize sites (lines 123 + 266) were already safe (usewith_context+?); left untouched.Part 2 of 2 — SafeUrl still open
SafeUrl::parseforsrc/storage/mod.rs:1071VERISIMDB_URLis still pending. Needs more careful audit because:http://localhost:8080when env unset).SafeUrlparser is an RFC-3986 scheme/host/port/path/query/fragment splitter; the Rust port can wrapurl::Urlfrom theurlcrate + add proptest scheme-required invariants against proven's reference.Keeping this issue open as the SafeUrl tracker.