Skip to content

Commit 7ba8cc7

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#38)
* 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(abi): make Idris2 ABI proofs genuinely compile and verify under 0.7.0 The src/interface/abi/{Types,Layout,Foreign}.idr files were scaffolded from a template and never compiler-checked. This commit makes the whole ABI package typecheck cleanly (zero errors, zero warnings) under Idris2 0.7.0 and adds a module of machine-checked theorems. Buildability: - Moved flat Types/Layout/Foreign.idr into the nested Julianiser/ABI/ namespace so file paths match module names. - Added src/interface/abi/julianiser-abi.ipkg listing the four ABI modules. Type/Layout/Foreign fixes: - thisPlatform: replaced the %runElab stub (needs ElabReflection) with Linux. - DecEq SourceLanguage / Result: replaced the non-compiling `decEq _ _ = No absurd` catch-alls with explicit off-diagonal `No (\case Refl impossible)`. - DecEq JuliaType: implemented a genuine structural decision procedure as a mutual block (decEqJT / decEqJTVect) handling the parametric constructors (JArray, JTuple, JDict, JUnion) and all off-diagonal pairs; the vector helper decides heterogeneous equality so it never needs the erased length at runtime. - createHandle: used `choose (ptr /= 0)` to supply the `So (ptr /= 0)` auto proof for MkHandle instead of leaving it unsolved. - Layout.paddingFor: replaced `alignment - …` (Nat has no Neg) with `minus`. - Added a sound `decDivides` decision procedure; replaced the unprovable `alignUpCorrect … = DivideBy … Refl` with the deciding `alignUpDivides`. - Concrete StructLayouts (astNode/translationRecord/benchmarkResult) now supply their erased proofs explicitly ({sizeCorrect = Oh}, {aligned = DivideBy k Refl}). - Added decFieldsAligned + checkCABI building real FieldsAligned witnesses. - verifyLayout now discharges both MkStructLayout obligations (size via choose, divisibility via decDivides) instead of omitting the `aligned` proof. - offsetInBounds: changed the unsound universal `So (...)` return into `Maybe (So (...))` decided via choose (filled the `?offsetInBoundsProof` hole). - Foreign: scoped prim__getString as a where-local `Bits64 -> String` at each use site (matching the reference solution) and hoisted prim__freeString. New theorems (src/interface/abi/Julianiser/ABI/Proofs.idr): - astNodeCompliant, translationRecordCompliant, benchmarkResultCompliant: CABICompliant witnesses built directly from per-field DivideBy proofs. - okIsZero, parseErrorIsFive, codegenErrorIsSix: pin the result-code encoding. - remapIsSucc, remapZeroIsOne: pin the Python-0-based to Julia-1-based remap. No believe_me / assert_total / idris_crash / postulate / %hint / holes are used. Added **/build/, *.ttc, *.ttm to .gitignore; build artifacts are not committed. 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 4c7f468 commit 7ba8cc7

7 files changed

Lines changed: 698 additions & 328 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 ABI proof 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/Julianiser/ABI/Foreign.idr

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,11 @@ export
4545
free : Handle -> IO ()
4646
free h = primIO (prim__free (handlePtr h))
4747

48+
||| Free a C string allocated by julianiser (shared infrastructure).
49+
export
50+
%foreign "C:julianiser_free_string, libjulianiser"
51+
prim__freeString : Bits64 -> PrimIO ()
52+
4853
--------------------------------------------------------------------------------
4954
-- Source Parsing
5055
--------------------------------------------------------------------------------
@@ -154,6 +159,9 @@ getJuliaCode h = do
154159
let str = prim__getString ptr
155160
primIO (prim__freeString ptr)
156161
pure (Just str)
162+
where
163+
%foreign "support:idris2_getString, libidris2_support"
164+
prim__getString : Bits64 -> String
157165

158166
--------------------------------------------------------------------------------
159167
-- Benchmark Operations
@@ -186,20 +194,6 @@ export
186194
getSpeedup : Handle -> IO Double
187195
getSpeedup h = primIO (prim__getSpeedup (handlePtr h))
188196

189-
--------------------------------------------------------------------------------
190-
-- String Operations (shared infrastructure)
191-
--------------------------------------------------------------------------------
192-
193-
||| Convert C string to Idris String
194-
export
195-
%foreign "support:idris2_getString, libidris2_support"
196-
prim__getString : Bits64 -> String
197-
198-
||| Free C string allocated by julianiser
199-
export
200-
%foreign "C:julianiser_free_string, libjulianiser"
201-
prim__freeString : Bits64 -> PrimIO ()
202-
203197
--------------------------------------------------------------------------------
204198
-- Error Handling
205199
--------------------------------------------------------------------------------
@@ -217,6 +211,9 @@ lastError = do
217211
if ptr == 0
218212
then pure Nothing
219213
else pure (Just (prim__getString ptr))
214+
where
215+
%foreign "support:idris2_getString, libidris2_support"
216+
prim__getString : Bits64 -> String
220217

221218
||| Get error description for result code
222219
export
@@ -244,6 +241,9 @@ version : IO String
244241
version = do
245242
ptr <- primIO prim__version
246243
pure (prim__getString ptr)
244+
where
245+
%foreign "support:idris2_getString, libidris2_support"
246+
prim__getString : Bits64 -> String
247247

248248
--------------------------------------------------------------------------------
249249
-- Utility Functions

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

Lines changed: 78 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ module Julianiser.ABI.Layout
1414
import Julianiser.ABI.Types
1515
import Data.Vect
1616
import Data.So
17+
import Data.Nat
18+
import Decidable.Equality
1719

1820
%default total
1921

@@ -27,24 +29,40 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
2729
paddingFor offset alignment =
2830
if offset `mod` alignment == 0
2931
then 0
30-
else alignment - (offset `mod` alignment)
32+
else minus alignment (offset `mod` alignment)
3133

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

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

43-
||| Proof that alignUp produces aligned result
57+
||| Sound divisibility check for an aligned size. The general theorem
58+
||| "alignUp size align is always divisible by align" needs div/mod lemmas
59+
||| from Data.Nat; here we *decide* it via `decDivides`, which returns a
60+
||| genuine witness when it holds. (Previously `alignUpCorrect … = DivideBy …
61+
||| Refl`, whose `Refl` cannot typecheck for symbolic inputs.)
4462
public export
45-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
46-
alignUpCorrect size align prf =
47-
DivideBy ((size + paddingFor size align) `div` align) Refl
63+
alignUpDivides : (size : Nat) -> (align : Nat) ->
64+
Maybe (Divides align (alignUp size align))
65+
alignUpDivides size align = decDivides align (alignUp size align)
4866

4967
--------------------------------------------------------------------------------
5068
-- Struct Field Layout
@@ -100,6 +118,8 @@ astNodeLayout =
100118
]
101119
32 -- Total size: 32 bytes
102120
8 -- Alignment: 8 bytes
121+
{sizeCorrect = Oh}
122+
{aligned = DivideBy 4 Refl} -- 32 = 4 * 8
103123

104124
--------------------------------------------------------------------------------
105125
-- Translation Record Layout
@@ -123,6 +143,8 @@ translationRecordLayout =
123143
]
124144
24 -- Total size: 24 bytes
125145
8 -- Alignment: 8 bytes
146+
{sizeCorrect = Oh}
147+
{aligned = DivideBy 3 Refl} -- 24 = 3 * 8
126148

127149
--------------------------------------------------------------------------------
128150
-- Benchmark Result Layout
@@ -152,22 +174,36 @@ benchmarkResultLayout =
152174
]
153175
40 -- Total size: 40 bytes
154176
8 -- Alignment: 8 bytes
177+
{sizeCorrect = Oh}
178+
{aligned = DivideBy 5 Refl} -- 40 = 5 * 8
155179

156180
--------------------------------------------------------------------------------
157181
-- Layout Verification
158182
--------------------------------------------------------------------------------
159183

160184
||| Proof that field offsets are correctly aligned
161185
public export
162-
data FieldsAligned : Vect n Field -> Type where
186+
data FieldsAligned : Vect k Field -> Type where
163187
NoFields : FieldsAligned []
164188
ConsField :
165189
(f : Field) ->
166-
(rest : Vect n Field) ->
190+
(rest : Vect k Field) ->
167191
Divides f.alignment f.offset ->
168192
FieldsAligned rest ->
169193
FieldsAligned (f :: rest)
170194

