Skip to content

Commit 81f8e33

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
vcl-ut: machine-verified L4 model + brutally honest proof-backed stance
verification/proofs/SafetyL4Model.idr — idris2 0.8.0 --check exit 0, %default total, ZERO believe_me/postulate/assert_total/sorry. Proves the de-vacuized NoRawUserInput, checkLevel4Sound (checker soundness), an injection-rejection negative test, and noRawUserInputCompose (genuine compositionality), against a byte-faithful self-contained model of the relevant AST fragment. Why a standalone harness: the shipped src/core/** corpus DOES NOT COMPILE on origin/main and has never been machine-checked (no ipkg/CI): ABI.Types has >=4 type errors (missing Decidable.Equality; malformed enum DecEq; CPtr=Bits n ill-typed; createQueryHandle missing So witness; thisPlatform %runElab w/o pragma); Grammar.idr forward-references Statement/EpistemicRequirement with no mutual block. The in-repo L4 fix (prior commit) is content-identical to the verified model but unverifiable in situ until the corpus is resurrected. - verification/proofs/VERIFICATION-STANCE.adoc: authoritative proof-backed stance; supersedes doc-only PR #19; full OWED catalogue + phased roadmap. - verification/proofs/README.adoc, PROOF-NEEDS.md: corrected (the 'Dangerous patterns: None detected' / 'high value low effort' lines were false). Refs hyperpolymath/standards#124 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 1c177cf commit 81f8e33

4 files changed

Lines changed: 319 additions & 2 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,9 @@
55

66
- **LOC**: ~8,000
77
- **Languages**: Rust, ReScript, Idris2, Zig
8-
- **Existing ABI proofs**: `src/interface/abi/*.idr` (template-level) + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`
9-
- **Dangerous patterns**: None detected
8+
- **Existing ABI proofs**: `src/interface/abi/*.idr` + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`, `Composition.idr`
9+
- **Machine-verified**: `verification/proofs/SafetyL4Model.idr` only (idris2 0.8.0 `--check`, exit 0, zero proof escapes) — the Level-4 SQL-injection remediation
10+
- **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.
1011

1112
## What Needs Proving
1213

@@ -19,6 +20,8 @@
1920
- Prove: parser (ReScript side) accepts exactly the Idris2-specified grammar
2021

2122
### Level System (src/core/Levels.idr)
23+
- ✅ L4 `NoRawUserInput` de-vacuized + `checkLevel4Sound` + `noRawUserInputCompose` (verified in `verification/proofs/SafetyL4Model.idr`)
24+
- ⚠️ L2/L3/L5 predicates still vacuous — de-vacuize with evidence-carrying constructors and prove each `checkLevelN` sound (as done for L4)
2225
- 10-level type safety hierarchy — prove level ordering is a lattice
2326
- Prove: level promotion/demotion preserves query safety
2427

‎verification/proofs/README.adoc‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,31 @@
11
= Proofs Unit
2+
3+
// SPDX-License-Identifier: PMPL-1.0-or-later
4+
5+
This directory holds the *machine-verified* proof artefacts for vcl-ut.
6+
7+
== Contents
8+
9+
`SafetyL4Model.idr`::
10+
Self-contained, idris2 0.8.0 `--check`-clean (exit 0, `%default total`,
11+
zero proof-escape symbols) model of the Level-4 SQL-injection safety
12+
remediation: the de-vacuized `NoRawUserInput` predicate, the checker
13+
soundness lemma `checkLevel4Sound`, a negative injection test, and the
14+
genuine compositionality proof `noRawUserInputCompose`.
15+
16+
`VERIFICATION-STANCE.adoc`::
17+
The authoritative, proof-backed statement of what is and is not
18+
verified. *Read this before trusting any "verified"/"type-safe"
19+
phrasing elsewhere in the repo.* It documents that the shipped
20+
`src/core/**` corpus does not compile on `origin/main` and has never
21+
been machine-checked, and gives the phased remediation roadmap.
22+
23+
== Verifying
24+
25+
[source,sh]
26+
----
27+
export IDRIS2_PREFIX=<idris2-0.8.0-prefix>
28+
idris2 --check verification/proofs/SafetyL4Model.idr # expect exit 0
29+
----
30+
31+
Tracked under hyperpolymath/standards#124.

‎verification/proofs/SafetyL4Model.idr‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
4+
||| Self-contained machine-checked model of the Level-4 (SQL-injection)
5+
||| safety remediation for vcl-ut (hyperpolymath/standards#124).
6+
|||
7+
||| WHY THIS IS A STANDALONE HARNESS, NOT AN IN-REPO PROOF
8+
||| ------------------------------------------------------
9+
||| The shipped `src/core/*.idr` + `src/interface/abi/*.idr` corpus does
10+
||| NOT compile on origin/main (see verification/proofs/VERIFICATION-
11+
||| STANCE.adoc for the full catalogue: ABI.Types missing
12+
||| `Decidable.Equality`, malformed enum `DecEq`, ill-typed
13+
||| `CPtr = Bits n`, `createQueryHandle` lacking its `So` witness;
14+
||| Grammar.idr forward-references `Statement`/`EpistemicClause` with no
15+
||| `mutual` block; no ipkg/CI ever checked any of it). The in-repo L4
16+
||| fix (commit on branch fix/vclut-l4-devacuize-honest-stance) is
17+
||| logically correct and reviewable but cannot be `idris2 --check`-ed
18+
||| in situ until the surrounding corpus is resurrected (tracked OWED).
19+
|||
20+
||| This module reproduces the *exact mathematical content* of that fix
21+
||| against a minimal, self-contained model of the relevant AST fragment,
22+
||| so the theorems themselves are genuinely machine-verified by
23+
||| idris2 0.8.0 with NO believe_me / postulate / assert_total / sorry.
24+
||| Every definition below is byte-faithful to the corresponding shipped
25+
||| definition (Grammar.hasStringLit, Composition.joinWhere,
26+
||| Levels.NoRawUserInput, Checker.checkLevel4 / checkLevel4Sound,
27+
||| Composition.noRawUserInputCompose).
28+
29+
module SafetyL4Model
30+
31+
%default total
32+
33+
-- ── Minimal model of the relevant Grammar fragment ───────────────────
34+
35+
||| The only `Literal` distinction Level-4 cares about: is it a string?
36+
public export
37+
data Literal = LitString String | LitOther
38+
39+
||| The Expr fragment that `hasStringLit` traverses. Constructor set and
40+
||| recursion are exactly those of the shipped `Grammar.Expr` clauses
41+
||| that `Grammar.hasStringLit` matches (others collapse to the `_`
42+
||| catch-all = False, modelled by `EOpaque`).
43+
public export
44+
data Expr
45+
= ELiteral Literal
46+
| ECompare Expr Expr
47+
| ELogic1 Expr -- ELogic _ l Nothing _
48+
| ELogic2 Expr Expr -- ELogic _ l (Just r) _
49+
| EAggregate Expr
50+
| EOpaque -- EField/EParam/EStar/ESubquery/... ⇒ False
51+
52+
||| Faithful copy of shipped `Grammar.hasStringLit`.
53+
public export
54+
hasStringLit : Expr -> Bool
55+
hasStringLit (ELiteral (LitString _)) = True
56+
hasStringLit (ELiteral LitOther) = False
57+
hasStringLit (ECompare l r) = hasStringLit l || hasStringLit r
58+
hasStringLit (ELogic1 l) = hasStringLit l
59+
hasStringLit (ELogic2 l r) = hasStringLit l || hasStringLit r
60+
hasStringLit (EAggregate e) = hasStringLit e
61+
hasStringLit EOpaque = False
62+
63+
||| A statement is modelled by just its WHERE clause (all `checkLevel4`
64+
||| / `NoRawUserInput` depends on).
65+
public export
66+
WhereClause : Type
67+
WhereClause = Maybe Expr
68+
69+
||| Faithful copy of shipped `Grammar.whereHasStringLit`.
70+
public export
71+
whereHasStringLit : WhereClause -> Bool
72+
whereHasStringLit w = maybe False hasStringLit w
73+
74+
-- ── Levels.NoRawUserInput (the de-vacuized predicate) ────────────────
75+
76+
||| Was `data NoRawUserInput where AllParameterised : NoRawUserInput stmt`
77+
||| — vacuous (held for ANY statement, incl. injection). Now carries the
78+
||| real evidence `whereHasStringLit = False`.
79+
public export
80+
data NoRawUserInput : WhereClause -> Type where
81+
MkNoRawUserInput : whereHasStringLit w = False -> NoRawUserInput w
82+
83+
-- ── Checker.checkLevel4 + soundness ──────────────────────────────────
84+
85+
public export
86+
checkLevel4 : WhereClause -> (Bool, String)
87+
checkLevel4 w = l4Verdict (whereHasStringLit w)
88+
where
89+
l4Verdict : Bool -> (Bool, String)
90+
l4Verdict True = (False, "L4 FAILED — raw string literal in WHERE")
91+
l4Verdict False = (True, "L4 — WHERE uses only parameterised inputs")
92+
93+
falseNotTrue : (False = True) -> Void
94+
falseNotTrue Refl impossible
95+
96+
||| Soundness: `checkLevel4` accepting a statement genuinely yields the
97+
||| (now real) `NoRawUserInput` witness. Vacuously unstateable before
98+
||| the de-vacuization.
99+
export
100+
checkLevel4Sound : (w : WhereClause) -> (m : String) ->
101+
checkLevel4 w = (True, m) -> NoRawUserInput w
102+
checkLevel4Sound w m prf with (whereHasStringLit w) proof p
103+
checkLevel4Sound w m prf | False = MkNoRawUserInput p
104+
checkLevel4Sound w m prf | True = void (falseNotTrue (cong fst prf))
105+
106+
-- A negative check: an injection-bearing WHERE is *rejected* (the old
107+
-- vacuous predicate would have "accepted" it via AllParameterised).
108+
export
109+
injectionRejected :
110+
fst (checkLevel4 (Just (ECompare EOpaque (ELiteral (LitString "1=1"))))) = False
111+
injectionRejected = Refl
112+
113+
-- ── Composition.joinWhere + noRawUserInputCompose ────────────────────
114+
115+
||| Faithful copy of shipped `Composition.joinWhere`.
116+
public export
117+
joinWhere : WhereClause -> WhereClause -> WhereClause
118+
joinWhere Nothing Nothing = Nothing
119+
joinWhere (Just w) Nothing = Just w
120+
joinWhere Nothing (Just w) = Just w
121+
joinWhere (Just w1) (Just w2) = Just (ELogic2 w1 w2)
122+
123+
trueNotFalse : (True = False) -> Void
124+
trueNotFalse Refl impossible
125+
126+
||| `False`-absorbing disjunction: both disjuncts False ⇒ whole False.
127+
orFalseFalse : (x : Bool) -> x = False -> (y : Bool) -> y = False ->
128+
(x || y) = False
129+
orFalseFalse False Refl _ yp = yp
130+
orFalseFalse True xp _ _ = void (trueNotFalse xp)
131+
132+
||| The join of two injection-free WHERE clauses is injection-free.
133+
||| Mirrors shipped `Composition.noRawUserInputCompose`'s `joinFree`.
134+
joinFree :
135+
(a, b : WhereClause) ->
136+
whereHasStringLit a = False ->
137+
whereHasStringLit b = False ->
138+
whereHasStringLit (joinWhere a b) = False
139+
joinFree Nothing Nothing _ _ = Refl
140+
joinFree (Just _) Nothing p1 _ = p1
141+
joinFree Nothing (Just _) _ p2 = p2
142+
joinFree (Just x) (Just y) p1 p2 =
143+
orFalseFalse (hasStringLit x) p1 (hasStringLit y) p2
144+
145+
||| Level-4 injection-freedom is GENUINELY closed under join (not
146+
||| vacuously, as when the predicate was `AllParameterised`).
147+
export
148+
noRawUserInputCompose :
149+
(w1, w2 : WhereClause) ->
150+
NoRawUserInput w1 -> NoRawUserInput w2 ->
151+
NoRawUserInput (joinWhere w1 w2)
152+
noRawUserInputCompose w1 w2 (MkNoRawUserInput n1) (MkNoRawUserInput n2) =
153+
MkNoRawUserInput (joinFree w1 w2 n1 n2)

‎verification/proofs/VERIFICATION-STANCE.adoc‎

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
= VCL-ut Verification Stance (proof-backed)
2+
:toc:
3+
:sectnums:
4+
5+
// SPDX-License-Identifier: PMPL-1.0-or-later
6+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
7+
8+
WARNING: vcl-ut is the interface between *hypatia* and *verisim*; both sides
9+
trust safety claims made here. This document states *precisely* what is and is
10+
not machine-verified, and takes precedence over any "verified" / "type-safe" /
11+
"formally proven" phrasing in `README.adoc`, `PROOF-NEEDS.md`, or module
12+
doc-comments. It is the proof-backed companion to (and supersedes) the
13+
doc-only `docs/VERIFICATION-STANCE.adoc` (PR #19).
14+
15+
Tracked under hyperpolymath/standards#124.
16+
17+
== Headline finding (verified, not sampled)
18+
19+
The shipped Idris2 "proof corpus" of vcl-ut *does not compile at all* on
20+
`origin/main`, at every layer, and has *never been machine-checked* (there is
21+
no `.ipkg`/Makefile/CI for `src/core/**` — only the unrelated trivial
22+
`src/abi/vclut.ipkg`, itself absent from CI). The previously-circulated stance
23+
("the dependent-type apparatus exists but is not connected") was *too
24+
generous*: the apparatus does not even typecheck. Concretely, reproduced with
25+
idris2 0.8.0:
26+
27+
* `src/interface/abi/Types.idr`
28+
** missing `import Decidable.Equality` (every `DecEq` use is an undefined name);
29+
** the `DecEq SafetyLevel/VclTotalError/QueryMode` instances are *malformed*
30+
(`decEq _ _ = No absurd` with no `Uninhabited (x = y)` — un-fixable by hand
31+
for 11/12-constructor enums without a derivation mechanism);
32+
** `CPtr p _ = Bits (ptrSize p)` is ill-typed (`Data.Bits.Bits` is an
33+
interface, not a `Nat -> Type` family);
34+
** `createQueryHandle ptr = Just (MkQueryHandle ptr)` omits the required
35+
`So (ptr /= 0)` witness;
36+
** `thisPlatform` uses `%runElab` without `%language ElabReflection`.
37+
* `src/core/Grammar.idr` — `Expr` (`ESubquery Statement`) and the epistemic
38+
clause constructors forward-reference `Statement` / `EpistemicRequirement`,
39+
which are defined ~100 lines later, with *no `mutual` block or forward
40+
declarations*. The file does not pass the type checker.
41+
42+
Because Grammar fails, every downstream module (`Schema`, `Levels`, `Checker`,
43+
`Composition`) is unverifiable in situ regardless of its own correctness.
44+
45+
== What IS genuinely machine-verified by this PR
46+
47+
`verification/proofs/SafetyL4Model.idr` — checked by **idris2 0.8.0,
48+
`idris2 --check`, exit 0, with `%default total` and ZERO
49+
`believe_me`/`really_believe_me`/`postulate`/`assert_total`/`idris_crash`/
50+
`sorry`**. It reproduces the *exact mathematical content* of the in-repo
51+
Level-4 (SQL-injection) remediation against a minimal, self-contained,
52+
byte-faithful model of the relevant AST fragment, proving:
53+
54+
. `NoRawUserInput` is no longer *vacuous*. It previously had the single
55+
catch-all constructor `AllParameterised : NoRawUserInput stmt`, inhabiting
56+
it for *every* statement — including a WHERE clause that is pure string
57+
interpolation. It now carries real evidence: `whereHasStringLit w = False`.
58+
. `checkLevel4Sound` — *soundness of the decision procedure*: if
59+
`checkLevel4` accepts, the statement genuinely carries the (now real)
60+
`NoRawUserInput` witness. This is the certificate↔checker connection for
61+
L4; it was previously unstateable (predicate vacuous, checker returned a
62+
bare `Bool`).
63+
. `injectionRejected` — negative test: a WHERE bearing a string literal
64+
(`… = '1=1'`) is *rejected*. Under the old vacuous predicate the
65+
corresponding query "type-checked" at Level 4.
66+
. `noRawUserInputCompose` — Level-4 injection-freedom is *genuinely* closed
67+
under join composition, because `joinWhere` introduces no string literal
68+
not already present. This replaces the two
69+
`MkL4 _ AllParameterised` uses in `Composition.compositionPreservation`,
70+
whose "preservation theorem" was therefore *vacuously true*.
71+
72+
The corresponding in-repo source fix is committed on branch
73+
`fix/vclut-l4-devacuize-honest-stance` (`src/core/{Grammar,Levels,Checker,
74+
Composition}.idr`). It is logically correct and reviewable, and is
75+
*identical in content* to the verified model, but cannot be
76+
`idris2 --check`-ed in situ until the corpus is resurrected (see roadmap).
77+
78+
== What is NOT proven (honest, precisely-scoped gaps — OWED)
79+
80+
. *Corpus does not compile* (above). Until fixed, NO in-repo Idris claim is
81+
machine-checked. Highest priority.
82+
. *L2/L3/L5 predicates remain vacuous.* `AllComparisonsTypeSafe` via
83+
`WhereTypeSafe LogicSafe` (holds for any logic expr); `L3`
84+
`AllNullableFieldsGuarded`'s `GuardedNull` (accepts any expr); `L5`
85+
`AllSelectItemsTyped`'s `ConsTyped` (no per-item typing evidence). As
86+
written, Levels 2, 3 and 5 prove nothing about the property they name.
87+
Only L4 has been de-vacuized.
88+
. *The certificate is disconnected from the checker for every level except
89+
the L4 evidence.* `Checker.checkQuery` returns a plain `CheckResult`
90+
record and never constructs a `SafetyCertificate`. The dependent types
91+
are decorative w.r.t. the decision procedure (L4 excepted, via
92+
`checkLevel4Sound`).
93+
. *`Composition.compositionPreservation`*: the L4 case is now genuine; the
94+
L2/L3/L5 cases remain vacuous (and self-document as such).
95+
. *The FFI boundary is a stub.* `ffi/zig/src/lib.zig` returns `2`
96+
(`L2`) for any query containing the substring `SELECT`; the Rust
97+
`extern "C"` counterpart does not exist. `src/abi/Foreign.idr`
98+
fabricates `Verified Ln` from a bare untrusted `Int`. The level tag
99+
hypatia/verisim receive is an *asserted integer from a substring check*,
100+
not a transported proof.
101+
102+
== Consumer guidance (hypatia / verisim)
103+
104+
* Treat *every* vcl-ut safety-level tag as an *advisory claim*, not a proof
105+
carrier. Do not weaken your own checks on the strength of a vcl-ut level.
106+
* The *only* claim with a genuine machine-checked basis is L4
107+
injection-freedom — and even that is, today, not wired through the
108+
(non-compiling) corpus or the (stubbed) FFI. Do not cite vcl-ut as
109+
"formally verified query safety" downstream.
110+
111+
== Remediation roadmap (phased, tracked standards#124)
112+
113+
. *Phase 0 (this PR):* de-vacuize L4 + checker soundness + real
114+
composition; machine-verify the content; document the true state.
115+
. *Phase 1:* make the corpus compile — `mutual` block in `Grammar.idr`;
116+
fix/replace `ABI.Types` (`Decidable.Equality`, a real `DecEq`
117+
derivation, `CPtr`, `createQueryHandle`, `thisPlatform`); add a
118+
`verification/proofs/vclut-core.ipkg` + CI step so it stays compiled.
119+
. *Phase 2:* de-vacuize L2/L3/L5 with evidence-carrying constructors and
120+
prove `checkLevelN` sound for each (as done for L4).
121+
. *Phase 3:* have `checkQuery` emit a real `SafetyCertificate`; transport
122+
it as an opaque proof token through a non-stub Zig/Rust FFI.
123+
124+
== Provenance
125+
126+
Audit + remediation 2026-05-18 (hyperpolymath/standards#124). Findings
127+
reproduced by reading the corpus and by `idris2 0.8.0 --build` /
128+
`--check` (compile failures above are reproducible verbatim). The verified
129+
model carries no proof-escape symbols. The risk here is *absent and
130+
non-compiling* proof masquerading as present proof at a doubly-trusted
131+
interface.

0 commit comments

Comments
 (0)