diff --git a/.machine_readable/contractiles/INDEX.a2ml b/.machine_readable/contractiles/INDEX.a2ml new file mode 100644 index 0000000..566da31 --- /dev/null +++ b/.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 +# +# 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// 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// — adjust, bust, dust, trust (partial: Xfile.a2ml + x.ncl)" +generator_source = "contractiles// — intend, must, trust (read by `contractile gen-just` → contractile.just)" +canonical_target = ".machine_readable/contractiles// — 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" diff --git a/CHANGELOG.md b/CHANGELOG.md index 0122a26..650c931 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 180fbf4..77db365 100644 --- a/PROOF-NEEDS.md +++ b/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,6 +14,8 @@ | 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 @@ -21,7 +23,6 @@ |-----------|------|-----| | **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 diff --git a/src/abi/AttestationUnforgeability.idr b/src/abi/AttestationUnforgeability.idr new file mode 100644 index 0000000..dab3999 --- /dev/null +++ b/src/abi/AttestationUnforgeability.idr @@ -0,0 +1,128 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +||| 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)