Skip to content

Commit cb0826d

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#42)
* Add SPDX header to LICENSE and set Cargo.toml license field The governance/licence-consistency check requires an SPDX-License-Identifier header on the LICENSE file and a `license` field in the manifest. The LICENSE body is MPL-2.0 text, so stamp `SPDX-License-Identifier: MPL-2.0` (matching the actual body) and set `license = "MPL-2.0"` (replacing `license-file`). Verified with standards/scripts/check-licence-consistency.sh (passes). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA * Normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs) Make the repo's licensing single and consistent, matching the wokelangiser reference policy and the merged iseriser pattern: - Remove contradictory PMPL-1.0-or-later / Palimpsest self-claims from README badges/footers, QUICKSTART, RSR_OUTLINE, STATE-VISUALIZER, and machine-readable governance (META, stapeln, deny.toml allow-list, copilot/AGENTIC SPDX directives, Trust/Must LICENSE-content checks, per-project CLAUDE.md). - Encode the docs split in REUSE dep5: *.adoc/*.md/docs/** -> CC-BY-SA-4.0, everything else -> MPL-2.0. - READMEs show MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges; full texts live in LICENSES/; root LICENSE stays MPL-2.0 for GitHub's licence chip. Preserves legitimate non-self references: cargo-deny's AGPL deny-list, the "never use AGPL" estate policy, and the Contributor Covenant CoC. Verified: standards/scripts/check-licence-consistency.sh passes; no residual PMPL/Palimpsest self-claims remain. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA * Fix k9iser Idris2 ABI proofs to genuinely compile and verify The src/interface/abi ABI was scaffolded from a template and never compiler-checked. Make it build clean under Idris2 0.7.0 with real proofs. Types.idr: - Replace %runElab thisPlatform stub (needed ElabReflection) with plain Linux. - DecEq Result: replace non-compiling `decEq _ _ = No absurd` with all 56 explicit off-diagonal `No (\case Refl impossible)` cases over 8 constructors. - createHandle: solve the auto `So (ptr /= 0)` via `choose` instead of leaving the MkHandle nonNull proof unsolved. - validationConsistent: was an unsound universally-quantified `So`; change to a decided `Maybe (So ...)` via choose. - CPtr: `Bits (ptrSize p)` does not typecheck (Bits is a class); represent a pointer as CSize p (pointer-sized integer). - cSizeOf/cAlignOf: drop the invalid `CInt _`/`CSize _` type-alias matches; the aliases reduce to Bits32/Bits64 handled by concrete clauses. - Annotate FFI format-code literals as Bits32. Layout.idr: - paddingFor: use Nat `minus` instead of `-` (Nat has no Neg). - Replace alignUpCorrect (`DivideBy ... Refl` on symbolic input) with sound decDivides + alignUpDivides. - Concrete StructLayouts: supply erased proofs {sizeCorrect = Oh} and {aligned = DivideBy k Refl} (40 = 5*8, 32 = 4*8). - checkCABI: implement via decFieldsAligned (was a ?hole). - verifyLayout: used nonexistent decSo and dropped the aligned obligation; reimplement returning Maybe with both obligations discharged. - offsetInBounds: was an unsound universal `So`; change to decided Maybe. - fieldOffset: return Maybe (Nat, Field) (the `(n : Nat ** Field)` auto-bound a stray implicit). - Rename Vect n -> Vect k to avoid shadowing warnings. Proofs.idr (new): machine-checked theorems — - k9ContractCompliant, validationResultCompliant, mustRuleCompliant built directly from per-field DivideBy witnesses (offset = k * alignment). - okIsZero, trustFailureIsSeven (result-code encoding the FFI depends on). - kennelIsZero, tiersOrdered (safety-tier ordering). Build: - Move flat files to src/interface/abi/K9iser/ABI/ so paths match namespaces. - Add src/interface/abi/k9iser-abi.ipkg. - Ignore Idris2 build artifacts (**/build/, *.ttc, *.ttm). `idris2 --build k9iser-abi.ipkg` exits 0 with zero warnings and zero errors. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --------- Co-authored-by: Jonathan D.A. Jewell <paraordinate@yahoo.co.uk> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent fb79ccc commit cb0826d

6 files changed

