GNPL — a narration/projection language for Lithoglyph

GNPL is Lithoglyph’s narration/projection language: it turns an evidence base into an account — for forensic histories, counterfactual paths, plural meanings, and synchronic/diachronic evidence interpretation.

Where a query language answers "what is true in the store?", GNPL answers "what account does this evidence support, told from whose stance, with what warrant — and what rival accounts does the same evidence also support?"

Table of Contents

• Read this first: why the code says GqlDt
• Design documents
• Status
• Build
  • Proof gate
• Licence
• ABI/FFI standard

Read this first: why the code says GqlDt

This repository is named gnpl, but every source file under src/ is currently namespaced GqlDt. That is expected, not a mistake. GNPL is being built as a layer on top of GQLdt, in this repository.

Layer	What it is	Status
src/GqlDt/	GQLdt — a dependently-typed query language in Lean 4. Extensional: "what is". Already carries the substrate GNPL needs — Provenance/ActorId, Provenance/Rationale, Types/Confidence.	Builds ✅
src/Gnpl/	GNPL — the narration layer. Intensional: "what account". Lowers to GQLdt queries.	Not yet implemented

GNPL  ──lowers to──▶  GQLdt  ──FFI──▶  Lithoglyph
(what account)      (what is)        (the data store)

Nothing in GQLdt is being discarded: it becomes GNPL’s compilation target.

History. This repo was reserved for GNPL, then filled by a squash-import of the GQLdt sources from the nextgen-databases/lithoglyph/ monorepo. The migration registry of the time defined GNPL narrowly, as simply a renamed "Glyph query language". That reading has since been superseded: narration/projection is the primary purpose, and practical value to Lithoglyph-as-a-database is the second. See the design documents below.

Design documents

Document	Question it answers
docs/THEORY.adoc	What is a narration/projection language, and what gap does it fill? Positions GNPL against query languages, bitemporal stores, provenance semirings, argumentation frameworks, belief revision and narratology.
docs/LITHOGLYPH.adoc	What does GNPL concretely give Lithoglyph, as a database?

Status

Component	State	Notes
GQLdt core (Lean 4)	typechecks	lake build completes; 34/35 targets; Lean reports no incomplete proofs — but see the trusted-base caveat below
Proof obligations	16 axioms outstanding	all stubs, none necessary; enumerated in docs/proof-debt.md
Tests	none	lake test reports no test driver configured
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
bridge/zig/, ffi/zig/	stale	skeletons on the pre-0.15 Zig Build API; nothing links against them

Build

# Lean core (first build fetches mathlib — expect a long run)
$ lake build

# Zig FFI bridge — must exist before the Lean FFI executables link
$ cd bridge && zig build && zig build test

Toolchains: Lean is pinned by lean-toolchain (v4.15.0, read automatically by elan); Zig and Idris2 are pinned in mise.toml. Per the estate ABI/FFI standard, ABI definitions are Idris2 (src/GQLdt/ABI/*.idr) and the FFI implementation is Zig (bridge/).

Proof gate

scripts/check-lean-proofs.sh enforces the manifest invariant "No sorry in Lean 4 proofs". Its authoritative mode reads Lean’s own diagnostics:

$ lake build 2>&1 | tee lake-build.log
$ ./scripts/check-lean-proofs.sh --build-log lake-build.log

It deliberately does not use a bare grep -r "sorry\|admit": this repo legitimately contains an admit constructor, a .admit reference, a "sorry" lexer keyword and a commented-out sorry, none of which are incomplete proofs.

Important

A green proof gate here means "nothing is admitted mid-proof". It does not mean "nothing is assumed." Lean’s sorry warning does not fire on axiom, and this repository declares 16 axioms — including five in executable position (parseToIR, deserializeIR, many, many1, sepBy), which therefore have no implementation at all. docs/proof-debt.md enumerates all 16 with file:line, classifies each, and is enforced in CI by the estate trusted-base policy. Read it before relying on any claim of verification here.

Licence

Code is MPL-2.0; documentation (.md, .adoc) is CC-BY-SA-4.0. See LICENSE and LICENSES/.

ABI/FFI standard

See ABI-FFI-README.md for the estate-wide ABI (Idris2) / FFI (Zig) standard this repository follows.