// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk = GNPL — a narration/projection language for Lithoglyph :toc: macro :toclevels: 2

image:https://img.shields.io/badge/License-MPL–2.0-blue.svg[License: MPL-2.0,link=“https://www.mozilla.org/en-US/MPL/2.0/”] image:https://img.shields.io/badge/docs-CC–BY–SA–4.0-lightgrey.svg[Docs: CC-BY-SA-4.0,link=“https://creativecommons.org/licenses/by-sa/4.0/”]

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 link:PROOF-PROGRESS.adoc[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?

toc::[]

== 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 link:docs/narration-slice.adoc[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 link:docs/executable-boundary.adoc[the executable boundary] for the actual source-to-IR path, rejection behaviour and remaining proof assumptions.

== Design documents

[cols=“1,3”,options=header] |=== | Document | Question it answers

link:docs/THEORY.adoc[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.

link:docs/LITHOGLYPH.adoc[docs/LITHOGLYPH.adoc]
What does GNPL concretely give Lithoglyph, as a database?

link:docs/STATE-OF-PLAY.adoc[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.

link:docs/proof-debt.adoc[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

[source,console]

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:

[source,console]

$ 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 link:docs/executable-boundary.adoc[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 link:ABI-FFI-README.adoc[ABI-FFI-README.adoc] for the estate-wide ABI (Idris2) / FFI (Zig) standard this repository follows.