From 8dd9681fadbc3169a53d04959f2231f523639b30 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 18:57:30 +0000 Subject: [PATCH] P3: prove TypeCompat (level 3) as a real operand-type-compatibility guarantee MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Typedqliser/ABI/TypeCompat.idr | 210 ++++++++++++++++++ src/interface/abi/typedqliser-abi.ipkg | 1 + 2 files changed, 211 insertions(+) create mode 100644 src/interface/abi/Typedqliser/ABI/TypeCompat.idr diff --git a/src/interface/abi/Typedqliser/ABI/TypeCompat.idr b/src/interface/abi/Typedqliser/ABI/TypeCompat.idr new file mode 100644 index 0000000..1b63ef1 --- /dev/null +++ b/src/interface/abi/Typedqliser/ABI/TypeCompat.idr @@ -0,0 +1,210 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Semantic proof for TypedQLiser's `TypeCompat` level (level 3: +||| "operand types compatible"). +||| +||| Alongside `Semantics.InjectionFree` (level 5) and `SchemaBound.SchemaBound` +||| (level 2), this makes `TypeCompat` (level 3) a real, machine-checked property +||| over the shared query AST: every comparison in the WHERE predicate compares a +||| column against a value whose type matches the column's declared type. A bound +||| parameter adopts the column's type (so it is always compatible); a literal is +||| `TInt` and a raw string is `TText`, so comparing them against a column of a +||| different type has *no* proof. It provides: +||| +||| 1. a small SQL type universe and a typed column environment; +||| 2. `ValueCompat`/`PredTypeCompat`/`QueryTypeCompat` — the proposition that +||| every comparison's operands are type-compatible (uninhabited on a clash); +||| 3. `decQueryTypeCompat`, a sound + complete `Dec`, so "Proven" is backed by +||| a constructive witness and a type clash can never be certified; +||| 4. a certifier proven sound (`certifyTypeCompatSound`), level-ordinal +||| identity, and positive + negative controls. +||| +||| The query AST (`Query`/`Pred`/`Value`) is reused verbatim from `Semantics`. + +module Typedqliser.ABI.TypeCompat + +import Typedqliser.ABI.Types +import Typedqliser.ABI.Semantics + +%default total + +-------------------------------------------------------------------------------- +-- A minimal SQL type universe + typed column environment +-------------------------------------------------------------------------------- + +||| The column/value types this level distinguishes. +public export +data SqlType = TInt | TText | TBool + +||| A typed column environment: declared columns with their types (the resolved +||| form of a table's schema, as produced by the SchemaBound level). +public export +ColEnv : Type +ColEnv = List (String, SqlType) + +||| Resolve a column's declared type by name (first match wins). +public export +lookupType : String -> ColEnv -> Maybe SqlType +lookupType _ [] = Nothing +lookupType c ((n, ty) :: xs) = if n == c then Just ty else lookupType c xs + +||| `Just` is injective. A top-level function clause (its `Refl` covers cleanly, +||| whereas an inline `case … of Refl` on a resolver equation does not, because +||| coverage does not reduce `lookupType` under a lifted scrutinee). +justInj : Just x = Just y -> x = y +justInj Refl = Refl + +-------------------------------------------------------------------------------- +-- Value/column type compatibility as a genuine proposition +-------------------------------------------------------------------------------- + +||| `ValueCompat ct v` holds when value `v` may be compared against a column of +||| type `ct`. A bound parameter adopts any column type; a literal is `TInt`; a +||| raw splice is `TText`. There is no constructor for a mismatch (e.g. a literal +||| against a `TText` column), so such a `ValueCompat` is uninhabited. +public export +data ValueCompat : (ct : SqlType) -> Value -> Type where + ParamAny : ValueCompat ct (Param i) -- a bound parameter adopts ct + LitInt : ValueCompat TInt (Lit n) -- integer literal ↔ TInt column + SpliceTxt : ValueCompat TText (RawSplice s) -- string splice ↔ TText column + +-- Refutations of the type clashes (single impossible clauses; the value index +-- prunes the non-matching constructors). +litNotText : Not (ValueCompat TText (Lit n)) +litNotText LitInt impossible + +litNotBool : Not (ValueCompat TBool (Lit n)) +litNotBool LitInt impossible + +spliceNotInt : Not (ValueCompat TInt (RawSplice s)) +spliceNotInt SpliceTxt impossible + +spliceNotBool : Not (ValueCompat TBool (RawSplice s)) +spliceNotBool SpliceTxt impossible + +||| Sound + complete decision for one value against a column type. +public export +decValueCompat : (ct : SqlType) -> (v : Value) -> Dec (ValueCompat ct v) +decValueCompat _ (Param i) = Yes ParamAny +decValueCompat TInt (Lit n) = Yes LitInt +decValueCompat TText (Lit n) = No litNotText +decValueCompat TBool (Lit n) = No litNotBool +decValueCompat TInt (RawSplice s) = No spliceNotInt +decValueCompat TText (RawSplice s) = Yes SpliceTxt +decValueCompat TBool (RawSplice s) = No spliceNotBool + +||| A predicate is type-compatible (w.r.t. an environment) when every comparison +||| resolves its column's type and the compared value matches that type. +public export +data PredTypeCompat : (env : ColEnv) -> Pred -> Type where + CmpTC : (colType : lookupType col env = Just ct) -> ValueCompat ct v -> + PredTypeCompat env (Cmp col v) + AndTC : PredTypeCompat env p -> PredTypeCompat env q -> PredTypeCompat env (And p q) + OrTC : PredTypeCompat env p -> PredTypeCompat env q -> PredTypeCompat env (Or p q) + +||| Sound + complete decision for predicate type-compatibility. The `Cmp` case +||| resolves the column type via a `proof`-bound equation, exactly as the +||| SchemaBound level resolves table columns. +public export +decPredTypeCompat : (env : ColEnv) -> (p : Pred) -> Dec (PredTypeCompat env p) +decPredTypeCompat env (Cmp col v) with (lookupType col env) proof eq + _ | Nothing = No $ \(CmpTC colType _) => case trans (sym eq) colType of Refl impossible + _ | Just ct = case decValueCompat ct v of + Yes vc => Yes (CmpTC eq vc) + No nvc => No $ \(CmpTC colType vc) => case trans (sym colType) eq of Refl => nvc vc +decPredTypeCompat env (And p q) = case decPredTypeCompat env p of + No np => No (\(AndTC pp _) => np pp) + Yes pp => case decPredTypeCompat env q of + Yes qq => Yes (AndTC pp qq) + No nq => No (\(AndTC _ qq) => nq qq) +decPredTypeCompat env (Or p q) = case decPredTypeCompat env p of + No np => No (\(OrTC pp _) => np pp) + Yes pp => case decPredTypeCompat env q of + Yes qq => Yes (OrTC pp qq) + No nq => No (\(OrTC _ qq) => nq qq) + +||| A query is type-compatible when its WHERE predicate is. +public export +data QueryTypeCompat : (env : ColEnv) -> Query -> Type where + MkQTC : PredTypeCompat env w -> QueryTypeCompat env (Select t sel w) + +||| The headline decision procedure for the query level. +public export +decQueryTypeCompat : (env : ColEnv) -> (q : Query) -> Dec (QueryTypeCompat env q) +decQueryTypeCompat env (Select t sel w) = case decPredTypeCompat env w of + Yes pc => Yes (MkQTC pc) + No npc => No (\(MkQTC pc) => npc pc) + +-------------------------------------------------------------------------------- +-- Certifier soundness: a `Proven` TypeCompat status is never a lie +-------------------------------------------------------------------------------- + +||| Certify the TypeCompat (level 3) obligation for a query against a typed +||| environment. `Proven` only when the decision procedure produced a real proof. +public export +certifyTypeCompat : (env : ColEnv) -> (q : Query) -> ProofStatus +certifyTypeCompat env q = case decQueryTypeCompat env q of + Yes _ => Proven + No _ => Refuted + +||| Soundness: a `Proven` verdict entails the property. With `decQueryTypeCompat` +||| being a `Dec`, a type-incompatible query can never be reported `Proven`. +export +certifyTypeCompatSound : (env : ColEnv) -> (q : Query) -> + certifyTypeCompat env q = Proven -> QueryTypeCompat env q +certifyTypeCompatSound env q prf with (decQueryTypeCompat env q) + certifyTypeCompatSound env q prf | Yes ok = ok + certifyTypeCompatSound env q Refl | No _ impossible + +||| `TypeCompat` is level 3 — the certified obligation is the third of ten. +export +typeCompatIsLevelThree : levelNat TypeCompat = 3 +typeCompatIsLevelThree = Refl + +-------------------------------------------------------------------------------- +-- Positive control: a well-typed query is provably type-compatible +-------------------------------------------------------------------------------- + +||| `users(id : Int, name : Text, age : Int)`. +public export +exampleEnv : ColEnv +exampleEnv = [("id", TInt), ("name", TText), ("age", TInt)] + +||| `SELECT id, name FROM users WHERE age = 18 AND name = $1` — `age` (Int) vs an +||| integer literal, and `name` (Text) vs a bound parameter: both compatible. +public export +goodQuery : Query +goodQuery = + Select "users" ["id", "name"] (And (Cmp "age" (Lit 18)) (Cmp "name" (Param 1))) + +||| Machine-checked: the query is type-compatible against `exampleEnv`. +export +goodQueryTypeCompat : QueryTypeCompat TypeCompat.exampleEnv TypeCompat.goodQuery +goodQueryTypeCompat = MkQTC (AndTC (CmpTC Refl LitInt) (CmpTC Refl ParamAny)) + +||| …and the certifier reports `Proven` for it (computes to `Proven`). +export +goodQueryCertifiesProven : + certifyTypeCompat TypeCompat.exampleEnv TypeCompat.goodQuery = Proven +goodQueryCertifiesProven = Refl + +-------------------------------------------------------------------------------- +-- Negative control: a type clash CANNOT be certified +-------------------------------------------------------------------------------- + +||| `SELECT id FROM users WHERE name = 42` — comparing a `Text` column against an +||| integer literal is a type clash. +public export +badQuery : Query +badQuery = Select "users" ["id"] (Cmp "name" (Lit 42)) + +||| Machine-checked: there is **no** proof that the clash is type-compatible. +||| `name` resolves to `TText`, but `ValueCompat TText (Lit 42)` is uninhabited, +||| so the property is genuinely refuted (this is what makes it non-vacuous). +||| The witness is transported at the term level (`replace`/`justInj`) rather +||| than via `case … of Refl`, which coverage rejects on the stuck resolver LHS. +export +badQueryNotTypeCompat : Not (QueryTypeCompat TypeCompat.exampleEnv TypeCompat.badQuery) +badQueryNotTypeCompat (MkQTC (CmpTC {ct} colType vc)) = + litNotText (replace {p = \x => ValueCompat x (Lit 42)} (sym (justInj colType)) vc) diff --git a/src/interface/abi/typedqliser-abi.ipkg b/src/interface/abi/typedqliser-abi.ipkg index 65241c3..f9ca4a1 100644 --- a/src/interface/abi/typedqliser-abi.ipkg +++ b/src/interface/abi/typedqliser-abi.ipkg @@ -11,3 +11,4 @@ modules = Typedqliser.ABI.Types , Typedqliser.ABI.Proofs , Typedqliser.ABI.Semantics , Typedqliser.ABI.SchemaBound + , Typedqliser.ABI.TypeCompat