refactor: migrate Markdown to AsciiDoc

ABI-FFI-README.adoc

@@ -0,0 +1,127 @@
+== ABI / FFI — how GNPL reaches Lithoglyph
+
+This repository follows the estate standard: *ABI defined in Idris2, FFI
+implemented in Zig*, meeting at the C ABI. No C is written by hand.
+
+____
+*History:* this file was previously the unfilled RSR template — 385
+lines of `+{{project}}+` placeholders documenting an `+ffi/zig/+` tree
+that did not compile. It has been replaced with what the repository
+actually contains.
+____
+
+=== The path
+
+....
+GNPL  ──lowers to──▶  GQLdt (Lean 4)
+                          │
+                          │ FFI: links -Lbridge/zig-out/lib -llith_bridge
+                          ▼
+                      bridge/ (Zig)  ── C ABI ──▶  Lithoglyph Form.Bridge
+....
+
+`+lakefile.lean+` links the Lean executables against
+`+bridge/zig-out/lib/liblith_bridge.a+`. *That archive must exist before
+`+lake build+` runs.*
+
+=== Layout
+
+[width="100%",cols="50%,50%",options="header",]
+|===
+|Path |Role
+|`+src/GQLdt/ABI/Types.idr+` |ABI type definitions
+
+|`+src/GQLdt/ABI/Layout.idr+` |memory-layout proofs
+
+|`+src/GQLdt/ABI/Foreign.idr+` |foreign declarations
+
+|`+bridge/build.zig+` |build script (`+addLibrary+`, Zig ≥ 0.15 API)
+
+|`+bridge/lith_root.zig+` |FFI entry point — the exported C surface
+
+|`+bridge/lith_types.zig+` |C-ABI structs (`+ActorIdC+`, `+RationaleC+`,
+`+ProvenanceC+`, `+TrackedValueC+`, `+ProofBlob+`, `+PromptScoresC+`)
+
+|`+bridge/lith_insert.zig+`, `+bridge/lith_persist.zig+` |insert +
+persistence implementation
+|===
+
+`+bridge/+` is the *only* live Zig tree. Two earlier skeletons
+(`+bridge/zig/+`, `+ffi/zig/+`) were removed — they were written against
+the pre-0.15 Build API (`+addStaticLibrary+`,
+`+std.heap.GeneralPurposeAllocator+`), failed to compile on the pinned
+Zig 0.16.0, and nothing linked against them.
+
+=== Building
+
+[source,bash]
+----
+cd bridge
+zig build                          # produces zig-out/lib/liblith_bridge.a
+zig build test                     # unit tests
+zig build -Doptimize=ReleaseFast   # optimised
+----
+
+Cross-compilation works as usual (`+-Dtarget=aarch64-macos+`, etc.).
+
+Then, from the repository root:
+
+[source,bash]
+----
+lake build
+----
+
+Zig is pinned to *0.16.0* in `+mise.toml+`. Lean is pinned by
+`+lean-toolchain+` (`+leanprover/lean4:v4.15.0+`), which elan reads
+automatically.
+
+=== Exported C surface
+
+Seventeen functions, all `+callconv(.C)+`, from `+bridge/+`:
+
+*Lifecycle* — `+lith_init+`, `+lith_is_init+`, `+lith_close+`,
+`+lith_save+` *Data* — `+lith_insert+`, `+lith_insert_row+`,
+`+lith_delete_row+`, `+lith_table_count+` *PROMPT scores* —
+`+lith_get_scores+`, `+lith_compute_overall+` *Proofs* —
+`+lith_verify_proof+` *Utility* — `+lith_validate_non_empty+`,
+`+lith_timestamp_now+`, `+lith_get_last_error+` *Debug/test* —
+`+lith_debug_init_counter+`, `+lith_debug_magic+`, `+lith_test_fresh+`
+
+Provenance crosses the boundary as real structs, not opaque blobs:
+`+ActorIdC+`, `+RationaleC+`, `+ProvenanceC+` and `+TrackedValueC+` are
+marshalled directly. This is what makes the GNPL narration layer
+buildable over this stack — see `+docs/LITHOGLYPH.adoc+`.
+
+____
+*Caveat.* `+PromptScoresC.computeOverall+` takes an *unweighted mean* of
+the six PROMPT dimensions. It is not probabilistically principled, and
+must not become a load-bearing entrenchment ordering without being
+revisited — see open question 2 in `+docs/THEORY.adoc+`.
+____
+
+=== Why this split
+
+*Idris2 for the ABI* — dependent types let struct size, field alignment
+and cross-version compatibility be _proved_ rather than asserted, so an
+ABI change that would break a caller fails at compile time.
+
+*Zig for the FFI* — `+export fn … callconv(.C)+` is C-compatible without
+a C compiler, without libc, and with cross-compilation built in.
+
+=== Adding a function
+
+[arabic]
+. Declare the type in `+src/GQLdt/ABI/Types.idr+`; add a layout proof in
+`+Layout.idr+`.
+. Declare it in `+src/GQLdt/ABI/Foreign.idr+`.
+. Implement and `+export+` it in `+bridge/+` (match the ABI types
+exactly).
+. `+cd bridge && zig build && zig build test+`, then `+lake build+` from
+the root.
+
+=== Related
+
+* `+docs/THEORY.adoc+` — what GNPL is, and what gap it fills
+* `+docs/LITHOGLYPH.adoc+` — what GNPL gives Lithoglyph as a database
+* `+docs/proof-debt.md+` — the 16 outstanding axioms; *read before
+relying on any verification claim*

