From 0e1bbb47e9829b6a227c4efdb99ec2d84871db3c Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:55:07 +0100 Subject: [PATCH] docs: de-conflate KRL from Tangle, restate the readiness grade honestly MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The three projects are distinct and were built for different purposes. QuandleDB is the knot database. KRL is its resolution language, developed alongside it. Tangle is a separate, general language for knot mathematics that happens to share the subject matter. Documentation in this repository had fused KRL and Tangle into a single compilation pipeline that does not exist. README.md * Removed the claim that KRL "lowers through TangleIR into Tangle-level computation", and the layer table presenting Tangle as KRL's substrate. `TangleIR` appears 0 times in the KRL implementation; the struct definitions the README documented as "the single hardest-designed artifact in the stack" correspond to no code. * Removed `KRLAdapter.jl` as the named canonical implementation. It no longer exists. A short note records that both claims were false, so the correction is legible rather than silent. * Removed the `TanglePL` usage example, which imports packages that do not exist. * Restated what the repository actually holds, and what it does not: there is no parser here, so nothing in this tree can execute a KRL program. * Added the known divergence between this repository's grammar and QuandleDB's — disjoint on core vocabulary, with `|` bound to opposite meanings. * Restructured to a single

. Ddraig SSG certifies pages against a decidable a11y predicate requiring exactly one

