PROOF-PROGRAMME.adoc

PROOF-PROGRAMME.md — panic-attack from first principles

Strategic plan for moving panic-attack from “two completed sibling Idris2 proofs (PA1 + PA2)” to end-to-end formal soundness of detection, inference, and persistence — without changing perf or functionality.

Status as of 2026-06-02

Completed proofs

ID	File	Mechanises
PA1	src/abi/PatternCompleteness.idr	Every Lang constructor has at least one analyzer; every WPCategory has at least one detector; cross-language checks apply uniformly. Top theorem: completeScanForAll.
PA2	src/abi/ClassificationSoundness.idr	Severity is totally ordered (LTE); maxSeverity is commutative + idempotent; numeric ABI encoding preserves the ordering.

Open obligations (from PROOF-NEEDS.md line 19–23)

Component	Property
Bridge reachability soundness	No reachable dep wrongly classified as phantom.
Attestation chain unforgeability	Intent/evidence/seal triple cryptographically binds; tampering detectable.
Kanren taint analysis	Taint propagation tracks every tainted dataflow (no missed sinks).

Three-layer landscape

Layer 1 — Surface (per-category detection soundness + completeness)

For each WeakPointCategory, two properties: - Soundness: every detector emission corresponds to a real instance of the pattern. - Completeness: every real instance of the pattern is detected (modulo declared scope — e.g. test files, see [[v2.5.5 test_context]]).

PA1 proves dispatch completeness (every category has a detector). PA2 proves severity ordering on what’s emitted. Layer-1 work extends this per category to the pattern-recognition function itself.

Layer 1.0 — Common machinery (one-time, foundational): - Formalise Pattern as a regex/AST predicate over normalised source. - Prove the comment / string-literal stripping function (strip_inline_cfg_test_modules + global comment-strip) is idempotent and preserves non-token positions. This justifies the analyzer’s stripping pass as a sound preprocessing step. - Recommended prover: Idris2 (sibling to existing PA1/PA2). Difficulty: medium. Value: every category proof becomes a simple application of Layer 1.0
the category’s regex.

Layer 1.1–1.25 — Per category (25 obligations, parallelisable):

For PA001..PA025 each, state and prove:

soundness :  (file : String) -> (locs : List Loc)
          -> detect category file = Just locs
          -> AllOf (\loc => isInstanceOf category (locate file loc)) locs

completeness :  (file : String) -> (loc : Loc)
             -> isInstanceOf category (locate file loc)
             -> stripFalsePositives category file loc = NotSuppressed
             -> Elem loc (Maybe.toList (detect category file))

Worked example — PA004 (UnsafeCode):

-- src/abi/PA004_UnsafeCode.idr
SoundnessPA004 : (file : String) -> (loc : Loc)
              -> contains (stripStrings file) "unsafe " loc
              -> isUnsafeBlock (locate file loc)

This is decidable because contains is a constructive predicate. The matching Rust detector at src/assail/analyzer.rs:1052 simply mirrors the same predicate.

Estimate: 25 obligations × ~30 LoC each = ~750 LoC of Idris2 proof; ~2 weeks of focused work.

Cross-fit with proven: Layer-1 categories that wrap simple validators (PA017 PathTraversal, PA022 CryptoMisuse on the hash-algorithm side) can borrow proofs from proven’s SafePath and SafeCrypto directly — see proven swap-outs below.

Layer 2 — Engine (inference: miniKanren + taint)

2.1 miniKanren unification soundness

src/kanren/core.rs ships a v2.0.0 microKanren-style engine: Term, Substitution, Goal, mplus/bind. Three properties to mechanise:

1. Unification correctness — unify(u, v, σ) returns σ' iff there’s an mgu θ with θ(u) = θ(v) extending σ.

2. Substitution composition — walk*(t, σ) is the canonical representative of t’s equivalence class in σ.

3. Search completeness — mplus interleaving doesn’t drop a satisfiable goal under bounded depth.

Recommended prover: Coq (because the standard miniKanren correctness proofs by Bender/Hemann use Coq; reuse their reasoning machinery). Difficulty: hard but well-trodden.

