diff --git a/.github/workflows/lean-proofs.yml b/.github/workflows/lean-proofs.yml index 57908b0..03982e2 100644 --- a/.github/workflows/lean-proofs.yml +++ b/.github/workflows/lean-proofs.yml @@ -74,7 +74,15 @@ jobs: set -euo pipefail banned_count=0 for pat in '\bsorry\b' '\baxiom\b' '\badmit\b' '\bAdmitted\b'; do - matches=$(grep -nE "$pat" Tangle.lean | grep -vE "^\s*--|^\s*/--|/-" || true) + # NB the comment filter must account for grep -n's ":" prefix. + # The previous pattern anchored on "^\s*--", which could NEVER match + # once -n had prepended "178:" — so the documented "outside comments" + # exemption was dead, and only the unanchored "/-" alternative + # excluded anything. It went unnoticed purely because no comment had + # yet contained one of these words; the TG-7 trusted-base note does. + # Anchoring after the prefix restores the intended behaviour and is + # STRICTER than the old unanchored "/-" catch-all. + matches=$(grep -nE "$pat" Tangle.lean | grep -vE "^[0-9]+:[[:space:]]*(--|/--|/-)" || true) if [ -n "$matches" ]; then echo "::error::Forbidden token matching '$pat' in Tangle.lean:" echo "$matches" diff --git a/.github/workflows/ocaml-ci.yml b/.github/workflows/ocaml-ci.yml new file mode 100644 index 0000000..9d9a87c --- /dev/null +++ b/.github/workflows/ocaml-ci.yml @@ -0,0 +1,111 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# OCaml compiler build + test gate. +# +# ── Why this exists ──────────────────────────────────────────────────────── +# Until 2026-07-29 the OCaml compiler — the lexer, parser, typechecker and +# interpreter, plus a test suite of well over 4,000 assertions (TG-3 1008, +# TG-5 189, TG-7 2220, TG-8 2311, and the parser/typecheck/eval/e2e/property/ +# round-trip suites) — was **not built or run by CI at all**. Only the Lean +# proofs were gated. A semantics change to `eval.ml` could therefore land +# fully green with nothing having compiled it. +# +# That gap was found while implementing the TG-7 ruling (#50), which changes +# what `==` MEANS on braids. A change of that weight must be gated, so this +# workflow makes `dune build` + `dune test` the oracle: any PR that breaks the +# compiler or a single assertion fails here rather than landing silently. +# +# ── Toolchain choice ─────────────────────────────────────────────────────── +# Debian/Ubuntu packages (`ocaml-dune`, `menhir`) rather than an OCaml setup +# ACTION, deliberately: it adds no new third-party action pin to the estate's +# allowlist, and no pin that can later become unresolvable — the failure mode +# that produces a workflow with NO check run at all. + +name: OCaml CI + +on: + push: + branches: [main] + paths: + - 'compiler/**' + - '.github/workflows/ocaml-ci.yml' + pull_request: + paths: + - 'compiler/**' + - '.github/workflows/ocaml-ci.yml' + workflow_dispatch: {} + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + build-and-test: + name: Build + test the OCaml compiler + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + - name: Install OCaml toolchain + run: | + set -euo pipefail + sudo apt-get update -qq + sudo apt-get install -y --no-install-recommends ocaml ocaml-dune menhir + ocaml -version + dune --version + menhir --version + + - name: Build + working-directory: compiler + run: dune build + + - name: Test + working-directory: compiler + run: | + set -euo pipefail + # `dune test` exits non-zero if any suite fails. Also fail on any + # "FAIL" line: several suites print their own tally and would + # otherwise report failures while still exiting 0. + dune test --force 2>&1 | tee /tmp/dune-test.log + # Match a FAIL *marker* only: "FAIL" followed by ':' or whitespace. + # NOT case-insensitive, and NOT bare "FAIL" — several suites print a + # "Failed: 0" tally, which a looser pattern flags as a failure. (It + # did: this gate's first run went red on a suite reporting zero + # failures. A gate that cries wolf is worse than no gate.) + if grep -qE '^[[:space:]]*FAIL([:[:space:]])' /tmp/dune-test.log; then + echo "::error::A test reported FAIL — see the log above." + grep -nE '^[[:space:]]*FAIL([:[:space:]])' /tmp/dune-test.log | head -20 + exit 1 + fi + # Nonzero tallies, in either shape the suites use. + if grep -qE '([1-9][0-9]*) failed|Failed:[[:space:]]*[1-9]' /tmp/dune-test.log; then + echo "::error::A suite reported a nonzero failure count." + grep -nE '([1-9][0-9]*) failed|Failed:[[:space:]]*[1-9]' /tmp/dune-test.log + exit 1 + fi + echo "OCaml compiler: build + all suites GREEN." + + - name: TG-7 semantics guard + working-directory: compiler + run: | + set -euo pipefail + # The TG-7 ruling (#50) is only real if `==` actually decides + # braid-group equality. These cases are FALSE under list equality, + # so their presence and passing is what distinguishes the two + # semantics — guard against a silent revert. + missing=0 + for t in "braid relation s1.s2.s1 == s2.s1.s2" \ + "far commutation s1.s3 == s3.s1" \ + "non-equivalent braids still compare false"; do + grep -qF "$t" test/test_eval.ml || { echo "::error::TG-7 test missing: $t"; missing=1; } + done + [ "$missing" -eq 0 ] || exit 1 + echo "TG-7 semantics tests present." diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md index 9a9e779..1ab64a3 100644 --- a/ASSUMPTIONS.md +++ b/ASSUMPTIONS.md @@ -32,6 +32,7 @@ Cross-references use `[[A-TG-N.M]]` syntax, resolved here. | 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 | | 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` | | 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_ | +| A-TG-7.2 | IMPL | `braidEquiv` (`proofs/Tangle.lean`) and `braid_equiv.ml` implement Dehornoy handle reduction **correctly**, and agree with each other. Since the 2026-07-29 ruling (#50) routed `==` through them, this is **load-bearing for the semantics of `==`**: the Step relation's metatheory is proven only *relative to* `braidEquiv`, never that it decides braid-group equality. Evidenced by testing (2220 + 8 assertions), not proof. Retired by the mechanised Garside/Dehornoy proof (#51, research-grade). The Lean port is additionally **fuel-bounded**, so termination is assumed rather than proven. | TG-7 | `compiler/lib/braid_equiv.ml`; `proofs/Tangle.lean` §BRAID-GROUP EQUIVALENCE; `compiler/test/tg7` | | A-TG-8.1 | DESIGN | Each dialect's grammar is a strict superset of core's EBNF (`tangle.ebnf`) | TG-8 | `dialects/*/grammar.ebnf` | | 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 | | A-TG-9.1 | DESIGN | `tangle-lsp` emits diagnostics in four documented categories (`PARSE_ERROR`, `MISSPELLING_HINT`, `STRUCTURAL_HINT`, `NAME_HINT`); only `PARSE_ERROR` corresponds to a grammar-level rejection. The other three are LSP-only by design (Option B from TG-9 audit; Option A — full refinement via FFI to `typecheck.ml` — remains queued at #28). Each emission site is tagged in the `Diagnostic.source` field as `tangle-lsp[CATEGORY]`. | TG-9 | `compiler/tangle-lsp/src/backend.rs`; `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md` | diff --git a/PROOF-NARRATIVE.md b/PROOF-NARRATIVE.md index a8a7d0e..87c5a1a 100644 --- a/PROOF-NARRATIVE.md +++ b/PROOF-NARRATIVE.md @@ -413,17 +413,56 @@ by isotopy." Currently `eqBraids` only checks list equality, so `σ_1 σ_2 σ_1` and `σ_2 σ_1 σ_2` are reported unequal. That's the trivial reading. -**Status.** Current `eqBraids` is a soundness floor (if equal lists -then equal braids), not a completeness ceiling. Promoting it to -braid-group equivalence is a research-grade extension. +**Status — LANDED 2026-07-29 (owner ruling #50), with a stated trusted base.** +`==` on braids now decides braid-group equivalence in both engines: + +- **OCaml** — `eval.ml` `Eq` (and `Isotopy`, which for braids denotes the + *same* relation) route through `compiler/lib/braid_equiv.ml` (Dehornoy + handle reduction). `Identity` is `VBraid []`, so identity comparisons flow + through the same case. +- **Lean** — `Step.eqBraids` / `eqIdBraid` / `eqBraidId`, and the three + `echoEq` counterparts, use `braidEquiv` / `isTrivialBraid`: a faithful + in-Lean port of the same procedure, in §BRAID-GROUP EQUIVALENCE of + `Tangle.lean`. + +`σ₁σ₂σ₁ == σ₂σ₁σ₂` is now `true`, which is what the README's "equivalence is +defined by isotopy" always claimed. Progress / Preservation / Determinism were +re-verified **unchanged** — all three need only that the right-hand side is a +*total function into `Bool`*, which `braidEquiv` is; Determinism in particular +is immediate, since a function applied to fixed arguments yields a fixed result. + +> ### ⚠ TRUSTED, NOT PROVEN — the honest boundary +> `braidEquiv` is a **definition**, not an axiom: nothing is postulated, and +> the sorry/axiom gate passes legitimately. But **the gate passing does NOT +> mean this claim is proven.** What is established is that the metatheory +> holds *relative to* `braidEquiv`. What is **not** established is that +> `braidEquiv` correctly **decides** braid-group equality — that is the +> mechanised Garside/Dehornoy correctness proof, which remains research-grade +> and out of scope (#51). +> +> Correctness is currently evidenced **by testing only**: `compiler/test/tg7` +> (2220 assertions — defining relations, 400 constructed-equivalent pairs, +> invariant-distinguished negatives) plus 8 semantics-distinguishing cases in +> `test_eval.ml`. Testing is not proof. +> +> Termination in the Lean port is by an explicit **fuel** bound mirroring the +> OCaml `max_steps`, not by a well-founded measure. Dehornoy reduction does +> terminate, but proving that *is* the research obligation above; fuel keeps +> the definitions total without smuggling in an unproven termination claim. **Assumptions.** - [[A-TG-7.1]] Word problem in the braid group is solvable in polynomial time on finitely many strands (Birman–Ko–Lee / Garside-normal-form algorithm — known true). - -**How to discharge.** Implement Birman–Ko–Lee normal form; -re-prove `Step.eqBraids` against the normal form. +- [[A-TG-7.2]] `braidEquiv` (Lean) and `braid_equiv.ml` (OCaml) implement + Dehornoy handle reduction *correctly*, and agree with each other. Evidenced + by testing, not proof. **This is the load-bearing unproven assumption of + TG-7.** + +**How to discharge the remainder.** Mechanise the Dehornoy correctness +argument (or a Birman–Ko–Lee normal form) in Lean, prove `braidEquiv u v = +true ↔ u ≡ v` in the braid group, and prove termination to replace the fuel +bound. That retires [[A-TG-7.2]]. ### TG-8 — Dialect conservativity diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 4e79c6b..72e8f23 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -59,7 +59,7 @@ Cross-referenced to [PROOF-NARRATIVE.md §3](PROOF-NARRATIVE.md#3-remaining-obli | TG-4 | Pretty-print/parse round-trip on closed values | INV | OCaml property test (cheap) | P2 | 4h | **LANDED** (PR #46 — OCaml property test in `compiler/test/test_roundtrip.ml`, 26-entry corpus including 8 echo/product constructors; 52 round-trip runs) | | TG-5 | `compositional.ml` (418 LoC) rewriter preserves types | TP | OCaml property test | P2 | — | **LANDED** (`compiler/test/tg5/tg5_invariants.ml`, 189 assertions in `dune runtest`). compositional is below the Ty layer, so "preserves types" = preserves the PD-lowering structural invariants + echo residue-recovery: `OpenWord`/`ClosedDiagram`/`EchoClosed` each pinned (closedness, `\|crossings\|`=unit-length, source unit-expanded, **verbatim residue** for `EchoClose` with `expand(residue)=diagram word` and echo-diagram pdv1-identical to plain `close`), error paths, count pins. Lean IR model = optional later rung | | TG-6 | WASM compilation preserves semantics (source eval ≡ wasm exec) | TP / ALG | differential + Lean bisimulation | P1 | — | **RUNG LANDED (differential)**: `compiler/tangle-wasm/tests/differential.rs` EXECUTES the generated wasm with the `wasmi` interpreter (dev-dep) and checks the braid strand-permutation equals an independent reference model (trefoil, non-commuting pairs, braid-relation pairs, 5-strand weave). Validates codegen vs the permutation semantics; not a cross-binary diff against `eval.ml`, and Markov helpers untested. Full source↔wasm bisimulation (WasmCert) remains research-grade | -| TG-7 | `Step.eqBraids` decides braid-group equivalence (not list equality) | ALG / DOM | OCaml + Lean 4 | P2 | — | **RUNG LANDED (non-semantic)**: `compiler/lib/braid_equiv.ml` decides braid-group equivalence via Dehornoy handle reduction, out-of-band (leaves `==`/`Step.eqBraids` as list equality). Tested (`compiler/test/tg7`, 2220 assertions: defining relations + 400 constructed-equivalent pairs + invariant-distinguished negatives). **Still OWNER-GATED**: whether to route `==` through it (a semantics change to eval.ml + Lean Step + proofs) is a language-design decision; Lean correctness (Garside/Dehornoy) remains research-grade | +| TG-7 | `Step.eqBraids` decides braid-group equivalence (not list equality) | ALG / DOM | OCaml + Lean 4 | P2 | — | **SEMANTICS LANDED 2026-07-29** (owner ruling #50 → (a) true braid-group equivalence). `==` on braids now decides braid-group equality in BOTH engines: OCaml `eval.ml` `Eq`/`Isotopy` route through `compiler/lib/braid_equiv.ml`; Lean `Step.eqBraids`/`eqIdBraid`/`eqBraidId` (and the three `echoEq` counterparts) use `braidEquiv`, a faithful in-Lean port of the same Dehornoy procedure. Progress/Preservation/Determinism re-verified unchanged (they need only a total function into `Bool`). Tested: `compiler/test/tg7` 2220 assertions + 8 new semantics-distinguishing cases in `test_eval.ml`. **Remaining (research-grade): the mechanised Garside/Dehornoy correctness proof — `braidEquiv` is TRUSTED, NOT PROVEN; the Step relation is proven only RELATIVE to it** | | TG-8 | Each dialect (braid-calculus, quantum-circuit, skein-algebra, string-diagram, virtual-knot) is a conservative extension of core | TP | OCaml model + Lean per-dialect | P3 | — | **TEMPLATE LANDED (virtual-knot)**: `compiler/lib/dialect_vk.ml` models VBₙ ⊃ Bₙ as core + a virtual layer that DELEGATES to `Braid_equiv` on the real fragment, so conservativity holds by construction; `compiler/test/tg8` (2311 assertions) verifies faithful embedding, core-delegation, invariant agreement, proper extension, virtual involution, honest undecided-frontier. Remaining: surface-syntax parser integration, the other 4 dialects (replicate the template), and a Lean conservativity proof | | TG-9 | LSP diagnostics are a subset of `HasType` failures (no LSP-only diagnostics) | INV | Audit + refactor | P2 | — | **LANDED** (`tangle-lsp` delegates all diagnostics to `tanglec --check` ⇒ `compiler/lib/check.ml`; hand-rolled LSP-only false positives removed. Subset holds by construction. Tests: `test_check.ml` + tangle-lsp unit/delegation tests) | | TG-10 | Echo-types integrated into the type system: `Echo[ρ,τ]` former + `echoClose`/`lower`/`residue`/`echoAdd`/`echoEq` + product type (`pair`/`fst`/`snd`), with Progress/Preservation/Determinism/TypeSafety extended to cover them and the non-injectivity / residue-recovery capstones proven | TP / DOM | Lean 4 | P1 | — | **LANDED** (`proofs/Tangle.lean` §ECHO-TYPES) | @@ -73,10 +73,11 @@ Concrete approach, effort, risk, and dependencies for what is left after TG-0/1/2/3/4/5/9/10 landed. **Landable rungs of TG-6, TG-7, and TG-8 also landed** (2026-06-14): TG-6 a `wasmi` differential test; TG-7 an out-of-band `braid_equiv` checker; TG-8 a virtual-knot conservative-extension template. What -genuinely remains is **owner-gated or research-grade**: TG-7's *semantics -change* (decision); TG-8's *surface-syntax integration + other 4 dialects + -Lean conservativity proof*; TG-6's *full source↔wasm bisimulation* and TG-7's -*Lean correctness proof*. +genuinely remains is **research-grade**: TG-8's *surface-syntax integration + +other 4 dialects + Lean conservativity proof*; TG-6's *full source↔wasm +bisimulation*; and TG-7's *Lean correctness proof*. (TG-7's **semantics +change is no longer owner-gated — it was ruled and landed 2026-07-29**, see +#50 and the TG-7 row above.) ### TG-3 — OCaml `typecheck.ml` refines Lean `HasType` — ✅ **LANDED 2026-06-14** - **Key lever (used):** TG-2 proves Lean `infer ≡ HasType`, so refinement diff --git a/compiler/lib/braid_equiv.ml b/compiler/lib/braid_equiv.ml index df8dd90..53a2755 100644 --- a/compiler/lib/braid_equiv.ml +++ b/compiler/lib/braid_equiv.ml @@ -2,12 +2,16 @@ (* braid_equiv.ml — decide braid-GROUP equivalence of braid words via Dehornoy * handle reduction. * - * TG-7, NON-SEMANTIC rung. The language's `==` on braids (eval.ml `VBraid` - * equality and the Lean `Step.eqBraids` rule) is LIST equality and is left - * UNCHANGED by this module — `braid_equiv` is an out-of-band decision procedure - * for callers who want true braid-group equivalence (e.g. tooling, future - * `compute`-style checks). Changing `==` itself to use this is a separate - * language-design decision (see PROOF-NEEDS.md TG-7). + * TG-7, SEMANTIC rung as of 2026-07-29. Owner ruling tangle#50 settled the + * open question in favour of true braid-group equivalence: the language's `==` + * on braids (eval.ml `Eq` on `VBraid`, and the Lean `Step.eqBraids` rule via + * `braidEquiv`) now DECIDES braid-group equality, not list equality. `~` + * (isotopy) routes here too — for braids, isotopy IS equality in the braid + * group, so the two must agree. + * + * Rationale: syntactic equality contradicts the language's own thesis, that + * programs are topological objects and equivalence is isotopy. `==` must not + * be the one place that quietly reverts to comparing representations. * * Algorithm (Dehornoy 1997, "A fast method for comparing braids"). A braid * word on σ₁,σ₂,… A σᵢ-handle is a factor diff --git a/compiler/lib/braid_equiv.mli b/compiler/lib/braid_equiv.mli index d85060e..a726156 100644 --- a/compiler/lib/braid_equiv.mli +++ b/compiler/lib/braid_equiv.mli @@ -1,9 +1,9 @@ (* SPDX-License-Identifier: MPL-2.0 *) -(* braid_equiv.mli — out-of-band braid-GROUP equivalence (TG-7, non-semantic). +(* braid_equiv.mli — braid-GROUP equivalence (TG-7; the semantics of `==`). * - * Decides braid-group equality via Dehornoy handle reduction. This does NOT - * change the language's `==` on braids (eval.ml / Lean Step keep list equality); - * it is a separate decision procedure for callers wanting true equivalence. *) + * Decides braid-group equality via Dehornoy handle reduction. As of the + * owner ruling tangle#50 (2026-07-29) this IS the language's `==` on braids + * (eval.ml `Eq`, Lean `Step.eqBraids` via `braidEquiv`), and `~` too. *) (** A braid word as unit letters (index >= 1, sign +/-1). *) type letter = { idx : int; sgn : int } diff --git a/compiler/lib/eval.ml b/compiler/lib/eval.ml index dc742a8..f53cf83 100644 --- a/compiler/lib/eval.ml +++ b/compiler/lib/eval.ml @@ -121,6 +121,17 @@ let gen_of_ast (g : generator) : gen = let gens_of_ast (gs : generator list) : gen list = List.map gen_of_ast gs +(** Convert a runtime generator back to an AST generator. The two records are + structurally identical but nominally distinct; [Braid_equiv] is written + against the AST type, so the braid-equivalence used by `==` and `~` (TG-7) + needs this direction too. *) +let ast_of_gen (g : gen) : generator = + { gen_index = g.g_index; gen_exponent = g.g_exponent } + +(** Convert a list of runtime generators to AST generators. *) +let ast_of_gens (gs : gen list) : generator list = + List.map ast_of_gen gs + (** Compute the width (number of strands) of a braid word. * width = max(index + 1) over all generators, or 0 if empty. *) @@ -575,28 +586,53 @@ and eval_binop (op : binop) (v1 : value) (v2 : value) : value = | _ -> eval_error "Cannot divide %s by %s" (pp_value v1) (pp_value v2) end - (* Equality: structural comparison *) + (* Equality. Scalars compare structurally; BRAIDS compare up to braid-GROUP + equivalence (TG-7, owner ruling tangle#50). Syntactic equality would + contradict the language's own thesis — programs are topological objects and + equivalence is isotopy — so `==` must not be the one place that quietly + reverts to comparing representations. Mirrored by the Lean `Step.eqBraids` + rule, which uses `braidEquiv`. + + `Identity` evaluates to `VBraid []`, so identity comparisons flow through + this same case and correctly ask "is this word trivial?". + + Correctness of the decision procedure is established by testing + (compiler/test/tg7), NOT by proof — see braid_equiv.ml and + PROOF-NARRATIVE.md §TG-7. *) | Eq -> begin match v1, v2 with | VInt a, VInt b -> VBool (a = b) | VFloat a, VFloat b -> VBool (a = b) | VBool a, VBool b -> VBool (a = b) | VString a, VString b -> VBool (a = b) - | VBraid g1, VBraid g2 -> VBool (g1 = g2) + | VBraid g1, VBraid g2 -> VBool (Braid_equiv.equiv (ast_of_gens g1) (ast_of_gens g2)) | _ -> eval_error "Cannot compare %s == %s" (pp_value v1) (pp_value v2) end - (* Isotopy: compare simplified braid words *) + (* Isotopy. For BRAIDS, isotopy IS equality in the braid group, so `~` and + `==` denote the same relation and must agree. This previously compared + `simplify_gens`, which only cancels adjacent inverses (Reidemeister II) and + does not implement the braid relation σᵢσⱼσᵢ = σⱼσᵢσⱼ — an incomplete + decision procedure. Leaving it that way while `==` became complete would + have made `a == b` provable with `a ~ b` false, which is incoherent. This + is therefore a COMPLETENESS fix, not a change of intended meaning. + + CAVEAT for closed tangles: isotopy of a LINK (the closure of a braid) is + Markov equivalence — braid-group equality plus conjugation and + stabilisation. Those moves are NOT implemented. Braid equality is + sufficient but not necessary for closures to be isotopic, so on + `tv_closed` tangles this remains a SOUND but INCOMPLETE under-approximation: + `true` is trustworthy, `false` only means "not equal as braids". *) | Isotopy -> begin match v1, v2 with | VBraid g1, VBraid g2 -> - VBool (simplify_gens g1 = simplify_gens g2) + VBool (Braid_equiv.equiv (ast_of_gens g1) (ast_of_gens g2)) | VTangle t1, VTangle t2 -> - VBool (simplify_gens t1.tv_word = simplify_gens t2.tv_word) + VBool (Braid_equiv.equiv (ast_of_gens t1.tv_word) (ast_of_gens t2.tv_word)) | VBraid g1, VTangle t2 -> - VBool (simplify_gens g1 = simplify_gens t2.tv_word) + VBool (Braid_equiv.equiv (ast_of_gens g1) (ast_of_gens t2.tv_word)) | VTangle t1, VBraid g2 -> - VBool (simplify_gens t1.tv_word = simplify_gens g2) + VBool (Braid_equiv.equiv (ast_of_gens t1.tv_word) (ast_of_gens g2)) | _ -> eval_error "Cannot test isotopy of %s ~ %s" (pp_value v1) (pp_value v2) end diff --git a/compiler/test/test_eval.ml b/compiler/test/test_eval.ml index 17f2c25..5ed37f0 100644 --- a/compiler/test/test_eval.ml +++ b/compiler/test/test_eval.ml @@ -594,7 +594,61 @@ let test_equality () = eval (BinOp (Isotopy, BraidLit [sigma 1], BraidLit [sigma 2])) - = VBool false) + = VBool false); + + (* ---------------------------------------------------------------- *) + (* TG-7 (tangle#50): `==` decides braid-GROUP equivalence, NOT list *) + (* equality. Every case below is FALSE under list equality and TRUE *) + (* under the ruling, so these are the tests that actually distinguish *) + (* the two semantics — the pre-existing cases above pass either way. *) + (* ---------------------------------------------------------------- *) + + test "TG-7: braid relation s1.s2.s1 == s2.s1.s2" (fun () -> + (* The defining braid relation. Distinct words, same group element. *) + eval (BinOp (Eq, + BraidLit [sigma 1; sigma 2; sigma 1], + BraidLit [sigma 2; sigma 1; sigma 2])) + = VBool true); + + test "TG-7: far commutation s1.s3 == s3.s1" (fun () -> + (* |i - j| >= 2 generators commute. *) + eval (BinOp (Eq, + BraidLit [sigma 1; sigma 3], + BraidLit [sigma 3; sigma 1])) + = VBool true); + + test "TG-7: free cancellation s1.s1^-1 == identity" (fun () -> + eval (BinOp (Eq, BraidLit [sigma 1; sigma_inv 1], Identity)) = VBool true); + + test "TG-7: identity == s1.s1^-1 (symmetric)" (fun () -> + eval (BinOp (Eq, Identity, BraidLit [sigma 1; sigma_inv 1])) = VBool true); + + test "TG-7: non-equivalent braids still compare false" (fun () -> + (* Guards against a decision procedure that says `true` for everything — + s1 and s1^-1 differ in writhe, so they cannot be equal. *) + eval (BinOp (Eq, BraidLit [sigma 1], BraidLit [sigma_inv 1])) = VBool false); + + test "TG-7: s1.s2 =/= s2.s1 (adjacent gens do NOT commute)" (fun () -> + eval (BinOp (Eq, + BraidLit [sigma 1; sigma 2], + BraidLit [sigma 2; sigma 1])) + = VBool false); + + test "TG-7: `~` agrees with `==` on the braid relation" (fun () -> + (* For braids, isotopy IS braid-group equality; the two operators must + not disagree. `~` previously used free reduction only and returned + false here. *) + eval (BinOp (Isotopy, + BraidLit [sigma 1; sigma 2; sigma 1], + BraidLit [sigma 2; sigma 1; sigma 2])) + = VBool true); + + test "TG-7: echoEq lowers to braid-group equality" (fun () -> + (* echoEq reuses the Eq logic, so it must follow the ruling too. *) + eval (Lower (EchoEq ( + BraidLit [sigma 1; sigma 2; sigma 1], + BraidLit [sigma 2; sigma 1; sigma 2]))) + = VBool true) (* ================================================================== *) (* 11. Error cases *) diff --git a/proofs/Tangle.lean b/proofs/Tangle.lean index 50751cd..8f7195a 100644 --- a/proofs/Tangle.lean +++ b/proofs/Tangle.lean @@ -145,6 +145,135 @@ def generatorWidth (gs : List Generator) : Nat := def shiftGenerators (gs : List Generator) (n : Nat) : List Generator := gs.map fun g => { g with idx := g.idx + n } +-- ═══════════════════════════════════════════════════════════════════════ +-- BRAID-GROUP EQUIVALENCE (TG-7) +-- ═══════════════════════════════════════════════════════════════════════ +-- +-- Owner ruling 2026-07-29 (tangle#50): `==` on braids decides braid-GROUP +-- equivalence, NOT list equality. Syntactic equality contradicts the +-- language's own thesis — programs are topological objects and equivalence is +-- isotopy — so `==` must not be the one place that quietly reverts to +-- comparing representations. +-- +-- This is a faithful port of `compiler/lib/braid_equiv.ml` (Dehornoy 1997, +-- "A fast method for comparing braids"). A σᵢ-handle is a factor +-- σᵢ^e · w₀ · σ_{i+1}^d · w₁ · ⋯ · σ_{i+1}^d · w_m · σᵢ^{-e} +-- whose interior uses only σⱼ with j ≥ i+2 apart from same-sign σ_{i+1}. It +-- reduces to +-- w₀ · (σ_{i+1}^{-e} σᵢ^d σ_{i+1}^e) · w₁ · ⋯ · w_m +-- and a handle-free, freely-reduced word is empty iff the braid is trivial, so +-- equiv u v ⇔ reduce (u · v⁻¹) = ε. +-- +-- ── TRUSTED, NOT PROVEN ──────────────────────────────────────────────── +-- These are DEFINITIONS, not axioms — nothing here is postulated, and the +-- metatheory below (Progress / Preservation / Determinism) goes through for +-- `braidEquiv` exactly as it did for list equality, because all three need +-- only that it is a TOTAL FUNCTION into `Bool`. Determinism in particular is +-- unaffected: a function applied to fixed arguments yields a fixed result. +-- +-- What is NOT established here is that `braidEquiv` DECIDES braid-group +-- equality. That is the mechanised Garside/Dehornoy correctness proof, which +-- is research-grade and explicitly out of scope (tangle#51). Until it exists, +-- `braidEquiv` is trusted code that the `Step` relation is proven *relative +-- to*. The sorry/axiom gate passing does NOT mean this claim is proven; see +-- PROOF-NARRATIVE.md §TG-7. +-- +-- Termination is by an explicit FUEL parameter rather than a well-founded +-- measure, mirroring the OCaml `max_steps` safety bound. Dehornoy reduction +-- does terminate, but proving that is precisely the research-grade obligation +-- above; fuel keeps these definitions total and computable without smuggling +-- in an unproven termination claim. + +/-- A braid word as unit letters: index ≥ 1 and sign ±1. + Mirrors `type letter` in braid_equiv.ml. -/ +structure Letter where + idx : Nat + sgn : Int + deriving DecidableEq, Repr + +/-- Expand generators with arbitrary nonzero exponents into unit letters. -/ +def unitsOf (gs : List Generator) : List Letter := + gs.flatMap fun g => + List.replicate g.exp.natAbs { idx := g.idx, sgn := if g.exp ≥ 0 then 1 else -1 } + +/-- Inverse braid word: reverse order, negate every sign. (ab)⁻¹ = b⁻¹a⁻¹. -/ +def inverseWord (w : List Letter) : List Letter := + (w.map fun l => { l with sgn := -l.sgn }).reverse + +/-- Free reduction: cancel adjacent σ·σ⁻¹. -/ +def freeReduce (w : List Letter) : List Letter := + w.foldr (fun x acc => + match acc with + | y :: rest => if x.idx = y.idx && x.sgn = -y.sgn then rest else x :: acc + | [] => [x]) [] + +/-- Does the letter at the head open a handle over `rest`? Returns the + interior and the tail after the closing letter, or `none`. + Mirrors `handle_at` / the `scan` loop in braid_equiv.ml. -/ +def scanHandle (i : Nat) (e : Int) : + List Letter → Option Int → List Letter → Option (List Letter × List Letter) + | [], _, _ => none -- no close → not a handle + | l :: ls, dOpt, acc => + if l.idx = i then + if l.sgn = -e then some (acc.reverse, ls) -- closes the handle + else none -- same-sign σᵢ → blocked + else if l.idx < i then none -- σ_{ scanHandle i e ls (some l.sgn) (l :: acc) + | some d => if d = l.sgn then scanHandle i e ls dOpt (l :: acc) + else none -- mixed σ_{i+1} signs + else scanHandle i e ls dOpt (l :: acc) -- j ≥ i+2 → interior, ok + +/-- Rewrite a handle's interior: σ_{i+1}^d ↦ σ_{i+1}^{-e} σᵢ^d σ_{i+1}^e. -/ +def rewriteInterior (i : Nat) (e : Int) (interior : List Letter) : List Letter := + interior.flatMap fun l => + if l.idx = i + 1 then + [ { idx := i + 1, sgn := -e }, { idx := i, sgn := l.sgn }, { idx := i + 1, sgn := e } ] + else [l] + +/-- Reduce the leftmost handle; `none` if the word is handle-free. -/ +def reduceOne : List Letter → Option (List Letter) + | [] => none + | l :: ls => + match scanHandle l.idx l.sgn ls none [] with + | some (interior, tail) => some (rewriteInterior l.idx l.sgn interior ++ tail) + | none => + match reduceOne ls with + | some ls' => some (l :: ls') + | none => none + +/-- Default fuel; mirrors `default_max_steps` in braid_equiv.ml. -/ +def defaultFuel : Nat := 1000000 + +/-- Reduce to a handle-free, freely-reduced word (fuel-bounded). -/ +def reduceFuel : Nat → List Letter → List Letter + | 0, w => w -- safety net + | fuel + 1, w => + match reduceOne w with + | none => w + | some w' => reduceFuel fuel (freeReduce w') + +/-- Reduce with the default fuel. -/ +def reduceWord (w : List Letter) : List Letter := + reduceFuel defaultFuel (freeReduce w) + +/-- A unit word is trivial iff it reduces to the empty word. -/ +def isTrivialWord (w : List Letter) : Bool := reduceWord w == [] + +/-- A generator list denotes the trivial (identity) braid. -/ +def isTrivialBraid (gs : List Generator) : Bool := isTrivialWord (unitsOf gs) + +/-- **Braid-group equivalence**: `u ≡ v` iff `u · v⁻¹` is trivial. + This is what `==` on braids means (tangle#50). -/ +def braidEquiv (u v : List Generator) : Bool := + isTrivialWord (unitsOf u ++ inverseWord (unitsOf v)) + +/-- Writhe (exponent sum): invariant under the braid relations. A necessary + condition for equivalence, exposed for testing. -/ +def writhe (gs : List Generator) : Int := + gs.foldl (fun a g => a + g.exp) 0 + -- ═══════════════════════════════════════════════════════════════════════ -- DE BRUIJN SUBSTITUTION MACHINERY -- ═══════════════════════════════════════════════════════════════════════ @@ -333,10 +462,10 @@ inductive Step : Expr → Expr → Prop where | eqRight : IsValue e₁ → Step e₂ e₂' → Step (.eq e₁ e₂) (.eq e₁ e₂') | eqNums : Step (.eq (.num n₁) (.num n₂)) (.boolLit (n₁ == n₂)) | eqStrs : Step (.eq (.str s₁) (.str s₂)) (.boolLit (s₁ == s₂)) - | eqBraids : Step (.eq (.braidLit gs₁) (.braidLit gs₂)) (.boolLit (gs₁ == gs₂)) + | eqBraids : Step (.eq (.braidLit gs₁) (.braidLit gs₂)) (.boolLit (braidEquiv gs₁ gs₂)) | eqIdId : Step (.eq .identity .identity) (.boolLit true) - | eqIdBraid : Step (.eq .identity (.braidLit gs)) (.boolLit (gs == [])) - | eqBraidId : Step (.eq (.braidLit gs) .identity) (.boolLit (gs == [])) + | eqIdBraid : Step (.eq .identity (.braidLit gs)) (.boolLit (isTrivialBraid gs)) + | eqBraidId : Step (.eq (.braidLit gs) .identity) (.boolLit (isTrivialBraid gs)) -- Echo (structured loss): `echoClose` is a redex that reduces into a formed -- echo value `echoVal residue result`; `lower`/`residue` are the two generic -- projections off a formed echo value. `lower` yields the result component @@ -373,13 +502,13 @@ inductive Step : Expr → Expr → Prop where | echoEqStrs : Step (.echoEq (.str s₁) (.str s₂)) (.echoVal (.pair (.str s₁) (.str s₂)) (.boolLit (s₁ == s₂))) | echoEqBraids : Step (.echoEq (.braidLit gs₁) (.braidLit gs₂)) - (.echoVal (.pair (.braidLit gs₁) (.braidLit gs₂)) (.boolLit (gs₁ == gs₂))) + (.echoVal (.pair (.braidLit gs₁) (.braidLit gs₂)) (.boolLit (braidEquiv gs₁ gs₂))) | echoEqIdId : Step (.echoEq .identity .identity) (.echoVal (.pair .identity .identity) (.boolLit true)) | echoEqIdBraid : Step (.echoEq .identity (.braidLit gs)) - (.echoVal (.pair .identity (.braidLit gs)) (.boolLit (gs == []))) + (.echoVal (.pair .identity (.braidLit gs)) (.boolLit (isTrivialBraid gs))) | echoEqBraidId : Step (.echoEq (.braidLit gs) .identity) - (.echoVal (.pair (.braidLit gs) .identity) (.boolLit (gs == []))) + (.echoVal (.pair (.braidLit gs) .identity) (.boolLit (isTrivialBraid gs))) -- Let-binding: congruence on the bound expression, then β-reduction once it -- is a value (the bound value is substituted into the body's variable 0). | letStep : Step e₁ e₁' → Step (.lett e₁ e₂) (.lett e₁' e₂)