Skip to content

Commit 5957feb

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 4: prove the FFI result-code seam is injective + faithful (#38)
* P3: prove TypeCompat (level 3) as a real operand-type-compatibility guarantee Continues the flagship semantic-proof coverage (InjectionFree level 5, SchemaBound level 2) with TypeCompat (level 3: "operand types compatible"). Adds `Typedqliser.ABI.TypeCompat`, to the same quality bar: * a small SQL type universe (`SqlType`) and a typed column environment (`ColEnv`) with a total `lookupType` resolver, reusing the existing `Query`/`Pred`/`Value` AST; * `ValueCompat`/`PredTypeCompat`/`QueryTypeCompat` — the proposition that every WHERE comparison compares a column against a value of a matching type (a bound parameter adopts the column's type; a literal is TInt; a raw splice is TText). There is no constructor for a type clash, so a mismatched comparison is uninhabited; * `decQueryTypeCompat` — a sound + complete `Dec`, so a "Proven" TypeCompat certificate is backed by a constructive witness and a type clash can never be certified; * `certifyTypeCompatSound` (a `Proven` verdict provably entails the property); `typeCompatIsLevelThree : levelNat TypeCompat = 3`; * positive control (a well-typed query, with the certifier computing to `Proven`) and negative control (`name : Text` compared to an integer literal provably cannot be certified). Verified with idris2 0.7.0: `idris2 --build typedqliser-abi.ipkg` exits 0 with zero warnings (all 7 modules). Adversarially checked — three deliberately-false proofs (wrong level ordinal, a TInt literal certified against a TText column, and a type-compatible witness for the clash query) are all rejected by the type checker. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: add Layer-3 NullSafe (level 4) theorem with guard discovery Adds Typedqliser.ABI.Invariants, a second, deeper, distinct machine-checked property over the existing Semantics query model (Query/Pred/Value reused verbatim). Where the Layer-2 flagship (Semantics.InjectionFree, level 5) is a purely structural property, NullSafe (level 4) is context-sensitive: a projected nullable column is safe only if the WHERE predicate guards it, with guards discovered by union under And and intersection under Or (disjunctive weakening). Includes a sound + complete decision procedure (decQueryNullSafe : Dec ...), a certifier proven sound (certifyNullSafeSound), the level-ordinal identity plus a proof it differs from InjectionFree, three positive controls and three non-vacuity controls (unguarded projection, And/union, Or/intersection). Builds clean with zero warnings; the deliberately-false adversarial proof is rejected. No believe_me/postulate/assert_total/%hint; %default total throughout. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * Add Layer-4 ABI<->FFI seam proof (Typedqliser.ABI.FfiSeam) Prove the FFI result-code encoding is SOUND: the C integer the Zig FFI returns faithfully round-trips back to the ABI value, and distinct ABI outcomes never collide on the wire. - intToResult / intToStatus: total decoders (if x == n over boolean Bits32 ==, which reduces on concrete literals). - resultRoundTrip / statusRoundTrip: lossless encoding, proved by Refl. - resultToIntInjective / statusToIntInjective: injectivity DERIVED from the round-trip via a local justInj + cong. - Positive controls (decodeOk/decodeNullPointer/decodeUnknown/decodeProven) and machine-checked non-vacuity controls (okNotError, schemaNotNull, provenNotRefuted) refuting collisions of distinct codes. Genuine total proof: no believe_me / postulate / assert_total / sorry. Builds clean with zero warnings; a false seam claim is rejected by --check. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
1 parent b55c2b7 commit 5957feb

2 files changed

Lines changed: 151 additions & 0 deletions

File tree

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

Lines changed: 150 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,150 @@
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+
||| Layer-4 proof: SEALING THE ABI<->FFI SEAM for TypedQLiser.
5+
|||
6+
||| The Idris2 ABI (`Typedqliser.ABI.Types`) defines the FFI result-code enum
7+
||| `Result` together with `resultToInt : Result -> Bits32` (the integer the Zig
8+
||| FFI hands back to C), and likewise `ProofStatus` / `statusToInt`. The estate
9+
||| has a STRUCTURAL gate (`scripts/abi-ffi-gate.py`) checking the Idris and Zig
10+
||| enums agree by name+value. THIS module is the PROOF-SIDE guarantee: the
11+
||| encodings are SOUND — distinct ABI outcomes never collide on the wire, and
12+
||| the C integer faithfully round-trips back to the ABI value.
13+
|||
14+
||| Strategy: build total decoders with `if x == n` over boolean `Bits32` `(==)`
15+
||| (which reduces on concrete literals), prove the round-trip lossless by `Refl`,
16+
||| and DERIVE injectivity from the round-trip via `justInj` + `cong`.
17+
18+
module Typedqliser.ABI.FfiSeam
19+
20+
import Typedqliser.ABI.Types
21+
22+
%default total
23+
24+
--------------------------------------------------------------------------------
25+
-- Local lemma
26+
--------------------------------------------------------------------------------
27+
28+
||| `Just` is injective. Proved locally (no library dependency) so the seam
29+
||| module stands on its own.
30+
private
31+
justInj : {0 x, y : a} -> Just x = Just y -> x = y
32+
justInj Refl = Refl
33+
34+
--------------------------------------------------------------------------------
35+
-- Result: decoder
36+
--------------------------------------------------------------------------------
37+
38+
||| Decode a C integer back into a `Result`. Total; unrecognised codes -> Nothing.
39+
||| Written with `if … == …` so that the boolean `Bits32` equality reduces on
40+
||| concrete literals and the round-trip `Refl`s below check definitionally.
41+
public export
42+
intToResult : Bits32 -> Maybe Result
43+
intToResult x =
44+
if x == 0 then Just Ok
45+
else if x == 1 then Just Error
46+
else if x == 2 then Just InvalidQuery
47+
else if x == 3 then Just SchemaError
48+
else if x == 4 then Just NullPointer
49+
else Nothing
50+
51+
--------------------------------------------------------------------------------
52+
-- Result: round-trip (faithful / lossless encoding)
53+
--------------------------------------------------------------------------------
54+
55+
||| The C integer round-trips back to the originating ABI value, for every
56+
||| `Result`. This is the faithfulness of the wire encoding.
57+
public export
58+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
59+
resultRoundTrip Ok = Refl
60+
resultRoundTrip Error = Refl
61+
resultRoundTrip InvalidQuery = Refl
62+
resultRoundTrip SchemaError = Refl
63+
resultRoundTrip NullPointer = Refl
64+
65+
--------------------------------------------------------------------------------
66+
-- Result: injectivity (no two outcomes collide on the wire)
67+
--------------------------------------------------------------------------------
68+
69+
||| The encoding is unambiguous: distinct `Result`s map to distinct integers.
70+
||| DERIVED from the round-trip — if `resultToInt a = resultToInt b` then
71+
||| `intToResult` of both sides are equal, i.e. `Just a = Just b`, hence `a = b`.
72+
public export
73+
resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b
74+
resultToIntInjective a b prf =
75+
justInj $
76+
trans (sym (resultRoundTrip a)) (trans (cong intToResult prf) (resultRoundTrip b))
77+
78+
--------------------------------------------------------------------------------
79+
-- ProofStatus: decoder, round-trip, injectivity
80+
--------------------------------------------------------------------------------
81+
82+
||| Decode a C integer back into a `ProofStatus`. Total; unknown -> Nothing.
83+
public export
84+
intToStatus : Bits32 -> Maybe ProofStatus
85+
intToStatus x =
86+
if x == 0 then Just Proven
87+
else if x == 1 then Just Refuted
88+
else if x == 2 then Just Skipped
89+
else if x == 3 then Just Timeout
90+
else Nothing
91+
92+
||| The proof-status integer round-trips back to its `ProofStatus`.
93+
public export
94+
statusRoundTrip : (s : ProofStatus) -> intToStatus (statusToInt s) = Just s
95+
statusRoundTrip Proven = Refl
96+
statusRoundTrip Refuted = Refl
97+
statusRoundTrip Skipped = Refl
98+
statusRoundTrip Timeout = Refl
99+
100+
||| `statusToInt` is injective — distinct proof statuses never collide on the wire.
101+
public export
102+
statusToIntInjective : (a, b : ProofStatus) -> statusToInt a = statusToInt b -> a = b
103+
statusToIntInjective a b prf =
104+
justInj $
105+
trans (sym (statusRoundTrip a)) (trans (cong intToStatus prf) (statusRoundTrip b))
106+
107+
--------------------------------------------------------------------------------
108+
-- Positive controls (concrete decodes reduce to Refl)
109+
--------------------------------------------------------------------------------
110+
111+
||| Decoding the wire value `0` yields `Ok`.
112+
public export
113+
decodeOk : intToResult 0 = Just Ok
114+
decodeOk = Refl
115+
116+
||| Decoding the wire value `4` yields `NullPointer`.
117+
public export
118+
decodeNullPointer : intToResult 4 = Just NullPointer
119+
decodeNullPointer = Refl
120+
121+
||| Decoding an out-of-range wire value yields `Nothing`.
122+
public export
123+
decodeUnknown : intToResult 99 = Nothing
124+
decodeUnknown = Refl
125+
126+
||| Decoding the wire value `0` yields `Proven`.
127+
public export
128+
decodeProven : intToStatus 0 = Just Proven
129+
decodeProven = Refl
130+
131+
--------------------------------------------------------------------------------
132+
-- Negative / non-vacuity controls (machine-checked dis-equalities)
133+
--------------------------------------------------------------------------------
134+
135+
||| NON-VACUITY: two DISTINCT result codes encode to DISTINCT integers.
136+
||| `Ok` -> 0 and `Error` -> 1, and the primitive `Bits32` literals `0` and `1`
137+
||| are provably unequal, so the coverage checker discharges `Refl impossible`.
138+
public export
139+
okNotError : Not (resultToInt Ok = resultToInt Error)
140+
okNotError Refl impossible
141+
142+
||| NON-VACUITY: `SchemaError` (3) and `NullPointer` (4) differ on the wire.
143+
public export
144+
schemaNotNull : Not (resultToInt SchemaError = resultToInt NullPointer)
145+
schemaNotNull Refl impossible
146+
147+
||| NON-VACUITY for `ProofStatus`: `Proven` (0) and `Refuted` (1) differ.
148+
public export
149+
provenNotRefuted : Not (statusToInt Proven = statusToInt Refuted)
150+
provenNotRefuted Refl impossible

‎src/interface/abi/typedqliser-abi.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,3 +13,4 @@ modules = Typedqliser.ABI.Types
1313
, Typedqliser.ABI.SchemaBound
1414
, Typedqliser.ABI.TypeCompat
1515
, Typedqliser.ABI.Invariants
16+
, Typedqliser.ABI.FfiSeam

0 commit comments

Comments
 (0)