Lines changed: 296 additions & 54 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ Thumbs.db
1818
/dist/
1919
/out/
2020

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

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ prim__parseConfigFile : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32
5858
export
5959
parseConfigFile : Handle -> (pathPtr : Bits64) -> ConfigFormat -> IO (Either Result ())
6060
parseConfigFile h pathPtr fmt = do
61-
let fmtInt = case fmt of
61+
let fmtInt : Bits32 = case fmt of
6262
FormatTOML => 0
6363
FormatYAML => 1
6464
FormatJSON => 2
@@ -78,7 +78,7 @@ prim__parseConfigBuffer : Bits64 -> Bits64 -> Bits32 -> Bits32 -> PrimIO Bits32
7878
export
7979
parseConfigBuffer : Handle -> (bufPtr : Bits64) -> (len : Bits32) -> ConfigFormat -> IO (Either Result ())
8080
parseConfigBuffer h bufPtr len fmt = do
81-
let fmtInt = case fmt of
81+
let fmtInt : Bits32 = case fmt of
8282
FormatTOML => 0
8383
FormatYAML => 1
8484
FormatJSON => 2
@@ -157,7 +157,7 @@ prim__generateContract : Bits64 -> Bits32 -> PrimIO Bits32
157157
export
158158
generateContract : Handle -> SafetyTier -> IO (Either Result ())
159159
generateContract h tier = do
160-
let tierInt = case tier of
160+
let tierInt : Bits32 = case tier of
161161
Kennel => 0
162162
Yard => 1
163163
Hunt => 2

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

Lines changed: 83 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ module K9iser.ABI.Layout
1313
import K9iser.ABI.Types
1414
import Data.Vect
1515
import Data.So
16+
import Data.Nat
17+
import Decidable.Equality
1618

1719
%default total
1820

@@ -26,24 +28,42 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
2628
paddingFor offset alignment =
2729
if offset `mod` alignment == 0
2830
then 0
29-
else alignment - (offset `mod` alignment)
31+
else minus alignment (offset `mod` alignment)
3032

31-
||| Proof that alignment divides aligned size
33+
||| Proof that alignment divides aligned size: `m = k * n`.
3234
public export
3335
data Divides : Nat -> Nat -> Type where
3436
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
3537

38+
||| Sound decision procedure for divisibility. Returns a genuine
39+
||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing.
40+
||| Division by zero is undecidable here and yields Nothing.
41+
public export
42+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
43+
decDivides Z _ = Nothing
44+
decDivides (S k) m =
45+
let q = m `div` (S k) in
46+
case decEq m (q * (S k)) of
47+
Yes prf => Just (DivideBy q prf)
48+
No _ => Nothing
49+
3650
||| Round up to next alignment boundary
3751
public export
3852
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
3953
alignUp size alignment =
4054
size + paddingFor size alignment
4155

