Skip to content

Commit 0b4089c

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
P3: prove SchemaBound (level 2) as a real schema-resolution guarantee (#35)
Extends the flagship semantic-proof coverage beyond InjectionFree (level 5) to SchemaBound (level 2: "all references resolve in the schema"). Adds `Typedqliser.ABI.SchemaBound`, mirroring the Semantics/InjectionFree quality bar: * a faithful schema model (`TableDef`/`Schema`) with a total, deterministic `tableCols` resolver, reusing the existing `Query`/`Pred`/`Value` AST; * `QuerySchemaBound` — the proposition that the query's table resolves and every referenced column (projected ++ predicate) is declared. There is no constructor admitting a dangling reference, so the property is uninhabited for an unresolved column; * `decSchemaBound` — a sound + complete `Dec`, so a "Proven" SchemaBound certificate is backed by a constructive witness and a dangling reference can never be certified; * `certifySchemaBoundSound` — the certifier's `Proven` verdict provably entails the property; `schemaBoundIsLevelTwo : levelNat SchemaBound = 2`; * positive control (an explicit witness + the certifier computing to `Proven`) and negative control (`ssn` dangling reference provably cannot be certified). Verified with idris2 0.7.0: `idris2 --build typedqliser-abi.ipkg` exits 0 with zero warnings. Adversarially checked — three deliberately-false proofs (wrong level ordinal, a dangling `Elem`, a schema-bound witness for the dangling query) are all rejected by the type checker. Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx Co-authored-by: Claude <noreply@anthropic.com>
1 parent 6d367ae commit 0b4089c

2 files changed

Lines changed: 208 additions & 0 deletions

File tree

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

Lines changed: 207 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,207 @@
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 `SchemaBound` level (level 2:
5+
||| "all references resolve in the schema").
6+
|||
7+
||| Where `Semantics.idr` makes `InjectionFree` (level 5) a real, machine-checked
8+
||| property, this module does the same for `SchemaBound` (level 2): a query is
9+
||| schema-bound when its table resolves in a schema and *every* column it
10+
||| references — both the projected columns and those mentioned in the WHERE
11+
||| predicate — is declared for that table. It provides:
12+
|||
13+
||| 1. a `Schema` of table definitions (name + declared columns);
14+
||| 2. `QuerySchemaBound`, the proposition that the query's table resolves and
15+
||| all referenced columns are declared;
16+
||| 3. `decSchemaBound`, a sound + complete decision procedure returning a
17+
||| genuine `Dec`, so a "Proven" SchemaBound certificate is backed by a
18+
||| constructive witness and a dangling reference can never be certified;
19+
||| 4. a certifier whose `Proven` verdict is *proven* to entail the property
20+
||| (`certifySchemaBoundSound`), plus positive and negative controls.
21+
|||
22+
||| The query AST (`Query`/`Pred`/`Value`) is reused verbatim from `Semantics`.
23+
24+
module Typedqliser.ABI.SchemaBound
25+
26+
import Typedqliser.ABI.Types
27+
import Typedqliser.ABI.Semantics
28+
import Data.List
29+
import Data.List.Elem
30+
import Decidable.Equality
31+
32+
%default total
33+
34+
--------------------------------------------------------------------------------
35+
-- A minimal but faithful schema model
36+
--------------------------------------------------------------------------------
37+
38+
||| One table: its name and the columns it declares.
39+
public export
40+
record TableDef where
41+
constructor MkTable
42+
tableName : String
43+
tableColumns : List String
44+
45+
||| A schema is a list of table definitions.
46+
public export
47+
Schema : Type
48+
Schema = List TableDef
49+
50+
||| Resolve a table's declared columns by name (first match wins, as in a real
51+
||| catalogue with unique table names). `Nothing` when the table is absent.
52+
public export
53+
tableCols : String -> Schema -> Maybe (List String)
54+
tableCols _ [] = Nothing
55+
tableCols t (MkTable nm cs :: rest) = if nm == t then Just cs else tableCols t rest
56+
57+
||| Every column a predicate references in a comparison.
58+
public export
59+
predRefs : Pred -> List String
60+
predRefs (Cmp col _) = [col]
61+
predRefs (And p q) = predRefs p ++ predRefs q
62+
predRefs (Or p q) = predRefs p ++ predRefs q
63+
64+
--------------------------------------------------------------------------------
65+
-- "Every reference is a declared column" as a genuine proposition
66+
--------------------------------------------------------------------------------
67+
68+
||| `AllBound cols refs` holds when every name in `refs` is an element of `cols`.
69+
||| There is no constructor that admits a `ref` absent from `cols`, so a dangling
70+
||| reference makes the proposition uninhabited.
71+
public export
72+
data AllBound : (cols : List String) -> (refs : List String) -> Type where
73+
ABNil : AllBound cols []
74+
ABCons : Elem r cols -> AllBound cols rs -> AllBound cols (r :: rs)
75+
76+
||| Sound + complete decision for `AllBound`, structurally over `refs`.
77+
public export
78+
decAllBound : (cols : List String) -> (refs : List String) -> Dec (AllBound cols refs)
79+
decAllBound _ [] = Yes ABNil
80+
decAllBound cols (r :: rs) = case isElem r cols of
81+
No nel => No (\(ABCons el _) => nel el)
82+
Yes el => case decAllBound cols rs of
83+
Yes rest => Yes (ABCons el rest)
84+
No nrest => No (\(ABCons _ rest) => nrest rest)
85+
86+
||| A query is schema-bound when its table resolves to some declared column set
87+
||| `cols`, and all referenced columns (projected ++ predicate) are in `cols`.
88+
||| The stored `tableCols t s = Just cols` equation pins `cols` to the (total,
89+
||| deterministic) resolver — so completeness needs no separate uniqueness lemma.
90+
public export
91+
data QuerySchemaBound : Schema -> Query -> Type where
92+
MkSB :
93+
(cols : List String) ->
94+
(resolves : tableCols t s = Just cols) ->
95+
AllBound cols (sel ++ predRefs w) ->
96+
QuerySchemaBound s (Select t sel w)
97+
98+
--------------------------------------------------------------------------------
99+
-- Sound + complete decision procedure (returns a real proof)
100+
--------------------------------------------------------------------------------
101+
102+
||| Decide schema-boundedness, returning a genuine `QuerySchemaBound` witness
103+
||| when it holds. The `proof eq` binding gives the resolver equation both the
104+
||| `Yes` witness and the `No` refutation need.
105+
public export
106+
decSchemaBound : (s : Schema) -> (q : Query) -> Dec (QuerySchemaBound s q)
107+
decSchemaBound s (Select t sel w) with (tableCols t s) proof eq
108+
_ | Nothing = No $ \(MkSB cols prf _) => case trans (sym eq) prf of Refl impossible
109+
_ | Just cs = case decAllBound cs (sel ++ predRefs w) of
110+
Yes ab => Yes (MkSB cs eq ab)
111+
No nab => No $ \(MkSB cols prf ab) => case trans (sym prf) eq of Refl => nab ab
112+
113+
--------------------------------------------------------------------------------
114+
-- Certifier soundness: a `Proven` SchemaBound status is never a lie
115+
--------------------------------------------------------------------------------
116+
117+
||| Certify the SchemaBound (level 2) obligation for a query against a schema.
118+
||| `Proven` is emitted only when the decision procedure produced a real proof.
119+
public export
120+
certifySchemaBound : (s : Schema) -> (q : Query) -> ProofStatus
121+
certifySchemaBound s q = case decSchemaBound s q of
122+
Yes _ => Proven
123+
No _ => Refuted
124+
125+
||| Soundness: if the certifier reports `Proven`, the query really is schema-bound
126+
||| against that schema. With `decSchemaBound` being a `Dec`, a query that is not
127+
||| schema-bound can therefore never be reported `Proven`.
128+
export
129+
certifySchemaBoundSound : (s : Schema) -> (q : Query) ->
130+
certifySchemaBound s q = Proven -> QuerySchemaBound s q
131+
certifySchemaBoundSound s q prf with (decSchemaBound s q)
132+
certifySchemaBoundSound s q prf | Yes ok = ok
133+
certifySchemaBoundSound s q Refl | No _ impossible
134+
135+
||| `SchemaBound` is level 2 — the certified obligation is the second of ten.
136+
export
137+
schemaBoundIsLevelTwo : levelNat SchemaBound = 2
138+
schemaBoundIsLevelTwo = Refl
139+
140+
--------------------------------------------------------------------------------
141+
-- Positive control: a query over declared columns is provably schema-bound
142+
--------------------------------------------------------------------------------
143+
144+
||| A one-table schema: `users(id, name, email)`.
145+
public export
146+
exampleSchema : Schema
147+
exampleSchema = [MkTable "users" ["id", "name", "email"]]
148+
149+
||| `SELECT id, name FROM users WHERE email = $1` — all references declared.
150+
public export
151+
boundQuery : Query
152+
boundQuery = Select "users" ["id", "name"] (Cmp "email" (Param 1))
153+
154+
||| Machine-checked: the query is schema-bound against `exampleSchema`.
155+
export
156+
boundQuerySchemaBound : QuerySchemaBound SchemaBound.exampleSchema SchemaBound.boundQuery
157+
boundQuerySchemaBound =
158+
MkSB ["id", "name", "email"] Refl
159+
(ABCons Here (ABCons (There Here) (ABCons (There (There Here)) ABNil)))
160+
161+
||| …and the certifier reports `Proven` for it (computes to `Proven`).
162+
export
163+
boundQueryCertifiesProven :
164+
certifySchemaBound SchemaBound.exampleSchema SchemaBound.boundQuery = Proven
165+
boundQueryCertifiesProven = Refl
166+
167+
--------------------------------------------------------------------------------
168+
-- Negative control: a dangling column reference CANNOT be certified
169+
--------------------------------------------------------------------------------
170+
171+
||| `ssn` is not a declared column of `users`.
172+
ssnNotInUsers : Not (Elem "ssn" ["id", "name", "email"])
173+
ssnNotInUsers Here impossible
174+
ssnNotInUsers (There Here) impossible
175+
ssnNotInUsers (There (There Here)) impossible
176+
ssnNotInUsers (There (There (There later))) = absurd later
177+
178+
||| The reference list `["id", "ssn", "id"]` is not all-bound by `users`'s
179+
||| columns, because `ssn` is not among them. A top-level helper (rather than a
180+
||| nested `case`) so coverage is checked against the concrete reference list.
181+
noSsnBound : Not (AllBound ["id", "name", "email"] ["id", "ssn", "id"])
182+
noSsnBound (ABCons _ (ABCons ssnEl _)) = ssnNotInUsers ssnEl
183+
184+
||| `Just` is injective. A top-level function clause (its `Refl` covers cleanly,
185+
||| whereas an inline `case … of Refl` on the resolver equation does not, because
186+
||| coverage does not reduce `tableCols` under the lifted case scrutinee).
187+
justInj : Just x = Just y -> x = y
188+
justInj Refl = Refl
189+
190+
||| `SELECT id, ssn FROM users WHERE id = $1` — `ssn` is a dangling reference.
191+
public export
192+
unboundQuery : Query
193+
unboundQuery = Select "users" ["id", "ssn"] (Cmp "id" (Param 1))
194+
195+
||| Machine-checked: there is **no** proof that the query is schema-bound — the
196+
||| dangling `ssn` reference has no `Elem` witness, so the property is genuinely
197+
||| refuted (this is what makes the guarantee non-vacuous).
198+
export
199+
unboundQueryNotSchemaBound : Not (QuerySchemaBound SchemaBound.exampleSchema SchemaBound.unboundQuery)
200+
unboundQueryNotSchemaBound (MkSB cols prf ab) =
201+
-- Transport `ab` along `cols = ["id","name","email"]` (derived by injectivity
202+
-- from the resolver equation) at the term level — no `case … of Refl`, so the
203+
-- coverage checker never has to reduce `tableCols` under a lifted scrutinee.
204+
noSsnBound
205+
(replace {p = \c => AllBound c ["id", "ssn", "id"]}
206+
(sym (justInj (the (Just ["id", "name", "email"] = Just cols) prf)))
207+
ab)

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ modules = Typedqliser.ABI.Types
1010
, Typedqliser.ABI.Foreign
1111
, Typedqliser.ABI.Proofs
1212
, Typedqliser.ABI.Semantics
13+
, Typedqliser.ABI.SchemaBound

0 commit comments

Comments
 (0)