Estimate: ~1500 LoC Coq (Bender’s thesis is ~900 LoC; we extend with our taint goals). 4 weeks.

2.2 Taint propagation completeness

src/kanren/taint.rs defines taint flow rules (CommandInjection / UnsafeDeserialization / DynamicCodeExecution / UnsafeFFI / AtomExhaustion / PathTraversal). The property:

If a source-to-sink dataflow path exists in the program AST, the rule engine emits a WeakPoint whose recommended_attack reflects the sink category.

Two sub-obligations: - Source coverage: every taint source the rules recognise is enumerated in a Datasource ADT and reflected in the proof. - Sink coverage: same for sinks. - Transitivity: if flows(a→b) and flows(b→c), then flows(a→c).

Mechanise as a fixed-point lattice in Coq. The kanren engine becomes the procedural computation of the lattice; the proof shows the procedural answer = the least fixed point.

2.3 Cross-language analyzer soundness

src/kanren/crosslang.rs — when a finding crosses an FFI boundary (Rust ↔ Zig, Rust ↔ C, Python ↔ Rust), the cross-language rules emit a UnsafeFFI weak point. Soundness here = the FFI boundary in the AST is a real ABI boundary.

This is hard because it requires modelling ABIs in the prover. Defer to Layer-2 follow-up; PA1’s per-language detector dispatch already gives us a coarse safety net.

Layer 3 — Persistence + Integrity

3.1 Hexad↔Octad isomorphism

src/storage/mod.rs defines PanicAttackHexad (6-tuple in panic-attack’s own model) and pushes to verisimdb as an Octad (8-tuple). The hexad has fewer fields; the octad adds attestation
provenance.

Property: the round-trip panic-attack-hexad → verisimdb-octad → panic-attack-hexad is the identity on the hexad fields.

Recommended prover: proptest in Rust with arbitrary instances on both records. The structural-equivalence proof is trivial enough (both are records of Option<String> and Vec<String>) that property testing is sufficient evidence; formalising in Idris2 would be busywork.

Estimate: 50 LoC proptest, 1 day.

3.2 Attestation chain unforgeability

src/attestation/{chain,envelope,evidence,intent,seal}.rs. The triple is Intent → Evidence → Seal; the Seal includes an Ed25519 signature over (Intent, Evidence).

Properties: 1. Integrity: tampering with Intent or Evidence invalidates Seal. 2. Authenticity: only the holder of the signing key can produce a valid Seal. 3. Non-repudiation: a valid Seal is publicly verifiable.

These reduce to standard Ed25519 properties (EUF-CMA). Mechanise via: - A small Idris2 model of the chain with abstract Sig and Hash operations. - An assumption ed25519_euf_cma : ∀ k m m'. Verify(k, m, Sign(k, m)) ∧ ¬Verify(k, m', Sign(k, m)). - Derive (1)–(3) from the assumption + chain structure.

The proof is trivial given the cryptographic assumption — the work is being honest about the assumption and matching it to the ed25519-dalek API our Rust code uses.

Recommended prover: Idris2 (matches PA1/PA2; tiny). Difficulty: easy. Value: high — attestation is load-bearing for the audit trail.

Estimate: 200 LoC Idris2, 3 days.

3.3 Bridge reachability soundness

src/bridge/reachability.rs walks Cargo.lock + crate graph to classify deps as Mitigable / Unmitigable / Informational. The “phantom” classification is the most consequential — a phantom dep that’s actually reachable becomes a missed vuln.

Property: classify(dep) = Phantom ⇒ dep does not appear on any reachable path from the root crate.

This is a graph reachability proof. Formalise the lockfile as a labelled graph, the reachability predicate as transitive closure of dep edges, and classify as a sound under-approximation: if it returns Phantom, the corresponding reachability is False.

Recommended prover: Coq (graph reasoning is well-trodden; Idris2 can do it but Coq’s Set libraries are nicer for transitive closure). Difficulty: medium. Value: high — this is the PR #87 issue from earlier.

Estimate: ~600 LoC Coq, 1.5 weeks.

