Skip to content

Commit be1d62d

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#32)
* 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 Idris2 ABI proofs to genuinely compile and verify under 0.7.0 The scaffolded ABI under src/interface/abi was never compiler-checked. This makes all four modules build cleanly (zero errors, zero warnings) with /usr/local/bin/idris2 0.7.0 and adds real machine-checked theorems. Types.idr: - Replace %runElab thisPlatform (ElabReflection not enabled) with plain Linux. - DecEq Result: replace uncompilable "decEq _ _ = No absurd" catch-all with explicit off-diagonal No (\case Refl impossible) cases for all 56 distinct ordered constructor pairs. - createHandle: solve the {auto 0 nonNull : So (ptr /= 0)} proof via choose (ptr /= 0) instead of an unsolved Just (MkHandle ptr). - Rename the duplicate NimObject record to NimObjectDef (it collided with the NimObject constructor of NimTypeKind). - Fix CPtr to return a concrete pointer-sized integer type per platform. - Fix cSizeOf/cAlignOf which tried to pattern-match on the type-level functions CInt/CSize (illegal); match concrete Bits widths instead. - import Decidable.Equality. Layout.idr: - paddingFor: use minus (Nat has no Neg) instead of (-). - Add sound decDivides : (n m : Nat) -> Maybe (Divides n m) via div + decEq. - alignUpCorrect: was an unsound universally-quantified Refl proof; now a sound decision returning Maybe (Divides align (alignUp size align)). - checkCABI: implement decFieldsAligned over the Vect and return a real CABICompliant witness (or Left) instead of the ?fieldsAlignedProof hole. - offsetInBounds: was an unsound universally-quantified So; now returns Maybe (So ...) decided via choose. - verifyLayout: supply the erased sizeCorrect/aligned proofs explicitly (choose + decDivides) instead of leaving them unsolved. - Concrete nimBufferLayout/nimResultLayout: supply {sizeCorrect = Oh} and {aligned = DivideBy k Refl}. - nimBufferLayoutValid/nimResultLayoutValid: build the FieldsAligned witness directly (one DivideBy per field) instead of holes; qualify layout names. - Rename shadowing implicit n to k in Vect signatures. - import Data.Nat, Decidable.Equality. Foreign.idr: - Declare prim__getString before the generation wrappers so it resolves to the user Bits64 -> String type rather than the builtin Ptr String shape. Proofs.idr (new): - nimBufferCompliant, nimResultCompliant: CABICompliant proofs built directly. - okIsZero, nullPointerIsFour, okDistinctFromError: result-encoding facts. Buildability: - git mv flat files into Nimiser/ABI/ to match module namespaces. - Add nimiser-abi.ipkg (modules Types, Layout, Foreign, Proofs). - Add **/build/, *.ttc, *.ttm to .gitignore. 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 6908e75 commit be1d62d

6 files changed

Lines changed: 235 additions & 44 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,3 +104,8 @@ sync_report*.txt
104104
# Hypatia scan cache (local-only)
105105
.hypatia/
106106
target/
107+
108+
# Idris2 build artefacts
109+
**/build/
110+
*.ttc
111+
*.ttm

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

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,15 @@ export
5050
free : Handle -> IO ()
5151
free h = primIO (prim__free (handlePtr h))
5252

53+
--------------------------------------------------------------------------------
54+
-- String Marshalling (declared early; used by the generation wrappers below)
55+
--------------------------------------------------------------------------------
56+
57+
||| Convert C string to Idris String
58+
export
59+
%foreign "support:idris2_getString, libidris2_support"
60+
prim__getString : Bits64 -> String
61+
5362
--------------------------------------------------------------------------------
5463
-- Nim Compilation Pipeline
5564
--------------------------------------------------------------------------------
@@ -102,7 +111,9 @@ genTemplate h tmpl = do
102111
(if tmpl.exported then 1 else 0))
103112
if ptr == 0
104113
then pure (Left TemplateError)
105-
else pure (Right (prim__getString ptr))
114+
else do
115+
let str = prim__getString ptr
116+
pure (Right str)
106117