and no heading-level skips; the old README had 8, which is why GitHub Pages was failing. Verified by compiling Ddraig locally and running it: old README FAIL (exit 1), new README ok (exit 0). READINESS.md * Grade D -> E. The entire evidence base for D was a parser, AST, lowering pass and 57-test matrix in `KRLAdapter.jl`, which no longer exists, so none of it can be checked. The CRG demotion table gives `D -> E` for "the scope narrows so far that the component barely does anything", which is what happened. * Replaced the evidence section with checks that were executed on 2026-07-21: grammar smoke 20/20, zig build test 3/3, aspect 4/4, e2e 4/4. * Documented the limitations plainly, including that no conformance suite exists, so "conforms to the KRL spec" is not currently a checkable claim. * Removed the duplicated "Path to C"/"Path to B" sections. ASSUMPTIONS.md * Added a Status column. Seven DESIGN assumptions named code in `KRLAdapter.jl`. A DESIGN assumption is defined in this file as "true by construction in our code" — with the code gone there is no construction left to be true by. * A-KR-1.1, 1.2, 2.1, 3.2, 4.1 marked UNANCHORED; A-KR-6.1 and 6.2 marked VOID (both presuppose two implementations, and only one exists). * Verified that no re-anchoring is possible: `sigma`, `cup`, `cap`, `r1_simplify` and any pretty-printer appear 0 times in `quandledb/server/krl/`. The braid generators these assumptions describe are implemented nowhere. * The four MATH assumptions are untouched — they rest on external theorems. TOPOLOGY.md * Was pure RSR-template residue describing the template itself, its dogfood gate, and "500+ RSR-based repositories" downstream. Replaced with KRL's actual topology: the three project boundaries, the ABI/FFI layering, and the spec/implementation seam that no conformance suite currently checks. * States that this repository exposes no Groove service and has no `.well-known/groove/manifest.json`, rather than implying one exists. --- ASSUMPTIONS.md | 46 +++++-- READINESS.md | 177 +++++++++++------------- README.md | 363 ++++++++++++------------------------------------- TOPOLOGY.md | 89 +++++++++--- 4 files changed, 276 insertions(+), 399 deletions(-) diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md index 733a0bd..5d59a80 100644 --- a/ASSUMPTIONS.md +++ b/ASSUMPTIONS.md @@ -17,19 +17,38 @@ Cross-references use `[[A-KR-N.M]]` syntax, resolved here. --- -| ID | Class | Statement | Cited by | Where it lives | -|----|-------|-----------|----------|----------------| -| A-KR-1.1 | DESIGN | Every `KRLExpr` AST variant has a matching arm in `KRLAdapter.jl::lower.jl` | KR-1 | `KRLAdapter.jl/src/parser/lower.jl` | -| A-KR-1.2 | DESIGN | `KRLAdapter.jl/src/parser/ast.jl` defines the only AST shapes the parser produces | KR-1 | `KRLAdapter.jl/src/parser/ast.jl` + `parser.jl` | -| A-KR-2.1 | DESIGN | 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 | KRL grammar definitions; `KRLAdapter.jl/src/operations.jl` | -| A-KR-2.2 | MATH | `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 | 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 | `KRLAdapter.jl::r1_simplify` / `r2_simplify` / `r3_simplify` implement those moves faithfully (R3 is a current GAP — see `quandledb/PROOF-NARRATIVE.md` QD-2) | KR-3 | `KRLAdapter.jl/src/operations.jl` | -| A-KR-4.1 | DESIGN | KRL pretty-printer's bracketing is unambiguous: `;` only inside parens; tensor `\|` has lower precedence than compose `;` inside parens | KR-4 | `KRLAdapter.jl` pretty; `spec/grammar.ebnf` | -| A-KR-6.1 | DESIGN | `KRLAdapter.jl::parse_krl` and `quandledb/server/krl/Parser.jl::parse_any` both target `spec/grammar.ebnf` v0.1.0 | KR-6 | `spec/grammar.ebnf` | -| A-KR-6.2 | DESIGN | Both implementations share the same `Token` enumeration: keyword set, identifier shape, integer/string literal shapes | KR-6 | `KRLAdapter.jl/src/parser/lexer.jl` and `quandledb/server/krl/Lexer.jl` | -| A-KR-8.1 | MATH (partial) | 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 | Two non-isomorphic quandles have distinct canonical presentations (true by definition of "canonical") | KR-8 | Standard algebraic-presentation result | +| 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`. --- @@ -65,3 +84,4 @@ file with the date and reason. | 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/READINESS.md b/READINESS.md index 0b1f763..3c713da 100644 --- a/READINESS.md +++ b/READINESS.md @@ -7,130 +7,117 @@ Copyright (c) Jonathan D.A. Jewell # Component Readiness — KRL **Standard:** [CRG v2.0 STRICT](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades) -**Current Grade:** D -**Assessed:** 2026-04-12 (promoted E → D after iteration 2) +**Current Grade:** E +**Assessed:** 2026-07-21 (demoted D → E) **Assessor:** Jonathan D.A. Jewell --- -## Grade rationale (evidence for D — promoted from E) +## Why the grade moved D → E -Grade D criterion: "Works on some inputs, test matrix present." +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. -### Evidence +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. -- **Parser implemented:** `KRLAdapter.jl/src/parser/` (Julia, Option B decision 2026-04-12) - - `lexer.jl` — full lexer with position tracking, `KRLLexError` - - `ast.jl` — all AST node types (`KRLProgram`, `KRLBinding`, `KRLGenerator`, - `KRLCompose`, `KRLTensor`, `KRLPrefixOp`, `KRLParenExpr`, `KRLIdentifier`, - `KRLQuery`, `KRLFilter`, `KRLIntValue`, `KRLStrValue`, `KRLIdentValue`) - - `parser.jl` — recursive descent, full v0.1.0 grammar - - `lower.jl` — AST → TangleIR lowering with `KRLLowerError` -- **Grammar ambiguity resolved:** `;` as sequential composition only fires - inside parenthesised expressions (`in_parens=true`); at statement level `;` - is the terminator. -- **Test matrix:** `KRLAdapter.jl/test/parser_test.jl` — 5 testsets, 57 tests - - Lexer: keywords, identifiers, integers, strings, operators, punctuation, - comments stripped, position tracking, lex error, unterminated string - - Parser: 20 grammar cases including all generators, let bindings, sequential - compose (with parens), tensor product, prefix ops, queries with `and` chains - - Parser errors: missing `;`, unrecognised token, missing index, zero index - - Example .krl files: all 4 examples in `krl/examples/` parse without error - - Lowering: sigma/sigma_inv → TangleIR, compose, trefoil, mirror, let binding, - unbound identifier error, query → KRLQueryPlan -- **5577 tests pass** (full KRLAdapter.jl suite including parser tests) - -### Grammar coverage - -The implemented grammar (v0.1.0): - -| Construct | Status | -|-----------|--------| -| `let` binding | ✅ | -| `sigma`, `sigma_inv`, `cup`, `cap` generators | ✅ | -| Sequential composition `(a ; b)` | ✅ | -| Tensor product `a \| b` | ✅ | -| `close`, `mirror`, `simplify`, `normalise`, `classify` | ✅ | -| `find where` queries with `and` | ✅ | -| Parenthesised sub-expressions | ✅ | -| Identifier references (let-bound) | ✅ | -| Line comments `--` | ✅ | -| String, integer, identifier filter values | ✅ | - -### What is NOT yet implemented (documented gaps — D grade) - -- **No typechecker.** Port-arity compatibility (e.g. composing a 2-strand - braid with a 3-strand tangle) not verified at parse time. -- **R2 simplification across compose() boundaries.** `simplify_ir` detects - R2 bigons by arc-index overlap, but `compose()` renumbers arcs so adjacent - sigma/sigma_inv pairs are not detected. Tracked in `KRLAdapter.jl` issues. -- **No pretty-printer.** `KRLProgram → string` round-trip not yet implemented. -- **No RESOLVE family.** `classify` is parsed and lowered (identity) but - not dispatched to the query layer. +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 E rationale (retained for history) - -Grade E criterion: "At least 1 test, documented failures." - -### Evidence (iteration 1) - -- Grammar drafted: `spec/grammar.ebnf`, `spec/grammar-overview.md` -- 4 examples in `examples/` -- Shell smoke test: `tests/smoke/grammar_smoke.sh` (16 lexical assertions) +## 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."* -## Path to C (alpha-stable) +Every item below was executed on 2026-07-21, not inferred from documentation. -After D: typechecker (port-arity + generator index validity), deeper TangleIR -compilation correctness, annotation per-directory, dogfooding by parsing 20+ -KRL programs from the knot table. Fix R2 simplification across compose() -boundaries. +### Evidence -## Path to B (beta) +| 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`. -After C: 6+ diverse external targets (knot researchers, DSL authors, -topology educators) write KRL programs and report back. +--- -## Path to C (alpha-stable) +## Rework needed to reach D -After D: typechecker (port-arity + generator index validity), compiler -to TangleIR via KRLAdapter.jl, deep annotation per-directory, real -dogfooding by parsing 20+ KRL programs representing knots from the -knot table. +Grade D requires a matrix of tested scenarios and at least one test per claimed +capability. Concretely: -## Path to B (beta) +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. -After C: 6+ diverse external targets (knot researchers, DSL authors, -topology educators) write KRL programs and report back. +Until at least (1) and (2) exist, this repository specifies a language nobody +can be shown to implement. --- ## Iteration history -### Iteration 0 (X grade — 2026-04-05 initial scaffold) -Templated from rsr-template-repo. Zero KRL-specific content. +### 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 1 (promoted to E — 2026-04-05) -- spec/grammar.ebnf (v0.1.0 EBNF) -- spec/grammar-overview.md -- 4 examples/ programs -- tests/smoke/grammar_smoke.sh (16 lexical assertions, all passing) +### 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 2 (promoted to D — 2026-04-12) -- Decision: Option B — Julia in KRLAdapter.jl -- Implemented: lexer, AST, recursive-descent parser, lowering (KRLAdapter.jl) -- Grammar ambiguity fixed: `;` as compose only inside parentheses -- 57 dedicated parser tests + all 4 example files parse cleanly -- 5577 total KRLAdapter.jl tests pass +### 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 on typechecker implementation or when 20+ knot-table programs -have been parsed successfully. +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 your README. +Run `just crg-badge` to generate the shields.io badge for the README. diff --git a/README.md b/README.md index ca874f3..fe12847 100644 --- a/README.md +++ b/README.md @@ -3,307 +3,124 @@ SPDX-License-Identifier: CC-BY-SA-4.0 SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell --> -[![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 architecture map (HTML)](docs/krl_map.html) - -# What it is - -KRL (Knot Resolution Language) is QuandleDB’s canonical resolution DSL: -a database-facing language whose domain is knot/tangle identity, -equivalence, transformation, and disambiguation. It is the user- and -author-facing language for constructing, transforming, resolving, and -retrieving knot/tangle presentations, invariants, fingerprints, -equivalence classes, witnesses, and disambiguation results. - -The name reflects the central operation: *resolution*. In knot theory, -resolution is how crossings are resolved in the skein relation — the -algebraic heart of invariant computation. KRL extends this to cover -every interaction with the system: resolving structure, resolving -equivalence, resolving queries. - -KRL is database-facing but not *merely* a query language. "Query" would -name only one of four operations; "resolution" names the mathematical -act that runs through all of them. Two framings to avoid: "a database -language" alone wrongly suggests SQL-for-knots, and "a surface DSL over -Tangle" alone makes QuandleDB incidental and KRL too compiler-ish. KRL -is precisely QuandleDB’s resolution DSL — it lowers through TangleIR -into Tangle-level computation, with QuandleDB and Skein.jl as its -persistence and computation backends. - -# Architecture position - -KRL is the surface language of a federated resolution stack. Each layer -answers a distinct question: - - ---- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Layer

