Skip to content

Commit 8af3b8c

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 2: prove attestation binding soundness (tamper-evidence) — flagship Idris2 proof (#37)
## Summary Raises a2mliser's Idris2 ABI to **Layer 2** with its first flagship semantic proof. a2mliser's headline is adding cryptographic attestation to markup; this proves **attestation binding soundness**: an attestation verifies a document iff its bound digest equals the document's content digest, so a tampered document (content changed, old attestation reused) has no `Verifies` proof — the tamper-evidence guarantee. Mirrors the estate flagship-proof pattern: `Document`/`Attestation` model, `Verifies` proposition (uninhabited on digest mismatch), sound+complete `Dec`, certifier proven sound, `attestVerifies` + `bindingUnique` theorems, positive + negative controls. ## Changes - Adds `src/interface/abi/A2mliser/ABI/Semantics.idr` — `attest`/`Verifies`, `decVerifies`, `certifyOkSound`/`certifyMismatchRefutes`, `bindingUnique`, and negative control `tamperedNotVerifiable`. - Registers the module in `a2mliser-abi.ipkg`. ## RSR Quality Checklist ### Required - [x] Tests pass — ABI builds clean (see Testing) - [x] Linter clean — zero warnings - [x] No banned language patterns - [x] No banned functions — genuine proof - [x] SPDX headers present - [x] No secrets ### As Applicable - [x] ABI/FFI changes validated — additive proof; FFI untouched ## Testing Verified with **Idris2 0.7.0**: `idris2 --build a2mliser-abi.ipkg` → exit 0, zero warnings. **Adversarial check**: a deliberately-false proof (verifying a tampered document) was rejected. `build/` removed. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- _Generated by [Claude Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent ccdc0d4 commit 8af3b8c

2 files changed

Lines changed: 183 additions & 1 deletion

File tree

‎src/interface/abi/A2mliser/ABI/Semantics.idr‎

Lines changed: 182 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,182 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Flagship semantic proof for a2mliser: attestation binding soundness.
5+
|||
6+
||| Headline domain property (A2ML cryptographic attestation):
7+
||| an attestation tag is bound to the exact content it was issued over.
8+
||| An attestation `Verifies` a document if and only if the digest carried
9+
||| by the attestation equals the digest of the document. Consequently a
10+
||| TAMPERED document (content changed while keeping the old attestation)
11+
||| has NO `Verifiable` proof: the bad case is uninhabited.
12+
|||
13+
||| This is the faithful core of "verify succeeds only for the content it
14+
||| was issued over". We model a content digest as a `Nat` (an abstract
15+
||| collision-free fingerprint of markup bytes); the binding logic is
16+
||| algorithm-agnostic, exactly as in the real engine.
17+
18+
module A2mliser.ABI.Semantics
19+
20+
import A2mliser.ABI.Types
21+
import Data.So
22+
import Decidable.Equality
23+
24+
%default total
25+
26+
--------------------------------------------------------------------------------
27+
-- Faithful domain model
28+
--------------------------------------------------------------------------------
29+
30+
||| A document is some markup content fingerprinted to a digest.
31+
||| `contentDigest` is the abstract fingerprint of the markup bytes; two
32+
||| documents with different content have different digests (collision-free
33+
||| model). The `markup` field is carried for faithfulness but the binding
34+
||| is over the digest, mirroring sign-the-digest cryptography.
35+
public export
36+
record Document where
37+
constructor MkDocument
38+
markup : String
39+
contentDigest : Nat
40+
41+
||| An attestation tag binds to one specific content digest. It is the
42+
||| (abstract) signature whose payload is `boundDigest`.
43+
public export
44+
record Attestation where
45+
constructor MkAttestation
46+
||| The digest the attestation was issued over (what the signature covers).
47+
boundDigest : Nat
48+
||| The signing algorithm (reuses the real ABI type for faithfulness).
49+
algorithm : SignatureAlgorithm
50+
51+
||| Issue an attestation over a document: it binds to that document's digest.
52+
||| This is the ONLY honest way to mint an attestation for a document.
53+
public export
54+
attest : SignatureAlgorithm -> Document -> Attestation
55+
attest alg doc = MkAttestation (contentDigest doc) alg
56+
57+
--------------------------------------------------------------------------------
58+
-- The headline property: attestation binding
59+
--------------------------------------------------------------------------------
60+
61+
||| `Verifies att doc` is inhabited exactly when the attestation's bound
62+
||| digest equals the document's content digest. There is precisely ONE
63+
||| constructor, and it DEMANDS the binding equality as evidence. There is
64+
||| NO constructor for the mismatched (tampered) case — that case is
65+
||| uninhabited by construction.
66+
public export
67+
data Verifies : Attestation -> Document -> Type where
68+
||| The attestation was issued over exactly this content.
69+
Bound : (prf : boundDigest att = contentDigest doc) -> Verifies att doc
70+
71+
||| A document/attestation pair is `Verifiable` iff a `Verifies` proof exists.
72+
public export
73+
Verifiable : Attestation -> Document -> Type
74+
Verifiable = Verifies
75+
76+
--------------------------------------------------------------------------------
77+
-- Sound + complete decision procedure
78+
--------------------------------------------------------------------------------
79+
80+
||| Decide verifiability. Sound: a `Yes` carries a real `Verifies` witness.
81+
||| Complete: a `No` carries a refutation of every possible witness.
82+
public export
83+
decVerifies : (att : Attestation) -> (doc : Document) -> Dec (Verifies att doc)
84+
decVerifies att doc =
85+
case decEq (boundDigest att) (contentDigest doc) of
86+
Yes prf => Yes (Bound prf)
87+
No ctra => No (\(Bound prf) => ctra prf)
88+
89+
--------------------------------------------------------------------------------
90+
-- Certifier + soundness fact
91+
--------------------------------------------------------------------------------
92+
93+
||| Internal: map a raw `Dec` outcome to the ABI's own result code.
94+
||| Kept top-level so it reduces by pattern matching in the proofs below.
95+
public export
96+
certifyVia : Dec (Verifies att doc) -> AttestationResult
97+
certifyVia (Yes _) = Ok
98+
certifyVia (No _) = DigestMismatch
99+
100+
||| Map a verification attempt to the ABI's own result code.
101+
public export
102+
certify : Attestation -> Document -> AttestationResult
103+
certify att doc = certifyVia (decVerifies att doc)
104+
105+
||| Soundness: if the certifier returns `Ok`, a genuine binding proof exists.
106+
||| (Forces `Ok` to mean the attestation truly covers this content.)
107+
public export
108+
certifyOkSound : (att : Attestation) -> (doc : Document)
109+
-> certify att doc = Ok -> Verifies att doc
110+
certifyOkSound att doc okEq with (decVerifies att doc)
111+
certifyOkSound att doc okEq | Yes ok = ok
112+
certifyOkSound att doc Refl | No _ impossible
113+
114+
||| Completeness/contrapositive: a `DigestMismatch` certificate means the
115+
||| pair is genuinely NOT verifiable.
116+
public export
117+
certifyMismatchRefutes : (att : Attestation) -> (doc : Document)
118+
-> certify att doc = DigestMismatch -> Not (Verifies att doc)
119+
certifyMismatchRefutes att doc mmEq with (decVerifies att doc)
120+
certifyMismatchRefutes att doc Refl | Yes _ impossible
121+
certifyMismatchRefutes att doc mmEq | No ctra = ctra
122+
123+
--------------------------------------------------------------------------------
124+
-- Core theorems about attestation binding
125+
--------------------------------------------------------------------------------
126+
127+
||| An honestly-issued attestation always verifies the document it was
128+
||| issued over (the engine never rejects untampered content).
129+
public export
130+
attestVerifies : (alg : SignatureAlgorithm) -> (doc : Document)
131+
-> Verifies (attest alg doc) doc
132+
attestVerifies alg doc = Bound Refl
133+
134+
||| Binding soundness (tamper-evidence): if an attestation verifies BOTH a
135+
||| document and a re-issued document, their content digests are identical.
136+
||| Therefore you cannot make one attestation verify two contents that
137+
||| differ — exactly the "bound to the content it was issued over" guarantee.
138+
public export
139+
bindingUnique : (att : Attestation) -> (d1, d2 : Document)
140+
-> Verifies att d1 -> Verifies att d2
141+
-> contentDigest d1 = contentDigest d2
142+
bindingUnique att d1 d2 (Bound p1) (Bound p2) = trans (sym p1) p2
143+
144+
--------------------------------------------------------------------------------
145+
-- Positive control (inhabited witness)
146+
--------------------------------------------------------------------------------
147+
148+
||| A concrete document and the attestation honestly issued over it.
149+
public export
150+
goodDoc : Document
151+
goodDoc = MkDocument "<a2ml:doc>hello</a2ml:doc>" 1729
152+
153+
public export
154+
goodAtt : Attestation
155+
goodAtt = attest Ed25519 goodDoc
156+
157+
||| POSITIVE CONTROL: the honest attestation verifies the original document.
158+
public export
159+
goodVerifies : Verifies Semantics.goodAtt Semantics.goodDoc
160+
goodVerifies = Bound Refl
161+
162+
--------------------------------------------------------------------------------
163+
-- Negative control (the tampered document is not verifiable)
164+
--------------------------------------------------------------------------------
165+
166+
||| The SAME document content edited (tampered): different digest, but an
167+
||| attacker tries to reuse the old `goodAtt`.
168+
public export
169+
tamperedDoc : Document
170+
tamperedDoc = MkDocument "<a2ml:doc>HELLO (edited)</a2ml:doc>" 9999
171+
172+
||| NEGATIVE CONTROL: the original attestation does NOT verify the tampered
173+
||| document. Machine-checked: any putative `Verifies` proof yields the
174+
||| absurd equality `1729 = 9999`, which reduces to `Refl impossible`.
175+
public export
176+
tamperedNotVerifiable : Not (Verifies Semantics.goodAtt Semantics.tamperedDoc)
177+
tamperedNotVerifiable (Bound prf) = absurdEq prf
178+
where
179+
||| `prf` definitionally has type `1729 = 9999`; name the concrete,
180+
||| constructor-headed equality so its refutation reduces.
181+
absurdEq : (the Nat 1729 = the Nat 9999) -> Void
182+
absurdEq Refl impossible

‎src/interface/abi/a2mliser-abi.ipkg‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
-- SPDX-License-Identifier: MPL-2.0
22
package a2mliser-abi
33
sourcedir = "."
4-
modules = A2mliser.ABI.Types, A2mliser.ABI.Layout, A2mliser.ABI.Foreign, A2mliser.ABI.Proofs
4+
modules = A2mliser.ABI.Types, A2mliser.ABI.Layout, A2mliser.ABI.Foreign, A2mliser.ABI.Proofs, A2mliser.ABI.Semantics

0 commit comments

Comments
 (0)