feat(assail): route languages through a tested table; retire the vacuous PA1

0-AI-MANIFEST.a2ml

@@ -37,8 +37,6 @@
       (jit-context "src/jit_context.rs"
         "JIT-framework classifier: Cranelift / Llvm / Wasm / Javascript / None"))
     (proof-modules
-      (pa1 "src/abi/PatternCompleteness.idr"
-        "Pattern detection completeness — every Lang / WPCategory has a detector")
       (pa2 "src/abi/ClassificationSoundness.idr"
         "Classification soundness — Severity total order + maxSeverity commutativity")
       (layer-1-0 "src/abi/Stripping.idr"

EXPLAINME.adoc

@@ -52,7 +52,7 @@ The README makes claims. This file backs them up.
 | `src/comment_marker.rs` | Inline `// panic-attack: accepted [- reason]` suppression marker — `//` / `#` / `--` / `;` / `%` leaders, string-literal aware
 | `src/ffi_kind.rs` | UnsafeFFI (PA013) subtyping: BuildSystem (`build.zig` / `build.rs` — audit-accepted), RuntimeAbi (`bindings/` / `ffi/` / `sys/` / `cdef.zig`), TestMock (`tests/mocks/` / `_stub`), Unknown
 | `src/jit_context.rs` | JIT-framework classifier: Cranelift / Llvm / Wasm / Javascript / None; `transmute_targets_fn_ptr` recogniser for fn-ptr type-punning
-| `src/abi/PanicAttack/ABI/PatternCompleteness.idr` | PA1 Idris2 model of analyzer dispatch; vacuous as stated (see `PROOF-NEEDS.adoc`)
+| `src/assail/routing.rs` | PA1 routing table: which analyzer each language reaches and when cross-language checks run; its claims are tested exhaustively (see `PROOF-NEEDS.adoc`)
 | `src/abi/PanicAttack/ABI/ClassificationSoundness.idr` | PA2 Idris2 proof — severity total order, `sevMax` upper bounds, monotone encoding
 | `src/abi/PanicAttack/ABI/Stripping.idr` | Layer 1.0 — Idris2 model of line-comment stripping, proved idempotent (`stripLineCommentsIdempotent`)
 | `src/kanren/` | Logic engine (unification, fact database, taint, cross-lang)

PROOF-NEEDS.adoc

@@ -104,25 +104,34 @@ signature scheme. So these are theorems of a symbolic (Dolev-Yao style)
 model, not a computational security reduction. Model to
 `src/attestation/`: `ASSUMED`. A computational proof is not claimed.
 
-|Every language reaches an analyzer; every weak-point category has a
-detector; cross-language checks run on every file (PA1)
-|`src/abi/PanicAttack/ABI/PatternCompleteness.idr`
-|`PROVEN` (model); supports no claim about the Rust code
-|The theorem is vacuous: `GenericAnalyzer : HasAnalyzer lang` inhabits
-the witness type for every language, so it holds whatever the dispatch
-does. Rust gives the narrower guarantee that actually holds:
-`match file_lang` in `src/assail/analyzer.rs` ends in
-`_ => analyze_generic`, and `rustc` checks the match is exhaustive. That
-covers every file that reaches the match. A file with no source language
-and no configuration adapter (`Language::Unknown`, no adapter) is marked
-`unsupported` in the coverage ledger and skipped first, so not every file
-reaches an analyzer.
-
-The model has also drifted. Its `Lang` has 50 constructors and
-`src/types.rs` has 52; `C` and `Php` are missing. `crossLangAlwaysApplied`
-says cross-language checks run on every file, but the Rust code skips them
-when `configuration.is_some()`. That model claim is false of the
-implementation.
+|Analyzer routing (PA1). (a) Every language analyzer in `analyzer.rs` is
+reached by some language. (b) No language falls back to the generic
+analyzer while a dedicated one exists for it. (c) Cross-language checks run
+exactly on non-configuration content, and on scripts embedded in
+configuration. (d) The README's language counts equal the languages the
+table supports.
+|`src/assail/routing.rs`: `route`, `Route::analyzer`, `runs_cross_language`
+and their tests
+|`TESTED`
+|The dispatch in `analyze_inner` matches on `route(file_lang)`, so the
+table is the code that runs, not a model of it. `route` and the dispatch
+are exhaustive matches with no wildcard, so `rustc` makes every language
+and every route explicit. The tests run over all 52 `Language` variants
+(`Language::ALL`, kept complete by an exhaustive `ordinal` match). (a) and
+(b) compare the table with the analyzer methods found in the source. (c)
+scans a Justfile and a Lua file end to end. Each test was seen to fail on
+a planted fault: an unrouted analyzer, Java sent to the generic analyzer,
+cross-language checks forced on, and the README's stale count of 49.
+
+Routing is not coverage: `Language::Unknown` goes to `InputAdapter`, and a
+file there with no configuration adapter is marked `unsupported` in the
+coverage ledger and skipped. So (a) and (b) say which analyzer each
+language reaches, not that every file is analysed.
+
+This replaces the Idris2 `PatternCompleteness.idr`, which was vacuous
+(`GenericAnalyzer` inhabited its witness for every language), stale (50 of
+52 languages) and partly false (it said cross-language checks always
+run). It is retired.
 
 |Declarations for the ABI-facing types and their C integer encodings
 |`src/abi/PanicAttack/ABI/Types.idr`
@@ -193,10 +202,18 @@ gap.
 fixed point) is theory and belongs in Agda with Rocq and Lean rechecks.
 Its realisation in `src/kanren/` is a Rust obligation.
 
-|Replace or retire PA1
-|Creusot/Pearlite and Verus, or retire
-|A non-vacuous statement would be, for example, that each language with
-a dedicated analyzer is routed to it. If that is not wanted, retire the
-module, because `rustc`'s exhaustiveness check already gives the current
-guarantee.
+|Prove PA1 (a) to (c) on `route` and `runs_cross_language`
+|Creusot/Pearlite and Verus
+|Pearlite contracts on the two functions, proved by both verifiers. The
+tests above are exhaustive over a finite enum, but they are tests, and (a)
+reads the source with a pattern match. (d) is a documentation check and
+stays a test.
+
+|Unquoted `http://` URLs are missed by the cross-language check
+|Fix first, then test
+|`analyze_cross_language` strips C-style `//` comments from every file
+before matching, which also cuts `curl http://host` in shell. A quoted
+URL is found; an unquoted one in a `.sh` file or a Justfile recipe is not.
+This is a recall gap in the InsecureProtocol detector, found while testing
+PA1 (c).
 |===

PROOF-PROGRAMME.adoc

@@ -1,3 +1,3 @@
 == PROOF-PROGRAMME.md — panic-attack from first principles
 
 ____
@@ -14,10 +14,11 @@
 [width="100%",cols="34%,33%,33%",options="header",]
 |===
 |ID |File |Mechanises
-|*PA1* |`+src/abi/PanicAttack/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+`.
+|*PA1* |`+src/assail/routing.rs+` |The routing table the dispatch uses: every
+language analyzer is reached, no language falls back to the generic
+analyzer while a dedicated one exists, cross-language checks run exactly
+off configuration, and the README language counts match. Tested
+exhaustively; the earlier Idris2 model was vacuous and is retired.
 
 |*PA2* |`+src/abi/PanicAttack/ABI/ClassificationSoundness.idr+` |`+Severity+` is totally
 ordered (`+LTE+`); `+maxSeverity+` is commutative + idempotent; numeric
@@ -316,7 +317,7 @@
 
 * `+PROOF-NEEDS.md+` — current proof-debt ledger (this document is the
 long-term plan; that one tracks the immediate next step).
-* `+src/abi/PanicAttack/ABI/PatternCompleteness.idr+` (PA1)
+* `+src/assail/routing.rs+` (PA1)
 * `+src/abi/PanicAttack/ABI/ClassificationSoundness.idr+` (PA2)
 * `+hyperpolymath/proven+` — leaf validator library; cross-fit
 candidates listed above.

README.adoc

@@ -12,7 +12,7 @@ image:https://api.thegreenwebfoundation.org/greencheckimage/github.com[Green Web
 image:https://img.shields.io/badge/status-active-green[Status]
 image:https://img.shields.io/badge/domain-security--analysis-blue[Domain]
 image:https://img.shields.io/badge/tests-897%20passing-brightgreen[Tests]
-image:https://img.shields.io/badge/languages-49-blue[Languages]
+image:https://img.shields.io/badge/languages-51-blue[Languages]
 
 **panic-attack** is a multi-language security analysis and stress-testing system.
 
@@ -69,7 +69,7 @@ panic-attack exists to address this by combining:
 
 panic-attack provides:
 
-* **49-language static analysis** across multiple families
+* **51-language static analysis** across multiple families
 * **Weak point detection** (30 canonical categories; see the PA rule-ID table below)
 * **Attack simulation (6 axes)**: CPU, memory, disk, network, concurrency, time
 * **miniKanren logic engine** for taint analysis and cross-language reasoning
@@ -235,7 +235,7 @@ Current state: **v2.5.0**
 * v2.5.5 cohort landed 2026-06-02: context-aware FP suppression via `test_context` / `comment_marker` / `ffi_kind` / `jit_context` modules — `// panic-attack: accepted` inline markers, automatic PanicPath suppression in test-only code, build.zig/build.rs auto-accept, Cranelift/LLVM/Wasm/JS JIT detection. See `PROOF-PROGRAMME.md` for the formal soundness landscape
 * 0 warnings
 * 38 CLI subcommands
-* 49 supported languages (30 canonical weak-point categories PA001–PA029; `PA001b` is a distinct stable rule ID grouped with PA001 under one allocation semantic class for cross-tool de-duplication)
+* 51 supported languages (30 canonical weak-point categories PA001–PA029; `PA001b` is a distinct stable rule ID grouped with PA001 under one allocation semantic class for cross-tool de-duplication)
 
 See link:ROADMAP.adoc[ROADMAP.adoc] for full capability breakdown and milestones.