Skip to content

Commit 8d1c48e

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#31)
* 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 so they genuinely compile and verify The src/interface/abi ABI files were scaffolded from a template and never compiler-checked. This makes the whole ABI build clean under Idris2 0.7.0 (idris2 --build otpiser-abi.ipkg: zero errors, zero warnings) with genuine proofs throughout (no believe_me/assert/postulate/holes). Types.idr: - Replace the non-compiling `decEq _ _ = No absurd` catch-alls with explicit off-diagonal cases (No (\case Refl impossible)) for SupervisorStrategy and the 7-constructor Result enum; add `import Decidable.Equality`. - Fix createHandle smart constructor to discharge the {auto 0 nonNull} proof via `choose (ptr /= 0)`. - Replace `thisPlatform = %runElab ...` (needs ElabReflection) with a plain value (Linux). - Reorder ChildType before ChildSpec (use-before-definition). - Fix HasWorkers.HasChildWorker unbindable implicit by naming the tail vector. - Fix CPtr: `Bits (ptrSize p)` is ill-typed (Bits is an interface); map each platform to a concrete pointer-width integer type. - Make treeSize/workerCount/treeDepth pass totality with explicit structural folds over the child Vect (recursion through `map` was not seen as total). Layout.idr: - paddingFor: replace `alignment - (...)` (Nat has no Neg) with `minus`; import Data.Nat. - Add sound `decDivides`/`decFieldsAligned` decision procedures; rewrite `checkCABI` to use them instead of a `?fieldsAlignedProof` hole. - Make `alignUpDivides`/`verifyLayout` discharge the StructLayout obligations via `choose` + `decDivides` (division never reduces under Refl). - Supply concrete StructLayout proofs explicitly: {sizeCorrect = Oh} and {aligned = DivideBy k Refl}. - offsetInBounds: change the unsound universally-quantified `So (...)` to a decidable `Maybe (So (...))` via `choose`. - Rename shadowing implicit `n` bindings to `k`. Foreign.idr: - Move the prim__getString foreign declaration above its first use so its `Bits64 -> String` type is in scope (forward ref was resolving to the support `Ptr String` variant and failing to unify). Proofs.idr (new): machine-checked theorems — - supervisorNodeCompliant / childSpecCompliant / genServerCallbackCompliant: direct FieldsAligned witnesses (one DivideBy per field) proving each concrete layout is C-ABI compliant. - okIsZero, nullPointerIsFour, okDistinctFromMalformed: pin the Result wire encoding; strategyEncodingRoundTrips re-exports the round-trip theorem. Buildability: move flat files to Otpiser/ABI/ nested layout; add otpiser-abi.ipkg; ignore Idris build artefacts (**/build/, *.ttc, *.ttm). 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 a54e3e7 commit 8d1c48e

6 files changed

Lines changed: 298 additions & 56 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 build artefacts
22+
**/build/
23+
*.ttc
24+
*.ttm
25+
2126
# Dependencies
2227
/node_modules/
2328
/vendor/

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

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,18 @@ import Otpiser.ABI.Layout
1717

1818
%default total
1919

20+
--------------------------------------------------------------------------------
21+
-- String Operations (shared FFI utilities)
22+
--------------------------------------------------------------------------------
23+
-- Declared first so its type is in scope for every use below. Without this,
24+
-- a forward reference lets the elaborator pick up the support `Ptr String`
25+
-- variant and the call sites fail to unify against our `Bits64` pointers.
26+
27+
||| Convert C string to Idris String
28+
export
29+
%foreign "support:idris2_getString, libidris2_support"
30+
prim__getString : Bits64 -> String
31+
2032
--------------------------------------------------------------------------------
2133
-- Library Lifecycle
2234
--------------------------------------------------------------------------------
@@ -236,11 +248,8 @@ prim__serializedSize : Bits64 -> Bits64 -> PrimIO Bits32
236248
--------------------------------------------------------------------------------
237249
-- String Operations (shared FFI utilities)
238250
--------------------------------------------------------------------------------
239-
240-
||| Convert C string to Idris String
241-
export
242-
%foreign "support:idris2_getString, libidris2_support"
243-
prim__getString : Bits64 -> String
251+
-- (prim__getString is declared near the top of this module so its type is in
252+
-- scope for all callers above.)
244253

245254
||| Free C string allocated by otpiser
246255
export

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

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

