docs(proof): PROOF-PROGRAMME.md — first-principles 3-layer landscape (#104)

## What

PROOF-PROGRAMME.md — strategic plan for moving panic-attack from "PA1 +
PA2 done" (the two Idris2 modules at `src/abi/*.idr`) to **end-to-end
formally sound across Surface / Engine / Persistence**.

## Three layers

| Layer | What | Prover | LoC est. |
|---|---|---|---|
| **1. Surface** | Per-category detection soundness + completeness (25
PA codes + 1 shared comment/string-strip idempotence) | Idris2 sibling
to PA1/PA2 | ~750 |
| **2. Engine** | miniKanren unification + search + taint propagation
(fixed-point lattice) | Coq (Bender-style) | ~1500 |
| **3. Persistence** | Hexad↔Octad roundtrip + attestation chain
unforgeability + bridge reachability | Idris2 + proptest + Coq | ~800 |

## Proven cross-fit (from 2026-06-02 survey)

Two leaf-validator candidates qualify as **semantic-equivalent +
perf-neutral**:

| # | Swap | Where | 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 vs
proven's Idris2 reference |
| 2 | `SafeUrl::parse` | `src/storage/mod.rs:1071` `VERISIMDB_URL`
unvalidated before HTTP POST | port-to-Rust wrapping `url::Url` +
proptest scheme-required invariant |

Both **NOT FFI** — `libproven.so` dylib build dep too heavy for `cargo
install panic-attack` distribution model.

**Skip list** (semantic mismatch / already total): SafeJson (serde
already total + typed), SafeRegex (regex crate is RE2-lineage),
SafeDateTime (chrono total on emit), SafeCommand (no shell
interpolation), SafeEnv (compile-time keys), SafeUUID (we use
deterministic timestamps for replayability).

**Proven gaps** (must prove from first principles): miniKanren engine,
hexad data model, A2ML attestation chain, bridge reachability, sweep
tracker, adjudicate/axial merge logic.

## Sequencing

9 phases, ~16 calendar weeks to row 8. Per-phase: 1 PR. Per-row items
parallelisable.

Each new proof module must `Qed`-close (Coq) / be totality-checked
(Idris2) before landing. No `Admitted` placeholders.

## Why now

ROADMAP "Long-Term" bullet "Formal verification of core analysis rules
(via proven library)" — this document operationalises it.

## What this is NOT

- A 25-PR storm. Group by phase.
- A perf regression. proven swap-outs are perf-evaluated; rest is pure
proof artefacts.
- A sweep adding `Admitted`. Honest open obligations stay in
PROOF-NEEDS.md.

## Refs

- `PROOF-NEEDS.md` — immediate ledger
- `src/abi/PatternCompleteness.idr` (PA1)
- `src/abi/ClassificationSoundness.idr` (PA2)
- `hyperpolymath/proven` — leaf validators (cross-fit candidates listed
in §Proven cross-fit)

Author: hyperpolymath

PROOF-PROGRAMME.md

@@ -0,0 +1,198 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+# 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)**:
+```idris
+-- 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](#proven-cross-fit) 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.