P3: prove SchemaBound (level 2) as a real schema-resolution guarantee

[hyperpolymath]

Summary

Deepens the flagship semantic-proof coverage of the TypedQLiser ABI. Today only InjectionFree (level 5) is a real, machine-checked property (PR #33); the other nine levels carry only an abstract ProofStatus. This PR makes SchemaBound (level 2 — "all references resolve in the schema") a genuine, sound + complete decidable property over the existing query AST, to the same quality bar as InjectionFree.

Changes

• Adds src/interface/abi/Typedqliser/ABI/SchemaBound.idr:
  • A faithful schema model — TableDef (name + declared columns), Schema, and a total, deterministic tableCols resolver — reusing the existing Query/Pred/Value AST from Semantics verbatim.
  • QuerySchemaBound s q — the proposition that the query's table resolves and every referenced column (projected ++ predicate) is declared. There is no constructor that admits a dangling reference, so the property is uninhabited for an unresolved column.
  • decSchemaBound : (s : Schema) -> (q : Query) -> Dec (QuerySchemaBound s q) — a sound + complete decision procedure, so a Proven SchemaBound certificate is backed by a constructive witness and a dangling reference can never be certified.
  • certifySchemaBound + certifySchemaBoundSound (a Proven verdict provably entails the property), and schemaBoundIsLevelTwo : levelNat SchemaBound = 2.
  • Positive control (an explicit witness and the certifier computing to Proven) and negative control (the ssn dangling reference 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/the/sym/absurd 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 (bootstrapped from source):

$ cd src/interface/abi && idris2 --build typedqliser-abi.ipkg
1/6: Building Typedqliser.ABI.Types ...
2/6: Building Typedqliser.ABI.Semantics ...
3/6: Building Typedqliser.ABI.SchemaBound ...
4/6: Building Typedqliser.ABI.Layout ...
5/6: Building Typedqliser.ABI.Proofs ...
6/6: 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 SchemaBound = 3 (it is 2) — rejected.
2. Elem "ssn" ["id","name","email"] — rejected (no witness exists).
3. A QuerySchemaBound exampleSchema unboundQuery witness for the dangling-reference 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