Skip to content

Commit a03cd3d

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
P3: prove InjectionFree (level 5) as a real query-checking guarantee (#33)
* P1: implement missing FFI functions + fix result-code semantics The Zig FFI (src/interface/ffi/src/main.zig) was generic scaffolding that drifted from the Idris2 ABI, which is the source of truth (src/interface/abi/Typedqliser/ABI/Foreign.idr and .../Types.idr). Two core domain functions declared in Foreign.idr were missing from the Zig: * typedqliser_check_query : Bits64 -> String -> Bits32 -> PrimIO Bits32 (handle pointer, query C-string, requested safety level) -> result code. Validates a query against the registered schema up to the requested level and records the achieved certificate level on the handle. * typedqliser_certificate_level : Bits64 -> PrimIO Bits32 (handle pointer) -> highest safety level the last checked query achieved (0 if none), within the ten cumulative type-safety levels. Both are now exported `callconv(.C)` functions with arities/types matching the Idris %foreign declarations exactly (the handle is threaded as a Bits64 pointer value, reconstructed FFI-side). Result-code semantics corrected to match Typedqliser.ABI.Types.resultToInt: Ok=0, Error=1, InvalidQuery=2, SchemaError=3, NullPointer=4. The generic scaffold encoded codes 2 and 3 as invalid_param / out_of_memory, so cross-FFI those codes meant the WRONG thing. They are renamed to invalid_query (2) and schema_error (3) and all usages updated. The pre-existing extra exports (build_info, free_string, get_string, is_initialized, last_error, process, process_array, register_callback) are kept as a harmless superset; init/free/version are unchanged in behaviour. Verification: * zig test src/interface/ffi/src/main.zig -lc -> all 8 tests pass (added tests exercising check_query + certificate_level, the malformed-query InvalidQuery path, the SchemaError path, null-handle rejection, and a guard pinning the result codes to resultToInt). * idris2 --build src/interface/abi/typedqliser-abi.ipkg -> exit 0. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH * ci: add ABI↔FFI conformance gate Adds scripts/abi-ffi-gate.py + .github/workflows/abi-ffi-gate.yml enforcing that the Zig FFI matches the Idris2 ABI (source of truth), on top of this branch's FFI fix. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH * P3: prove InjectionFree (level 5) as a real query-checking guarantee The ten type-safety levels were abstract labels carrying a per-level ProofStatus, with nothing tying a "Proven" verdict to an actual property of an actual query. This makes the flagship level — InjectionFree (level 5, "no string interpolation in structure", the no-SQL-injection guarantee) — a genuine, machine-checked semantic property. New module Typedqliser.ABI.Semantics: - a minimal but faithful query AST whose value leaves are bound parameters / literals (safe) or RawSplice interpolated strings (the injection vector); - QueryInjectionFree: the proposition that no RawSplice node occurs anywhere (ValueOk has no constructor for RawSplice, so it is genuinely uninhabited); - decInjectionFree: a sound + complete decision procedure returning a real Dec proof; - certifyProvenSound: a theorem that a `Proven` InjectionFree verdict entails the property — the certifier cannot lie; - positive control (a parameterized query is provably injection-free and certifies Proven by reduction) and a negative control proving the interpolated `'; DROP TABLE users;--` query has NO injection-free proof. Adversarially verified under Idris2 0.7.0: the full ABI builds clean (zero warnings, no believe_me/postulate/holes), and an attempt to prove the injection query safe is rejected by the type checker (Param vs RawSplice mismatch) — the guarantee is non-vacuous. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 4b1839b commit a03cd3d

4 files changed

Lines changed: 320 additions & 0 deletions

File tree

‎.github/workflows/abi-ffi-gate.yml‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# abi-ffi-gate.yml — enforce that the Zig FFI conforms to the Idris2 ABI.
3+
#
4+
# The Idris2 ABI (src/interface/abi) is the source of truth. This gate fails if
5+
# the Zig FFI (src/interface/ffi) drifts from it: a declared C function with no
6+
# export, a mismatched result-code map, or an unrendered template token. A
7+
# second job builds + tests the Zig FFI under the pinned Zig 0.14.0.
8+
name: ABI-FFI Gate
9+
10+
on:
11+
pull_request:
12+
push:
13+
branches: [main, master]
14+
15+
permissions:
16+
contents: read
17+
18+
jobs:
19+
conformance:
20+
name: ABI ↔ FFI structural conformance
21+
runs-on: ubuntu-latest
22+
steps:
23+
- uses: actions/checkout@v4
24+
- name: Run ABI-FFI gate
25+
run: python3 scripts/abi-ffi-gate.py
26+
27+
zig-build:
28+
name: Zig FFI builds + tests (Zig 0.14.0)
29+
runs-on: ubuntu-latest
30+
steps:
31+
- uses: actions/checkout@v4
32+
- name: Install Zig 0.14.0
33+
run: |
34+
curl -fsSL https://ziglang.org/download/0.14.0/zig-linux-x86_64-0.14.0.tar.xz -o /tmp/zig.tar.xz
35+
tar -xf /tmp/zig.tar.xz -C /tmp
36+
echo "/tmp/zig-linux-x86_64-0.14.0" >> "$GITHUB_PATH"
37+
- name: zig test FFI
38+
run: zig test src/interface/ffi/src/main.zig -lc

‎scripts/abi-ffi-gate.py‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
#!/usr/bin/env python3
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
#
5+
# abi-ffi-gate.py — fail (exit 1) if the Zig FFI does not conform to the Idris2
6+
# ABI. The Idris2 ABI is the source of truth. Checks, with no toolchain needed:
7+
#
8+
# 1. the Zig FFI carries no unrendered `{{...}}` template tokens;
9+
# 2. every `%foreign "C:<name>"` symbol declared anywhere in the ABI .idr
10+
# sources is exported by the Zig FFI (`export fn <name>`);
11+
# 3. the Zig `Result = enum(c_int)` and the Idris `resultToInt` agree on BOTH
12+
# names and integer values (the `Error`/`err` spelling is treated as one).
13+
#
14+
# Usage: python3 scripts/abi-ffi-gate.py [repo_root] (defaults to cwd)
15+
16+
import os
17+
import re
18+
import sys
19+
import glob
20+
21+
22+
def camel_to_snake(s):
23+
return re.sub(r"(?<!^)(?=[A-Z])", "_", s).lower()
24+
25+
26+
def canon_rc(name):
27+
n = name.lower()
28+
return "error" if n in ("err", "error") else n
29+
30+
31+
def find_result_enum(zig):
32+
"""Return {variant: value} for the C-ABI Result enum, or {}."""
33+
best = {}
34+
for m in re.finditer(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}", zig, re.S):
35+
body = m.group(1)
36+
variants = {}
37+
for vm in re.finditer(r'@?"?([A-Za-z_][A-Za-z0-9_]*)"?\s*=\s*(\d+)', body):
38+
variants[canon_rc(vm.group(1))] = int(vm.group(2))
39+
# The Result enum is the one starting at ok = 0.
40+
if variants.get("ok") == 0 and len(variants) > len(best):
41+
best = variants
42+
return best
43+
44+
45+
def main():
46+
root = sys.argv[1] if len(sys.argv) > 1 else "."
47+
name = os.path.basename(os.path.abspath(root))
48+
abi_dir = os.path.join(root, "src/interface/abi")
49+
zig_path = os.path.join(root, "src/interface/ffi/src/main.zig")
50+
errs = []
51+
52+
idr_files = [
53+
p for p in glob.glob(os.path.join(abi_dir, "**", "*.idr"), recursive=True)
54+
if os.sep + "build" + os.sep not in p
55+
]
56+
if not idr_files:
57+
print(f"ABI-FFI GATE: SKIP ({name}) — no Idris2 ABI .idr files under {abi_dir}")
58+
return 0
59+
if not os.path.exists(zig_path):
60+
print(f"ABI-FFI GATE: FAIL ({name}) — no Zig FFI at {zig_path}")
61+
return 1
62+
63+
idr = "\n".join(open(p, encoding="utf-8").read() for p in idr_files)
64+
zig = open(zig_path, encoding="utf-8").read()
65+
66+
# 1. unrendered template tokens
67+
toks = sorted(set(re.findall(r"\{\{[A-Za-z0-9_]+\}\}", zig)))
68+
if toks:
69+
errs.append(f"Zig FFI has unrendered template tokens: {toks}")
70+
71+
# 2. foreign C symbols must be exported
72+
csyms = sorted(set(re.findall(r"C:([A-Za-z0-9_]+)", idr)))
73+
exports = set(re.findall(r"export fn ([A-Za-z0-9_]+)", zig))
74+
missing = [s for s in csyms if s not in exports]
75+
if missing:
76+
errs.append(f"{len(missing)} ABI function(s) not exported by the Zig FFI: {missing}")
77+
78+
# 3. result-code map (names + values) must agree
79+
idr_rc = {}
80+
for m in re.finditer(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr):
81+
idr_rc[canon_rc(camel_to_snake(m.group(1)))] = int(m.group(2))
82+
zig_rc = find_result_enum(zig)
83+
if idr_rc and not zig_rc:
84+
errs.append("no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes")
85+
elif idr_rc and zig_rc and idr_rc != zig_rc:
86+
errs.append(
87+
"Result-code map differs (name or value):\n"
88+
f" Idris resultToInt: {dict(sorted(idr_rc.items()))}\n"
89+
f" Zig Result enum: {dict(sorted(zig_rc.items()))}"
90+
)
91+
92+
if errs:
93+
print(f"ABI-FFI GATE: FAIL ({name})")
94+
for e in errs:
95+
print(" - " + e)
96+
return 1
97+
print(f"ABI-FFI GATE: OK ({name}) — {len(csyms)} ABI functions exported, "
98+
f"{len(idr_rc)} result codes match")
99+
return 0
100+
101+
102+
if __name__ == "__main__":
103+
sys.exit(main())

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

Lines changed: 178 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
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 proofs for TypedQLiser's type-safety levels.
5+
|||
6+
||| The ten levels in `Types.idr` are, on their own, abstract labels carrying a
7+
||| per-level `ProofStatus`. This module makes one of them — `InjectionFree`
8+
||| (level 5: "no string interpolation in structure", i.e. the no-SQL-injection
9+
||| guarantee) — a *real*, machine-checked property over an actual query model:
10+
|||
11+
||| 1. a minimal but faithful query AST whose value leaves are either bound
12+
||| parameters / literals (safe) or raw spliced strings (an injection vector);
13+
||| 2. `QueryInjectionFree`, the proposition that no raw splice occurs anywhere;
14+
||| 3. `decInjectionFree`, a sound + complete decision procedure returning a
15+
||| genuine proof (`Dec`), so a "Proven" InjectionFree certificate is backed
16+
||| by a constructive witness and a raw splice can never be certified safe;
17+
||| 4. a certifier whose `Proven` verdict is *proven* to entail the property
18+
||| (`certifyProvenSound`), plus positive and negative controls.
19+
20+
module Typedqliser.ABI.Semantics
21+
22+
import Typedqliser.ABI.Types
23+
import Data.So
24+
import Data.Vect
25+
import Decidable.Equality
26+
27+
%default total
28+
29+
--------------------------------------------------------------------------------
30+
-- A minimal but faithful query model
31+
--------------------------------------------------------------------------------
32+
33+
||| A value appearing in a query. Only `RawSplice` — an interpolated string
34+
||| spliced into the query structure — is an injection vector; bound parameters
35+
||| and literals are safe.
36+
public export
37+
data Value : Type where
38+
Param : (idx : Nat) -> Value -- bound parameter placeholder ($1, $2, …)
39+
Lit : (n : Integer) -> Value -- literal constant
40+
RawSplice : (s : String) -> Value -- interpolated string fragment (UNSAFE)
41+
42+
||| A WHERE predicate over columns and values.
43+
public export
44+
data Pred : Type where
45+
Cmp : (col : String) -> (v : Value) -> Pred
46+
And : Pred -> Pred -> Pred
47+
Or : Pred -> Pred -> Pred
48+
49+
||| A SELECT query.
50+
public export
51+
data Query : Type where
52+
Select : (table : String) -> (cols : List String) -> (where_ : Pred) -> Query
53+
54+
--------------------------------------------------------------------------------
55+
-- InjectionFree as a genuine proposition (no RawSplice node anywhere)
56+
--------------------------------------------------------------------------------
57+
58+
||| A value is injection-safe unless it is a raw splice. There is deliberately
59+
||| no constructor for `RawSplice`, so `ValueOk (RawSplice s)` is uninhabited.
60+
public export
61+
data ValueOk : Value -> Type where
62+
ParamOk : ValueOk (Param i)
63+
LitOk : ValueOk (Lit n)
64+
65+
||| No `ValueOk` witnesses a raw splice — the heart of the guarantee.
66+
public export
67+
Uninhabited (ValueOk (RawSplice s)) where
68+
uninhabited ParamOk impossible
69+
uninhabited LitOk impossible
70+
71+
||| A predicate is injection-free when every comparison value is safe.
72+
public export
73+
data PredInjectionFree : Pred -> Type where
74+
CmpFree : ValueOk v -> PredInjectionFree (Cmp col v)
75+
AndFree : PredInjectionFree p -> PredInjectionFree q -> PredInjectionFree (And p q)
76+
OrFree : PredInjectionFree p -> PredInjectionFree q -> PredInjectionFree (Or p q)
77+
78+
||| A query is injection-free when its WHERE predicate is.
79+
public export
80+
data QueryInjectionFree : Query -> Type where
81+
SelectFree : PredInjectionFree w -> QueryInjectionFree (Select t c w)
82+
83+
--------------------------------------------------------------------------------
84+
-- Sound + complete decision procedure (returns a real proof)
85+
--------------------------------------------------------------------------------
86+
87+
public export
88+
decValueOk : (v : Value) -> Dec (ValueOk v)
89+
decValueOk (Param i) = Yes ParamOk
90+
decValueOk (Lit n) = Yes LitOk
91+
decValueOk (RawSplice s) = No absurd
92+
93+
public export
94+
decPredFree : (p : Pred) -> Dec (PredInjectionFree p)
95+
decPredFree (Cmp col v) = case decValueOk v of
96+
Yes ok => Yes (CmpFree ok)
97+
No no => No (\(CmpFree ok) => no ok)
98+
decPredFree (And p q) = case decPredFree p of
99+
No np => No (\(AndFree pp _) => np pp)
100+
Yes pp => case decPredFree q of
101+
Yes qq => Yes (AndFree pp qq)
102+
No nq => No (\(AndFree _ qq) => nq qq)
103+
decPredFree (Or p q) = case decPredFree p of
104+
No np => No (\(OrFree pp _) => np pp)
105+
Yes pp => case decPredFree q of
106+
Yes qq => Yes (OrFree pp qq)
107+
No nq => No (\(OrFree _ qq) => nq qq)
108+
109+
||| The headline decision procedure: decide injection-freedom, returning a
110+
||| genuine `QueryInjectionFree` witness when it holds.
111+
public export
112+
decInjectionFree : (q : Query) -> Dec (QueryInjectionFree q)
113+
decInjectionFree (Select t c w) = case decPredFree w of
114+
Yes ok => Yes (SelectFree ok)
115+
No no => No (\(SelectFree ok) => no ok)
116+
117+
--------------------------------------------------------------------------------
118+
-- Certifier soundness: a `Proven` InjectionFree status is never a lie
119+
--------------------------------------------------------------------------------
120+
121+
||| Certify the InjectionFree (level 5) obligation for a query. `Proven` is
122+
||| emitted only when the decision procedure produced a real proof.
123+
public export
124+
certifyInjectionFree : (q : Query) -> ProofStatus
125+
certifyInjectionFree q = case decInjectionFree q of
126+
Yes _ => Proven
127+
No _ => Refuted
128+
129+
||| Soundness: if the certifier reports `Proven`, the query really is
130+
||| injection-free. (Together with `decInjectionFree` being a `Dec`, this also
131+
||| means a query that is *not* injection-free can never be reported `Proven`.)
132+
export
133+
certifyProvenSound : (q : Query) -> certifyInjectionFree q = Proven -> QueryInjectionFree q
134+
certifyProvenSound q prf with (decInjectionFree q)
135+
certifyProvenSound q prf | Yes ok = ok
136+
certifyProvenSound q Refl | No _ impossible
137+
138+
||| `InjectionFree` is level 5 — the certified obligation is the fifth of ten.
139+
export
140+
injectionFreeIsLevelFive : levelNat InjectionFree = 5
141+
injectionFreeIsLevelFive = Refl
142+
143+
--------------------------------------------------------------------------------
144+
-- Positive control: a parameterized query is provably injection-free
145+
--------------------------------------------------------------------------------
146+
147+
||| `SELECT id, name FROM users WHERE id = $1` — fully parameterized.
148+
public export
149+
safeQuery : Query
150+
safeQuery = Select "users" ["id", "name"] (Cmp "id" (Param 1))
151+
152+
||| Machine-checked: the parameterized query is injection-free.
153+
export
154+
safeQueryInjectionFree : QueryInjectionFree Semantics.safeQuery
155+
safeQueryInjectionFree = SelectFree (CmpFree ParamOk)
156+
157+
||| …and the certifier reports `Proven` for it (computes to `Proven`).
158+
export
159+
safeQueryCertifiesProven : certifyInjectionFree Semantics.safeQuery = Proven
160+
safeQueryCertifiesProven = Refl
161+
162+
--------------------------------------------------------------------------------
163+
-- Negative control: an interpolated query CANNOT be certified injection-free
164+
--------------------------------------------------------------------------------
165+
166+
||| `SELECT id FROM users WHERE name = '<spliced user input>'` — a classic
167+
||| injection vector built by string interpolation.
168+
public export
169+
unsafeQuery : Query
170+
unsafeQuery =
171+
Select "users" ["id"] (Cmp "name" (RawSplice "'; DROP TABLE users;--"))
172+
173+
||| Machine-checked: there is **no** proof that the interpolated query is
174+
||| injection-free. This is what makes the guarantee non-vacuous — `ValueOk`
175+
||| has no constructor for a raw splice, so the property is genuinely refuted.
176+
export
177+
unsafeQueryNotInjectionFree : Not (QueryInjectionFree Semantics.unsafeQuery)
178+
unsafeQueryNotInjectionFree (SelectFree (CmpFree ok)) = absurd ok

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ modules = Typedqliser.ABI.Types
99
, Typedqliser.ABI.Layout
1010
, Typedqliser.ABI.Foreign
1111
, Typedqliser.ABI.Proofs
12+
, Typedqliser.ABI.Semantics

0 commit comments

Comments
 (0)