Skip to content

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

Description

@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 FFIlibproven.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

Metadata

Metadata

Assignees

No one assigned

    Labels

    choreRoutine maintenance with no behaviour changemigrationPorting between languages or toolchains (e.g. -> AffineScript)proofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debt

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions