Skip to content

Commit 6c1a419

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#34)
* 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 makes them typecheck cleanly (zero errors, zero warnings) under Idris2 0.7.0 with real, non-faked proofs, and adds a machine-checked theorem module. Buildability: - Moved flat files into the Lustreiser.ABI namespace dir (src/interface/abi/Lustreiser/ABI/{Types,Layout,Foreign}.idr) so file paths match module namespaces. - Added src/interface/abi/lustreiser-abi.ipkg listing all four modules. Systemic fixes: - Types.thisPlatform: replaced the %runElab stub (needs ElabReflection) with a plain value (Linux). - DecEq TemporalOperator and DecEq Result: replaced the non-compiling `decEq _ _ = No absurd` catch-all with explicit off-diagonal cases `No (\case Refl impossible)` for every ordered pair of distinct constructors. - createHandle: replaced `Just (MkHandle ptr)` (unsolved `So (ptr /= 0)` auto proof) with a `choose`-based smart constructor supplying {nonNull = ok}. - Layout.paddingFor: `alignment - ...` (no Neg for Nat) -> `minus alignment ...`. - Added decDivides (sound Maybe (Divides n m) via div + decEq) and replaced the unprovable alignUpCorrect/Refl with alignUpDivides routed through decDivides. - checkCABI: implemented decFieldsAligned and removed the ?fieldsAlignedProof hole; returns a genuine CABICompliant witness or Left. - offsetInBounds: changed the unsound universally-true `So (...)` return type to `Maybe (So (...))` decided via choose. - Concrete StructLayout values (lustrePortLayout, lustreContextLayout) now supply their erased auto-implicit proofs explicitly ({sizeCorrect = Oh}, {aligned = DivideBy 4 Refl}; 32 = 4 * 8). - verifyLayout now discharges both erased obligations with real witnesses. - Lifted NodeLayout's invalid record `where` helper (totalBufferSize) to a top-level function. - Renamed shadowing Vect-length implicits to unique names to clear all "implicitly bind lowercase names" warnings. - Foreign: declared prim__getString locally per-function (where blocks) matching the working reference, fixing the Bits64/Ptr String unification error. Real theorems (src/interface/abi/Lustreiser/ABI/Proofs.idr): - lustrePortCompliant, lustreContextCompliant: CABICompliant proofs built directly from per-field DivideBy k Refl witnesses (offset = k * alignment). - okIsZero, deadlineViolationIsFive, clockErrorIsSix: pin the result-code encoding the Zig FFI depends on. - preIsStateful, fbyIsStateful, whenIsStateless, mergeIsStateless: pin the temporal-operator state classification. Build: `cd src/interface/abi && idris2 --build lustreiser-abi.ipkg` exits 0 with zero errors and zero warnings. 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 7479e0b commit 6c1a419

6 files changed

Lines changed: 296 additions & 55 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/Lustreiser/ABI/Foreign.idr

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -171,6 +171,9 @@ getClockTree h = do
171171
if ptr == 0
172172
then pure Nothing
173173
else pure (Just (prim__getString ptr))
174+
where
175+
%foreign "support:idris2_getString, libidris2_support"
176+
prim__getString : Bits64 -> String
174177

175178
--------------------------------------------------------------------------------
176179
-- Stream Buffer Management
@@ -211,11 +214,6 @@ checkMemoryFit h ram = do
211214
-- String Operations
212215
--------------------------------------------------------------------------------
213216

214-
||| Convert C string to Idris String
215-
export
216-
%foreign "support:idris2_getString, libidris2_support"
217-
prim__getString : Bits64 -> String
218-
219217
||| Free C string allocated by the library
220218
export
221219
%foreign "C:lustreiser_free_string, liblustreiser"
@@ -237,6 +235,9 @@ getString h = do
237235
let str = prim__getString ptr
238236
primIO (prim__freeString ptr)
239237
pure (Just str)
238+
where
239+
%foreign "support:idris2_getString, libidris2_support"
240+
prim__getString : Bits64 -> String
240241

241242
--------------------------------------------------------------------------------
242243
-- Error Handling
@@ -255,6 +256,9 @@ lastError = do
255256
if ptr == 0
256257
then pure Nothing
257258
else pure (Just (prim__getString ptr))
259+
where
260+
%foreign "support:idris2_getString, libidris2_support"
261+
prim__getString : Bits64 -> String
258262

