proofs: attestation unforgeability (Idris2, §3.2) + contractile INDEX registry

.machine_readable/contractiles/INDEX.a2ml

@@ -0,0 +1,93 @@
+# SPDX-License-Identifier: MPL-2.0
+# INDEX.a2ml — Contractile Registry (panic-attack)
+# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Machine-readable catalogue of the contractile verbs present in this repo.
+# Consumers (CI scripts, the contractile CLI, Hypatia rules) SHOULD read this
+# file to discover the available verbs and their on-disk locations rather than
+# hard-coding the list.
+#
+# Canonical shape: hyperpolymath/standards docs/CONTRACTILE-SPEC.adoc §Registry,
+# exemplified by hyperpolymath/echidna .machine_readable/contractiles/ (v2.0.0,
+# full trident shape for all six verbs).
+#
+# STATUS: panic-attack's contractile set predates the trident consolidation and
+# is currently SCATTERED across three trees (see [layout]). This registry
+# catalogues what exists and its real location; the physical consolidation to
+# the canonical .machine_readable/contractiles/<verb>/ trident shape is tracked
+# in issue #124 — it is held because the root `contractiles/` tree is read by
+# `contractile gen-just` to emit contractile.just, so a blind move would break
+# the generator, and the authoritative CONTRACTILE-SPEC lives in the (here
+# unreachable) standards repo.
+
+---
+id = "contractiles-registry"
+project = "panic-attack"
+version = "0.1.0"   # 0.1.0: registry introduced over the existing pre-consolidation layout.
+spec = "hyperpolymath/standards docs/CONTRACTILE-SPEC.adoc"
+canonical_reference = "hyperpolymath/echidna .machine_readable/contractiles/INDEX.a2ml (v2.0.0)"
+base_schema = ".machine_readable/contractiles/_base.ncl (NOT YET PRESENT — see #124; reference: echidna _base.ncl)"
+last_updated = "2026-06-04"
+consolidation_tracking = "https://github.com/hyperpolymath/panic-attack/issues/124"
+
+## Layout — current reality (three trees, pending consolidation in #124)
+
+[layout]
+flat = ".machine_readable/*.contractile  — ADJUST, INTENT, MUST, TRUST (legacy flat form)"
+machine_readable_tridents = ".machine_readable/contractiles/<verb>/  — adjust, bust, dust, trust (partial: Xfile.a2ml + x.ncl)"
+generator_source = "contractiles/<verb>/  — intend, must, trust (read by `contractile gen-just` → contractile.just)"
+canonical_target = ".machine_readable/contractiles/<verb>/  — full trident: Xfile.a2ml + x.ncl + x.k9.ncl + manifest"
+
+## Verbs
+# Canonical verb set per the standard: adjust, bust, dust, intend, must, trust
+# (six, on the trident shape), plus the k9 trust-tier template exception.
+# panic-attack has all six present in at least one tree; none yet on the full
+# trident. `present` lists the actual on-disk files today.
+
+[[verbs]]
+name = "must"
+semantics = "invariant assertion — release-blocking"
+authority = "blocking"
+gating = "hard (exit-nonzero)"
+present = ["contractiles/must/Mustfile.a2ml", ".machine_readable/MUST.contractile"]
+trident_status = "file-only — missing must.ncl + must.k9.ncl + must.manifest.a2ml"
+
+[[verbs]]
+name = "trust"
+semantics = "security + provenance + safe-hacking"
+authority = "blocking"
+gating = "hard (exit-nonzero)"
+present = ["contractiles/trust/Trustfile.a2ml", ".machine_readable/contractiles/trust/Trustfile.a2ml", ".machine_readable/TRUST.contractile"]
+trident_status = "DUPLICATE — root and .machine_readable Trustfile.a2ml differ; reconcile in #124"
+
+[[verbs]]
+name = "intend"
+semantics = "north-star (commitments + aspirations)"
+authority = "reporting"
+gating = "non-gating (continue)"
+present = ["contractiles/intend/Intentfile.a2ml", ".machine_readable/INTENT.contractile"]
+trident_status = "file-only — missing intend.ncl + intend.k9.ncl + intend.manifest.a2ml"
+
+[[verbs]]
+name = "adjust"
+semantics = "drift tolerances + corrective actions"
+authority = "advisory"
+gating = "advisory (continue-with-warnings)"
+present = [".machine_readable/contractiles/adjust/Adjustfile.a2ml", ".machine_readable/contractiles/adjust/adjust.ncl", ".machine_readable/ADJUST.contractile"]
+trident_status = "pair — missing adjust.k9.ncl + adjust.manifest.a2ml"
+
+[[verbs]]
+name = "bust"
+semantics = "hard-stop / expiry / must-not-run declarations"
+authority = "blocking"
+gating = "hard (exit-nonzero)"
+present = [".machine_readable/contractiles/bust/Bustfile.a2ml", ".machine_readable/contractiles/bust/bust.ncl"]
+trident_status = "pair — missing bust.k9.ncl + bust.manifest.a2ml"
+
+[[verbs]]
+name = "dust"
+semantics = "rollback / recovery / deprecation / audit-trail preservation"
+authority = "advisory"
+gating = "advisory (continue-with-warnings)"
+present = [".machine_readable/contractiles/dust/Dustfile.a2ml"]
+trident_status = "file-only — missing dust.ncl + dust.k9.ncl + dust.manifest.a2ml"

