diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index f3a0556..38e7c9a 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -1,50 +1,116 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# STATE.a2ml — Gql Dt project state +# STATE.a2ml — hyperpolymath/gnpl project state +# +# Rewritten 2026-07-28. The previous revision was stale and partly corrupt: it named the +# project "gql-dt", was dated 2026-02-01, listed already-completed milestones as critical +# next actions, and its `purpose` field held a fragment of a build error rather than a +# purpose. Every figure below is measured, not estimated; see [evidence]. + [metadata] -project = "gql-dt" -version = "0.2.0" -last-updated = "2026-02-01" +project = "gnpl" +version = "0.3.0" +last-updated = "2026-07-28" status = "active" -session = "converted from scheme — 2026-04-11" +session = "proof-debt foundation; PRs #6 #7 #8 merged" [project-context] -name = "Gql Dt" -purpose = """References to removed .tracked and .confidence constructors, missing API updates""" -completion-percentage = 45 +name = "GNPL" +purpose = """ +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?". + +It is built as a layer ON TOP OF GQLdt in this repository and lowers to it: +GNPL (what account) -> GQLdt (what is) -> Zig FFI -> Lithoglyph (the store). +This is why sources are namespaced GqlDt in a repository named gnpl. +""" +completion-percentage = 40 [position] phase = "partial-implementation" # design | implementation | testing | maintenance | archived -maturity = "experimental" # experimental | alpha | beta | production | lts +maturity = "experimental" # experimental | alpha | beta | production | lts + +[layers] +# Two layers, one repo. Nothing is being extracted or discarded. +gqldt = "built and tested — the extensional query core, src/GqlDt/" +gnpl = "design only — docs/THEORY.adoc + docs/LITHOGLYPH.adoc; no src/Gnpl/ yet" + +[verification] +# What is actually established, and by what. A gate that has never gone red is not +# evidence; both gates below were canary-tested in both directions. +lean-build = "pass" # lake build, 34/35 targets +lean-tests = "pass" # lake test, 163 checks, 3 suites +lean-test-count = 163 +lean-test-suites = ["lexer_test", "parser_test", "type_safety_test"] +zig-bridge-build = "pass" # cd bridge && zig build && zig build test +incomplete-proofs = 0 # Lean reports no `sorry` +trusted-base-axioms = 16 # `axiom` does NOT trigger Lean's sorry warning +trusted-base-doc = "docs/proof-debt.md" +gates-canary-tested = true + +[caveat] +# The single most important thing for a machine reading this file to carry forward. +note = """ +A green proof gate here means "nothing is admitted mid-proof". It does NOT mean "nothing +is assumed". Lean 4 emits `declaration uses 'sorry'` for sorry/sorryAx only — `axiom` +produces no warning at all. This repository declares 16 axioms, all stubs, none necessary +in the trusted-base-policy sense. FIVE are in EXECUTABLE position (parseToIR, +deserializeIR, many, many1, sepBy) and therefore have no implementation: code calling them +typechecks and cannot run. So "34/35 targets build" is a claim about TYPECHECKING, not +about a working parser. Read docs/proof-debt.md before relying on any verification claim. +""" [route-to-mvp] milestones = [ - # No milestones recorded + "DONE 2026-07-21 — identity: repo established as GNPL-over-GQLdt; licence restored to MPL-2.0", + "DONE 2026-07-21 — design: docs/THEORY.adoc (the general case) + docs/LITHOGLYPH.adoc (the tethered case)", + "DONE 2026-07-27 — dead code: two pre-0.15-API Zig trees removed; bridge/ is the only one", + "DONE 2026-07-28 — foundation: lake test wired, 163 checks, suites can fail", + "DONE 2026-07-28 — lexer conformance: 19 spec defects fixed (peek off-by-one)", + "NEXT — proof debt D1: delete or prove executePreservesTypes (currently vacuous)", + "NEXT — proof debt D3: construct the six asserted PromptScores examples (gated on averaging decision)", + "THEN — proof debt D2: implement many/many1/sepBy, unblocking four parse* axioms", + "THEN — src/Gnpl/ skeleton: Fabula, Projection, Focalization, Account, Warrant", ] [blockers-and-issues] issues = [ - # No blockers recorded + "DECISION NEEDED — averaging rule for PROMPT scores. PromptScores carries a proof field, overall_correct : overall.val = (sum)/6, so the arithmetic mean is welded into the TYPE. Changing it is a proof-obligation change on every value, in Lean and Zig simultaneously. Gates proof-debt D3.", + "DECISION NEEDED — flake.nix vs guix.scm. Estate policy: Guix primary, Nix fallback, satisfying NEITHER is the violation. This repo has no guix.scm, so flake.nix is the only artefact satisfying it; removing it without a verified guix.scm turns Governance red.", + "UPSTREAM hyperpolymath/standards#516 — Hypatia setup-beam pin cannot map ImageOS=ubuntu24; scanner never runs for any caller. Only red on gnpl main.", + "UPSTREAM hyperpolymath/standards#486 — governance/Allowlist Preflight cannot resolve allowed-actions.json (the file EXISTS; path resolution after sparse-checkout). standards' own main is red on it too.", + "UPSTREAM hyperpolymath/standards#520 — scorecard.yml template violates the estate SARIF policy as distributed.", + "NO test coverage for the FFI boundary — ffi_test is excluded from lake test because it links liblith_bridge.a; it is covered only by the zig-ffi CI job.", ] [critical-next-actions] actions = [ - "Update Dockerfile for Lean 4 + elan", - "Add CI workflow for lake build", - "Start Milestone 5: Zig FFI Bridge", - "Create bridge/lith_types.zig", - "Complete Milestone 5 (Zig FFI)", - "Begin Milestone 6 (GQL Parser)", - "UNIFIED-ROADMAP.scm", - "Dependently-typed query language - critical path item", - "M5: Zig FFI Bridge (blocks Studio M3, real type checking)", - "M6: GQL Parser (blocks full FQLdt compilation)", - "Complete M5 Zig FFI - highest priority", - "Integrate with Lithoglyph's EBNF grammar", - "Proof blob serialization (CBOR RFC 8949)", + "Discharge proof-debt D1: executePreservesTypes reduces to `... -> True` with body commented `-- Placeholder`. It reads as a soundness theorem and discharges nothing. Deleting it is strictly better than keeping a vacuous placeholder.", + "Settle the averaging rule, then discharge D3 once against the final definition.", + "Add a test driver entry for the FFI boundary once liblith_bridge.a can be assumed present.", +] + +[history-landmines] +notes = [ + "The gnpl extract from nextgen-databases was a SQUASH; granular history survives only in the _split_gnpl branch there. Never prune it.", + "Local branches backup/sweeps-mistral-vibe and fix-ci-estate hold three superseded agent-generated sweep commits. Do not replay them: sweep2 is boilerplate mise.toml, sweep3 is an AGPL clobber into an MPL-2.0 repo.", + "Callers pin standards reusables at @main, not a SHA, so upstream permission/interface changes reach this repo instantly and unannounced. This caused two separate estate-wide outages in July 2026.", ] +[evidence] +# Commands a machine or human can run to reproduce every claim above. +build = "lake build" +test = "lake test" +bridge = "cd bridge && zig build && zig build test" +proof-gate = "lake build 2>&1 | tee lake-build.log && ./scripts/check-lean-proofs.sh --build-log lake-build.log" +trusted-base = "bash /scripts/check-trusted-base.sh ." + [maintenance-status] -last-run-utc = "2026-02-01T00:00:00Z" -last-result = "unknown" # unknown | pass | warn | fail +last-run-utc = "2026-07-28T18:45:00Z" +last-result = "pass" # unknown | pass | warn | fail +last-result-detail = "lake build exit 0; lake test exit 0 with 163 checks across 3 suites; verified from a clean checkout of merged main (9de0713)." diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index b82cfa6..5fd7451 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -6,9 +6,9 @@ (manifest (identity - (name "GQL-DT") - (full-name "Dependently-Typed Glyph Query Language") - (version "0.2.0") + (name "GNPL") + (full-name "Glyph Narration & Projection Language") + (version "0.3.0") (repo "https://github.com/hyperpolymath/gnpl") (license "MPL-2.0") (author "Jonathan D.A. Jewell ") @@ -16,23 +16,64 @@ (monorepo-parent "nextgen-databases")) (purpose - "Compile-time verification of database constraints via dependent types. - Lean 4 implementation with Mathlib integration. Provides type-safe - query language for Lithoglyph with proofs of query correctness, - normalization, and constraint satisfaction.") + "Lithoglyph's narration/projection language. 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?' — for forensic histories, counterfactual + paths, plural meanings, and synchronic/diachronic evidence interpretation. + TWO LAYERS, ONE REPO. GNPL is built on top of GQLdt here and lowers to it: + GNPL (what account) -> GQLdt (what is) -> Zig FFI -> Lithoglyph (the store). + This is why every source file is namespaced GqlDt in a repo named gnpl; that + is expected, not a mistake. GQLdt is the dependently-typed query core — Lean 4 + with Mathlib, compile-time verification of database constraints, provenance + tracking and normalization proofs — and it is GNPL's compilation target. + + STATUS: GQLdt builds and is tested (163 checks). GNPL itself is DESIGN ONLY — + docs/THEORY.adoc and docs/LITHOGLYPH.adoc; there is no src/Gnpl/ yet.") + + (caveat-for-agents + "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 + repo declares 16 axioms — five in EXECUTABLE position (parseToIR, deserializeIR, + many, many1, sepBy), which therefore have no implementation at all. Code calling + them typechecks and cannot run. Do not report this repository as 'verified' on the + strength of a green build. See docs/proof-debt.md.") + + ;; Corrected 2026-07-28: all six of the previous entries pointed at files that do not + ;; exist. The .scm state/meta/ecosystem/roadmap files were converted to .a2ml under + ;; .machine_readable/6a2/ and never repointed; there is no AI.a2ml and no justfile. + ;; Every path below was checked to exist at the time of writing. (canonical-locations - (ai-instructions "AI.a2ml") - (state ".machine_readable/STATE.scm") - (meta ".machine_readable/META.scm") - (ecosystem ".machine_readable/ECOSYSTEM.scm") - (roadmap ".machine_readable/ROADMAP.scm") - (build "justfile") + (agent-instructions ".machine_readable/6a2/AGENTIC.a2ml") + (state ".machine_readable/6a2/STATE.a2ml") + (meta ".machine_readable/6a2/META.a2ml") + (ecosystem ".machine_readable/6a2/ECOSYSTEM.a2ml") + (playbook ".machine_readable/6a2/PLAYBOOK.a2ml") + (neurosym ".machine_readable/6a2/NEUROSYM.a2ml") + (roadmap ".machine_readable/ROADMAP.a2ml") + (proof-debt "docs/proof-debt.md") + (design-theory "docs/THEORY.adoc") + (design-application "docs/LITHOGLYPH.adoc") + (architecture "ARCHITECTURE.md") + (governance "GOVERNANCE.md") + (build "lakefile.lean") + (test "lakefile.lean") ;; @[test_driver] script test + (proof-gate "scripts/check-lean-proofs.sh") (container-build "Containerfile") (container-deploy "selur-compose.yml") (spec "spec/") + (ffi-bridge "bridge/") + (abi "src/GQLdt/ABI/") (lean-entry "src/GqlDt.lean")) + ;; Commands that reproduce every claim this manifest makes. + (evidence + (build "lake build") + (test "lake test") ;; 163 checks across 3 suites + (bridge "cd bridge && zig build && zig build test") + (proof-gate "lake build 2>&1 | tee lake-build.log && ./scripts/check-lean-proofs.sh --build-log lake-build.log")) + (tech-stack (primary "Lean 4") (lean-version "v4.15.0") diff --git a/README.adoc b/README.adoc index 91765d7..d89a6af 100644 --- a/README.adoc +++ b/README.adoc @@ -64,6 +64,15 @@ Lithoglyph-as-a-database is the second. See the design documents below. | 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. Machine-readable twin: + `.machine_readable/6a2/STATE.a2ml`. + +| link:docs/proof-debt.md[`docs/proof-debt.md`] +| All 16 outstanding axioms with `file:line` and disposition. **Read before relying on any + verification claim.** |=== == Status diff --git a/docs/STATE-OF-PLAY.adoc b/docs/STATE-OF-PLAY.adoc new file mode 100644 index 0000000..80eaa8c --- /dev/null +++ b/docs/STATE-OF-PLAY.adoc @@ -0,0 +1,155 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += GNPL — state of play +:toc: macro +:toclevels: 2 + +*As at 2026-07-28, `main` = `9de0713`.* The machine-readable counterpart is +`.machine_readable/6a2/STATE.a2ml`; both are regenerated together and should agree. + +This document exists because the repository's own claims about itself were, for a period, +false — a README describing a template, a lexer advertised as supporting operators it could +not lex, and a manifest pointing at six files that did not exist. What follows is written +to be *checkable*: every claim names the command that establishes it. + +toc::[] + +== What this is, in one paragraph + +GNPL is Lithoglyph's *narration/projection* language. 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?". It is built as a layer on top of GQLdt *in this repository* and lowers to it. +That is why every source file is namespaced `GqlDt` in a repo called `gnpl`: GQLdt is not +a leftover, it is the compilation target. + +---- +GNPL ──lowers to──▶ GQLdt ──FFI──▶ Lithoglyph +(what account) (what is) (the data store) +---- + +== Where things actually stand + +[cols="2,1,3",options=header] +|=== +| Component | State | Established by + +| GQLdt core (Lean 4) +| *typechecks* +| `lake build` — 34/35 targets, exit 0 + +| Test suites +| *163 checks, green* +| `lake test` — Lexer, Parser, TypeSafety; exit 0 + +| Zig FFI bridge (`bridge/`) +| *builds, tests pass* +| `cd bridge && zig build && zig build test` — emits `liblith_bridge.a` + +| Incomplete proofs (`sorry`) +| *none* +| `scripts/check-lean-proofs.sh --build-log` + +| Trusted base +| *16 axioms outstanding* +| estate `check-trusted-base.sh`; enumerated in `docs/proof-debt.md` + +| GNPL narration layer +| *design only* +| `docs/THEORY.adoc`, `docs/LITHOGLYPH.adoc`; no `src/Gnpl/` yet +|=== + +=== The caveat that matters most + +[IMPORTANT] +==== +*A green proof gate means "nothing is admitted mid-proof". It does not mean "nothing is +assumed."* + +Lean 4 emits `declaration uses 'sorry'` for `sorry`/`sorryAx` only — **`axiom` produces no +warning at all**. This repository declares *16 axioms*, all stubs, none necessary in the +policy sense. **Five sit in executable position** (`parseToIR`, `deserializeIR`, `many`, +`many1`, `sepBy`) and therefore have *no implementation*: code calling them typechecks and +cannot run. + +So "34/35 targets build" is a statement about **typechecking**, not about a working parser. +Read `docs/proof-debt.md` before relying on any verification claim made here. +==== + +== How to check any of this yourself + +[source,console] +---- +$ lake build # the Lean core typechecks +$ lake test # 163 checks, 3 suites +$ cd bridge && zig build && zig build test # the FFI bridge +$ cd .. && lake build 2>&1 | tee lake-build.log +$ ./scripts/check-lean-proofs.sh --build-log lake-build.log +---- + +Build *order* matters: `lakefile.lean` links `bridge/zig-out/lib/liblith_bridge.a`, so the +Zig archive must exist before the Lean FFI executables link. + +== Gates, and why they are trusted + +Every gate here has been shown to go *red* on a seeded fault and green when it is removed. +That is the standard, because this repository has shipped, and since removed, four gates +that could not fail: + +* a naming check that compared a string to itself, over files that did not exist; +* a `lake test` step whose `|| echo` swallowed genuine failures; +* test suites whose `main : IO Unit` always exited 0 while printing "All tests passed!"; +* a `Containerfile` masking both its build steps with `|| echo`. + +A gate that has never gone red is not evidence of anything. + +== What is known to be missing + +* **No FFI-boundary coverage in `lake test`.** `ffi_test` links `liblith_bridge.a`, so it + is excluded from the driver and covered only by the `zig-ffi` CI job. +* **No property tests.** Nothing in `docs/proof-debt.md` §(b) can cite a refutation budget + yet, so nothing has been promoted there. +* **`src/Gnpl/` does not exist.** The narration layer is specified, not built. + +== Open decisions + +Two questions are recorded here because work is genuinely blocked on them, and guessing +would be worse than waiting. + +*1. The averaging rule for PROMPT scores.* `PromptScores` carries a proof field — +`overall_correct : overall.val = (…sum…) / 6` — so the arithmetic mean is welded into the +*type*. Changing it is a proof-obligation change on every value, in Lean and in Zig +simultaneously, not an edit to one function. An unweighted arithmetic mean also lets a +source with *zero provenance* score 83/100, which is hard to defend for an evidence +database. This gates proof-debt item D3. + +*2. `flake.nix` versus `guix.scm`.* Estate policy is Guix primary, Nix fallback, and +satisfying *neither* is the violation. This repo has no `guix.scm`, so `flake.nix` is the +only artefact satisfying the policy; removing it without a verified replacement turns +Governance red. + +== Sequencing + +Foundation first, breadth before depth — the base layer is whatever makes everything else +*verifiable*. + +. *Done.* Suites can fail; `lake test` runs; gates canary-tested. +. *Next, unblocked:* proof-debt **D1** — `executePreservesTypes` reduces to `… → True` + with its body commented `-- Placeholder`. It reads as a soundness theorem and discharges + nothing. Deleting it is strictly better than keeping it. +. *Next, gated on decision 1:* **D3** — construct the six asserted `PromptScores` examples. + They are the demonstrations of the repo's central claim, and are currently axioms, so + they demonstrate the opposite of what their comments say. +. *Then:* **D2** — implement `many`/`many1`/`sepBy`; the four `parse*` axioms exist only + because these three do. +. *Then:* `src/Gnpl/` — `Fabula`, `Projection`, `Focalization`, `Account`, `Warrant`, + carrying the no-narration-without-warrant constructor discipline. + +== Related + +* `README.adoc` — start here; the two-layer story +* `ARCHITECTURE.md` — layout, build order, verification posture +* `GOVERNANCE.md` — the rules a change must clear, and why each exists +* `docs/proof-debt.md` — all 16 axioms with `file:line` and disposition +* `docs/THEORY.adoc` — what a narration language is, and what gap it fills +* `docs/LITHOGLYPH.adoc` — what GNPL gives Lithoglyph specifically diff --git a/docs/proof-debt.md b/docs/proof-debt.md index b3f1032..4f5993f 100644 --- a/docs/proof-debt.md +++ b/docs/proof-debt.md @@ -45,10 +45,21 @@ GQLdt sources, recorded honestly for the first time. ## (b) Budgeted — tested with refutation budget -- (none — this repo has **no executable test coverage**: `lake test` reports - `no test driver configured`. Nothing here can currently be budgeted, because there is - no refutation budget to cite. Adding a `@[test_driver]` is a prerequisite for moving - any item into this section.) +- (none yet — but the prerequisite is now met.) + +**Updated 2026-07-28.** This section previously read *"this repo has no executable test +coverage: `lake test` reports `no test driver configured` … adding a `@[test_driver]` is a +prerequisite for moving any item into this section."* That prerequisite has been satisfied: +`lake test` now runs three suites and **163 checks**, and the gate is canary-tested in both +directions (a seeded false check turns it red; removing it returns green). + +So items *can* now be moved here — but none has been yet, and none should be moved without +a **stated refutation budget**. Coverage existing is not the same as a given axiom being +covered. The policy's requirement is a citable budget ("property-tested at N inputs by +``, last green on ``"), because without one "covered by tests" is +unfalsifiable — which is the whole reason this section exists. + +The nearest candidate is **D4** (`inferredInsertTypesMatch`); see its entry. ## (c) Necessary axiom @@ -116,11 +127,14 @@ Declared `axiom`, therefore **unimplemented**, not merely unproven: - **Kind**: the one item with a *reasoned* justification in-source — the dynamic schema lookup in `inferInsert` already performs the check, and reconstructing that proof structurally would require reflecting the schema into the type system. - - **Assessment**: plausible, and closest of the 16 to a genuine §(b)/§(c) entry — but it - cannot be promoted to §(b) today because there is no test suite to give it a - refutation budget, and not to §(c) because it *is* derivable in principle. - - **Plan**: promote to §(b) once a test driver exists and this path is property-tested; - or discharge via schema reflection (the source's own "future work"). + - **Assessment**: plausible, and closest of the 16 to a genuine §(b)/§(c) entry. Not + §(c), because it *is* derivable in principle. Not yet §(b) either — but the reason has + changed as of 2026-07-28: a test suite now exists (163 checks), so the blocker is no + longer "no coverage at all", it is that **this specific path is not property-tested** + and has no citable refutation budget. + - **Plan**: property-test `inferInsert` over generated schema/value pairs, then promote + to §(b) quoting the command and the input count; or discharge via schema reflection + (the source's own "future work"). The first is now genuinely reachable. ## (e) Detector false positives — no action