Skip to content

Commit 47239ed

Browse files
claudeclaude
committed
Fix Idris2 ABI proofs to genuinely compile and verify (0.7.0)
The src/interface/abi ABI was scaffolded from a template and never compiler-checked. This makes all three modules plus a new Proofs module build cleanly under Idris2 0.7.0 with zero errors and zero warnings, using only genuine, machine-checked proofs (no believe_me / postulate / holes / assert_total). Types.idr: - thisPlatform: replace unsupported %runElab (no ElabReflection) with a plain value (Linux). - DecEq SignatureAlgorithm / HashAlgorithm / AttestationResult: replace the non-compiling "decEq _ _ = No absurd" catch-all with explicit off-diagonal cases (No (\case Refl impossible)) for every distinct pair. - createHandle: solve the {auto 0 nonNull : So (ptr /= 0)} obligation via Data.So.choose instead of leaving it unsolved. - chainLength: define structurally (the index n is erased and was not accessible). - cSizeOf / cAlignOf: drop the unmatchable CInt _/CSize _ clauses (type- function applications cannot be pattern-matched; the primitive Bits32/ Bits64 cases already cover them). - EnvelopeHeader._pad: rename to padField (Idris record fields may not start with underscore). Layout.idr: - paddingFor: use Data.Nat.minus (Nat has no Neg) instead of (-). - Concrete StructLayout values: supply the erased auto-implicit proofs explicitly ({sizeCorrect = Oh} and {aligned = DivideBy k Refl} with totalSize = k * alignment). - verifyLayout: build the StructLayout with real proofs; add a sound decDivides : (n m : Nat) -> Maybe (Divides n m) (q = div m n; DivideBy q only when decEq m (q*n) holds). - checkCABI: implement via a sound decFieldsAligned over the field Vect (decDivides on each field's alignment vs offset); return Right/Left. - envelope/provenance CABI proofs: build FieldsAligned witnesses directly (qualify the layout name as Layout.* so it is not auto-bound implicit). - offsetInBounds: change the unsound universally-quantified So return type to Maybe (So ...) via choose. - Remove alignUpCorrect (its DivideBy ... Refl body was unprovable by Refl and its (align > 0) used Bool where a Type was required). - Rename signature-level Vect n Field binders to Vect k Field to avoid shadowing StructLayout's implicit n. Proofs.idr (new module, real theorems): - C-ABI compliance for every concrete layout (envelopeHeaderCompliant, digestBufferCompliant, ed25519SignatureCompliant, ed448SignatureCompliant, provenanceEntryCompliant) via direct DivideBy witnesses per field. - Result-code encoding pinned: okIsZero, signatureInvalidIsFive, okNotChainBroken. Build wiring: - Move flat src/interface/abi/{Types,Layout,Foreign}.idr to the nested A2mliser/ABI/ layout matching the A2mliser.ABI.* namespaces. - Add src/interface/abi/a2mliser-abi.ipkg. - .gitignore: add **/build/, *.ttc, *.ttm; do not commit the build dir. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA
1 parent 21906d2 commit 47239ed

6 files changed

Lines changed: 282 additions & 41 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,14 @@ Thumbs.db
1515
/target/
1616
/_build/
1717
/build/
18+
**/build/
1819
/dist/
1920
/out/
2021

22+
# Idris2
23+
*.ttc
24+
*.ttm
25+
2126
# Dependencies
2227
/node_modules/
2328
/vendor/

src/interface/abi/Foreign.idr renamed to src/interface/abi/A2mliser/ABI/Foreign.idr

File renamed without changes.

src/interface/abi/Layout.idr renamed to src/interface/abi/A2mliser/ABI/Layout.idr

Lines changed: 84 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ module A2mliser.ABI.Layout
1515
import A2mliser.ABI.Types
1616
import Data.Vect
1717
import Data.So
18+
import Data.Nat
19+
import Decidable.Equality
1820

1921
%default total
2022

@@ -28,7 +30,7 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
2830
paddingFor offset alignment =
2931
if offset `mod` alignment == 0
3032
then 0
31-
else alignment - (offset `mod` alignment)
33+
else minus alignment (offset `mod` alignment)
3234

3335
||| Proof that alignment divides aligned size
3436
public export
@@ -41,11 +43,6 @@ alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4143
alignUp size alignment =
4244
size + paddingFor size alignment
4345

44-
||| Proof that alignUp produces aligned result
45-
public export
46-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
47-
alignUpCorrect size align prf =
48-
DivideBy ((size + paddingFor size align) `div` align) Refl
4946

5047
--------------------------------------------------------------------------------
5148
-- Struct Field Layout
@@ -77,7 +74,7 @@ record StructLayout where
7774

7875
||| Calculate total struct size with padding
7976
public export
80-
calcStructSize : Vect n Field -> Nat -> Nat
77+
calcStructSize : Vect k Field -> Nat -> Nat
8178
calcStructSize [] align = 0
8279
calcStructSize (f :: fs) align =
8380
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -86,23 +83,38 @@ calcStructSize (f :: fs) align =
8683

8784
||| Proof that field offsets are correctly aligned
8885
public export
89-
data FieldsAligned : Vect n Field -> Type where
86+
data FieldsAligned : Vect k Field -> Type where
9087
NoFields : FieldsAligned []
9188
ConsField :
9289
(f : Field) ->
93-
(rest : Vect n Field) ->
90+
(rest : Vect k Field) ->
9491
Divides f.alignment f.offset ->
9592
FieldsAligned rest ->
9693
FieldsAligned (f :: rest)
9794

98-
||| Verify a struct layout is valid
95+
||| Decide whether `n` divides `m`, returning a Divides witness when it does.
96+
||| Sound: only returns Just when m is genuinely a multiple of n.
97+
public export
98+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
99+
decDivides Z m = Nothing
100+
decDivides (S k) m =
101+
let q = div m (S k) in
102+
case decEq m (q * (S k)) of
103+
Yes prf => Just (DivideBy q prf)
104+
No _ => Nothing
105+
106+
||| Verify a struct layout is valid.
107+
||| Requires both the size obligation and a genuine divisibility witness.
99108
public export
100-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
109+
verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
101110
verifyLayout fields align =
102-
let size = calcStructSize fields align
103-
in case decSo (size >= sum (map (\f => f.size) fields)) of
104-
Yes prf => Right (MkStructLayout fields size align)
105-
No _ => Left "Invalid struct size"
111+
let size = calcStructSize fields align in
112+
case decSo (size >= sum (map (\f => f.size) fields)) of
113+
No _ => Left "Invalid struct size"
114+
Yes prf =>
115+
case decDivides align size of
116+
Nothing => Left "Struct size not aligned"
117+
Just dv => Right (MkStructLayout fields size align {sizeCorrect = prf} {aligned = dv})
106118

107119
--------------------------------------------------------------------------------
108120
-- Attestation Envelope Header Layout
@@ -135,6 +147,8 @@ envelopeHeaderLayout =
135147
]
136148
32 -- Total size: 32 bytes
137149
8 -- Alignment: 8 bytes
150+
{sizeCorrect = Oh}
151+
{aligned = DivideBy 4 Refl}
138152

