From 21a9a23d69ee675c373901ffd20e178c1d05507b Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Jul 2026 18:18:13 +0100
Subject: [PATCH 1/4] test: make the test suites capable of failing, and wire
 `lake test`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Foundation work before any axiom is discharged: nothing in this repo could be
verified by running it, so every proof-debt item was unfalsifiable in practice.

Four layers of the base were soft, and each hid the next:

1. `lake test` reported "no test driver configured" — no driver existed.
2. The suites printed "FAIL"/"✗" and then printed "All tests passed!"
   unconditionally, with `main : IO Unit`, so the process always exited 0.
   LexerTest even documented a counter — "Count of test failures, tracked via
   IO.Ref" — that was never implemented.
3. `test/TypeSafetyTests.lean` was declared by NO Lake target, so it was never
   built. It had rotted and no longer compiled.
4. `lake build` only builds the default target (the `GqlDt` library), so the
   test executables were never compiled by CI either. `lexer_test` had also
   rotted.

Changes:

* `test/TestHarness.lean` (new) — the failure counter LexerTest's comment
  promised, plus `summarise`, which turns the tally into a process exit code.
* All four suites now record failures and return `IO UInt32`. ParserTest's 18
  `✗` sites were printing to stdout and returning Unit; they now record.
  The unconditional "All tests passed!" banners are gone.
* `lakefile.lean` — added `lean_lib TestSupport` (so the suites can import the
  harness), `lean_exe type_safety_test` (previously unbuildable), and a
  `@[test_driver] script test` that runs the Lean suites and aggregates exit
  codes. ffi_test is deliberately excluded: it links liblith_bridge.a and is
  covered by the zig-ffi CI job, so including it would make `lake test` fail on
  a clean checkout for a non-Lean reason.

Compile fixes needed to get the rotted suites building at all:

* LexerTest: `String.containsSubstr` does not exist in Lean 4.15. All three
  probes test single characters, so `String.contains` is the right primitive.
* TypeSafetyTests: `Prompt`/`Provenance` were not opened; `insertEvidence`
  takes a `Provenance.Rationale`, not a `NonEmptyString`; `BoundedNat`'s
  min/max are structure PARAMETERS, not fields, so `BoundedNat.mk 0 100 100 …`
  passed bounds as data — replaced with anonymous constructors that let the
  expected type supply them. Added a top-level `main` alias, since the suite's
  `main` sits inside a namespace and the linker found no entry point.

Result: `lake test` runs, exits 1, and reports 19 REAL failures in the lexer
that were previously invisible — multi-character operators (`<=`, `>=`, `!=`,
`<>`) never lex as single tokens, `:` lexes as `::`, a bare `-` produces no
token at all, and block comments are unimplemented (`/* b */` lexes as
`/ * b * /`). Parser and TypeSafety suites pass.

Those 19 are NOT fixed here — this commit only makes them visible. The README's
"✅ Lexer: ... operators, literals, comments" claim is now known to be false.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 lakefile.lean             | 45 +++++++++++++++++++++++++++++++++
 test/FFITest.lean         |  6 +++--
 test/LexerTest.lean       | 25 ++++++++++--------
 test/ParserTest.lean      | 40 +++++++++++++++--------------
 test/TestHarness.lean     | 53 +++++++++++++++++++++++++++++++++++++++
 test/TypeSafetyTests.lean | 35 ++++++++++++++++++--------
 6 files changed, 163 insertions(+), 41 deletions(-)
 create mode 100644 test/TestHarness.lean

diff --git a/lakefile.lean b/lakefile.lean
index d0a4d83..95f9c17 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -22,6 +22,13 @@ lean_lib GqlDt where
   srcDir := "src"
   roots := #[`GqlDt]
 
+-- Shared test support (failure counter + exit-code summary).
+-- Declared as a library so the individual test executables can `import TestHarness`;
+-- a bare file under a target's srcDir is not otherwise resolvable as a module.
+lean_lib TestSupport where
+  srcDir := "test"
+  roots := #[`TestHarness]
+
 -- FFI Test executable (requires Zig library to be built first)
 -- Build Zig lib: cd bridge && zig build
 lean_exe ffi_test where
@@ -43,6 +50,44 @@ lean_exe lexer_test where
   srcDir := "test"
   root := `LexerTest
 
+-- Type-safety test executable.
+-- test/TypeSafetyTests.lean existed but was declared by no target, so it was never
+-- built and never run — it could not even fail to compile.
+lean_exe type_safety_test where
+  srcDir := "test"
+  root := `TypeSafetyTests
+
+-- Test driver: `lake test`.
+--
+-- Without this, `lake test` reported "no test driver configured" and exited non-zero,
+-- so CI had to tolerate that failure — which meant CI also tolerated genuine test
+-- failures. The suites below now return a real exit code (see test/TestHarness.lean).
+--
+-- ffi_test is deliberately excluded: it links against bridge/zig-out/lib/liblith_bridge.a,
+-- which requires `cd bridge && zig build` first. It is run separately by the zig-ffi CI
+-- job, where that artifact is guaranteed to exist. Including it here would make `lake test`
+-- fail on a clean checkout for a reason unrelated to Lean.
+@[test_driver]
+script test do
+  let suites := #["lexer_test", "parser_test", "type_safety_test"]
+  let mut failed : Array String := #[]
+  for suite in suites do
+    let bin := System.mkFilePath [".lake", "build", "bin", suite]
+    if !(← System.FilePath.pathExists bin) then
+      IO.eprintln s!"✗ {suite}: binary not found at {bin} — run `lake build` first"
+      failed := failed.push suite
+      continue
+    IO.println s!"\n▶ {suite}"
+    let child ← IO.Process.spawn { cmd := bin.toString }
+    if (← child.wait) != 0 then
+      failed := failed.push suite
+  if failed.isEmpty then
+    IO.println s!"\n✅ all {suites.size} Lean suite(s) passed"
+    return 0
+  else
+    IO.eprintln s!"\n❌ FAILED: {String.intercalate ", " failed.toList}"
+    return 1
+
 -- GQLdt CLI/REPL (with FFI persistence backend)
 lean_exe gqldt where
   srcDir := "src"
