Skip to content

Commit 4337b23

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: add CHANGELOG + proof-regression workflow guide
CHANGELOG captures unreleased compositional PD API, pdv1 format, WASM fixes, Zig ABI modernisation, KRL architecture docs integration. PROOF-REGRESSION-WORKFLOW.adoc documents Tangle's Lean 4 integration as a pattern other KRL-stack repos can adopt. Proof-regression is the only test category (of 16) that's 4/5 absent in the estate blitz — tangle is the exception. This doc lowers the barrier for siblings to adopt formal proofs. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent a003623 commit 4337b23

2 files changed

Lines changed: 177 additions & 0 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
3+
4+
# Changelog — Tangle
5+
6+
Tangle is a Turing-complete topological programming language. This file
7+
tracks notable changes to the compiler, stdlib, tooling, and WASM runtime.
8+
9+
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
10+
11+
## [Unreleased]
12+
13+
### Added
14+
- Compositional PD compiler API (`compositional.ml` / `.mli`):
15+
`expr`, `planar_diagram`, `compiled`, `skein_payload` types
16+
- `pdv1_blob_of_pd`: canonical text serialisation format
17+
(`pdv1|x=a,b,c,d,s;...|c=arc,arc;...`)
18+
- `compile_and_send_to_skein`: direct Tangle → Skein integration entry point
19+
- Playground scaffold in `playground/` (placeholder PWA + 2 example programs)
20+
- README rewrite introducing KRL architecture + visual map (docs/krl_map.html)
21+
- CRG v2 READINESS.md (grade C)
22+
23+
### Changed
24+
- Tangle composition typecheck: correct permutation application
25+
- WASM: fixed composed braid locals and helper expectations
26+
- Zig ABI layer modernized
27+
28+
### Fixed
29+
- EXPLAINME.adoc section heading quotes
30+
31+
## Earlier commits (no versions tagged)
32+
33+
### UX infrastructure
34+
- Justfile with doctor, tour, help-me, assail recipes
35+
- UX Manifesto deployment
36+
- Agent instructions methodology layer
37+
38+
### Formal proofs
39+
- Lean 4 proofs: progress, preservation, determinism
40+
- TOPOLOGY.md documentation added
41+
42+
### RSR compliance
43+
- A2ML migration of state files
44+
- SPDX headers, license migration to PMPL-1.0-or-later
45+
- stapeln.toml container definition
46+
- Standard workflow deployment (codeql, hypatia, scorecard, etc.)
47+
48+
### Language development
49+
- Compiler (OCaml/dune): parser, typechecker, evaluator, pretty-printer, REPL
50+
- WASM backend (`tangle-wasm/`)
51+
- LSP server (`tangle-lsp/`)
52+
- Stdlib (`lib/stdlib.tangle`)

