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.

For proof progress summary, see PROOF-PROGRESS.adoc.

GNPL asks: what account does this evidence support, from whose stance, with what warrant, and what rival accounts does the same evidence support?

Table of Contents

• Implementation boundary
• Design documents
• Status
• Build
  • Proof gate
• Licence
• ABI/FFI standard

Implementation boundary

GNPL owns the public semantics. Existing type validation, selection and storage machinery is a private substrate. The historical src/GqlDt/ namespace is a compatibility detail, not a second public language or a fixed lowering contract. The first narration interpreter is implemented in src/Gnpl/: it checks direct evidence, constructs an ordered account under a declared focalization, and re-evaluates that account after a hypothetical source withdrawal.

Start with the runnable narration slice. It uses an imported evidence snapshot; the live Lithoglyph journal adapter, general derivation chains and Glyphbase rendering remain integration work.

See the executable boundary for the actual source-to-IR path, rejection behaviour and remaining proof assumptions.

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?
docs/STATE-OF-PLAY.adoc	Where the project actually stands, what is verified and by which command, what is known missing, and which decisions are open. Descriptive anchors belong under .machine_readable/descriptiles/; historical checkpoints may lag.
docs/proof-debt.adoc	Historical proof-debt inventory; its totals predate the executable-boundary fixes. Check the current source and boundary document before relying on a proof claim.

Status

• lake build succeeds. lake test runs five suites, including 35 narration checks and 26 private-substrate checks alongside the existing suites.

• The narration kernel constructs witnesses for direct-evidence support. It refuses inaccessible, withdrawn, missing or mismatched citations. A limited rival relation preserves conflicting accounts without choosing a winner.

• Lean proves that withdrawn evidence cannot support an assertion and that checked narration preserves the requested claims and their telling order. A default-build audit checks that these proofs and narrate depend only on Lean’s propext axiom, with no project-specific axiom dependency.

• The substrate parses one complete statement, validates inserts against a supplied schema and supports in-memory insertion/retrieval. It rejects unverified proof mode, unchecked mutations, incomplete wire interchange and persistent-execution requests.

• Existing ABI/FFI code is separate from a verified, durable narration pipeline.

• The direct-evidence rule checks traceability and declared admission policy. It does not establish external truth, authenticate source declarations, or settle confidence composition and general narrative inference.

Build

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

$ lake test

# Produce an account with its warrant trail
$ .lake/build/bin/gnpl narrate --evidence examples/narration/evidence.json --projection examples/narration/inspection.gnpl

# 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 means no incomplete proof was reported by that gate. It does not establish an axiom-free trusted base. Parser implementations and insert validation no longer rely on their former executable/typing axioms, but the existing floating-point equality assumption and other module assumptions remain in the private substrate. The independent narration kernel has the narrower audited footprint described above. See the current boundary before interpreting older proof-debt totals or completion percentages.

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.adoc for the estate-wide ABI (Idris2) / FFI (Zig) standard this repository follows.