diff --git a/test/FFITest.lean b/test/FFITest.lean
index db8ddb8..b6df2fc 100644
--- a/test/FFITest.lean
+++ b/test/FFITest.lean
@@ -11,6 +11,7 @@
 -- 3. Run: .lake/build/bin/ffi_test
 
 import GqlDt.FFI.Bridge
+import TestHarness
 import GqlDt.Types.BoundedNat
 import GqlDt.Prompt.PromptScores
 
@@ -118,7 +119,7 @@ def testIntegration : IO Unit := do
   IO.println "✓ Integration tests passed"
 
 /-- Main test runner -/
-def main : IO Unit := do
+def main : IO UInt32 := do
   IO.println "═══════════════════════════════════════════════"
   IO.println "  GqlDt FFI Integration Tests"
   IO.println "═══════════════════════════════════════════════"
@@ -137,5 +138,6 @@ def main : IO Unit := do
   IO.println ""
 
   IO.println "═══════════════════════════════════════════════"
-  IO.println "  All tests passed!"
+  IO.println "  FFI tests completed"
   IO.println "═══════════════════════════════════════════════"
+  GnplTest.summarise "FFI"
diff --git a/test/LexerTest.lean b/test/LexerTest.lean
index 580d4dd..f82ddd5 100644
--- a/test/LexerTest.lean
+++ b/test/LexerTest.lean
@@ -10,6 +10,7 @@
 -- Run with: lake build lexer_test && lake env lean --run test/LexerTest.lean
 
 import GqlDt.Lexer
+import TestHarness
 
 open GqlDt.Lexer
 
@@ -17,12 +18,15 @@ open GqlDt.Lexer
 -- Test Helpers
 -- ============================================================================
 
-/-- Count of test failures, tracked via IO.Ref -/
-def runTest (name : String) (passed : Bool) : IO Unit := do
-  if passed then
-    IO.println s!"  PASS: {name}"
-  else
-    IO.eprintln s!"  FAIL: {name}"
+/--
+Run one named check, recording the outcome in the shared failure counter.
+
+Previously this printed `FAIL` and returned `Unit`, so a failing check left no trace the
+process could act on — despite the doc comment claiming a counter. It now delegates to
+`GnplTest.check`, and `main` turns the tally into an exit code.
+-/
+def runTest (name : String) (passed : Bool) : IO Unit :=
+  GnplTest.check name passed
 
 /-- Extract token types from a tokenization result, excluding EOF -/
 def tokenTypes (result : Except String (List Token)) : List TokenType :=
@@ -259,19 +263,19 @@ def testStringLiterals : IO Unit := do
   -- Escape sequences
   runTest "'line\\nbreak'" (
     match firstType "'line\\nbreak'" with
-    | some (.litString s) => s.containsSubstr "\n"
+    | some (.litString s) => s.contains '\n'
     | _ => false
   )
 
   runTest "'tab\\there'" (
     match firstType "'tab\\there'" with
-    | some (.litString s) => s.containsSubstr "\t"
+    | some (.litString s) => s.contains '\t'
     | _ => false
   )
 
   runTest "'escaped\\\\backslash'" (
     match firstType "'escaped\\\\backslash'" with
-    | some (.litString s) => s.containsSubstr "\\"
+    | some (.litString s) => s.contains '\\'
     | _ => false
   )
 
@@ -586,7 +590,7 @@ def testEdgeCases : IO Unit := do
 -- Main Test Runner
 -- ============================================================================
 
-def main : IO Unit := do
+def main : IO UInt32 := do
   IO.println "==============================================="
   IO.println "  GQL-DT Lexer Unit Tests"
   IO.println "==============================================="
@@ -611,3 +615,4 @@ def main : IO Unit := do
   IO.println "==============================================="
   IO.println "  Lexer tests completed"
   IO.println "==============================================="
+  GnplTest.summarise "Lexer"
diff --git a/test/ParserTest.lean b/test/ParserTest.lean
index 5465595..dc74b0c 100644
--- a/test/ParserTest.lean
+++ b/test/ParserTest.lean
@@ -6,6 +6,7 @@
 -- Run with: lake build && lean --run test/ParserTest.lean
 
 import GqlDt.Query
+import TestHarness
 
 open GqlDt.Query
 open GqlDt.Query.Parser
@@ -17,7 +18,7 @@ def testSelectAll : IO Unit := do
   | .ok q =>
     IO.println s!"  ✓ Parsed: table = {q.from.name}, projection = all"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test SELECT with columns -/
 def testSelectColumns : IO Unit := do
@@ -31,7 +32,7 @@ def testSelectColumns : IO Unit := do
     | _ =>
       IO.println "    (unexpected projection type)"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test SELECT with WHERE clause -/
 def testSelectWhere : IO Unit := do
@@ -45,7 +46,7 @@ def testSelectWhere : IO Unit := do
     | none =>
       IO.println "    where = none"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test INSERT statement -/
 def testInsert : IO Unit := do
@@ -57,9 +58,9 @@ def testInsert : IO Unit := do
       IO.println s!"  ✓ Parsed INSERT: table = {i.table.name}"
       IO.println s!"    values count = {i.values.length}"
     | _ =>
