Skip to content

ARCHITECTURE.adoc

Latest commit

 

History

History
63 lines (53 loc) · 2.96 KB

ARCHITECTURE.adoc

File metadata and controls

63 lines (53 loc) · 2.96 KB
Raw

GNPL architecture

GNPL constructs warranted accounts over evidence under an explicit focalization. The first interpreter uses direct evidence and an imported immutable snapshot. Selection, type validation and storage modules are private machinery; they do not define a second public language or prescribe a lowering target.

Evidence snapshot + .gnpl projection
                |
                v
     GNPL direct-evidence kernel
                |
                v
   Checked account or explicit refusal

The live Lithoglyph adapter and Glyphbase account workflow remain integration work. The contract describes what must cross that boundary.

Layout

Path Role

src/Gnpl/Core.lean

Lean/Std kernel: evidence, focalization, witnesses, ordered accounts, rivalry and withdrawal

src/Gnpl/Surface.lean

Complete projection parser with JSON-escaped strings

src/Gnpl/Json.lean

Versioned evidence import and readable account/refusal output

src/GnplMain.lean

gnpl narrate and gnpl counterfactual CLI

src/GqlDt/

Private legacy namespace: selection, validation, IR, provenance and experimental storage

src/GQLdt/ABI/

Idris2 ABI definitions

bridge/

Separate experimental Zig FFI bridge

test/

Five executable suites plus a default-build narration axiom audit

examples/narration/

Projection examples and an evidence fixture

docs/narration-slice.adoc

Implemented public fragment and trust boundary

spec/

Historical/private-substrate specifications; see its index for scope

.machine_readable/descriptiles/

Canonical descriptive metadata

Per the estate standard, ABI definitions use Idris2 and FFI implementation uses Zig. The new narration kernel does not import the private storage modules and requires no FFI call to construct an account.

Build and verification

lake build builds the default targets, including the narration CLI and audit; lake test runs five suites. Explicit FFI targets require the bridge archive to be built first with cd bridge && zig build && zig build test. FFI testing is a separate boundary and is not established by the narration suite.

The account type carries witnesses for every requested assertion. Lean checks withdrawal exclusion and exact preservation of requested claims and telling order. The audit requires Lean’s transitive axiom report to remain [propext] for narrate and both theorems. An intentionally incorrect audit expectation was rejected in an isolated failure control.

The private substrate retains separate proof assumptions. The incomplete-proof gate checks Lean diagnostics; it does not prove an axiom-free repository. See the executable boundary for current refusals and the narration guide for imported-input assumptions.