1921
%default total
2022

@@ -28,24 +30,41 @@ 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
3537
data Divides : Nat -> Nat -> Type where
3638
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
3739

40+
||| Sound decision procedure for divisibility.
41+
||| Returns a genuine `Divides d v` witness when `d` divides `v`, else Nothing.
42+
||| For `d = S j`, compute the candidate quotient `q = v `div` (S j)` and check
43+
||| `v = q * (S j)` decidably; the equality proof IS the divisibility witness.
44+
||| Division never reduces under Refl, so we go through `decEq`, never a hole.
45+
public export
46+
decDivides : (d : Nat) -> (v : Nat) -> Maybe (Divides d v)
47+
decDivides Z _ = Nothing
48+
decDivides (S j) v =
49+
let q = v `div` (S j) in
50+
case decEq v (q * (S j)) of
51+
Yes prf => Just (DivideBy q prf)
52+
No _ => Nothing
53+
3854
||| Round up to next alignment boundary
3955
public export
4056
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4157
alignUp size alignment =
4258
size + paddingFor size alignment
4359

44-
||| Proof that alignUp produces aligned result
60+
||| Decision: is the rounded-up size actually a multiple of the alignment?
61+
||| `alignUp` uses `div`/`mod`, which do not reduce under `Refl`, so the
62+
||| divisibility witness is produced by the sound `decDivides` decision
63+
||| procedure rather than asserted. Returns Nothing only if the (decidable)
64+
||| check fails for the given inputs.
4565
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
66+
alignUpDivides : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align))
67+
alignUpDivides size align = decDivides align (alignUp size align)
4968

5069
--------------------------------------------------------------------------------
5170
-- Struct Field Layout
@@ -77,7 +96,7 @@ record StructLayout where
7796

7897
||| Calculate total struct size with padding
7998
public export
80-
calcStructSize : Vect n Field -> Nat -> Nat
99+
calcStructSize : Vect k Field -> Nat -> Nat
81100
calcStructSize [] align = 0
82101
calcStructSize (f :: fs) align =
83102
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -86,23 +105,30 @@ calcStructSize (f :: fs) align =
86105

87106
||| Proof that field offsets are correctly aligned
88107
public export
89-
data FieldsAligned : Vect n Field -> Type where
108+
data FieldsAligned : Vect k Field -> Type where
90109
NoFields : FieldsAligned []
91110
ConsField :
92111
(f : Field) ->
93-
(rest : Vect n Field) ->
112+
(rest : Vect k Field) ->
94113
Divides f.alignment f.offset ->
95114
FieldsAligned rest ->
96115
FieldsAligned (f :: rest)
97116

98-
||| Verify a struct layout is valid
117+
||| Verify a struct layout is valid.
118+
||| Both record obligations are discharged by sound decisions: `choose` for the
119+
||| size bound (`So`) and `decDivides` for the alignment witness. No assertions.
99120
public export
100-
verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
121+
verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
101122
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"
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 alignment"
129+
Just alignProof =>
130+
Right (MkStructLayout fields size align
131+
{sizeCorrect = sizeOk} {aligned = alignProof})
106132

107133
--------------------------------------------------------------------------------
108134
-- Supervision Tree Node Layout
@@ -133,6 +159,8 @@ supervisorNodeLayout =
133159
]
134160
32 -- Total size: 32 bytes
135161
8 -- Alignment: 8 bytes
162+
{sizeCorrect = Oh}
163+
{aligned = DivideBy 4 Refl} -- 32 = 4 * 8
136164

137165
||| Layout of a serialised ChildSpec for FFI transport.
138166
|||
@@ -157,6 +185,8 @@ childSpecLayout =
157185
]
158186
32 -- Total size: 32 bytes
159187
8 -- Alignment: 8 bytes
188+
{sizeCorrect = Oh}
189+
{aligned = DivideBy 4 Refl} -- 32 = 4 * 8
160190

161191
||| Layout of a GenServerCallback specification for FFI transport.
162192
|||
@@ -185,6 +215,8 @@ genServerCallbackLayout =
185215
]
186216
40 -- Total size: 40 bytes
187217
8 -- Alignment: 8 bytes
218+
{sizeCorrect = Oh}
219+
{aligned = DivideBy 5 Refl} -- 40 = 5 * 8
188220