Role — and the question it answers

KRL
-(this repository)

User-/author-facing resolution DSL. "What question or claim -are we making about knot-structured identity?" Spec, ABI, FFI -scaffolds; implementations in KRLAdapter.jl (canonical) and -quandledb/server/krl/.

TangleIR

Lowered intermediate representation. "What normalized -computational object represents that resolution task?" Defined in -KRLAdapter.jl, consumed by -hyperpolymath/tangle.

Tangle

Full computational / programming substrate. "What executable -knot-theoretic program or transformation system carries this out?" -Proven type-safe small-step semantics -(hyperpolymath/tangle/proofs/Tangle.lean).

QuandleDB

Persistence + invariant/equivalence database. "Where -presentations, invariants, fingerprints, equivalence classes, witnesses, -and results live." (hyperpolymath/quandledb)

Skein.jl

Computational / backend library. "One engine that computes, -transforms, normalizes, or evaluates the objects." -(hyperpolymath/Skein.jl)

+# KRL — Knot Resolution Language -**This repo** is responsible for: - -- The KRL grammar specification (`spec/grammar.ebnf`). - -- Idris2 ABI types (`src/interface/Abi/`). - -- Zig FFI scaffolds (`src/interface/ffi/`). - -- Example programs (`examples/`). - -- The proof narrative (`PROOF-NARRATIVE.md`) and obligations registry. +[![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) -The actual KRL parser, lowering, and adapter implementations live in the -companion repos `KRLAdapter.jl` (canonical) and `quandledb/server/krl/` -(server-side query parser — different role). See `PROOF-NARRATIVE.md` -for the two-implementation rationale and the equivalence obligation -`KR-6`. +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. -KRL is **not** responsible for: +## What it is -- Invariant computation (→ JuliaKnot.jl) +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. -- Persistence (→ Skein.jl) +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. -- Equivalence reasoning (→ QuandleDB) +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. -- Surface-language implementation (→ KRLAdapter.jl) +## Where KRL sits -# The four KRL operations +Three separate projects, developed for different purposes: -KRL has exactly four operations. The four-verb shape is deliberate: it -stops "querying" from becoming the whole identity of the language. +| 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. | -**construct** -create or declare presentations, structures, claims, datasets +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.** -**transform** -rewrite, normalize, compose, concatenate, permute, mutate +> [!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. -**resolve** -decide / disambiguate / evaluate equivalence or identity questions +## The four operations -**retrieve** -inspect, fetch, project, explain, or return stored or computed results +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

