test: make the suites capable of failing — and fix the 19 lexer defects that exposed

.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

.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

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.

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.

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.

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

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)

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
@@ -33,16 +40,62 @@ 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
 
+-- 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
+
+-- 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"

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)

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"