-      IO.println "  ✗ Got wrong statement type"
+      GnplTest.fail "✗ Got wrong statement type"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test INSERT with provenance -/
 def testInsertProvenance : IO Unit := do
@@ -73,9 +74,9 @@ def testInsertProvenance : IO Unit := do
       IO.println s!"    actor = {repr i.actor}"
       IO.println s!"    rationale = {repr i.rationale}"
     | _ =>
-      IO.println "  ✗ Got wrong statement type"
+      GnplTest.fail "✗ Got wrong statement type"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test UPDATE statement -/
 def testUpdate : IO Unit := do
@@ -88,9 +89,9 @@ def testUpdate : IO Unit := do
       IO.println s!"    set count = {u.set.length}"
       IO.println s!"    has where = {u.whereClause.isSome}"
     | _ =>
-      IO.println "  ✗ Got wrong statement type"
+      GnplTest.fail "✗ Got wrong statement type"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test DELETE statement -/
 def testDelete : IO Unit := do
@@ -102,9 +103,9 @@ def testDelete : IO Unit := do
       IO.println s!"  ✓ Parsed DELETE: table = {d.table.name}"
       IO.println s!"    has where = {d.whereClause.isSome}"
     | _ =>
-      IO.println "  ✗ Got wrong statement type"
+      GnplTest.fail "✗ Got wrong statement type"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Test expression parsing -/
 def testExpressions : IO Unit := do
@@ -113,31 +114,31 @@ def testExpressions : IO Unit := do
   -- Simple comparison
   match parseExpr "x = 1" with
   | .ok _ => IO.println "  ✓ x = 1"
-  | .error e => IO.println s!"  ✗ x = 1: {e}"
+  | .error e => GnplTest.fail s!"✗ x = 1: {e}"
 
   -- String comparison
   match parseExpr "name = \"Alice\"" with
   | .ok _ => IO.println "  ✓ name = \"Alice\""
-  | .error e => IO.println s!"  ✗ name = \"Alice\": {e}"
+  | .error e => GnplTest.fail s!"✗ name = \"Alice\": {e}"
 
   -- AND expression
   match parseExpr "a = 1 AND b = 2" with
   | .ok _ => IO.println "  ✓ a = 1 AND b = 2"
-  | .error e => IO.println s!"  ✗ a = 1 AND b = 2: {e}"
+  | .error e => GnplTest.fail s!"✗ a = 1 AND b = 2: {e}"
 
   -- OR expression
   match parseExpr "a = 1 OR b = 2" with
   | .ok _ => IO.println "  ✓ a = 1 OR b = 2"
-  | .error e => IO.println s!"  ✗ a = 1 OR b = 2: {e}"
+  | .error e => GnplTest.fail s!"✗ a = 1 OR b = 2: {e}"
 
   -- Comparison operators
   match parseExpr "x > 10" with
   | .ok _ => IO.println "  ✓ x > 10"
-  | .error e => IO.println s!"  ✗ x > 10: {e}"
+  | .error e => GnplTest.fail s!"✗ x > 10: {e}"
 
   match parseExpr "x <= 100" with
   | .ok _ => IO.println "  ✓ x <= 100"
-  | .error e => IO.println s!"  ✗ x <= 100: {e}"
+  | .error e => GnplTest.fail s!"✗ x <= 100: {e}"
 
 /-- Test SELECT with ORDER BY and LIMIT -/
 def testSelectAdvanced : IO Unit := do
@@ -148,10 +149,10 @@ def testSelectAdvanced : IO Unit := do
     IO.println s!"    orderBy count = {q.orderBy.length}"
     IO.println s!"    limit = {repr q.limit}"
   | .error e =>
-    IO.println s!"  ✗ Failed: {e}"
+    GnplTest.fail s!"✗ Failed: {e}"
 
 /-- Main test runner -/
-def main : IO Unit := do
+def main : IO UInt32 := do
   IO.println "═══════════════════════════════════════════════"
   IO.println "  GQL Parser Tests"
   IO.println "═══════════════════════════════════════════════"
@@ -187,3 +188,4 @@ def main : IO Unit := do
   IO.println "═══════════════════════════════════════════════"
   IO.println "  Parser tests completed"
   IO.println "═══════════════════════════════════════════════"