259263
||| Get error description for result code
260264
export
@@ -282,6 +286,9 @@ version : IO String
282286
version = do
283287
ptr <- primIO prim__version
284288
pure (prim__getString ptr)
289+
where
290+
%foreign "support:idris2_getString, libidris2_support"
291+
prim__getString : Bits64 -> String
285292

286293
||| Get library build info
287294
export
@@ -294,6 +301,9 @@ buildInfo : IO String
294301
buildInfo = do
295302
ptr <- primIO prim__buildInfo
296303
pure (prim__getString ptr)
304+
where
305+
%foreign "support:idris2_getString, libidris2_support"
306+
prim__getString : Bits64 -> String
297307

298308
--------------------------------------------------------------------------------
299309
-- Callback Support

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

Lines changed: 91 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ import Lustreiser.ABI.Types
2121
import Data.Vect
2222
import Data.So
2323
import Data.Nat
24+
import Decidable.Equality
2425

2526
%default total
2627

@@ -35,25 +36,42 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
3536
paddingFor offset alignment =
3637
if offset `mod` alignment == 0
3738
then 0
38-
else alignment - (offset `mod` alignment)
39+
else minus alignment (offset `mod` alignment)
3940

40-
||| Proof that alignment divides aligned size
41+
||| Proof that alignment divides aligned size: `m = k * n`.
4142
public export
4243
data Divides : Nat -> Nat -> Type where
4344
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
4445

46+
||| Sound decision procedure for divisibility. Returns a genuine
47+
||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing.
48+
||| Division by zero is undecidable here and yields Nothing.
49+
public export
50+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
51+
decDivides Z _ = Nothing
52+
decDivides (S k) m =
53+
let q = m `div` (S k) in
54+
case decEq m (q * (S k)) of
55+
Yes prf => Just (DivideBy q prf)
56+
No _ => Nothing
57+
4558
||| Round up to next alignment boundary
4659
public export
4760
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
4861
alignUp size alignment =
4962
size + paddingFor size alignment
5063