107118
||| Generate Nim macro code from a macro definition
108119
||| Returns a C string containing generated Nim source, or null on error.
@@ -121,17 +132,14 @@ genMacro h mac = do
121132
(if mac.generatesExport then 1 else 0))
122133
if ptr == 0
123134
then pure (Left MacroError)
124-
else pure (Right (prim__getString ptr))
135+
else do
136+
let str = prim__getString ptr
137+
pure (Right str)
125138

126139
--------------------------------------------------------------------------------
127140
-- String Operations
128141
--------------------------------------------------------------------------------
129142

130-
||| Convert C string to Idris String
131-
export
132-
%foreign "support:idris2_getString, libidris2_support"
133-
prim__getString : Bits64 -> String
134-
135143
||| Free C string allocated by the Nim library
136144
export
137145
%foreign "C:nimiser_free_string, libnimiser"

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

Lines changed: 73 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ module Nimiser.ABI.Layout
2020
import Nimiser.ABI.Types
2121
import Data.Vect
2222
import Data.So
23+
import Data.Nat
24+
import Decidable.Equality
2325

2426
%default total
2527

@@ -33,24 +35,38 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
3335
paddingFor offset alignment =
3436
if offset `mod` alignment == 0
3537
then 0
36-
else alignment - (offset `mod` alignment)
38+
else minus alignment (offset `mod` alignment)
3739

3840
||| Proof that alignment divides aligned size
3941
public export
4042
data Divides : Nat -> Nat -> Type where
4143
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
4244

45+
||| Sound decision procedure: does n divide m?
46+
||| For n = S j, compute q = div m (S j) and check m == q * (S j).
47+
||| Division does not reduce definitionally, so the equality is checked, not
48+
||| asserted.
49+
public export
50+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
51+
decDivides Z _ = Nothing
52+
decDivides (S j) m =
53+
let q = div m (S j) in
54+
case decEq m (q * (S j)) of
55+
Yes prf => Just (DivideBy q prf)
56+
No _ => Nothing
57+
4358
||| Round up to next alignment boundary
4459
public export
4560
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4661
alignUp size alignment =
4762
size + paddingFor size alignment
4863

49-
||| Proof that alignUp produces aligned result
64+
||| Decide whether alignUp produced an aligned result for a given alignment.
65+
||| (Division does not reduce definitionally, so this is decided rather than
66+
||| proven by `Refl`; a universally-quantified `Refl` proof would be unsound.)
5067
public export
51-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
52-
alignUpCorrect size align prf =
53-
DivideBy ((size + paddingFor size align) `div` align) Refl
68+
alignUpCorrect : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align))
69+
alignUpCorrect size align = decDivides align (alignUp size align)
5470

5571
--------------------------------------------------------------------------------
5672
-- Struct Field Layout
@@ -82,7 +98,7 @@ record StructLayout where
8298

8399
||| Calculate total struct size with padding
84100
public export
85-
calcStructSize : Vect n Field -> Nat -> Nat
101+
calcStructSize : Vect k Field -> Nat -> Nat
86102
calcStructSize [] align = 0
87103
calcStructSize (f :: fs) align =
88104
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -91,23 +107,28 @@ calcStructSize (f :: fs) align =
91107

92108
||| Proof that field offsets are correctly aligned
93109
public export
94-
data FieldsAligned : Vect n Field -> Type where
110+
data FieldsAligned : Vect k Field -> Type where
95111
NoFields : FieldsAligned []
96112
ConsField :
97113
(f : Field) ->
98-
(rest : Vect n Field) ->
114+
(rest : Vect k Field) ->
99115
Divides f.alignment f.offset ->
100116
FieldsAligned rest ->
101117
FieldsAligned (f :: rest)
102118

