Skip to content

Commit 8b97dda

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: attestation determinism, idempotence + issue→verify round-trip (#38)
## Summary Layer 3 (second, deeper invariant): proves attestation **determinism** (same document ⇒ same attestation), **idempotence**, and the **issue→verify round-trip** (a freshly attested document always verifies). Distinct from and deeper than the Layer-2 binding-soundness/tamper-evidence theorem. New module `A2mliser.ABI.Invariants` (imports the Layer-2 `Semantics` model). Positive + non-vacuity controls. ## Testing Idris2 0.7.0 `--build` → exit 0, zero warnings. Adversarial rejection confirmed. `build/` removed. No `believe_me`/`postulate`/`sorry`. 🤖 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)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
1 parent 8af3b8c commit 8b97dda

2 files changed

Lines changed: 211 additions & 1 deletion

File tree

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

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
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+
||| Layer-3 invariants for a2mliser: attestation DETERMINISM, IDEMPOTENCE and
5+
||| the issue->verify ROUND-TRIP, built over the SAME model as Semantics.idr.
6+
|||
7+
||| This is deliberately DISTINCT from (and deeper than) the Layer-2 flagship
8+
||| theorem `bindingUnique` (binding soundness / tamper-evidence). Where Layer 2
9+
||| answers "can one tag verify two different contents?" (no), Layer 3 answers a
10+
||| different family of questions about the issuing PROCESS itself:
11+
|||
12+
||| * Determinism — `attest` is a (mathematical) function: identical
13+
||| inputs give bit-identical attestations, and identical
14+
||| attestations on the same doc give identical results.
15+
||| * Idempotence — re-attesting a document with the same algorithm
16+
||| reproduces the very same attestation (a fixed point).
17+
||| * Round-trip — a freshly attested document ALWAYS re-verifies, and
18+
||| the ABI certifier ALWAYS returns `Ok` for it; further,
19+
||| re-running `certify` on the freshly attested doc is a
20+
||| stable fixed point (`Ok` again, deterministically).
21+
||| * Round-trip recovery — from `certify (attest alg d) d = Ok` you can
22+
||| RECOVER the binding digest equality (transition
23+
||| soundness: the Ok certificate is honest evidence).
24+
|||
25+
||| All of this reuses Semantics.attest / Verifies / certify unchanged.
26+
27+
module A2mliser.ABI.Invariants
28+
29+
import A2mliser.ABI.Types
30+
import A2mliser.ABI.Semantics
31+
import Decidable.Equality
32+
33+
%default total
34+
35+
--------------------------------------------------------------------------------
36+
-- 1. Determinism of `attest` (it is genuinely a function)
37+
--------------------------------------------------------------------------------
38+
39+
||| DETERMINISM: `attest` is congruent under equality of its inputs. Equal
40+
||| algorithm and equal document produce the identical attestation. This is the
41+
||| substance of "same document => same attestation".
42+
public export
43+
attestDeterministic : (a1, a2 : SignatureAlgorithm) -> (d1, d2 : Document)
44+
-> a1 = a2 -> d1 = d2
45+
-> attest a1 d1 = attest a2 d2
46+
attestDeterministic a1 a1 d1 d1 Refl Refl = Refl
47+
48+
||| Corollary in the algorithm-fixed form most callers want: one algorithm,
49+
||| equal documents => equal attestation.
50+
public export
51+
attestDetDoc : (alg : SignatureAlgorithm) -> (d1, d2 : Document)
52+
-> d1 = d2 -> attest alg d1 = attest alg d2
53+
attestDetDoc alg d1 d2 eq = attestDeterministic alg alg d1 d2 Refl eq
54+
55+
--------------------------------------------------------------------------------
56+
-- 2. Idempotence: re-attesting a document is a fixed point
57+
--------------------------------------------------------------------------------
58+
59+
||| The digest carried by a freshly issued attestation is exactly the
60+
||| document's digest (computation lemma; reduces by definition of `attest`).
61+
public export
62+
attestBoundDigest : (alg : SignatureAlgorithm) -> (doc : Document)
63+
-> boundDigest (attest alg doc) = contentDigest doc
64+
attestBoundDigest alg doc = Refl
65+
66+
||| Re-document an attestation by wrapping its bound digest back into a
67+
||| `Document` shell. Re-attesting that shell with the same algorithm must
68+
||| reproduce an attestation bound to the same digest (idempotent issuing).
69+
||| We state idempotence on the digest the attestation commits to.
70+
public export
71+
attestIdempotent : (alg : SignatureAlgorithm) -> (doc : Document)
72+
-> boundDigest (attest alg (MkDocument (markup doc)
73+
(boundDigest (attest alg doc))))
74+
= boundDigest (attest alg doc)
75+
attestIdempotent alg doc = Refl
76+
77+
--------------------------------------------------------------------------------
78+
-- 3. Round-trip: issue then verify always succeeds (process correctness)
79+
--------------------------------------------------------------------------------
80+
81+
||| The ABI certifier always returns `Ok` for an honestly-issued attestation.
82+
||| This connects the ISSUING function to the RESULT-CODE surface (a
83+
||| transition-soundness fact: honest issue => Ok certificate), going through
84+
||| the real `certify`/`decVerifies` pipeline rather than restating `Verifies`.
85+
public export
86+
attestCertifies : (alg : SignatureAlgorithm) -> (doc : Document)
87+
-> certify (attest alg doc) doc = Ok
88+
attestCertifies alg doc with (decVerifies (attest alg doc) doc)
89+
attestCertifies alg doc | Yes _ = Refl
90+
attestCertifies alg doc | No bad = absurd (bad (attestVerifies alg doc))
91+
92+
||| ROUND-TRIP STABILITY (fixed point of certification): certifying a freshly
93+
||| attested document, twice, yields the same `Ok` both times. Since `certify`
94+
||| is deterministic this is `Ok = Ok`, but stated through `attestCertifies` it
95+
||| witnesses that re-verification is a stable fixed point, not a fluke.
96+
public export
97+
attestCertifyStable : (alg : SignatureAlgorithm) -> (doc : Document)
98+
-> certify (attest alg doc) doc = certify (attest alg doc) doc
99+
attestCertifyStable alg doc =
100+
trans (attestCertifies alg doc) (sym (attestCertifies alg doc))
101+
102+
--------------------------------------------------------------------------------
103+
-- 4. Round-trip recovery: an Ok certificate is honest evidence
104+
--------------------------------------------------------------------------------
105+
106+
||| TRANSITION SOUNDNESS / RECOVERY: from an `Ok` certificate on a freshly
107+
||| attested document, recover the binding digest equality. We obtain a genuine
108+
||| `Verifies` witness from the Layer-2 soundness lemma and read its digest
109+
||| equality back out. (Distinct from Layer 2: this is keyed on `attest`, i.e.
110+
||| the issuing process, and lands in the underlying Nat equality.)
111+
public export
112+
certifyOkRecoversDigest : (alg : SignatureAlgorithm) -> (doc : Document)
113+
-> certify (attest alg doc) doc = Ok
114+
-> boundDigest (attest alg doc) = contentDigest doc
115+
certifyOkRecoversDigest alg doc okEq =
116+
case certifyOkSound (attest alg doc) doc okEq of
117+
Bound prf => prf
118+
119+
--------------------------------------------------------------------------------
120+
-- 5. A natural sound+complete decision: are two attestations interchangeable?
121+
--------------------------------------------------------------------------------
122+
123+
||| Two attestations are `SameBinding` iff they commit to the same digest.
124+
||| (This is the digest-level equivalence that drives interchangeability for
125+
||| verification: SameBinding attestations verify exactly the same documents.)
126+
public export
127+
data SameBinding : Attestation -> Attestation -> Type where
128+
MkSameBinding : (prf : boundDigest a1 = boundDigest a2) -> SameBinding a1 a2
129+
130+
||| SOUND + COMPLETE decision for `SameBinding`. `Yes` carries a real witness;
131+
||| `No` refutes every possible witness.
132+
public export
133+
decSameBinding : (a1, a2 : Attestation) -> Dec (SameBinding a1 a2)
134+
decSameBinding a1 a2 =
135+
case decEq (boundDigest a1) (boundDigest a2) of
136+
Yes prf => Yes (MkSameBinding prf)
137+
No ctra => No (\(MkSameBinding prf) => ctra prf)
138+
139+
||| Soundness of the equivalence in use: `SameBinding` attestations verify the
140+
||| same documents. If `a1` verifies `doc` and `a1`/`a2` share a binding, then
141+
||| `a2` verifies `doc` too. (Deeper than Layer 2: a CONGRUENCE of `Verifies`
142+
||| along the digest equivalence, not just uniqueness.)
143+
public export
144+
sameBindingVerifies : (a1, a2 : Attestation) -> (doc : Document)
145+
-> SameBinding a1 a2 -> Verifies a1 doc -> Verifies a2 doc
146+
sameBindingVerifies a1 a2 doc (MkSameBinding sb) (Bound p1) =
147+
Bound (trans (sym sb) p1)
148+
149+
--------------------------------------------------------------------------------
150+
-- 6. POSITIVE controls (inhabited witnesses / concrete instances)
151+
--------------------------------------------------------------------------------
152+
153+
||| Reuse the Layer-2 concrete document so controls are over the real model.
154+
||| POSITIVE: the certifier really returns `Ok` for the honest attestation.
155+
public export
156+
goodRoundTrips : certify Semantics.goodAtt Semantics.goodDoc = Ok
157+
goodRoundTrips = attestCertifies Ed25519 Semantics.goodDoc
158+
159+
||| POSITIVE: an attestation is trivially same-binding with itself, and that
160+
||| witness lets it re-verify the original document via the congruence lemma.
161+
public export
162+
goodSelfSame : SameBinding Semantics.goodAtt Semantics.goodAtt
163+
goodSelfSame = MkSameBinding Refl
164+
165+
public export
166+
goodSameVerifies : Verifies Semantics.goodAtt Semantics.goodDoc
167+
goodSameVerifies =
168+
sameBindingVerifies Semantics.goodAtt Semantics.goodAtt Semantics.goodDoc
169+
goodSelfSame Semantics.goodVerifies
170+
171+
||| POSITIVE: idempotence holds concretely for the good document.
172+
public export
173+
goodIdempotent : boundDigest (attest Ed25519
174+
(MkDocument (markup Semantics.goodDoc)
175+
(boundDigest (attest Ed25519 Semantics.goodDoc))))
176+
= boundDigest (attest Ed25519 Semantics.goodDoc)
177+
goodIdempotent = attestIdempotent Ed25519 Semantics.goodDoc
178+
179+
--------------------------------------------------------------------------------
180+
-- 7. NEGATIVE / non-vacuity controls (must be refutable)
181+
--------------------------------------------------------------------------------
182+
183+
||| The honest attestation over `goodDoc` (digest 1729) and a tag bound to the
184+
||| tampered digest (9999) are NOT same-binding. Machine-checked refutation:
185+
||| any putative witness yields the absurd `1729 = 9999`.
186+
public export
187+
goodTamperNotSameBinding :
188+
Not (SameBinding Semantics.goodAtt (attest Ed25519 Semantics.tamperedDoc))
189+
goodTamperNotSameBinding (MkSameBinding prf) = absurdEq prf
190+
where
191+
absurdEq : (the Nat 1729 = the Nat 9999) -> Void
192+
absurdEq Refl impossible
193+
194+
||| NON-VACUITY of the round-trip recovery: the recovered digest equality for
195+
||| the good document is the concrete, true `1729 = 1729`. (If recovery were
196+
||| vacuous it could not produce this honest equality.)
197+
public export
198+
goodRecoveredDigest : boundDigest Semantics.goodAtt = contentDigest Semantics.goodDoc
199+
goodRecoveredDigest =
200+
certifyOkRecoversDigest Ed25519 Semantics.goodDoc goodRoundTrips
201+
202+
||| NEGATIVE CONTROL: the certifier does NOT return `Ok` for the original
203+
||| attestation against the tampered document. Any such equality is refuted
204+
||| through the Layer-2 soundness lemma (it would yield a forbidden `Verifies`).
205+
public export
206+
tamperNotCertifiedOk :
207+
Not (certify Semantics.goodAtt Semantics.tamperedDoc = Ok)
208+
tamperNotCertifiedOk okEq =
209+
Semantics.tamperedNotVerifiable
210+
(certifyOkSound Semantics.goodAtt Semantics.tamperedDoc okEq)

‎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, A2mliser.ABI.Semantics
4+
modules = A2mliser.ABI.Types, A2mliser.ABI.Layout, A2mliser.ABI.Foreign, A2mliser.ABI.Proofs, A2mliser.ABI.Semantics, A2mliser.ABI.Invariants

0 commit comments

Comments
 (0)