Primary site

Example syntax

Construct

Tangles, ports, composition, tensor

TanglePL

compose sigma1 -sigma1
-tensor a b
-close t

Transform

PD code, Reidemeister moves

JuliaKnot.jl

simplify t
-normalise t
-mirror t

Resolve

Isotopy, quandle, equivalence class

QuandleDB

equivalent? a b
-classify t
-near t

Retrieve

Invariants, witnesses, stored resolutions

Skein.jl + QuandleDB

find where jones -= p
-where crossing < -8

+| 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. +> resolution-relevant artefacts: presentations, invariants, witnesses, +> equivalence classes, prior resolutions, explanations and provenance. > -> Generic data access — arbitrary filters, dashboards, reporting, -> analytics, exploratory search, index tuning — is an **engine-layer** -> affordance (Skein.jl predicates over SQLite; QuandleDB’s filtered -> endpoints), deliberately **not** elevated to a KRL operation or a -> rival query language. A separate query language is **deferred**, not -> absent; see `docs/decisions/0002-query-language-deferred.adoc` for the -> rationale and trigger conditions. - -# Grammar (sketch) +> 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`. - expr ::= atom - | expr ';' expr (* sequential composition *) - | expr '|' expr (* tensor product *) - | 'close' expr (* closure / trace *) - | 'mirror' expr - | 'simplify' expr - | 'let' IDENT '=' expr +## What this repository holds - atom ::= IDENT (* named tangle *) - | generator - - generator ::= 'sigma' INT (* positive crossing *) - | 'sigma_inv' INT (* negative crossing *) - | 'cup' INT (* cup on strands i,i+1 *) - | 'cap' INT (* cap on strands i,i+1 *) - - query ::= 'find' 'where' filter ('and' filter)* - filter ::= IDENT '=' value - | IDENT '<' INT - | IDENT '>' INT - -# TangleIR — the canonical interchange - -All KRL expressions compile to `TangleIR`. This is the object that flows -between all layers of the stack: - -```julia -struct Port - id::Symbol - side::Symbol # :top | :bottom | :left | :right - index::Int - orientation::Symbol # :in | :out | :unknown -end - -struct CrossingIR - id::Symbol - sign::Int # +1 (positive) | -1 (negative) - arcs::NTuple{4,Int} # PD-style: (a, b, c, d) arc indices -end - -struct TangleMetadata - name::Union{String,Nothing} - source_text::Union{String,Nothing} - tags::Vector{String} - provenance::Symbol # :user | :derived | :rewritten | :imported - extra::Dict{Symbol,Any} -end - -struct TangleIR - id::UUID - ports_in::Vector{Port} - ports_out::Vector{Port} - crossings::Vector{CrossingIR} - components::Vector{Vector{Int}} # arc index groups per component - metadata::TangleMetadata -end -``` - -`TangleIR` is the single hardest-designed artifact in the stack. Every -other interface is a view over it, a service to it, or a transformation -of it. - -# Usage - -```julia -using TanglePL, Skein - -# parse and compile -ir = compile_tangle("sigma1 ; sigma1 ; sigma1") - -# store -db = SkeinDB("knots.db") -id = store!(db, ir; name="trefoil") - -# query -candidates = find_equivalence_candidates(db, ir) - -# retrieve source -src = reconstruct_source(ir) # generates valid KRL; not necessarily original -``` - -# Status +- 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. -- Grammar: defined (sketch above, formal PEG in progress) +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. -- AST: defined +## Status -- Typechecker: boundary arity checking implemented +Assessed against what is in this tree, not against absent work. -- Compiler (AST → TangleIR): in development +| 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 | -- Decompiler (IR → source): stub, in progress +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. -- Skein integration: planned +## Known divergence -# Related +Two documents currently call themselves the KRL grammar, and they do not agree: -- Skein — persistence - and query +| | `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 | -- [QuandleDB](../quandle-db/README.adoc) — semantic fingerprinting +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. -- JuliaKnot — - invariant engine +## Related -- [Next-generation languages](../nextgen-languages/README.adoc) +- [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/TOPOLOGY.md b/TOPOLOGY.md index 4ad8569..2a9efd4 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.md @@ -2,35 +2,88 @@ SPDX-License-Identifier: CC-BY-SA-4.0 Copyright (c) Jonathan D.A. Jewell --> - + -# Architecture Topology +# Architecture Topology — KRL -## System Overview +## System overview -RSR (Rhodium Standard Repository) template provides the canonical scaffold for all hyperpolymath projects, with integrated CI/CD, documentation, and service discovery patterns. +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. -## Component Overview +## Project boundaries -| Component | Language | Purpose | -|-----------|----------|---------| -| dogfood-gate workflow | YAML | Quality checks (CRG, security, linting) | -| eclexiaiser-validate job | YAML | Resource cost awareness scoring | -| Groove discovery | JSON | Service endpoint registration | +| 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. | -## Data Flow +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 ``` -[Code Push] → [GitHub Actions] → [hypatia scan] → [eclexiaiser validate] → [Results] + 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 ``` -## Integration Points +`tests/aspect_tests.sh` enforces that every `%foreign` declaration is covered by +a Zig export. -- **Upstream**: Hypatia (neurosymbolic CI/CD), eclexiaiser (resource scoring) -- **Downstream**: All RSR-based repositories (500+ instances) +## 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 -- Container: Stapeln Six ecosystem -- CI/CD: GitHub Actions → Hypatia scan → eclexiaiser-validate (6 scorecard dimensions) → Mirror -- Service Discovery: Groove protocol (.well-known/groove/manifest.json) +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.