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

* 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.

---------

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

Author: hyperpolymath

src/plugins/sql.rs

@@ -159,6 +159,21 @@ 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
+        {
+            for cte in &with.cte_tables {
+                names.push(cte.alias.name.value.to_lowercase());
+            }
+        }
+        names
+    }
+
     /// Extract all column references from a statement.
     fn extract_column_refs(statement: &Statement) -> Vec<(Option<String>, String)> {
         let mut cols = Vec::new();
@@ -386,8 +401,11 @@ 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 !schema.tables.iter().any(|t| t.name == *table_name) {
+                if !cte_names.contains(table_name)
+                    && !schema.tables.iter().any(|t| t.name == *table_name)
+                {
                     issues.push(SchemaIssue {
                         message: format!("Table '{}' not found in schema", table_name),
                     });
@@ -518,6 +536,43 @@ impl QueryLanguagePlugin for SqlPlugin {
                                 });
                             }
                         }
+                        // Unqualified `*`: expand to every nullable column of
+                        // each table in scope (so `SELECT * FROM users` is
+                        // null-checked, not silently skipped).
+                        SelectItem::Wildcard(_) => {
+                            for table_name in &table_refs {
+                                if let Some(table) =
+                                    schema.tables.iter().find(|t| t.name == *table_name)
+                                {
+                                    for col in table.columns.iter().filter(|c| c.nullable) {
+                                        issues.push(NullIssue {
+                                            message: format!(
+                                                "Nullable column '{}' selected via wildcard without COALESCE or null handling",
+                                                col.name
+                                            ),
+                                            column: col.name.clone(),
+                                        });
+                                    }
+                                }
+                            }
+                        }
+                        // Alias-qualified `u.*`: expand the resolved table only.
+                        SelectItem::QualifiedWildcard(obj, _) => {
+                            let table_name =
+                                Self::resolve_qualifier(&aliases, &obj.to_string().to_lowercase());
+                            if let Some(table) = schema.tables.iter().find(|t| t.name == table_name)
+                            {
+                                for col in table.columns.iter().filter(|c| c.nullable) {
+                                    issues.push(NullIssue {
+                                        message: format!(
+                                            "Nullable column '{}' selected via wildcard without COALESCE or null handling",
+                                            col.name
+                                        ),
+                                        column: col.name.clone(),
+                                    });
+                                }
+                            }
+                        }
                         _ => {}
                     }
                 }

tests/integration_test.rs

@@ -608,17 +608,48 @@ fn l4_nullable_comment_author() {
 }
 
 #[test]
-fn l4_select_star_not_flagged() {
-    // SELECT * doesn't produce individual Identifier expressions for each column,
-    // so the null checker won't flag individual columns.
+fn l4_select_star_flags_nullable() {
+    // `SELECT *` is expanded to the table's columns, so its nullable columns
+    // (users.email, users.age) are flagged like an explicit selection would be.
     let plugin = get_plugin("sql").unwrap();
     let schema = test_schema();
     let issues = plugin.null_check("SELECT * FROM users", &schema).unwrap();
-    // The current implementation only checks UnnamedExpr(Identifier), not Wildcard.
-    // This test documents current behavior.
     assert!(
-        issues.is_empty(),
-        "SELECT * is not individually checked for null (current behavior)"
+        issues.iter().any(|i| i.column == "email"),
+        "SELECT * must flag nullable 'email'. Got: {:?}",
+        issues
+    );
+    assert!(
+        issues.iter().any(|i| i.column == "age"),
+        "SELECT * must flag nullable 'age'. Got: {:?}",
+        issues
+    );
+    // Non-nullable columns (id, name) must NOT be flagged.
+    assert!(
+        !issues
+            .iter()
+            .any(|i| i.column == "id" || i.column == "name"),
+        "SELECT * must not flag non-nullable columns. Got: {:?}",
+        issues
+    );
+}
+
+#[test]
+fn l2_cte_name_not_flagged_as_missing_table() {
+    // A CTE name is a valid in-query table source, not a schema table, so it
+    // must not be reported as "not found in schema".
+    let plugin = get_plugin("sql").unwrap();
+    let schema = test_schema();
+    let issues = plugin
+        .schema_check(
+            "WITH recent AS (SELECT id FROM users) SELECT id FROM recent",
+            &schema,
+        )
+        .unwrap();
+    assert!(
+        !issues.iter().any(|i| i.message.contains("recent")),
+        "CTE name 'recent' must not be flagged as a missing table. Got: {:?}",
+        issues
     );
 }