Proven cross-fit

From the hyperpolymath/proven survey (2026-06-02): two leaf-validator candidates qualify as semantic-equivalent + perf-neutral:

#	Swap	Where	Path
1	SafePath::has_traversal + sanitize_filename	src/abduct/mod.rs:123,266; src/main.rs:2314,2377 (fs::canonicalize(..).unwrap_or_else(|_| dir) patterns)	port-to-Rust with proptest invariants against proven’s Idris2 reference. NOT FFI (dylib build cost too high for cargo install).
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.

What proven does NOT cover (and Layer 1–3 must prove from first principles): - miniKanren engine (Layer 2.1) - 49-language analyzer dispatch (PA1 already covers this) - Hexad/Octad data model (Layer 3.1) - A2ML attestation chain (Layer 3.2) - Bridge reachability (Layer 3.3) - Sweep tracker / mass-panic temporal index (no equivalent) - Adjudicate / Axial / Ambush / Abduct merge logic (bespoke)

Skip (semantic mismatch or already-total): - SafeJson — serde_json::from_str is already total + typed. - SafeRegex — regex crate is already RE2-lineage (linear-time, ReDoS-safe). - SafeDateTime — chrono::Utc::now().to_rfc3339() is total on emit. - SafeCommand — Command::new(&str_args) doesn’t shell-interpolate. - SafeEnv — env keys in panic-attack are compile-time literals. - SafeUUID — semantic mismatch (we use deterministic timestamps for replayability).

Sequencing

Recommended order (each row is parallel-iseable; rows are sequenced):

#	Phase	Output	Estimated effort	Risk
1	Foundation: Layer 1.0 (comment/string-strip idempotence + token preservation)	src/abi/Stripping.idr + 1 Idris2 module	3–5 days	low
2	Quick wins: Hexad↔Octad roundtrip proptest + Layer 1 PA001/PA004/PA017	200 LoC Rust proptest + 3 Idris2 modules	1 week	low
3	Cross-fit: SafePath + SafeUrl ports (with proptest against proven’s Idris2 reference)	2 Rust modules + 2 proptest suites	1 week	low
4	Persistence: Attestation chain (Layer 3.2)	1 Idris2 module	1 week	low
5	Engine: miniKanren correctness (Layer 2.1, ~1500 LoC Coq)	formal/Kanren.v	4 weeks	medium (well-trodden, but big)
6	Surface: remaining PA categories (Layer 1.1–1.25 minus quick-wins)	~22 Idris2 modules	4 weeks	medium
7	Reachability: bridge soundness (Layer 3.3, Coq graph)	formal/BridgeReachability.v	1.5 weeks	medium
8	Taint completeness: kanren taint flow (Layer 2.2)	extends formal/Kanren.v	3 weeks	high (fixpoint lattice + soundness witness)
9	FFI ABI (Layer 2.3 deferred — needs ABI modelling)	TBD	TBD	high — defer until 1–8 land

Total to row 8: ~16 calendar weeks of focused proof work for “panic-attack is provably sound to the per-category and per-flow level”. After row 8, only the cross-language FFI ABI soundness remains as an aspirational item.

What this is NOT

• Not a sweep to add Admitted placeholders. Every new Idris2 module must Qed-close (or its Coq equivalent) before landing. If a proof is too hard, the obligation stays open and we record it in PROOF-NEEDS.md — that’s the honest path.

• Not a performance regression. proven swap-outs are explicitly evaluated for perf neutrality; the rest of the programme is pure docs/proof artefacts that don’t touch the hot path.

• Not a 25-PR storm. Group by phase; one PR per phase row above.

References

• PROOF-NEEDS.md — current proof-debt ledger (this document is the long-term plan; that one tracks the immediate next step).

• src/abi/PatternCompleteness.idr (PA1)

• src/abi/ClassificationSoundness.idr (PA2)

• hyperpolymath/proven — leaf validator library; cross-fit candidates listed above.

• ROADMAP.adoc “Long-Term” section: “Formal verification of core analysis rules (via proven library)” — this document operationalises that bullet.