Skip to content

Commit cc46136

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
docs(proof): Tangle proof narrative + assumption registry (#25)
Adds the coherent proof story for Tangle and brings PROOF-NEEDS.md into line with what has actually been proven in proofs/Tangle.lean. Added: - PROOF-NARRATIVE.md — the single coherent story. Covers the 16 Lean results already proven (Progress, Preservation, Determinism, Type Safety + 12 supporting lemmas) AND the 9 remaining obligations (TG-1..TG-9) with statement, "why valuable", status, explicit assumptions, and "how to discharge" per obligation. - ASSUMPTIONS.md — registry of 16 load-bearing unproven assumptions (classified MATH / DESIGN / EMPIRICAL). Rewritten: - PROOF-NEEDS.md — previously read as if Tangle were greenfield ("Prove: type soundness... Prove: type checking terminates..."). Now correctly: * acknowledges proofs/Tangle.lean delivers Progress + Preservation + Determinism + Type Safety for the let-free fragment (16 results, all Qed), * enumerates the 9 remaining obligations TG-1..TG-9 with category, prover, priority, effort estimate. Tier promoted from "HIGH" prose-only to T1 Critical (this repo owns the type system). The narrative makes the let-free-fragment scope of T-TypeSafety explicit (it was previously a header comment inside Tangle.lean), and proposes TG-1 as the standard POPLmark-machinery extension. Part of the focused krl + quandledb + tangle audit/elevation pass. Not estate-wide. Companion PRs in krl (#23) and quandledb landing in parallel. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent bdf5968 commit cc46136

3 files changed

Lines changed: 485 additions & 33 deletions

File tree

‎ASSUMPTIONS.md‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
# Assumptions Registry — Tangle
6+
7+
Every load-bearing **unproven** assumption used in this repo, with an
8+
ID, classification, and the obligation it supports.
9+
10+
Classifications:
11+
- **MATH** — true by an external mathematical theorem (cite it)
12+
- **DESIGN** — true by construction in our code (must remain true; flag if you change the named code)
13+
- **EMPIRICAL** — believed from testing; not formally verified
14+
- **CRYPTO** — standard cryptographic-primitive assumption
15+
16+
Cross-references use `[[A-TG-N.M]]` syntax, resolved here.
17+
18+
---
19+
20+
| ID | Class | Statement | Cited by | Where it lives |
21+
|----|-------|-----------|----------|----------------|
22+
| A-TG-1.1 | DESIGN | Capture-avoiding substitution is well-defined on the de Bruijn representation `HasType` uses | TG-1 | `Tangle.lean` `Ctx` definition + de Bruijn discipline |
23+
| A-TG-1.2 | MATH | Standard weakening + substitution lemmas hold for the `HasType` rules (POPLmark / TAPL §8) | TG-1 | TAPL Ch. 9; Pierce 2002 |
24+
| A-TG-2.1 | DESIGN | Type-checking proceeds by syntactic recursion on `Expr` (no impredicative steps; matches `typecheck.ml`'s shape) | TG-2 | `compiler/lib/typecheck.ml` |
25+
| A-TG-2.2 | DESIGN | Equality on `Ty` is decidable (Lean: `deriving DecidableEq`; OCaml: structural `=`) | TG-2 | `Tangle.lean::Ty`; `compiler/lib/ast.ml` |
26+
| A-TG-3.1 | DESIGN | The OCaml AST in `compiler/lib/ast.ml` is in bijection with the Lean AST in `Tangle.lean::Expr` | TG-3 | Both files, by construction |
27+
| A-TG-3.2 | DESIGN | OCaml `String.equal`, `Int.equal` coincide with Lean's `==` on the values used at runtime | TG-3 | Standard library agreement; verify at the FFI boundary |
28+
| A-TG-4.1 | DESIGN | `pretty.ml`'s bracketing is unambiguous w.r.t. `parser.mly`'s precedence | TG-4 | `compiler/lib/pretty.ml`, `compiler/lib/parser.mly` |
29+
| A-TG-4.2 | DESIGN | Lexer never strips information needed by the parser (e.g. whitespace within braid literals) | TG-4 | `compiler/lib/lexer.mll` |
30+
| A-TG-5.1 | DESIGN | Every rewrite in `compositional.ml` is `Expr → Expr` (no mutation) | TG-5 | `compiler/lib/compositional.ml` |
31+
| A-TG-5.2 | DESIGN | No rewrite introduces a new free variable | TG-5 | Each rewrite, individually |
32+
| A-TG-6.1 | MATH | WASM small-step semantics is well-defined; assume the official Wasm spec / WasmCert-Isabelle definition | TG-6 | wasm-spec, WasmCert-Isabelle |
33+
| A-TG-6.2 | DESIGN | Source semantics has no floating-point non-determinism (Tangle has only `Int` currently) | TG-6 | `Tangle.lean::Ty` lacks `.float` |
34+
| A-TG-7.1 | MATH | Word problem in the braid group `B_n` is solvable in polynomial time (Birman–Ko–Lee / Garside normal form) | TG-7 | Birman–Ko–Lee 1998; _A New Approach to the Word and Conjugacy Problems in the Braid Groups_ |
35+
| A-TG-8.1 | DESIGN | Each dialect's grammar is a strict superset of core's EBNF (`tangle.ebnf`) | TG-8 | `dialects/*/grammar.ebnf` |
36+
| A-TG-8.2 | DESIGN | Each dialect's typing rules are additive (new constructors + their typing rules only; no modification of existing rules) | TG-8 | Per-dialect spec |
37+
| A-TG-9.1 | DESIGN | `tangle-lsp` reuses `compiler/lib/typecheck.ml` as the diagnostic engine (no LSP-only diagnostics) | TG-9 | `compiler/tangle-lsp/src/` |
38+
39+
---
40+
41+
## How to use this file
42+
43+
- **Reading code.** When you see a function whose correctness depends
44+
on something not enforced by the local types — _that's an
45+
assumption_. Find or add the entry here and reference it by ID.
46+
- **Writing a proof.** Every proof obligation in
47+
[PROOF-NARRATIVE.md](PROOF-NARRATIVE.md) names its assumptions by ID.
48+
Before discharging the proof, audit the assumptions block.
49+
- **Modifying load-bearing code.** Each DESIGN assumption names a
50+
file/component. If you edit that file, re-validate the assumption
51+
(or update the obligation if the design changed intentionally).
52+
53+
## Promoting / demoting assumptions
54+
55+
| From | To | Trigger |
56+
|------|-----|---------|
57+
| EMPIRICAL → MATH | discharge with a citation |
58+
| EMPIRICAL → DESIGN | refactor to make it a structural invariant |
59+
| MATH → (delete) | obligation has been re-cast not to need it |
60+
| DESIGN → MATH (rare) | the design happens to encode a known theorem |
61+
62+
When you change a row, leave a one-line note in the changelog with the
63+
date and reason.
64+
65+
---
66+
67+
## Changelog
68+
69+
| Date | Change | By |
70+
|------|--------|-----|
71+
| 2026-06-01 | Initial registry, scoped to Tangle metatheory + implementation refinement obligations | Audit |

‎PROOF-NARRATIVE.md‎

Lines changed: 315 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,315 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0
3+
Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
# Proof Narrative — Tangle
6+
7+
This file is the **single coherent story** of what Tangle proves, what
8+
it assumes, and what it has left to prove.
9+
10+
For the per-obligation checklist with status/prover/effort, see
11+
[PROOF-NEEDS.md](PROOF-NEEDS.md).
12+
For the registry of every load-bearing unproven assumption, see
13+
[ASSUMPTIONS.md](ASSUMPTIONS.md).
14+
15+
---
16+
17+
## 1. Position in the stack
18+
19+
Tangle is the **semantic core** of a four-layer federated stack:
20+
21+
```
22+
┌─────────────────────────────────────────────────────────┐
23+
│ KRL surface language (hyperpolymath/krl) │
24+
└─────────────────┬───────────────────────────────────────┘
25+
│ lowers via KR-1, KR-2 to
26+
▼
27+
┌─────────────────────────────────────────────────────────┐
28+
│ TangleIR (canonical interchange obj) │
29+
└─────────────────┬───────────────────────────────────────┘
30+
│ has semantics via
31+
▼
32+
┌─────────────────────────────────────────────────────────┐
33+
│ Tangle CORE (THIS REPO) │
34+
│ proofs/Tangle.lean — 16 mechanised results │
35+
│ compiler/lib/*.ml — OCaml implementation │
36+
│ compiler/tangle-wasm — WASM backend │
37+
│ compiler/tangle-lsp — LSP server │
38+
│ dialects/ — braid-calculus, quantum-circuit, etc. │
39+
└─────────────────┬───────────────────────────────────────┘
40+
│ persisted/queried via
41+
▼
42+
┌─────────────────────────────────────────────────────────┐
43+
│ Skein.jl + QuandleDB │
44+
└─────────────────────────────────────────────────────────┘
45+
```
46+
47+
Consequence: **Tangle owes a real metatheory.** It owns the type
48+
system that everyone above and below depends on. Tangle.lean already
49+
delivers a substantial slice of this; this document makes the
50+
delivered slice and the remaining gap explicit.
51+
52+
## 2. Proven now
53+
54+
All 16 results live in [`proofs/Tangle.lean`](proofs/Tangle.lean)
55+
(Lean 4, ~560 LoC, no `sorry`, no `axiom`).
56+
57+
### Theorems (the main results)
58+
59+
| ID | Statement | Where |
60+
|----|-----------|-------|
61+
| **T-Progress** | Every well-typed closed term is either a value or can take a step. | `Tangle.lean:247-326` |
62+
| **T-Preservation** | Stepping preserves types: `Γ ⊢ e : τ ∧ e → e' ⟹ Γ ⊢ e' : τ`. | `Tangle.lean:333-415` |
63+
| **T-Determinism** | The step relation is deterministic: `e → e₁ ∧ e → e₂ ⟹ e₁ = e₂`. | `Tangle.lean:422-549` |
64+
| **T-TypeSafety** | Well-typed closed terms never get stuck (Progress + Preservation corollary). | `Tangle.lean:556-558` |
65+
66+
Each is proven for the **let-free fragment** of the core: numerals,
67+
strings, booleans, identity, braid literals, composition, tensor,
68+
pipeline, close, addition, and equality.
69+
70+
### Supporting lemmas
71+
72+
| ID | Statement | Where |
73+
|----|-----------|-------|
74+
| T-ValueNoStep | Values are normal forms: `IsValue e ⟹ ¬ Step e e'`. | `Tangle.lean:189` |
75+
| T-CanonicalNum | A typed-Num value is `.num n` for some `n`. | `Tangle.lean:193-194` |
76+
| T-CanonicalStr | A typed-Str value is `.str s` for some `s`. | `Tangle.lean:197-198` |
77+
| T-CanonicalWord | A typed-Word[n] value is `.identity` (n=0) or `.braidLit gs` (n = width gs). | `Tangle.lean:201-209` |
78+
| T-WidthAppend | `width(gs₁ ++ gs₂) = max(width gs₁, width gs₂)`. | `Tangle.lean:219-221` |
79+
| T-WidthShift | `width(shift gs n) = if gs=[] then 0 else width gs + n`. | `Tangle.lean:235-238` |
80+
| T-FoldlMaxInit (private) | Algebraic identity for the width fold. | `Tangle.lean:212-217` |
81+
| T-FoldlShiftInit (private) | Algebraic identity for the shifted width fold. | `Tangle.lean:223-233` |
82+
83+
### Type-system and step-relation definitions
84+
85+
`Tangle.lean` also defines, as inductive types (so they are
86+
themselves proofs of the form "these are the rules"):
87+
88+
- **`Expr`** — the AST (mirrors `compiler/lib/ast.ml`)
89+
- **`Ty`** — `num`, `str`, `bool`, `word n`
90+
- **`IsValue`** — value predicate
91+
- **`HasType`** — typing judgment, 13 rules (`tNum`, `tStr`, `tBool`,
92+
`tIdentity`, `tBraid`, `tComposeWord`, `tTensorWord`, `tPipeline`,
93+
`tCloseWord`, `tAddNum`, `tEqWord`, `tEqNum`, `tEqStr`)
94+
- **`Step`** — small-step semantics, 26 rules
95+
96+
These are the formal spec the OCaml implementation is meant to refine
97+
(see TG-3 below).
98+
99+
## 3. Remaining obligations (the narrative arc)
100+
101+
What's not yet proven, why it matters, and what assumption each rests on.
102+
103+
### TG-1 — Type safety extended to `let`-binding
104+
105+
**Claim.** Type safety extends to the language fragment with `let`.
106+
107+
**Why valuable.** The header comment of `Tangle.lean` explicitly
108+
parks this: "T-Let: ... a future version can add the full substitution
109+
machinery from e.g. Autosubst." Until then T-TypeSafety is for the
110+
let-free fragment only. `let` is in the surface language (`compiler/
111+
lib/ast.ml`), so users can write programs the proof doesn't cover.
112+
113+
**Assumptions.**
114+
- [[A-TG-1.1]] Capture-avoiding substitution is well-defined on the
115+
de Bruijn representation already used by `HasType`.
116+
- [[A-TG-1.2]] The standard "weakening" and "substitution" lemmas hold
117+
for the existing `HasType` rules.
118+
119+
**How to discharge.** Add the substitution lemma, extend `Step` with
120+
a `let`-reduction rule, extend each cases-on-`hs` block in
121+
preservation. Standard POPLmark machinery; ~150 LoC.
122+
123+
### TG-2 — Decidability of type checking
124+
125+
**Claim.** There is a total function `infer : Expr → Option Ty` such
126+
that `infer e = some τ ↔ HasType [] e τ`.
127+
128+
**Why valuable.** `Tangle.lean` establishes the *relation* `HasType`
129+
but not the *algorithm* `typecheck.ml`. Without TG-2 we have a proven
130+
type system but no proof that the OCaml type checker actually decides
131+
it.
132+
133+
**Assumptions.**
134+
- [[A-TG-2.1]] Type-checking proceeds by syntactic recursion on `Expr`
135+
(no impredicative steps).
136+
- [[A-TG-2.2]] Equality on `Ty` is decidable (it is — `deriving DecidableEq`).
137+
138+
**How to discharge.** Define `infer` in Lean as a structural recursion
139+
on `Expr`. Prove the `↔` by case analysis matching the structure of
140+
`HasType`'s rules.
141+
142+
### TG-3 — OCaml impl refines the Lean spec
143+
144+
**Claim.** For every `e` accepted by `compiler/lib/typecheck.ml` with
145+
type `τ`, the Lean-level proposition `HasType [] e τ` holds (and
146+
conversely).
147+
148+
**Why valuable.** Bridges the metatheory (Lean) to the implementation
149+
(OCaml). Right now we have two systems claiming to be the same; the
150+
claim is unchecked.
151+
152+
**Assumptions.**
153+
- [[A-TG-3.1]] The OCaml AST in `compiler/lib/ast.ml` is in bijection
154+
with the Lean AST in `Tangle.lean`.
155+
- [[A-TG-3.2]] OCaml's `String.equal`, `Int.equal` etc. coincide with
156+
Lean's notions on the values used.
157+
158+
**How to discharge.** Two routes:
159+
1. _Translation validation._ Generate Lean witnesses from OCaml's
160+
typecheck results on a test corpus. Cheap but only empirical.
161+
2. _Refinement._ Mechanise the OCaml algorithm in Lean and prove
162+
equivalence to `HasType`. Expensive but airtight.
163+
164+
### TG-4 — Pretty-print/parse round-trip
165+
166+
**Claim.** `parse(pretty e) = e` for every closed value `e`.
167+
168+
**Why valuable.** Free fuzz oracle. Also the foundation of any "IR
169+
viewer" tooling that re-parses what `pretty` emitted.
170+
171+
**Assumptions.**
172+
- [[A-TG-4.1]] `pretty.ml`'s bracketing is unambiguous w.r.t. the
173+
grammar.
174+
- [[A-TG-4.2]] Lexer never strips information needed by the parser
175+
(e.g. whitespace within braid literals).
176+
177+
**How to discharge.** Property test in `compiler/test/`.
178+
179+
### TG-5 — `compositional.ml` rewriter preserves types
180+
181+
**Claim.** Every rewrite in `compiler/lib/compositional.ml` (418 LoC)
182+
preserves typing: `Γ ⊢ e : τ ∧ e ↝ e' ⟹ Γ ⊢ e' : τ`.
183+
184+
**Why valuable.** That file has zero test coverage (see [B6] in the
185+
bug audit) and is a high-blast-radius refactor target. Type
186+
preservation is the cheapest soundness contract.
187+
188+
**Assumptions.**
189+
- [[A-TG-5.1]] Each rewrite is a function from `Expr` to `Expr` —
190+
no in-place mutation.
191+
- [[A-TG-5.2]] No rewrite introduces a new free variable.
192+
193+
**How to discharge.** First, add a test file
194+
(`compiler/test/compositional_test.ml`) covering each rewrite.
195+
Then add Lean-level rewrite-preservation lemmas, one per rewrite,
196+
in a new file `proofs/Compositional.lean` parameterised on
197+
`Tangle.lean`'s `HasType`.
198+
199+
### TG-6 — WASM compilation preserves semantics
200+
201+
**Claim.** For every closed well-typed `e`, the source-level
202+
evaluation of `e` and the WASM execution of `compile_to_wasm(e)`
203+
agree on the observable result.
204+
205+
**Why valuable.** The *compiler correctness* theorem. Warranted because
206+
Tangle claims structural reasoning means *something* on the runtime.
207+
Without this, Tangle's wasm backend is "trust us, the structure
208+
survives."
209+
210+
**Assumptions.**
211+
- [[A-TG-6.1]] Standard WASM semantics (assumed; specified by Wasm
212+
Cert / Wasm spec).
213+
- [[A-TG-6.2]] No floating-point non-determinism in the source
214+
semantics (Tangle has only Int currently).
215+
216+
**How to discharge.** Bisimulation between OCaml `eval` and the WASM
217+
small-step. Heavy — this is the high-value research-paper-grade slice
218+
(see typed-wasm proof debt in the estate).
219+
220+
### TG-7 — Braid-axiom equality in `eqBraids`
221+
222+
**Claim.** `Step.eqBraids` should decide *braid-group equivalence*,
223+
not list equivalence. I.e., `σ_i σ_j σ_i = σ_j σ_i σ_j when |i-j|=1`
224+
and `σ_i σ_j = σ_j σ_i when |i-j|≥2` should be decidable in finite
225+
generators.
226+
227+
**Why valuable.** The README claims "program equivalence is defined
228+
by isotopy." Currently `eqBraids` only checks list equality, so
229+
`σ_1 σ_2 σ_1` and `σ_2 σ_1 σ_2` are reported unequal. That's the
230+
trivial reading.
231+
232+
**Status.** Current `eqBraids` is a soundness floor (if equal lists
233+
then equal braids), not a completeness ceiling. Promoting it to
234+
braid-group equivalence is a research-grade extension.
235+
236+
**Assumptions.**
237+
- [[A-TG-7.1]] Word problem in the braid group is solvable in
238+
polynomial time on finitely many strands (Birman–Ko–Lee /
239+
Garside-normal-form algorithm — known true).
240+
241+
**How to discharge.** Implement Birman–Ko–Lee normal form;
242+
re-prove `Step.eqBraids` against the normal form.
243+
244+
### TG-8 — Dialect conservativity
245+
246+
**Claim.** Each dialect under `dialects/`
247+
(`braid-calculus`, `quantum-circuit`, `skein-algebra`, `string-diagram`,
248+
`virtual-knot`) is a **conservative extension** of core Tangle: any
249+
core program embedded into the dialect typechecks iff it typechecked
250+
in core.
251+
252+
**Why valuable.** Lets dialect work proceed without re-proving safety
253+
each time. Also stops dialect-introduced ambiguities from quietly
254+
weakening core soundness.
255+
256+
**Assumptions.**
257+
- [[A-TG-8.1]] Each dialect's grammar is a strict superset of core's
258+
EBNF.
259+
- [[A-TG-8.2]] Each dialect's typing rules are *additive* — they only
260+
add new constructors and their typing rules, never modify existing
261+
ones.
262+
263+
**How to discharge.** Per dialect: define `HasType_dialect` in Lean as
264+
`HasType` plus new rules; prove embedding preservation.
265+
266+
### TG-9 — LSP diagnostics ⊆ `HasType` failures
267+
268+
**Claim.** Every diagnostic emitted by `tangle-lsp` corresponds to a
269+
failure of the `HasType` judgment in `Tangle.lean`. (No
270+
LSP-only diagnostics that the spec doesn't reject.)
271+
272+
**Why valuable.** Stops IDE drift from the language definition.
273+
Without it, users get red squigglies in the editor for things that
274+
compile, or vice versa.
275+
276+
**Assumptions.**
277+
- [[A-TG-9.1]] `tangle-lsp` shares the OCaml `typecheck.ml` as its
278+
diagnostic engine (true by construction; verify after each refactor).
279+
280+
**How to discharge.** Audit `tangle-lsp/src/` for any
281+
LSP-only diagnostic emission; route everything through `typecheck.ml`.
282+
Single-PR scope.
283+
284+
## 4. The "stupid proof" exclusions
285+
286+
For completeness, we explicitly do **not** pursue:
287+
288+
- _"`Expr` has exactly these constructors"_ — enforced by the inductive
289+
definition.
290+
- _"Compose is left-associative"_ — surface syntax decision, not a
291+
semantic claim.
292+
- _"`compile_to_wasm` returns a Vec<u8>"_ — Rust type assertion.
293+
- _"`generatorWidth (g :: gs) ≥ g.idx + 1`"_ — implied by T-WidthAppend
294+
+ cons semantics, no extra proof gains anything.
295+
296+
## 5. How to add a new obligation
297+
298+
1. Add a row to [PROOF-NEEDS.md](PROOF-NEEDS.md) with `TG-N` id,
299+
category, prover, priority, effort.
300+
2. Add the narrative entry here with statement, _why valuable_,
301+
status, **assumptions**, _how to discharge_. Assumptions block
302+
is non-optional.
303+
3. Each new assumption gets an entry in [ASSUMPTIONS.md](ASSUMPTIONS.md)
304+
with `A-TG-N.M` id and MATH/DESIGN/EMPIRICAL/CRYPTO classification.
305+
306+
## 6. References
307+
308+
- Implementation: [`compiler/lib/`](compiler/lib/) (OCaml, 2649 LoC).
309+
- Formal core: [`proofs/Tangle.lean`](proofs/Tangle.lean) (Lean 4,
310+
560 LoC, all `Qed`).
311+
- Spec: [`docs/spec/FORMAL-SEMANTICS.md`](docs/spec/FORMAL-SEMANTICS.md).
312+
- Decisions: [`docs/spec/DECISIONS-LOCKED.md`](docs/spec/DECISIONS-LOCKED.md).
313+
- Companion narratives:
314+
- `hyperpolymath/krl/PROOF-NARRATIVE.md` — surface-language obligations
315+
- `hyperpolymath/quandledb/PROOF-NARRATIVE.md` — quandle / DB proofs

0 commit comments

Comments
 (0)