proofs: attestation-chain unforgeability (Idris2) — PROOF-PROGRAMME §3.2

[hyperpolymath]

Context

PROOF-PROGRAMME §3.2. The attestation chain (src/attestation/{intent,evidence,seal,chain,envelope}.rs) binds Intent → Evidence → Seal, where the Seal carries an Ed25519 signature over (Intent, Evidence).

Goal

A new Idris2 module under src/abi/ (sibling to PatternCompleteness.idr / ClassificationSoundness.idr / Stripping.idr) that models the chain with abstract Hash / Sig operations and derives:

1. Integrity — tampering with Intent or Evidence invalidates the Seal.
2. Authenticity — only the holder of the signing key can produce a valid Seal.
3. Non-repudiation — a valid Seal is publicly verifiable.

Constraints

• Must Qed-close. The cryptographic assumption (Ed25519 EUF-CMA) is taken as a hypothesis / interface parameter, not a postulate — panic-attack's own ProofDrift detector (PA021) bans postulate/believe_me/Admitted. So this is a conditional theorem: "given EUF-CMA, unforgeability holds."
• Match the assumption to the ed25519-dalek API the Rust code uses.

Notes

• Estimate per programme: ~200 LoC Idris2, low difficulty (the work is being honest about the assumption).
• Toolchain confirmed working: Idris2 0.8.0 typechecks PA1/PA2/Stripping in-repo.
• Deferred from the 2026-06-04 close-out session (the rest of that session's audit landed in feat: assay / assimilate / aggregate — proof-integration subcommands #121 + chore(close-out): CI hardening + hexad proof + doc accuracy + 6a2 metadata #122).

https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb