Skip to content

Commit 8dd9681

Browse files
claudeclaude
committed
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
1 parent 0b4089c commit 8dd9681

2 files changed

Lines changed: 211 additions & 0 deletions

File tree

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

Lines changed: 210 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,210 @@
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+
||| Semantic proof for TypedQLiser's `TypeCompat` level (level 3:
5+
||| "operand types compatible").
6+
|||
7+
||| Alongside `Semantics.InjectionFree` (level 5) and `SchemaBound.SchemaBound`
8+
||| (level 2), this makes `TypeCompat` (level 3) a real, machine-checked property
9+
||| over the shared query AST: every comparison in the WHERE predicate compares a
10+
||| column against a value whose type matches the column's declared type. A bound
11+
||| parameter adopts the column's type (so it is always compatible); a literal is
12+
||| `TInt` and a raw string is `TText`, so comparing them against a column of a
13+
||| different type has *no* proof. It provides:
14+
|||
15+
||| 1. a small SQL type universe and a typed column environment;
16+
||| 2. `ValueCompat`/`PredTypeCompat`/`QueryTypeCompat` — the proposition that
17+
||| every comparison's operands are type-compatible (uninhabited on a clash);
18+
||| 3. `decQueryTypeCompat`, a sound + complete `Dec`, so "Proven" is backed by
19+
||| a constructive witness and a type clash can never be certified;
20+
||| 4. a certifier proven sound (`certifyTypeCompatSound`), level-ordinal
21+
||| identity, and positive + negative controls.
22+
|||
23+
||| The query AST (`Query`/`Pred`/`Value`) is reused verbatim from `Semantics`.
24+
25+
module Typedqliser.ABI.TypeCompat
26+
27+
import Typedqliser.ABI.Types
28+
import Typedqliser.ABI.Semantics
29+
30+
%default total
31+
32+
--------------------------------------------------------------------------------
33+
-- A minimal SQL type universe + typed column environment
34+
--------------------------------------------------------------------------------
35+
36+
||| The column/value types this level distinguishes.
37+
public export
38+
data SqlType = TInt | TText | TBool
39+
40+
||| A typed column environment: declared columns with their types (the resolved
41+
||| form of a table's schema, as produced by the SchemaBound level).
42+
public export
43+
ColEnv : Type
44+
ColEnv = List (String, SqlType)
45+
46+
||| Resolve a column's declared type by name (first match wins).
47+
public export
48+
lookupType : String -> ColEnv -> Maybe SqlType
49+
lookupType _ [] = Nothing
50+
lookupType c ((n, ty) :: xs) = if n == c then Just ty else lookupType c xs
51+
52+
||| `Just` is injective. A top-level function clause (its `Refl` covers cleanly,
53+
||| whereas an inline `case … of Refl` on a resolver equation does not, because
54+
||| coverage does not reduce `lookupType` under a lifted scrutinee).
55+
justInj : Just x = Just y -> x = y
56+
justInj Refl = Refl
57+
58+
--------------------------------------------------------------------------------
59+
-- Value/column type compatibility as a genuine proposition
60+
--------------------------------------------------------------------------------
61+
62+
||| `ValueCompat ct v` holds when value `v` may be compared against a column of
63+
||| type `ct`. A bound parameter adopts any column type; a literal is `TInt`; a
64+
||| raw splice is `TText`. There is no constructor for a mismatch (e.g. a literal
65+
||| against a `TText` column), so such a `ValueCompat` is uninhabited.
66+
public export
67+
data ValueCompat : (ct : SqlType) -> Value -> Type where
68+
ParamAny : ValueCompat ct (Param i) -- a bound parameter adopts ct
69+
LitInt : ValueCompat TInt (Lit n) -- integer literal ↔ TInt column
70+
SpliceTxt : ValueCompat TText (RawSplice s) -- string splice ↔ TText column
71+
72+
-- Refutations of the type clashes (single impossible clauses; the value index
73+
-- prunes the non-matching constructors).
74+
litNotText : Not (ValueCompat TText (Lit n))
75+
litNotText LitInt impossible
76+
77+
litNotBool : Not (ValueCompat TBool (Lit n))
78+
litNotBool LitInt impossible
79+
80+
spliceNotInt : Not (ValueCompat TInt (RawSplice s))
81+
spliceNotInt SpliceTxt impossible
82+
83+
spliceNotBool : Not (ValueCompat TBool (RawSplice s))
84+
spliceNotBool SpliceTxt impossible
85+
86+
||| Sound + complete decision for one value against a column type.
87+
public export
88+
decValueCompat : (ct : SqlType) -> (v : Value) -> Dec (ValueCompat ct v)
89+
decValueCompat _ (Param i) = Yes ParamAny
90+
decValueCompat TInt (Lit n) = Yes LitInt
91+
decValueCompat TText (Lit n) = No litNotText
92+
decValueCompat TBool (Lit n) = No litNotBool
93+
decValueCompat TInt (RawSplice s) = No spliceNotInt
94+
decValueCompat TText (RawSplice s) = Yes SpliceTxt
95+
decValueCompat TBool (RawSplice s) = No spliceNotBool
96+
97+
||| A predicate is type-compatible (w.r.t. an environment) when every comparison
98+
||| resolves its column's type and the compared value matches that type.
99+
public export
100+
data PredTypeCompat : (env : ColEnv) -> Pred -> Type where
101+
CmpTC : (colType : lookupType col env = Just ct) -> ValueCompat ct v ->
102+
PredTypeCompat env (Cmp col v)
103+
AndTC : PredTypeCompat env p -> PredTypeCompat env q -> PredTypeCompat env (And p q)
104+
OrTC : PredTypeCompat env p -> PredTypeCompat env q -> PredTypeCompat env (Or p q)
105+
106+
||| Sound + complete decision for predicate type-compatibility. The `Cmp` case
107+
||| resolves the column type via a `proof`-bound equation, exactly as the
108+
||| SchemaBound level resolves table columns.
109+
public export
110+
decPredTypeCompat : (env : ColEnv) -> (p : Pred) -> Dec (PredTypeCompat env p)
111+
decPredTypeCompat env (Cmp col v) with (lookupType col env) proof eq
112+
_ | Nothing = No $ \(CmpTC colType _) => case trans (sym eq) colType of Refl impossible
113+
_ | Just ct = case decValueCompat ct v of
114+
Yes vc => Yes (CmpTC eq vc)
115+
No nvc => No $ \(CmpTC colType vc) => case trans (sym colType) eq of Refl => nvc vc
116+
decPredTypeCompat env (And p q) = case decPredTypeCompat env p of
117+
No np => No (\(AndTC pp _) => np pp)
118+
Yes pp => case decPredTypeCompat env q of
119+
Yes qq => Yes (AndTC pp qq)
120+
No nq => No (\(AndTC _ qq) => nq qq)
121+
decPredTypeCompat env (Or p q) = case decPredTypeCompat env p of
122+
No np => No (\(OrTC pp _) => np pp)
123+
Yes pp => case decPredTypeCompat env q of
124+
Yes qq => Yes (OrTC pp qq)
125+
No nq => No (\(OrTC _ qq) => nq qq)
126+
127+
||| A query is type-compatible when its WHERE predicate is.
128+
public export
129+
data QueryTypeCompat : (env : ColEnv) -> Query -> Type where
130+
MkQTC : PredTypeCompat env w -> QueryTypeCompat env (Select t sel w)
131+
132+
||| The headline decision procedure for the query level.
133+
public export
134+
decQueryTypeCompat : (env : ColEnv) -> (q : Query) -> Dec (QueryTypeCompat env q)
135+
decQueryTypeCompat env (Select t sel w) = case decPredTypeCompat env w of
136+
Yes pc => Yes (MkQTC pc)
137+
No npc => No (\(MkQTC pc) => npc pc)
138+
139+
--------------------------------------------------------------------------------
140+
-- Certifier soundness: a `Proven` TypeCompat status is never a lie
141+
--------------------------------------------------------------------------------
142+
143+
||| Certify the TypeCompat (level 3) obligation for a query against a typed
144+
||| environment. `Proven` only when the decision procedure produced a real proof.
145+
public export
146+
certifyTypeCompat : (env : ColEnv) -> (q : Query) -> ProofStatus
147+
certifyTypeCompat env q = case decQueryTypeCompat env q of
148+
Yes _ => Proven
149+
No _ => Refuted
150+
151+
||| Soundness: a `Proven` verdict entails the property. With `decQueryTypeCompat`
152+
||| being a `Dec`, a type-incompatible query can never be reported `Proven`.
153+
export
154+
certifyTypeCompatSound : (env : ColEnv) -> (q : Query) ->
155+
certifyTypeCompat env q = Proven -> QueryTypeCompat env q
156+
certifyTypeCompatSound env q prf with (decQueryTypeCompat env q)
157+
certifyTypeCompatSound env q prf | Yes ok = ok
158+
certifyTypeCompatSound env q Refl | No _ impossible
159+
160+
||| `TypeCompat` is level 3 — the certified obligation is the third of ten.
161+
export
162+
typeCompatIsLevelThree : levelNat TypeCompat = 3
163+
typeCompatIsLevelThree = Refl
164+
165+
--------------------------------------------------------------------------------
166+
-- Positive control: a well-typed query is provably type-compatible
167+
--------------------------------------------------------------------------------
168+
169+
||| `users(id : Int, name : Text, age : Int)`.
170+
public export
171+
exampleEnv : ColEnv
172+
exampleEnv = [("id", TInt), ("name", TText), ("age", TInt)]
173+
174+
||| `SELECT id, name FROM users WHERE age = 18 AND name = $1` — `age` (Int) vs an
175+
||| integer literal, and `name` (Text) vs a bound parameter: both compatible.
176+
public export
177+
goodQuery : Query
178+
goodQuery =
179+
Select "users" ["id", "name"] (And (Cmp "age" (Lit 18)) (Cmp "name" (Param 1)))
180+
181+
||| Machine-checked: the query is type-compatible against `exampleEnv`.
182+
export
183+
goodQueryTypeCompat : QueryTypeCompat TypeCompat.exampleEnv TypeCompat.goodQuery
184+
goodQueryTypeCompat = MkQTC (AndTC (CmpTC Refl LitInt) (CmpTC Refl ParamAny))
185+
186+
||| …and the certifier reports `Proven` for it (computes to `Proven`).
187+
export
188+
goodQueryCertifiesProven :
189+
certifyTypeCompat TypeCompat.exampleEnv TypeCompat.goodQuery = Proven
190+
goodQueryCertifiesProven = Refl
191+
192+
--------------------------------------------------------------------------------
193+
-- Negative control: a type clash CANNOT be certified
194+
--------------------------------------------------------------------------------
195+
196+
||| `SELECT id FROM users WHERE name = 42` — comparing a `Text` column against an
197+
||| integer literal is a type clash.
198+
public export
199+
badQuery : Query
200+
badQuery = Select "users" ["id"] (Cmp "name" (Lit 42))
201+
202+
||| Machine-checked: there is **no** proof that the clash is type-compatible.
203+
||| `name` resolves to `TText`, but `ValueCompat TText (Lit 42)` is uninhabited,
204+
||| so the property is genuinely refuted (this is what makes it non-vacuous).
205+
||| The witness is transported at the term level (`replace`/`justInj`) rather
206+
||| than via `case … of Refl`, which coverage rejects on the stuck resolver LHS.
207+
export
208+
badQueryNotTypeCompat : Not (QueryTypeCompat TypeCompat.exampleEnv TypeCompat.badQuery)
209+
badQueryNotTypeCompat (MkQTC (CmpTC {ct} colType vc)) =
210+
litNotText (replace {p = \x => ValueCompat x (Lit 42)} (sym (justInj colType)) vc)

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,4 @@ modules = Typedqliser.ABI.Types
1111
, Typedqliser.ABI.Proofs
1212
, Typedqliser.ABI.Semantics
1313
, Typedqliser.ABI.SchemaBound
14+
, Typedqliser.ABI.TypeCompat

0 commit comments

Comments
 (0)