Skip to content

docs: de-conflate KRL from Tangle, restate the readiness grade honestly #54

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jul 21, 2026
Merged

docs: de-conflate KRL from Tangle, restate the readiness grade honestly #54

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 33 additions & 13 deletions ASSUMPTIONS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`.

---

Expand Down Expand Up @@ -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 |
177 changes: 82 additions & 95 deletions READINESS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,130 +7,117 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
# 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.
Loading
Loading