Skip to content

Commit 579d759

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 5: end-to-end soundness capstone certificate (#39)
* P3: prove TypeCompat (level 3) as a real operand-type-compatibility guarantee 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: add Layer-3 NullSafe (level 4) theorem with guard discovery Adds Typedqliser.ABI.Invariants, a second, deeper, distinct machine-checked property over the existing Semantics query model (Query/Pred/Value reused verbatim). Where the Layer-2 flagship (Semantics.InjectionFree, level 5) is a purely structural property, NullSafe (level 4) is context-sensitive: a projected nullable column is safe only if the WHERE predicate guards it, with guards discovered by union under And and intersection under Or (disjunctive weakening). Includes a sound + complete decision procedure (decQueryNullSafe : Dec ...), a certifier proven sound (certifyNullSafeSound), the level-ordinal identity plus a proof it differs from InjectionFree, three positive controls and three non-vacuity controls (unguarded projection, And/union, Or/intersection). Builds clean with zero warnings; the deliberately-false adversarial proof is rejected. No believe_me/postulate/assert_total/%hint; %default total throughout. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * Add Layer-4 ABI<->FFI seam proof (Typedqliser.ABI.FfiSeam) Prove the FFI result-code encoding is SOUND: the C integer the Zig FFI returns faithfully round-trips back to the ABI value, and distinct ABI outcomes never collide on the wire. - intToResult / intToStatus: total decoders (if x == n over boolean Bits32 ==, which reduces on concrete literals). - resultRoundTrip / statusRoundTrip: lossless encoding, proved by Refl. - resultToIntInjective / statusToIntInjective: injectivity DERIVED from the round-trip via a local justInj + cong. - Positive controls (decodeOk/decodeNullPointer/decodeUnknown/decodeProven) and machine-checked non-vacuity controls (okNotError, schemaNotNull, provenNotRefuted) refuting collisions of distinct codes. Genuine total proof: no believe_me / postulate / assert_total / sorry. Builds clean with zero warnings; a false seam claim is rejected by --check. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi(capstone): Layer-5 end-to-end ABI soundness certificate Assemble the existing per-layer proofs into one inhabited record `ABISound` and a single value `abiContractDischarged` built from the already-exported witnesses: - Layer-2 flagship: safeQueryInjectionFree (InjectionFree, level 5) - Layer-2 companions: boundQuerySchemaBound (SchemaBound, level 2), goodQueryTypeCompat (TypeCompat, level 3) - Layer-3 invariant: guardedQueryNullSafe (NullSafe, level 4) - Layer-4 FFI seam: resultToIntInjective The capstone proves no new domain theorem; its content is that the whole chain holds simultaneously — if any prior layer were unsound the value would not typecheck. Adversarial control: a false certificate (deriving Ok = Error through the seam) is rejected by the typechecker. %default total, SPDX MPL-2.0, zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
1 parent 5957feb commit 579d759

2 files changed

Lines changed: 101 additions & 0 deletions

File tree

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

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
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+
||| Layer-5 CAPSTONE: a single end-to-end ABI SOUNDNESS CERTIFICATE for
5+
||| TypedQLiser.
6+
|||
7+
||| Every prior layer proved one face of the ABI contract in isolation:
8+
|||
9+
||| * Layer-2 (`Semantics`) — the FLAGSHIP type-safety property: a fully
10+
||| parameterized query is InjectionFree (level 5). Witness reused:
11+
||| `safeQueryInjectionFree`.
12+
||| * Layer-3 (`Invariants`) — the DEEPER, context-sensitive invariant: a
13+
||| guarded nullable projection is NullSafe (level 4). Witness reused:
14+
||| `guardedQueryNullSafe`.
15+
||| * Layer-3 companions — `SchemaBound` (level 2) and `TypeCompat` (level 3)
16+
||| pin the remaining static-semantics levels. Witnesses reused:
17+
||| `boundQuerySchemaBound`, `goodQueryTypeCompat`.
18+
||| * Layer-4 (`FfiSeam`) — the ABI<->FFI SEAM is sealed: distinct result
19+
||| codes never collide on the wire. Theorem reused: `resultToIntInjective`.
20+
|||
21+
||| This module ASSEMBLES those already-proven facts into ONE inhabited record,
22+
||| `ABISound`, and exhibits a single value `abiContractDischarged : ABISound`
23+
||| built entirely from the existing exported witnesses. It proves no NEW domain
24+
||| theorem; its content is that the whole chain — manifest-level type-safety
25+
||| levels -> the ABI semantic proofs (flagship InjectionFree + the deeper
26+
||| NullSafe invariant + SchemaBound + TypeCompat) -> the FFI seam injectivity —
27+
||| holds SIMULTANEOUSLY. If any prior layer were unsound, its exported witness
28+
||| would not exist and this capstone value would not typecheck. The certificate
29+
||| is therefore an end-to-end soundness statement for the TypedQLiser ABI.
30+
31+
module Typedqliser.ABI.Capstone
32+
33+
import Typedqliser.ABI.Types
34+
import Typedqliser.ABI.Semantics
35+
import Typedqliser.ABI.SchemaBound
36+
import Typedqliser.ABI.TypeCompat
37+
import Typedqliser.ABI.Invariants
38+
import Typedqliser.ABI.FfiSeam
39+
40+
%default total
41+
42+
--------------------------------------------------------------------------------
43+
-- The capstone certificate type
44+
--------------------------------------------------------------------------------
45+
46+
||| `ABISound` bundles the KEY proven facts of the TypedQLiser ABI into one
47+
||| record. Each field is a proposition that some prior layer already discharged;
48+
||| an inhabitant of `ABISound` is therefore a single object whose existence is
49+
||| equivalent to the conjunction of all layers being sound.
50+
public export
51+
record ABISound where
52+
constructor MkABISound
53+
||| Layer-2 flagship: the canonical parameterized positive control is
54+
||| injection-free (level 5).
55+
flagshipInjectionFree : QueryInjectionFree Semantics.safeQuery
56+
||| Layer-2 companion: SchemaBound (level 2) holds for its positive control.
57+
schemaBound : QuerySchemaBound SchemaBound.exampleSchema SchemaBound.boundQuery
58+
||| Layer-2 companion: TypeCompat (level 3) holds for its positive control.
59+
typeCompatible : QueryTypeCompat TypeCompat.exampleEnv TypeCompat.goodQuery
60+
||| Layer-3 deeper invariant: NullSafe (level 4) holds for the guarded control.
61+
invariantNullSafe : QueryNullSafe Invariants.nullableCols Invariants.guardedQuery
62+
||| Layer-4 FFI seam: distinct ABI result codes never collide on the C wire.
63+
ffiSeamInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b
64+
65+
--------------------------------------------------------------------------------
66+
-- The capstone value: the whole ABI contract discharged at once
67+
--------------------------------------------------------------------------------
68+
69+
||| THE CAPSTONE. A single inhabited value of `ABISound`, constructed purely from
70+
||| the witnesses and theorems exported by the prior layers — no new axioms, no
71+
||| `believe_me`, no `postulate`. Its successful typechecking IS the end-to-end
72+
||| soundness certificate: manifest type-safety levels -> ABI semantic proofs
73+
||| (flagship + invariant + schema/type bounds) -> FFI seam, all at once.
74+
public export
75+
abiContractDischarged : ABISound
76+
abiContractDischarged =
77+
MkABISound
78+
safeQueryInjectionFree
79+
boundQuerySchemaBound
80+
goodQueryTypeCompat
81+
guardedQueryNullSafe
82+
resultToIntInjective
83+
84+
--------------------------------------------------------------------------------
85+
-- Capstone-level corollaries projected back out of the certificate
86+
--------------------------------------------------------------------------------
87+
88+
||| From the discharged certificate we can recover any single layer's guarantee —
89+
||| e.g. the flagship InjectionFree witness — showing the bundle genuinely
90+
||| contains (does not merely assert) each layer's proof.
91+
public export
92+
flagshipFromCapstone : QueryInjectionFree Semantics.safeQuery
93+
flagshipFromCapstone = abiContractDischarged.flagshipInjectionFree
94+
95+
||| And the FFI-seam injectivity, specialised to a concrete distinct pair,
96+
||| applied through the certificate: `Ok` and `Error` can only be equal on the
97+
||| wire if they are equal as `Result`s (they are not — see `okNotError`).
98+
public export
99+
seamFromCapstone : resultToInt Ok = resultToInt Error -> Ok = Error
100+
seamFromCapstone = abiContractDischarged.ffiSeamInjective Ok Error

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,4 @@ modules = Typedqliser.ABI.Types
1414
, Typedqliser.ABI.TypeCompat
1515
, Typedqliser.ABI.Invariants
1616
, Typedqliser.ABI.FfiSeam
17+
, Typedqliser.ABI.Capstone

0 commit comments

Comments
 (0)