+  GnplTest.summarise "Parser"
diff --git a/test/TestHarness.lean b/test/TestHarness.lean
new file mode 100644
index 0000000..bc79514
--- /dev/null
+++ b/test/TestHarness.lean
@@ -0,0 +1,53 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+-- TestHarness.lean — shared failure accounting for the GQLdt test suites.
+--
+-- Why this exists: every suite in test/ previously printed "FAIL"/"✗" to stdout and
+-- then carried on to print "All tests passed!" unconditionally, with `main : IO Unit`
+-- so the process always exited 0. A failing test was therefore invisible to `lake test`,
+-- to CI, and to a human skim-reading the tail of the log.
+--
+-- LexerTest even documented a failure counter — "Count of test failures, tracked via
+-- IO.Ref" — that was never implemented.
+--
+-- This module supplies the counter that comment promised, and `summarise` turns it into
+-- a process exit code. A suite is only honest if a failing check can turn it red.
+
+namespace GnplTest
+
+/-- Number of failed checks recorded so far, across every suite in this process. -/
+initialize failureCount : IO.Ref Nat ← IO.mkRef 0
+
+/-- Record a passing check. -/
+def pass (name : String) : IO Unit :=
+  IO.println s!"  PASS: {name}"
+
+/-- Record a failing check. Increments the counter that `summarise` reads. -/
+def fail (name : String) (detail : String := "") : IO Unit := do
+  failureCount.modify (· + 1)
+  if detail.isEmpty then
+    IO.eprintln s!"  FAIL: {name}"
+  else
+    IO.eprintln s!"  FAIL: {name} — {detail}"
+
+/-- Assert a boolean condition, recording the outcome either way. -/
+def check (name : String) (passed : Bool) : IO Unit :=
+  if passed then pass name else fail name
+
+/--
+Print the suite verdict and yield the process exit code: `0` iff nothing failed.
+
+Use as the last line of `main`, whose type must be `IO UInt32` for the code to reach
+the operating system.
+-/
+def summarise (suite : String) : IO UInt32 := do
+  let n ← failureCount.get
+  if n == 0 then
+    IO.println s!"✅ {suite}: all checks passed"
+    return 0
+  else
+    IO.eprintln s!"❌ {suite}: {n} check(s) FAILED"
+    return 1
+
+end GnplTest
diff --git a/test/TypeSafetyTests.lean b/test/TypeSafetyTests.lean
index 055e5ff..165c5d9 100644
--- a/test/TypeSafetyTests.lean
+++ b/test/TypeSafetyTests.lean
@@ -5,6 +5,7 @@
 -- Demonstrate type safety enforcement at compile time
 
 import GqlDt.TypeSafe
+import TestHarness
 import GqlDt.TypeChecker
 import GqlDt.Types.BoundedNat
 import GqlDt.Types.NonEmptyString
@@ -12,19 +13,28 @@ import GqlDt.Prompt
 
 namespace GqlDt.Tests.TypeSafety
 
-open TypeSafe TypeChecker AST Types
+-- `Prompt` and `Provenance` are needed for PromptScores.create and Rationale respectively.
+-- Their absence is why this file stopped compiling: it was declared by no Lake target, so
+-- nothing ever built it and the rot went unnoticed.
+open TypeSafe TypeChecker AST Types Prompt Provenance
 
 -- Test 1: Valid insertion compiles
 def test_valid_insert : InsertStmt evidenceSchema :=
   let title := NonEmptyString.mk "Test Evidence" (by decide)
+  -- `min`/`max` are structure *parameters* of BoundedNat, not fields — the old
+  -- `BoundedNat.mk 0 100 100 …` passed them as data, which is why this stopped
+  -- elaborating. The anonymous constructor lets the expected type (PromptDimension,
+  -- i.e. BoundedNat 0 100) supply them, leaving val + the two bound proofs.
   let scores := PromptScores.create
-    (BoundedNat.mk 0 100 100 (by omega) (by omega))
-    (BoundedNat.mk 0 100 100 (by omega) (by omega))
-    (BoundedNat.mk 0 100 95 (by omega) (by omega))
-    (BoundedNat.mk 0 100 95 (by omega) (by omega))
-    (BoundedNat.mk 0 100 100 (by omega) (by omega))
-    (BoundedNat.mk 0 100 95 (by omega) (by omega))
-  let rationale := NonEmptyString.mk "Test rationale" (by decide)
+    ⟨100, by omega, by omega⟩
+    ⟨100, by omega, by omega⟩
+    ⟨95,  by omega, by omega⟩
+    ⟨95,  by omega, by omega⟩
+    ⟨100, by omega, by omega⟩
+    ⟨95,  by omega, by omega⟩
+  -- insertEvidence takes a Provenance.Rationale, not a bare NonEmptyString — the whole
+  -- point of the type is that a rationale cannot be confused with any other string.
+  let rationale := Rationale.fromString "Test rationale"
 
   insertEvidence title scores rationale
 