51-
||| Proof that alignUp produces aligned result
64+
||| Sound divisibility check for an aligned size. The general theorem
65+
||| "alignUp size align is always divisible by align" needs div/mod lemmas
66+
||| from Data.Nat and is tracked as residual proof work; here we *decide* it
67+
||| via `decDivides`, which returns a genuine witness when it holds. For the
68+
||| concrete ABI layouts below, divisibility is proven outright (`DivideBy`).
69+
||| (Previously `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot
70+
||| typecheck for symbolic inputs.)
5271
public export
53-
alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) ->
54-
Divides align (alignUp size align)
55-
alignUpCorrect size align prf =
56-
DivideBy ((size + paddingFor size align) `div` align) Refl
72+
alignUpDivides : (size : Nat) -> (align : Nat) ->
73+
Maybe (Divides align (alignUp size align))
74+
alignUpDivides size align = decDivides align (alignUp size align)
5775

5876
--------------------------------------------------------------------------------
5977
-- Stream Buffer Layout
@@ -95,6 +113,12 @@ data FitsInRegion : StreamBuffer -> Nat -> Type where
95113
-- Node State Layout
96114
--------------------------------------------------------------------------------
97115

116+
||| Total bytes occupied by a vector of stream buffers (lifted out of the
117+
||| `NodeLayout` record, where a `where` block is not valid syntax).
118+
public export
119+
totalBufferSize : {0 nb : Nat} -> Vect nb StreamBuffer -> Nat
120+
totalBufferSize = sum . map bufferBytes
121+
98122
||| The complete memory layout for a Lustre node's state.
99123
||| This includes all input buffers, output buffers, and internal
100124
||| state variables for temporal operators.
@@ -107,17 +131,14 @@ public export
107131
record NodeLayout where
108132
constructor MkNodeLayout
109133
nodeName : String
110-
inputBuffers : Vect n StreamBuffer
111-
outputBuffers : Vect m StreamBuffer
112-
stateBuffers : Vect k StreamBuffer -- for pre/fby internal state
134+
inputBuffers : Vect numIn StreamBuffer
135+
outputBuffers : Vect numOut StreamBuffer
136+
stateBuffers : Vect numState StreamBuffer -- for pre/fby internal state
113137
totalSize : Nat
114138
alignment : Nat
115139
{auto 0 sizeCorrect : So (totalSize >= totalBufferSize inputBuffers +
116140
totalBufferSize outputBuffers +
117141
totalBufferSize stateBuffers)}
118-
where
119-
totalBufferSize : Vect j StreamBuffer -> Nat
120-
totalBufferSize = sum . map bufferBytes
121142

122143
||| Calculate the total memory footprint of a node layout
123144
public export
@@ -147,15 +168,15 @@ nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
147168
public export
148169
record StructLayout where
149170
constructor MkStructLayout
150-
fields : Vect n Field
171+
fields : Vect numFields Field
151172
totalSize : Nat
152173
alignment : Nat
153174
{auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
154175
{auto 0 aligned : Divides alignment totalSize}
155176

156177
||| Calculate total struct size with padding
157178
public export
158-
calcStructSize : Vect n Field -> Nat -> Nat
179+
calcStructSize : {0 nf : Nat} -> Vect nf Field -> Nat -> Nat
159180
calcStructSize [] align = 0
160181
calcStructSize (f :: fs) align =
161182
let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -164,24 +185,43 @@ calcStructSize (f :: fs) align =
164185

165186
||| Proof that field offsets are correctly aligned
166187
public export
167-
data FieldsAligned : Vect n Field -> Type where
188+
data FieldsAligned : Vect nf Field -> Type where
168189
NoFields : FieldsAligned []
169190
ConsField :
170191
(f : Field) ->
171-
(rest : Vect n Field) ->
192+
(rest : Vect nf Field) ->
172193
Divides f.alignment f.offset ->
173194
FieldsAligned rest ->
174195
FieldsAligned (f :: rest)
175196

176-
||| Verify a struct layout is valid
197+
||| Decide field alignment for every field, building a real `FieldsAligned`
198+
||| witness from per-field divisibility proofs.
199+
public export
200+
decFieldsAligned : {0 nf : Nat} -> (fs : Vect nf Field) -> Maybe (FieldsAligned fs)
201+
decFieldsAligned [] = Just NoFields
202+
decFieldsAligned (f :: fs) =
203+
case decDivides f.alignment f.offset of
204+
Nothing => Nothing
205+
Just dvd => case decFieldsAligned fs of
206+
Nothing => Nothing
207+
Just rest => Just (ConsField f fs dvd rest)
208+
209+
||| Verify a struct layout is valid. Builds a `StructLayout` only when BOTH
210+
||| obligations are discharged with genuine witnesses: the declared size covers
211+
||| the sum of field sizes (`decSo`) and the alignment divides the total size
212+
||| (`decDivides`). (Previously `MkStructLayout fields size align` left the
213+
||| erased `aligned : Divides alignment totalSize` proof unsolved.)
177214
public export
178-
verifyLayout : (fields : Vect n Field) -> (align : Nat) ->
215+
verifyLayout : {0 nf : Nat} -> (fields : Vect nf Field) -> (align : Nat) ->
179216
Either String StructLayout
180217
verifyLayout fields align =
181218
let size = calcStructSize fields align
182219
in case decSo (size >= sum (map (\f => f.size) fields)) of
183-
Yes prf => Right (MkStructLayout fields size align)
184220
No _ => Left "Invalid struct size"
221+
Yes prf => case decDivides align size of
222+
Nothing => Left "Total struct size is not aligned"
223+
Just dvd => Right (MkStructLayout fields size align
224+
{sizeCorrect = prf} {aligned = dvd})
185225

186226
--------------------------------------------------------------------------------
187227
-- Lustre-Specific Layouts
@@ -202,6 +242,8 @@ lustrePortLayout elemSize =
202242
]
203243
32 -- Total size: 32 bytes
204244
8 -- Alignment: 8 bytes
245+
{sizeCorrect = Oh}
246+
{aligned = DivideBy 4 Refl}
205247

206248
||| Layout for a Lustre node's execution context.
207249
||| Passed to every node step function — contains timing info and state.
@@ -218,6 +260,8 @@ lustreContextLayout =
218260
]
219261
32 -- Total size: 32 bytes
220262
8 -- Alignment: 8 bytes
263+
{sizeCorrect = Oh}
264+
{aligned = DivideBy 4 Refl}
221265

222266
--------------------------------------------------------------------------------
223267
-- Platform-Specific Layouts
@@ -240,7 +284,7 @@ platformAlignment _ = 8
240284

241285
||| Verify layout is correct for all platforms
242286
public export
243-
verifyAllPlatforms :
287+
verifyAllPlatforms : {0 t : Type} ->
244288
(layouts : (p : Platform) -> PlatformLayout p t) ->
245289
Either String ()
246290
verifyAllPlatforms layouts = Right ()
@@ -253,22 +297,22 @@ verifyAllPlatforms layouts = Right ()
253297
||| the target's available static RAM. This is critical for bare-metal
254298
||| embedded targets where memory is measured in kilobytes.
255299
public export
256-
data FitsInRAM : Vect n NodeLayout -> Nat -> Type where
257-
AllNodesFit : (layouts : Vect n NodeLayout) ->
300+
data FitsInRAM : {0 nl : Nat} -> Vect nl NodeLayout -> Nat -> Type where
301+
AllNodesFit : {0 nl : Nat} -> (layouts : Vect nl NodeLayout) ->
258302
(availableRAM : Nat) ->
259-
So (sum (map layoutFootprint layouts) <= availableRAM) ->
303+
So (sum (map Layout.layoutFootprint layouts) <= availableRAM) ->
260304
FitsInRAM layouts availableRAM
261305

262306
||| Check that a set of node layouts fits within available RAM
263307
public export
264-
checkRAMBudget : (layouts : Vect n NodeLayout) -> (ram : Nat) ->
308+
checkRAMBudget : {0 nl : Nat} -> (layouts : Vect nl NodeLayout) -> (ram : Nat) ->
265309
Either String (FitsInRAM layouts ram)
266310
checkRAMBudget layouts ram =
267-
let required = sum (map layoutFootprint layouts)
268-
in case decSo (required <= ram) of
269-
Yes prf => Right (AllNodesFit layouts ram prf)
270-
No _ => Left ("Total memory required (" ++ show required ++
271-
" bytes) exceeds available RAM (" ++ show ram ++ " bytes)")
311+
case decSo (sum (map Layout.layoutFootprint layouts) <= ram) of
312+
Yes prf => Right (AllNodesFit layouts ram prf)
313+
No _ => Left ("Total memory required (" ++
314+
show (sum (map Layout.layoutFootprint layouts)) ++
315+
" bytes) exceeds available RAM (" ++ show ram ++ " bytes)")
272316

273317
--------------------------------------------------------------------------------
274318
-- C ABI Compatibility
@@ -282,14 +326,25 @@ data CABICompliant : StructLayout -> Type where
282326
FieldsAligned layout.fields ->
283327
CABICompliant layout
284328

285-
||| Check if layout follows C ABI
329+
||| Check if layout follows C ABI, returning a genuine `CABICompliant` proof
330+
||| (built from real per-field divisibility witnesses) or an error when some
331+
||| field offset is misaligned. (Previously `CABIOk layout ?fieldsAlignedProof`
332+
||| with an unsolved hole.)
286333
public export
287334
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
288335
checkCABI layout =
289-
Right (CABIOk layout ?fieldsAlignedProof)
290-
291-
||| Proof that field offset is within struct bounds
336+
case decFieldsAligned layout.fields of
337+
Just prf => Right (CABIOk layout prf)
338+
Nothing => Left "Field offsets are not correctly aligned for the C ABI"
339+
340+
||| Decide whether a field lies within a struct's byte bounds, returning a
341+
||| genuine proof when `offset + size <= totalSize`. The previous signature
342+
||| asserted this for *every* field unconditionally, which is unsound (a field
343+
||| need not belong to the layout); this honest version decides it via `choose`.
292344
public export
293345
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
294-
So (f.offset + f.size <= layout.totalSize)
295-
offsetInBounds layout f = ?offsetInBoundsProof
346+
Maybe (So (f.offset + f.size <= layout.totalSize))
347+
offsetInBounds layout f =
348+
case choose (f.offset + f.size <= layout.totalSize) of
349+
Left ok => Just ok
350+
Right _ => Nothing

0 commit comments

Comments
 (0)