From 248357d81eb7b872c7d8b6e47fa2280b93667bea Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 24 Aug 2026 08:24:14 +0100 Subject: [PATCH] refactor: migrate repository documentation from Markdown to AsciiDoc --- ASSUMPTIONS.adoc | 144 +++++++++++ ASSUMPTIONS.md | 87 ------- CHANGELOG.adoc | 9 + CHANGELOG.md | 15 -- CODE_OF_CONDUCT.adoc | 24 ++ CODE_OF_CONDUCT.md | 30 --- CONTRIBUTING.adoc | 9 + CONTRIBUTING.md | 12 - PROOF-NARRATIVE.adoc | 305 ++++++++++++++++++++++ PROOF-NARRATIVE.md | 316 ----------------------- PROOF-NEEDS.adoc | 112 ++++++++ PROOF-NEEDS.md | 83 ------ PROOF-STATUS.adoc | 127 +++++++++ PROOF-STATUS.md | 96 ------- READINESS.adoc | 144 +++++++++++ READINESS.md | 123 --------- README.adoc | 167 ++++++++++++ README.md | 126 --------- REQUIRES_INITIALISATION.adoc | 153 +++++++++++ REQUIRES_INITIALISATION.md | 144 ----------- SECURITY.adoc | 16 ++ SECURITY.md | 23 -- TEST-NEEDS.adoc | 126 +++++++++ TEST-NEEDS.md | 88 ------- TOPOLOGY.adoc | 108 ++++++++ TOPOLOGY.md | 89 ------- docs/tech-debt-2026-05-26.adoc | 83 ++++++ docs/tech-debt-2026-05-26.md | 72 ------ examples/README.adoc | 28 +- examples/README.md | 22 -- llm-warmup-dev.adoc | 19 ++ llm-warmup-dev.md | 20 -- llm-warmup-user.adoc | 19 ++ llm-warmup-user.md | 20 -- openlearn/README.adoc | 92 +++++++ openlearn/README.md | 85 ------ openlearn/modules/00-why-resolution.adoc | 34 +++ openlearn/modules/00-why-resolution.md | 35 --- openlearn/references/bibliography.adoc | 42 +++ openlearn/references/bibliography.md | 44 ---- playground/README.adoc | 45 ++++ playground/README.md | 45 ---- spec/grammar-overview.adoc | 112 ++++++++ spec/grammar-overview.md | 99 ------- 44 files changed, 1915 insertions(+), 1677 deletions(-) create mode 100644 ASSUMPTIONS.adoc delete mode 100644 ASSUMPTIONS.md create mode 100644 CHANGELOG.adoc delete mode 100644 CHANGELOG.md create mode 100644 CODE_OF_CONDUCT.adoc delete mode 100644 CODE_OF_CONDUCT.md create mode 100644 CONTRIBUTING.adoc delete mode 100644 CONTRIBUTING.md create mode 100644 PROOF-NARRATIVE.adoc delete mode 100644 PROOF-NARRATIVE.md create mode 100644 PROOF-NEEDS.adoc delete mode 100644 PROOF-NEEDS.md create mode 100644 PROOF-STATUS.adoc delete mode 100644 PROOF-STATUS.md create mode 100644 READINESS.adoc delete mode 100644 READINESS.md create mode 100644 README.adoc delete mode 100644 README.md create mode 100644 REQUIRES_INITIALISATION.adoc delete mode 100644 REQUIRES_INITIALISATION.md create mode 100644 SECURITY.adoc delete mode 100644 SECURITY.md create mode 100644 TEST-NEEDS.adoc delete mode 100644 TEST-NEEDS.md create mode 100644 TOPOLOGY.adoc delete mode 100644 TOPOLOGY.md create mode 100644 docs/tech-debt-2026-05-26.adoc delete mode 100644 docs/tech-debt-2026-05-26.md delete mode 100644 examples/README.md create mode 100644 llm-warmup-dev.adoc delete mode 100644 llm-warmup-dev.md create mode 100644 llm-warmup-user.adoc delete mode 100644 llm-warmup-user.md create mode 100644 openlearn/README.adoc delete mode 100644 openlearn/README.md create mode 100644 openlearn/modules/00-why-resolution.adoc delete mode 100644 openlearn/modules/00-why-resolution.md create mode 100644 openlearn/references/bibliography.adoc delete mode 100644 openlearn/references/bibliography.md create mode 100644 playground/README.adoc delete mode 100644 playground/README.md create mode 100644 spec/grammar-overview.adoc delete mode 100644 spec/grammar-overview.md diff --git a/ASSUMPTIONS.adoc b/ASSUMPTIONS.adoc new file mode 100644 index 0000000..b1106ec --- /dev/null +++ b/ASSUMPTIONS.adoc @@ -0,0 +1,144 @@ +== Assumptions Registry — KRL + +Every load-bearing *unproven* assumption used in this repo, with an ID, +classification, and the obligation it supports. + +Classifications: - *MATH* — true by an external mathematical theorem +(cite it) - *DESIGN* — true by construction in our code (must remain +true; flag if you change the named code) - *EMPIRICAL* — believed from +testing; not formally verified - *CRYPTO* — standard +cryptographic-primitive assumption + +Cross-references use `+[[A-KR-N.M]]+` syntax, resolved here. + +''''' + +[width="100%",cols="10%,12%,14%,19%,17%,28%",options="header",] +|=== +|ID |Class |Status |Statement |Cited by |Where it lives +|A-KR-1.1 |DESIGN |*UNANCHORED* |Every `+KRLExpr+` AST variant has a +matching arm in the lowering pass |KR-1 |was +`+KRLAdapter.jl/src/parser/lower.jl+` — gone; no lowering pass exists +anywhere + +|A-KR-1.2 |DESIGN |*UNANCHORED* |The AST module defines the only AST +shapes the parser produces |KR-1 |was +`+KRLAdapter.jl/src/parser/ast.jl+` — gone. +`+quandledb/server/krl/Ast.jl+` exists but encodes a _different_ +language (see below) + +|A-KR-2.1 |DESIGN |*UNANCHORED* |Generator arity is fixed: +`+sigma i / sigma_inv i : in=i+1, out=i+1+`; `+cup i : in=0, out=2+`; +`+cap i : in=2, out=0+` |KR-2 |`+spec/grammar.ebnf+` only. No +implementation defines these generators — `+sigma+`, `+cup+` and `+cap+` +appear 0 times in `+quandledb/server/krl/+` + +|A-KR-2.2 |MATH |holds |`+arity_in(a \| b) = arity_in(a) + arity_in(b)+` +and same for output (monoidal-category tensor) |KR-2 |Standard +categorical tangle definition + +|A-KR-3.1 |MATH |holds |Reidemeister’s theorem: R1+R2+R3 generate +isotopy equivalence on tangle diagrams |KR-3 |Reidemeister 1927; +Kauffman _Knots and Physics_ ch. 1 + +|A-KR-3.2 |DESIGN |*UNANCHORED* |`+r1_simplify+` / `+r2_simplify+` / +`+r3_simplify+` implement those moves faithfully |KR-3 |was +`+KRLAdapter.jl/src/operations.jl+` — gone. No Reidemeister +simplification exists in `+quandledb/server/krl/+` + +|A-KR-4.1 |DESIGN |*UNANCHORED* |The pretty-printer’s bracketing is +unambiguous: `+;+` only inside parens; tensor `+\|+` has lower +precedence than compose `+;+` inside parens |KR-4 |No pretty-printer +exists in any current implementation + +|A-KR-6.1 |DESIGN |*VOID* |Two independent parsers both target +`+spec/grammar.ebnf+` v0.1.0 |KR-6 |Only one parser now exists +(`+quandledb/server/krl/Parser.jl+`), and it targets +`+quandledb/spec/grammar.ebnf+`, not this one + +|A-KR-6.2 |DESIGN |*VOID* |Both implementations share the same `+Token+` +enumeration |KR-6 |Only one lexer now exists +(`+quandledb/server/krl/Lexer.jl+`); there is nothing to share with + +|A-KR-8.1 |MATH (partial) |holds |Fundamental-quandle functor is +faithful on prime alternating knots; partial in general |KR-8 |Joyce +1982; for partial cases see Eisermann _The number of knot group +representations_ + +|A-KR-8.2 |MATH |holds |Two non-isomorphic quandles have distinct +canonical presentations (true by definition of "`canonical`") |KR-8 +|Standard algebraic-presentation result +|=== + +=== On the UNANCHORED and VOID rows + +A DESIGN assumption is defined above as _"`true by construction in our +code (must remain true; flag if you change the named code)`"_. Seven +rows named code in `+KRLAdapter.jl+`, which no longer exists, so there +is no construction left to be true by. They are recorded here rather +than deleted, because the statements are still the design intent — but +none of them is currently checkable, and none may be cited as +discharged. + +*UNANCHORED* means the statement stands as intent but names no live +code. *VOID* means the statement presupposes two implementations, and +only one exists. + +Re-anchoring is blocked on the specification itself. +`+spec/grammar.ebnf+` (here) and `+quandledb/spec/grammar.ebnf+` are +disjoint on core vocabulary: the braid generators these assumptions +describe appear only in the former, and only the latter is implemented. +Until the two are reconciled and a conformance suite exists, these rows +cannot be re-anchored to anything. See `+READINESS.md+`. + +''''' + +=== How to use this file + +* *Reading code.* When you see a function whose correctness depends on +something not enforced by the local types — _that’s an assumption_. Find +or add the entry here and reference it by ID. +* *Writing a proof.* Every proof obligation in PROOF-NARRATIVE.md names +its assumptions by ID. Before discharging the proof, audit the +assumptions. +* *Modifying load-bearing code.* Each DESIGN assumption names a file. If +you edit that file, re-validate the assumption (or update the obligation +if you changed the design intentionally). + +=== Promoting / demoting assumptions + +[width="100%",cols="30%,25%,45%",options="header",] +|=== +|From |To |Trigger +|EMPIRICAL → MATH |discharge with a citation | + +|EMPIRICAL → DESIGN |refactor to make it a structural invariant | + +|MATH → (delete) |obligation it supports has been re-cast not to need it +| + +|DESIGN → MATH (rare) |the design happens to encode a known theorem | + +|any → CRYPTO |only for cryptographic primitives (BLAKE3, SHA-256, etc.) +| +|=== + +When you change a row, leave a one-line note at the bottom of this file +with the date and reason. + +''''' + +=== Changelog + +[width="100%",cols="32%,42%,26%",options="header",] +|=== +|Date |Change |By +|2026-06-01 |Initial registry, scoped to KRL surface obligations |Audit + +|2026-07-21 |Added Status column. Marked A-KR-1.1, 1.2, 2.1, 3.2 and 4.1 +UNANCHORED and A-KR-6.1, 6.2 VOID: all seven named code in +`+KRLAdapter.jl+`, which no longer exists. Verified that no replacement +exists — `+sigma+`, `+cup+`, `+cap+`, `+r1_simplify+` and any +pretty-printer appear 0 times in `+quandledb/server/krl/+`. The four +MATH rows are unaffected. |Audit +|=== diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md deleted file mode 100644 index 5d59a80..0000000 --- a/ASSUMPTIONS.md +++ /dev/null @@ -1,87 +0,0 @@ - -# Assumptions Registry — KRL - -Every load-bearing **unproven** assumption used in this repo, with an -ID, classification, and the obligation it supports. - -Classifications: -- **MATH** — true by an external mathematical theorem (cite it) -- **DESIGN** — true by construction in our code (must remain true; flag if you change the named code) -- **EMPIRICAL** — believed from testing; not formally verified -- **CRYPTO** — standard cryptographic-primitive assumption - -Cross-references use `[[A-KR-N.M]]` syntax, resolved here. - ---- - -| ID | Class | Status | Statement | Cited by | Where it lives | -|----|-------|--------|-----------|----------|----------------| -| A-KR-1.1 | DESIGN | **UNANCHORED** | Every `KRLExpr` AST variant has a matching arm in the lowering pass | KR-1 | was `KRLAdapter.jl/src/parser/lower.jl` — gone; no lowering pass exists anywhere | -| A-KR-1.2 | DESIGN | **UNANCHORED** | The AST module defines the only AST shapes the parser produces | KR-1 | was `KRLAdapter.jl/src/parser/ast.jl` — gone. `quandledb/server/krl/Ast.jl` exists but encodes a *different* language (see below) | -| A-KR-2.1 | DESIGN | **UNANCHORED** | Generator arity is fixed: `sigma i / sigma_inv i : in=i+1, out=i+1`; `cup i : in=0, out=2`; `cap i : in=2, out=0` | KR-2 | `spec/grammar.ebnf` only. No implementation defines these generators — `sigma`, `cup` and `cap` appear 0 times in `quandledb/server/krl/` | -| A-KR-2.2 | MATH | holds | `arity_in(a \| b) = arity_in(a) + arity_in(b)` and same for output (monoidal-category tensor) | KR-2 | Standard categorical tangle definition | -| A-KR-3.1 | MATH | holds | Reidemeister's theorem: R1+R2+R3 generate isotopy equivalence on tangle diagrams | KR-3 | Reidemeister 1927; Kauffman _Knots and Physics_ ch. 1 | -| A-KR-3.2 | DESIGN | **UNANCHORED** | `r1_simplify` / `r2_simplify` / `r3_simplify` implement those moves faithfully | KR-3 | was `KRLAdapter.jl/src/operations.jl` — gone. No Reidemeister simplification exists in `quandledb/server/krl/` | -| A-KR-4.1 | DESIGN | **UNANCHORED** | The pretty-printer's bracketing is unambiguous: `;` only inside parens; tensor `\|` has lower precedence than compose `;` inside parens | KR-4 | No pretty-printer exists in any current implementation | -| A-KR-6.1 | DESIGN | **VOID** | Two independent parsers both target `spec/grammar.ebnf` v0.1.0 | KR-6 | Only one parser now exists (`quandledb/server/krl/Parser.jl`), and it targets `quandledb/spec/grammar.ebnf`, not this one | -| A-KR-6.2 | DESIGN | **VOID** | Both implementations share the same `Token` enumeration | KR-6 | Only one lexer now exists (`quandledb/server/krl/Lexer.jl`); there is nothing to share with | -| A-KR-8.1 | MATH (partial) | holds | Fundamental-quandle functor is faithful on prime alternating knots; partial in general | KR-8 | Joyce 1982; for partial cases see Eisermann _The number of knot group representations_ | -| A-KR-8.2 | MATH | holds | Two non-isomorphic quandles have distinct canonical presentations (true by definition of "canonical") | KR-8 | Standard algebraic-presentation result | - -### On the UNANCHORED and VOID rows - -A DESIGN assumption is defined above as *"true by construction in our code -(must remain true; flag if you change the named code)"*. Seven rows named code -in `KRLAdapter.jl`, which no longer exists, so there is no construction left to -be true by. They are recorded here rather than deleted, because the statements -are still the design intent — but none of them is currently checkable, and none -may be cited as discharged. - -**UNANCHORED** means the statement stands as intent but names no live code. -**VOID** means the statement presupposes two implementations, and only one -exists. - -Re-anchoring is blocked on the specification itself. `spec/grammar.ebnf` (here) -and `quandledb/spec/grammar.ebnf` are disjoint on core vocabulary: the braid -generators these assumptions describe appear only in the former, and only the -latter is implemented. Until the two are reconciled and a conformance suite -exists, these rows cannot be re-anchored to anything. See `READINESS.md`. - ---- - -## How to use this file - -- **Reading code.** When you see a function whose correctness depends - on something not enforced by the local types — _that's an - assumption_. Find or add the entry here and reference it by ID. -- **Writing a proof.** Every proof obligation in - [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md) names its assumptions by - ID. Before discharging the proof, audit the assumptions. -- **Modifying load-bearing code.** Each DESIGN assumption names a - file. If you edit that file, re-validate the assumption (or update - the obligation if you changed the design intentionally). - -## Promoting / demoting assumptions - -| From | To | Trigger | -|------|-----|---------| -| EMPIRICAL → MATH | discharge with a citation | -| EMPIRICAL → DESIGN | refactor to make it a structural invariant | -| MATH → (delete) | obligation it supports has been re-cast not to need it | -| DESIGN → MATH (rare) | the design happens to encode a known theorem | -| any → CRYPTO | only for cryptographic primitives (BLAKE3, SHA-256, etc.) | - -When you change a row, leave a one-line note at the bottom of this -file with the date and reason. - ---- - -## Changelog - -| Date | Change | By | -|------|--------|-----| -| 2026-06-01 | Initial registry, scoped to KRL surface obligations | Audit | -| 2026-07-21 | Added Status column. Marked A-KR-1.1, 1.2, 2.1, 3.2 and 4.1 UNANCHORED and A-KR-6.1, 6.2 VOID: all seven named code in `KRLAdapter.jl`, which no longer exists. Verified that no replacement exists — `sigma`, `cup`, `cap`, `r1_simplify` and any pretty-printer appear 0 times in `quandledb/server/krl/`. The four MATH rows are unaffected. | Audit | diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..ca1c652 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,9 @@ +== Changelog + +All notable changes to this project will be documented in this file. + +The format is based on https://keepachangelog.com/en/1.1.0/[Keep a +Changelog], and this project adheres to +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. + +=== [Unreleased] diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index ec7f2e1..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,15 +0,0 @@ - -# Changelog - -All notable changes to this project will be documented in this file. - -The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), -and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - - - - -## [Unreleased] diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd2a83c --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,24 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We pledge to make participation a harassment-free experience for +everyone. + +=== Our Standards + +*Positive behavior:* * Using welcoming language * Being respectful of +differing viewpoints * Accepting constructive criticism * Focusing on +what is best for the community + +*Unacceptable behavior:* * Harassment, trolling, or personal attacks * +Publishing private information without permission + +=== Enforcement + +Report issues to the maintainers. All complaints will be reviewed. + +=== Attribution + +Adapted from https://www.contributor-covenant.org/[Contributor Covenant] +v2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index bbe9219..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,30 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..5949bf0 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,9 @@ +== Contributing + +[arabic] +. Fork the repository +. Create a feature branch +. Ensure SPDX headers on all files +. Submit a pull request + +*Author:* Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index b7e3340..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,12 +0,0 @@ - -# Contributing - -1. Fork the repository -2. Create a feature branch -3. Ensure SPDX headers on all files -4. Submit a pull request - -**Author:** Jonathan D.A. Jewell diff --git a/PROOF-NARRATIVE.adoc b/PROOF-NARRATIVE.adoc new file mode 100644 index 0000000..d194055 --- /dev/null +++ b/PROOF-NARRATIVE.adoc @@ -0,0 +1,305 @@ +== Proof Narrative — KRL + +This file is the *single coherent story* of what KRL proves, what it +assumes, and what it has left to prove. It is the document a reader +should open first when asking _"`is this language sound, and how do I +know?`"_. + +For the per-obligation status checklist, see PROOF-NEEDS.md. For the +registry of every load-bearing unproven assumption, see ASSUMPTIONS.md. + +''''' + +=== 1. Position in the stack + +KRL is the *surface language* of a four-layer federated stack. It is +_not_ a standalone implementation; the canonical implementations live in +sibling repos: + +.... +┌─────────────────────────────────────────────────────────┐ +│ KRL surface language (this repo) │ +│ • spec/grammar.ebnf (v0.1.0) │ +│ • Idris2 ABI types (src/interface/Abi/) │ +│ • Zig FFI scaffold (src/interface/ffi/) │ +│ • examples (examples/) │ +└─────────────────┬───────────────────────────────────────┘ + │ implements + ▼ +┌─────────────────────────────────────────────────────────┐ +│ KRLAdapter.jl — canonical parser / lower │ +│ quandledb/server/krl/ — server-side query parser │ +└─────────────────┬───────────────────────────────────────┘ + │ lowers to + ▼ +┌─────────────────────────────────────────────────────────┐ +│ TangleIR — canonical interchange object │ +└─────────────────┬───────────────────────────────────────┘ + │ semantics on + ▼ +┌─────────────────────────────────────────────────────────┐ +│ Tangle (hyperpolymath/tangle) — proven core │ +│ Progress · Preservation · Determinism · Type Safety │ +└─────────────────┬───────────────────────────────────────┘ + │ persisted+queried via + ▼ +┌─────────────────────────────────────────────────────────┐ +│ Skein.jl + QuandleDB — storage + semantic index │ +└─────────────────────────────────────────────────────────┘ +.... + +Consequence: *this repo’s proof obligations are spec-level, not +implementation-level*. We owe a precise definition of what a KRL program +_is_, plus refinement-style obligations against the two parser +implementations. + +=== 2. Proven now + +[cols=",,,",options="header",] +|=== +|ID |Statement |Form |Where +|— |_none yet at the KRL surface level_ |— |— +|=== + +The Idris2 / Lean / Coq files previously sitting under +`+verification/proofs/+` were rsr-template-repo boilerplate (generic +`+Bounded+`, `+ApiResult+`, typed-arithmetic `+TypeSafety+`). They +asserted nothing about KRL. They have been deleted in the same PR as +this narrative to avoid the "`looks proven, isn’t`" failure mode. Their +content is recoverable from the PR description if anyone wants the +template back. + +*The actually-proven results that the KRL stack benefits from live in +`+hyperpolymath/tangle/proofs/Tangle.lean+`* (16 theorems and lemmas +including Progress, Preservation, Determinism, and Type Safety for the +core Tangle calculus that KRL lowers into). See the tangle repo’s +`+PROOF-NARRATIVE.md+` for details. Until KRL has its own surface +proofs, the soundness story rests on (a) the Tangle core proofs and (b) +the _unproven_ claim that KRL faithfully lowers into that core. That +claim is `+KR-1+` and `+KR-2+` below. + +=== 3. Obligations (the narrative arc) + +The arc from "`KRL text`" to "`trusted query result`": + +.... +KRL source text + │ [KR-7] parser rejects ill-typed concrete syntax + ▼ +KRLProgram AST + │ [KR-1] lowering is total on parseable programs + │ [KR-2] lowering preserves port arity + ▼ +TangleIR + │ [hyperpolymath/tangle: T-Progress, T-Preservation, T-Determinism] + ▼ +Tangle value + │ [KR-3] simplify is semantics-preserving + │ [KR-8] equivalent? is sound w.r.t. fundamental-quandle iso + ▼ +Query result +.... + +Each obligation in detail: + +==== KR-1 — Lowering is total on parseable programs + +*Claim.* For every `+KRLProgram p+` produced by `+parse_krl+`, the +function `+lower(p)+` returns a `+TangleIR+` (never raises +`+KRLLowerError+`). + +*Why valuable.* A `+KRLLowerError+` at runtime means the parser accepted +a program that the lowering rejected — a soundness regression that the +lexer/parser/AST should have prevented. Closing this proves +parser-and-lowering agree on the language. + +*Status.* Unproven. Currently `+KRLLowerError+` is raised from +`+KRLAdapter.jl/src/parser/lower.jl+` on (a) unbound identifiers and (b) +un-matched AST variants. Case (a) is correct (it’s a real user error); +case (b) is the soundness gap. + +*Assumptions (load-bearing for this claim).* - [[A-KR-1.1]] Every +`+KRLExpr+` AST variant has a matching arm in `+lower.jl+`. - +[[A-KR-1.2]] The AST defined in `+KRLAdapter.jl/src/parser/ast.jl+` is +the _only_ AST shape the parser can produce. + +*How to discharge.* Add an exhaustiveness check to the lowering function +(compile-time in Julia is weak; consider a property-based test +enumerating every constructor as a stop-gap, with Idris2 as the target +prover for the long term). + +==== KR-2 — Lowering preserves port arity + +*Claim.* If `+p : KRLProgram+` lowers to `+ir : TangleIR+`, then for +every sub-expression `+(compose a b)+` in `+p+`, the number of output +ports of `+lower(a)+` equals the number of input ports of `+lower(b)+`. + +*Why valuable.* Composition is the central operation. Without this, you +can write KRL that lowers to ill-formed TangleIR — e.g. composing a +2-strand braid with a 3-strand tangle — and the error surfaces +downstream as garbled invariant computation, not as a clear "`your +program is wrong`" message. + +*Status.* Unproven, and the typechecker that would enforce this at parse +time is *not yet implemented* (acknowledged in `+READINESS.md+` under +"`Path to C`"). + +*Assumptions.* - [[A-KR-2.1]] Generators have known fixed arity: +`+sigma i : in=i, out=i+1+` (and same arity in/out), +`+cup i : in=0, out=2+`, `+cap i : in=2, out=0+`. - [[A-KR-2.2]] +Tensor and compose distribute over arity in the obvious way: +`+arity_in(a | b) = arity_in(a) + arity_in(b)+`. + +*How to discharge.* Implement port-arity checking in the typechecker; +prove the typechecker sound against this property. + +==== KR-3 — `+simplify+` is semantics-preserving + +*Claim.* For every `+e : KRLExpr+` and its simplified form +`+e' = simplify(e)+`, the lowered TangleIR objects `+lower(e)+` and +`+lower(e')+` represent the same tangle up to isotopy. + +*Why valuable.* This is the _retrieval guarantee_: queries against the +simplified form must return the same answer as queries against the +original. Without it, simplification is a performance trick that can +change semantics. + +*Status.* Unproven; `+simplify+` is partially implemented in +KRLAdapter.jl (R2 detection works inside a single sigma sequence but not +across `+compose+` boundaries — see `+READINESS.md+`). + +*Assumptions.* - [[A-KR-3.1]] R1, R2, R3 are the complete set of local +moves needed to relate isotopic tangles (Reidemeister’s theorem; +mathematically established). - [[A-KR-3.2]] `+r1_simplify+`, +`+r2_simplify+`, `+r3_simplify+` (when implemented; R3 is currently a +gap — see `+quandledb/PROOF-NARRATIVE.md+` QD-2) faithfully implement +those moves. + +*How to discharge.* Prove each rewrite preserves the fundamental quandle +presentation (which encodes isotopy). + +==== KR-4 — Pretty-print/parse round-trip + +*Claim.* For every `+e : KRLExpr+` produced by `+parse_krl+`, +`+parse_krl(pretty(e)) = e+`. + +*Why valuable.* A free fuzz oracle. Catches a whole class of "`lossy +IR`" bugs at the parse boundary. Also the foundation of the +`+reconstruct_source+` claim in `+README.adoc+`. + +*Status.* Unproven; `+pretty+` exists in KRLAdapter.jl but no round-trip +test. + +*Assumptions.* - [[A-KR-4.1]] The pretty-printer’s choice of bracketing +is unambiguous w.r.t. the grammar (e.g. `+;+` only inside parens at the +expression level — see `+READINESS.md+`). + +*How to discharge.* Add a property test in `+KRLAdapter.jl/test/+` that +round-trips every well-formed program from `+examples/+`. + +==== KR-5 — Idris2/Zig ABI primitives are load-bearing + +*Claim.* `+SafePtr+`, `+Handle+`, `+Bounded+`, `+NonEmpty+` (currently +in `+src/interface/Abi/+` and `+verification/proofs/idris2/+`) must +either be *referenced by the actual Zig FFI surface* or be deleted. + +*Why valuable.* Right now they’re floating. They were rsr-template +content; they have non-trivial dependent-type structure but no consumer. + +*Status.* Decision pending. Recommended decision: keep `+SafePtr+` and +`+Handle+`, wire them through the FFI; delete `+Bounded+` and +`+NonEmpty+` as unused. + +==== KR-6 — Two-parser equivalence + +*Claim.* For every input string `+s+`, `+KRLAdapter.jl::parse_krl(s)+` +and `+quandledb/server/krl/Parser.jl::parse_any(s)+` either both succeed +with equal ASTs or both fail. + +*Why valuable.* The two implementations exist by design — one for +end-user code, one for query-time parsing — but if they accept different +languages, the server can run queries the user can’t write, and vice +versa. + +*Status.* Unproven; no differential test exists. + +*Assumptions.* - [[A-KR-6.1]] Both implementations target the same EBNF +grammar (`+spec/grammar.ebnf+` v0.1.0). - [[A-KR-6.2]] Both +implementations have the same notion of "`valid identifier`", "`valid +integer literal`", "`valid string literal`". + +*How to discharge.* Build a differential fuzz harness that feeds random +strings to both and asserts result equivalence. Easy single PR. + +==== KR-7 — Generator-index validity + +*Claim.* `+sigma N+`, `+sigma_inv N+`, `+cup N+`, `+cap N+` are accepted +iff `+N ≥ 1+`. + +*Why valuable.* Small but catches a real class of off-by-one bugs; also +a parser-level invariant that should be asserted explicitly. + +*Status.* Currently encoded in the existing parser-error case ("`zero +index`" rejected). Not asserted as a property test. + +==== KR-8 — `+equivalent?+` is sound w.r.t. quandle isomorphism + +*Claim.* If `+equivalent?(a, b)+` returns `+true+`, then the fundamental +quandles of `+a+` and `+b+` are isomorphic. + +*Why valuable.* This is the central claim of the retrieval layer. False +positives mean the database lies; without this, `+equivalent?+` is +heuristic, not semantic. + +*Status.* Unproven; implementation in QuandleDB. Soundness rests on +[[A-KR-8.1]] and the fingerprint determinism claim +`+quandledb/PROOF-NARRATIVE.md+` QD-4. + +*Assumptions.* - [[A-KR-8.1]] Fundamental-quandle functor is _faithful_ +on isotopy classes (true for prime alternating knots; partial in general +— this needs to be a stated and bounded assumption). - [[A-KR-8.2]] +Fingerprint collisions are mathematically impossible for non-isomorphic +quandles (this is a property of the canonicalisation, not the hash). + +*How to discharge.* Either: - Restrict the claim to the +prime-alternating subset (where the functor is provably faithful), or - +State the obligation as "`equivalence is sound modulo the +fundamental-quandle relation`", which is weaker but provable. + +=== 4. The "`stupid proof`" exclusions + +For completeness, things we deliberately do *not* prove: + +* _"``+KRLProgram+` is a record with these fields`"_ — enforced by the +Julia type system; no proof needed. +* _"``+parse_krl+` returns a `+KRLProgram+``"_ — Julia type assertion. +* _"`Compose is associative when types agree`"_ — implied by list-append +associativity. +* _"`BLAKE3 is collision-resistant`"_ — out of scope; cryptographic +primitive assumption inherited from QuandleDB. + +If you find yourself drafting a proof in one of these categories, delete +the draft. + +=== 5. How to add a new obligation + +[arabic] +. Add an entry to PROOF-NEEDS.md with an ID (`+KR-N+`), category, +prover, priority, effort estimate. +. Add the narrative entry here: statement, _why valuable_, status, +*assumptions*, how to discharge. The assumptions block is non-optional. +. For each new assumption, add an entry to ASSUMPTIONS.md with an ID +(`+A-KR-N.M+`) and a note on whether it is _mathematical_ (true by +external theorem), _design_ (true by our construction), or _empirical_ +(believed, not verified). + +=== 6. References + +* Architecture: README.adoc, section "`Architecture position`". +* Companion narratives: +** `+hyperpolymath/tangle/PROOF-NARRATIVE.md+` — semantic core proofs +** `+hyperpolymath/quandledb/PROOF-NARRATIVE.md+` — quandle / DB proofs +* Implementations: +** `+KRLAdapter.jl+` — canonical parser, AST, lower +** `+quandledb/server/krl/+` — server-side query parser +* Spec: spec/grammar.ebnf, spec/grammar-overview.md. diff --git a/PROOF-NARRATIVE.md b/PROOF-NARRATIVE.md deleted file mode 100644 index 2919b29..0000000 --- a/PROOF-NARRATIVE.md +++ /dev/null @@ -1,316 +0,0 @@ - -# Proof Narrative — KRL - -This file is the **single coherent story** of what KRL proves, what it -assumes, and what it has left to prove. It is the document a reader -should open first when asking _"is this language sound, and how do I -know?"_. - -For the per-obligation status checklist, see [PROOF-NEEDS.md](PROOF-NEEDS.md). -For the registry of every load-bearing unproven assumption, see -[ASSUMPTIONS.md](ASSUMPTIONS.md). - ---- - -## 1. Position in the stack - -KRL is the **surface language** of a four-layer federated stack. It is -*not* a standalone implementation; the canonical implementations live -in sibling repos: - -``` -┌─────────────────────────────────────────────────────────┐ -│ KRL surface language (this repo) │ -│ • spec/grammar.ebnf (v0.1.0) │ -│ • Idris2 ABI types (src/interface/Abi/) │ -│ • Zig FFI scaffold (src/interface/ffi/) │ -│ • examples (examples/) │ -└─────────────────┬───────────────────────────────────────┘ - │ implements - ▼ -┌─────────────────────────────────────────────────────────┐ -│ KRLAdapter.jl — canonical parser / lower │ -│ quandledb/server/krl/ — server-side query parser │ -└─────────────────┬───────────────────────────────────────┘ - │ lowers to - ▼ -┌─────────────────────────────────────────────────────────┐ -│ TangleIR — canonical interchange object │ -└─────────────────┬───────────────────────────────────────┘ - │ semantics on - ▼ -┌─────────────────────────────────────────────────────────┐ -│ Tangle (hyperpolymath/tangle) — proven core │ -│ Progress · Preservation · Determinism · Type Safety │ -└─────────────────┬───────────────────────────────────────┘ - │ persisted+queried via - ▼ -┌─────────────────────────────────────────────────────────┐ -│ Skein.jl + QuandleDB — storage + semantic index │ -└─────────────────────────────────────────────────────────┘ -``` - -Consequence: **this repo's proof obligations are spec-level, not -implementation-level**. We owe a precise definition of what a KRL -program *is*, plus refinement-style obligations against the two -parser implementations. - -## 2. Proven now - -| ID | Statement | Form | Where | -|----|-----------|------|-------| -| — | _none yet at the KRL surface level_ | — | — | - -The Idris2 / Lean / Coq files previously sitting under -`verification/proofs/` were rsr-template-repo boilerplate (generic -`Bounded`, `ApiResult`, typed-arithmetic `TypeSafety`). They asserted -nothing about KRL. They have been deleted in the same PR as this -narrative to avoid the "looks proven, isn't" failure mode. Their -content is recoverable from the PR description if anyone wants the -template back. - -**The actually-proven results that the KRL stack benefits from live -in `hyperpolymath/tangle/proofs/Tangle.lean`** (16 theorems and -lemmas including Progress, Preservation, Determinism, and Type Safety -for the core Tangle calculus that KRL lowers into). See the tangle -repo's `PROOF-NARRATIVE.md` for details. Until KRL has its own surface -proofs, the soundness story rests on (a) the Tangle core proofs and -(b) the *unproven* claim that KRL faithfully lowers into that core. -That claim is `KR-1` and `KR-2` below. - -## 3. Obligations (the narrative arc) - -The arc from "KRL text" to "trusted query result": - -``` -KRL source text - │ [KR-7] parser rejects ill-typed concrete syntax - ▼ -KRLProgram AST - │ [KR-1] lowering is total on parseable programs - │ [KR-2] lowering preserves port arity - ▼ -TangleIR - │ [hyperpolymath/tangle: T-Progress, T-Preservation, T-Determinism] - ▼ -Tangle value - │ [KR-3] simplify is semantics-preserving - │ [KR-8] equivalent? is sound w.r.t. fundamental-quandle iso - ▼ -Query result -``` - -Each obligation in detail: - -### KR-1 — Lowering is total on parseable programs - -**Claim.** For every `KRLProgram p` produced by `parse_krl`, the -function `lower(p)` returns a `TangleIR` (never raises `KRLLowerError`). - -**Why valuable.** A `KRLLowerError` at runtime means the parser -accepted a program that the lowering rejected — a soundness regression -that the lexer/parser/AST should have prevented. Closing this proves -parser-and-lowering agree on the language. - -**Status.** Unproven. Currently `KRLLowerError` is raised from -`KRLAdapter.jl/src/parser/lower.jl` on (a) unbound identifiers and -(b) un-matched AST variants. Case (a) is correct (it's a real user -error); case (b) is the soundness gap. - -**Assumptions (load-bearing for this claim).** -- [[A-KR-1.1]] Every `KRLExpr` AST variant has a matching arm in `lower.jl`. -- [[A-KR-1.2]] The AST defined in `KRLAdapter.jl/src/parser/ast.jl` is - the *only* AST shape the parser can produce. - -**How to discharge.** Add an exhaustiveness check to the lowering -function (compile-time in Julia is weak; consider a property-based -test enumerating every constructor as a stop-gap, with Idris2 as the -target prover for the long term). - -### KR-2 — Lowering preserves port arity - -**Claim.** If `p : KRLProgram` lowers to `ir : TangleIR`, then for -every sub-expression `(compose a b)` in `p`, the number of output -ports of `lower(a)` equals the number of input ports of `lower(b)`. - -**Why valuable.** Composition is the central operation. Without this, -you can write KRL that lowers to ill-formed TangleIR — e.g. composing -a 2-strand braid with a 3-strand tangle — and the error surfaces -downstream as garbled invariant computation, not as a clear "your -program is wrong" message. - -**Status.** Unproven, and the typechecker that would enforce this at -parse time is **not yet implemented** (acknowledged in `READINESS.md` -under "Path to C"). - -**Assumptions.** -- [[A-KR-2.1]] Generators have known fixed arity: - `sigma i : in=i, out=i+1` (and same arity in/out), `cup i : in=0, - out=2`, `cap i : in=2, out=0`. -- [[A-KR-2.2]] Tensor and compose distribute over arity in the obvious - way: `arity_in(a | b) = arity_in(a) + arity_in(b)`. - -**How to discharge.** Implement port-arity checking in the -typechecker; prove the typechecker sound against this property. - -### KR-3 — `simplify` is semantics-preserving - -**Claim.** For every `e : KRLExpr` and its simplified form -`e' = simplify(e)`, the lowered TangleIR objects `lower(e)` and -`lower(e')` represent the same tangle up to isotopy. - -**Why valuable.** This is the *retrieval guarantee*: queries against -the simplified form must return the same answer as queries against -the original. Without it, simplification is a performance trick that -can change semantics. - -**Status.** Unproven; `simplify` is partially implemented in -KRLAdapter.jl (R2 detection works inside a single sigma sequence but -not across `compose` boundaries — see `READINESS.md`). - -**Assumptions.** -- [[A-KR-3.1]] R1, R2, R3 are the complete set of local moves needed - to relate isotopic tangles (Reidemeister's theorem; mathematically - established). -- [[A-KR-3.2]] `r1_simplify`, `r2_simplify`, `r3_simplify` (when - implemented; R3 is currently a gap — see - `quandledb/PROOF-NARRATIVE.md` QD-2) faithfully implement those moves. - -**How to discharge.** Prove each rewrite preserves the fundamental -quandle presentation (which encodes isotopy). - -### KR-4 — Pretty-print/parse round-trip - -**Claim.** For every `e : KRLExpr` produced by `parse_krl`, -`parse_krl(pretty(e)) = e`. - -**Why valuable.** A free fuzz oracle. Catches a whole class of "lossy -IR" bugs at the parse boundary. Also the foundation of the -`reconstruct_source` claim in `README.adoc`. - -**Status.** Unproven; `pretty` exists in KRLAdapter.jl but no -round-trip test. - -**Assumptions.** -- [[A-KR-4.1]] The pretty-printer's choice of bracketing is - unambiguous w.r.t. the grammar (e.g. `;` only inside parens at the - expression level — see `READINESS.md`). - -**How to discharge.** Add a property test in `KRLAdapter.jl/test/` -that round-trips every well-formed program from `examples/`. - -### KR-5 — Idris2/Zig ABI primitives are load-bearing - -**Claim.** `SafePtr`, `Handle`, `Bounded`, `NonEmpty` (currently in -`src/interface/Abi/` and `verification/proofs/idris2/`) must either be -**referenced by the actual Zig FFI surface** or be deleted. - -**Why valuable.** Right now they're floating. They were rsr-template -content; they have non-trivial dependent-type structure but no -consumer. - -**Status.** Decision pending. Recommended decision: keep `SafePtr` and -`Handle`, wire them through the FFI; delete `Bounded` and `NonEmpty` -as unused. - -### KR-6 — Two-parser equivalence - -**Claim.** For every input string `s`, `KRLAdapter.jl::parse_krl(s)` -and `quandledb/server/krl/Parser.jl::parse_any(s)` either both -succeed with equal ASTs or both fail. - -**Why valuable.** The two implementations exist by design — one for -end-user code, one for query-time parsing — but if they accept -different languages, the server can run queries the user can't write, -and vice versa. - -**Status.** Unproven; no differential test exists. - -**Assumptions.** -- [[A-KR-6.1]] Both implementations target the same EBNF grammar - (`spec/grammar.ebnf` v0.1.0). -- [[A-KR-6.2]] Both implementations have the same notion of "valid - identifier", "valid integer literal", "valid string literal". - -**How to discharge.** Build a differential fuzz harness that feeds -random strings to both and asserts result equivalence. Easy single PR. - -### KR-7 — Generator-index validity - -**Claim.** `sigma N`, `sigma_inv N`, `cup N`, `cap N` are accepted iff -`N ≥ 1`. - -**Why valuable.** Small but catches a real class of off-by-one bugs; -also a parser-level invariant that should be asserted explicitly. - -**Status.** Currently encoded in the existing parser-error case -("zero index" rejected). Not asserted as a property test. - -### KR-8 — `equivalent?` is sound w.r.t. quandle isomorphism - -**Claim.** If `equivalent?(a, b)` returns `true`, then the fundamental -quandles of `a` and `b` are isomorphic. - -**Why valuable.** This is the central claim of the retrieval layer. -False positives mean the database lies; without this, `equivalent?` is -heuristic, not semantic. - -**Status.** Unproven; implementation in QuandleDB. Soundness rests on -[[A-KR-8.1]] and the fingerprint determinism claim -`quandledb/PROOF-NARRATIVE.md` QD-4. - -**Assumptions.** -- [[A-KR-8.1]] Fundamental-quandle functor is *faithful* on isotopy - classes (true for prime alternating knots; partial in general — this - needs to be a stated and bounded assumption). -- [[A-KR-8.2]] Fingerprint collisions are mathematically impossible - for non-isomorphic quandles (this is a property of the - canonicalisation, not the hash). - -**How to discharge.** Either: -- Restrict the claim to the prime-alternating subset (where the - functor is provably faithful), or -- State the obligation as "equivalence is sound modulo the - fundamental-quandle relation", which is weaker but provable. - -## 4. The "stupid proof" exclusions - -For completeness, things we deliberately do **not** prove: - -- _"`KRLProgram` is a record with these fields"_ — enforced by the - Julia type system; no proof needed. -- _"`parse_krl` returns a `KRLProgram`"_ — Julia type assertion. -- _"Compose is associative when types agree"_ — implied by list-append - associativity. -- _"BLAKE3 is collision-resistant"_ — out of scope; cryptographic - primitive assumption inherited from QuandleDB. - -If you find yourself drafting a proof in one of these categories, -delete the draft. - -## 5. How to add a new obligation - -1. Add an entry to [PROOF-NEEDS.md](PROOF-NEEDS.md) with an ID - (`KR-N`), category, prover, priority, effort estimate. -2. Add the narrative entry here: statement, _why valuable_, - status, **assumptions**, how to discharge. The assumptions block - is non-optional. -3. For each new assumption, add an entry to - [ASSUMPTIONS.md](ASSUMPTIONS.md) with an ID (`A-KR-N.M`) and a - note on whether it is _mathematical_ (true by external theorem), - _design_ (true by our construction), or _empirical_ (believed, - not verified). - -## 6. References - -- Architecture: [README.adoc](README.adoc), section "Architecture position". -- Companion narratives: - - `hyperpolymath/tangle/PROOF-NARRATIVE.md` — semantic core proofs - - `hyperpolymath/quandledb/PROOF-NARRATIVE.md` — quandle / DB proofs -- Implementations: - - `KRLAdapter.jl` — canonical parser, AST, lower - - `quandledb/server/krl/` — server-side query parser -- Spec: [spec/grammar.ebnf](spec/grammar.ebnf), [spec/grammar-overview.md](spec/grammar-overview.md). diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..2367ee2 --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,112 @@ +== Proof Requirements — KRL + +____ +The single coherent story is PROOF-NARRATIVE.md. The assumption registry +is ASSUMPTIONS.md. This file is the *per-obligation checklist* with +status, prover, priority. +____ + +=== Proof Tier + +*Tier:* T2 — High. KRL is the surface language of a federated stack +whose correctness claims (semantic-equivalence queries, +isotopy-respecting retrieval) rest on KRL→TangleIR lowering being +trustworthy. The semantic core (TangleIR/Tangle) is already partially +proven; KRL’s job is to guarantee faithful lowering. + +=== Proof categories + +[width="100%",cols="24%,36%,40%",options="header",] +|=== +|Code |Meaning |Applies? +|*TP* |Typing proofs (port-arity, lowering totality) |Yes + +|*INV* |Invariant proofs (round-trip, grammar refinement) |Yes + +|*SEC* |Security proofs |No + +|*CONC* |Concurrency proofs |No + +|*ALG* |Algorithm proofs (simplification correctness) |Yes + +|*ABI* |ABI/FFI proofs (Zig FFI boundary, Idris2 layout) |Yes (low +priority) + +|*DOM* |Domain proofs (quandle equivalence soundness) |Yes +|=== + +=== Obligations + +[width="100%",cols="9%,18%,17%,13%,17%,13%,13%",options="header",] +|=== +|# |Statement |Category |Prover |Priority |Effort |Status +|KR-1 |`+lower+` is total on parseable programs |TP |Idris2 + Julia +property test |P1 |1d |NOT STARTED + +|KR-2 |`+lower+` preserves port arity |TP |Idris2 + typechecker impl |P1 +|3d |NOT STARTED (typechecker not implemented) + +|KR-3 |`+simplify+` is semantics-preserving (KR-3a: R1; KR-3b: R2; +KR-3c: R3) |ALG |Lean4 or property test against quandle iso |P1 |5d +|PARTIAL (R2 across compose() is gap) + +|KR-4 |Pretty/parse round-trip: `+parse(pretty(e)) = e+` |INV |Julia +property test (cheap) |P1 |4h |NOT STARTED + +|KR-5 |Idris2 `+SafePtr+` / `+Handle+` are load-bearing in the Zig FFI +surface |ABI |Decision + wiring |P3 |2h |DECISION PENDING + +|KR-6 |`+KRLAdapter.jl::parse_krl+` ≡ +`+quandledb/server/krl::parse_any+` on the v0.1.0 grammar |INV +|Differential property test |P1 |4h |NOT STARTED + +|KR-7 |`+sigma N+`, `+cup N+`, etc. accepted iff `+N ≥ 1+` |INV |Grammar +smoke test extension |P2 |1h |PARTIAL (error path exists, not +property-tested) + +|KR-8 |`+equivalent?+` is sound w.r.t. fundamental-quandle isomorphism +|DOM |Lean4 (factored through QuandleDB’s QD-3) |P1 |5d |NOT STARTED +|=== + +For full statements, _why valuable_, and the assumptions each obligation +rests on, see PROOF-NARRATIVE.md. For the assumptions themselves, see +ASSUMPTIONS.md. + +=== Dangerous patterns (BANNED) + +CI rejects any PR introducing any of these: + +[cols=",,",options="header",] +|=== +|Pattern |Language |Meaning +|`+believe_me+` |Idris2 |Unsafe cast +|`+assert_total+` |Idris2 |Skip totality check +|`+postulate+` |Idris2 / Agda |Unproven axiom +|`+sorry+` |Lean4 |Incomplete proof +|`+Admitted+` |Coq |Incomplete proof +|`+unsafeCoerce+` |Haskell |Unsafe cast +|`+Obj.magic+` |OCaml / ReScript |Unsafe cast +|`+unsafe+` (unaudited) |Rust |Unsafe block without safety comment +|=== + +Enforced by `+panic-attack assail --proofs-only+`. + +=== Where proofs go + +.... +verification/proofs/ +├── idris2/ — ABI / type-level invariants (KR-1, KR-2, KR-5) +├── lean4/ — Semantic claims (KR-3, KR-8) +└── julia/ — Property tests against KRLAdapter.jl (KR-4, KR-6, KR-7) +.... + +(The previous `+coq/+` directory has been removed; obligations have been +re-allocated to Lean4 where the Tangle metatheory lives.) + +=== References + +* Companion narratives: `+hyperpolymath/tangle/PROOF-NARRATIVE.md+` +(semantic core), `+hyperpolymath/quandledb/PROOF-NARRATIVE.md+` (quandle +/ DB). +* Implementations under proof: `+KRLAdapter.jl+`, +`+quandledb/server/krl/+`. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index 78cc1c7..0000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,83 +0,0 @@ - -# Proof Requirements — KRL - -> The single coherent story is [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). -> The assumption registry is [ASSUMPTIONS.md](ASSUMPTIONS.md). -> This file is the **per-obligation checklist** with status, prover, priority. - -## Proof Tier - -**Tier:** T2 — High. -KRL is the surface language of a federated stack whose correctness -claims (semantic-equivalence queries, isotopy-respecting retrieval) -rest on KRL→TangleIR lowering being trustworthy. The semantic core -(TangleIR/Tangle) is already partially proven; KRL's job is to -guarantee faithful lowering. - -## Proof categories - -| Code | Meaning | Applies? | -|------|---------|----------| -| **TP** | Typing proofs (port-arity, lowering totality) | Yes | -| **INV** | Invariant proofs (round-trip, grammar refinement) | Yes | -| **SEC** | Security proofs | No | -| **CONC** | Concurrency proofs | No | -| **ALG** | Algorithm proofs (simplification correctness) | Yes | -| **ABI** | ABI/FFI proofs (Zig FFI boundary, Idris2 layout) | Yes (low priority) | -| **DOM** | Domain proofs (quandle equivalence soundness) | Yes | - -## Obligations - -| # | Statement | Category | Prover | Priority | Effort | Status | -|---|-----------|----------|--------|----------|--------|--------| -| KR-1 | `lower` is total on parseable programs | TP | Idris2 + Julia property test | P1 | 1d | NOT STARTED | -| KR-2 | `lower` preserves port arity | TP | Idris2 + typechecker impl | P1 | 3d | NOT STARTED (typechecker not implemented) | -| KR-3 | `simplify` is semantics-preserving (KR-3a: R1; KR-3b: R2; KR-3c: R3) | ALG | Lean4 or property test against quandle iso | P1 | 5d | PARTIAL (R2 across compose() is gap) | -| KR-4 | Pretty/parse round-trip: `parse(pretty(e)) = e` | INV | Julia property test (cheap) | P1 | 4h | NOT STARTED | -| KR-5 | Idris2 `SafePtr` / `Handle` are load-bearing in the Zig FFI surface | ABI | Decision + wiring | P3 | 2h | DECISION PENDING | -| KR-6 | `KRLAdapter.jl::parse_krl` ≡ `quandledb/server/krl::parse_any` on the v0.1.0 grammar | INV | Differential property test | P1 | 4h | NOT STARTED | -| KR-7 | `sigma N`, `cup N`, etc. accepted iff `N ≥ 1` | INV | Grammar smoke test extension | P2 | 1h | PARTIAL (error path exists, not property-tested) | -| KR-8 | `equivalent?` is sound w.r.t. fundamental-quandle isomorphism | DOM | Lean4 (factored through QuandleDB's QD-3) | P1 | 5d | NOT STARTED | - -For full statements, _why valuable_, and the assumptions each -obligation rests on, see [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). -For the assumptions themselves, see [ASSUMPTIONS.md](ASSUMPTIONS.md). - -## Dangerous patterns (BANNED) - -CI rejects any PR introducing any of these: - -| Pattern | Language | Meaning | -|---------|----------|---------| -| `believe_me` | Idris2 | Unsafe cast | -| `assert_total` | Idris2 | Skip totality check | -| `postulate` | Idris2 / Agda | Unproven axiom | -| `sorry` | Lean4 | Incomplete proof | -| `Admitted` | Coq | Incomplete proof | -| `unsafeCoerce` | Haskell | Unsafe cast | -| `Obj.magic` | OCaml / ReScript | Unsafe cast | -| `unsafe` (unaudited) | Rust | Unsafe block without safety comment | - -Enforced by `panic-attack assail --proofs-only`. - -## Where proofs go - -``` -verification/proofs/ -├── idris2/ — ABI / type-level invariants (KR-1, KR-2, KR-5) -├── lean4/ — Semantic claims (KR-3, KR-8) -└── julia/ — Property tests against KRLAdapter.jl (KR-4, KR-6, KR-7) -``` - -(The previous `coq/` directory has been removed; obligations have -been re-allocated to Lean4 where the Tangle metatheory lives.) - -## References - -- Companion narratives: - `hyperpolymath/tangle/PROOF-NARRATIVE.md` (semantic core), - `hyperpolymath/quandledb/PROOF-NARRATIVE.md` (quandle / DB). -- Implementations under proof: `KRLAdapter.jl`, `quandledb/server/krl/`. diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc new file mode 100644 index 0000000..0efb019 --- /dev/null +++ b/PROOF-STATUS.adoc @@ -0,0 +1,127 @@ +== Proof Status — KRL + +____ +Requirements: PROOF-NEEDS.md. Single coherent story: PROOF-NARRATIVE.md. +Assumption registry: ASSUMPTIONS.md. +____ + +This file tracks the per-obligation status. Updated 2026-06-01. + +=== Summary + +[width="99%",cols="18%,10%,8%,19%,13%,13%,19%",options="header",] +|=== +|Category |Total |Done |In Progress |Partial |Blocked |Not Started +|Typing (TP) |2 |0 |0 |0 |0 |2 +|Invariant (INV) |3 |0 |0 |1 |0 |2 +|Algorithm (ALG) |1 |0 |0 |1 |0 |0 +|ABI (ABI) |1 |0 |0 |0 |0 |1 (decision pending) +|Domain (DOM) |1 |0 |0 |0 |0 |1 +|*Total* |*8* |*0* |*0* |*2* |*0* |*6* +|=== + +*Overall:* 0% proven, 25% partial. + +The partial entries (`+KR-3+` simplification across compose() and +`+KR-7+` generator index validity) have implementations or smoke +coverage but no property test or formal proof. + +=== Proofs done + +[cols=",,,,,",options="header",] +|=== +|ID |Proof |Prover |File |Date |Verified by +|— |none yet at the KRL surface level |— |— |— |— +|=== + +The Tangle core proofs (Progress, Preservation, Determinism, Type Safety ++ 12 lemmas, 16 results total) in +`+hyperpolymath/tangle/proofs/Tangle.lean+` are foundational for KRL +because KRL lowers into Tangle. They are tracked in tangle’s +PROOF-STATUS, not here. + +=== Proofs in progress + +[cols=",,,,,",options="header",] +|=== +|ID |Proof |Prover |Assignee |Started |Blocker +|— |— |— |— |— |— +|=== + +=== Proofs partial + +[width="100%",cols="17%,29%,25%,29%",options="header",] +|=== +|ID |Proof |Form |Notes +|KR-3 |`+simplify+` semantics-preserving |Property test in +`+KRLAdapter.jl/test/+` |R1 + R2 (within a single sigma sequence) +covered. R2 across `+compose()+` not covered. R3 implementation gap. See +`+quandledb/PROOF-NARRATIVE.md+` QD-2. + +|KR-7 |`+sigma N+` accepted iff `+N ≥ 1+` |Parser error path |Not +property-tested. +|=== + +=== Proofs blocked + +[width="100%",cols="18%,30%,52%",options="header",] +|=== +|ID |Proof |Blocked by +|KR-2 |Lowering preserves port arity |Typechecker not yet implemented +(see `+READINESS.md+`) + +|KR-3c |R3 invariance |`+KnotTheory.jl+` has no R3 simplifier (see +quandledb QD-2) +|=== + +=== Proofs remaining + +[width="100%",cols="10%,14%,21%,17%,21%,17%",options="header",] +|=== +|ID |Proof |Category |Prover |Priority |Effort +|KR-1 |`+lower+` total on parseable programs |TP |Idris2 + property test +|P1 |1d + +|KR-2 |`+lower+` preserves port arity |TP |Idris2 + impl |P1 |3d + +|KR-3 |`+simplify+` semantics-preserving |ALG |Lean4 / property |P1 |5d + +|KR-4 |Pretty/parse round-trip |INV |Property |P1 |4h + +|KR-5 |ABI primitives load-bearing |ABI |Decision |P3 |2h + +|KR-6 |Two-parser equivalence |INV |Differential property test |P1 |4h + +|KR-7 |Generator index validity |INV |Property test |P2 |1h + +|KR-8 |`+equivalent?+` sound |DOM |Lean4 (via QuandleDB QD-3) |P1 |5d +|=== + +=== Verification commands + +[source,bash] +---- +# Check all Idris2 proofs +just proof-check-idris2 + +# Check all Lean4 proofs +just proof-check-lean4 + +# Run all proof checks +just proof-check-all + +# Scan for dangerous patterns +panic-attack assail --proofs-only +---- + +=== Changelog + +[width="100%",cols="32%,42%,26%",options="header",] +|=== +|Date |Change |By +|2026-04-04 |Initial proof status tracking |Template (rsr-template-repo) + +|2026-06-01 |Replaced template-content scaffold with KRL-specific +obligations KR-1..KR-8. Deleted template-content proof files +(Coq/Lean/Idris) that had zero KRL content. |Audit +|=== diff --git a/PROOF-STATUS.md b/PROOF-STATUS.md deleted file mode 100644 index 55efe6f..0000000 --- a/PROOF-STATUS.md +++ /dev/null @@ -1,96 +0,0 @@ - -# Proof Status — KRL - -> Requirements: [PROOF-NEEDS.md](PROOF-NEEDS.md). -> Single coherent story: [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). -> Assumption registry: [ASSUMPTIONS.md](ASSUMPTIONS.md). - -This file tracks the per-obligation status. Updated 2026-06-01. - -## Summary - -| Category | Total | Done | In Progress | Partial | Blocked | Not Started | -|----------|-------|------|-------------|---------|---------|-------------| -| Typing (TP) | 2 | 0 | 0 | 0 | 0 | 2 | -| Invariant (INV) | 3 | 0 | 0 | 1 | 0 | 2 | -| Algorithm (ALG) | 1 | 0 | 0 | 1 | 0 | 0 | -| ABI (ABI) | 1 | 0 | 0 | 0 | 0 | 1 (decision pending) | -| Domain (DOM) | 1 | 0 | 0 | 0 | 0 | 1 | -| **Total** | **8** | **0** | **0** | **2** | **0** | **6** | - -**Overall:** 0% proven, 25% partial. - -The partial entries (`KR-3` simplification across compose() and -`KR-7` generator index validity) have implementations or smoke -coverage but no property test or formal proof. - -## Proofs done - -| ID | Proof | Prover | File | Date | Verified by | -|----|-------|--------|------|------|-------------| -| — | none yet at the KRL surface level | — | — | — | — | - -The Tangle core proofs (Progress, Preservation, Determinism, -Type Safety + 12 lemmas, 16 results total) in -`hyperpolymath/tangle/proofs/Tangle.lean` are foundational for KRL -because KRL lowers into Tangle. They are tracked in tangle's -PROOF-STATUS, not here. - -## Proofs in progress - -| ID | Proof | Prover | Assignee | Started | Blocker | -|----|-------|--------|----------|---------|---------| -| — | — | — | — | — | — | - -## Proofs partial - -| ID | Proof | Form | Notes | -|----|-------|------|-------| -| KR-3 | `simplify` semantics-preserving | Property test in `KRLAdapter.jl/test/` | R1 + R2 (within a single sigma sequence) covered. R2 across `compose()` not covered. R3 implementation gap. See `quandledb/PROOF-NARRATIVE.md` QD-2. | -| KR-7 | `sigma N` accepted iff `N ≥ 1` | Parser error path | Not property-tested. | - -## Proofs blocked - -| ID | Proof | Blocked by | -|----|-------|------------| -| KR-2 | Lowering preserves port arity | Typechecker not yet implemented (see `READINESS.md`) | -| KR-3c | R3 invariance | `KnotTheory.jl` has no R3 simplifier (see quandledb QD-2) | - -## Proofs remaining - -| ID | Proof | Category | Prover | Priority | Effort | -|----|-------|----------|--------|----------|--------| -| KR-1 | `lower` total on parseable programs | TP | Idris2 + property test | P1 | 1d | -| KR-2 | `lower` preserves port arity | TP | Idris2 + impl | P1 | 3d | -| KR-3 | `simplify` semantics-preserving | ALG | Lean4 / property | P1 | 5d | -| KR-4 | Pretty/parse round-trip | INV | Property | P1 | 4h | -| KR-5 | ABI primitives load-bearing | ABI | Decision | P3 | 2h | -| KR-6 | Two-parser equivalence | INV | Differential property test | P1 | 4h | -| KR-7 | Generator index validity | INV | Property test | P2 | 1h | -| KR-8 | `equivalent?` sound | DOM | Lean4 (via QuandleDB QD-3) | P1 | 5d | - -## Verification commands - -```bash -# Check all Idris2 proofs -just proof-check-idris2 - -# Check all Lean4 proofs -just proof-check-lean4 - -# Run all proof checks -just proof-check-all - -# Scan for dangerous patterns -panic-attack assail --proofs-only -``` - -## Changelog - -| Date | Change | By | -|------|--------|-----| -| 2026-04-04 | Initial proof status tracking | Template (rsr-template-repo) | -| 2026-06-01 | Replaced template-content scaffold with KRL-specific obligations KR-1..KR-8. Deleted template-content proof files (Coq/Lean/Idris) that had zero KRL content. | Audit | diff --git a/READINESS.adoc b/READINESS.adoc new file mode 100644 index 0000000..8afbd23 --- /dev/null +++ b/READINESS.adoc @@ -0,0 +1,144 @@ +== Component Readiness — KRL + +*Standard:* +https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades[CRG +v2.0 STRICT] *Current Grade:* E *Assessed:* 2026-07-21 (demoted D → E) +*Assessor:* Jonathan D.A. Jewell + +''''' + +=== Why the grade moved D → E + +The previous assessment (2026-04-12) recorded Grade D on the strength of +a parser, AST, recursive-descent implementation and a 57-test matrix, +all of which lived in `+KRLAdapter.jl+`. *That repository no longer +exists* — it was discarded, deliberately and not recoverably. + +None of the D evidence can be checked. Under the CRG demotion table, +`+D → E+` applies when _"`the scope narrows so far that the component +barely does anything`"_, which is precisely what happened: with the +adapter gone, nothing in this repository can parse or execute a KRL +program. + +This is a correction to the record, not a regression in the work. The +grade was restated rather than left standing on evidence nobody can +inspect. + +''''' + +=== Grade rationale (evidence for E) + +Grade E criterion: _"`Does something slight … there is a kernel of value +… at least one successful test case demonstrating the kernel of +functionality, and documentation of known failures and limitations.`"_ + +Every item below was executed on 2026-07-21, not inferred from +documentation. + +==== Evidence + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Artefact |Check |Result +|`+spec/grammar.ebnf+` |114-line EBNF, v0.1.0 |present + +|`+examples/*.krl+` |4 example programs |present + +|`+tests/smoke/grammar_smoke.sh+` |lexical conformance of examples to +the grammar |20 checks, all pass + +|`+src/interface/ffi/+` |`+zig build test+` |3/3 pass + +|`+src/interface/ffi/+` |`+zig build+` |produces `+libkrl.a+` + +|`+src/interface/Abi/+` |`+%foreign+` declarations |4, all covered by 11 +Zig exports + +|`+tests/aspect_tests.sh+` |SPDX, banned constructs, ABI/FFI +correspondence |4/4 pass + +|`+tests/e2e.sh+` |full local pipeline |4/4 pass, negative-controlled +|=== + +The kernel of value is the specification plus a set of examples that +provably conform to it at the lexical level, over a C ABI that compiles +and is tested. + +==== Known failures and limitations + +* *No parser, and therefore no execution.* Nothing in this repository +can read a `+.krl+` program and produce a result. `+grammar_smoke.sh+` +is lexical only and says so in its own header. +* *The specification is contested.* `+spec/grammar.ebnf+` here and +`+quandledb/spec/grammar.ebnf+` both claim to be KRL v0.1.0 and are +disjoint on core vocabulary; `+|+` is bound to opposite meanings in the +two. See README. +* *No conformance suite.* There is no executable artefact that an +implementation can be tested against, so "`conforms to the KRL spec`" is +not currently a checkable claim. +* *Proof obligations are unmet.* `+PROOF-STATUS.md+` records 0 of 8 +obligations proven, 2 partial. +* *`+rust-ci.yml+` gates nothing* — it calls the shared Rust reusable, +but this repository contains no `+Cargo.toml+`. + +''''' + +=== Rework needed to reach D + +Grade D requires a matrix of tested scenarios and at least one test per +claimed capability. Concretely: + +[arabic] +. *Reconcile the two grammars* into one normative specification, +resolving the `+|+` collision. +. *Write an executable conformance suite* — programs plus expected +results — so that spec conformance becomes testable rather than +asserted. +. *Run that suite against `+quandledb/server/krl/+`*, the actual +implementation (3,035 lines of Julia plus 1,732 lines of tests). One +passing test per claimed capability is the D bar. + +Until at least (1) and (2) exist, this repository specifies a language +nobody can be shown to implement. + +''''' + +=== Iteration history + +==== Iteration 0 — X (2026-04-05) + +Templated from `+rsr-template-repo+`. Zero KRL-specific content. + +==== Iteration 1 — promoted to E (2026-04-05) + +* `+spec/grammar.ebnf+` (v0.1.0 EBNF) and `+spec/grammar-overview.md+` +* 4 `+examples/+` programs +* `+tests/smoke/grammar_smoke.sh+` (16 lexical assertions) + +==== Iteration 2 — promoted to D (2026-04-12) — *evidence since lost* + +Decision "`Option B — Julia in `+KRLAdapter.jl+``"; lexer, AST, +recursive-descent parser and lowering implemented there, with 57 +dedicated parser tests. The repository holding all of it has since been +discarded, so none of this is verifiable. Retained here as history, not +as evidence. + +==== Iteration 3 — demoted to E (2026-07-21) + +* Grade restated against what is actually present and runnable in this +tree. +* Zig FFI shim repaired: it had never compiled (`+opaque+` type with +fields). +* Three vacuous or false gates repaired (`+aspect_tests.sh+`, +`+e2e.sh+`). +* False `+TangleIR+` lowering claims and dead `+KRLAdapter.jl+` +references removed from the README. + +=== Review cycle + +Reassess when a conformance suite exists and has been run against +`+quandledb/server/krl/+`. + +''''' + +Run `+just crg-badge+` to generate the shields.io badge for the README. diff --git a/READINESS.md b/READINESS.md deleted file mode 100644 index 3c713da..0000000 --- a/READINESS.md +++ /dev/null @@ -1,123 +0,0 @@ - - - -# Component Readiness — KRL - -**Standard:** [CRG v2.0 STRICT](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades) -**Current Grade:** E -**Assessed:** 2026-07-21 (demoted D → E) -**Assessor:** Jonathan D.A. Jewell - ---- - -## Why the grade moved D → E - -The previous assessment (2026-04-12) recorded Grade D on the strength of a -parser, AST, recursive-descent implementation and a 57-test matrix, all of -which lived in `KRLAdapter.jl`. **That repository no longer exists** — it was -discarded, deliberately and not recoverably. - -None of the D evidence can be checked. Under the CRG demotion table, `D → E` -applies when *"the scope narrows so far that the component barely does -anything"*, which is precisely what happened: with the adapter gone, nothing in -this repository can parse or execute a KRL program. - -This is a correction to the record, not a regression in the work. The grade was -restated rather than left standing on evidence nobody can inspect. - ---- - -## Grade rationale (evidence for E) - -Grade E criterion: *"Does something slight … there is a kernel of value … at -least one successful test case demonstrating the kernel of functionality, and -documentation of known failures and limitations."* - -Every item below was executed on 2026-07-21, not inferred from documentation. - -### Evidence - -| Artefact | Check | Result | -|---|---|---| -| `spec/grammar.ebnf` | 114-line EBNF, v0.1.0 | present | -| `examples/*.krl` | 4 example programs | present | -| `tests/smoke/grammar_smoke.sh` | lexical conformance of examples to the grammar | 20 checks, all pass | -| `src/interface/ffi/` | `zig build test` | 3/3 pass | -| `src/interface/ffi/` | `zig build` | produces `libkrl.a` | -| `src/interface/Abi/` | `%foreign` declarations | 4, all covered by 11 Zig exports | -| `tests/aspect_tests.sh` | SPDX, banned constructs, ABI/FFI correspondence | 4/4 pass | -| `tests/e2e.sh` | full local pipeline | 4/4 pass, negative-controlled | - -The kernel of value is the specification plus a set of examples that provably -conform to it at the lexical level, over a C ABI that compiles and is tested. - -### Known failures and limitations - -- **No parser, and therefore no execution.** Nothing in this repository can - read a `.krl` program and produce a result. `grammar_smoke.sh` is lexical - only and says so in its own header. -- **The specification is contested.** `spec/grammar.ebnf` here and - `quandledb/spec/grammar.ebnf` both claim to be KRL v0.1.0 and are disjoint on - core vocabulary; `|` is bound to opposite meanings in the two. See README. -- **No conformance suite.** There is no executable artefact that an - implementation can be tested against, so "conforms to the KRL spec" is not - currently a checkable claim. -- **Proof obligations are unmet.** `PROOF-STATUS.md` records 0 of 8 obligations - proven, 2 partial. -- **`rust-ci.yml` gates nothing** — it calls the shared Rust reusable, but this - repository contains no `Cargo.toml`. - ---- - -## Rework needed to reach D - -Grade D requires a matrix of tested scenarios and at least one test per claimed -capability. Concretely: - -1. **Reconcile the two grammars** into one normative specification, resolving - the `|` collision. -2. **Write an executable conformance suite** — programs plus expected results — - so that spec conformance becomes testable rather than asserted. -3. **Run that suite against `quandledb/server/krl/`**, the actual - implementation (3,035 lines of Julia plus 1,732 lines of tests). One passing - test per claimed capability is the D bar. - -Until at least (1) and (2) exist, this repository specifies a language nobody -can be shown to implement. - ---- - -## Iteration history - -### Iteration 0 — X (2026-04-05) -Templated from `rsr-template-repo`. Zero KRL-specific content. - -### Iteration 1 — promoted to E (2026-04-05) -- `spec/grammar.ebnf` (v0.1.0 EBNF) and `spec/grammar-overview.md` -- 4 `examples/` programs -- `tests/smoke/grammar_smoke.sh` (16 lexical assertions) - -### Iteration 2 — promoted to D (2026-04-12) — **evidence since lost** -Decision "Option B — Julia in `KRLAdapter.jl`"; lexer, AST, recursive-descent -parser and lowering implemented there, with 57 dedicated parser tests. The -repository holding all of it has since been discarded, so none of this is -verifiable. Retained here as history, not as evidence. - -### Iteration 3 — demoted to E (2026-07-21) -- Grade restated against what is actually present and runnable in this tree. -- Zig FFI shim repaired: it had never compiled (`opaque` type with fields). -- Three vacuous or false gates repaired (`aspect_tests.sh`, `e2e.sh`). -- False `TangleIR` lowering claims and dead `KRLAdapter.jl` references removed - from the README. - -## Review cycle - -Reassess when a conformance suite exists and has been run against -`quandledb/server/krl/`. - ---- - -Run `just crg-badge` to generate the shields.io badge for the README. diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..57bf83d --- /dev/null +++ b/README.adoc @@ -0,0 +1,167 @@ +== KRL — Knot Resolution Language + +https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/krl[image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF +Best Practices]] + +KRL (pronounced "`curl`") is the resolution language for +https://github.com/hyperpolymath/quandledb[QuandleDB]. This repository +holds its *normative specification*; the implementation lives in +QuandleDB. + +=== What it is + +QuandleDB is a *knot database* — a database whose stored objects are +knots and tangles, and whose identity relation is equivalence under +ambient isotopy rather than byte equality. KRL is the language you use +to work with it. + +The point of a dedicated language is that the interesting questions +about a knot database are hard ones — is this the same knot, what class +does it fall in, what witnesses the answer — and you should be able to +ask them directly rather than assembling them out of general-purpose +data access. Record retrieval is one operation _within_ KRL, because +without it you could not get at anything; it is not what KRL is for. + +The name reflects the central operation. In knot theory, _resolution_ is +how crossings are resolved in the skein relation — the algebraic heart +of invariant computation. KRL generalises the word to every interaction +with the system: resolving structure, resolving equivalence, resolving +queries. + +=== Where KRL sits + +Three separate projects, developed for different purposes: + +[width="100%",cols="50%,50%",options="header",] +|=== +|Project |What it is +|https://github.com/hyperpolymath/quandledb[*QuandleDB*] |The knot +database. Stores presentations, invariants, fingerprints, equivalence +classes and witnesses. + +|*KRL* (this repository) |QuandleDB’s resolution language. Specified +here, implemented in `+quandledb/server/krl/+`. + +|https://github.com/hyperpolymath/tangle[*Tangle*] |A separate, general +language for knot mathematics — topological, algebraic, geometric and +logical. Turing-complete; not a backend for KRL. +|=== + +KRL and QuandleDB were designed together and are deliberately close. +Tangle is a different project with a different remit that happens to +share the subject matter. The two are related by domain, not by +architecture: *KRL does not compile to, lower into, or depend on +Tangle.* + +____ +[!IMPORTANT] Earlier revisions of this README described a +`+KRL → TangleIR → Tangle+` compilation pipeline and named +`+KRLAdapter.jl+` as the canonical implementation. Neither is true. +`+TangleIR+` does not appear anywhere in the KRL implementation, and +`+KRLAdapter.jl+` no longer exists. Those claims have been removed +rather than restated. +____ + +=== The four operations + +KRL has four operation families. The four-verb shape is deliberate: it +stops "`querying`" from becoming the whole identity of the language. + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Operation |Knot concept |What it does +|*construct* |Tangles, ports, composition, tensor |create or declare +presentations, structures, claims, datasets + +|*transform* |PD code, Reidemeister moves |rewrite, normalise, compose, +concatenate, permute, mutate + +|*resolve* |Isotopy, quandle, equivalence class |decide, disambiguate, +or evaluate equivalence and identity questions + +|*retrieve* |Invariants, witnesses, stored resolutions |inspect, fetch, +project, explain, or return stored or computed results +|=== + +____ +[!NOTE] *Retrieve is not arbitrary database querying.* It recovers +resolution-relevant artefacts: presentations, invariants, witnesses, +equivalence classes, prior resolutions, explanations and provenance. + +Generic data access — arbitrary filters, dashboards, reporting, +analytics, index tuning — is an engine-layer affordance, deliberately +not elevated to a KRL operation. A separate query language is +*deferred*, not absent; see +`+docs/decisions/0002-query-language-deferred.adoc+`. +____ + +=== What this repository holds + +* The grammar specification (`+spec/grammar.ebnf+`). +* Idris2 ABI declarations (`+src/interface/Abi/+`). +* A Zig FFI shim over the C ABI (`+src/interface/ffi/+`). +* Example programs (`+examples/*.krl+`). +* The proof narrative (`+PROOF-NARRATIVE.md+`) and obligations registry. + +It does *not* hold a parser or evaluator. Those are in +`+quandledb/server/krl/+` — 3,035 lines of Julia (lexer, parser, AST, +evaluator, SQL front end) with 1,732 lines of tests. + +=== Status + +Assessed against what is in this tree, not against absent work. + +[width="100%",cols="50%,50%",options="header",] +|=== +|Component |State +|Grammar specification |Drafted (`+spec/grammar.ebnf+`, 114 lines) + +|Examples |Four `+.krl+` programs, lexically checked against the grammar +by `+tests/smoke/grammar_smoke.sh+` (20 checks) + +|Idris2 ABI |Declared — 4 `+%foreign+` declarations + +|Zig FFI |Compiles; 3/3 unit tests pass; `+zig build+` produces +`+libkrl.a+` + +|Parser / evaluator |Not in this repository (see above) + +|Conformance suite |Not yet written — planned, see below +|=== + +There is no parser here, so nothing in this repository can execute a KRL +program. `+tests/smoke/grammar_smoke.sh+` performs lexical-level +checking only and says so. + +=== Known divergence + +Two documents currently call themselves the KRL grammar, and they do not +agree: + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +| |`+krl/spec/grammar.ebnf+` |`+quandledb/spec/grammar.ebnf+` +|Size |114 lines |402 lines + +|Construction |`+sigma+`, `+sigma_inv+`, `+cup+`, `+cap+` |none + +|Retrieval |`+find … where …+` |`+from … \| filter \| sort \| …+` +pipeline + +|Implemented |no |yes +|=== + +They are disjoint on core vocabulary, and `+|+` is bound to *opposite +meanings* in the two — tensor product here, pipeline separator there. +Reconciling them, and giving this repository an executable conformance +suite so that "`the spec`" becomes a thing an implementation can be +tested against, is the next body of work. It is not done, and this +README does not claim otherwise. + +=== Related + +* https://github.com/hyperpolymath/quandledb[QuandleDB] — the knot +database +* https://github.com/hyperpolymath/tangle[Tangle] — general +knot-mathematics language (separate project) +* link:docs/krl_map.html[KRL architecture map (HTML)] diff --git a/README.md b/README.md deleted file mode 100644 index fe12847..0000000 --- a/README.md +++ /dev/null @@ -1,126 +0,0 @@ - - -# KRL — Knot Resolution Language - -[![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/krl) - -KRL (pronounced "curl") is the resolution language for -[QuandleDB](https://github.com/hyperpolymath/quandledb). This repository holds -its **normative specification**; the implementation lives in QuandleDB. - -## What it is - -QuandleDB is a **knot database** — a database whose stored objects are knots and -tangles, and whose identity relation is equivalence under ambient isotopy rather -than byte equality. KRL is the language you use to work with it. - -The point of a dedicated language is that the interesting questions about a knot -database are hard ones — is this the same knot, what class does it fall in, what -witnesses the answer — and you should be able to ask them directly rather than -assembling them out of general-purpose data access. Record retrieval is one -operation *within* KRL, because without it you could not get at anything; it is -not what KRL is for. - -The name reflects the central operation. In knot theory, *resolution* is how -crossings are resolved in the skein relation — the algebraic heart of invariant -computation. KRL generalises the word to every interaction with the system: -resolving structure, resolving equivalence, resolving queries. - -## Where KRL sits - -Three separate projects, developed for different purposes: - -| Project | What it is | -|---|---| -| [**QuandleDB**](https://github.com/hyperpolymath/quandledb) | The knot database. Stores presentations, invariants, fingerprints, equivalence classes and witnesses. | -| **KRL** (this repository) | QuandleDB's resolution language. Specified here, implemented in `quandledb/server/krl/`. | -| [**Tangle**](https://github.com/hyperpolymath/tangle) | A separate, general language for knot mathematics — topological, algebraic, geometric and logical. Turing-complete; not a backend for KRL. | - -KRL and QuandleDB were designed together and are deliberately close. Tangle is a -different project with a different remit that happens to share the subject -matter. The two are related by domain, not by architecture: **KRL does not -compile to, lower into, or depend on Tangle.** - -> [!IMPORTANT] -> Earlier revisions of this README described a `KRL → TangleIR → Tangle` -> compilation pipeline and named `KRLAdapter.jl` as the canonical -> implementation. Neither is true. `TangleIR` does not appear anywhere in the -> KRL implementation, and `KRLAdapter.jl` no longer exists. Those claims have -> been removed rather than restated. - -## The four operations - -KRL has four operation families. The four-verb shape is deliberate: it stops -"querying" from becoming the whole identity of the language. - -| Operation | Knot concept | What it does | -|---|---|---| -| **construct** | Tangles, ports, composition, tensor | create or declare presentations, structures, claims, datasets | -| **transform** | PD code, Reidemeister moves | rewrite, normalise, compose, concatenate, permute, mutate | -| **resolve** | Isotopy, quandle, equivalence class | decide, disambiguate, or evaluate equivalence and identity questions | -| **retrieve** | Invariants, witnesses, stored resolutions | inspect, fetch, project, explain, or return stored or computed results | - -> [!NOTE] -> **Retrieve is not arbitrary database querying.** It recovers -> resolution-relevant artefacts: presentations, invariants, witnesses, -> equivalence classes, prior resolutions, explanations and provenance. -> -> Generic data access — arbitrary filters, dashboards, reporting, analytics, -> index tuning — is an engine-layer affordance, deliberately not elevated to a -> KRL operation. A separate query language is **deferred**, not absent; see -> `docs/decisions/0002-query-language-deferred.adoc`. - -## What this repository holds - -- The grammar specification (`spec/grammar.ebnf`). -- Idris2 ABI declarations (`src/interface/Abi/`). -- A Zig FFI shim over the C ABI (`src/interface/ffi/`). -- Example programs (`examples/*.krl`). -- The proof narrative (`PROOF-NARRATIVE.md`) and obligations registry. - -It does **not** hold a parser or evaluator. Those are in -`quandledb/server/krl/` — 3,035 lines of Julia (lexer, parser, AST, evaluator, -SQL front end) with 1,732 lines of tests. - -## Status - -Assessed against what is in this tree, not against absent work. - -| Component | State | -|---|---| -| Grammar specification | Drafted (`spec/grammar.ebnf`, 114 lines) | -| Examples | Four `.krl` programs, lexically checked against the grammar by `tests/smoke/grammar_smoke.sh` (20 checks) | -| Idris2 ABI | Declared — 4 `%foreign` declarations | -| Zig FFI | Compiles; 3/3 unit tests pass; `zig build` produces `libkrl.a` | -| Parser / evaluator | Not in this repository (see above) | -| Conformance suite | Not yet written — planned, see below | - -There is no parser here, so nothing in this repository can execute a KRL -program. `tests/smoke/grammar_smoke.sh` performs lexical-level checking only and -says so. - -## Known divergence - -Two documents currently call themselves the KRL grammar, and they do not agree: - -| | `krl/spec/grammar.ebnf` | `quandledb/spec/grammar.ebnf` | -|---|---|---| -| Size | 114 lines | 402 lines | -| Construction | `sigma`, `sigma_inv`, `cup`, `cap` | none | -| Retrieval | `find … where …` | `from … \| filter \| sort \| …` pipeline | -| Implemented | no | yes | - -They are disjoint on core vocabulary, and `|` is bound to **opposite meanings** -in the two — tensor product here, pipeline separator there. Reconciling them, -and giving this repository an executable conformance suite so that "the spec" -becomes a thing an implementation can be tested against, is the next body of -work. It is not done, and this README does not claim otherwise. - -## Related - -- [QuandleDB](https://github.com/hyperpolymath/quandledb) — the knot database -- [Tangle](https://github.com/hyperpolymath/tangle) — general knot-mathematics language (separate project) -- [KRL architecture map (HTML)](docs/krl_map.html) diff --git a/REQUIRES_INITIALISATION.adoc b/REQUIRES_INITIALISATION.adoc new file mode 100644 index 0000000..98de172 --- /dev/null +++ b/REQUIRES_INITIALISATION.adoc @@ -0,0 +1,153 @@ +== REQUIRES INITIALISATION + +*This repository is not finished being set up.* 11 substitution token(s) +across 6 file(s) still have no value. + +=== Why this is not already done + +This repo was created from `+hyperpolymath/rsr-template-repo+`. The mint +(`+just repo-init+`) fills every token that has a single mechanical +answer — owner, repo, author, dates, licence, branch — and it has done +so here. + +The tokens below are the ones it _deliberately cannot_ answer. They need +a decision or a fact that exists only in your head: what this project is +for, what command builds it, which port the service listens on, whether +a PGP key is held at all. The template’s own token vocabulary says as +much — you cannot sensibly answer "`required invariants`" in a +thirty-second bootstrap. + +They were left *visibly unfilled on purpose*. The alternatives were both +worse: inventing plausible values would put confident falsehoods into a +security policy and an architecture document, and silently deleting the +sections would hide the fact that a decision is owed. A visible gap is +honest; a fabricated answer is not. + +=== Do not delete this file until every item below is resolved + +This file is the only marker that the work is outstanding. Deleting it +early does not finish the setup, it just conceals it — and the next +person or agent to arrive will reasonably assume the repo is complete. + +* *If you are a person:* delete this file yourself once the last item is +done. +* *If you are an agent:* resolve what you legitimately can, leave the +rest, and delete this file only when no token below remains anywhere in +the tree. Do not delete it to make a gate go green. + +Re-running the estate top-up tool will remove this file automatically +once nothing is outstanding, so the safest way to finish is to fix the +tokens and let the check confirm it. + +=== Do these first + +`+.github/settings.yml+` is applied to the forge by a GitHub App. An +unfilled token here can be written into the repository’s real name or +description. This has fired before in this estate: illegal braces were +collapsed to dashes and a repo was renamed `+-REPO-+`, which then read +as deleted. + +* `+{{DESCRIPTION}}+` — One-line description used in +.github/settings.yml. HIGH PRIORITY: settings.yml is applied by a GitHub +App, so an unfilled token here can be written into forge metadata +verbatim. + +=== What is needed, and where it goes + +==== `+{{BUILD_CMD}}+` + +The exact command that builds this project. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{BUILD_OUTPUT_PATH}}+` + +Where the build artefact lands. + +Appears in: + +* `+QUICKSTART-MAINTAINER.adoc+` + +==== `+{{DEPS}}+` + +Prose summary of runtime/build dependencies. + +Appears in: + +* `+QUICKSTART-MAINTAINER.adoc+` + +==== `+{{DESCRIPTION}}+` + +One-line description used in .github/settings.yml. HIGH PRIORITY: +settings.yml is applied by a GitHub App, so an unfilled token here can +be written into forge metadata verbatim. + +Appears in: + +* `+.github/settings.yml+` + +==== `+{{LANG_STACK}}+` + +The language stack, in prose. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{MUST_INVARIANTS}}+` + +The invariants this project guarantees. Not answerable in a bootstrap; +it is the point of the repo. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{PGP_KEY_URL}}+` + +Public URL the PGP key can be fetched from. Same caveat as +PGP_FINGERPRINT. + +Appears in: + +* `+.well-known/security.txt+` + +==== `+{{PROJECT_DOMAIN}}+` + +Taxonomy value for the subject domain. + +Appears in: + +* `+.machine_readable/6a2/anchor/ANCHOR.a2ml+` + +==== `+{{PROJECT_KIND}}+` + +Taxonomy value (library, service, tool, lab…). + +Appears in: + +* `+.machine_readable/6a2/anchor/ANCHOR.a2ml+` + +==== `+{{PROJECT_UNIQUE_STRENGTH}}+` + +What this does that its alternatives do not. + +Appears in: + +* `+.machine_readable/bot_directives/methodology.a2ml+` + +==== `+{{TEST_CMD}}+` + +The exact command that runs its tests. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +''''' + +Generated by the estate top-up pass. Rationale and the governing rulings +are in `+hyperpolymath/standards+`; the token vocabulary is +`+.machine_readable/ai/PLACEHOLDERS.adoc+` in `+rsr-template-repo+`. diff --git a/REQUIRES_INITIALISATION.md b/REQUIRES_INITIALISATION.md deleted file mode 100644 index a84e0e1..0000000 --- a/REQUIRES_INITIALISATION.md +++ /dev/null @@ -1,144 +0,0 @@ - - -# REQUIRES INITIALISATION - -**This repository is not finished being set up.** 11 substitution token(s) across 6 file(s) still have no value. - -## Why this is not already done - -This repo was created from `hyperpolymath/rsr-template-repo`. The mint -(`just repo-init`) fills every token that has a single mechanical answer — -owner, repo, author, dates, licence, branch — and it has done so here. - -The tokens below are the ones it *deliberately cannot* answer. They need a -decision or a fact that exists only in your head: what this project is for, -what command builds it, which port the service listens on, whether a PGP key -is held at all. The template's own token vocabulary says as much — you cannot -sensibly answer "required invariants" in a thirty-second bootstrap. - -They were left **visibly unfilled on purpose**. The alternatives were both -worse: inventing plausible values would put confident falsehoods into a -security policy and an architecture document, and silently deleting the -sections would hide the fact that a decision is owed. A visible gap is -honest; a fabricated answer is not. - -## Do not delete this file until every item below is resolved - -This file is the only marker that the work is outstanding. Deleting it early -does not finish the setup, it just conceals it — and the next person or agent -to arrive will reasonably assume the repo is complete. - -- **If you are a person:** delete this file yourself once the last item is done. -- **If you are an agent:** resolve what you legitimately can, leave the rest, - and delete this file only when no token below remains anywhere in the tree. - Do not delete it to make a gate go green. - -Re-running the estate top-up tool will remove this file automatically once -nothing is outstanding, so the safest way to finish is to fix the tokens and -let the check confirm it. - -## Do these first - -`.github/settings.yml` is applied to the forge by a GitHub App. An -unfilled token here can be written into the repository's real name or -description. This has fired before in this estate: illegal braces were -collapsed to dashes and a repo was renamed `-REPO-`, which then read as -deleted. - -- `{{DESCRIPTION}}` — One-line description used in .github/settings.yml. HIGH PRIORITY: settings.yml is applied by a GitHub App, so an unfilled token here can be written into forge metadata verbatim. - -## What is needed, and where it goes - -### `{{BUILD_CMD}}` - -The exact command that builds this project. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{BUILD_OUTPUT_PATH}}` - -Where the build artefact lands. - -Appears in: - -- `QUICKSTART-MAINTAINER.adoc` - -### `{{DEPS}}` - -Prose summary of runtime/build dependencies. - -Appears in: - -- `QUICKSTART-MAINTAINER.adoc` - -### `{{DESCRIPTION}}` - -One-line description used in .github/settings.yml. HIGH PRIORITY: settings.yml is applied by a GitHub App, so an unfilled token here can be written into forge metadata verbatim. - -Appears in: - -- `.github/settings.yml` - -### `{{LANG_STACK}}` - -The language stack, in prose. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{MUST_INVARIANTS}}` - -The invariants this project guarantees. Not answerable in a bootstrap; it is the point of the repo. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{PGP_KEY_URL}}` - -Public URL the PGP key can be fetched from. Same caveat as PGP_FINGERPRINT. - -Appears in: - -- `.well-known/security.txt` - -### `{{PROJECT_DOMAIN}}` - -Taxonomy value for the subject domain. - -Appears in: - -- `.machine_readable/6a2/anchor/ANCHOR.a2ml` - -### `{{PROJECT_KIND}}` - -Taxonomy value (library, service, tool, lab…). - -Appears in: - -- `.machine_readable/6a2/anchor/ANCHOR.a2ml` - -### `{{PROJECT_UNIQUE_STRENGTH}}` - -What this does that its alternatives do not. - -Appears in: - -- `.machine_readable/bot_directives/methodology.a2ml` - -### `{{TEST_CMD}}` - -The exact command that runs its tests. - -Appears in: - -- `QUICKSTART-DEV.adoc` - ---- - -Generated by the estate top-up pass. Rationale and the governing rulings are -in `hyperpolymath/standards`; the token vocabulary is -`.machine_readable/ai/PLACEHOLDERS.adoc` in `rsr-template-repo`. diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..e47fdd9 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,16 @@ +== Security Policy + +=== Reporting a Vulnerability + +If you discover a security vulnerability, please report it responsibly. + +*Email:* j.d.a.jewell@open.ac.uk + +*Please include:* - Description of the vulnerability - Steps to +reproduce - Potential impact + +*Response timeline:* - Acknowledgement within 48 hours - Initial +assessment within 7 days - Fix or mitigation within 90 days + +*Safe harbour:* We will not pursue legal action against security +researchers who follow responsible disclosure. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index c7c239f..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,23 +0,0 @@ - -# Security Policy - -## Reporting a Vulnerability - -If you discover a security vulnerability, please report it responsibly. - -**Email:** j.d.a.jewell@open.ac.uk - -**Please include:** -- Description of the vulnerability -- Steps to reproduce -- Potential impact - -**Response timeline:** -- Acknowledgement within 48 hours -- Initial assessment within 7 days -- Fix or mitigation within 90 days - -**Safe harbour:** We will not pursue legal action against security researchers who follow responsible disclosure. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..985253a --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,126 @@ +== Test Requirements — KRL + +____ +Implementation-level proofs and their property-test stand-ins are in +PROOF-NEEDS.md. This file is the *test-coverage register*: every test +that exists, every test that should exist, and the CRG grade against +`+standards/component-readiness-grades+`. +____ + +=== CRG Grade + +*Current grade:* D *Last assessed:* 2026-06-01 (this audit). Promoted E +→ D 2026-04-12 (see READINESS.md). + +D grade criterion: "`Works on some inputs, test matrix present.`" The +test matrix at the spec/grammar/example level is present in this repo. +The actual KRL parser/lower test suite (5577 tests) lives in the +canonical implementation `+KRLAdapter.jl+`. + +=== Test inventory + +==== In this repo + +[width="99%",cols="18%,16%,44%,22%",options="header",] +|=== +|Path |Kind |What it covers |Status +|`+tests/smoke/grammar_smoke.sh+` |Shell smoke |16 lexical assertions on +grammar tokens |PASSING + +|`+tests/aspect_tests.sh+` |Shell |Aspect tagging (`+src/aspects/+`) +|PASSING + +|`+tests/e2e.sh+` |Shell entry-point |Wraps the e2e suite |PASSING + +|`+tests/e2e/template_instantiation_test.sh+` |Shell E2E |Template +instantiation end-to-end |PASSING (template artefact; flag for removal +below) + +|`+tests/workflows/validate_workflows_test.sh+` |Shell |All +`+.github/workflows/+` files have SPDX header + `+name:+` field |PASSING + +|`+src/interface/ffi/test/integration_test.zig+` |Zig |Placeholder FFI +integration test |PASSING (`+placeholder_test_implementation_required+`) + +|`+benches/template_bench.sh+` |Shell |5 micro-benchmarks (validation, +build, tests, workflows, instantiation) |PASSING +|=== + +==== Out-of-repo (companion suites under proof for this repo’s claims) + +[width="100%",cols="22%,21%,57%",options="header",] +|=== +|Path |Kind |What it covers +|`+KRLAdapter.jl/test/parser_test.jl+` |Julia property |Lexer / parser / +lower / 4 example programs (~57 dedicated parser tests) + +|`+KRLAdapter.jl/test/*.jl+` |Julia |Full KRLAdapter suite (~5577 tests) + +|`+quandledb/server/krl/test/*.jl+` |Julia |Server-side parser +equivalence (lexer / parser / sql / seam — 1713 LoC) +|=== + +=== Gaps (what we owe) + +Cross-referenced to PROOF-NEEDS.md and PROOF-NARRATIVE.md. + +[width="100%",cols="11%,33%,30%,26%",options="header",] +|=== +|# |Test gap |Tied to |Effort +|TG-K1 |Round-trip property test: `+parse(pretty(e)) = e+` for every +example |KR-4 |4h + +|TG-K2 |Differential test: +`+KRLAdapter.jl::parse_krl(s) ≡ quandledb/server/krl::parse_any(s)+` on +a generated corpus |KR-6 |4h + +|TG-K3 |Property test: `+sigma 0+`, `+cup 0+`, `+cap 0+` rejected; +`+sigma N+` for `+N ≥ 1+` accepted |KR-7 |1h + +|TG-K4 |Property test: lowering exhausts every `+KRLExpr+` variant (no +`+KRLLowerError+` from un-matched case) |KR-1 / [[A-KR-1.1]] |2h + +|TG-K5 |Property test: port-arity preservation on every `+compose+` and +`+tensor+` in `+examples/+` |KR-2 |4h + +|TG-K6 |Cross-platform fingerprint test (Linux/macOS/WSL) — coordinate +with QuandleDB QD-4 |KR-8 / quandledb QD-4 |1d + +|TG-K7 |Fuzz harness: random byte-strings → `+parse_krl+` → assert +"`either valid AST or `+KRLParseError+`, never a panic`" |KR-1 |1d + +|TG-K8 |Bench: parse-and-lower throughput vs program size (target: +linear) |(perf) |4h + +|TG-K9 |Bench: round-trip cost (`+parse ∘ pretty+`) on the example +corpus |(perf) |4h +|=== + +=== Removed (the template-content cleanup) + +The previous `+TEST-NEEDS.md+` was rsr-template-repo boilerplate +referring to "`rsr-template-repo`" throughout. Its claimed *CRG Grade: C +— ACHIEVED 2026-04-04* referred to the template itself, not to KRL. That +content has been removed; KRL’s actual grade is D, per READINESS.md. + +The template-specific test items (template instantiation, workflow +validation count, build-system zig 0.15.2 update, etc.) remain +inventoried above only because their files still exist; they should be +evaluated for removal when KRL gains repo-specific equivalents. + +=== How to add a new test + +[arabic] +. Add a row to *Test inventory* with path, kind, what-it-covers, status. +. If it discharges a proof obligation, reference the `+KR-N+` id and +note in PROOF-NARRATIVE.md under the relevant obligation’s "`How to +discharge`" line. +. If new assumptions emerge, register them in ASSUMPTIONS.md. + +=== CRG path forward + +* *D → C:* Implement the typechecker (KR-2), discharge KR-1 and KR-4 as +property tests, demonstrate parsing 20+ programs from the knot table. +* *C → B:* 6+ diverse external targets writing KRL programs. +* *B → A:* All P1 obligations in PROOF-NEEDS proven (not just +property-tested). diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 38a2421..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,88 +0,0 @@ - -# Test Requirements — KRL - -> Implementation-level proofs and their property-test stand-ins are in -> [PROOF-NEEDS.md](PROOF-NEEDS.md). This file is the **test-coverage -> register**: every test that exists, every test that should exist, -> and the CRG grade against `standards/component-readiness-grades`. - -## CRG Grade - -**Current grade:** D -**Last assessed:** 2026-06-01 (this audit). Promoted E → D 2026-04-12 -(see [READINESS.md](READINESS.md)). - -D grade criterion: "Works on some inputs, test matrix present." -The test matrix at the spec/grammar/example level is present in this -repo. The actual KRL parser/lower test suite (5577 tests) lives in -the canonical implementation `KRLAdapter.jl`. - -## Test inventory - -### In this repo - -| Path | Kind | What it covers | Status | -|------|------|----------------|--------| -| `tests/smoke/grammar_smoke.sh` | Shell smoke | 16 lexical assertions on grammar tokens | PASSING | -| `tests/aspect_tests.sh` | Shell | Aspect tagging (`src/aspects/`) | PASSING | -| `tests/e2e.sh` | Shell entry-point | Wraps the e2e suite | PASSING | -| `tests/e2e/template_instantiation_test.sh` | Shell E2E | Template instantiation end-to-end | PASSING (template artefact; flag for removal below) | -| `tests/workflows/validate_workflows_test.sh` | Shell | All `.github/workflows/` files have SPDX header + `name:` field | PASSING | -| `src/interface/ffi/test/integration_test.zig` | Zig | Placeholder FFI integration test | PASSING (`placeholder_test_implementation_required`) | -| `benches/template_bench.sh` | Shell | 5 micro-benchmarks (validation, build, tests, workflows, instantiation) | PASSING | - -### Out-of-repo (companion suites under proof for this repo's claims) - -| Path | Kind | What it covers | -|------|------|----------------| -| `KRLAdapter.jl/test/parser_test.jl` | Julia property | Lexer / parser / lower / 4 example programs (~57 dedicated parser tests) | -| `KRLAdapter.jl/test/*.jl` | Julia | Full KRLAdapter suite (~5577 tests) | -| `quandledb/server/krl/test/*.jl` | Julia | Server-side parser equivalence (lexer / parser / sql / seam — 1713 LoC) | - -## Gaps (what we owe) - -Cross-referenced to [PROOF-NEEDS.md](PROOF-NEEDS.md) and [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). - -| # | Test gap | Tied to | Effort | -|---|----------|---------|--------| -| TG-K1 | Round-trip property test: `parse(pretty(e)) = e` for every example | KR-4 | 4h | -| TG-K2 | Differential test: `KRLAdapter.jl::parse_krl(s) ≡ quandledb/server/krl::parse_any(s)` on a generated corpus | KR-6 | 4h | -| TG-K3 | Property test: `sigma 0`, `cup 0`, `cap 0` rejected; `sigma N` for `N ≥ 1` accepted | KR-7 | 1h | -| TG-K4 | Property test: lowering exhausts every `KRLExpr` variant (no `KRLLowerError` from un-matched case) | KR-1 / [[A-KR-1.1]] | 2h | -| TG-K5 | Property test: port-arity preservation on every `compose` and `tensor` in `examples/` | KR-2 | 4h | -| TG-K6 | Cross-platform fingerprint test (Linux/macOS/WSL) — coordinate with QuandleDB QD-4 | KR-8 / quandledb QD-4 | 1d | -| TG-K7 | Fuzz harness: random byte-strings → `parse_krl` → assert "either valid AST or `KRLParseError`, never a panic" | KR-1 | 1d | -| TG-K8 | Bench: parse-and-lower throughput vs program size (target: linear) | (perf) | 4h | -| TG-K9 | Bench: round-trip cost (`parse ∘ pretty`) on the example corpus | (perf) | 4h | - -## Removed (the template-content cleanup) - -The previous `TEST-NEEDS.md` was rsr-template-repo boilerplate -referring to "rsr-template-repo" throughout. Its claimed -**CRG Grade: C — ACHIEVED 2026-04-04** referred to the template -itself, not to KRL. That content has been removed; KRL's actual grade -is D, per [READINESS.md](READINESS.md). - -The template-specific test items (template instantiation, workflow -validation count, build-system zig 0.15.2 update, etc.) remain -inventoried above only because their files still exist; they should -be evaluated for removal when KRL gains repo-specific equivalents. - -## How to add a new test - -1. Add a row to **Test inventory** with path, kind, what-it-covers, status. -2. If it discharges a proof obligation, reference the `KR-N` id and - note in [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md) under the - relevant obligation's "How to discharge" line. -3. If new assumptions emerge, register them in [ASSUMPTIONS.md](ASSUMPTIONS.md). - -## CRG path forward - -- **D → C:** Implement the typechecker (KR-2), discharge KR-1 and KR-4 - as property tests, demonstrate parsing 20+ programs from the knot table. -- **C → B:** 6+ diverse external targets writing KRL programs. -- **B → A:** All P1 obligations in PROOF-NEEDS proven (not just - property-tested). diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc new file mode 100644 index 0000000..dd393ed --- /dev/null +++ b/TOPOLOGY.adoc @@ -0,0 +1,108 @@ +== Architecture Topology — KRL + +=== System overview + +KRL is the resolution language for QuandleDB, a knot database. This +repository holds the *specification* and the *ABI surface*; the parser +and evaluator live in QuandleDB. That split is the single most important +fact about this repository’s topology, and it is the source of most of +its current problems. + +=== Project boundaries + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Project |Repository |Relationship to KRL +|QuandleDB |`+hyperpolymath/quandledb+` |Hosts the KRL implementation +(`+server/krl/+`) and the database KRL addresses. Developed jointly with +KRL. + +|KRL |`+hyperpolymath/krl+` (this repo) |Normative specification, Idris2 +ABI, Zig FFI, examples. + +|Tangle |`+hyperpolymath/tangle+` |*Separate project.* A general +language for knot mathematics. Shares the subject matter; there is no +compilation or dependency relationship in either direction. +|=== + +There is no `+KRL → TangleIR → Tangle+` pipeline. Earlier documentation +in both this repository and `+tangle+` described one; it does not exist, +and `+TangleIR+` appears nowhere in the KRL implementation. + +=== Component overview + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Component |Language |Location |Purpose +|Grammar specification |EBNF |`+spec/grammar.ebnf+` |Normative surface +syntax (contested — see below) + +|ABI declarations |Idris2 |`+src/interface/Abi/+` |4 `+%foreign+` +declarations; types and memory layout + +|FFI shim |Zig |`+src/interface/ffi/+` |11 `+export fn+` over the C ABI; +builds `+libkrl.a+` + +|Examples |KRL |`+examples/*.krl+` |4 programs, lexically checked +against the grammar + +|Smoke suite |Bash |`+tests/smoke/grammar_smoke.sh+` |20 lexical +conformance checks + +|Parser / evaluator |Julia |`+quandledb/server/krl/+` — *not here* +|Lexer, parser, AST, evaluator, SQL front end +|=== + +=== The spec/implementation seam + +.... + spec/grammar.ebnf ──(normative, 114 lines, braid algebra) + │ + ✗ no conformance suite — nothing checks this link + │ + quandledb/spec/grammar.ebnf ──(402 lines, pipeline syntax) + │ + └──> quandledb/server/krl/ (3,035 lines Julia + 1,732 lines tests) +.... + +The two grammar documents are disjoint on core vocabulary, and `+|+` is +bound to opposite meanings in them — tensor product here, pipeline +separator there. Only the second is implemented. Closing this seam with +a reconciled specification and an executable conformance suite is the +primary outstanding work; see `+READINESS.md+`. + +=== ABI/FFI layering + +.... + Idris2 src/interface/Abi/{Types,Layout,Foreign}.idr + │ %foreign declarations (4) + ▼ + C ABI ───────────────────────────────────────── + ▲ + │ export fn (11) + Zig src/interface/ffi/src/main.zig ──> libkrl.a +.... + +`+tests/aspect_tests.sh+` enforces that every `+%foreign+` declaration +is covered by a Zig export. + +=== Integration points + +* *Upstream:* `+hyperpolymath/standards+` (shared reusable workflows, +CRG), Hypatia (neurosymbolic CI scan), eclexiaiser (resource scoring). +* *Downstream:* QuandleDB consumes the specification. Nothing else +depends on this repository. + +=== Deployment + +This repository ships no runtime service. Its outputs are the +specification, `+libkrl.a+`, and the published documentation site +(Ddraig SSG → GitHub Pages). + +* CI/CD: GitHub Actions — E2E/aspect/smoke/FFI gates, governance, secret +scanning, CodeQL, Hypatia. +* Service discovery: *none*. There is no +`+.well-known/groove/manifest.json+`, because this repository exposes no +service. The `+groove-check+` job treats absence as a pass for exactly +this case. `+.well-known/+` carries `+security.txt+`, `+humans.txt+` and +`+ai.txt+` only. diff --git a/TOPOLOGY.md b/TOPOLOGY.md deleted file mode 100644 index 2a9efd4..0000000 --- a/TOPOLOGY.md +++ /dev/null @@ -1,89 +0,0 @@ - - - -# Architecture Topology — KRL - -## System overview - -KRL is the resolution language for QuandleDB, a knot database. This repository -holds the **specification** and the **ABI surface**; the parser and evaluator -live in QuandleDB. That split is the single most important fact about this -repository's topology, and it is the source of most of its current problems. - -## Project boundaries - -| Project | Repository | Relationship to KRL | -|---|---|---| -| QuandleDB | `hyperpolymath/quandledb` | Hosts the KRL implementation (`server/krl/`) and the database KRL addresses. Developed jointly with KRL. | -| KRL | `hyperpolymath/krl` (this repo) | Normative specification, Idris2 ABI, Zig FFI, examples. | -| Tangle | `hyperpolymath/tangle` | **Separate project.** A general language for knot mathematics. Shares the subject matter; there is no compilation or dependency relationship in either direction. | - -There is no `KRL → TangleIR → Tangle` pipeline. Earlier documentation in both -this repository and `tangle` described one; it does not exist, and `TangleIR` -appears nowhere in the KRL implementation. - -## Component overview - -| Component | Language | Location | Purpose | -|---|---|---|---| -| Grammar specification | EBNF | `spec/grammar.ebnf` | Normative surface syntax (contested — see below) | -| ABI declarations | Idris2 | `src/interface/Abi/` | 4 `%foreign` declarations; types and memory layout | -| FFI shim | Zig | `src/interface/ffi/` | 11 `export fn` over the C ABI; builds `libkrl.a` | -| Examples | KRL | `examples/*.krl` | 4 programs, lexically checked against the grammar | -| Smoke suite | Bash | `tests/smoke/grammar_smoke.sh` | 20 lexical conformance checks | -| Parser / evaluator | Julia | `quandledb/server/krl/` — **not here** | Lexer, parser, AST, evaluator, SQL front end | - -## The spec/implementation seam - -``` - spec/grammar.ebnf ──(normative, 114 lines, braid algebra) - │ - ✗ no conformance suite — nothing checks this link - │ - quandledb/spec/grammar.ebnf ──(402 lines, pipeline syntax) - │ - └──> quandledb/server/krl/ (3,035 lines Julia + 1,732 lines tests) -``` - -The two grammar documents are disjoint on core vocabulary, and `|` is bound to -opposite meanings in them — tensor product here, pipeline separator there. Only -the second is implemented. Closing this seam with a reconciled specification and -an executable conformance suite is the primary outstanding work; see -`READINESS.md`. - -## ABI/FFI layering - -``` - Idris2 src/interface/Abi/{Types,Layout,Foreign}.idr - │ %foreign declarations (4) - ▼ - C ABI ───────────────────────────────────────── - ▲ - │ export fn (11) - Zig src/interface/ffi/src/main.zig ──> libkrl.a -``` - -`tests/aspect_tests.sh` enforces that every `%foreign` declaration is covered by -a Zig export. - -## Integration points - -- **Upstream:** `hyperpolymath/standards` (shared reusable workflows, CRG), - Hypatia (neurosymbolic CI scan), eclexiaiser (resource scoring). -- **Downstream:** QuandleDB consumes the specification. Nothing else depends on - this repository. - -## Deployment - -This repository ships no runtime service. Its outputs are the specification, -`libkrl.a`, and the published documentation site (Ddraig SSG → GitHub Pages). - -- CI/CD: GitHub Actions — E2E/aspect/smoke/FFI gates, governance, secret - scanning, CodeQL, Hypatia. -- Service discovery: **none**. There is no - `.well-known/groove/manifest.json`, because this repository exposes no - service. The `groove-check` job treats absence as a pass for exactly this - case. `.well-known/` carries `security.txt`, `humans.txt` and `ai.txt` only. diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..e1dc4ab --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,83 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2026 +Jonathan D.A. Jewell (hyperpolymath) –> + +== Tech-Debt Audit — krl — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. *Companion:* +https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+` +2026-05-26-estate-*-debt audits]. *Combined severity:* `+LOW+`. + +This file records the _raw findings_ — it does not by itself fix the +debt. Each section ends with a '`Recommended next move`' line; closing +the debt is follow-up work. + +=== 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this +repo: + +.... +files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 6. *Severity:* `+>06+`. + +*Marker types* (any non-zero counts above): - Coq `+Axiom+`/`+Admitted+` +— unconditional proof escapes. - Lean `+sorry+`/`+axiom+` — Lean’s +equivalent. - Agda `+postulate+` — accepted axiomatically. - Idris2 +`+believe_me+`/`+assert_total+` — runtime-safe coercion / totality +assumption. - Idris2 top-level `+partial+` — totality-check waived. - F* +`+assume val+`/`+admit_p+` — F* admit. - `+TODO PROOF+` / `+OWED:+` — +self-documented debt markers. - `+unsafePerformIO+`/`+unsafeCoerce+` — +soundness-relevant escape hatches in Haskell/Rust source. + +*Recommended next move:* triage each finding into one of: (a) discharge +by proof, (b) cover with property-tests + a documented refutation +budget, or (c) annotate as a known/necessary axiom (e.g. `+funExt+`) in +`+docs/proof-debt.md+`. + +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`+LICENSE+` +|SPDX header |`+MPL-2.0+` +|Manifest licence |`+NONE+` +|Body classifier |`+Palimp-MPL-2.0+` +|Severity |`+ok+` +|=== + +*Recommended next move:* none for licence. + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |178 +|`+docs/+` files |56 +|`+docs/+` LoC |2498 +|CHANGELOG.md |Y +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`+OK+` +|=== + +*Recommended next move:* none for docs. + +=== Cross-references + +* Estate proof-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+` +* Estate licence-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+` +* Estate documentation-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+` + +''''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). +This file is informational — closing the debt is follow-up work owned by +the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index 3c47a68..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,72 +0,0 @@ - -SPDX-License-Identifier: CC-BY-SA-4.0 -SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) ---> - -# Tech-Debt Audit — krl — 2026-05-26 - -**Source:** estate-wide automated scan 2026-05-26. -**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). -**Combined severity:** `LOW`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -Scanner counted the following markers in proof-bearing files of this repo: - -``` -files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 6. **Severity:** `>06`. - -**Marker types** (any non-zero counts above): -- Coq `Axiom`/`Admitted` — unconditional proof escapes. -- Lean `sorry`/`axiom` — Lean's equivalent. -- Agda `postulate` — accepted axiomatically. -- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. -- Idris2 top-level `partial` — totality-check waived. -- F\* `assume val`/`admit_p` — F\* admit. -- `TODO PROOF` / `OWED:` — self-documented debt markers. -- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. - -**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `NONE` | -| Body classifier | `Palimp-MPL-2.0` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 178 | -| `docs/` files | 56 | -| `docs/` LoC | 2498 | -| CHANGELOG.md | Y | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `OK` | - -**Recommended next move:** none for docs. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer. diff --git a/examples/README.adoc b/examples/README.adoc index f0bf52e..2a972b1 100644 --- a/examples/README.adoc +++ b/examples/README.adoc @@ -1,3 +1,25 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -= examples Pillar +== KRL Examples + +Example programs demonstrating each of the four KRL operation families. + +[width="100%",cols="50%,50%",options="header",] +|=== +|File |Demonstrates +|`+trefoil.krl+` |CONSTRUCT (sigma), RESOLVE (close), TRANSFORM (mirror, +simplify) + +|`+figure_eight.krl+` |CONSTRUCT with alternating crossings, amphichiral +mirror + +|`+query-by-jones.krl+` |RETRIEVE via `+find where+` queries + +|`+tensor-and-close.krl+` |CONSTRUCT via tensor product + closure +|=== + +== Running these + +KRL has no parser yet (grade E as of 2026-04-05). These examples are for +reading only — they will be runnable once the grammar is implemented. + +See `+../spec/grammar.ebnf+` for the formal grammar and +`+../spec/grammar-overview.md+` for an introduction. diff --git a/examples/README.md b/examples/README.md deleted file mode 100644 index 992e408..0000000 --- a/examples/README.md +++ /dev/null @@ -1,22 +0,0 @@ - -## KRL Examples - -Example programs demonstrating each of the four KRL operation families. - -| File | Demonstrates | -|---|---| -| `trefoil.krl` | CONSTRUCT (sigma), RESOLVE (close), TRANSFORM (mirror, simplify) | -| `figure_eight.krl` | CONSTRUCT with alternating crossings, amphichiral mirror | -| `query-by-jones.krl` | RETRIEVE via `find where` queries | -| `tensor-and-close.krl` | CONSTRUCT via tensor product + closure | - -## Running these - -KRL has no parser yet (grade E as of 2026-04-05). These examples are for -reading only — they will be runnable once the grammar is implemented. - -See `../spec/grammar.ebnf` for the formal grammar and `../spec/grammar-overview.md` -for an introduction. diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..53a88aa --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — rsr-template-repo (Developer) + +=== What is rsr-template-repo? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-dev.md b/llm-warmup-dev.md deleted file mode 100644 index 67aac34..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — rsr-template-repo (Developer) - -## What is rsr-template-repo? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc new file mode 100644 index 0000000..c13529e --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — rsr-template-repo (User) + +=== What is rsr-template-repo? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.md b/llm-warmup-user.md deleted file mode 100644 index 2eaf893..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — rsr-template-repo (User) - -## What is rsr-template-repo? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/openlearn/README.adoc b/openlearn/README.adoc new file mode 100644 index 0000000..ea0c0a4 --- /dev/null +++ b/openlearn/README.adoc @@ -0,0 +1,92 @@ +== KRL — OpenLearn Course + +An OpenLearn-style free course introducing the KRL stack: what it is, +why it exists, and how to use it. + +=== Status + +*Scaffold.* Directory structure is in place. Content is pending. + +=== Intended audience + +* Mathematicians new to computational knot theory +* Programmers curious about domain-specific query languages grounded in +algebra +* Open University OpenLearn browsers looking for a worked example of +formal/algebraic DSL design + +=== Intended scope + +==== Module 0 — Why "`Resolution`"? + +Knot theory’s skein relations, how resolution is the central operation, +why "`query`" would undersell it. + +==== Module 1 — Tangles and TangleIR + +Open tangles, closed tangles, ports, crossings, PD codes, composition. +Introduce TangleIR as the canonical interchange object. + +==== Module 2 — The KRL Stack + +Stack layers: KRL surface → TanglePL → TangleIR → Skein.jl + +KnotTheory.jl via KRLAdapter.jl → QuandleDB semantic fingerprints. + +==== Module 3 — Constructing Knots in KRL + +Walkthrough: trefoil, figure-eight. Running a KRL program through the +stack. + +==== Module 4 — Transforming (Reidemeister) + +R1, R2, R3 moves. Simplification. Isotopy invariants. + +==== Module 5 — Resolving (Equivalence) + +Quandle presentations. Fundamental quandle as a functor. Colouring +counts. + +==== Module 6 — Retrieving (Query + Persistence) + +Skein.jl as the store; query by invariant. + +==== Module 7 — Where KRL Fits in the Verisim Framework (optional advanced) + +Octadic structure, observation functors, KRL as a resolution system. + +==== Module 8 — Towards Types (advanced) + +Tropical types, Katagoria/TypeLL integration. (Requires user’s notes to +be written first.) + +=== Directory layout + +.... +openlearn/ +├── README.md (this file) +├── modules/ (module content — markdown/adoc/notebook) +├── exercises/ (interactive exercises, worksheets) +└── references/ (bibliography, links, pre-reqs) +.... + +=== Prerequisites (candidates for pre-reqs / "`If you already know…`" boxes) + +* Basic linear algebra +* Undergraduate abstract algebra (groups, modules — not strictly +required) +* Ability to read Julia or follow pseudocode +* No prior knot theory required (covered from scratch) + +=== Target duration + +~8–12 hours of study (typical OpenLearn course length). + +=== Contribution notes + +Each module should include: 1. Learning outcomes (3–5 bullet points) 2. +Narrative explanation with diagrams (SVG preferred) 3. Interactive +exercises that can run in the KRL playground 4. "`Reflection`" prompt at +the end 5. References to further reading + +Modules 7 and 8 are blocked on the user’s own notes crystallising +(Verisim octadic framework, Katagoria, TypeLL, tropical types). diff --git a/openlearn/README.md b/openlearn/README.md deleted file mode 100644 index 67d6d78..0000000 --- a/openlearn/README.md +++ /dev/null @@ -1,85 +0,0 @@ - -# KRL — OpenLearn Course - -An OpenLearn-style free course introducing the KRL stack: what it is, why it -exists, and how to use it. - -## Status - -**Scaffold.** Directory structure is in place. Content is pending. - -## Intended audience - -- Mathematicians new to computational knot theory -- Programmers curious about domain-specific query languages grounded in algebra -- Open University OpenLearn browsers looking for a worked example of - formal/algebraic DSL design - -## Intended scope - -### Module 0 — Why "Resolution"? -Knot theory's skein relations, how resolution is the central operation, -why "query" would undersell it. - -### Module 1 — Tangles and TangleIR -Open tangles, closed tangles, ports, crossings, PD codes, composition. -Introduce TangleIR as the canonical interchange object. - -### Module 2 — The KRL Stack -Stack layers: KRL surface → TanglePL → TangleIR → Skein.jl + KnotTheory.jl -via KRLAdapter.jl → QuandleDB semantic fingerprints. - -### Module 3 — Constructing Knots in KRL -Walkthrough: trefoil, figure-eight. Running a KRL program through the stack. - -### Module 4 — Transforming (Reidemeister) -R1, R2, R3 moves. Simplification. Isotopy invariants. - -### Module 5 — Resolving (Equivalence) -Quandle presentations. Fundamental quandle as a functor. Colouring counts. - -### Module 6 — Retrieving (Query + Persistence) -Skein.jl as the store; query by invariant. - -### Module 7 — Where KRL Fits in the Verisim Framework (optional advanced) -Octadic structure, observation functors, KRL as a resolution system. - -### Module 8 — Towards Types (advanced) -Tropical types, Katagoria/TypeLL integration. (Requires user's notes to be -written first.) - -## Directory layout - -``` -openlearn/ -├── README.md (this file) -├── modules/ (module content — markdown/adoc/notebook) -├── exercises/ (interactive exercises, worksheets) -└── references/ (bibliography, links, pre-reqs) -``` - -## Prerequisites (candidates for pre-reqs / "If you already know..." boxes) - -- Basic linear algebra -- Undergraduate abstract algebra (groups, modules — not strictly required) -- Ability to read Julia or follow pseudocode -- No prior knot theory required (covered from scratch) - -## Target duration - -~8–12 hours of study (typical OpenLearn course length). - -## Contribution notes - -Each module should include: -1. Learning outcomes (3–5 bullet points) -2. Narrative explanation with diagrams (SVG preferred) -3. Interactive exercises that can run in the KRL playground -4. "Reflection" prompt at the end -5. References to further reading - -Modules 7 and 8 are blocked on the user's own notes crystallising -(Verisim octadic framework, Katagoria, TypeLL, tropical types). diff --git a/openlearn/modules/00-why-resolution.adoc b/openlearn/modules/00-why-resolution.adoc new file mode 100644 index 0000000..b6caaa7 --- /dev/null +++ b/openlearn/modules/00-why-resolution.adoc @@ -0,0 +1,34 @@ +== Module 0 — Why "`Resolution`"? + +*Draft placeholder. Content to be written.* + +=== Learning outcomes + +After this module you will be able to: + +[arabic] +. State what the skein relation is in knot theory +. Explain what "`resolving a crossing`" means algebraically +. Describe why "`query`" undersells what the KRL language does +. Give the four operations KRL supports and how each relates to +resolution + +=== Content (to be written) + +* The skein relation +* Crossing resolution as the algebraic heart of invariant computation +* From "`resolve a crossing`" to "`resolve structure, equivalence, and +queries`" +* The four KRL operations: Construct, Transform, Resolve, Retrieve + +=== Exercises + +* To be added + +=== Reflection + +* To be added + +=== References + +* To be added diff --git a/openlearn/modules/00-why-resolution.md b/openlearn/modules/00-why-resolution.md deleted file mode 100644 index e7da9a0..0000000 --- a/openlearn/modules/00-why-resolution.md +++ /dev/null @@ -1,35 +0,0 @@ - -# Module 0 — Why "Resolution"? - -**Draft placeholder. Content to be written.** - -## Learning outcomes - -After this module you will be able to: - -1. State what the skein relation is in knot theory -2. Explain what "resolving a crossing" means algebraically -3. Describe why "query" undersells what the KRL language does -4. Give the four operations KRL supports and how each relates to resolution - -## Content (to be written) - -- The skein relation -- Crossing resolution as the algebraic heart of invariant computation -- From "resolve a crossing" to "resolve structure, equivalence, and queries" -- The four KRL operations: Construct, Transform, Resolve, Retrieve - -## Exercises - -- To be added - -## Reflection - -- To be added - -## References - -- To be added diff --git a/openlearn/references/bibliography.adoc b/openlearn/references/bibliography.adoc new file mode 100644 index 0000000..6fce6cd --- /dev/null +++ b/openlearn/references/bibliography.adoc @@ -0,0 +1,42 @@ +== Bibliography — KRL OpenLearn Course + +Key references for the KRL stack. + +=== Knot theory + +* Kauffman, L. H. — _On Knots_ (foundational) +* Manturov, V. O. — _Knot Theory_ +* Lickorish, W. B. R. — _An Introduction to Knot Theory_ + +=== Quandles + +* Joyce, D. — "`A classifying invariant of knots, the knot quandle`" +(1982) +* Carter, J. S. — _A Survey of Quandle Ideas_ + +=== Skein relations + +* Jones, V. F. R. — the Jones polynomial papers +* HOMFLY — Freyd, Yetter, Hoste, Lickorish, Millett, Ocneanu + +=== Computational knot theory + +* KnotInfo (knotinfo.math.indiana.edu) +* SnapPy + +=== Category theory for knot theory + +* Baez, J. and Dolan, J. — "`Higher-dimensional algebra and topological +quantum field theory`" + +=== Tangle algebras and compositional diagrams + +* Turaev, V. — _Quantum Invariants of Knots and 3-Manifolds_ + +=== (To be added) Verisim octadic framework + +* User’s own notes — not yet written + +=== (To be added) Katagoria, TypeLL, tropical types + +* User’s own notes — not yet written diff --git a/openlearn/references/bibliography.md b/openlearn/references/bibliography.md deleted file mode 100644 index 9321e23..0000000 --- a/openlearn/references/bibliography.md +++ /dev/null @@ -1,44 +0,0 @@ - -# Bibliography — KRL OpenLearn Course - -Key references for the KRL stack. - -## Knot theory - -- Kauffman, L. H. — *On Knots* (foundational) -- Manturov, V. O. — *Knot Theory* -- Lickorish, W. B. R. — *An Introduction to Knot Theory* - -## Quandles - -- Joyce, D. — "A classifying invariant of knots, the knot quandle" (1982) -- Carter, J. S. — *A Survey of Quandle Ideas* - -## Skein relations - -- Jones, V. F. R. — the Jones polynomial papers -- HOMFLY — Freyd, Yetter, Hoste, Lickorish, Millett, Ocneanu - -## Computational knot theory - -- KnotInfo (knotinfo.math.indiana.edu) -- SnapPy - -## Category theory for knot theory - -- Baez, J. and Dolan, J. — "Higher-dimensional algebra and topological quantum field theory" - -## Tangle algebras and compositional diagrams - -- Turaev, V. — *Quantum Invariants of Knots and 3-Manifolds* - -## (To be added) Verisim octadic framework - -- User's own notes — not yet written - -## (To be added) Katagoria, TypeLL, tropical types - -- User's own notes — not yet written diff --git a/playground/README.adoc b/playground/README.adoc new file mode 100644 index 0000000..11f0db2 --- /dev/null +++ b/playground/README.adoc @@ -0,0 +1,45 @@ +== KRL Playground + +A local PWA playground for KRL (Knot Resolution Language, pronounced +"`curl`"). + +=== Status + +*Scaffold only.* KRL itself is at CRG grade X (no grammar/parser yet). +This playground will follow the language implementation. + +=== Intended architecture + +* *Backend:* KRL source → KRLAdapter.jl (for TangleIR + Skein +persistence) +* *Runtime:* Deno server calling Julia via stdin/stdout or HTTP to a +`+KRLAdapter.jl+`-powered service +* *UI:* ReScript + React SPA with Monaco editor configured for KRL +syntax +* *Execution modes:* +** `+parse+` — show AST +** `+typecheck+` — boundary arity check, port compatibility +** `+compile+` — TangleIR output +** `+invariants+` — compute Jones, Alexander, determinant, signature via +KRLAdapter +** `+store+` — persist to in-memory Skein DB; show query results +** `+visualise+` — render the compiled tangle diagram +* *Share-by-URL:* URL-encoded KRL source + +=== Directory layout + +.... +playground/ +├── README.md (this file) +├── public/ (PWA shell when built) +└── examples/ (starter .krl programs) +.... + +=== Next steps + +This playground is blocked on KRL reaching grade E (grammar + 1 smoke +test). See repo-level `+READINESS.md+` for the KRL implementation path. + +See sibling playgrounds for patterns: - +`+/var/mnt/eclipse/repos/nextgen-languages/eclexia/playground/+` - +`+/var/mnt/eclipse/repos/nextgen-languages/betlang/playground/+` diff --git a/playground/README.md b/playground/README.md deleted file mode 100644 index 24335d6..0000000 --- a/playground/README.md +++ /dev/null @@ -1,45 +0,0 @@ - -# KRL Playground - -A local PWA playground for KRL (Knot Resolution Language, pronounced "curl"). - -## Status - -**Scaffold only.** KRL itself is at CRG grade X (no grammar/parser yet). -This playground will follow the language implementation. - -## Intended architecture - -- **Backend:** KRL source → KRLAdapter.jl (for TangleIR + Skein persistence) -- **Runtime:** Deno server calling Julia via stdin/stdout or HTTP to a - `KRLAdapter.jl`-powered service -- **UI:** ReScript + React SPA with Monaco editor configured for KRL syntax -- **Execution modes:** - - `parse` — show AST - - `typecheck` — boundary arity check, port compatibility - - `compile` — TangleIR output - - `invariants` — compute Jones, Alexander, determinant, signature via KRLAdapter - - `store` — persist to in-memory Skein DB; show query results - - `visualise` — render the compiled tangle diagram -- **Share-by-URL:** URL-encoded KRL source - -## Directory layout - -``` -playground/ -├── README.md (this file) -├── public/ (PWA shell when built) -└── examples/ (starter .krl programs) -``` - -## Next steps - -This playground is blocked on KRL reaching grade E (grammar + 1 smoke test). -See repo-level `READINESS.md` for the KRL implementation path. - -See sibling playgrounds for patterns: -- `/var/mnt/eclipse/repos/nextgen-languages/eclexia/playground/` -- `/var/mnt/eclipse/repos/nextgen-languages/betlang/playground/` diff --git a/spec/grammar-overview.adoc b/spec/grammar-overview.adoc new file mode 100644 index 0000000..32c2b11 --- /dev/null +++ b/spec/grammar-overview.adoc @@ -0,0 +1,112 @@ +== KRL Grammar Overview — v0.1.0 + +*Status:* DRAFT. Grammar drafted 2026-04-05. No parser yet; this +document plus `+grammar.ebnf+` are the only artefacts. + +KRL (pronounced "`curl`") is the Knot Resolution Language — a +compositional DSL for constructing, transforming, resolving, and +retrieving topological objects (tangles, knots, links). + +=== The four operation families + +KRL’s syntax is designed around four verbs that together span every +interaction with the system: + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Family |Operations |Grammar production +|*CONSTRUCT* |build tangles from generators |`+generator+`, +`+compose_expr+`, `+tensor_expr+` + +|*TRANSFORM* |Reidemeister moves, mirror, simplify, normalise +|`+prefix_op+` + +|*RESOLVE* |closure, equivalence, classification |`+"close"+`, +`+"classify"+` + +|*RETRIEVE* |query by invariant |`+query+`, `+filter+` +|=== + +=== Minimal example + +[source,krl] +---- +-- Construct the trefoil as three positive crossings in sequence +let trefoil = close (sigma 1 ; sigma 1 ; sigma 1) ; + +-- Transform by mirror +let mirror_trefoil = mirror trefoil ; + +-- Retrieve by invariant +find where jones = trefoil and crossing < 8 ; +---- + +=== Operator precedence + +From weakest to strongest binding: + +[arabic] +. `+;+` — sequential composition (left-associative) +. `+|+` — tensor product (left-associative) +. prefix operators (`+close+`, `+mirror+`, `+simplify+`, `+normalise+`, +`+classify+`) +. atoms: generators, identifiers, parenthesised expressions + +So `+mirror sigma 1 ; sigma 2+` parses as +`+(mirror (sigma 1)) ; (sigma 2)+`. + +=== Reserved words + +.... +let close mirror simplify normalise classify +find where and +sigma sigma_inv cup cap +.... + +=== Comments + +Line comments start with `+--+` and extend to end of line. + +=== Known gaps (documented failures — honest for grade E) + +[arabic] +. *No parser.* The grammar is written, not implemented. Path to D is +"`grammar → AST → typechecker → compiler to TangleIR (via +KRLAdapter.jl)`". +. *Equivalence predicates (`+equivalent?+`, `+near+`) not yet in +grammar.* Placeholder comment in EBNF; will be added in v0.2. +. *No polymorphic generators.* Only `+sigma N+`, `+sigma_inv N+`, +`+cup N+`, `+cap N+` are defined. No way yet to parameterise by strand +count. +. *No type annotations.* Type safety is by port-arity checking at +compile time; not surface syntax. Will interact with TypeLL integration +later. +. *No import mechanism.* Multi-file programs not yet supported. +. *No error-location reporting.* No parser means no error messages. + +=== Target implementation language for v0.2 parser + +*Decision (2026-04-12): Option B — Julia in KRLAdapter.jl.* + +Rationale: - Grammar is small (3-level precedence, ~12 productions); no +parser generator needed - KRLAdapter.jl is already the correct +integration layer — AST → TangleIR lowering lives naturally alongside +the existing adapters - No bootstrap risk from Tangle (grade C, still +evolving) - Fastest path from E → D grade + +Implementation: `+KRLAdapter.jl/src/parser/+` (lexer.jl, ast.jl, +parser.jl, lower.jl). Public API: +`+parse_krl(src::String) -> KRLProgram+`, +`+lower_krl(prog) -> KRLLoweredProgram+`. + +Option A (Tangle-embedded) remains the aspirational long-term target +once Tangle reaches grade B and has stable macro/DSL hosting. Option C +(sibling OCaml) is archived — would duplicate tangle infrastructure +without benefit at this scale. + +=== See also + +* `+grammar.ebnf+` — the formal grammar +* `+../examples/+` — example KRL programs +* `+../tests/smoke/+` — grammar smoke tests +* `+../EXPLAINME.adoc+` — honest scope of the krl repository diff --git a/spec/grammar-overview.md b/spec/grammar-overview.md deleted file mode 100644 index fea4df7..0000000 --- a/spec/grammar-overview.md +++ /dev/null @@ -1,99 +0,0 @@ - - - -# KRL Grammar Overview — v0.1.0 - -**Status:** DRAFT. Grammar drafted 2026-04-05. No parser yet; this document plus `grammar.ebnf` are the only artefacts. - -KRL (pronounced "curl") is the Knot Resolution Language — a compositional DSL -for constructing, transforming, resolving, and retrieving topological objects -(tangles, knots, links). - -## The four operation families - -KRL's syntax is designed around four verbs that together span every -interaction with the system: - -| Family | Operations | Grammar production | -|---|---|---| -| **CONSTRUCT** | build tangles from generators | `generator`, `compose_expr`, `tensor_expr` | -| **TRANSFORM** | Reidemeister moves, mirror, simplify, normalise | `prefix_op` | -| **RESOLVE** | closure, equivalence, classification | `"close"`, `"classify"` | -| **RETRIEVE** | query by invariant | `query`, `filter` | - -## Minimal example - -```krl --- Construct the trefoil as three positive crossings in sequence -let trefoil = close (sigma 1 ; sigma 1 ; sigma 1) ; - --- Transform by mirror -let mirror_trefoil = mirror trefoil ; - --- Retrieve by invariant -find where jones = trefoil and crossing < 8 ; -``` - -## Operator precedence - -From weakest to strongest binding: - -1. `;` — sequential composition (left-associative) -2. `|` — tensor product (left-associative) -3. prefix operators (`close`, `mirror`, `simplify`, `normalise`, `classify`) -4. atoms: generators, identifiers, parenthesised expressions - -So `mirror sigma 1 ; sigma 2` parses as `(mirror (sigma 1)) ; (sigma 2)`. - -## Reserved words - -``` -let close mirror simplify normalise classify -find where and -sigma sigma_inv cup cap -``` - -## Comments - -Line comments start with `--` and extend to end of line. - -## Known gaps (documented failures — honest for grade E) - -1. **No parser.** The grammar is written, not implemented. Path to D is - "grammar → AST → typechecker → compiler to TangleIR (via KRLAdapter.jl)". -2. **Equivalence predicates (`equivalent?`, `near`) not yet in grammar.** - Placeholder comment in EBNF; will be added in v0.2. -3. **No polymorphic generators.** Only `sigma N`, `sigma_inv N`, `cup N`, `cap N` - are defined. No way yet to parameterise by strand count. -4. **No type annotations.** Type safety is by port-arity checking at compile - time; not surface syntax. Will interact with TypeLL integration later. -5. **No import mechanism.** Multi-file programs not yet supported. -6. **No error-location reporting.** No parser means no error messages. - -## Target implementation language for v0.2 parser - -**Decision (2026-04-12): Option B — Julia in KRLAdapter.jl.** - -Rationale: -- Grammar is small (3-level precedence, ~12 productions); no parser generator needed -- KRLAdapter.jl is already the correct integration layer — AST → TangleIR lowering - lives naturally alongside the existing adapters -- No bootstrap risk from Tangle (grade C, still evolving) -- Fastest path from E → D grade - -Implementation: `KRLAdapter.jl/src/parser/` (lexer.jl, ast.jl, parser.jl, lower.jl). -Public API: `parse_krl(src::String) -> KRLProgram`, `lower_krl(prog) -> KRLLoweredProgram`. - -Option A (Tangle-embedded) remains the aspirational long-term target once Tangle -reaches grade B and has stable macro/DSL hosting. Option C (sibling OCaml) is -archived — would duplicate tangle infrastructure without benefit at this scale. - -## See also - -- `grammar.ebnf` — the formal grammar -- `../examples/` — example KRL programs -- `../tests/smoke/` — grammar smoke tests -- `../EXPLAINME.adoc` — honest scope of the krl repository