Skip to content

docs(proof): KRL-specific proof narrative + assumption registry; drop template content #23

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
Jun 1, 2026
Merged

docs(proof): KRL-specific proof narrative + assumption registry; drop template content #23

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
67 changes: 67 additions & 0 deletions ASSUMPTIONS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
<!--
SPDX-License-Identifier: MPL-2.0
Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
# 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 | 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 |

---

## 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 |
316 changes: 316 additions & 0 deletions PROOF-NARRATIVE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,316 @@
<!--
SPDX-License-Identifier: MPL-2.0
Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
# 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).
Loading
Loading