feat(sql): validate tables inside subqueries and derived tables (L2) (#43)

* 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

* ci: make CI green — bump rust-ci to standards@8dc2bf0 (toolchain: stable fix); port ABI-FFI gate Python->Bash (Python is estate-banned)

Resolves the standing baseline CI reds (rust-ci toolchain error, governance
Language/anti-pattern, governance workflow-lint) without altering the proven
ABI. The Bash gate reproduces the former Python gate's verdict verbatim
(validated across all -iser repos) and catches the same drift classes.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

* ci: adopt canonical Julia ABI-FFI gate (estate standard, matches verisimiser) in place of the interim Bash port

* style: cargo fmt + clippy --fix to satisfy rust-ci (fmt --check + clippy -D warnings)

* style: cargo fmt + clippy --fix under stable 1.96 (CI toolchain) — fmt --check + clippy -D warnings clean

* feat(sql): resolve table aliases in L2/L3/L4 checks

Aliased column references like `u.id` in `FROM users u` were not resolved
to their real table, so the schema-binding (L2), type-compatibility (L3),
and null-safety (L4) checks mishandled them: L2 raised false positives on
valid aliased queries, while L3/L4 silently skipped aliased columns (false
negatives). Build a qualifier->table map from the FROM/JOIN clauses and
resolve qualifiers through it across all three levels, including
alias-qualified projections in the null check.

Strengthens the previously no-op l2_valid_multi_table_join test and adds
L2/L3/L4 alias-resolution tests.

* feat(sql): null-check SELECT * + recognise CTE names (L4/L2 soundness)

Two more soundness holes in the SQL safety levels:

- L4 (null-safety): `SELECT *` / `u.*` were not expanded, so nullable
  columns selected via a wildcard were silently not flagged. Expand a
  wildcard to the in-scope table columns (resolving the alias for a
  qualified `u.*`) and flag the nullable ones.
- L2 (schema-binding): a `WITH cte AS (...)` name referenced in FROM was
  reported as 'table not found', a false positive. Collect CTE names and
  exclude them from the table-existence check.

Updates l4_select_star (was a no-op documenting the gap) to assert the
nullable columns are now flagged, and adds an L2 CTE test.

* feat(sql): validate tables inside subqueries and derived tables (L2)

Schema-binding (L2) only checked the outermost FROM, so a missing table
in a WHERE ... IN (SELECT ...) subquery, a derived table, a CTE body, or
a set operation went undetected (false negative). Add a recursive walk
that collects every real table source across all scopes plus the
non-schema sources (CTE names, derived-table aliases) to exclude, and use
it for the L2 table-existence check. Column resolution stays scoped to the
top level to avoid correlated-reference false positives.

Adds tests for a missing table in a subquery and in a derived table, and
a no-false-positive test for a valid subquery.

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

src/plugins/sql.rs

@@ -159,19 +159,133 @@ impl SqlPlugin {
             .unwrap_or_else(|| qualifier.to_string())
     }
 
-    /// Names introduced by a `WITH` clause. These act as table sources within
-    /// the query but are not part of the schema, so they must not be flagged as
-    /// "table not found".
-    fn extract_cte_names(statement: &Statement) -> Vec<String> {
-        let mut names = Vec::new();
-        if let Statement::Query(query) = statement
-            && let Some(with) = &query.with
-        {
+    /// Recursively collect every real table referenced anywhere in the
+    /// statement — top level, JOINs, CTE bodies, derived tables, and subqueries
+    /// in `WHERE`/`HAVING`/projection — alongside the "non-schema" sources that
+    /// must not be validated against the schema (CTE names and derived-table
+    /// aliases). Lets L2 catch a missing table inside a subquery, not just the
+    /// outermost `FROM`.
+    fn extract_all_table_sources(statement: &Statement) -> (Vec<String>, Vec<String>) {
+        let mut real = Vec::new();
+        let mut nonschema = Vec::new();
+        match statement {
+            Statement::Query(query) => Self::walk_query(query, &mut real, &mut nonschema),
+            Statement::Insert(insert) => {
+                real.push(insert.table_name.to_string().to_lowercase());
+                if let Some(source) = &insert.source {
+                    Self::walk_query(source, &mut real, &mut nonschema);
+                }
+            }
+            Statement::Update { table, .. } => Self::walk_twj(table, &mut real, &mut nonschema),
+            Statement::Delete(delete) => match &delete.from {
+                sqlparser::ast::FromTable::WithFromKeyword(twjs)
+                | sqlparser::ast::FromTable::WithoutKeyword(twjs) => {
+                    for twj in twjs {
+                        Self::walk_twj(twj, &mut real, &mut nonschema);
+                    }
+                }
+            },
+            _ => {}
+        }
+        real.sort();
+        real.dedup();
+        (real, nonschema)
+    }
+
+    fn walk_query(query: &Query, real: &mut Vec<String>, nonschema: &mut Vec<String>) {
+        if let Some(with) = &query.with {
             for cte in &with.cte_tables {
-                names.push(cte.alias.name.value.to_lowercase());
+                nonschema.push(cte.alias.name.value.to_lowercase());
+                Self::walk_query(&cte.query, real, nonschema);
             }
         }
-        names
+        Self::walk_setexpr(query.body.as_ref(), real, nonschema);
+    }
+
+    fn walk_setexpr(set: &SetExpr, real: &mut Vec<String>, nonschema: &mut Vec<String>) {
+        match set {
+            SetExpr::Select(select) => {
+                for twj in &select.from {
+                    Self::walk_twj(twj, real, nonschema);
+                }
+                if let Some(sel) = &select.selection {
+                    Self::walk_expr_subqueries(sel, real, nonschema);
+                }
+                for item in &select.projection {
+                    if let SelectItem::UnnamedExpr(e) | SelectItem::ExprWithAlias { expr: e, .. } =
+                        item
+                    {
+                        Self::walk_expr_subqueries(e, real, nonschema);
+                    }
+                }
+            }
+            SetExpr::Query(q) => Self::walk_query(q, real, nonschema),
+            SetExpr::SetOperation { left, right, .. } => {
+                Self::walk_setexpr(left, real, nonschema);
+                Self::walk_setexpr(right, real, nonschema);
+            }
+            _ => {}
+        }
+    }
+
+    fn walk_twj(twj: &TableWithJoins, real: &mut Vec<String>, nonschema: &mut Vec<String>) {
+        Self::walk_factor(&twj.relation, real, nonschema);
+        for join in &twj.joins {
+            Self::walk_factor(&join.relation, real, nonschema);
+        }
+    }
+
+    fn walk_factor(factor: &TableFactor, real: &mut Vec<String>, nonschema: &mut Vec<String>) {
+        match factor {
+            TableFactor::Table { name, .. } => real.push(name.to_string().to_lowercase()),
+            TableFactor::Derived {
+                subquery, alias, ..
+            } => {
+                if let Some(a) = alias {
+                    nonschema.push(a.name.value.to_lowercase());
+                }
+                Self::walk_query(subquery, real, nonschema);
+            }
+            TableFactor::NestedJoin {
+                table_with_joins, ..
+            } => Self::walk_twj(table_with_joins, real, nonschema),
+            _ => {}
+        }
+    }
+
+    /// Descend an expression to find nested subqueries (we only need their
+    /// table sources here, not their columns).
+    fn walk_expr_subqueries(expr: &Expr, real: &mut Vec<String>, nonschema: &mut Vec<String>) {
+        match expr {
+            Expr::Subquery(q) | Expr::Exists { subquery: q, .. } => {
+                Self::walk_query(q, real, nonschema)
+            }
+            Expr::InSubquery {
+                expr: inner,
+                subquery,
+                ..
+            } => {
+                Self::walk_expr_subqueries(inner, real, nonschema);
+                Self::walk_query(subquery, real, nonschema);
+            }
+            Expr::InList {
+                expr: inner, list, ..
+            } => {
+                Self::walk_expr_subqueries(inner, real, nonschema);
+                for e in list {
+                    Self::walk_expr_subqueries(e, real, nonschema);
+                }
+            }
+            Expr::BinaryOp { left, right, .. } => {
+                Self::walk_expr_subqueries(left, real, nonschema);
+                Self::walk_expr_subqueries(right, real, nonschema);
+            }
+            Expr::Nested(e)
+            | Expr::IsNull(e)
+            | Expr::IsNotNull(e)
+            | Expr::UnaryOp { expr: e, .. } => Self::walk_expr_subqueries(e, real, nonschema),
+            _ => {}
+        }
     }
 
     /// Extract all column references from a statement.
@@ -401,9 +515,12 @@ impl QueryLanguagePlugin for SqlPlugin {
             // Check table references
             let table_refs = Self::extract_table_refs(stmt);
             let aliases = Self::extract_table_aliases(stmt);
-            let cte_names = Self::extract_cte_names(stmt);
-            for table_name in &table_refs {
-                if !cte_names.contains(table_name)
+            // Validate table existence across every scope (including subqueries
+            // and derived tables), excluding non-schema sources (CTE names and
+            // derived-table aliases).
+            let (all_tables, nonschema_sources) = Self::extract_all_table_sources(stmt);
+            for table_name in &all_tables {
+                if !nonschema_sources.contains(table_name)
                     && !schema.tables.iter().any(|t| t.name == *table_name)
                 {
                     issues.push(SchemaIssue {

tests/integration_test.rs

@@ -653,6 +653,69 @@ fn l2_cte_name_not_flagged_as_missing_table() {
     );
 }
 
+#[test]
+fn l2_subquery_missing_table_flagged() {
+    // A missing table inside a `WHERE ... IN (SELECT ...)` subquery must be
+    // caught, not only the outermost FROM.
+    let plugin = get_plugin("sql").unwrap();
+    let schema = test_schema();
+    let issues = plugin
+        .schema_check(
+            "SELECT id FROM users WHERE id IN (SELECT user_id FROM nonexistent_table)",
+            &schema,
+        )
+        .unwrap();
+    assert!(
+        issues
+            .iter()
+            .any(|i| i.message.contains("nonexistent_table")),
+        "Missing table inside a subquery must be flagged. Got: {:?}",
+        issues
+    );
+}
+
+#[test]
+fn l2_valid_subquery_no_false_positive() {
+    // Both the outer and the subquery tables exist, so no table-binding issue.
+    let plugin = get_plugin("sql").unwrap();
+    let schema = test_schema();
+    let issues = plugin
+        .schema_check(
+            "SELECT id FROM users WHERE id IN (SELECT user_id FROM posts)",
+            &schema,
+        )
+        .unwrap();
+    assert!(
+        !issues.iter().any(|i| i.message.contains("not found")),
+        "Valid subquery over existing tables must not raise a binding issue. Got: {:?}",
+        issues
+    );
+}
+
+#[test]
+fn l2_derived_table_validated() {
+    // A derived table's inner FROM is validated (bogus_table flagged), while
+    // the derived-table alias `sub` is a non-schema source and is not flagged.
+    let plugin = get_plugin("sql").unwrap();
+    let schema = test_schema();
+    let issues = plugin
+        .schema_check(
+            "SELECT sub.x FROM (SELECT id FROM bogus_table) sub",
+            &schema,
+        )
+        .unwrap();
+    assert!(
+        issues.iter().any(|i| i.message.contains("bogus_table")),
+        "Missing table inside a derived table must be flagged. Got: {:?}",
+        issues
+    );
+    assert!(
+        !issues.iter().any(|i| i.message.contains("'sub'")),
+        "Derived-table alias 'sub' must not be flagged as a missing table. Got: {:?}",
+        issues
+    );
+}
+
 // ============================================================================
 // End-to-end: Full query -> manifest -> check pipeline
 // ============================================================================