CHANGELOG.md

@@ -2,6 +2,31 @@
 
 ## [Unreleased]
 
+### Added — attestation unforgeability proof (Idris2, PROOF-PROGRAMME §3.2)
+
+- **`src/abi/AttestationUnforgeability.idr`**: Idris2 proof that the
+  intent→evidence→seal attestation chain is unforgeable. Models
+  `chain_hash = H(intent‖evidence‖report)` + the Ed25519 signature with the
+  cryptographic facts (chain-hash collision-resistance, Ed25519 EUF-CMA
+  message- and signer-binding, signature correctness) as a `parameters`
+  block — hypotheses, **not** `postulate` (PA021 bans escape hatches), so it
+  is an honest *conditional* theorem. Under `%default total` it Qed-closes
+  `integrity` (tampering any phase invalidates the seal), `authenticity`
+  (a verifying seal comes from the matching key), and `nonRepudiation`
+  (a genuine seal verifies), plus two corollaries. Typechecks under Idris2
+  0.8.0. Closes #123.
+
+### Added — contractile registry (INDEX.a2ml)
+
+- **`.machine_readable/contractiles/INDEX.a2ml`**: the previously-missing
+  contractile registry, modelled on echidna's canonical INDEX. Catalogues all
+  six verbs (must / trust / intend / adjust / bust / dust) with their *actual
+  current locations* across the three pre-consolidation trees, flags the
+  duplicate `trust` Trustfile, and records the canonical trident target. The
+  physical consolidation of the three trees stays in #124 — it couples to the
+  `contractile gen-just` generator (which reads the root `contractiles/` tree)
+  and needs the standards CONTRACTILE-SPEC to do safely.
+
 ### Added — `assay` / `assimilate` / `aggregate` proof-integration subcommands
 
 Three new a-themed subcommands that wire panic-attack into the

PROOF-NEEDS.md

@@ -2,7 +2,7 @@
 
 ## Current State
 