195+
||| Decide field alignment for every field, building a real `FieldsAligned`
196+
||| witness from per-field divisibility proofs.
197+
public export
198+
decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs)
199+
decFieldsAligned [] = Just NoFields
200+
decFieldsAligned (f :: fs) =
201+
case decDivides f.alignment f.offset of
202+
Nothing => Nothing
203+
Just dvd => case decFieldsAligned fs of
204+
Nothing => Nothing
205+
Just rest => Just (ConsField f fs dvd rest)
206+
171207
||| Proof that a struct follows C ABI rules
172208
public export
173209
data CABICompliant : StructLayout -> Type where
@@ -176,23 +212,39 @@ data CABICompliant : StructLayout -> Type where
176212
FieldsAligned layout.fields ->
177213
CABICompliant layout
178214

215+
||| Verify a layout against the C ABI alignment rules, returning a genuine
216+
||| `CABICompliant` proof (built from real per-field divisibility witnesses)
217+
||| or an error when some field offset is misaligned.
218+
public export
219+
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
220+
checkCABI layout =
221+
case decFieldsAligned layout.fields of
222+
Just prf => Right (CABIOk layout prf)
223+
Nothing => Left "Field offsets are not correctly aligned for the C ABI"
224+
179225
||| Calculate total struct size with padding
180226
public export
181-
calcStructSize : Vect n Field -> Nat -> Nat
227+
calcStructSize : Vect k Field -> Nat -> Nat
182228
calcStructSize [] align = 0
183229
calcStructSize (f :: fs) align =
184230
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
185231
lastSize = foldr (\field, _ => field.size) f.size fs
186232
in alignUp (lastOffset + lastSize) align
187233

188-
||| Verify a struct layout is valid
234+
||| Verify a struct layout is valid. Both erased proof obligations on
235+
||| `MkStructLayout` are discharged with genuine witnesses: the size bound via
236+
||| `choose`, and divisibility via `decDivides`. Returns Left when either fails.
237+
||| (Previously it constructed `MkStructLayout` without supplying the `aligned`
238+
||| proof, which did not typecheck.)
189239
public export
190-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
240+
verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
191241
verifyLayout fields align =
192-
let size = calcStructSize fields align
193-
in case decSo (size >= sum (map (\f => f.size) fields)) of
194-
Yes prf => Right (MkStructLayout fields size align)
195-
No _ => Left "Invalid struct size"
242+
let size = calcStructSize fields align in
243+
case choose (size >= sum (map (\f => f.size) fields)) of
244+
Left szOk => case decDivides align size of
245+
Just algn => Right (MkStructLayout fields size align {sizeCorrect = szOk} {aligned = algn})
246+
Nothing => Left "Total size is not a multiple of alignment"
247+
Right _ => Left "Invalid struct size"
196248

197249
--------------------------------------------------------------------------------
198250
-- Platform-Specific Layouts
@@ -222,7 +274,15 @@ fieldOffset layout name =
222274
Just idx => Just (finToNat idx ** index idx layout.fields)
223275
Nothing => Nothing
224276