139153
--------------------------------------------------------------------------------
140154
-- Digest Buffer Layout
@@ -150,6 +164,8 @@ digestBufferLayout =
150164
]
151165
32 -- Total size: 32 bytes
152166
1 -- Alignment: 1 byte (byte array)
167+
{sizeCorrect = Oh}
168+
{aligned = DivideBy 32 Refl}
153169

154170
--------------------------------------------------------------------------------
155171
-- Signature Buffer Layout
@@ -164,6 +180,8 @@ ed25519SignatureLayout =
164180
]
165181
64 -- Total size: 64 bytes
166182
1 -- Alignment: 1 byte
183+
{sizeCorrect = Oh}
184+
{aligned = DivideBy 64 Refl}
167185

168186
||| Layout for an Ed448 signature buffer (114 bytes).
169187
public export
@@ -174,6 +192,8 @@ ed448SignatureLayout =
174192
]
175193
114 -- Total size: 114 bytes (no padding needed for byte arrays)
176194
1 -- Alignment: 1 byte
195+
{sizeCorrect = Oh}
196+
{aligned = DivideBy 114 Refl}
177197

178198
--------------------------------------------------------------------------------
179199
-- Provenance Chain Entry Layout
@@ -201,6 +221,8 @@ provenanceEntryLayout =
201221
]
202222
56 -- Total size: 56 bytes
203223
8 -- Alignment: 8 bytes
224+
{sizeCorrect = Oh}
225+
{aligned = DivideBy 7 Refl}
204226

