docs: record user-classification registry + Rocq scaffold classifier

CHANGELOG.md: Unreleased section captures the two 2026-04-18 features
(classification registry + Rocq scaffold classifier), the pipeline
change, test coverage, and the 007-end verified drop from 8 active
findings to 0.

.claude/CLAUDE.md: ProofDrift bullet updated with the Rocq-specific
refinement (Section-awareness + module-level `Parameter` classifier);
new "User-Classification Registry" section documents the file format,
lookup paths, public API, pattern intent, and cites 007 as the
reference implementation.

No code changes — purely authoritative documentation for the
315917b + 6d6822a features shipped this week.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.claude/CLAUDE.md

@@ -178,12 +178,44 @@ Three self-contained modes — none requires the others:
 ## v2.5.0 Detection Categories (COMPLETE — 25 categories total)
 
 All five detection categories shipped in v2.5.0 (2026-04-12):
-- **ProofDrift (PA021)**: Proof escape hatches in Isabelle/Coq/Lean/Agda/Idris2; Julia mirror patterns; Obj.magic in Coq-extracted OCaml (distinguished from hand-written via `type __ = Obj.t` marker)
+- **ProofDrift (PA021)**: Proof escape hatches in Isabelle/Coq/Lean/Agda/Idris2; Julia mirror patterns; Obj.magic in Coq-extracted OCaml (distinguished from hand-written via `type __ = Obj.t` marker). Rocq-specific refinement (2026-04-18): the detector is Section-aware (`Variable`/`Hypothesis`/`Parameter` inside a `Section ... End` are discharged, not counted) and classifies module-level `Parameter` declarations by stated type (carrier types, decidability witnesses, non-Prop function symbols are abstractions; Prop-valued remains counted). See `count_rocq_unverified_postulates` in `src/assail/analyzer.rs`.
 - **CryptoMisuse (PA022)**: Weak hash (MD5/SHA-1) in security context; timing-unsafe == on secrets; JWT sig bypass — `dangerous_insecure_decode` (Rust), `ParseUnverified` (Go), `verify_signature:False`/`algorithms=["none"]` (Python), `jwt.decode` without `jwt.verify` / `decodeJwt` without `jwtVerify` (JS)
 - **SupplyChain (PA023)**: Unpinned deps, absent lock files, unverified manifests
 - **InputBoundary (PA024)**: Unchecked CBOR/MessagePack (Rust), JSON.parse without try-catch (JS/Julia)
 - **MutationGap (PA025)**: No cargo-mutants config (Rust), all-type-only assertions (Julia), no property testing (Elixir)
 
+## User-Classification Registry (2026-04-18)
+
+Optional project-local classification file that flips audited findings
+to `suppressed = true` after the kanren structural-suppression pass:
+
+- Path: `<project>/audits/assail-classifications.a2ml` (preferred) or
+  `<project>/.panic-attack-classifications.a2ml` (fallback).
+- Format (A2ML S-expression):
+  ```
+  (assail-classifications
+    (classification
+      (file "crates/foo/src/bar.rs")
+      (category "UnsafeCode")
+      (audit "audits/audit-ffi-unsafe.md §1")
+      (rationale "one-line summary")))
+  ```
+- Public API: `UserClassification`, `load_user_classifications(root)`,
+  `apply_user_classifications(&mut report, root)` in `src/assail/mod.rs`.
+- Called automatically by `analyze()` / `analyze_verbose()` after
+  `apply_suppression`.
+
+**Pattern intent**: the registry lives in a separate file from the
+source under scan, so adding a new unsafe block cannot self-suppress —
+the registry edit is a reviewable companion change. This keeps
+suppressions non-gameable by single-side edits while still letting
+repositories record honest audits of legitimate-FFI and other
+genuinely-sound residuals.
+
+**Reference implementation**: `hyperpolymath/007`
+`audits/assail-classifications.a2ml` (cross-references
+`audits/audit-ffi-unsafe.md §1` for `zig_bridge.rs` UnsafeCode).
+
 ## Integration Points
 
 - **panicbot**: gitbot-fleet verifier bot — invokes `panic-attack assail --output-format json`, translates WeakPoints to Findings (PA001-PA025). Directives at `.machine_readable/bot_directives/panicbot.scm`

CHANGELOG.md

@@ -1,5 +1,55 @@
 # Changelog
 
+## [Unreleased] — 2026-04-18
+
+### Added
+- **User-classification registry** (`assail::UserClassification`,
+  `load_user_classifications`, `apply_user_classifications`): panic-attack
+  now reads an optional project-local classification file at every assail
+  pass and flips matching findings to `suppressed = true` after the kanren
+  structural-suppression pass. Two lookup paths:
+  - `<project_root>/audits/assail-classifications.a2ml` (preferred)
+  - `<project_root>/.panic-attack-classifications.a2ml` (fallback)
+  File format is a simple A2ML S-expression with `(classification (file …)
+  (category …) (audit …) (rationale …))` blocks; `;;` line comments
+  ignored. The registry pattern lets repositories record audited findings
+  out-of-band from the source under scan so a PR adding a new unsafe
+  block cannot self-suppress without a reviewable companion edit to
+  the registry.
+- **Rocq scaffold classifier** (`analyze_coq` +
+  `count_rocq_unverified_postulates` + `is_rocq_abstraction_parameter`):
+  the Rocq detector no longer counts Section-scoped `Variable` /
+  `Hypothesis` / `Parameter` declarations (they discharge at `End
+  Section`) and classifies module-level `Parameter` declarations by
+  stated type: carrier types (`Type`, `Set`), decidability witnesses
+  (`forall _, { _ = _ } + { _ <> _ }`), and function types with a
+  concrete non-Prop codomain are treated as abstraction parameters.
+  Prop-valued declarations (classical excluded-middle, choice,
+  unresolved theorem statements) remain counted. Removes the
+  false-positive stream that surfaced on every canonical-proof-suite
+  scaffold.
+
+### Changed
+- **Suppression pipeline**: `analyze()` and `analyze_verbose()` now
+  chain `apply_suppression` → `apply_user_classifications` in that
+  order; the explicit post-analyze calls in `assail::analyze` and
+  `assail::analyze_verbose` at the module boundary are retained for
+  API-contract clarity but are no-ops when an `Analyzer` pass has
+  already run.
+- **Rocq test coverage**: 12 new unit tests across `analyzer.rs`
+  (Section-scoped Variables / module-level Type carriers / decidable
+  equality / concrete-codomain functions / Prop-valued axioms /
+  missing type annotation / full scaffold shape — 7 tests) and
+  `mod.rs` (missing-registry / single-entry / multiple-entry /
+  comment handling / end-to-end suppression-flip — 5 tests).
+
+### Verified
+- 007 canonical-proof-suite scan: active finding count **8 → 0**
+  (the 6 scaffold ProofDrifts via the detector enhancement, the 2
+  `zig_bridge.rs` UnsafeCode findings via the classification registry
+  pointing at `audits/audit-ffi-unsafe.md §1`). No in-source
+  suppression markers added to either repo.
+
 ## [2.5.0] - 2026-04-12
 
 ### Added