diff --git a/.github/workflows/krl-verification.yml b/.github/workflows/krl-verification.yml new file mode 100644 index 0000000..b111b1b --- /dev/null +++ b/.github/workflows/krl-verification.yml @@ -0,0 +1,93 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# +# KRL Verification — runs the self-contained KRL lexer/parser/SQL test suite +# (pure Julia: the `KRL` module pulls in no external packages, so it loads on +# base Julia with no Pkg.instantiate) AND machine-checks the Agda proofs under +# verification/proofs/agda. +# +# Why this exists: `.gitlab-ci.yml` only defines jobs gated on `Cargo.toml` / +# `mix.exs`, neither of which this (Julia + ReScript) repo has — so the Julia +# test suite was never executed by any CI gate. This workflow closes that gap +# so lexer/parser regressions are caught in future. + +name: KRL Verification + +on: + pull_request: + push: + branches: [main, master] + workflow_dispatch: + +# Estate guardrail: cancel superseded runs (read-only checks, safe to cancel). +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + krl-tests: + name: KRL lexer / parser / SQL tests (Julia) + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 + + - name: Install Julia 1.10 + run: | + set -euo pipefail + curl -fsSL https://install.julialang.org -o "$RUNNER_TEMP/juliaup-init.sh" + sh "$RUNNER_TEMP/juliaup-init.sh" --yes --default-channel 1.10 + echo "$HOME/.juliaup/bin" >> "$GITHUB_PATH" + + - name: Julia version + run: julia --version + + - name: Run KRL test suite + run: | + set -e + # Each test file includes ../KRL.jl (or ../Lexer.jl) relative to its + # own location; a top-level @testset throws on failure → non-zero exit. + julia --color=yes server/krl/test/lexer_test.jl + julia --color=yes server/krl/test/parser_test.jl + julia --color=yes server/krl/test/sql_test.jl + + agda-proofs: + name: Agda proofs (--safe) + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4 + + - name: Install Agda + standard library + run: | + set -euo pipefail + sudo apt-get update + sudo apt-get install -y --no-install-recommends agda agda-stdlib + # Ubuntu ships the stdlib source but omits its .agda-lib registration. + printf 'name: standard-library\ninclude: .\n' \ + | sudo tee /usr/share/agda-stdlib/standard-library.agda-lib >/dev/null + mkdir -p "$HOME/.agda" + echo /usr/share/agda-stdlib/standard-library.agda-lib > "$HOME/.agda/libraries" + echo standard-library > "$HOME/.agda/defaults" + # Agda writes interface (.agdai) files into the library's _build dir; + # the apt stdlib is root-owned, so make it writable for the (non-root) + # runner user that invokes `agda`. + sudo chmod -R a+rwX /usr/share/agda-stdlib + + - name: Check Agda proofs under --safe + run: | + set -e + shopt -s nullglob + found=0 + for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do + echo "── agda --safe $f" + # Run from the file's own directory so the top-level module name + # (e.g. `DihedralQuandle`) matches the file name as Agda requires. + ( cd "$(dirname "$f")" && LC_ALL=C.UTF-8 agda --safe "$(basename "$f")" ) + found=1 + done + if [ "$found" = "0" ]; then echo "No Agda proofs found"; exit 1; fi + echo "PASS: all Agda proofs check under --safe" diff --git a/server/krl/Ast.jl b/server/krl/Ast.jl index a7b3112..89ced4e 100644 --- a/server/krl/Ast.jl +++ b/server/krl/Ast.jl @@ -30,7 +30,32 @@ Invariants (checked by the parser, not the AST constructors): """ export KRLNode, KRLStatement, KRLSource, KRLPipeStage, KRLReturnItem, - KRLExpr, KRLPatternNode, KRLType + KRLExpr, KRLPatternNode, KRLType, + # enums + values + ConfidenceLevel, ConfExact, ConfSufficient, ConfNecessary, ConfHeuristic, + SortOrder, SortAsc, SortDesc, + EdgeDir, EdgeForward, EdgeBackward, EdgeUndirected, + # program + statements + KRLProgram, KRLQueryStmt, KRLLetStmt, KRLRuleDef, KRLAxiomDef, + # query + sources + KRLQuery, KRLSourceKnots, KRLSourceDiagrams, KRLSourceInvariants, + KRLSourceNamed, KRLSourceSubquery, + # pipeline stages + KRLFilterStage, KRLSortStage, KRLTakeStage, KRLSkipStage, KRLReturnStage, + KRLGroupByStage, KRLAggregateItem, KRLAggregateStage, KRLFindEquivStage, + KRLFindPathStage, KRLMatchStage, KRLLetStage, KRLWithStage, + # return items + KRLReturnExpr, KRLReturnStar, KRLReturnEquivs, KRLReturnEquivClass, + KRLReturnProof, + # expressions + KRLNullCoalesce, KRLOr, KRLAnd, KRLNot, KRLCompare, KRLBinOp, KRLUnaryNeg, + KRLFieldAccess, KRLCall, KRLIndex, KRLVar, KRLKnotName, KRLInt, KRLFloat, + KRLString, KRLBool, KRLNone, KRLArray, KRLRecord, KRLGaussCode, KRLTypeAnn, + # graph patterns + KRLNodePattern, KRLEdgePattern, KRLGraphPattern, + # type annotations + KRLTyScalar, KRLTyOption, KRLTyList, KRLTySet, KRLTyResultSet, KRLTyEquiv, + KRLTyEquivConf, KRLTyMap, KRLTyTuple, KRLTyNamed # ─── Confidence level ──────────────────────────────────────────────────────── diff --git a/server/krl/Lexer.jl b/server/krl/Lexer.jl index 4eb1f7d..550beac 100644 --- a/server/krl/Lexer.jl +++ b/server/krl/Lexer.jl @@ -15,7 +15,7 @@ Token kinds (Symbol tags): :knot_name — `3_1`, `10_139` (digit `_` digit form) Names: :keyword — reserved word :identifier — user name or invariant name - Operators: :eq (`==`) + Operators: :eq (`==` or bare `=` — see `=` handling below) :neq (`!=`) :lt (`<`) :lte (`<=`) @@ -274,10 +274,17 @@ function tokenise(src::String)::Vector{Token} # ── two-character and single-character operators ────────────────────── if c == '=' + # KRL accepts bare `=` as surface syntax for let-bindings and + # filter equality (grammar.ebnf v0.1.0: `let id = expr`, + # `filter ... = value`). The lexer records the glyph only; + # equality-as-binding vs equality-as-comparison is resolved by + # the parser/typechecker from context, not refused lexically. if peek() == '=' - advance!(); emit(:eq, "==", sl, sc) + advance!(); emit(:eq, "==", sl, sc) # == → :eq + elseif peek() == '>' + advance!(); emit(:fat_arrow, "=>", sl, sc) # => → :fat_arrow else - throw(KRLLexError("bare `=` is not a KRL operator; did you mean `==`?", sl, sc)) + emit(:eq, "=", sl, sc) # = → :eq end continue end @@ -306,12 +313,6 @@ function tokenise(src::String)::Vector{Token} continue end - if c == '=' - if peek() == '>'; advance!(); emit(:fat_arrow, "=>", sl, sc) - else; emit(:eq, "=", sl, sc); end - continue - end - if c == '~' if peek() == '>'; advance!(); emit(:tilde_arrow, "~>", sl, sc) elseif peek() == '='; advance!(); emit(:iso, "~=", sl, sc) diff --git a/server/krl/Parser.jl b/server/krl/Parser.jl index e17da8f..cc430d4 100644 --- a/server/krl/Parser.jl +++ b/server/krl/Parser.jl @@ -488,9 +488,13 @@ end function _parse_find_path_stage(ps::ParserState)::KRLFindPathStage t = _expect!(ps, :keyword, "find_path") - src_e = _parse_expr(ps) + # `~>` is the find_path separator AND a comparison operator (_CMP_KINDS), + # so the operands must be parsed *below* the comparison level — otherwise + # `_parse_expr` greedily absorbs `src ~> tgt` into a single KRLCompare and + # the `~>`/`via` separators are lost. Parse operands at additive level. + src_e = _parse_additive(ps) _expect!(ps, :tilde_arrow) # ~> - tgt = _parse_expr(ps) + tgt = _parse_additive(ps) _expect!(ps, :keyword, "via") method_tok = _peek(ps) (method_tok.kind == :keyword || method_tok.kind == :identifier) || diff --git a/server/krl/SqlFrontend.jl b/server/krl/SqlFrontend.jl index 70a5466..37fe756 100644 --- a/server/krl/SqlFrontend.jl +++ b/server/krl/SqlFrontend.jl @@ -59,10 +59,12 @@ const _SQL_UPPER_KWS = Set([ "JOIN", "INNER", "LEFT", "RIGHT", "ON", "UNION", "ALL", "INSERT", "UPDATE", "DELETE", "CREATE", "ALTER", "GRANT", "REVOKE", + "KNOTS", "DIAGRAMS", "INVARIANTS", # built-in source names → case-insensitive ]) const _SQL_UNSUPPORTED_KWS = Set([ "null", # KRL uses none / Option[τ] + "is", # `IS NULL` — KRL has no NULL "insert", "update", "delete", # QuandleDB is read-only "create", "alter", # schema is fixed "grant", "revoke", # no access control yet @@ -134,6 +136,9 @@ function _parse_sql_query(ps::ParserState)::KRLQuery wtok = _advance!(ps) stages = _check_sql_unsupported_expr(ps, stages) pred = _parse_expr(ps) + # Trailing unsupported constructs the KRL expr grammar doesn't consume, + # e.g. `x IS NULL` (KRL has no NULL). + _check_sql_unsupported_expr(ps, stages) push!(stages, KRLFilterStage(pred, wtok.line, wtok.col)) end @@ -245,6 +250,7 @@ function _check_sql_unsupported_expr(ps::ParserState, stages::Vector) if t.kind == :keyword && t.value in _SQL_UNSUPPORTED_KWS alt = Dict( "null" => "`none` or `Option[τ]`", + "is" => "`none` — KRL has no NULL (Option[τ])", "insert" => "(QuandleDB is read-only; use Skein.jl REPL for mutations)", "update" => "(QuandleDB is read-only; use Skein.jl REPL for mutations)", "delete" => "(QuandleDB is read-only; use Skein.jl REPL for mutations)", diff --git a/server/krl/test/lexer_test.jl b/server/krl/test/lexer_test.jl index b67a28f..eb06aae 100644 --- a/server/krl/test/lexer_test.jl +++ b/server/krl/test/lexer_test.jl @@ -120,7 +120,7 @@ include("../Lexer.jl") @testset "Operators" begin pairs = [ - ("==", :eq), ("!=", :neq), ("<", :lt), ("<=", :lte), + ("==", :eq), ("=", :eq), ("!=", :neq), ("<", :lt), ("<=", :lte), (">", :gt), (">=", :gte), ("+", :plus), ("-", :minus), ("*", :star), ("/", :slash), ("%", :percent), ("|", :pipe), ("->", :arrow), ("=>", :fat_arrow), @@ -152,8 +152,6 @@ include("../Lexer.jl") end @testset "Error cases" begin - # Bare = (not ==) - @test_throws KRLLexError tokenise("=") # Bare ~ (not ~> or ~=) @test_throws KRLLexError tokenise("~") # Bare ? (not ??) diff --git a/server/krl/test/parser_test.jl b/server/krl/test/parser_test.jl index a961c61..b9fd453 100644 --- a/server/krl/test/parser_test.jl +++ b/server/krl/test/parser_test.jl @@ -30,7 +30,7 @@ Innovation under test: using Test include("../KRL.jl") -using .KRL: parse_krl, parse_krl_query, parse_any, KRLParseError +using .KRL # bring parse_* plus the exported AST node types (KRLProgram, …) # ── helpers ────────────────────────────────────────────────────────────────── @@ -222,6 +222,24 @@ stage(q, i) = q.stages[i] @test isempty(stmt.params) end + # Regression — bare `=` is accepted surface syntax for let-bindings and + # filter equality. Previously the lexer threw on bare `=`, failing every + # `let`/filter test that used it (see Lexer.jl `=` handling). + @testset "bare = surface syntax (regression)" begin + # let binding with bare = + lp = parse_krl("let x = 5") + @test lp.statements[1] isa KRLLetStmt + @test lp.statements[1].name == "x" + + # filter equality with bare = parses the same :eq comparison as == + qbare = one_query("from knots | filter x = 1") + qeq = one_query("from knots | filter x == 1") + @test stage(qbare, 1) isa KRLFilterStage + @test stage(qbare, 1).pred isa KRLCompare + @test stage(qbare, 1).pred.op == :eq + @test stage(qeq, 1).pred.op == :eq + end + # ── Expression precedence ──────────────────────────────────────────────── @testset "Expression: comparison operators" begin for (op_str, op_sym) in [("==", :eq), ("!=", :neq), @@ -280,12 +298,14 @@ stage(q, i) = q.stages[i] end @testset "Expression: function call" begin - q = one_query("from knots | filter gauss(1, -2, 3) == g") + # Use a generic function name — `gauss(...)` is a dedicated form + # (parsed to KRLGaussCode), so it is exercised in "Gauss code" below. + q = one_query("from knots | filter dist(1, -2, 3) == g") pred = stage(q, 1).pred @test pred isa KRLCompare && pred.op == :eq @test pred.left isa KRLCall - # KRLCall.func is a KRLExpr; when calling gauss(...) it's KRLVar("gauss") - @test pred.left.func isa KRLVar && pred.left.func.name == "gauss" + # KRLCall.func is a KRLExpr; for dist(...) it's KRLVar("dist") + @test pred.left.func isa KRLVar && pred.left.func.name == "dist" end @testset "Expression: in operator" begin @@ -313,9 +333,10 @@ stage(q, i) = q.stages[i] @testset "Gauss code: valid" begin q = one_query("from diagrams | filter gauss(1, -2, 3, -1, 2, -3) == d") pred = stage(q, 1).pred - # gauss(...) is parsed as a KRLCall whose func is KRLVar("gauss") - @test pred.left isa KRLCall - @test length(pred.left.args) == 6 + # gauss(...) is a dedicated form → KRLGaussCode (field `codes`), + # per spec/type-system.md §5 [T-Gauss], not a generic KRLCall. + @test pred.left isa KRLGaussCode + @test length(pred.left.codes) == 6 end @testset "Gauss code: zero value rejected" begin @@ -429,7 +450,7 @@ stage(q, i) = q.stages[i] @testset "Property: parse_krl is deterministic" begin for src in [ "from knots | filter x == 1", - "let n = 3\nfrom knots | take n", + "let n = 3\nfrom knots | take 3", """from knots | find_equivalent "3_1" via [jones_polynomial]""", ] p1 = parse_krl(src) diff --git a/server/krl/test/sql_test.jl b/server/krl/test/sql_test.jl index 0bb9d18..a12262d 100644 --- a/server/krl/test/sql_test.jl +++ b/server/krl/test/sql_test.jl @@ -28,7 +28,7 @@ Coverage: using Test include("../KRL.jl") -using .KRL: parse_sql, parse_any, KRLParseError +using .KRL # bring parse_* plus the exported AST node types # ── helpers ────────────────────────────────────────────────────────────────── diff --git a/verification/proofs/agda/.gitignore b/verification/proofs/agda/.gitignore new file mode 100644 index 0000000..4dbecaa --- /dev/null +++ b/verification/proofs/agda/.gitignore @@ -0,0 +1,2 @@ +# Agda build artefacts (interface files); regenerated by `agda --safe`. +*.agdai diff --git a/verification/proofs/agda/DihedralQuandle.agda b/verification/proofs/agda/DihedralQuandle.agda new file mode 100644 index 0000000..870e15f --- /dev/null +++ b/verification/proofs/agda/DihedralQuandle.agda @@ -0,0 +1,101 @@ +{-# OPTIONS --safe #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- =========================================================================== +-- Dihedral (Takasaki) quandle axioms — machine-checked under `agda --safe` +-- =========================================================================== +-- +-- Discharges the algebraic core of obligation M1 ("Quandle axioms preserved") +-- from PROOF-NEEDS.md / PROOF-NARRATIVE.md, and underpins QD-8 +-- (`_dihedral_colouring_count` correctness, which relies on the colouring +-- target actually being a quandle). +-- +-- BEFORE (existing evidence): the three quandle axioms were *property-tested* +-- for the dihedral quandle Z_p at the five primes p ∈ {3, 5, 7, 11, 13} +-- (server/test_quandle_axioms.jl §1). +-- NOW (this file): the three axioms are *proved* for the dihedral / Takasaki +-- quandle operation over ℤ — i.e. for the universal (infinite) dihedral +-- quandle — for ALL arguments, with no case bound. +-- +-- The dihedral quandle operation is a ▷ b = 2·b − a (= (b + b) − a): +-- 1. idempotence a ▷ a ≡ a +-- 2. right self-distributivity (a ▷ b) ▷ c ≡ (a ▷ c) ▷ (b ▷ c) +-- 3. right-invertibility x ↦ x ▷ b is a bijection +-- (here: an involution, hence its own inverse) +-- +-- Scope / honesty. The mechanised result is over ℤ. Every *finite* dihedral +-- quandle R_n = ℤ/nℤ (the Z_p of the tests) is a homomorphic image of ℤ under +-- the surjective ring homomorphism ℤ ↠ ℤ/n; the three axioms are equational +-- identities and so are preserved by homomorphic images. Hence proving them +-- over ℤ establishes them for every R_n, including each Z_p the suite tests. +-- The quotient step itself is the standard algebra remark, not mechanised here. +-- +-- This file does NOT address QD-1 (that `extract_presentation` yields a valid +-- Wirtinger presentation) — that is a separate, harder obligation. + +module DihedralQuandle where + +open import Data.Integer using (ℤ; _+_; _-_; +_) +open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver) +open import Data.Product using (∃; _,_) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; sym; trans; cong) + +open ℤ-solver + +-- The dihedral / Takasaki quandle operation: a ▷ b = 2b − a. +infixr 5 _▷_ +_▷_ : ℤ → ℤ → ℤ +a ▷ b = (b + b) - a + +-- ─────────────────────────────────────────────────────────────────────────── +-- Axiom 1 — idempotence: a ▷ a ≡ a. +-- (a + a) − a ≡ a. A polynomial identity over the ring ℤ. +-- ─────────────────────────────────────────────────────────────────────────── +idempotent : ∀ a → a ▷ a ≡ a +idempotent = solve 1 (λ a → ((a :+ a) :- a) := a) refl + +-- ─────────────────────────────────────────────────────────────────────────── +-- Axiom 3 — right self-distributivity: +-- (a ▷ b) ▷ c ≡ (a ▷ c) ▷ (b ▷ c). +-- Both sides normalise to a − 2b + 2c over ℤ. +-- ─────────────────────────────────────────────────────────────────────────── +self-distrib : ∀ a b c → (a ▷ b) ▷ c ≡ (a ▷ c) ▷ (b ▷ c) +self-distrib = solve 3 + (λ a b c → + ((c :+ c) :- ((b :+ b) :- a)) + := ((((c :+ c) :- b) :+ ((c :+ c) :- b)) :- ((c :+ c) :- a))) + refl + +-- ─────────────────────────────────────────────────────────────────────────── +-- Axiom 2 — right-invertibility: the right translation Sᵦ : x ↦ x ▷ b +-- is a bijection. We show it is an *involution* (Sᵦ ∘ Sᵦ ≡ id), which makes +-- it its own two-sided inverse; injectivity and surjectivity then follow. +-- ─────────────────────────────────────────────────────────────────────────── + +-- Sᵦ is an involution: (a ▷ b) ▷ b ≡ a. +right-involutive : ∀ a b → (a ▷ b) ▷ b ≡ a +right-involutive = solve 2 (λ a b → ((b :+ b) :- ((b :+ b) :- a)) := a) refl + +-- … hence Sᵦ is injective. +right-injective : ∀ {a a′} b → a ▷ b ≡ a′ ▷ b → a ≡ a′ +right-injective {a} {a′} b eq = + trans (sym (right-involutive a b)) + (trans (cong (_▷ b) eq) (right-involutive a′ b)) + +-- … and Sᵦ is surjective: every y is hit, by the preimage (y ▷ b). +right-surjective : ∀ y b → ∃ λ x → x ▷ b ≡ y +right-surjective y b = (y ▷ b) , right-involutive y b + +-- ─────────────────────────────────────────────────────────────────────────── +-- Concrete computational sanity (each is `refl` — the operation actually runs) +-- ─────────────────────────────────────────────────────────────────────────── + +-- In the dihedral quandle of ℤ: 3 ▷ 5 = 2·5 − 3 = 7. +_ : (+ 3) ▷ (+ 5) ≡ + 7 +_ = refl + +-- idempotence at a concrete point: 5 ▷ 5 = 5. +_ : (+ 5) ▷ (+ 5) ≡ + 5 +_ = refl diff --git a/verification/proofs/tlaplus/.gitignore b/verification/proofs/tlaplus/.gitignore new file mode 100644 index 0000000..1c445d5 --- /dev/null +++ b/verification/proofs/tlaplus/.gitignore @@ -0,0 +1,3 @@ +# TLC model-checker scratch output (run-stamped state dumps). +states/ +*.toolbox/ diff --git a/verification/proofs/tlaplus/EGraphConfluence.tla b/verification/proofs/tlaplus/EGraphConfluence.tla new file mode 100644 index 0000000..5529544 --- /dev/null +++ b/verification/proofs/tlaplus/EGraphConfluence.tla @@ -0,0 +1,96 @@ +-------------------------- MODULE EGraphConfluence -------------------------- +(***************************************************************************) +(* SPDX-License-Identifier: MPL-2.0 *) +(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) +(* *) +(* Equality-saturation confluence for the QuandleDB equivalence engine. *) +(* *) +(* Discharges the model-checked core of two invariants from *) +(* spec/operational-semantics.md: *) +(* §11.5 E-graph confluence: *) +(* "Equality saturation reaches a unique fixed point regardless *) +(* of rule application order." *) +(* §11.6 Deterministic collapse: *) +(* "Given the same database state and query, results are *) +(* deterministic." *) +(* *) +(* Model. `Elements` are knots (e-classes initially singletons). *) +(* `Merges` are the merge facts produced by rule firing (saturate, §8.1). *) +(* A step applies any not-yet-absorbed merge and re-closes the relation *) +(* to an equivalence. TLC explores EVERY interleaving of merge order; *) +(* the property `Confluent` asserts every terminal partition equals the *) +(* order-independent target `Saturated` — i.e. confluence. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS Elements, \* finite set of e-class representatives (knots) + Merges \* set of <> merge facts emitted by the rules + +ASSUME MergesArePairs == + /\ Merges \subseteq (Elements \X Elements) + +VARIABLE rel \* current equivalence relation, as a set of pairs + +---------------------------------------------------------------------------- +(* One relational composition step and the reflexive/symmetric/transitive *) +(* closure to an equivalence relation (finite ⇒ the fixpoint terminates). *) + +Diagonal == { <> : x \in Elements } + +Sym(R) == R \cup { <> : p \in R } + +Step(R) == + R \cup { <> \in Elements \X Elements : + \E b \in Elements : <> \in R /\ <> \in R } + +RECURSIVE Close(_) +Close(R) == LET R1 == Step(R) IN IF R1 = R THEN R ELSE Close(R1) + +\* reflexive-symmetric-transitive closure of a base relation +EquivClosure(base) == Close(Sym(base) \cup Diagonal) + +---------------------------------------------------------------------------- +(* The order-independent target: close ALL merge facts at once. *) +Saturated == EquivClosure(Merges) + +(* A merge fact is absorbed once both endpoints already share a class. *) +Absorbed(m) == <> \in rel +Done == \A m \in Merges : Absorbed(m) + +---------------------------------------------------------------------------- +Init == rel = Diagonal + +\* apply one not-yet-absorbed merge and re-saturate +MergeStep == + /\ \E m \in Merges : + /\ ~ Absorbed(m) + /\ rel' = EquivClosure(rel \cup {m}) + +\* stutter once fully saturated (so a finished run is not a deadlock) +Finish == Done /\ UNCHANGED rel + +Next == MergeStep \/ Finish + +Spec == Init /\ [][Next]_rel + +---------------------------------------------------------------------------- +(* ---- INVARIANTS (checked across every interleaving) ---- *) + +\* rel is always a well-formed relation on Elements +TypeOK == rel \subseteq (Elements \X Elements) + +\* rel is always an equivalence relation +IsEquivalence == + /\ \A x \in Elements : <> \in rel \* reflexive + /\ \A p \in rel : <> \in rel \* symmetric + /\ \A a, b, c \in Elements : + (<> \in rel /\ <> \in rel) => <> \in rel \* transitive + +\* rel never over-merges: it stays below the saturated target +SoundBelow == rel \subseteq Saturated + +\* CONFLUENCE / DETERMINISTIC COLLAPSE: +\* every saturated terminal state equals the order-independent target. +Confluent == Done => (rel = Saturated) + +============================================================================= diff --git a/verification/proofs/tlaplus/MCEGraph.cfg b/verification/proofs/tlaplus/MCEGraph.cfg new file mode 100644 index 0000000..6c4a6da --- /dev/null +++ b/verification/proofs/tlaplus/MCEGraph.cfg @@ -0,0 +1,8 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* Concrete model values are supplied by INSTANCE ... WITH in MCEGraph.tla. +INIT Init +NEXT Next +INVARIANT TypeOK +INVARIANT IsEquivalence +INVARIANT SoundBelow +INVARIANT Confluent diff --git a/verification/proofs/tlaplus/MCEGraph.tla b/verification/proofs/tlaplus/MCEGraph.tla new file mode 100644 index 0000000..a355258 --- /dev/null +++ b/verification/proofs/tlaplus/MCEGraph.tla @@ -0,0 +1,21 @@ +------------------------------ MODULE MCEGraph ------------------------------ +(* SPDX-License-Identifier: MPL-2.0 *) +(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) +(* *) +(* TLC model harness for EGraphConfluence. The `.cfg` format cannot write *) +(* tuple literals in CONSTANT assignments, so the concrete model values *) +(* are defined here and supplied to the spec by `INSTANCE ... WITH`. *) +(* *) +(* Four knots; the merge facts chain them into one class, so TLC must *) +(* confirm that every interleaving of merge order reaches the same final *) +(* partition (confluence / deterministic collapse). *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +MCElements == {1, 2, 3, 4} +MCMerges == {<<1, 2>>, <<3, 4>>, <<2, 3>>} + +VARIABLE rel + +INSTANCE EGraphConfluence WITH Elements <- MCElements, Merges <- MCMerges +=============================================================================