‎docs/PROOF-REGRESSION-WORKFLOW.adoc‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
4+
= Proof-Regression Workflow (Tangle's Lean 4 Integration)
5+
Jonathan Jewell (hyperpolymath)
6+
:toc:
7+
8+
== Purpose
9+
10+
Tangle is the only repo in the KRL stack with formal proofs integrated
11+
(Lean 4). This document records the workflow so it can be adopted by
12+
sibling repos (KnotTheory.jl, Skein.jl, KRLAdapter.jl, quandledb) that
13+
would benefit from proof-regression testing.
14+
15+
== What "proof-regression" means (per CRG v2)
16+
17+
A test category in the 16-category taxonomy. Definition: tests that verify
18+
formal proofs *still discharge* after code changes. Not code tests —
19+
proof tests. If a change breaks a previously-discharged proof, the change
20+
is blocked.
21+
22+
Estate-wide gap from 2026-04-05 blitz: only tangle has this category.
23+
The other 4 KRL-stack repos score ✗ or ○.
24+
25+
== Tangle's Lean 4 proof structure
26+
27+
Location: `proofs/` at repo root.
28+
29+
[cols="1,3",options="header"]
30+
|===
31+
|File | Obligations
32+
33+
|`proofs/Progress.lean` | Progress: well-typed terms reduce or are values
34+
|`proofs/Preservation.lean` | Preservation: reduction preserves type
35+
|`proofs/Determinism.lean` | Determinism: reduction relation is deterministic
36+
|===
37+
38+
(Exact file layout may vary — see `proofs/` directory for current state.)
39+
40+
== The regression mechanism
41+
42+
1. Proofs live as .lean files under `proofs/`.
43+
2. `lean --build` (or `lake build` if a `lakefile.lean` exists) checks all
44+
proofs.
45+
3. CI runs the Lean checker on every PR.
46+
4. If any proof fails to check, CI fails → PR blocked.
47+
48+
The proof bodies *are* the regression tests. No separate assertions needed.
49+
50+
== Workflow for adopting this in sibling repos
51+
52+
=== Step 1 — Identify a proof candidate
53+
54+
Look for a claim in the codebase that:
55+
- is stated in a natural-language doc (e.g. an invariant in EXPLAINME.adoc)
56+
- can be mechanised: expressible in some proof system's type theory
57+
- would catch a real bug if the proof breaks
58+
59+
Examples for the KRL stack:
60+
61+
- **KRLAdapter.jl**: `mirror` is an involution (sign-wise) — candidate for Idris2 or Lean 4 formalisation.
62+
- **Skein.jl**: schema migration v3→v4 preserves records (harder; needs a model of SQLite).
63+
- **KnotTheory.jl**: `simplify_pd` output is isotopic to input — complex, would
64+
benefit the whole field.
65+
66+
=== Step 2 — Choose proof system
67+
68+
Per hyperpolymath standard: Idris2 (preferred for dependently-typed ABI/FFI
69+
layer) or Lean 4 (if following tangle's pattern). ATS2 rejected.
70+
71+
For the KRL stack specifically, Idris2 is the main choice given the
72+
standard Idris2 ABI + Zig FFI architecture.
73+
74+
=== Step 3 — Write the proof
75+
76+
- Translate the claim to a formal statement.
77+
- Build up lemmas as needed.
78+
- Discharge using tactics.
79+
80+
=== Step 4 — Wire to CI
81+
82+
Add a CI job that runs `idris2 --check-only` or `lake build` on your proofs
83+
directory. Fail the build if any proof fails.
84+
85+
=== Step 5 — Document
86+
87+
Update PROOF-NEEDS.md: move the claim from "Would benefit from formal proof"
88+
to "Currently verified (by Idris2/Lean 4)".
89+
90+
== Current adoption status (2026-04-05)
91+
92+
[cols="2,2,3",options="header"]
93+
|===
94+
|Repo | Proof-regression | Notes
95+
96+
|tangle | ✓ Lean 4 | Progress, preservation, determinism proved
97+
|KRLAdapter.jl | ✗ | Property tests stand in — see PROOF-NEEDS.md
98+
|KnotTheory.jl | ○ | PROOF-NEEDS.md exists, no discharged proofs
99+
|Skein.jl | ✗ | PROOF-NEEDS.md added 2026-04-05
100+
|quandledb | ✗ | Has Idris2 ABI Types.idr but no proofs
101+
|===
102+
103+
== Why bother
104+
105+
1. **Specification-by-construction.** The proof is the spec. No drift between
106+
documentation and behaviour.
107+
2. **Regression-blocker with zero false positives.** If the proof fails, the
108+
claim fails. No flaky tests.
109+
3. **Standard-raising for the estate.** CRG v2 taxonomy has proof-regression
110+
as a distinct test category; adopting it moves repos closer to grade A.
111+
112+
== When not to bother
113+
114+
- The claim is too narrow to justify proof infrastructure (e.g. trivially-
115+
checked by a 3-line property test).
116+
- The proof system doesn't have the libraries you need.
117+
- The cost of writing the proof exceeds the value of catching regressions
118+
(common for storage/IO layers).
119+
120+
== See also
121+
122+
- Tangle's `proofs/` directory
123+
- `https://leanprover-community.github.io/` (Lean 4 resources)
124+
- `https://www.idris-lang.org/` (Idris2 resources)
125+
- PROOF-NEEDS.md in sibling repos

0 commit comments

Comments
 (0)