42-
||| Proof that alignUp produces aligned result
56+
||| Sound divisibility check for an aligned size. The general theorem
57+
||| "alignUp size align is always divisible by align" needs div/mod lemmas and
58+
||| is tracked as residual proof work; here we *decide* it via `decDivides`,
59+
||| which returns a genuine witness when it holds. For the concrete ABI layouts
60+
||| below, divisibility is proven outright (`DivideBy`). (Previously
61+
||| `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot typecheck for
62+
||| symbolic inputs.)
4363
public export
44-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
45-
alignUpCorrect size align prf =
46-
DivideBy ((size + paddingFor size align) `div` align) Refl
64+
alignUpDivides : (size : Nat) -> (align : Nat) ->
65+
Maybe (Divides align (alignUp size align))
66+
alignUpDivides size align = decDivides align (alignUp size align)
4767

4868
--------------------------------------------------------------------------------
4969
-- Struct Field Layout
@@ -75,7 +95,7 @@ record StructLayout where
7595

7696
||| Calculate total struct size with padding
7797
public export
78-
calcStructSize : Vect n Field -> Nat -> Nat
98+
calcStructSize : Vect k Field -> Nat -> Nat
7999
calcStructSize [] align = 0
80100
calcStructSize (f :: fs) align =
81101
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -84,23 +104,44 @@ calcStructSize (f :: fs) align =
84104

85105
||| Proof that field offsets are correctly aligned
86106
public export
87-
data FieldsAligned : Vect n Field -> Type where
107+
data FieldsAligned : Vect k Field -> Type where
88108
NoFields : FieldsAligned []
89109
ConsField :
90110
(f : Field) ->
91-
(rest : Vect n Field) ->
111+
(rest : Vect k Field) ->
92112
Divides f.alignment f.offset ->
93113
FieldsAligned rest ->
94114
FieldsAligned (f :: rest)
95115

96-
||| Verify a struct layout is valid
116+
||| Decide field alignment for every field, building a real `FieldsAligned`
117+
||| witness from per-field divisibility proofs.
118+
public export
119+
decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs)
120+
decFieldsAligned [] = Just NoFields
121+
decFieldsAligned (f :: fs) =
122+
case decDivides f.alignment f.offset of
123+
Nothing => Nothing
124+
Just dvd => case decFieldsAligned fs of
125+
Nothing => Nothing
126+
Just rest => Just (ConsField f fs dvd rest)
127+
128+
||| Verify a struct layout is valid and construct it. Both erased obligations
129+
||| are discharged from real decision procedures: the size lower bound via
130+
||| `choose`, and the size/alignment divisibility via `decDivides`. Returns
131+
||| Nothing when either obligation cannot be met. (Previously used a nonexistent
132+
||| `decSo` and silently dropped the `aligned` obligation.)
97133
public export
98-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
134+
verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Maybe StructLayout
99135
verifyLayout fields align =
100-
let size = calcStructSize fields align
101-
in case decSo (size >= sum (map (\f => f.size) fields)) of
102-
Yes prf => Right (MkStructLayout fields size align)
103-
No _ => Left "Invalid struct size"
136+
let size = calcStructSize fields align in
137+
case choose (size >= sum (map (\f => f.size) fields)) of
138+
Right _ => Nothing
139+
Left okSize =>
140+
case decDivides align size of
141+
Nothing => Nothing
142+
Just okAlign =>
143+
Just (MkStructLayout fields size align
144+
{sizeCorrect = okSize, aligned = okAlign})
104145

105146
--------------------------------------------------------------------------------
106147
-- K9 Contract Layout
@@ -132,6 +173,8 @@ k9ContractLayout =
132173
]
133174
40 -- Total size: 40 bytes
134175
8 -- Alignment: 8 bytes (pointer alignment)
176+
{sizeCorrect = Oh}
177+
{aligned = DivideBy 5 Refl}
135178

136179
||| Layout for the ValidationResult struct.
137180
|||
@@ -156,6 +199,8 @@ validationResultLayout =
156199
]
157200
32 -- Total size: 32 bytes (with 4 bytes tail padding)
158201
8 -- Alignment: 8 bytes
202+
{sizeCorrect = Oh}
203+
{aligned = DivideBy 4 Refl}
159204

160205
||| Layout for MustRule struct.
161206
|||
@@ -176,6 +221,8 @@ mustRuleLayout =
176221
]
177222
32 -- Total size: 32 bytes (with 4 bytes tail padding)
178223
8 -- Alignment: 8 bytes
224+
{sizeCorrect = Oh}
225+
{aligned = DivideBy 4 Refl}
179226

180227
--------------------------------------------------------------------------------
181228
-- Platform-Specific Layouts
@@ -206,35 +253,40 @@ data CABICompliant : StructLayout -> Type where
206253
FieldsAligned layout.fields ->
207254
CABICompliant layout
208255

209-
||| Check if layout follows C ABI
256+
||| Verify a layout against the C ABI alignment rules, returning a genuine
257+
||| `CABICompliant` proof (built from real per-field divisibility witnesses)
258+
||| or an error when some field offset is misaligned. (Previously a `?hole`.)
210259
public export
211260
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
212261
checkCABI layout =
213-
Right (CABIOk layout ?fieldsAlignedProof)
214-
215-
||| Proof that K9 contract layout is C ABI compliant
216-
export
217-
k9ContractCABI : CABICompliant k9ContractLayout
218-
k9ContractCABI = CABIOk k9ContractLayout ?k9ContractFieldsAligned
262+
case decFieldsAligned layout.fields of
263+
Just prf => Right (CABIOk layout prf)
264+
Nothing => Left "Field offsets are not correctly aligned for the C ABI"
219265

220-
||| Proof that validation result layout is C ABI compliant
221-
export
222-
validationResultCABI : CABICompliant validationResultLayout
223-
validationResultCABI = CABIOk validationResultLayout ?validationResultFieldsAligned
266+
-- The concrete per-layout C-ABI compliance witnesses live in
267+
-- `K9iser.ABI.Proofs`, where each layout name is qualified (`Layout.foo`) in
268+
-- the theorem type so it is not auto-bound as an implicit.
224269

225270
--------------------------------------------------------------------------------
226271
-- Offset Calculation
227272
--------------------------------------------------------------------------------
228273

229274
||| Calculate field offset with proof of correctness
230275
public export
231-
fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (n : Nat ** Field)
276+
fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (Nat, Field)
232277
fieldOffset layout name =
233278
case findIndex (\f => f.name == name) layout.fields of
234-
Just idx => Just (finToNat idx ** index idx layout.fields)
279+
Just idx => Just (finToNat idx, index idx layout.fields)
235280
Nothing => Nothing
236281

237-
||| Proof that field offset is within struct bounds
282+
||| Decide whether a field lies within a struct's byte bounds, returning a
283+
||| genuine proof when `offset + size <= totalSize`. The previous signature
284+
||| asserted this for *every* field unconditionally, which is false (a field
285+
||| need not belong to the layout); this honest version decides it.
238286
public export
239-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
240-
offsetInBounds layout f = ?offsetInBoundsProof
287+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
288+
Maybe (So (f.offset + f.size <= layout.totalSize))
289+
offsetInBounds layout f =
290+
case choose (f.offset + f.size <= layout.totalSize) of
291+
Left ok => Just ok
292+
Right _ => Nothing

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

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
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 proofs over the k9iser ABI.
5+
|||
6+
||| These are not runtime tests — they are propositional statements the Idris2
7+
||| type checker must discharge at compile time. If any concrete ABI layout
8+
||| were misaligned, the result-code encoding wrong, or a decision procedure
9+
||| mis-defined, this module would fail to typecheck and the proof build would
10+
||| go red.
11+
|||
12+
||| The C-ABI compliance witnesses are built directly from per-field
13+
||| divisibility proofs (`DivideBy k Refl`, where `offset = k * alignment`).
14+
||| Multiplication reduces during type checking, so these are fully verified by
15+
||| the compiler; we avoid routing them through `Nat` division, which is a
16+
||| primitive that does not reduce at the type level.
17+
18+
module K9iser.ABI.Proofs
19+
20+
import K9iser.ABI.Types
21+
import K9iser.ABI.Layout
22+
import Data.So
23+
import Data.Vect
24+
25+
%default total
26+
27+
--------------------------------------------------------------------------------
28+
-- The concrete FFI struct layouts are provably C-ABI compliant.
29+
--------------------------------------------------------------------------------
30+
31+
||| Every field offset in the K9Contract layout divides its alignment:
32+
||| 0|8, 8|8, 16|4, 20|4, 24|4, 28|4, 32|4, 36|4.
33+
export
34+
k9ContractCompliant : CABICompliant Layout.k9ContractLayout
35+
k9ContractCompliant =
36+
CABIOk k9ContractLayout
37+
(ConsField _ _ (DivideBy 0 Refl)
38+
(ConsField _ _ (DivideBy 1 Refl)
39+
(ConsField _ _ (DivideBy 4 Refl)
40+
(ConsField _ _ (DivideBy 5 Refl)
41+
(ConsField _ _ (DivideBy 6 Refl)
42+
(ConsField _ _ (DivideBy 7 Refl)
43+
(ConsField _ _ (DivideBy 8 Refl)
44+
(ConsField _ _ (DivideBy 9 Refl)
45+
NoFields))))))))
46+
47+
||| Every field offset in the ValidationResult layout is aligned:
48+
||| 0|8, 8|4, 12|4, 16|4, 20|4, 24|4.
49+
export
50+
validationResultCompliant : CABICompliant Layout.validationResultLayout
51+
validationResultCompliant =
52+
CABIOk validationResultLayout
53+
(ConsField _ _ (DivideBy 0 Refl)
54+
(ConsField _ _ (DivideBy 2 Refl)
55+
(ConsField _ _ (DivideBy 3 Refl)
56+
(ConsField _ _ (DivideBy 4 Refl)
57+
(ConsField _ _ (DivideBy 5 Refl)
58+
(ConsField _ _ (DivideBy 6 Refl)
59+
NoFields))))))
60+
61+
||| Every field offset in the MustRule layout is aligned:
62+
||| 0|8, 8|8, 16|8, 24|4.
63+
export
64+
mustRuleCompliant : CABICompliant Layout.mustRuleLayout
65+
mustRuleCompliant =
66+
CABIOk mustRuleLayout
67+
(ConsField _ _ (DivideBy 0 Refl)
68+
(ConsField _ _ (DivideBy 1 Refl)
69+
(ConsField _ _ (DivideBy 2 Refl)
70+
(ConsField _ _ (DivideBy 6 Refl)
71+
NoFields))))
72+
73+
--------------------------------------------------------------------------------
74+
-- Result-code round-trip: the encoding the Zig FFI depends on.
75+
--------------------------------------------------------------------------------
76+
77+
||| The success code is zero, as every FFI caller assumes.
78+
export
79+
okIsZero : resultToInt Ok = 0
80+
okIsZero = Refl
81+
82+
||| The trust-failure code is seven (the last code in the enumeration).
83+
export
84+
trustFailureIsSeven : resultToInt TrustFailure = 7
85+
trustFailureIsSeven = Refl
86+
87+
--------------------------------------------------------------------------------
88+
-- Safety-tier ordering: the tier levels are strictly increasing.
89+
--------------------------------------------------------------------------------
90+
91+
||| Kennel is the least-powerful tier (level 0).
92+
export
93+
kennelIsZero : tierLevel Kennel = 0
94+
kennelIsZero = Refl
95+
96+
||| The safety tiers are strictly ordered Kennel < Yard < Hunt by level.
97+
export
98+
tiersOrdered : So (tierLevel Kennel < tierLevel Yard &&
99+
tierLevel Yard < tierLevel Hunt)
100+
tiersOrdered = Oh

0 commit comments

Comments
 (0)