vcl-ut HOLE: de-vacuize L4 SQL-injection predicate + machine-verified model + honest stance

PROOF-NEEDS.md

@@ -5,8 +5,9 @@
 
 - **LOC**: ~8,000
 - **Languages**: Rust, ReScript, Idris2, Zig
-- **Existing ABI proofs**: `src/interface/abi/*.idr` (template-level) + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`
-- **Dangerous patterns**: None detected
+- **Existing ABI proofs**: `src/interface/abi/*.idr` + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`, `Composition.idr`
+- **Machine-verified**: `verification/proofs/SafetyL4Model.idr` only (idris2 0.8.0 `--check`, exit 0, zero proof escapes) — the Level-4 SQL-injection remediation
+- **Dangerous patterns**: ⚠️ The `src/core/**` Idris2 corpus **does not compile** on `origin/main` and has **never been machine-checked** (no `.ipkg`/CI). `ABI.Types` has ≥4 type errors; `Grammar.idr` forward-references types with no `mutual` block. L2/L3/L5 safety predicates are **vacuous** (inhabited for any input, incl. injection); `SafetyCertificate` is never constructed by `checkQuery`; the Zig FFI is a `SELECT`-substring stub. See `verification/proofs/VERIFICATION-STANCE.adoc` for the authoritative, proof-backed catalogue. The earlier "None detected" line was wrong.
 
 ## What Needs Proving
 
@@ -19,6 +20,8 @@
 - Prove: parser (ReScript side) accepts exactly the Idris2-specified grammar
 
 ### Level System (src/core/Levels.idr)
+- ✅ L4 `NoRawUserInput` de-vacuized + `checkLevel4Sound` + `noRawUserInputCompose` (verified in `verification/proofs/SafetyL4Model.idr`)
+- ⚠️ L2/L3/L5 predicates still vacuous — de-vacuize with evidence-carrying constructors and prove each `checkLevelN` sound (as done for L4)
 - 10-level type safety hierarchy — prove level ordering is a lattice
 - Prove: level promotion/demotion preserves query safety
 

src/core/Checker.idr

@@ -19,6 +19,7 @@ module VclTotal.Core.Checker
 import VclTotal.ABI.Types
 import VclTotal.Core.Grammar
 import VclTotal.Core.Schema
+import VclTotal.Core.Levels
 import Data.List
 import Data.Maybe
 
@@ -208,18 +209,14 @@ resolveExprType (EAnnounce _ _ _ ty) _   = ty
 
 ||| Check whether an expression contains any ELiteral (LitString _) nodes.
 ||| Used by Level 4 to detect potential injection vectors.
+|||
+||| This is now a thin alias for `Grammar.hasStringLit`, the single
+||| source of truth shared with the Level-4 proof predicate
+||| (`Levels.NoRawUserInput`). Keeping one definition is what makes
+||| `checkLevel4Sound` a genuine soundness proof rather than a check
+||| against a parallel re-implementation that could silently drift.
 containsLiteralString : Expr -> Bool
-containsLiteralString (ELiteral (LitString _) _) = True
-containsLiteralString (ECompare _ l r _)          =
-  containsLiteralString l || containsLiteralString r
-containsLiteralString (ELogic _ l Nothing _)      = containsLiteralString l
-containsLiteralString (ELogic _ l (Just r) _)     =
-  containsLiteralString l || containsLiteralString r
-containsLiteralString (EAggregate _ e _)           = containsLiteralString e
-containsLiteralString (EEpistemic _ _ e _)         = containsLiteralString e
-containsLiteralString (EAnnounce _ p b _)          =
-  containsLiteralString p || containsLiteralString b
-containsLiteralString _                            = False
+containsLiteralString = hasStringLit
 
 ||| Resolve the type of a SelectItem using the schema.
 ||| Returns TAny if the item's type cannot be determined.
@@ -357,13 +354,36 @@ checkLevel3 stmt schema =
 ||| @return (True, _) if WHERE contains no literal strings; (False, diagnostic) otherwise.
 public export
 checkLevel4 : Statement -> (Bool, String)
-checkLevel4 stmt =
-  case whereClause stmt of
-    Nothing => (True, "L4:InjectionProof — no WHERE clause, no injection risk")
-    Just wExpr =>
-      if containsLiteralString wExpr
-        then (False, "L4:InjectionProof FAILED — raw string literal in WHERE clause")
-        else (True, "L4:InjectionProof — WHERE uses only parameterised inputs")
+checkLevel4 stmt = l4Verdict (whereHasStringLit stmt)
+  where
+    l4Verdict : Bool -> (Bool, String)
+    l4Verdict True  =
+      (False, "L4:InjectionProof FAILED — raw string literal in WHERE clause")
+    l4Verdict False =
+      (True,  "L4:InjectionProof — WHERE uses only parameterised inputs")
+
+||| Disjointness of Bool constructors (local, to avoid relying on a
+||| particular Prelude `Uninhabited` instance name across idris2 0.8.0).
+falseNotTrue : (False = True) -> Void
+falseNotTrue Refl impossible
+
+||| **Soundness of the Level-4 decision procedure.**
+|||
+||| If `checkLevel4` accepts a statement, that statement genuinely
+||| carries an `L4_InjectionProof` — its WHERE clause provably embeds no
+||| string literal (`whereHasStringLit stmt = False`). This lemma is what
+||| connects the *real* (no longer vacuous) Level-4 predicate to the
+||| actual decision procedure. Before this remediation `checkLevel4`
+||| returned a bare `Bool` while `NoRawUserInput` was inhabited by the
+||| catch-all `AllParameterised`, so no soundness statement was even
+||| meaningful: a pure string-interpolation injection query type-checked
+||| at Level 4. Tracked: hyperpolymath/standards#124.
+export
+checkLevel4Sound : (stmt : Statement) -> (m : String) ->
+                   checkLevel4 stmt = (True, m) -> L4_InjectionProof stmt
+checkLevel4Sound stmt m prf with (whereHasStringLit stmt) proof p
+  checkLevel4Sound stmt m prf | False = MkL4 stmt (MkNoRawUserInput p)
+  checkLevel4Sound stmt m prf | True  = void (falseNotTrue (cong fst prf))
 
 ||| Level 5 — ResultTyped: every SELECT item resolves to a known type
 ||| (not TAny). Ensures the result set schema is fully determined.

src/core/Composition.idr

@@ -519,6 +519,42 @@ l10Compose (MkL10 _ (EpClause as1 rs1) prf1) (MkL10 _ (EpClause as2 rs2) prf2) =
   MkL10 (composeJoin _ _) (EpClause (as1 ++ as2) (rs1 ++ rs2)) $
     rewrite prf1 in rewrite prf2 in Refl
 
+-- ── L4 injection-freedom is genuinely closed under join ──────────────
+
+||| Level-4 injection-freedom is **genuinely** preserved by join
+||| composition — not merely vacuously, as it was when `NoRawUserInput`
+||| had the catch-all `AllParameterised` constructor.
+|||
+||| `joinWhere` (Composition.idr) maps the two WHERE clauses to one of:
+||| `Nothing`, one side verbatim, or `ELogic And w1 (Just w2) TBool`.
+||| None of these introduces a string literal that was not already in
+||| `w1` or `w2`, so `hasStringLit` of the joined clause is exactly the
+||| disjunction of the two sides — `False` whenever both inputs are
+||| injection-free. No `believe_me`/`postulate`/`assert_total`.
+export
+noRawUserInputCompose :
+  (q1, q2 : Statement) ->
+  NoRawUserInput q1 -> NoRawUserInput q2 ->
+  NoRawUserInput (composeJoin q1 q2)
+noRawUserInputCompose q1 q2 (MkNoRawUserInput n1) (MkNoRawUserInput n2) =
+  MkNoRawUserInput (joinFree (whereClause q1) (whereClause q2) n1 n2)
+  where
+    -- `whereHasStringLit s` reduces to `maybe False hasStringLit
+    -- (whereClause s)`; `whereClause (composeJoin q1 q2)` reduces to
+    -- `joinWhere (whereClause q1) (whereClause q2)`.  So the goal is
+    -- exactly `joinFree (whereClause q1) (whereClause q2) n1 n2`.
+    joinFree :
+      (w1m, w2m : Maybe Expr) ->
+      maybe False hasStringLit w1m = False ->
+      maybe False hasStringLit w2m = False ->
+      maybe False hasStringLit (joinWhere w1m w2m) = False
+    joinFree Nothing   Nothing   _  _  = Refl
+    joinFree (Just _)  Nothing   p1 _  = p1
+    joinFree Nothing   (Just _)  _  p2 = p2
+    joinFree (Just a)  (Just b)  p1 p2 =
+      -- goal reduces to: hasStringLit a || hasStringLit b = False
+      rewrite p1 in p2
+
 -- ── The main theorem ─────────────────────────────────────────────────
 
 ||| Theorem [Composition Preservation]
@@ -575,28 +611,33 @@ compositionPreservation _ _ schema NullSafe _
          (MkL2 (composeJoin _ _) schema (WhereTypeSafe LogicSafe))
          (MkL3 (composeJoin _ _) schema GuardedNull)
 
-compositionPreservation _ _ schema InjectionProof _
-    (CertL4 _ l1a _ _ _)
-    (CertL4 _ l1b _ _ _) =
-  -- L4: AllParameterised holds for any statement (it asserts all user values
-  -- come through EParam, a structural invariant maintained by the parser;
-  -- composeJoin does not introduce raw user input).
+compositionPreservation q1 q2 schema InjectionProof _
+    (CertL4 _ l1a _ _ (MkL4 _ nri1))
+    (CertL4 _ l1b _ _ (MkL4 _ nri2)) =
+  -- L4: GENUINE compositional proof. `joinWhere` either keeps one side
+  -- verbatim or combines with `ELogic And`, introducing no new string
+  -- literal, so injection-freedom of both inputs gives injection-freedom
+  -- of the join (noRawUserInputCompose). This replaces the previous
+  -- `MkL4 _ AllParameterised`, which type-checked only because the
+  -- Level-4 predicate was vacuous. See standards#124.
   CertL4 (MkL0 (composeJoin _ _))
          (l1Compose l1a l1b)
          (MkL2 (composeJoin _ _) schema (WhereTypeSafe LogicSafe))
          (MkL3 (composeJoin _ _) schema GuardedNull)
-         (MkL4 (composeJoin _ _) AllParameterised)
-
-compositionPreservation _ _ schema ResultTyped _
-    (CertL5 _ l1a _ _ _ _)
-    (CertL5 _ l1b _ _ _ _) =
-  -- L5: the combined select list is typed item-by-item;
-  -- ConsTyped/NilTyped witnesses hold for any list structure.
+         (MkL4 (composeJoin q1 q2) (noRawUserInputCompose q1 q2 nri1 nri2))
+
+compositionPreservation q1 q2 schema ResultTyped _
+    (CertL5 _ l1a _ _ (MkL4 _ nri1) _)
+    (CertL5 _ l1b _ _ (MkL4 _ nri2) _) =
+  -- L5: the L4 sub-certificate is now the GENUINE
+  -- noRawUserInputCompose proof (not the old vacuous AllParameterised).
+  -- L5's own ConsTyped/NilTyped witnesses remain structurally vacuous
+  -- and are scoped OWED in verification/proofs/VERIFICATION-STANCE.adoc.
   CertL5 (MkL0 (composeJoin _ _))
          (l1Compose l1a l1b)
          (MkL2 (composeJoin _ _) schema (WhereTypeSafe LogicSafe))
          (MkL3 (composeJoin _ _) schema GuardedNull)
-         (MkL4 (composeJoin _ _) AllParameterised)
+         (MkL4 (composeJoin q1 q2) (noRawUserInputCompose q1 q2 nri1 nri2))
          (MkL5 (composeJoin _ _) schema (selectItemsTypedCompose _ _))
   where
     -- Combined select items are typed because each piece is typed

src/core/Grammar.idr

@@ -319,6 +319,38 @@ record Statement where
   -- Metadata
   requestedLevel : SafetyLevel
 
+-- ═══════════════════════════════════════════════════════════════════════
+-- Injection-safety primitive (canonical single source of truth)
+-- ═══════════════════════════════════════════════════════════════════════
+
+||| Whether an expression embeds a string literal anywhere in its tree.
+|||
+||| A string literal in a predicate position is the canonical SQL-injection
+||| vector: user-controlled text concatenated into the query instead of
+||| being bound through an `EParam` placeholder. The Level-4 injection
+||| witness (`Levels.NoRawUserInput`) is defined as the *negation* of this
+||| over the WHERE clause, and `Checker.checkLevel4` decides it. Keeping
+||| the function here (in Grammar, the AST home) makes it the single
+||| source of truth shared by the proof predicate and the decision
+||| procedure, so the soundness lemma is a direct equality, not a
+||| re-implementation that could drift.
+public export
+hasStringLit : Expr -> Bool
+hasStringLit (ELiteral (LitString _) _) = True
+hasStringLit (ECompare _ l r _)         = hasStringLit l || hasStringLit r
+hasStringLit (ELogic _ l Nothing _)     = hasStringLit l
+hasStringLit (ELogic _ l (Just r) _)    = hasStringLit l || hasStringLit r
+hasStringLit (EAggregate _ e _)         = hasStringLit e
+hasStringLit (EEpistemic _ _ e _)       = hasStringLit e
+hasStringLit (EAnnounce _ p b _)        = hasStringLit p || hasStringLit b
+hasStringLit _                          = False
+
+||| The WHERE clause of a statement embeds a string literal. `Nothing`
+||| (no WHERE) is injection-free by construction.
+public export
+whereHasStringLit : Statement -> Bool
+whereHasStringLit stmt = maybe False hasStringLit (whereClause stmt)
+
 -- ═══════════════════════════════════════════════════════════════════════
 -- Well-Formedness Predicates
 -- ═══════════════════════════════════════════════════════════════════════

src/core/Levels.idr

@@ -178,11 +178,26 @@ data AllNullableFieldsGuarded : Maybe Expr -> OctadSchema -> Type where
   NoWhereNull : AllNullableFieldsGuarded Nothing schema
   GuardedNull : AllNullableFieldsGuarded (Just expr) schema
 
-||| Proof that no raw user input appears in the query.
-||| User values must be EParam nodes, not embedded in strings.
+||| Proof that no raw user input appears in the query's WHERE clause.
+||| User values must arrive via `EParam` nodes, never as embedded string
+||| literals (the canonical SQL-injection vector).
+|||
+||| HISTORY (standards#124, vcl-ut HOLE remediation): this used to be
+|||
+|||   data NoRawUserInput : Statement -> Type where
+|||     AllParameterised : NoRawUserInput stmt
+|||
+||| which is *vacuous* — `AllParameterised` inhabits `NoRawUserInput stmt`
+||| for *every* statement, including one whose WHERE is pure string
+||| interpolation. Level 4 therefore proved nothing about the property it
+||| names. It now carries real structural evidence: the WHERE clause
+||| embeds no string literal (`Grammar.whereHasStringLit stmt = False`).
+||| `Checker.checkLevel4` decides exactly this predicate
+||| (see `checkLevel4Sound`), and it is genuinely closed under join
+||| composition (see `Composition.noRawUserInputCompose`).
 public export
 data NoRawUserInput : Statement -> Type where
-  AllParameterised : NoRawUserInput stmt
+  MkNoRawUserInput : whereHasStringLit stmt = False -> NoRawUserInput stmt
 
 ||| Proof that all select items have known types.
 public export

verification/proofs/README.adoc

@@ -1 +1,31 @@
 = Proofs Unit
+
+// SPDX-License-Identifier: PMPL-1.0-or-later
+
+This directory holds the *machine-verified* proof artefacts for vcl-ut.
+
+== Contents
+
+`SafetyL4Model.idr`::
+  Self-contained, idris2 0.8.0 `--check`-clean (exit 0, `%default total`,
+  zero proof-escape symbols) model of the Level-4 SQL-injection safety
+  remediation: the de-vacuized `NoRawUserInput` predicate, the checker
+  soundness lemma `checkLevel4Sound`, a negative injection test, and the
+  genuine compositionality proof `noRawUserInputCompose`.
+
+`VERIFICATION-STANCE.adoc`::
+  The authoritative, proof-backed statement of what is and is not
+  verified. *Read this before trusting any "verified"/"type-safe"
+  phrasing elsewhere in the repo.* It documents that the shipped
+  `src/core/**` corpus does not compile on `origin/main` and has never
+  been machine-checked, and gives the phased remediation roadmap.
+
+== Verifying
+
+[source,sh]
+----
+export IDRIS2_PREFIX=<idris2-0.8.0-prefix>
+idris2 --check verification/proofs/SafetyL4Model.idr   # expect exit 0
+----
+
+Tracked under hyperpolymath/standards#124.