P3: prove TypeCompat (level 3) as a real operand-type-compatibility guarantee

[hyperpolymath]

Summary

Continues deepening the flagship semantic-proof coverage of the TypedQLiser ABI. After InjectionFree (level 5, #33) and SchemaBound (level 2, #35), this makes TypeCompat (level 3 — "operand types compatible") a genuine, sound + complete decidable property over the existing query AST, to the same quality bar.

Builds on #35 (merged) — the diff here is the new TypeCompat module only.

Changes

• Adds src/interface/abi/Typedqliser/ABI/TypeCompat.idr:
  • A small SQL type universe (SqlType = TInt | TText | TBool) and a typed column environment (ColEnv) with a total lookupType resolver, reusing the existing Query/Pred/Value AST from Semantics.
  • 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 : (env : ColEnv) -> (q : Query) -> Dec (QueryTypeCompat env q) — sound + complete, so a Proven TypeCompat certificate is backed by a constructive witness and a type clash can never be certified.
  • certifyTypeCompat + certifyTypeCompatSound (a Proven verdict provably entails the property), and 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).
• Registers the new module in src/interface/abi/typedqliser-abi.ipkg.

RSR Quality Checklist

Required

• Tests pass (just test or equivalent) — ABI package builds clean (see Testing); change is ABI-only
• Code is formatted (just fmt or equivalent)
• Linter is clean (no new warnings or errors) — idris2 --build emits zero warnings
• No banned language patterns (no TypeScript, no npm/bun, no Go/Python)
• No unsafe blocks without // SAFETY: comments — none present
• No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry) — proofs are genuine (replace/trans/sym/local justInj only)
• SPDX license headers present on all new/modified source files
• No secrets, credentials, or .env files included

As Applicable

• ABI/FFI changes validated — ABI builds; this PR is additive proof code and touches no FFI symbols, so src/interface/abi/ and src/interface/ffi/ stay consistent

Testing

Verified with Idris2 0.7.0:

$ cd src/interface/abi && idris2 --build typedqliser-abi.ipkg
1/7: Building Typedqliser.ABI.Types ...
2/7: Building Typedqliser.ABI.Semantics ...
3/7: Building Typedqliser.ABI.TypeCompat ...
4/7: Building Typedqliser.ABI.SchemaBound ...
5/7: Building Typedqliser.ABI.Layout ...
6/7: Building Typedqliser.ABI.Proofs ...
7/7: Building Typedqliser.ABI.Foreign ...
EXIT: 0    # zero warnings

Adversarial verification — three deliberately-false proofs were checked in a throwaway module (not committed) and the type checker rejected all three (exit 1):

1. levelNat TypeCompat = 4 (it is 3) — rejected.
2. ValueCompat TText (Lit 42) = LitInt (a TInt literal against a TText column) — rejected (Mismatch between: TInt and TText).
3. A QueryTypeCompat exampleEnv badQuery witness for the type-clash query — rejected.

The generated build/ directory was removed and is not committed.

🤖 Generated with Claude Code

https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

---

Generated by Claude Code