Skip to content

Commit a98c5cb

Browse files
hyperpolymathJonathan D.A. Jewellclaude
authored
ABI: scaffold a real, verified Idris2 ABI (10 type-safety levels) (#30)
* 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 * typedqliser: scaffold a real, verified Idris2 ABI (10 type-safety levels) typedqliser previously had no Idris2 ABI at all (only a README + manifest in src/interface/abi/). Add a genuine, compiler-checked ABI modelling the domain from src/abi/mod.rs — the ten cumulative type-safety levels and the proof certificate that crosses the FFI boundary. - Types.idr: SafetyLevel (10 levels) + levelNat ordinal + cumulative levelDominates ordering; ProofStatus + encoding; Result codes; choose-based createHandle; LevelProof/ProofCertificate records; CertifiedComplete with a real `So (allProven v)` obligation + decision procedure. - Layout.idr: sound decDivides/decFieldsAligned/checkCABI machinery (matching the verified iseriser reference) + the 40-byte certificate descriptor layout. - Foreign.idr: C-ABI FFI declarations (init/free/check_query/certificate_level/ version) with Result-mapping safe wrappers. - Proofs.idr: machine-checked theorems — certificate descriptor is C-ABI compliant (direct DivideBy witnesses); level ordinals + cumulative ordering; status encoding pins; certificate completeness (non-vacuous). - typedqliser-abi.ipkg; ignore Idris build artifacts. Verified: idris2 --build typedqliser-abi.ipkg clean (0 errors/0 warnings); negative control — CertifiedComplete [Proven, Refuted] correctly fails to typecheck. 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 2de8295 commit a98c5cb

6 files changed

Lines changed: 480 additions & 0 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -116,3 +116,8 @@ deps/
116116
.cache/
117117
build/
118118
dist/
119+
120+
# Idris2 proof build artifacts
121+
**/build/
122+
*.ttc
123+
*.ttm

‎src/interface/abi/Typedqliser/ABI/Foreign.idr‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
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+
||| Foreign Function Interface declarations for TypedQLiser.
5+
|||
6+
||| C-compatible entry points implemented in the Zig FFI layer
7+
||| (src/interface/ffi/src/main.zig). Each safe wrapper maps the raw C result
8+
||| code back to the `Result` type from the ABI.
9+
10+
module Typedqliser.ABI.Foreign
11+
12+
import Typedqliser.ABI.Types
13+
import Typedqliser.ABI.Layout
14+
15+
%default total
16+
17+
||| Initialise the TypedQLiser proof engine; returns a context pointer.
18+
export
19+
%foreign "C:typedqliser_init,libtypedqliser"
20+
prim__init : PrimIO Bits64
21+
22+
export
23+
init : IO (Maybe Handle)
24+
init = do
25+
ptr <- primIO prim__init
26+
pure (createHandle ptr)
27+
28+
||| Release the proof engine context.
29+
export
30+
%foreign "C:typedqliser_free,libtypedqliser"
31+
prim__free : Bits64 -> PrimIO ()
32+
33+
export
34+
free : Handle -> IO ()
35+
free h = primIO (prim__free (handlePtr h))
36+
37+
||| Check a query (null-terminated C string) against a schema, up to the
38+
||| requested level. Returns a C result code.
39+
export
40+
%foreign "C:typedqliser_check_query,libtypedqliser"
41+
prim__checkQuery : Bits64 -> String -> Bits32 -> PrimIO Bits32
42+
43+
export
44+
checkQuery : Handle -> (query : String) -> (level : Bits32) -> IO (Either Result ())
45+
checkQuery h query level = do
46+
rc <- primIO (prim__checkQuery (handlePtr h) query level)
47+
pure $ case rc of
48+
0 => Right ()
49+
2 => Left InvalidQuery
50+
3 => Left SchemaError
51+
_ => Left Error
52+
53+
||| Highest safety level the last checked query achieved (0 if none).
54+
export
55+
%foreign "C:typedqliser_certificate_level,libtypedqliser"
56+
prim__certificateLevel : Bits64 -> PrimIO Bits32
57+
58+
export
59+
certificateLevel : Handle -> IO Nat
60+
certificateLevel h = do
61+
n <- primIO (prim__certificateLevel (handlePtr h))
62+
pure (cast n)
63+
64+
||| Library version string.
65+
export
66+
%foreign "C:typedqliser_version,libtypedqliser"
67+
prim__version : PrimIO Bits64
68+
69+
export
70+
version : IO String
71+
version = do
72+
ptr <- primIO prim__version
73+
pure (prim__getString ptr)
74+
where
75+
%foreign "support:idris2_getString, libidris2_support"
76+
prim__getString : Bits64 -> String

‎src/interface/abi/Typedqliser/ABI/Layout.idr‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
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+
||| Memory-layout proofs for the TypedQLiser ABI.
5+
|||
6+
||| The proof certificate descriptor crosses the Zig/C FFI boundary; this module
7+
||| pins its field layout and proves it is C-ABI aligned.
8+
9+
module Typedqliser.ABI.Layout
10+
11+
import Typedqliser.ABI.Types
12+
import Data.Vect
13+
import Data.So
14+
import Data.Nat
15+
import Decidable.Equality
16+
17+
%default total
18+
19+
public export
20+
paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
21+
paddingFor offset alignment =
22+
if offset `mod` alignment == 0
23+
then 0
24+
else minus alignment (offset `mod` alignment)
25+
26+
public export
27+
alignUp : (size : Nat) -> (alignment : Nat) -> Nat
28+
alignUp size alignment = size + paddingFor size alignment
29+
30+
||| `m = k * n` — n divides m.
31+
public export
32+
data Divides : Nat -> Nat -> Type where
33+
DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
34+
35+
||| Sound divisibility decision: returns a real witness when n divides m.
36+
public export
37+
decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
38+
decDivides Z _ = Nothing
39+
decDivides (S k) m =
40+
let q = m `div` (S k) in
41+
case decEq m (q * (S k)) of
42+
Yes prf => Just (DivideBy q prf)
43+
No _ => Nothing
44+
45+
public export
46+
record Field where
47+
constructor MkField
48+
name : String
49+
offset : Nat
50+
size : Nat
51+
alignment : Nat
52+
53+
public export
54+
record StructLayout where
55+
constructor MkStructLayout
56+
fields : Vect k Field
57+
totalSize : Nat
58+
alignment : Nat
59+
{auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
60+
{auto 0 aligned : Divides alignment totalSize}
61+
62+
||| The proof-certificate descriptor as it crosses the FFI (40 bytes, 8-aligned).
63+
public export
64+
certificateDescLayout : StructLayout
65+
certificateDescLayout =
66+
MkStructLayout
67+
[ MkField "query_hash_ptr" 0 8 8
68+
, MkField "schema_ver_ptr" 8 8 8
69+
, MkField "max_level" 16 4 4
70+
, MkField "num_proofs" 20 4 4
71+
, MkField "proofs_ptr" 24 8 8
72+
, MkField "result_code" 32 4 4
73+
, MkField "padding" 36 4 4
74+
]
75+
40
76+
8
77+
{sizeCorrect = Oh}
78+
{aligned = DivideBy 5 Refl}
79+
80+
||| Every field offset in a layout is correctly aligned.
81+
public export
82+
data FieldsAligned : Vect len Field -> Type where
83+
NoFields : FieldsAligned []
84+
ConsField :
85+
(f : Field) ->
86+
(rest : Vect len Field) ->
87+
Divides f.alignment f.offset ->
88+
FieldsAligned rest ->
89+
FieldsAligned (f :: rest)
90+
91+
||| Decide field alignment, building a real witness from per-field divisibility.
92+
public export
93+
decFieldsAligned : (fs : Vect len Field) -> Maybe (FieldsAligned fs)
94+
decFieldsAligned [] = Just NoFields
95+
decFieldsAligned (f :: fs) =
96+
case decDivides f.alignment f.offset of
97+
Nothing => Nothing
98+
Just dvd => case decFieldsAligned fs of
99+
Nothing => Nothing
100+
Just rest => Just (ConsField f fs dvd rest)
101+
102+
public export
103+
data CABICompliant : StructLayout -> Type where
104+
CABIOk : (layout : StructLayout) -> FieldsAligned layout.fields -> CABICompliant layout
105+
106+
||| Verify a layout against the C-ABI alignment rules; real proof or error.
107+
public export
108+
checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
109+
checkCABI layout =
110+
case decFieldsAligned layout.fields of
111+
Just prf => Right (CABIOk layout prf)
112+
Nothing => Left "Field offsets are not correctly aligned for the C ABI"
113+
114+
||| Decide whether a field lies within a struct's byte bounds (honest Maybe;
115+
||| the property is false for an arbitrary field, so it is decided not asserted).
116+
public export
117+
offsetInBounds : (layout : StructLayout) -> (f : Field) ->
118+
Maybe (So (f.offset + f.size <= layout.totalSize))
119+
offsetInBounds layout f =
120+
case choose (f.offset + f.size <= layout.totalSize) of
121+
Left ok => Just ok
122+
Right _ => Nothing

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

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
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 TypedQLiser ABI.
5+
|||
6+
||| These are propositional statements the Idris2 type checker must discharge at
7+
||| compile time — not runtime tests. If the certificate descriptor were
8+
||| misaligned, a level ordinal wrong, the status encoding off, or a "complete"
9+
||| certificate admitted a non-Proven level, this module would fail to typecheck.
10+
11+
module Typedqliser.ABI.Proofs
12+
13+
import Typedqliser.ABI.Types
14+
import Typedqliser.ABI.Layout
15+
import Data.So
16+
import Data.Vect
17+
18+
%default total
19+
20+
--------------------------------------------------------------------------------
21+
-- The certificate descriptor is provably C-ABI compliant.
22+
--------------------------------------------------------------------------------
23+
24+
||| Every field offset in the certificate descriptor divides its alignment:
25+
||| 0|8, 8|8, 16|4, 20|4, 24|8, 32|4, 36|4.
26+
export
27+
certificateDescCompliant : CABICompliant Layout.certificateDescLayout
28+
certificateDescCompliant =
29+
CABIOk Layout.certificateDescLayout
30+
(ConsField _ _ (DivideBy 0 Refl)
31+
(ConsField _ _ (DivideBy 1 Refl)
32+
(ConsField _ _ (DivideBy 4 Refl)
33+
(ConsField _ _ (DivideBy 5 Refl)
34+
(ConsField _ _ (DivideBy 3 Refl)
35+
(ConsField _ _ (DivideBy 8 Refl)
36+
(ConsField _ _ (DivideBy 9 Refl)
37+
NoFields)))))))
38+
39+
--------------------------------------------------------------------------------
40+
-- Level ordinals + cumulative ordering.
41+
--------------------------------------------------------------------------------
42+
43+
||| ParseSafe is level 1 (the floor).
44+
export
45+
parseSafeIsOne : levelNat ParseSafe = 1
46+
parseSafeIsOne = Refl
47+
48+
||| LinearSafe is level 10 (the ceiling).
49+
export
50+
linearSafeIsTen : levelNat LinearSafe = 10
51+
linearSafeIsTen = Refl
52+
53+
||| Cumulativity is reflected in the ordering: the top level dominates every
54+
||| other. A query at LinearSafe has therefore discharged InjectionFree.
55+
export
56+
linearDominatesInjectionFree : So (levelDominates LinearSafe InjectionFree)
57+
linearDominatesInjectionFree = Oh
58+
59+
||| The ordering is *not* symmetric: InjectionFree does not dominate LinearSafe.
60+
export
61+
injectionFreeBelowLinear : So (not (levelDominates InjectionFree LinearSafe))
62+
injectionFreeBelowLinear = Oh
63+
64+
--------------------------------------------------------------------------------
65+
-- Proof-status encoding the Zig FFI depends on.
66+
--------------------------------------------------------------------------------
67+
68+
export
69+
provenIsZero : statusToInt Proven = 0
70+
provenIsZero = Refl
71+
72+
export
73+
timeoutIsThree : statusToInt Timeout = 3
74+
timeoutIsThree = Refl
75+
76+
--------------------------------------------------------------------------------
77+
-- Certificate completeness (non-vacuous).
78+
--------------------------------------------------------------------------------
79+
80+
||| A certificate whose ten levels are all Proven is complete. The obligation is
81+
||| real: see `incompleteRejected` for the negative side.
82+
export
83+
tenAllProven : CertifiedComplete (replicate 10 Proven)
84+
tenAllProven = Complete Oh
85+
86+
||| A certificate with one Refuted level is NOT all-proven — witnessing that
87+
||| `CertifiedComplete`'s obligation `So (allProven v)` is not vacuously true
88+
||| (there is no `Complete` for this vector).
89+
export
90+
incompleteNotAllProven :
91+
So (not (allProven [Proven, Proven, Refuted, Proven]))
92+
incompleteNotAllProven = Oh

0 commit comments

Comments
 (0)