This is not the repository README. It documents one of two layers.
This repo is GNPL, a narration/projection language — see README.adoc, which is what GitHub renders on the landing page. GNPL answers "`what account does this evidence support, from whose stance, with what warrant`". It is being built on top of GQLdt and lowers to it:
GNPL ──lowers to──▶ GQLdt ──FFI──▶ Lithoglyph (what account) (what is) (the data store)The document below describes GQLdt only — the extensional query core under
src/GqlDt/, which is why the sources are namespacedGqlDtin a repo namedgnpl. Nothing here is being discarded; GQLdt becomes GNPL’s compilation target. Design rationale: docs/THEORY.adoc and docs/LITHOGLYPH.adoc.
GQLdt extends Lithoglyph’s query language with dependent types, enabling compile-time verification of database constraints, provenance tracking, and reversibility proofs.
Note: GQL stands for “Lithoglyph Query Language”—the native query interface for Lithoglyph. It is not related to HTML forms or form builders.
┌─────────────────────────────────────────────────────────────┐
│ GQL (Factor) │ GQLdt (Lean 4) │
│ - Runtime constraint checks │ - Compile-time proofs │
│ - Dynamic, practical │ - Static, verified │
│ - "Just run it" │ - "Prove it first" │
└───────────────┬────────────────┴────────────────┬───────────┘
│ │
▼ ▼
┌─────────────────────────────────────────────────────────────┐
│ Form.Bridge (Zig) - Bidirectional ABI │
│ - No C dependency │
│ - callconv(.C) for FFI compatibility │
├─────────────────────────────────────────────────────────────┤
│ Form.Model + Form.Blocks (Forth) │
│ - Single source of truth │
└─────────────────────────────────────────────────────────────┘
Same database, different guarantees:
| Aspect | GQL (practical) | GQLdt (verified) |
|---|---|---|
When constraints checked |
Runtime |
Compile-time |
Invalid insert |
Runtime error |
Won’t compile |
Reversibility |
Runtime inverse stored |
Proof that inverse exists |
PROMPT scores |
|
|
Provenance |
Application enforces |
Type system enforces |
-
Refinement Types:
BoundedNat 0 100,NonEmptyString,Confidence -
Dependent Types: Length-indexed vectors, provenance-tracked values
-
Proof Obligations: Compile-time verification of constraints
-
Reversibility Proofs: Prove operations have inverses before execution
-
Normalization Types: Type-encoded functional dependencies, normal form predicates (1NF-BCNF), proof-carrying schema evolution
-
Backward Compatible: Standard GQL is valid in dependent-type mode
Build Status: 34/35 modules compiling (97% success) - Updated 2026-02-01
Completed Milestones: - ✅ M1: Lean 4 project setup (v4.15.0
Mathlib) - ✅ M2: Core refinement types (BoundedNat, BoundedInt,
NonEmptyString, Confidence) - ✅ M3: PROMPT score types
(PromptDimension, PromptScores with auto-computed overall) - ✅ M4:
Provenance tracking (ActorId, Rationale, Tracked with proofs) - ✅ M5:
Specifications (EBNF grammar, lexical spec, railroad diagrams) - 🟡 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) —
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) - ✅ Serialization: CBOR encoding/decoding (RFC
8949), JSON support - ✅ Documentation: 8 comprehensive docs (seam
analysis, integration, language bindings, etc.) - ✅ Infrastructure:
Containerfile, Dockerfile, CI/CD workflow -
Recent Updates (2026-02-01): - Seam analysis: Fixed 76 issues, resolved 33 compilation blockers - Namespace consistency: Global GqlDt → GqlDt renaming across 24 files - Circular dependency: Created Serialization/Types.lean to break IR ↔ Serialization cycle - CBOR tags: Updated to vendor-specific range (55800-55804) to avoid IANA collisions - Lexer rewrite: Complete hand-rolled implementation (Parsec unavailable in Lean 4.15.0)
Next Steps: - Fix AST.lean nested inductive issue (TypedValue/Tracked relationship) - Achieve 35/35 modules compiling (100% build success) - Start M7 (Idris2 ABI) + M8 (Zig FFI) in parallel - M9: ReScript bindings (HIGHEST PRIORITY after M7+M8)
For detailed progress tracking, see .machine_readable/STATE.scm.
GQLdt compiles to operations on Form.Bridge, which uses Zig’s stable ABI:
/// Bidirectional FFI: Lean 4 → Zig → Forth core
/// and Forth core → Zig → Lean 4 callbacks
pub const LithStatus = struct {
code: i32,
error_blob: ?[*]const u8,
error_len: usize,
};
/// Forward: GQLdt → Form.Bridge
pub export fn lith_insert(
db: *LithDb,
collection: [*:0]const u8,
document: [*]const u8,
doc_len: usize,
proof_blob: [*]const u8, // Serialised proof from Lean 4
proof_len: usize,
) callconv(.C) LithStatus;
/// Reverse: Form.Bridge → GQLdt (for constraint checking)
pub export fn lith_register_constraint_checker(
db: *LithDb,
checker: *const fn (doc: [*]const u8, len: usize) callconv(.C) bool,
) callconv(.C) LithStatus;No C headers or libc required. Zig provides C-compatible calling convention for interop.
See spec/GQL_Dependent_Types_Complete_Specification.md for the full specification covering:
-
Type System (universes, primitives, constructors)
-
Refinement Types (bounded values, non-empty strings)
-
Dependent Types (provenance tracking, reversibility)
-
DDL/DML with proofs
-
Proof obligations and tactics
-
Complete examples (BoFIG journalism use case)
See spec/normalization-types.md for normalization types covering:
-
Functional dependency encoding (FunDep, Armstrong’s Axioms)
-
Normal form predicates (1NF, 2NF, 3NF, BCNF, 4NF)
-
Proof-carrying schema evolution (NormalizationStep)
-
Integration with Form.Normalizer
-
GQL syntax extensions for normalization commands
-
Ensure
justandpodmanare installed -
Run
just checkto verify Lean 4 proofs -
For non-bash shells, see
scripts/bootstrap_all.sh
-
Phase 1 (Month 1-6): Refinement types
-
Phase 2 (Month 7-12): Simple dependent types
-
Phase 3 (Month 13-18): Full verification
-
Phase 4 (Month 19-24): Normalization types (FunDep, normal forms, proof-carrying evolution)
-
-
The narrative-first database
-
-
Lithoglyph Self-Normalizing Spec - Self-normalizing database specification
-
Glyphbase - Lithoglyph web UI (Airtable-mode delivery)
-
lithoglyphdb - Reserved future home of the database (extraction pending)
-
BoFIG - Evidence graph for investigative journalism
-
-
Production pilot: reference manager with PROMPT scores
-
-
Lithoglyph Studio - Zero-friction GUI for GQLdt (planned; not yet published)
-
Lithoglyph Debugger - Proof-carrying database debugger, Lean 4 + Idris 2 (planned; not yet published)
-
FormBase - Open-source Airtable alternative with provenance