189221
--------------------------------------------------------------------------------
190222
-- Platform-Specific Layouts
@@ -215,21 +247,25 @@ data CABICompliant : StructLayout -> Type where
215247
FieldsAligned layout.fields ->
216248
CABICompliant layout
217249

218-
||| Check if layout follows C ABI
250+
||| Decide alignment of every field in a vector, building a FieldsAligned witness.
251+
public export
252+
decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields)
253+
decFieldsAligned [] = Just NoFields
254+
decFieldsAligned (f :: fs) =
255+
case decDivides f.alignment f.offset of
256+
Nothing => Nothing
257+
Just dv =>
258+
case decFieldsAligned fs of
259+
Nothing => Nothing
260+
Just rest => Just (ConsField f fs dv rest)
261+
262+
||| Check if layout follows C ABI by deciding field alignment soundly.
219263
public export
220264
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
221265
checkCABI layout =
222-
Right (CABIOk layout ?fieldsAlignedProof)
223-
224-
||| Proof that supervisor node layout is C ABI compliant
225-
export
226-
supervisorNodeCABI : CABICompliant supervisorNodeLayout
227-
supervisorNodeCABI = CABIOk supervisorNodeLayout ?supervisorFieldsAligned
228-
229-
||| Proof that child spec layout is C ABI compliant
230-
export
231-
childSpecCABI : CABICompliant childSpecLayout
232-
childSpecCABI = CABIOk childSpecLayout ?childSpecFieldsAligned
266+
case decFieldsAligned layout.fields of
267+
Just prf => Right (CABIOk layout prf)
268+
Nothing => Left "Struct fields are not C-ABI aligned"
233269

234270
--------------------------------------------------------------------------------
235271
-- Offset Calculation
@@ -243,7 +279,12 @@ fieldOffset layout name =
243279
Just idx => Just (finToNat idx ** index idx layout.fields)
244280
Nothing => Nothing
245281