103119
||| Verify a struct layout is valid
104120
public export
105-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
121+
verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
106122
verifyLayout fields align =
107-
let size = calcStructSize fields align
108-
in case decSo (size >= sum (map (\f => f.size) fields)) of
109-
Yes prf => Right (MkStructLayout fields size align)
110-
No _ => Left "Invalid struct size"
123+
let size = calcStructSize fields align in
124+
case choose (size >= sum (map (\f => f.size) fields)) of
125+
Right _ => Left "Invalid struct size"
126+
Left sizeOk =>
127+
case decDivides align size of
128+
Nothing => Left "Total size is not a multiple of the alignment"
129+
Just alignProof =>
130+
Right (MkStructLayout fields size align
131+
{sizeCorrect = sizeOk} {aligned = alignProof})
111132

112133
--------------------------------------------------------------------------------
113134
-- Nim Object Layout Rules
@@ -148,7 +169,7 @@ nimFieldAlign p ty = min (nimFieldSize p ty) (ptrSize p `div` 8)
148169
||| Convert a NimObject to a StructLayout using exportc rules
149170
||| (C-compatible: declaration order, natural alignment, trailing padding)
150171
public export
151-
nimObjectToLayout : Platform -> NimObject -> Either String StructLayout
172+
nimObjectToLayout : Platform -> NimObjectDef -> Either String StructLayout
152173
nimObjectToLayout p obj =
153174
let fields = computeFields p 0 obj.fields
154175
in verifyLayout (fromList fields) (maxAlign p obj.fields)
@@ -200,10 +221,25 @@ data CABICompliant : StructLayout -> Type where
200221
FieldsAligned layout.fields ->
201222
CABICompliant layout
202223

224+
||| Decide whether every field's offset is aligned to its alignment.
225+
public export
226+
decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields)
227+
decFieldsAligned [] = Just NoFields
228+
decFieldsAligned (f :: fs) =
229+
case decDivides f.alignment f.offset of
230+
Nothing => Nothing
231+
Just dv =>
232+
case decFieldsAligned fs of
233+
Nothing => Nothing
234+
Just rest => Just (ConsField f fs dv rest)
235+
203236
||| Check if layout follows C ABI
204237
public export
205238
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
206-
checkCABI layout = Right (CABIOk layout ?fieldsAlignedProof)
239+
checkCABI layout =
240+
case decFieldsAligned layout.fields of
241+
Just prf => Right (CABIOk layout prf)
242+
Nothing => Left "Struct fields are not correctly aligned for C ABI"
207243

208244
--------------------------------------------------------------------------------
209245
-- Nim-Specific Layout Examples
@@ -224,6 +260,8 @@ nimBufferLayout =
224260
]
225261
16 -- Total size: 16 bytes
226262
8 -- Alignment: 8 bytes (pointer)
263+
{sizeCorrect = Oh}
264+
{aligned = DivideBy 2 Refl}
227265

228266
||| Example: Nim object with default alignment
229267
||| type NimResult {.exportc: "nimiser_result".} = object
@@ -239,16 +277,25 @@ nimResultLayout =
239277
]
240278
16 -- Total size: 16 bytes
241279
8 -- Alignment: 8 bytes
280+
{sizeCorrect = Oh}
281+
{aligned = DivideBy 2 Refl}
242282

243283
||| Proof that buffer layout is valid
244284
export
245-
nimBufferLayoutValid : CABICompliant nimBufferLayout
246-
nimBufferLayoutValid = CABIOk nimBufferLayout ?bufferFieldsAligned
285+
nimBufferLayoutValid : CABICompliant Layout.nimBufferLayout
286+
nimBufferLayoutValid =
287+
CABIOk nimBufferLayout
288+
(ConsField _ _ (DivideBy 0 Refl)
289+
(ConsField _ _ (DivideBy 2 Refl)
290+
(ConsField _ _ (DivideBy 3 Refl) NoFields)))
247291

