feat: assay / assimilate / aggregate — proof-integration subcommands (#121)

## What

Three new a-themed subcommands that wire panic-attack into the
**PROOF-PROGRAMME** loop (survey → swap → fold-in-proofs), plus a small
version-drift fix.

### `assay` — proven-library substitution survey (`src/assay/mod.rs`)
Surveys a target for code that has a formally proven drop-in equivalent
in a `proven` / `proven-servers` library, reporting each candidate with
the proof artifact that backs it. Operationalises the "Proven cross-fit"
table in `PROOF-PROGRAMME.md` mechanically. Built-in catalogue:
`SafePath`, `SafeUrl`.

On this repo it reports `safe-path` **Offered** (port present in
`src/safe_path.rs`, 5 call sites still to rewire) and `safe-url`
**NoReplacementSource** (14 `VERISIMDB_URL` hits, not yet ported).

### `assimilate` — perform the swap (`src/assay/mod.rs`)
Stages the proven module into the tree, backs up the original
(`*.orig`), and records provenance — source **BLAKE3** hash + proof
backing + pending call-site rewires — under `.assimilated/`. Module
swaps are automatic; call-site rewiring is **reported, never
auto-edited** (mechanically editing arbitrary call sites is not a
reviewable operation).

### `aggregate` — fold external prover output into a report
(`src/aggregate/mod.rs`)
Ingests prover artifacts (Agda / Idris2 / Coq·Rocq / Lean / Isabelle /
TSTP / Alethe / DRAT·LRAT). Each artifact is **BLAKE3-hashed for
non-repudiation**, given a friendly name, classified (`Closed` / `Holes`
/ `Refuted` / `Indeterminate` — comment-stripped so prose mentioning
`postulate`/`Admitted` does not false-trigger), and reconciled against
an existing report's findings (**Backed / Corroborated /
Contradicted**).

Every verdict is explicitly conditioned on the named checker's trust;
the recorded hash lets the tool show exactly which bytes it was handed
if the assessment is later challenged. `@name`/`@covers
[claim:]kind:value` annotations travel inside the artifact; CLI
`--label`/`--covers` override.

## Proof foundation
Idris2 0.8.0 installed and the existing foundation re-verified from
first principles (all typecheck): `Types`, `Stripping` (Layer 1.0),
`PatternCompleteness` (PA1), `ClassificationSoundness` (PA2).

## Tests
17 new unit tests; full library suite (395) green; zero new compiler
warnings.

## Naming note
`assay` / `assimilate` are clean, no clashes. `aggregate` has **no CLI
clash** but conceptually overlaps `adjudicate` (aggregates
panic-attack's own reports) and `assemblyline` ("aggregate results"). A
thematically tighter alternative for "bring an external proof forward as
evidence" is **`adduce`** (or `annex`) — trivial rename if preferred.

## Still open (not in this PR)
- New subcommands not yet added to `README.adoc` / `EXPLAINME.adoc`
(CLAUDE.md count corrected).
- Next proof obligation (Layer 1.0 block/strings/composition/position,
issue #114) not yet advanced.

https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb

---
_Generated by [Claude
Code](https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

CHANGELOG.md

@@ -2,6 +2,43 @@
 
 ## [Unreleased]
 
+### Added — `assay` / `assimilate` / `aggregate` proof-integration subcommands
+
+Three new a-themed subcommands that wire panic-attack into the
+PROOF-PROGRAMME loop (survey → swap → fold-in-proofs):
+
+- **`panic-attack assay [TARGET] [--proven DIR]…`** (`src/assay/mod.rs`):
+  surveys a target for code that has a formally proven drop-in equivalent
+  in a `proven` / `proven-servers` library and reports each candidate with
+  the proof artifact that backs it — operationalising the "Proven cross-fit"
+  table in `PROOF-PROGRAMME.md` mechanically instead of by hand. Built-in
+  catalogue: `SafePath` (canonicalize/unwrap pattern) and `SafeUrl`
+  (`VERISIMDB_URL`). On this repo: `safe-path` **Offered** (port present in
+  `src/safe_path.rs`, call sites still to rewire), `safe-url`
+  **NoReplacementSource** (not yet ported).
+- **`panic-attack assimilate [TARGET] --candidate ID [--proven DIR] [--from FILE] [--all] [--dry-run]`**:
+  performs a swap — stages the proven module into the tree, backs up the
+  original (`*.orig`), and writes a provenance record (source BLAKE3 hash +
+  proof backing + pending call-site rewires) under `.assimilated/`. Module
+  swaps are automatic; call-site rewiring is reported, never auto-edited
+  (mechanically editing arbitrary call sites is not a reviewable operation).
+- **`panic-attack aggregate --proof PATH… [--label PATH=NAME] [--covers PATH=SPEC] [--report BASE]`**
+  (`src/aggregate/mod.rs`): folds external prover output (Agda / Idris2 /
+  Coq·Rocq / Lean / Isabelle / TSTP / Alethe / DRAT·LRAT) into a report. Each
+  artifact is **BLAKE3-hashed for non-repudiation**, given a friendly name,
+  classified (Closed / Holes / Refuted / Indeterminate — comment-stripped so
+  prose mentioning `postulate` / `Admitted` does not false-trigger), and
+  reconciled against findings (**Backed / Corroborated / Contradicted**).
+  Every verdict is explicitly conditioned on the named checker's trust; the
+  recorded hash lets the tool show exactly which bytes it was handed if the
+  assessment is later challenged. `@name "…"` / `@covers [claim:]kind:value`
+  annotations travel inside the artifact; CLI `--label` / `--covers` override.
+
+Proof foundation re-verified from first principles under a fresh **Idris2
+0.8.0** install: `Types`, `Stripping` (Layer 1.0), `PatternCompleteness`
+(PA1) and `ClassificationSoundness` (PA2) all typecheck. 17 new unit tests;
+full library suite (395 tests) green; zero new compiler warnings.
+
 ## [2.5.5] — 2026-06-02
 
 Release of the v2.5.5 cohort that landed across 11 PRs in panic-attack + wiki + gitbot-fleet on 2026-06-02 PM. Tagged 2026-06-02 PM-evening.