P3: prove InjectionFree (level 5) as a real query-checking guarantee#33
Merged
Conversation
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
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
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
This was referenced Jun 27, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What & why
typedqliser's ten type-safety levels were, in the ABI, abstract labels carrying a per-level
ProofStatus— nothing tied aProvenverdict to an actual property of an actual query. This makes the flagship level a real, machine-checked semantic guarantee: InjectionFree (level 5) — "no string interpolation in structure", i.e. the no-SQL-injection property.Change — new module
Typedqliser.ABI.SemanticsRawSpliceinterpolated strings (the injection vector).QueryInjectionFree— the proposition that noRawSpliceoccurs anywhere.ValueOkhas no constructor forRawSplice, so it is genuinely uninhabited.decInjectionFree— a sound + complete decision procedure returning a realDecproof.certifyProvenSound— a theorem that aProvenInjectionFree verdict entails the property: the certifier cannot lie.… WHERE id = $1) is provably injection-free and certifiesProvenby reduction.… WHERE name = '; DROP TABLE users;--'is proven to have no injection-free proof (Not (QueryInjectionFree …)).Verification (Idris2 0.7.0)
idris2 --build typedqliser-abi.ipkg, all 5 modules, zero warnings).believe_me/postulate/ holes.Mismatch between Param ?i and RawSplice "'; DROP TABLE users;--". The guarantee genuinely cannot be subverted.This is the first of the priority-repo P3 deepenings (typedqliser #1); the same approach extends to the other nine levels.
CI note
rust-ci / Hypatia / governance reds are pre-existing estate-infra unrelated to this change; the
ABI-FFI Gatecheck is green.🤖 Generated with Claude Code
https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
Generated by Claude Code