-- **src/abi/*.idr**: 4 files — `Types.idr`, `PatternCompleteness.idr` (PA1 ✅ 2026-04-11), `ClassificationSoundness.idr` (PA2 ✅ 2026-04-11), `Stripping.idr` (PROOF-PROGRAMME Layer 1.0 line-comment slice ✅ 2026-06-02 — multi-comment semantics + slash-slash closure both Qed via mutual-recursive `bodyIsFixedPoint`)
+- **src/abi/*.idr**: 5 files — `Types.idr`, `PatternCompleteness.idr` (PA1 ✅ 2026-04-11), `ClassificationSoundness.idr` (PA2 ✅ 2026-04-11), `Stripping.idr` (PROOF-PROGRAMME Layer 1.0 line-comment slice ✅ 2026-06-02 — multi-comment semantics + slash-slash closure both Qed via mutual-recursive `bodyIsFixedPoint`), `AttestationUnforgeability.idr` (PROOF-PROGRAMME §3.2 ✅ 2026-06-04 — conditional unforgeability from Ed25519 EUF-CMA + chain-hash collision-resistance hypotheses)
 - **Dangerous patterns**: 0 in own code (3 references are in the analyzer that DETECTS believe_me in other repos); 282 `unwrap()` calls
 - **LOC**: ~31,700 (Rust)
 - **ABI layer**: Idris2 with completeness + soundness proofs + Layer-1.0 stripping foundation
@@ -14,14 +14,15 @@
 | PA1 Pattern detection completeness | `src/abi/PatternCompleteness.idr` | All 49 `Lang` constructors have an analyzer; all 20 `WPCategory` constructors have at least one detector; cross-language checks applied unconditionally to all languages. `completeScanForAll` is the top-level theorem. |
 | PA2 Classification soundness | `src/abi/ClassificationSoundness.idr` | Severity (Low/Medium/High/Critical) is totally ordered (`LTE`); `maxSeverity` is commutative and idempotent; numeric ABI encoding preserves the ordering. |
 | Layer 1.0 line-comment idempotence | `src/abi/Stripping.idr` | **2026-06-02 close-out (issue #113)**: corrects PR #111's single-comment model to multi-comment via mutual recursion (`stripLineComments ↔ stripLineCommentBody` — body calls back into main after each preserved newline). Qed-closes `stripLineCommentsIdempotent` for ALL cases including the slash-slash inductive via the load-bearing `bodyIsFixedPoint` lemma proved by mutual induction with the main theorem. 7 sanity-check theorems including the two-comments-on-different-lines case PR #111 silently mis-stripped. |
+| Attestation chain unforgeability | `src/abi/AttestationUnforgeability.idr` | **PROOF-PROGRAMME §3.2 (2026-06-04, issue #123)**: models the intent→evidence→seal chain (`chain_hash = H(intent‖evidence‖report)`, Ed25519-signed) with the cryptographic facts as a `parameters` block (hypotheses, **not** `postulate`). Under `%default total` Qed-closes `integrity` (tampering any phase invalidates the seal), `authenticity` (a verifying seal comes from the matching secret key), `nonRepudiation` (a genuine seal verifies), plus 2 corollaries. Conditional on chain-hash collision-resistance + Ed25519 EUF-CMA (message- and signer-binding) + signature correctness. |
+| Hexad↔Octad persistence round-trip | `src/storage/mod.rs` (proptest) | **PROOF-PROGRAMME §3.1 (2026-06-04, #122)**: `hexad_json_roundtrip_is_identity` proves the on-disk serde round-trip (`write_*_hexad` → `load_hexad_dir`) is the identity on the hexad JSON. The gateway octad projection is lossy by design, so the faithful integrity property is the persistence round-trip, not the literal hexad↔octad map. |
 
 ## What Still Needs Proving
 
 | Component | What | Why |
 |-----------|------|-----|
 | **Layer 1.0 — stripBlockComments + Strings + Composition + Position-Preservation** (issue #114) | Block-comment (`/* */`) and string-literal (`"..."`) strippers with same mutual-recursive shape; composition theorem proving the full pipeline is idempotent given each component is; position-preservation theorem justifying analyzer location-reporting against the stripped view as if it were original-source. | Four slices: `Stripping_Block.idr`, `Stripping_Strings.idr`, `Stripping_Composition.idr`, `Stripping_PositionPreservation.idr`. |
 | Bridge reachability soundness | Reachability analysis is sound (no reachable dep wrongly classified as phantom) | Unreachable code marked reachable wastes effort; reachable missed = security gap |
-| Attestation chain unforgeability | Intent/evidence/seal triple is cryptographically bound; tampering detectable | Tampered attestations break trust chain |
 | Kanren taint analysis | Taint propagation tracks all tainted data flows | Missed taint flow means missed vulnerability |
 
 ## Recommended Prover

src/abi/AttestationUnforgeability.idr

@@ -0,0 +1,128 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+||| Attestation-chain unforgeability (PROOF-PROGRAMME §3.2).
+|||
+||| Mirrors `src/attestation/{intent,evidence,seal}.rs`. The seal binds the
+||| three attestation phases via
+|||
+|||     chain_hash = H(intent_hash || evidence_hash || report_hash)
+|||
+||| and optionally signs that chain hash with Ed25519.
+|||
+||| The cryptographic facts the seal relies on are taken as explicit
+||| HYPOTHESES — a `parameters` block, NOT `postulate` (panic-attack's own
+||| ProofDrift detector, PA021, bans `postulate` / `believe_me` / `Admitted`).
+||| This therefore proves a *conditional* theorem: GIVEN the standard
+||| cryptographic assumptions, the chain is unforgeable. The assumptions are:
+|||
+|||   * `chainCR`         — collision resistance of the chain hash, in the
+|||                         idealised injective form (distinct phase triples
+|||                         hash apart). Matches the SHA-256 `chain_hash`.
+|||   * `sigCorrect`      — a genuine Ed25519 signature verifies.
+|||   * `sigBindsMessage` — EUF-CMA (message-binding facet): a signature made
+|||                         over `d` only verifies against `d`.
+|||   * `sigOnlySigner`   — EUF-CMA (signer-binding facet): a verifying
+|||                         signature comes from the matching secret key.
+|||
+||| From these — with no further assumptions, every lemma `Qed`-closes — we
+||| derive the three properties of PROOF-PROGRAMME §3.2:
+|||
+|||   1. `integrity`      — tampering with any phase invalidates the seal.
+|||   2. `authenticity`   — a verifying seal comes from the matching key.
+|||   3. `nonRepudiation` — a genuine seal is publicly verifiable.
+module PanicAttack.ABI.AttestationUnforgeability
+
+%default total
+
+-- ═══════════════════════════════════════════════════════════════════════
+-- Abstract chain + signature model, with the cryptographic assumptions as
+-- module parameters (hypotheses, not postulates).
+-- ═══════════════════════════════════════════════════════════════════════
+
+parameters
+  (Bytes, Digest, SecretKey, PublicKey, Sig : Type)
+  (chainHash : Bytes -> Bytes -> Bytes -> Digest)
+  (pubKey    : SecretKey -> PublicKey)
+  (sign      : SecretKey -> Digest -> Sig)
+  (verify    : PublicKey -> Digest -> Sig -> Bool)
+  (chainCR         : (i, e, r, i', e', r' : Bytes) ->
+                     chainHash i e r = chainHash i' e' r' ->
+                     ((i, e, r) = (i', e', r')))
+  (sigCorrect      : (sk : SecretKey) -> (d : Digest) ->
+                     verify (pubKey sk) d (sign sk d) = True)
+  (sigBindsMessage : (sk : SecretKey) -> (d, d' : Digest) ->
+                     verify (pubKey sk) d' (sign sk d) = True -> d = d')
+  (sigOnlySigner   : (pk : PublicKey) -> (d : Digest) -> (s : Sig) ->
+                     verify pk d s = True ->
+                     (sk : SecretKey ** (pk = pubKey sk, s = sign sk d)))
+
+  ||| The seal over the three phases: sign the chain hash.
+  seal : SecretKey -> Bytes -> Bytes -> Bytes -> Sig
+  seal sk i e r = sign sk (chainHash i e r)
+
+  ||| Public validity check (anyone with the public key can run it).
+  valid : PublicKey -> Bytes -> Bytes -> Bytes -> Sig -> Bool
+  valid pk i e r s = verify pk (chainHash i e r) s
+
+  -- ─────────────────────────────────────────────────────────────────────
+  -- 1. INTEGRITY: tampering with any phase invalidates the seal.
+  -- ─────────────────────────────────────────────────────────────────────
+
+  ||| If the phase triple is tampered (differs from the sealed one), a seal
+  ||| produced over the original phases fails to verify against the tampered
+  ||| ones. Proof: were it to verify, message-binding would force the chain
+  ||| hashes equal and collision-resistance the triples equal — contradiction.
+  integrity : (sk : SecretKey) ->
+              (i, e, r, i', e', r' : Bytes) ->
+              Not ((i, e, r) = (i', e', r')) ->
+              verify (pubKey sk) (chainHash i' e' r') (sign sk (chainHash i e r)) = False
+  integrity sk i e r i' e' r' neq
+      with (verify (pubKey sk) (chainHash i' e' r') (sign sk (chainHash i e r))) proof prf
+    integrity sk i e r i' e' r' neq | True =
+      absurd (neq (chainCR i e r i' e' r'
+                     (sigBindsMessage sk (chainHash i e r) (chainHash i' e' r') prf)))
+    integrity sk i e r i' e' r' neq | False = Refl
+
+  -- ─────────────────────────────────────────────────────────────────────
+  -- 2. AUTHENTICITY: a verifying seal comes from the matching secret key.
+  -- ─────────────────────────────────────────────────────────────────────
+
+  ||| A seal that verifies under `pk` must have been produced by the holder
+  ||| of the secret key whose public key is `pk`, signing exactly this
+  ||| chain hash. Direct from the signer-binding facet of EUF-CMA.
+  authenticity : (pk : PublicKey) -> (i, e, r : Bytes) -> (s : Sig) ->
+                 verify pk (chainHash i e r) s = True ->
+                 (sk : SecretKey ** (pk = pubKey sk, s = sign sk (chainHash i e r)))
+  authenticity pk i e r s ok = sigOnlySigner pk (chainHash i e r) s ok
+
+  -- ─────────────────────────────────────────────────────────────────────
+  -- 3. NON-REPUDIATION: a genuine seal is publicly verifiable.
+  -- ─────────────────────────────────────────────────────────────────────
+
+  ||| A seal produced by `sk` over `(i, e, r)` always verifies under the
+  ||| corresponding public key, so the signer cannot deny a seal that checks
+  ||| out — verification is a deterministic public function. (= correctness.)
+  nonRepudiation : (sk : SecretKey) -> (i, e, r : Bytes) ->
+                   verify (pubKey sk) (chainHash i e r) (sign sk (chainHash i e r)) = True
+  nonRepudiation sk i e r = sigCorrect sk (chainHash i e r)
+
+  -- ─────────────────────────────────────────────────────────────────────
+  -- Corollaries (sanity).
+  -- ─────────────────────────────────────────────────────────────────────
+
+  ||| The seal/valid wrappers agree with the underlying signature ops: a
+  ||| freshly produced seal is `valid`. Ties the readable API to property 3.
+  sealValid : (sk : SecretKey) -> (i, e, r : Bytes) ->
+              valid (pubKey sk) i e r (seal sk i e r) = True
+  sealValid sk i e r = sigCorrect sk (chainHash i e r)
+
+  ||| Two phase triples that share a verifying seal under one key are equal
+  ||| (no two distinct attestations collide under the same seal).
+  sealNoCollision : (sk : SecretKey) -> (i, e, r, i', e', r' : Bytes) ->
+                    verify (pubKey sk) (chainHash i e r) (sign sk (chainHash i e r)) = True ->
+                    verify (pubKey sk) (chainHash i' e' r') (sign sk (chainHash i e r)) = True ->
+                    ((i, e, r) = (i', e', r'))
+  sealNoCollision sk i e r i' e' r' _ tampered =
+    chainCR i e r i' e' r'
+      (sigBindsMessage sk (chainHash i e r) (chainHash i' e' r') tampered)