225-
||| Proof that field offset is within struct bounds
277+
||| Decide whether a field lies within a struct's byte bounds, returning a
278+
||| genuine proof when `offset + size <= totalSize`. The previous signature
279+
||| asserted this for *every* field unconditionally (returning a bare `So`),
280+
||| which is false (a field need not belong to the layout) and left an
281+
||| unsolved hole; this honest version decides it via `choose`.
226282
public export
227-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
228-
offsetInBounds layout f = ?offsetInBoundsProof
283+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
284+
Maybe (So (f.offset + f.size <= layout.totalSize))
285+
offsetInBounds layout f =
286+
case choose (f.offset + f.size <= layout.totalSize) of
287+
Left ok => Just ok
288+
Right _ => Nothing

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

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
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 julianiser 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 an index-remapping
9+
||| relation mis-defined, this module would fail to typecheck and the proof
10+
||| build would 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
15+
||| by the compiler; we deliberately avoid routing them through `Nat`
16+
||| division, which is a primitive that does not reduce at the type level.
17+
18+
module Julianiser.ABI.Proofs
19+
20+
import Julianiser.ABI.Types
21+
import Julianiser.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 AST-node layout divides its alignment:
32+
||| 0|4, 4|4, 8|8, 16|4, 20|4, 24|8.
33+
export
34+
astNodeCompliant : CABICompliant Layout.astNodeLayout
35+
astNodeCompliant =
36+
CABIOk astNodeLayout
37+
(ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 4
38+
(ConsField _ _ (DivideBy 1 Refl) -- offset 4 = 1 * 4
39+
(ConsField _ _ (DivideBy 1 Refl) -- offset 8 = 1 * 8
40+
(ConsField _ _ (DivideBy 4 Refl) -- offset 16 = 4 * 4
41+
(ConsField _ _ (DivideBy 5 Refl) -- offset 20 = 5 * 4
42+
(ConsField _ _ (DivideBy 3 Refl) -- offset 24 = 3 * 8
43+
NoFields))))))
44+
45+
||| Every field offset in the translation-record layout divides its alignment:
46+
||| 0|8, 8|8, 16|4, 20|4.
47+
export
48+
translationRecordCompliant : CABICompliant Layout.translationRecordLayout
49+
translationRecordCompliant =
50+
CABIOk translationRecordLayout
51+
(ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 8
52+
(ConsField _ _ (DivideBy 1 Refl) -- offset 8 = 1 * 8
53+
(ConsField _ _ (DivideBy 4 Refl) -- offset 16 = 4 * 4
54+
(ConsField _ _ (DivideBy 5 Refl) -- offset 20 = 5 * 4
55+
NoFields))))
56+
57+
||| Every field offset in the benchmark-result layout divides its alignment:
58+
||| 0|8, 8|8, 16|8, 24|4, 28|4, 32|4, 36|4.
59+
export
60+
benchmarkResultCompliant : CABICompliant Layout.benchmarkResultLayout
61+
benchmarkResultCompliant =
62+
CABIOk benchmarkResultLayout
63+
(ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 8
64+
(ConsField _ _ (DivideBy 1 Refl) -- offset 8 = 1 * 8
65+
(ConsField _ _ (DivideBy 2 Refl) -- offset 16 = 2 * 8
66+
(ConsField _ _ (DivideBy 6 Refl) -- offset 24 = 6 * 4
67+
(ConsField _ _ (DivideBy 7 Refl) -- offset 28 = 7 * 4
68+
(ConsField _ _ (DivideBy 8 Refl) -- offset 32 = 8 * 4
69+
(ConsField _ _ (DivideBy 9 Refl) -- offset 36 = 9 * 4
70+
NoFields)))))))
71+
72+
--------------------------------------------------------------------------------
73+
-- Result-code round-trip: the encoding the Zig FFI depends on.
74+
--------------------------------------------------------------------------------
75+
76+
||| `Ok` encodes to 0 — the success sentinel the FFI wrappers branch on.
77+
export
78+
okIsZero : resultToInt Ok = 0
79+
okIsZero = Refl
80+
81+
||| `ParseError` encodes to 5 — matched explicitly in `parsePython`/`parseR`.
82+
export
83+
parseErrorIsFive : resultToInt ParseError = 5
84+
parseErrorIsFive = Refl
85+
86+
||| `CodegenError` encodes to 6 — matched explicitly in `codegen`.
87+
export
88+
codegenErrorIsSix : resultToInt CodegenError = 6
89+
codegenErrorIsSix = Refl
90+
91+
--------------------------------------------------------------------------------
92+
-- Index remapping: Python 0-based -> Julia 1-based is the successor relation.
93+
--------------------------------------------------------------------------------
94+
95+
||| The remap of any Python index `n` is `S n` (1-based), carrying a genuine
96+
||| `IndexRemapCorrect` witness. This pins the slicing-correctness contract.
97+
export
98+
remapIsSucc : (n : Nat) -> fst (remapIndex n) = S n
99+
remapIsSucc n = Refl
100+
101+
||| Concretely: Python index 0 maps to Julia index 1.
102+
export
103+
remapZeroIsOne : fst (remapIndex 0) = 1
104+
remapZeroIsOne = Refl

0 commit comments

Comments
 (0)