248292
||| Proof that result layout is valid
249293
export
250-
nimResultLayoutValid : CABICompliant nimResultLayout
251-
nimResultLayoutValid = CABIOk nimResultLayout ?resultFieldsAligned
294+
nimResultLayoutValid : CABICompliant Layout.nimResultLayout
295+
nimResultLayoutValid =
296+
CABIOk nimResultLayout
297+
(ConsField _ _ (DivideBy 0 Refl)
298+
(ConsField _ _ (DivideBy 1 Refl) NoFields))
252299

253300
--------------------------------------------------------------------------------
254301
-- Offset Calculation
@@ -262,7 +309,11 @@ fieldOffset layout name =
262309
Just idx => Just (finToNat idx ** index idx layout.fields)
263310
Nothing => Nothing
264311

265-
||| Proof that field offset is within struct bounds
312+
||| Decide whether a field's offset is within struct bounds.
313+
||| In general a field may exceed the struct, so the result is a Maybe witness.
266314
public export
267-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
268-
offsetInBounds layout f = ?offsetInBoundsProof
315+
offsetInBounds : (layout : StructLayout) -> (f : Field) -> Maybe (So (f.offset + f.size <= layout.totalSize))
316+
offsetInBounds layout f =
317+
case choose (f.offset + f.size <= layout.totalSize) of
318+
Left ok => Just ok
319+
Right _ => Nothing

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

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
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 for the Nimiser ABI.
5+
|||
6+
||| Each concrete `StructLayout` value is proven `CABICompliant` by building
7+
||| the `FieldsAligned` witness directly (one `DivideBy` per field, where the
8+
||| field offset equals `k * alignment`). Multiplication reduces during
9+
||| typechecking; division does not — so these witnesses are built by hand
10+
||| rather than via `decFieldsAligned`.
11+
12+
module Nimiser.ABI.Proofs
13+
14+
import Nimiser.ABI.Types
15+
import Nimiser.ABI.Layout
16+
import Data.Vect
17+
18+
%default total
19+
20+
--------------------------------------------------------------------------------
21+
-- C-ABI compliance of the concrete struct layouts
22+
--------------------------------------------------------------------------------
23+
24+
||| The `nimiser_buffer` layout is C-ABI compliant.
25+
||| Fields: data @0 align 8 (0 = 0*8), len @8 align 4 (8 = 2*4),
26+
||| cap @12 align 4 (12 = 3*4).
27+
export
28+
nimBufferCompliant : CABICompliant Layout.nimBufferLayout
29+
nimBufferCompliant =
30+
CABIOk nimBufferLayout
31+
(ConsField _ _ (DivideBy 0 Refl)
32+
(ConsField _ _ (DivideBy 2 Refl)
33+
(ConsField _ _ (DivideBy 3 Refl) NoFields)))
34+
35+
||| The `nimiser_result` layout is C-ABI compliant.
36+
||| Fields: code @0 align 4 (0 = 0*4), message @8 align 8 (8 = 1*8).
37+
export
38+
nimResultCompliant : CABICompliant Layout.nimResultLayout
39+
nimResultCompliant =
40+
CABIOk nimResultLayout
41+
(ConsField _ _ (DivideBy 0 Refl)
42+
(ConsField _ _ (DivideBy 1 Refl) NoFields))
43+
44+
--------------------------------------------------------------------------------
45+
-- Result-code encoding facts
46+
--------------------------------------------------------------------------------
47+
48+
||| The success result encodes to the C integer 0.
49+
export
50+
okIsZero : resultToInt Ok = 0
51+
okIsZero = Refl
52+
53+
||| The null-pointer result encodes to the C integer 4 (a nontrivial, distinct
54+
||| code in the middle of the enumeration).
55+
export
56+
nullPointerIsFour : resultToInt NullPointer = 4
57+
nullPointerIsFour = Refl
58+
59+
||| The result encoding is injective on the two error codes we pin here:
60+
||| distinct constructors map to distinct integers, witnessed structurally.
61+
export
62+
okDistinctFromError : Not (resultToInt Ok = resultToInt Error)
63+
okDistinctFromError = \case Refl impossible

0 commit comments

Comments
 (0)