205227
--------------------------------------------------------------------------------
206228
-- Platform-Specific Layouts
@@ -234,21 +256,52 @@ data CABICompliant : StructLayout -> Type where
234256
FieldsAligned layout.fields ->
235257
CABICompliant layout
236258

259+
||| Decide, soundly, whether every field's offset is aligned to its own
260+
||| alignment, building a genuine FieldsAligned witness when so.
261+
public export
262+
decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields)
263+
decFieldsAligned [] = Just NoFields
264+
decFieldsAligned (f :: fs) =
265+
case decDivides f.alignment f.offset of
266+
Nothing => Nothing
267+
Just dv =>
268+
case decFieldsAligned fs of
269+
Nothing => Nothing
270+
Just rest => Just (ConsField f fs dv rest)
271+
237272
||| Check if layout follows C ABI
238273
public export
239274
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
240275
checkCABI layout =
241-
Right (CABIOk layout ?fieldsAlignedProof)
276+
case decFieldsAligned layout.fields of
277+
Just fa => Right (CABIOk layout fa)
278+
Nothing => Left "Struct fields are not C-ABI aligned"
242279

243-
||| Proof that envelope header layout is C ABI compliant
280+
||| Proof that envelope header layout is C ABI compliant.
281+
||| Each field offset is a multiple of its alignment, witnessed directly.
244282
export
245-
envelopeHeaderCABI : CABICompliant envelopeHeaderLayout
246-
envelopeHeaderCABI = CABIOk envelopeHeaderLayout ?envelopeHeaderFieldsAligned
247-
248-
||| Proof that provenance entry layout is C ABI compliant
283+
envelopeHeaderCABI : CABICompliant Layout.envelopeHeaderLayout
284+
envelopeHeaderCABI =
285+
CABIOk Layout.envelopeHeaderLayout
286+
(ConsField _ _ (DivideBy 0 Refl)
287+
(ConsField _ _ (DivideBy 1 Refl)
288+
(ConsField _ _ (DivideBy 2 Refl)
289+
(ConsField _ _ (DivideBy 3 Refl)
290+
(ConsField _ _ (DivideBy 2 Refl)
291+
(ConsField _ _ (DivideBy 6 Refl)
292+
(ConsField _ _ (DivideBy 7 Refl)
293+
NoFields)))))))
294+
295+
||| Proof that provenance entry layout is C ABI compliant.
249296
export
250-
provenanceEntryCABI : CABICompliant provenanceEntryLayout
251-
provenanceEntryCABI = CABIOk provenanceEntryLayout ?provenanceEntryFieldsAligned
297+
provenanceEntryCABI : CABICompliant Layout.provenanceEntryLayout
298+
provenanceEntryCABI =
299+
CABIOk Layout.provenanceEntryLayout
300+
(ConsField _ _ (DivideBy 0 Refl)
301+
(ConsField _ _ (DivideBy 4 Refl)
302+
(ConsField _ _ (DivideBy 5 Refl)
303+
(ConsField _ _ (DivideBy 6 Refl)
304+
NoFields))))
252305

253306
--------------------------------------------------------------------------------
254307
-- Offset Calculation
@@ -262,7 +315,12 @@ fieldOffset layout name =
262315
Just idx => Just (finToNat idx ** index idx layout.fields)
263316
Nothing => Nothing
264317