ARCHITECTURE.adoc

@@ -0,0 +1,107 @@
+== Architecture
+
+____
+An earlier unmerged sweep proposed a generic `+ARCHITECTURE.md+`
+describing a `+src/ tests/ config/+` layout with "`modular, maintainable
+architecture designed for clarity, scalability and long-term
+sustainability`". This repository has none of those directories and that
+text described nothing. What follows is the actual structure.
+____
+
+=== Two layers, one repository
+
+....
+GNPL          narration: "what account does this evidence support?"   <-- design only
+  │  lowers to
+GQLdt         query: "what is in the store?"                          <-- built, tested
+  │  FFI (liblith_bridge.a)
+Form.Bridge   Zig, C ABI                                              <-- built, tested
+  │
+Lithoglyph    Form.Model / Form.Blocks (Forth, append-only journal)   <-- separate repo
+....
+
+This is why a repository named `+gnpl+` contains sources namespaced
+`+GqlDt+`: GQLdt is not a leftover, it is GNPL’s compilation target. See
+`+README.adoc+`, and `+docs/THEORY.adoc+` for why the narration layer is
+the point.
+
+=== Layout
+
+[width="100%",cols="34%,33%,33%",options="header",]
+|===
+|Path |Language |Role
+|`+src/GqlDt/+` |Lean 4 |the query core — types, lexer, parser, IR,
+pipeline
+
+|`+src/GqlDt/Types/+` |Lean 4 |refinement types: `+BoundedNat+`,
+`+NonEmptyString+`, `+Confidence+`
+
+|`+src/GqlDt/Provenance/+` |Lean 4 |`+ActorId+`, `+Rationale+`,
+`+Tracked+` — the warrant substrate
+
+|`+src/GqlDt/Prompt/+` |Lean 4 |PROMPT six-dimension source scoring
+
+|`+src/GQLdt/ABI/+` |Idris2 |ABI definitions + memory-layout proofs
+
+|`+bridge/+` |Zig |FFI implementation; emits
+`+zig-out/lib/liblith_bridge.a+`
+
+|`+test/+` |Lean 4 |executable suites, run by `+lake test+`
+
+|`+spec/+` |Markdown/EBNF |the normative grammar and lexical
+specification
+
+|`+docs/+` |AsciiDoc/Markdown |design rationale and proof debt
+|===
+
+Per the estate standard, *ABI is Idris2 and FFI is Zig* — no
+hand-written C. `+bridge/+` is the only Zig tree; two pre-0.15-API
+skeletons were removed in #7.
+
+=== Build order (it matters)
+
+`+lakefile.lean+` links against `+bridge/zig-out/lib/liblith_bridge.a+`,
+so the Zig archive must exist _before_ the Lean executables link:
+
+[source,sh]
+----
+cd bridge && zig build && zig build test   # produces liblith_bridge.a
+cd ..     && lake build && lake test
+----
+
+Getting this backwards is why the `+Containerfile+` used to mask both
+steps with `+|| echo+`, which meant a wholly broken build still produced
+a "`successful`" image.
+
+=== Verification posture
+
+The claims this repository makes about itself are gated, and the gates
+are tested:
+
+[width="100%",cols="50%,50%",options="header",]
+|===
+|Gate |What it establishes
+|`+lake build+` |the Lean core typechecks
+
+|`+lake test+` |163 executable checks across Lexer / Parser / TypeSafety
+
+|`+scripts/check-lean-proofs.sh --build-log+` |Lean reports no
+_incomplete_ proof (`+sorry+`)
+
+|estate `+check-trusted-base.sh+` |every `+axiom+` is enumerated in
+`+docs/proof-debt.md+`
+
+|`+cd bridge && zig build test+` |the FFI bridge builds and its unit
+tests pass
+|===
+
+*A green proof gate means "`nothing is admitted mid-proof`", not
+"`nothing is assumed`".* Lean’s `+sorry+` warning does not fire on
+`+axiom+`, and 16 axioms remain — five of them in _executable_ position,
+so those functions have no implementation at all. Read
+`+docs/proof-debt.md+` before relying on any verification claim here.
+
+New gates are only accepted once they have been shown to go red on a
+seeded fault. The test driver and the proof gate were both canary-tested
+this way; the repository has a history of gates that could not fail, and
+the remedy is evidence, not intent.