@@ -130,7 +140,7 @@ theorem typeSafeQueriesPreserveInvariants {schema : Schema} (stmt : InsertStmt s
   exact valueInvariant_holds (stmt.values.get i)
 
 -- Run all tests
-def main : IO Unit := do
+def main : IO UInt32 := do
   IO.println "=== GQLdt Type Safety Tests ==="
   IO.println ""
 
@@ -151,6 +161,11 @@ def main : IO Unit := do
   test_execution_safety
   IO.println ""
 
-  IO.println "=== All tests passed! ==="
+  IO.println "=== Type-safety tests completed ==="
+  GnplTest.summarise "TypeSafety"
 
 end GqlDt.Tests.TypeSafety
+
+/-- Top-level entry point. The suite's `main` lives inside `GqlDt.Tests.TypeSafety`, so
+    without this alias the linker finds no `main` symbol and the executable fails to link. -/
+def main : IO UInt32 := GqlDt.Tests.TypeSafety.main

From 0077806ca9b4e701b602a96d95cb355a2d239b4a Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 28 Jul 2026 19:19:23 +0100
Subject: [PATCH 2/4] fix(lexer): two-character lookahead was off by one
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`LexerState.peek` takes an offset whose default is 1 and where **0 means the
CURRENT character** — `s.peek 0` is exactly `s.curr`. All seven two-character
lookahead sites passed 0, so every one compared the character it already held
against the character it expected next. The branches were all present and
correct; none could ever be taken.

Consequences, all of which `spec/GQL-DT-Lexical.md` mandates and none of which
worked:

* `<=`, `>=`, `!=`, `<>` (§ operator table, precedence 5) never lexed as single
  tokens — `<=` came out as `[opLt, opEq]`.
* `:` lexed as `::`. The lookahead saw its own `:` at offset 0, matched the
  double-colon branch, emitted `opDoubleColon` and advanced TWICE. The spec
  makes these distinct: `::` is cons (prec 6), `:` is type annotation.
* A bare `-` produced NO token: `skipWhitespaceAndComments` matched
  (curr, peek 0) = ('-', '-') and treated a single minus as the start of a line
  comment, swallowing the rest of the input.
* §8.2 C-style block comments were never recognised — `/* b */` lexed as
  `/ * b * /`.

Fix is `peek 0` → `peek 1` at all seven sites.

Also corrects one genuine TEST bug this exposed: `schema::table` was expected to
yield three identifiers, but `table` is a reserved SQL keyword and keywords are
case-insensitive, so it correctly lexes as `.kwTable` — as this same suite
asserts under "SQL Keywords". The qualified-identifier case now uses a
non-reserved name, and the keyword interaction is asserted explicitly rather
than left as a latent contradiction between two tests.

`lake test`: 19 failures → 0. 163 checks across Lexer/Parser/TypeSafety, exit 0.

Canary-tested both directions, because a gate that has never gone red is not
evidence of anything: seeding `firstType "SELECT" == some .kwDelete` turns
`lake test` red (exit 1, "Lexer: 1 check(s) FAILED"); removing it returns exit 0.

READMEs updated. The "✅ Lexer: ... operators, literals, comments" claim was
false when written and is now true and verified rather than asserted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 README.adoc          |  3 ++-
 README.md            |  5 ++++-
 src/GqlDt/Lexer.lean | 14 +++++++-------
 test/LexerTest.lean  | 11 +++++++++--
 4 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/README.adoc b/README.adoc
index 73cb46e..91765d7 100644
--- a/README.adoc
+++ b/README.adoc
@@ -76,7 +76,8 @@ Lithoglyph-as-a-database is the second. See the design documents below.
   no incomplete proofs — but see the trusted-base caveat below
 | Proof obligations | *16 axioms outstanding* | all stubs, none necessary; enumerated in
   link:docs/proof-debt.md[`docs/proof-debt.md`]
-| Tests | *none* | `lake test` reports `no test driver configured`
+| Tests | *163 checks, green* | `lake test` runs Lexer/Parser/TypeSafety suites. The gate is
+  canary-tested: a seeded false check turns it red
 | Zig FFI bridge (`bridge/`) | *builds* | produces `zig-out/lib/liblith_bridge.a`, the
   artifact `lakefile.lean` links; `zig build test` passes
 | GNPL narration layer | *design* | `docs/THEORY.adoc` + `docs/LITHOGLYPH.adoc`; no code yet
diff --git a/README.md b/README.md
index e106912..98a145f 100644
--- a/README.md
+++ b/README.md
@@ -78,7 +78,10 @@ GQLdt extends [Lithoglyph](https://github.com/hyperpolymath/nextgen-databases/tr
 - 🟡 M6: GQL-DT/GQL Parser (substantially complete - see below)
 
 **M6 Parser Status** (Substantially Complete):
-- ✅ Lexer: Hand-rolled 540-line implementation (80+ keywords, operators, literals, comments)
+- ✅ Lexer: Hand-rolled 540-line implementation (80+ keywords, operators, literals,
+  comments) — verified by 163 executable checks (`lake test`), not asserted. Two-character
+  lookahead was off by one until 2026-07-27, so `<=`/`>=`/`!=`/`<>` never lexed as single
+  tokens, `:` lexed as `::`, and block comments were skipped entirely; fixed and covered.
 - ✅ Parser: Combinator-based parser for INSERT/SELECT/UPDATE/DELETE
 - ✅ Type System: Refinement types, PROMPT scores, provenance tracking
 - ✅ Pipeline: 6-stage compilation (tokenize → parse → type check → IR → validate → serialize)
diff --git a/src/GqlDt/Lexer.lean b/src/GqlDt/Lexer.lean
index 34b90af..59e8cb2 100644
--- a/src/GqlDt/Lexer.lean
+++ b/src/GqlDt/Lexer.lean
@@ -263,14 +263,14 @@ partial def skipLineComment (s : LexerState) : LexerState :=
   | some _ => skipLineComment s.advance
 
 partial def skipBlockComment (s : LexerState) : LexerState :=
-  match s.curr, s.peek 0 with
+  match s.curr, s.peek 1 with
   | some '*', some '/' => s.advance.advance
   | none, _ => s
   | _, _ => skipBlockComment s.advance
 
 partial def skipWhitespaceAndComments (s : LexerState) : LexerState :=
   let s' := skipWhitespace s
-  match s'.curr, s'.peek 0 with
+  match s'.curr, s'.peek 1 with
   | some '-', some '-' => skipWhitespaceAndComments (skipLineComment (s'.advance.advance))
   | some '/', some '*' => skipWhitespaceAndComments (skipBlockComment (s'.advance.advance))
   | _, _ => s'
@@ -295,7 +295,7 @@ partial def parseString (s : LexerState) (quote : Char) : LexerState × String :
       if c = quote then
         (state.advance, acc)
       else if c = '\\' then
-        match state.peek 0 with
+        match state.peek 1 with
         | some 'n' => loop (state.advance.advance) (acc ++ "\n")
         | some 't' => loop (state.advance.advance) (acc ++ "\t")
         | some 'r' => loop (state.advance.advance) (acc ++ "\r")
@@ -357,21 +357,21 @@ def tokenizeOne (s : LexerState) : Option (Token × LexerState) :=
       else if c = '^' then some ({ type := .opCaret, line := line, column := column, lexeme := "^" }, s'.advance)
       else if c = '=' then some ({ type := .opEq, line := line, column := column, lexeme := "=" }, s'.advance)
       else if c = '<' then
-        match s'.peek 0 with
+        match s'.peek 1 with
         | some '=' => some ({ type := .opLe, line := line, column := column, lexeme := "<=" }, s'.advance.advance)
         | some '>' => some ({ type := .opNeq, line := line, column := column, lexeme := "<>" }, s'.advance.advance)
         | _ => some ({ type := .opLt, line := line, column := column, lexeme := "<" }, s'.advance)
       else if c = '>' then
-        match s'.peek 0 with
+        match s'.peek 1 with
         | some '=' => some ({ type := .opGe, line := line, column := column, lexeme := ">=" }, s'.advance.advance)
         | _ => some ({ type := .opGt, line := line, column := column, lexeme := ">" }, s'.advance)
       else if c = '!' then
-        match s'.peek 0 with
+        match s'.peek 1 with
         | some '=' => some ({ type := .opNeq, line := line, column := column, lexeme := "!=" }, s'.advance.advance)
         | _ => some ({ type := .opNot, line := line, column := column, lexeme := "!" }, s'.advance)
       else if c = '.' then some ({ type := .opDot, line := line, column := column, lexeme := "." }, s'.advance)
       else if c = ':' then
-        match s'.peek 0 with
+        match s'.peek 1 with
         | some ':' => some ({ type := .opDoubleColon, line := line, column := column, lexeme := "::" }, s'.advance.advance)
         | _ => some ({ type := .opColon, line := line, column := column, lexeme := ":" }, s'.advance)
       else if c = '(' then some ({ type := .leftParen, line := line, column := column, lexeme := "(" }, s'.advance)
diff --git a/test/LexerTest.lean b/test/LexerTest.lean
index f82ddd5..041a38c 100644
--- a/test/LexerTest.lean
+++ b/test/LexerTest.lean
@@ -316,8 +316,15 @@ def testIdentifiers : IO Unit := do
   )
 
   -- Qualified identifier via double colon
-  runTest "schema::table tokenizes" (
-    expectTypes "schema::table" [.identifier "schema", .opDoubleColon, .identifier "table"]
+  -- NB: the operand must not be a reserved word. `schema::table` does NOT produce three
+  -- identifiers, because SQL keywords are case-insensitive and `table` therefore lexes as
+  -- `.kwTable` — as this same suite asserts under "SQL Keywords". That is correct
+  -- behaviour, so the qualified-identifier case is tested with a non-reserved name.
+  runTest "schema::customers tokenizes" (
+    expectTypes "schema::customers" [.identifier "schema", .opDoubleColon, .identifier "customers"]
+  )
+  runTest "schema::table — `table` stays a keyword" (
+    expectTypes "schema::table" [.identifier "schema", .opDoubleColon, .kwTable]
   )
 
 -- ============================================================================

From 60947bb7d3fea771f3336574055baaccd0417691 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 28 Jul 2026 19:22:49 +0100
Subject: [PATCH 3/4] docs: add governance files, written for this repo rather
 than swept in
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Re-adds the five C-A-G-M files proposed by the unmerged `sweep4` commit
("Generated by Mistral Vibe"), which was the only one of the three sweeps whose
content was not already superseded. Not replayed — rewritten, because the sweep
version had two defects:

* `.github/CODEOWNERS` and `.github/funding.yml` named @metadatastician, which
  owns other estate repositories but not this one. Ownership here is
  @hyperpolymath.
* `ARCHITECTURE.md` was generic boilerplate describing a `src/ tests/ config/`
  layout with "modular, maintainable architecture designed for clarity,
  scalability and long-term sustainability". This repository has none of those
  directories. It would have actively misdescribed a Lean 4 + Zig + Idris2
  project — worse than having no file.

What they say instead:

* ARCHITECTURE.md — the real two-layer structure (GNPL lowers to GQLdt lowers to
  the Zig bridge), the actual directory map, the build ORDER (the Zig archive
  must exist before Lean links, which is what the Containerfile used to get
  backwards), and a verification-posture table naming each gate and what it does
  and does not establish.
* GOVERNANCE.md — the rules a change must clear, each traced to a specific past
  failure rather than asserted as principle: no handwaving, gates must be shown
  to go red, specs are normative, the trusted base is enumerated, foundation
  before depth. Also records the two cross-cutting surfaces that cannot be
  changed on one side only — the FFI boundary, and PROMPT scoring, where the
  averaging rule is welded into a proof field.
* MAINTAINERS, CODEOWNERS, funding.yml — correct owner; CODEOWNERS additionally
  calls out the proof surface, the ABI and docs/proof-debt.md.

The sweep commits remain on `backup/sweeps-mistral-vibe`; nothing is lost.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/CODEOWNERS  | 13 ++++++++
 .github/funding.yml |  2 ++
 ARCHITECTURE.md     | 78 +++++++++++++++++++++++++++++++++++++++++++++
 GOVERNANCE.md       | 62 +++++++++++++++++++++++++++++++++++
 MAINTAINERS         | 23 +++++++++++++
 5 files changed, 178 insertions(+)
 create mode 100644 .github/CODEOWNERS
 create mode 100644 .github/funding.yml
 create mode 100644 ARCHITECTURE.md
 create mode 100644 GOVERNANCE.md
 create mode 100644 MAINTAINERS

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
new file mode 100644
index 0000000..b6ca674
--- /dev/null
+++ b/.github/CODEOWNERS
@@ -0,0 +1,13 @@
+# Code owners for hyperpolymath/gnpl.
+#
+# NB: an earlier unmerged sweep proposed this file naming @metadatastician, which owns
+# other repositories in the estate but not this one. Ownership here is @hyperpolymath.
+
+* @hyperpolymath
+
+# The proof surface and the FFI boundary carry the load-bearing correctness claims;
+# call them out so changes there are never merged unreviewed.
+/src/GqlDt/       @hyperpolymath
+/src/GQLdt/ABI/   @hyperpolymath
+/bridge/          @hyperpolymath
+/docs/proof-debt.md @hyperpolymath
diff --git a/.github/funding.yml b/.github/funding.yml
new file mode 100644
index 0000000..10176ef
--- /dev/null
+++ b/.github/funding.yml
@@ -0,0 +1,2 @@
+# https://docs.github.com/en/repositories/managing-your-repositorys-custom-fields/displaying-a-sponsor-button-in-your-repository
+github: hyperpolymath
diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md
new file mode 100644
index 0000000..015f1a3
--- /dev/null
+++ b/ARCHITECTURE.md
@@ -0,0 +1,78 @@
+<!--
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+# Architecture
+
+> An earlier unmerged sweep proposed a generic `ARCHITECTURE.md` describing a
+> `src/ tests/ config/` layout with "modular, maintainable architecture designed for
+> clarity, scalability and long-term sustainability". This repository has none of those
+> directories and that text described nothing. What follows is the actual structure.
+
+## Two layers, one repository
+
+```
+GNPL          narration: "what account does this evidence support?"   <-- design only
+  │  lowers to
+GQLdt         query: "what is in the store?"                          <-- built, tested
+  │  FFI (liblith_bridge.a)
+Form.Bridge   Zig, C ABI                                              <-- built, tested
+  │
+Lithoglyph    Form.Model / Form.Blocks (Forth, append-only journal)   <-- separate repo
+```
+
+This is why a repository named `gnpl` contains sources namespaced `GqlDt`: GQLdt is not
+a leftover, it is GNPL's compilation target. See `README.adoc`, and `docs/THEORY.adoc`
+for why the narration layer is the point.
+
+## Layout
+
+| Path | Language | Role |
+|---|---|---|
+| `src/GqlDt/` | Lean 4 | the query core — types, lexer, parser, IR, pipeline |
+| `src/GqlDt/Types/` | Lean 4 | refinement types: `BoundedNat`, `NonEmptyString`, `Confidence` |
+| `src/GqlDt/Provenance/` | Lean 4 | `ActorId`, `Rationale`, `Tracked` — the warrant substrate |
+| `src/GqlDt/Prompt/` | Lean 4 | PROMPT six-dimension source scoring |
+| `src/GQLdt/ABI/` | Idris2 | ABI definitions + memory-layout proofs |
+| `bridge/` | Zig | FFI implementation; emits `zig-out/lib/liblith_bridge.a` |
+| `test/` | Lean 4 | executable suites, run by `lake test` |
+| `spec/` | Markdown/EBNF | the normative grammar and lexical specification |
+| `docs/` | AsciiDoc/Markdown | design rationale and proof debt |
+
+Per the estate standard, **ABI is Idris2 and FFI is Zig** — no hand-written C.
+`bridge/` is the only Zig tree; two pre-0.15-API skeletons were removed in #7.
+
+## Build order (it matters)
+
+`lakefile.lean` links against `bridge/zig-out/lib/liblith_bridge.a`, so the Zig archive
+must exist *before* the Lean executables link:
+
+```sh
+cd bridge && zig build && zig build test   # produces liblith_bridge.a
+cd ..     && lake build && lake test
+```
+
+Getting this backwards is why the `Containerfile` used to mask both steps with
+`|| echo`, which meant a wholly broken build still produced a "successful" image.
+
+## Verification posture
+
+The claims this repository makes about itself are gated, and the gates are tested:
+
+| Gate | What it establishes |
+|---|---|
+| `lake build` | the Lean core typechecks |
+| `lake test` | 163 executable checks across Lexer / Parser / TypeSafety |
+| `scripts/check-lean-proofs.sh --build-log` | Lean reports no *incomplete* proof (`sorry`) |
+| estate `check-trusted-base.sh` | every `axiom` is enumerated in `docs/proof-debt.md` |
+| `cd bridge && zig build test` | the FFI bridge builds and its unit tests pass |
+
+**A green proof gate means "nothing is admitted mid-proof", not "nothing is assumed".**
+Lean's `sorry` warning does not fire on `axiom`, and 16 axioms remain — five of them in
+*executable* position, so those functions have no implementation at all. Read
+`docs/proof-debt.md` before relying on any verification claim here.
+
+New gates are only accepted once they have been shown to go red on a seeded fault. The
+test driver and the proof gate were both canary-tested this way; the repository has a
+history of gates that could not fail, and the remedy is evidence, not intent.
diff --git a/GOVERNANCE.md b/GOVERNANCE.md
new file mode 100644
index 0000000..17f9cc3
--- /dev/null
+++ b/GOVERNANCE.md
@@ -0,0 +1,62 @@
+<!--
+SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+
+# Governance
+
+`hyperpolymath/gnpl` is maintained by @hyperpolymath (see `MAINTAINERS`). Decisions are
+made by the maintainer; this document records *how* they are made and what a change has to
+clear, so the bar is legible rather than tacit.
+
+## Scope of decisions
+
+| Kind | Who decides | Evidence expected |
+|---|---|---|
+| Bug fix, doc correction, gate repair | maintainer or contributor PR | the gate that now fails, or the measurement |
+| Grammar / lexical behaviour | maintainer, against `spec/GQL-DT-*.md` | the spec clause being conformed to |
+| ABI or FFI surface | maintainer | layout proof in `src/GQLdt/ABI/`, both sides updated together |
+| Adding or discharging an `axiom` | maintainer | `docs/proof-debt.md` updated in the same change |
+| Semantics of PROMPT scoring | maintainer | affects a proof field — see below |
+
+## The rules a change must clear
+
+These are not style preferences; each exists because it was violated and cost something.
+
+1. **No handwaving.** A claim in a README, a manifest or a commit message must be
+   verifiable by running something. "Verified" without a command that verifies it is a
+   defect.
+2. **Gates must be able to fail.** A new or repaired gate is not accepted until it has been
+   shown to go red on a deliberately seeded fault, and green when removed. This repository
+   has shipped a naming gate that compared a string to itself, a `lake test` step that
+   swallowed real failures, test suites whose `main : IO Unit` always exited 0, and a
+   container build that masked both its steps with `|| echo`.
+3. **Specs are normative.** Where `spec/GQL-DT-Lexical.md` and the implementation disagree,
+   the implementation is wrong until the spec is deliberately amended.
+4. **The trusted base is enumerated.** Every `axiom` appears in `docs/proof-debt.md` with
+   `file:line` and a disposition. Nothing may be recorded as "budgeted" without a stated
+   refutation budget — untested assurance is unfalsifiable.
+5. **Foundation before depth.** Work that makes the codebase *verifiable* precedes work
+   that deepens any one strand. The 19 lexer defects found in July 2026 were invisible for
+   as long as they were because nothing could run and fail.
+
+## Cross-cutting changes
+
+Two areas cannot be changed on one side only:
+
+- **The FFI boundary.** `bridge/lith_types.zig` and the Lean types must agree. A change to
+  one without the other silently breaks the proofs that cross it.
+- **PROMPT scoring.** `PromptScores` carries a proof field,
+  `overall_correct : overall.val = (…sum…) / 6`. The averaging rule is welded into the
+  type, so changing it is a proof obligation change on every value, in Lean and in Zig
+  simultaneously — not an edit to one function.
+
+## Estate context
+
+This repository consumes shared workflows from `hyperpolymath/standards`. Faults in those
+are reported upstream rather than patched around locally; where a local shim is
+unavoidable it carries a comment naming the upstream issue.
+
+## Contributing
+
+See `CONTRIBUTING.md`. Code is MPL-2.0, documentation is CC-BY-SA-4.0.
diff --git a/MAINTAINERS b/MAINTAINERS
new file mode 100644
index 0000000..9d97072
--- /dev/null
+++ b/MAINTAINERS
@@ -0,0 +1,23 @@
+# Maintainers — hyperpolymath/gnpl
+
+## Active
+
+| Name                    | GitHub          | Role    |
+|-------------------------|-----------------|---------|
+| Jonathan D.A. Jewell    | @hyperpolymath  | Primary |
+
+## Scope
+
+GNPL (the narration/projection layer) and GQLdt (the query layer it lowers to) live in
+this repository together — see `README.adoc`. The Zig FFI bridge under `bridge/` and the
+Idris2 ABI under `src/GQLdt/ABI/` are maintained here too; the Lithoglyph data store they
+talk to is maintained separately.
+
+## Expectations
+
+- Changes touching `src/GqlDt/`, `src/GQLdt/ABI/` or `bridge/` need review — they carry the
+  correctness claims.
+- `docs/proof-debt.md` must be updated in the same change as any axiom added or discharged.
+  The estate trusted-base policy enforces this in CI.
+- Gates must be able to fail. A new gate is not accepted until it has been shown to go red
+  on a seeded fault.

From 62a20270192ab7cb42e0ebac777df063339106d0 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 28 Jul 2026 19:32:50 +0100
Subject: [PATCH 4/4] fix(lake): build the test executables by default
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

CI failed at "Run Lean tests" with the driver reporting the suite binaries
missing — which was correct, and was the same fault this PR exists to close.

`lake build` builds only `@[default_target]`, which was the `GqlDt` library
alone. So the test executables were compiled by nothing: not by CI, not by a
plain local `lake build`. That is exactly why two of the four suites had rotted
to the point of not compiling, and my test driver inherited the problem by
expecting binaries that nothing had produced.

Marking the three pure-Lean suites `@[default_target]` closes the class, rather
than papering over it by adding an explicit build line to the workflow: the
suites can no longer silently stop compiling, because every `lake build`
compiles them.

ffi_test stays non-default — it links liblith_bridge.a, so making it default
would break a clean `lake build` before `cd bridge && zig build` has run.

Verified from a wiped `.lake/build/bin`: plain `lake build` produces
lexer_test, parser_test and type_safety_test; `lake test` then exits 0.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 lakefile.lean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index 95f9c17..bd649dd 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -40,12 +40,19 @@ lean_exe ffi_test where
     "-llith_bridge"
   ]
 
--- Parser test executable
+-- Parser test executable.
+-- The three pure-Lean suites are @[default_target] so a plain `lake build` compiles them.
+-- Without that, `lake build` built only the GqlDt library, the test executables were never
+-- compiled by CI or locally, and two of them silently rotted until they no longer compiled
+-- at all. "Declared but built by nothing" is the failure mode this whole change exists to
+-- close, so the suites must not reintroduce it.
+@[default_target]
 lean_exe parser_test where
   srcDir := "test"
   root := `ParserTest
 
 -- Lexer test executable
+@[default_target]
 lean_exe lexer_test where
   srcDir := "test"
   root := `LexerTest
@@ -53,6 +60,7 @@ lean_exe lexer_test where
 -- Type-safety test executable.
 -- test/TypeSafetyTests.lean existed but was declared by no target, so it was never
 -- built and never run — it could not even fail to compile.
+@[default_target]
 lean_exe type_safety_test where
   srcDir := "test"
   root := `TypeSafetyTests