265-
||| Proof that field offset is within struct bounds
318+
||| Decide whether a field lies within the struct bounds.
319+
||| The universally-quantified form is unsound (false for fields that do not
320+
||| belong to the layout), so this returns a Maybe witness via `choose`.
266321
public export
267-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
268-
offsetInBounds layout f = ?offsetInBoundsProof
322+
offsetInBounds : (layout : StructLayout) -> (f : Field) -> Maybe (So (f.offset + f.size <= layout.totalSize))
323+
offsetInBounds layout f =
324+
case choose (f.offset + f.size <= layout.totalSize) of
325+
Left ok => Just ok
326+
Right _ => Nothing

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

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
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+
||| Machine-checked theorems about the a2mliser ABI.
5+
|||
6+
||| This module carries genuine, compiler-verified proofs:
7+
||| * C-ABI compliance of every concrete struct layout, with each field's
8+
||| offset shown to be a multiple of its alignment via a direct `DivideBy`
9+
||| witness (multiplication reduces during typechecking; division does not,
10+
||| so the witnesses are built directly rather than via `decFieldsAligned`).
11+
||| * The result-code encoding is pinned (e.g. `Ok` maps to 0).
12+
|||
13+
||| @see A2mliser.ABI.Layout for the layout definitions being proven about.
14+
15+
module A2mliser.ABI.Proofs
16+
17+
import A2mliser.ABI.Types
18+
import A2mliser.ABI.Layout
19+
import Data.Vect
20+
21+
%default total
22+
23+
--------------------------------------------------------------------------------
24+
-- C-ABI Compliance of Concrete Layouts
25+
--------------------------------------------------------------------------------
26+
27+
||| The envelope-header layout is C-ABI compliant: every field's offset is a
28+
||| multiple of its alignment.
29+
||| hashAlgId 0 = 0*4 | sigAlgId 4 = 1*4 | digestLen 8 = 2*4
30+
||| signatureLen 12 = 3*4 | timestamp 16 = 2*8 | hasParent 24 = 6*4
31+
||| _pad 28 = 7*4
32+
export
33+
envelopeHeaderCompliant : CABICompliant Layout.envelopeHeaderLayout
34+
envelopeHeaderCompliant =
35+
CABIOk Layout.envelopeHeaderLayout
36+
(ConsField _ _ (DivideBy 0 Refl)
37+
(ConsField _ _ (DivideBy 1 Refl)
38+
(ConsField _ _ (DivideBy 2 Refl)
39+
(ConsField _ _ (DivideBy 3 Refl)
40+
(ConsField _ _ (DivideBy 2 Refl)
41+
(ConsField _ _ (DivideBy 6 Refl)
42+
(ConsField _ _ (DivideBy 7 Refl)
43+
NoFields)))))))
44+
45+
||| The digest-buffer layout is C-ABI compliant (single byte-aligned field at 0).
46+
export
47+
digestBufferCompliant : CABICompliant Layout.digestBufferLayout
48+
digestBufferCompliant =
49+
CABIOk Layout.digestBufferLayout
50+
(ConsField _ _ (DivideBy 0 Refl)
51+
NoFields)
52+
53+
||| The Ed25519 signature-buffer layout is C-ABI compliant.
54+
export
55+
ed25519SignatureCompliant : CABICompliant Layout.ed25519SignatureLayout
56+
ed25519SignatureCompliant =
57+
CABIOk Layout.ed25519SignatureLayout
58+
(ConsField _ _ (DivideBy 0 Refl)
59+
NoFields)
60+
61+
||| The Ed448 signature-buffer layout is C-ABI compliant.
62+
export
63+
ed448SignatureCompliant : CABICompliant Layout.ed448SignatureLayout
64+
ed448SignatureCompliant =
65+
CABIOk Layout.ed448SignatureLayout
66+
(ConsField _ _ (DivideBy 0 Refl)
67+
NoFields)
68+
69+
||| The provenance-entry layout is C-ABI compliant.
70+
||| header 0 = 0*8 | digestPtr 32 = 4*8
71+
||| signaturePtr 40 = 5*8 | parentPtr 48 = 6*8
72+
export
73+
provenanceEntryCompliant : CABICompliant Layout.provenanceEntryLayout
74+
provenanceEntryCompliant =
75+
CABIOk Layout.provenanceEntryLayout
76+
(ConsField _ _ (DivideBy 0 Refl)
77+
(ConsField _ _ (DivideBy 4 Refl)
78+
(ConsField _ _ (DivideBy 5 Refl)
79+
(ConsField _ _ (DivideBy 6 Refl)
80+
NoFields))))
81+
82+
--------------------------------------------------------------------------------
83+
-- Result-Code Encoding
84+
--------------------------------------------------------------------------------
85+
86+
||| `Ok` is encoded as the C success value 0.
87+
export
88+
okIsZero : resultToInt Ok = 0
89+
okIsZero = Refl
90+
91+
||| `SignatureInvalid` is encoded as 5, matching the FFI contract used by
92+
||| `verifyEd25519` / `verifyEnvelope` in Foreign.idr.
93+
export
94+
signatureInvalidIsFive : resultToInt SignatureInvalid = 5
95+
signatureInvalidIsFive = Refl
96+
97+
||| The result encoding is injective on the pair we rely on most at the FFI
98+
||| boundary: success (0) is distinct from a broken provenance chain (7).
99+
export
100+
okNotChainBroken : Not (resultToInt Ok = resultToInt ChainBroken)
101+
okNotChainBroken = \case Refl impossible

0 commit comments

Comments
 (0)