Skip to content

Commit b55c2b7

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: NullSafe (level 4) — a deeper, context-sensitive query-safety checker (#37)
* 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 --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 592255d commit b55c2b7

2 files changed

Lines changed: 301 additions & 0 deletions

File tree

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

Lines changed: 300 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,300 @@
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 `NullSafe` level (level 4: "nullable paths
5+
||| explicitly handled").
6+
|||
7+
||| This is the Layer-3, *deeper* companion to `Semantics.InjectionFree` (level
8+
||| 5). Where InjectionFree is a purely structural property (no `RawSplice` node
9+
||| occurs anywhere), null-safety is genuinely **context-sensitive**: whether a
10+
||| projected nullable column may be returned depends on what the WHERE clause
11+
||| has guarded. The novel ingredient is *guard discovery with disjunctive
12+
||| weakening*:
13+
|||
14+
||| * A comparison `Cmp col v` in the WHERE clause is, in SQL three-valued
15+
||| logic, NULL (and so filters the row) when `col` is NULL — it therefore
16+
||| **guards** `col`, establishing that any surviving row has `col` non-null.
17+
||| * Under `And p q`, a column is guarded if EITHER conjunct guards it (each
18+
||| conjunct must hold, so either filter suffices) — set union.
19+
||| * Under `Or p q`, a column is guarded only if BOTH branches guard it, since
20+
||| a surviving row may have satisfied either branch — set intersection.
21+
||| * A SELECTed nullable column is null-safe only if the WHERE clause guards
22+
||| it; a non-nullable projected column is always safe.
23+
|||
24+
||| The disjunctive weakening (intersection under `Or`) is what makes this strict
25+
||| ly deeper than the InjectionFree structural check, and distinct from
26+
||| SchemaBound (membership) and TypeCompat (type matching): the same projected
27+
||| column can be safe or unsafe depending on the boolean shape of the WHERE
28+
||| predicate, not merely on which nodes occur.
29+
|||
30+
||| Contents:
31+
||| 1. `guardsOf`, the columns a WHERE predicate guards (`And` = union, `Or` =
32+
||| intersection);
33+
||| 2. `ColNullSafe`/`QueryNullSafe`, the proposition that every projected
34+
||| nullable column is guarded;
35+
||| 3. `decQueryNullSafe`, a sound + complete decision procedure (`Dec`);
36+
||| 4. `certifyNullSafeSound` (a `Proven` verdict entails the property), the
37+
||| level-ordinal identity, and positive + non-vacuity controls.
38+
|||
39+
||| The query AST (`Query`/`Pred`/`Value`) is reused verbatim from `Semantics`.
40+
41+
module Typedqliser.ABI.Invariants
42+
43+
import Typedqliser.ABI.Types
44+
import Typedqliser.ABI.Semantics
45+
import Data.List
46+
import Data.List.Elem
47+
import Decidable.Equality
48+
49+
%default total
50+
51+
--------------------------------------------------------------------------------
52+
-- Nullable-column environment + guard discovery
53+
--------------------------------------------------------------------------------
54+
55+
||| The set of column names declared NULLABLE. A column not in this set is
56+
||| non-nullable and may be projected freely.
57+
public export
58+
NullEnv : Type
59+
NullEnv = List String
60+
61+
||| Set intersection of column-name lists, written so it *reduces*
62+
||| definitionally on concrete literals (`Data.List.intersect` gets stuck under
63+
||| its `Eq` wrapper, which would block the `Refl`/`impossible` controls).
64+
||| Keeps a left-hand column iff it also appears on the right.
65+
public export
66+
inter : List String -> List String -> List String
67+
inter xs ys = filter (\x => elem x ys) xs
68+
69+
||| Set union of column-name lists (right side appended where absent), likewise
70+
||| written to reduce on literals.
71+
public export
72+
uni : List String -> List String -> List String
73+
uni xs ys = xs ++ filter (\y => not (elem y xs)) ys
74+
75+
||| The columns a WHERE predicate GUARDS (proves non-null for surviving rows).
76+
||| A bare comparison guards its column; `And` takes the union (either filter
77+
||| suffices, since both conjuncts must hold); `Or` takes the intersection (only
78+
||| columns guarded on BOTH branches survive, since either branch may have held).
79+
public export
80+
guardsOf : Pred -> List String
81+
guardsOf (Cmp col _) = [col]
82+
guardsOf (And p q) = uni (guardsOf p) (guardsOf q)
83+
guardsOf (Or p q) = inter (guardsOf p) (guardsOf q)
84+
85+
||| Decidable membership of a column name in a string list, as a real `Dec`.
86+
public export
87+
decColElem : (c : String) -> (xs : List String) -> Dec (Elem c xs)
88+
decColElem c xs = isElem c xs
89+
90+
--------------------------------------------------------------------------------
91+
-- NullSafe as a genuine, context-sensitive proposition
92+
--------------------------------------------------------------------------------
93+
94+
||| `ColNullSafe env gs col` holds when projecting `col` is null-safe given the
95+
||| nullable set `env` and the set of columns `gs` guarded by the WHERE clause:
96+
||| either `col` is not nullable, or it has been guarded. There is no third
97+
||| constructor, so projecting an unguarded nullable column has no proof — the
98+
||| heart of the guarantee.
99+
public export
100+
data ColNullSafe : (env : NullEnv) -> (gs : List String) -> (col : String) -> Type where
101+
||| `col` is not in the nullable set, so projecting it is unconditionally safe.
102+
NotNullable : Not (Elem col env) -> ColNullSafe env gs col
103+
||| `col` is nullable but the WHERE clause guards it.
104+
Guarded : Elem col gs -> ColNullSafe env gs col
105+
106+
||| Every projected column is null-safe under the WHERE clause's guard set.
107+
public export
108+
data ColsNullSafe : (env : NullEnv) -> (gs : List String) -> List String -> Type where
109+
NilNS : ColsNullSafe env gs []
110+
ConsNS : ColNullSafe env gs col -> ColsNullSafe env gs cols ->
111+
ColsNullSafe env gs (col :: cols)
112+
113+
||| A query is null-safe when every column it PROJECTS is null-safe with respect
114+
||| to the columns its WHERE predicate guards.
115+
public export
116+
data QueryNullSafe : (env : NullEnv) -> Query -> Type where
117+
SelectNS : ColsNullSafe env (guardsOf w) cols ->
118+
QueryNullSafe env (Select t cols w)
119+
120+
--------------------------------------------------------------------------------
121+
-- Refutation helper
122+
--------------------------------------------------------------------------------
123+
124+
||| A nullable, unguarded column cannot be `ColNullSafe`.
125+
notColNullSafe : Elem col env -> Not (Elem col gs) -> Not (ColNullSafe env gs col)
126+
notColNullSafe inEnv _ (NotNullable notIn) = notIn inEnv
127+
notColNullSafe _ notG (Guarded g) = notG g
128+
129+
--------------------------------------------------------------------------------
130+
-- Sound + complete decision procedure (returns a real proof)
131+
--------------------------------------------------------------------------------
132+
133+
||| Decide one projected column. Nullable + unguarded is the only refuted case.
134+
public export
135+
decColNullSafe : (env : NullEnv) -> (gs : List String) -> (col : String) ->
136+
Dec (ColNullSafe env gs col)
137+
decColNullSafe env gs col = case decColElem col env of
138+
No notIn => Yes (NotNullable notIn)
139+
Yes inEnv => case decColElem col gs of
140+
Yes g => Yes (Guarded g)
141+
No notG => No (notColNullSafe inEnv notG)
142+
143+
||| Decide a whole projection list.
144+
public export
145+
decColsNullSafe : (env : NullEnv) -> (gs : List String) -> (cols : List String) ->
146+
Dec (ColsNullSafe env gs cols)
147+
decColsNullSafe env gs [] = Yes NilNS
148+
decColsNullSafe env gs (col :: cols) = case decColNullSafe env gs col of
149+
No nc => No (\(ConsNS c _) => nc c)
150+
Yes c => case decColsNullSafe env gs cols of
151+
Yes cs => Yes (ConsNS c cs)
152+
No ncs => No (\(ConsNS _ cs) => ncs cs)
153+
154+
||| The headline decision procedure: decide query null-safety, returning a
155+
||| genuine `QueryNullSafe` witness when it holds.
156+
public export
157+
decQueryNullSafe : (env : NullEnv) -> (q : Query) -> Dec (QueryNullSafe env q)
158+
decQueryNullSafe env (Select t cols w) = case decColsNullSafe env (guardsOf w) cols of
159+
Yes ok => Yes (SelectNS ok)
160+
No no => No (\(SelectNS ok) => no ok)
161+
162+
--------------------------------------------------------------------------------
163+
-- Certifier soundness: a `Proven` NullSafe status is never a lie
164+
--------------------------------------------------------------------------------
165+
166+
||| Certify the NullSafe (level 4) obligation for a query against a nullable set.
167+
||| `Proven` is emitted only when the decision procedure produced a real proof.
168+
public export
169+
certifyNullSafe : (env : NullEnv) -> (q : Query) -> ProofStatus
170+
certifyNullSafe env q = case decQueryNullSafe env q of
171+
Yes _ => Proven
172+
No _ => Refuted
173+
174+
||| Soundness: if the certifier reports `Proven`, the query really is null-safe.
175+
||| (As `decQueryNullSafe` is a `Dec`, a query that is *not* null-safe can never
176+
||| be reported `Proven`.)
177+
export
178+
certifyNullSafeSound : (env : NullEnv) -> (q : Query) ->
179+
certifyNullSafe env q = Proven -> QueryNullSafe env q
180+
certifyNullSafeSound env q prf with (decQueryNullSafe env q)
181+
certifyNullSafeSound env q prf | Yes ok = ok
182+
certifyNullSafeSound env q Refl | No _ impossible
183+
184+
||| `NullSafe` is level 4 — distinct from InjectionFree (level 5).
185+
export
186+
nullSafeIsLevelFour : levelNat NullSafe = 4
187+
nullSafeIsLevelFour = Refl
188+
189+
||| And it is a strictly different obligation from the Layer-2 theorem
190+
||| (InjectionFree, level 5): their ordinals are not equal.
191+
export
192+
nullSafeNotInjectionFree : levelNat NullSafe = levelNat InjectionFree -> Void
193+
nullSafeNotInjectionFree Refl impossible
194+
195+
--------------------------------------------------------------------------------
196+
-- Positive controls
197+
--------------------------------------------------------------------------------
198+
199+
||| The nullable set for the controls: only `email` may be NULL.
200+
public export
201+
nullableCols : NullEnv
202+
nullableCols = ["email"]
203+
204+
||| `SELECT email FROM users WHERE email = $1`.
205+
||| Projecting nullable `email` is null-safe because the WHERE comparison on
206+
||| `email` guards it (a NULL email is filtered out).
207+
public export
208+
guardedQuery : Query
209+
guardedQuery = Select "users" ["email"] (Cmp "email" (Param 1))
210+
211+
||| Machine-checked: the guarded query is null-safe.
212+
export
213+
guardedQueryNullSafe : QueryNullSafe Invariants.nullableCols Invariants.guardedQuery
214+
guardedQueryNullSafe = SelectNS (ConsNS (Guarded Here) NilNS)
215+
216+
||| …and the certifier reports `Proven` for it (computes to `Proven`).
217+
export
218+
guardedQueryCertifiesProven :
219+
certifyNullSafe Invariants.nullableCols Invariants.guardedQuery = Proven
220+
guardedQueryCertifiesProven = Refl
221+
222+
||| Second positive control: a non-nullable projected column needs no guard.
223+
||| `SELECT id FROM users WHERE email = $1` — `id` is not nullable.
224+
public export
225+
nonNullQuery : Query
226+
nonNullQuery = Select "users" ["id"] (Cmp "email" (Param 1))
227+
228+
export
229+
nonNullQueryNullSafe : QueryNullSafe Invariants.nullableCols Invariants.nonNullQuery
230+
nonNullQueryNullSafe = SelectNS (ConsNS (NotNullable idNotNullable) NilNS)
231+
where
232+
idNotNullable : Not (Elem "id" ["email"])
233+
idNotNullable (There rest) impossible
234+
235+
||| Third positive control: `And` guards via union. `SELECT email ... WHERE
236+
||| id = $1 AND email = $2` — the second conjunct guards `email`.
237+
public export
238+
andGuardedQuery : Query
239+
andGuardedQuery =
240+
Select "users" ["email"]
241+
(And (Cmp "id" (Param 1)) (Cmp "email" (Param 2)))
242+
243+
export
244+
andGuardedQueryCertifiesProven :
245+
certifyNullSafe Invariants.nullableCols Invariants.andGuardedQuery = Proven
246+
andGuardedQueryCertifiesProven = Refl
247+
248+
--------------------------------------------------------------------------------
249+
-- Non-vacuity / negative controls: an unguarded nullable projection has no proof
250+
--------------------------------------------------------------------------------
251+
252+
||| `SELECT email FROM users WHERE id = $1`.
253+
||| Nullable `email` is projected but only `id` is guarded — the returned email
254+
||| may be NULL, so there is no null-safety proof.
255+
public export
256+
unguardedQuery : Query
257+
unguardedQuery = Select "users" ["email"] (Cmp "id" (Param 1))
258+
259+
||| Machine-checked non-vacuity: there is **no** `QueryNullSafe` proof. Were the
260+
||| property vacuous, this would be unprovable; that it holds shows the guard
261+
||| discipline bites.
262+
export
263+
unguardedQueryNotNullSafe :
264+
Not (QueryNullSafe Invariants.nullableCols Invariants.unguardedQuery)
265+
unguardedQueryNotNullSafe (SelectNS (ConsNS ok _)) = case ok of
266+
NotNullable notIn => notIn Here
267+
Guarded g => emailNotInId g
268+
where
269+
emailNotInId : Not (Elem "email" ["id"])
270+
emailNotInId (There rest) impossible
271+
272+
||| And the certifier refuses (computes to `Refuted`, not `Proven`).
273+
export
274+
unguardedQueryCertifiesRefuted :
275+
certifyNullSafe Invariants.nullableCols Invariants.unguardedQuery = Refuted
276+
unguardedQueryCertifiesRefuted = Refl
277+
278+
||| Disjunctive weakening control: `SELECT email ... WHERE email = $1 OR id = $2`.
279+
||| Although the LEFT branch guards `email`, the right branch does not, and `Or`
280+
||| keeps only the intersection — so `email` ends up UNGUARDED. A row could have
281+
||| satisfied `id = $2` with a NULL email. Machine-checked: no proof. This is the
282+
||| case the structural (InjectionFree) view would miss entirely.
283+
public export
284+
orWeakenedQuery : Query
285+
orWeakenedQuery =
286+
Select "users" ["email"]
287+
(Or (Cmp "email" (Param 1)) (Cmp "id" (Param 2)))
288+
289+
export
290+
orWeakenedQueryNotNullSafe :
291+
Not (QueryNullSafe Invariants.nullableCols Invariants.orWeakenedQuery)
292+
orWeakenedQueryNotNullSafe (SelectNS (ConsNS ok _)) = case ok of
293+
NotNullable notIn => notIn Here
294+
Guarded g => emailNotGuarded g
295+
where
296+
-- `guardsOf (Or (Cmp "email" _) (Cmp "id" _)) = inter ["email"] ["id"]`
297+
-- reduces to `[]`, which has no `Elem`.
298+
emailNotGuarded : Not (Elem "email" (inter ["email"] ["id"]))
299+
emailNotGuarded Here impossible
300+
emailNotGuarded (There rest) impossible

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,4 @@ modules = Typedqliser.ABI.Types
1212
, Typedqliser.ABI.Semantics
1313
, Typedqliser.ABI.SchemaBound
1414
, Typedqliser.ABI.TypeCompat
15+
, Typedqliser.ABI.Invariants

0 commit comments

Comments
 (0)