246-
||| Proof that field offset is within struct bounds
282+
||| Decide whether a field lies within the struct's total size.
283+
||| This is genuinely partial (a field may lie outside an arbitrary layout),
284+
||| so it returns `Maybe` of the bound proof rather than asserting it.
247285
public export
248-
offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
249-
offsetInBounds layout f = ?offsetInBoundsProof
286+
offsetInBounds : (layout : StructLayout) -> (f : Field) -> Maybe (So (f.offset + f.size <= layout.totalSize))
287+
offsetInBounds layout f =
288+
case choose (f.offset + f.size <= layout.totalSize) of
289+
Left ok => Just ok
290+
Right _ => Nothing

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

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
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 ABI Theorems for Otpiser
5+
|||
6+
||| This module collects the genuine, compiler-verified theorems about the
7+
||| Otpiser C-ABI surface. Each `*Compliant` theorem exhibits a DIRECT
8+
||| `FieldsAligned` witness for a concrete `StructLayout`: one `DivideBy`
9+
||| per field, where `field.offset = k * field.alignment`. Multiplication
10+
||| reduces during type-checking (so `Refl` discharges each equation), whereas
11+
||| division does NOT — hence these witnesses are built by hand rather than via
12+
||| the `decFieldsAligned` decision procedure.
13+
|||
14+
||| The result-code lemmas pin the wire encoding of the FFI `Result` enum.
15+
|||
16+
||| @see Otpiser.ABI.Layout for the layouts and the `CABICompliant` relation
17+
||| @see Otpiser.ABI.Types for the `Result` encoding
18+
19+
module Otpiser.ABI.Proofs
20+
21+
import Otpiser.ABI.Types
22+
import Otpiser.ABI.Layout
23+
import Data.Vect
24+
25+
%default total
26+
27+
--------------------------------------------------------------------------------
28+
-- C-ABI compliance of the concrete struct layouts
29+
--------------------------------------------------------------------------------
30+
31+
||| The serialised supervisor-node layout is C-ABI compliant: every field's
32+
||| offset is an exact multiple of its alignment.
33+
||| nodeType@0/4, strategy@4/4, maxRestarts@8/4, maxSeconds@12/4,
34+
||| childCount@16/4, nameLen@20/4, namePtr@24/8.
35+
export
36+
supervisorNodeCompliant : CABICompliant Layout.supervisorNodeLayout
37+
supervisorNodeCompliant =
38+
CABIOk Layout.supervisorNodeLayout
39+
(ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 4
40+
(ConsField _ _ (DivideBy 1 Refl) -- offset 4 = 1 * 4
41+
(ConsField _ _ (DivideBy 2 Refl) -- offset 8 = 2 * 4
42+
(ConsField _ _ (DivideBy 3 Refl) -- offset 12 = 3 * 4
43+
(ConsField _ _ (DivideBy 4 Refl) -- offset 16 = 4 * 4
44+
(ConsField _ _ (DivideBy 5 Refl) -- offset 20 = 5 * 4
45+
(ConsField _ _ (DivideBy 3 Refl) -- offset 24 = 3 * 8
46+
NoFields)))))))
47+
48+
||| The serialised child-spec layout is C-ABI compliant.
49+
||| childIdLen@0/4, restartType@4/4, shutdownMs@8/4, childType@12/4,
50+
||| childIdPtr@16/8, modulePtr@24/8.
51+
export
52+
childSpecCompliant : CABICompliant Layout.childSpecLayout
53+
childSpecCompliant =
54+
CABIOk Layout.childSpecLayout
55+
(ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 4
56+
(ConsField _ _ (DivideBy 1 Refl) -- offset 4 = 1 * 4
57+
(ConsField _ _ (DivideBy 2 Refl) -- offset 8 = 2 * 4
58+
(ConsField _ _ (DivideBy 3 Refl) -- offset 12 = 3 * 4
59+
(ConsField _ _ (DivideBy 2 Refl) -- offset 16 = 2 * 8
60+
(ConsField _ _ (DivideBy 3 Refl) -- offset 24 = 3 * 8
61+
NoFields))))))
62+
63+
||| The serialised GenServer-callback layout is C-ABI compliant.
64+
||| moduleNameLen@0/4, stateTypeLen@4/4, callTypeCount@8/4, castTypeCount@12/4,
65+
||| infoTypeCount@16/4, padding@20/4, moduleNamePtr@24/8, stateTypePtr@32/8.
66+
export
67+
genServerCallbackCompliant : CABICompliant Layout.genServerCallbackLayout
68+
genServerCallbackCompliant =
69+
CABIOk Layout.genServerCallbackLayout
70+
(ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 4
71+
(ConsField _ _ (DivideBy 1 Refl) -- offset 4 = 1 * 4
72+
(ConsField _ _ (DivideBy 2 Refl) -- offset 8 = 2 * 4
73+
(ConsField _ _ (DivideBy 3 Refl) -- offset 12 = 3 * 4
74+
(ConsField _ _ (DivideBy 4 Refl) -- offset 16 = 4 * 4
75+
(ConsField _ _ (DivideBy 5 Refl) -- offset 20 = 5 * 4
76+
(ConsField _ _ (DivideBy 3 Refl) -- offset 24 = 3 * 8
77+
(ConsField _ _ (DivideBy 4 Refl) -- offset 32 = 4 * 8
78+
NoFields))))))))
79+
80+
--------------------------------------------------------------------------------
81+
-- Result-code wire-encoding lemmas
82+
--------------------------------------------------------------------------------
83+
84+
||| The success code encodes to 0 (the C convention for "no error").
85+
export
86+
okIsZero : resultToInt Ok = 0
87+
okIsZero = Refl
88+
89+
||| The null-pointer error encodes to 4, distinct from success.
90+
export
91+
nullPointerIsFour : resultToInt NullPointer = 4
92+
nullPointerIsFour = Refl
93+
94+
||| Encoding is injective on the two endpoints we care about most: success and
95+
||| the malformed-tree error never collide. Pins that 0 /= 6 under the encoding.
96+
export
97+
okDistinctFromMalformed : Not (resultToInt Ok = resultToInt MalformedTree)
98+
okDistinctFromMalformed = \case Refl impossible
99+
100+
--------------------------------------------------------------------------------
101+
-- Supervision-strategy round-trip (re-export as a named theorem)
102+
--------------------------------------------------------------------------------
103+
104+
||| Strategy encode/decode is a genuine round trip for every strategy.
105+
export
106+
strategyEncodingRoundTrips :
107+
(s : SupervisorStrategy) -> intToStrategy (strategyToInt s) = Just s
108+
strategyEncodingRoundTrips = strategyRoundTrip

0 commit comments

Comments
 (0)