From 6ea708cc6dc42cb83db036b7f9d295e080a90710 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:34:24 +0100 Subject: [PATCH 1/5] =?UTF-8?q?fix:=20post-Bareiss=20follow-up=20=E2=80=94?= =?UTF-8?q?=20conway=20marker=20removed,=20polynomial=20bounds=2012=20?= =?UTF-8?q?=E2=86=92=20128?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit main is currently RED: KnotTheory.jl#48 merged, so the conway @test_broken now reports 'Unexpected Pass' — a hard error, and exactly the forcing signal the marker existed to produce. This clears it. - conway(figure_eight) restored to a hard @test. Upstream now normalises alexander to Delta(1) = +1 (the Conway normalisation) instead of 'leading coefficient positive', which was the wrong canonical choice on mixed-sign knots; the value is 1 - z^2 exactly. - ALEXANDER/CONWAY_MAX_CROSSINGS 12 → 128. The bound of 12 was calibrated against the O(n!) cofactor determinant that #48 replaced with O(n^3) Bareiss elimination. Re-measured on (2,n)-torus closures (the worst case — no arc merging): n=40 → 0.07s, n=100 → 0.10s, n=140 → 0.61s, against 6h+ at n=16 before. 128 keeps the worst case sub-second while covering every realistic diagram. Jones (20) and HOMFLY (15) are unchanged — those are genuinely exponential. - The guard testset is reworked: with the three bounds now an order of magnitude apart, one diagram can no longer exercise them all. It tests a 16-crossing diagram (only HOMFLY defers; alexander, conway and jones must all be real) AND a 130-crossing diagram (all four defer). The second case asserts crossings > ALEXANDER_MAX_CROSSINGS explicitly, so raising the bound without raising the fixture fails loudly rather than going quiet. Validated locally against KnotTheory main (a2f2938): the full axioms suite passes with ZERO broken markers — a first for this suite. Co-Authored-By: Claude Fable 5 --- server/quandle_semantic.jl | 26 ++++++++------- server/test_quandle_axioms.jl | 59 ++++++++++++++++++++--------------- 2 files changed, 48 insertions(+), 37 deletions(-) diff --git a/server/quandle_semantic.jl b/server/quandle_semantic.jl index 21342d7..8fab58f 100644 --- a/server/quandle_semantic.jl +++ b/server/quandle_semantic.jl @@ -469,15 +469,19 @@ end const HOMFLY_MAX_CROSSINGS = 15 const HOMFLY_DEFERRED_SENTINEL = "deferred:too_many_crossings" -# KnotTheory's alexander_polynomial computes its polynomial-matrix minor -# determinant by naive cofactor expansion — O(n!) in the minor size, which -# tracks the crossing count. Measured on (2,n)-torus closures (s1^n, the -# worst case: no arc merging): n=12 → 12s, n=13 → 106s, n=16 → 6h+ (this -# hung CI to GitHub's job kill). conway_polynomial CALLS alexander_polynomial -# internally, so it inherits the same bound. jones_polynomial goes through -# the Kauffman bracket instead, which KnotTheory itself hard-limits at 20 -# crossings by THROWING — we convert that throw into the same sentinel. -const ALEXANDER_MAX_CROSSINGS = 12 +# alexander_polynomial's determinant is now fraction-free Bareiss +# elimination — O(n^3) polynomial operations (KnotTheory.jl#46/#48). +# Re-measured on (2,n)-torus closures (s1^n, the worst case: no arc +# merging): n=40 → 0.07s, n=100 → 0.10s, n=140 → 0.61s. The previous +# bound of 12 was calibrated against the O(n!) cofactor expansion it +# replaced (n=12 → 12s, n=13 → 106s, n=16 → 6h+ and a CI job killed at +# GitHub's 6-hour limit), so it is now an order of magnitude too tight. +# 128 keeps the worst case sub-second while covering every realistic +# diagram. conway_polynomial calls alexander_polynomial, so it shares +# the bound. jones_polynomial instead goes through the Kauffman bracket, +# which is genuinely 2^n and which KnotTheory hard-limits at 20 crossings +# by THROWING — we convert that throw into the same sentinel. +const ALEXANDER_MAX_CROSSINGS = 128 const CONWAY_MAX_CROSSINGS = ALEXANDER_MAX_CROSSINGS const JONES_MAX_CROSSINGS = 20 @@ -498,7 +502,7 @@ end _safe_alexander_serialised(pd::KnotTheory.PlanarDiagram) -> String Alexander polynomial, guarded by `ALEXANDER_MAX_CROSSINGS` (the upstream -determinant is O(n!) cofactor expansion). Returns the deferred sentinel +determinant is O(n^3) Bareiss elimination). Returns the deferred sentinel above the bound. """ function _safe_alexander_serialised(pd::KnotTheory.PlanarDiagram)::String @@ -510,7 +514,7 @@ end _safe_conway_serialised(pd::KnotTheory.PlanarDiagram) -> String Conway polynomial, guarded by `CONWAY_MAX_CROSSINGS` (upstream it is -computed FROM the Alexander polynomial, so it shares the O(n!) cost). +computed FROM the Alexander polynomial, so it shares that cost). Returns the deferred sentinel above the bound. """ function _safe_conway_serialised(pd::KnotTheory.PlanarDiagram)::String diff --git a/server/test_quandle_axioms.jl b/server/test_quandle_axioms.jl index 6a88384..43eb2ac 100644 --- a/server/test_quandle_axioms.jl +++ b/server/test_quandle_axioms.jl @@ -512,22 +512,32 @@ end end @testset "KT-2 ext: polynomial guards return sentinels above their bounds" begin - # Build a synthetic 16-crossing PD by braid word s1^16 — a genuine - # (2,16)-torus-link diagram (post KnotTheory#43; before that fix the - # broken braid closure made this degenerate and cheap, which is how the - # missing guards went unnoticed). 16 crossings exceeds - # HOMFLY_MAX_CROSSINGS (15) and ALEXANDER/CONWAY_MAX_CROSSINGS (12, - # the O(n!) upstream determinant: 12 → 12s, 13 → 106s, 16 → 6h+ and a - # CI job killed at GitHub's 6-hour limit), but not JONES_MAX_CROSSINGS - # (20, Kauffman bracket: 2.8s measured at 16). - pd_large = from_braid_word(join(["s1" for _ in 1:16], ".")).pd - d_large = quandle_descriptor(pd_large) - @test d_large.homfly_polynomial == HOMFLY_DEFERRED_SENTINEL - @test d_large.alexander_polynomial == HOMFLY_DEFERRED_SENTINEL - @test d_large.conway_polynomial == HOMFLY_DEFERRED_SENTINEL - # Jones stays real at 16 crossings — a sentinel here would mean the - # bound was tightened without re-measuring. - @test d_large.jones_polynomial != HOMFLY_DEFERRED_SENTINEL + # Each polynomial has its OWN bound, set by its own measured cost model, + # so one diagram cannot exercise them all. Both cases below are genuine + # (2,n)-torus-link diagrams (post KnotTheory#43 — before that fix the + # broken braid closure made them degenerate and cheap, which is how the + # missing guards went unnoticed until CI hung for 6 hours). + + # 16 crossings: above HOMFLY's 15 (skein recursion is exponential), but + # below Jones' 20 (Kauffman bracket, 2.8s measured here) and far below + # alexander/conway's 128 (Bareiss, O(n^3)). + pd16 = from_braid_word(join(["s1" for _ in 1:16], ".")).pd + d16 = quandle_descriptor(pd16) + @test d16.homfly_polynomial == HOMFLY_DEFERRED_SENTINEL + @test d16.jones_polynomial != HOMFLY_DEFERRED_SENTINEL + @test d16.alexander_polynomial != HOMFLY_DEFERRED_SENTINEL + @test d16.conway_polynomial != HOMFLY_DEFERRED_SENTINEL + + # 130 crossings: above every bound — all four defer. This also pins the + # alexander/conway bound itself: if someone raises it without raising + # this fixture, the test fails rather than silently going quiet. + pd_over = from_braid_word(join(["s1" for _ in 1:130], ".")).pd + @test length(pd_over.crossings) > ALEXANDER_MAX_CROSSINGS + d_over = quandle_descriptor(pd_over) + @test d_over.alexander_polynomial == HOMFLY_DEFERRED_SENTINEL + @test d_over.conway_polynomial == HOMFLY_DEFERRED_SENTINEL + @test d_over.jones_polynomial == HOMFLY_DEFERRED_SENTINEL + @test d_over.homfly_polynomial == HOMFLY_DEFERRED_SENTINEL end @testset "KT-2 ext: Jones polynomial distinguishes the test knots" begin @@ -675,17 +685,14 @@ end t = quandle_descriptor(trefoil().pd) @test t.conway_polynomial == "0:1,2:1" - # Figure-eight ∇(z) = 1 - z² → "0:1,2:-1" - # KNOWN-BROKEN (upstream KnotTheory.jl#42): the computed value is - # "0:-1,2:1" = -(1 - z²). Conway is canonically normalised (∇(unknot)=1, - # so there is NO legitimate unit ambiguity) — the sign flip comes from - # the Alexander determinant's row/sign convention on mixed-sign - # diagrams, the same missing unit normalisation tracked in #42. The - # trefoil and cinquefoil (all-positive crossings) are unaffected. - # First caught here: this fixture suite (issue #32) merged behind the - # 6-hour CI hang and had never actually executed before. + # Figure-eight ∇(z) = 1 - z² → "0:1,2:-1". This was @test_broken: the + # computed value was -(1 - z²) because alexander normalised its unit by + # "leading coefficient positive", the wrong canonical choice on + # mixed-sign knots. Fixed upstream (KnotTheory.jl#48) by normalising to + # Δ(1) = +1, the Conway normalisation — the marker then reported + # "unexpected pass", which is exactly the signal it existed to produce. f = quandle_descriptor(figure_eight().pd) - @test_broken f.conway_polynomial == "0:1,2:-1" + @test f.conway_polynomial == "0:1,2:-1" # Cinquefoil ∇(z) = 1 + 3z² + z⁴ → "0:1,2:3,4:1" c = quandle_descriptor(cinquefoil().pd) From dac9b3e5306c015557772a026a4bfe84ba45efd4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:43:31 +0100 Subject: [PATCH 2/5] docs(test): record the measured cause of the BR-5 quandle_key residual MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 11/200 count did not move when KnotTheory#48 merged, falsifying the assumption that the alexander/conway sign convention caused it. Split by Delta(1) over the same 200-trial corpus: links (Delta(1)=0): 11 mismatch, 87 agree knots (Delta(1)=±1): 0 mismatch, 102 agree Knots are now fully crossing-order invariant; the residual is entirely a multi-component-link defect. Upstream conway_polynomial reconstructs from an assumed symmetry about exponent 0 that no link satisfies (even span gives a half-integer centre), so it returns genuinely different polynomials for the same link — 1 + z^2 vs 1 — rather than a different unit. Filed as KnotTheory.jl#51 with the worked examples. Comment updated to cite that evidence instead of the old vague wording. The marker stays until #51 lands. Co-Authored-By: Claude Fable 5 --- server/test_br5_fuzz.jl | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/server/test_br5_fuzz.jl b/server/test_br5_fuzz.jl index 81ac80b..47fa54d 100644 --- a/server/test_br5_fuzz.jl +++ b/server/test_br5_fuzz.jl @@ -120,13 +120,23 @@ end @testset "BR-5: crossing-order invariance on random braid words" begin rng = MersenneTwister(BR5_SEED + 1) - # KNOWN-BROKEN (upstream): the polynomial segments of quandle_key - # (alexander/conway/homfly from KnotTheory.jl) are crossing-order - # sensitive on some diagrams — the polynomials are not normalised to a - # canonical unit (±t^k), so 25/200 seeded trials disagree. The layers - # this repo owns (presentation_hash, colouring counts) are asserted - # hard below; the key mismatch count is tracked and marked broken so - # the marker must be removed once KnotTheory.jl normalises. + # KNOWN-BROKEN (upstream KnotTheory.jl#51): the polynomial segments of + # quandle_key are crossing-order sensitive on multi-component LINKS. + # Measured over this 200-trial corpus, splitting by Delta(1): + # links (Delta(1)=0): 11 mismatch, 87 agree + # knots (Delta(1)=±1): 0 mismatch, 102 agree + # Knots became fully order-invariant when KnotTheory#48 landed the + # Delta(1)=+1 normalisation; that fix cannot apply to links, where + # Delta(1)=0 and the code falls back to an order-sensitive rule. Worse, + # conway_polynomial reconstructs from an assumed symmetry about + # exponent 0, which no link satisfies (even span ⟹ half-integer + # centre), so it returns genuinely DIFFERENT polynomials for the same + # link (e.g. 1 + z² vs 1) — not merely a different unit. + # NOTE: this count did NOT move when #48 merged. The earlier + # attribution of these mismatches to the alexander/conway sign + # convention was wrong; the sign fix was real but orthogonal. + # The layers this repo owns (presentation_hash, colouring counts) are + # asserted hard below and hold on every trial. quandle_key_mismatches = 0 for trial in 1:BR5_TRIALS nstrands = rand(rng, 3:4) From 68fe9e1752045112147e1ceef1206a94f6b70ebe Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:55:48 +0100 Subject: [PATCH 3/5] =?UTF-8?q?fix(ci):=20symlink=20siblings=20one=20level?= =?UTF-8?q?=20up=20=E2=80=94=20#83=20moved=20[sources]=20and=20broke=20ins?= =?UTF-8?q?tantiate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #83 changed server/Project.toml [sources] from ../../../.jl to ../../.jl but left this workflow symlinking two levels above the workspace. Every run since has died in 'Instantiate server project' with expected package KnotTheory [215268c9] to exist at path /home/runner/work/quandledb/KnotTheory.jl i.e. main has been red for this as well as the conway marker — the path error hits first, so the axioms suite never even ran. Symlink now targets $GITHUB_WORKSPACE/../, matching [sources]. Adds a check that reads server/Project.toml and asserts every [sources] path resolves to a real directory BEFORE instantiate, so the next drift names its own cause instead of surfacing as a registry-shaped error. Co-Authored-By: Claude Fable 5 --- .github/workflows/krl-verification.yml | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/.github/workflows/krl-verification.yml b/.github/workflows/krl-verification.yml index 14177ed..aac4811 100644 --- a/.github/workflows/krl-verification.yml +++ b/.github/workflows/krl-verification.yml @@ -68,9 +68,12 @@ jobs: julia --color=yes server/krl/test/seam_test.jl # server/Project.toml [sources] resolves KnotTheory/Skein/AcceleratorGate - # at server/../../../.jl — i.e. two directories above the repo - # checkout ($GITHUB_WORKSPACE/../../.jl). actions/checkout cannot - # write outside the workspace, so check out under deps/ and symlink. + # at server/../../.jl — i.e. one directory above the repo checkout + # ($GITHUB_WORKSPACE/../.jl). actions/checkout cannot write outside + # the workspace, so check out under deps/ and symlink. + # NOTE: keep this in step with server/Project.toml — #83 moved [sources] + # from ../../../ to ../../ without updating the symlink here, which broke + # every instantiate with "expected package KnotTheory to exist at path". - name: Checkout KnotTheory.jl uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4 with: @@ -93,8 +96,19 @@ jobs: run: | set -euo pipefail for p in KnotTheory.jl Skein.jl AcceleratorGate.jl; do - ln -sfn "$GITHUB_WORKSPACE/deps/$p" "$GITHUB_WORKSPACE/../../$p" + ln -sfn "$GITHUB_WORKSPACE/deps/$p" "$GITHUB_WORKSPACE/../$p" done + # Fail loudly here rather than inside Pkg.instantiate, whose error + # ("expected package ... to exist at path") names the path but not + # the cause. + julia --project=server -e ' + using TOML + src = TOML.parsefile("server/Project.toml")["sources"] + for (name, spec) in src + path = normpath(joinpath("server", spec["path"])) + isdir(path) || error("[sources] $name -> $(spec["path"]) resolves to $path, which does not exist; the symlink step above is out of step with server/Project.toml") + end + println("PASS: all [sources] paths resolve")' - name: Instantiate server project run: julia --color=yes --project=server -e 'using Pkg; Pkg.instantiate()' From a7b553a867425bfd080e8a1f458c207ff3f27b69 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 20:35:26 +0100 Subject: [PATCH 4/5] =?UTF-8?q?feat(krl):=20DB-6=20Phase=20A=20=E2=80=94?= =?UTF-8?q?=20`explain`=20keyword=20and=20structured=20query=20plan?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the Phase A gap on #34. Before this, EXPLAIN was reachable only over HTTP with raw SQL; the KRL surface the issue actually specifies did not exist — `explain` was in neither the lexer nor the parser, and there was no selectivity model at all. - `explain` is a reserved word and a statement prefix: `explain from … | …`. - It parses to KRLExplainStmt, deliberately a DISTINCT statement type rather than a flag on KRLQueryStmt, so every existing consumer of KRLQueryStmt still means "this query will actually execute" and cannot be handed a plan where it expected rows. - ExplainPlan.jl builds the plan shape the acceptance criteria specify: an ordered scan + per-stage operations, each filter carrying column, comparator, value, `indexed`, and a selectivity estimate. Conjunctions are split into separate filter operations, which is what makes the DB-7 reorder meaningful later. Honesty properties, both asserted by tests: - Selectivity is the stub the criteria permit pending DB-3 (#33), and says so: every estimate carries "selectivity_source" => "stub", and `plan_is_costed` returns false while any stub remains — so DB-7 cannot silently optimise against invented numbers. - `indexed` is driven by a deliberately short explicit column list. An over-claiming list would make it a fake signal, which is worse than reporting false. - A predicate the plan cannot describe (column-to-column, nested boolean, call) is reported opaquely rather than given a fabricated column. 25 assertions in server/krl/test/explain_test.jl, wired into the dependency-free CI step alongside the other pure-Julia suites. Existing lexer/parser/sql/seam suites all still pass. Co-Authored-By: Claude Fable 5 --- .github/workflows/krl-verification.yml | 1 + server/krl/Ast.jl | 16 ++- server/krl/ExplainPlan.jl | 152 +++++++++++++++++++++++++ server/krl/KRL.jl | 1 + server/krl/Lexer.jl | 2 + server/krl/Parser.jl | 13 ++- server/krl/test/explain_test.jl | 73 ++++++++++++ 7 files changed, 256 insertions(+), 2 deletions(-) create mode 100644 server/krl/ExplainPlan.jl create mode 100644 server/krl/test/explain_test.jl diff --git a/.github/workflows/krl-verification.yml b/.github/workflows/krl-verification.yml index aac4811..4ef93c6 100644 --- a/.github/workflows/krl-verification.yml +++ b/.github/workflows/krl-verification.yml @@ -66,6 +66,7 @@ jobs: julia --color=yes server/krl/test/parser_test.jl julia --color=yes server/krl/test/sql_test.jl julia --color=yes server/krl/test/seam_test.jl + julia --color=yes server/krl/test/explain_test.jl # server/Project.toml [sources] resolves KnotTheory/Skein/AcceleratorGate # at server/../../.jl — i.e. one directory above the repo checkout diff --git a/server/krl/Ast.jl b/server/krl/Ast.jl index 89ced4e..852fcb6 100644 --- a/server/krl/Ast.jl +++ b/server/krl/Ast.jl @@ -36,7 +36,7 @@ export KRLNode, KRLStatement, KRLSource, KRLPipeStage, KRLReturnItem, SortOrder, SortAsc, SortDesc, EdgeDir, EdgeForward, EdgeBackward, EdgeUndirected, # program + statements - KRLProgram, KRLQueryStmt, KRLLetStmt, KRLRuleDef, KRLAxiomDef, + KRLProgram, KRLQueryStmt, KRLExplainStmt, KRLLetStmt, KRLRuleDef, KRLAxiomDef, # query + sources KRLQuery, KRLSourceKnots, KRLSourceDiagrams, KRLSourceInvariants, KRLSourceNamed, KRLSourceSubquery, @@ -123,6 +123,20 @@ struct KRLQueryStmt <: KRLStatement col::Int end +""" + KRLExplainStmt(query, line, col) + +`explain from … | …` — DB-6 Phase A. Returns the query PLAN rather than +running the query. Deliberately a distinct statement type rather than a flag +on `KRLQueryStmt`, so that every existing consumer of `KRLQueryStmt` +continues to mean "this query will actually execute". +""" +struct KRLExplainStmt <: KRLStatement + query::KRLNode # KRLQuery + line::Int + col::Int +end + """ KRLLetStmt(name, type_ann, expr, line, col) diff --git a/server/krl/ExplainPlan.jl b/server/krl/ExplainPlan.jl new file mode 100644 index 0000000..dfa6771 --- /dev/null +++ b/server/krl/ExplainPlan.jl @@ -0,0 +1,152 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# +# DB-6 Phase A — structured query plan for `explain from … | …`. +# +# Produces the shape the DB-6 acceptance criteria specify: an ordered list of +# operations, each tagged with its kind and, for filters, the column, the +# comparator, the literal value, whether the column is indexed, and a +# selectivity estimate. +# +# HONESTY NOTE ON SELECTIVITY +# --------------------------- +# There are no column histograms yet — that is DB-3 (#33). The criteria +# explicitly permit a stub until DB-3 lands, so every estimate here is +# `SELECTIVITY_STUB` and is reported with `"selectivity_source" => "stub"`. +# Nothing downstream may treat these as measured: `plan_is_costed` returns +# false while any estimate is a stub, so a future DB-7 cost-based reorder +# cannot silently optimise against made-up numbers. + +# Included directly into the `KRL` module namespace (as Ast.jl / Parser.jl / +# Evaluator.jl are) — not a submodule, so AST types resolve without imports. + +"""Placeholder selectivity used until DB-3 (#33) provides real histograms.""" +const SELECTIVITY_STUB = 0.5 + +""" +Columns carrying a secondary index today. Kept deliberately small and +explicit: an over-claiming list would make `indexed` a fake signal, which is +worse than reporting `false`. Extend as DB-3 lands real indexes. +""" +const INDEXED_COLUMNS = Set([ + "colouring_count_3", + "colouring_count_5", + "presentation_hash", + "quandle_key", +]) + +_cmp_symbol(k::Symbol) = get(Dict( + :eq => "=", :neq => "!=", :lt => "<", :lte => "<=", + :gt => ">", :gte => ">=", :iso => "≅", :path => "~>", :in => "in", +), k, string(k)) + +_source_name(s::KRLSource) = + s isa KRLSourceKnots ? "knots" : + s isa KRLSourceDiagrams ? "diagrams" : + s isa KRLSourceInvariants ? "invariants" : + s isa KRLSourceNamed ? s.name : + s isa KRLSourceSubquery ? "" : "" + +# Pull (column, comparator, value) out of a comparison predicate when the +# shape is the simple `column literal` the plan can describe. Anything +# else (nested boolean, function call, column-to-column) yields `nothing` and +# is reported as an opaque predicate rather than being mis-described. +_literal_value(e::KRLExpr) = + e isa KRLInt ? e.n : + e isa KRLFloat ? e.x : + e isa KRLString ? e.s : + e isa KRLBool ? e.b : + e isa KRLKnotName ? e.name : nothing + +function _simple_comparison(e::KRLExpr) + e isa KRLCompare || return nothing + e.left isa KRLVar || return nothing + val = _literal_value(e.right) + val === nothing && return nothing + (e.left.name, _cmp_symbol(e.op), val) +end + +# Split a conjunction into its conjuncts so `filter a = 1 and b < 2` plans as +# two filter operations, which is what makes a future reorder meaningful. +function _conjuncts(e::KRLExpr) + e isa KRLAnd && return vcat(_conjuncts(e.left), _conjuncts(e.right)) + [e] +end + +function _filter_ops(pred::KRLExpr) + ops = Dict{String, Any}[] + for c in _conjuncts(pred) + simple = _simple_comparison(c) + if simple === nothing + push!(ops, Dict{String, Any}( + "op" => "filter", + "predicate" => "", + "indexed" => false, + "selectivity_estimate" => SELECTIVITY_STUB, + "selectivity_source" => "stub", + )) + else + col, cmp, val = simple + push!(ops, Dict{String, Any}( + "op" => "filter", + "column" => col, + "comparator" => cmp, + "value" => val, + "indexed" => col in INDEXED_COLUMNS, + "selectivity_estimate" => SELECTIVITY_STUB, + "selectivity_source" => "stub", + )) + end + end + ops +end + +""" + explain_plan(q::KRLQuery) -> Vector{Dict{String, Any}} + +Ordered plan for `q`: a `scan` of the source followed by one entry per +pipeline stage, with conjoined filters split into separate `filter` +operations. + +The order returned is **execution order as written** — no reordering is +performed. Cost-based reordering is DB-7 and requires real selectivity +(DB-3), which is why every estimate here is flagged `"stub"`. +""" +function explain_plan(q::KRLQuery)::Vector{Dict{String, Any}} + plan = Dict{String, Any}[Dict{String, Any}( + "op" => "scan", + "table" => _source_name(q.source), + )] + for stage in q.stages + if stage isa KRLFilterStage + append!(plan, _filter_ops(stage.pred)) + elseif stage isa KRLSortStage + push!(plan, Dict{String, Any}( + "op" => "sort", + "keys" => length(stage.items), + )) + elseif stage isa KRLTakeStage + push!(plan, Dict{String, Any}("op" => "take", "n" => stage.n)) + elseif stage isa KRLSkipStage + push!(plan, Dict{String, Any}("op" => "skip", "n" => stage.n)) + else + push!(plan, Dict{String, Any}("op" => _stage_op_name(stage))) + end + end + plan +end + +_stage_op_name(s::KRLPipeStage) = + s isa KRLReturnStage ? "return" : + s isa KRLGroupByStage ? "group_by" : + lowercase(replace(string(nameof(typeof(s))), "KRL" => "", "Stage" => "")) + +""" + plan_is_costed(plan) -> Bool + +`true` only when every selectivity estimate in `plan` came from real +statistics. While DB-3 (#33) is outstanding this is always `false` — the +guard that stops DB-7 optimising against stub numbers. +""" +plan_is_costed(plan::Vector{Dict{String, Any}}) = + !any(get(op, "selectivity_source", "stub") == "stub" for op in plan) diff --git a/server/krl/KRL.jl b/server/krl/KRL.jl index 19bf051..981822b 100644 --- a/server/krl/KRL.jl +++ b/server/krl/KRL.jl @@ -28,6 +28,7 @@ include("Lexer.jl") include("Ast.jl") include("Parser.jl") include("SqlFrontend.jl") +include("ExplainPlan.jl") include("Evaluator.jl") end # module KRL diff --git a/server/krl/Lexer.jl b/server/krl/Lexer.jl index 550beac..292251d 100644 --- a/server/krl/Lexer.jl +++ b/server/krl/Lexer.jl @@ -62,6 +62,8 @@ const TokenKind = Symbol # ───────────────────────────────────────────────────────────────────────────── const KRL_KEYWORDS = Set([ + # query-level modifiers + "explain", # pipeline stages "from", "filter", "sort", "take", "skip", "return", "group_by", "aggregate", diff --git a/server/krl/Parser.jl b/server/krl/Parser.jl index cc430d4..5126032 100644 --- a/server/krl/Parser.jl +++ b/server/krl/Parser.jl @@ -189,6 +189,17 @@ function _parse_statement(ps::ParserState)::KRLStatement return _parse_let_stmt(ps) end + # explain from … | … (DB-6 Phase A: plan, do not execute) + if _kw(ps, "explain") + _advance!(ps) + et = _peek(ps) + _kw(ps, "from") || throw(KRLParseError( + "expected `from` after `explain`, got $(et.kind)($(repr(et.value)))", + et.line, et.col)) + q = _parse_query(ps) + return KRLExplainStmt(q, t.line, t.col) + end + # from … | … (pipeline query) if _kw(ps, "from") q = _parse_query(ps) @@ -197,7 +208,7 @@ function _parse_statement(ps::ParserState)::KRLStatement t = _peek(ps) throw(KRLParseError( - "expected statement (from/let/rule/axiom), got $(t.kind)($(repr(t.value)))", + "expected statement (from/explain/let/rule/axiom), got $(t.kind)($(repr(t.value)))", t.line, t.col)) end diff --git a/server/krl/test/explain_test.jl b/server/krl/test/explain_test.jl new file mode 100644 index 0000000..2de3abe --- /dev/null +++ b/server/krl/test/explain_test.jl @@ -0,0 +1,73 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# +# DB-6 Phase A — `explain from … | …` produces a structured plan. + +using Test +include(joinpath(@__DIR__, "..", "KRL.jl")) +using .KRL: parse_krl, explain_plan, plan_is_costed, SELECTIVITY_STUB, + KRLExplainStmt, KRLQueryStmt, KRLParseError + +@testset "DB-6: explain is a distinct statement, not a query" begin + prog = parse_krl("explain from knots | filter crossing < 8") + @test length(prog.statements) == 1 + @test prog.statements[1] isa KRLExplainStmt + # A plain query must NOT become an explain — the two are distinguishable + # so no existing consumer can be handed a plan where it expected rows. + @test parse_krl("from knots | filter crossing < 8").statements[1] isa KRLQueryStmt +end + +@testset "DB-6: explain requires a query after it" begin + @test_throws KRLParseError parse_krl("explain") + @test_throws KRLParseError parse_krl("explain take 5") +end + +@testset "DB-6: plan shape matches the acceptance criteria" begin + prog = parse_krl( + "explain from knots | filter colouring_count_3 = 9 and crossing < 8 | take 5") + plan = explain_plan(prog.statements[1].query) + + @test plan[1]["op"] == "scan" + @test plan[1]["table"] == "knots" + + # A conjunction becomes SEPARATE filter operations — that is what makes a + # future cost-based reorder (DB-7) meaningful. + @test plan[2]["op"] == "filter" + @test plan[2]["column"] == "colouring_count_3" + @test plan[2]["comparator"] == "=" + @test plan[2]["value"] == 9 + @test plan[2]["indexed"] == true # carries a secondary index + + @test plan[3]["column"] == "crossing" + @test plan[3]["comparator"] == "<" + @test plan[3]["value"] == 8 + @test plan[3]["indexed"] == false # does not + + @test plan[4]["op"] == "take" + @test plan[4]["n"] == 5 +end + +@testset "DB-6: selectivity is honestly labelled a stub until DB-3" begin + plan = explain_plan( + parse_krl("explain from knots | filter crossing < 8").statements[1].query) + filt = plan[2] + @test filt["selectivity_estimate"] == SELECTIVITY_STUB + @test filt["selectivity_source"] == "stub" + # The guard that stops DB-7 optimising against invented numbers. This must + # stay false until real histograms land (#33) — if it ever returns true + # while estimates are stubs, the cost model is lying. + @test plan_is_costed(plan) == false +end + +@testset "DB-6: a predicate the plan cannot describe is not mis-described" begin + # Column-to-column comparison is not a simple `column literal`, so + # it must be reported opaquely rather than given a fabricated column. + plan = explain_plan( + parse_krl("explain from knots | filter crossing < genus").statements[1].query) + @test plan[2]["op"] == "filter" + @test plan[2]["predicate"] == "" + @test !haskey(plan[2], "column") + @test plan[2]["indexed"] == false +end + +println("krl-explain-tests-ok") From 6fca1982598b9acaa6fb3c8c85e032bfc0f81ee7 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:25:43 +0100 Subject: [PATCH 5/5] docs: reconcile the two DB-6 surfaces; refresh machine-readable state MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/db-6-explain-strategy.md said "Phase A landed 2026-06-01" while issue #34's Phase A had never been built. Both statements were true of DIFFERENT surfaces, and conflating them is what made #34 look closable: SQL-side EXPLAIN QUERY PLAN over read-path SQL landed 2026-06-01 KRL-side explain keyword + structured plan landed 2026-07-28 The document now names both explicitly and documents the KRL surface: syntax, plan shape, why explain is its own statement type, why selectivity is a labelled stub guarded by plan_is_costed(), why the indexed column list is deliberately short, and what Phase B needs. .machine_readable/6a2/STATE.a2ml was last touched 2026-02-13 and recorded no milestones, no blockers and no next actions — the file agents read to orient themselves said nothing. It now carries measured state: phase testing, the DB-6/DB-3 milestone chain, four live issues (Guix gate, ruleset --admin, doc drift, ungated tiers) with evidence paths, ordered next actions with owners, and zero-known-broken-markers = true. Co-Authored-By: Claude Fable 5 --- .machine_readable/6a2/STATE.a2ml | 40 +++++++++++---- docs/db-6-explain-strategy.md | 86 +++++++++++++++++++++++++++++++- 2 files changed, 116 insertions(+), 10 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 3adb7ab..b30758a 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -5,34 +5,56 @@ [metadata] project = "quandledb" version = "0.1.0" -last-updated = "2026-02-13" +last-updated = "2026-07-28" status = "active" -session = "converted from scheme — 2026-04-11" +session = "CI/correctness campaign — 2026-07-21 → 2026-07-28" [project-context] name = "Quandledb" purpose = """Knot-theory database application — the invariant/equivalence + semantic-identity face of the KRL stack (quandle fingerprints, equivalence/identity), as a read-only HTTP API + AffineScript UI wrapping the Skein.jl engine. Hosts the server-side KRL parser (server/krl/).""" -completion-percentage = 40 +completion-percentage = 55 [position] -phase = "initial" # design | implementation | testing | maintenance | archived +phase = "testing" # design | implementation | testing | maintenance | archived maturity = "experimental" # experimental | alpha | beta | production | lts [route-to-mvp] milestones = [ - # No milestones recorded + { id = "M-CI", name = "Mathematical core gated in CI", status = "done", landed = "2026-07-21", note = "PR #72: quandle axioms, Reidemeister invariance, BR-5 fuzz, EXPLAIN and TLA+ model check all run on every push; both new gate types negative-tested (a real failure exits non-zero)." }, + { id = "DB-6A-SQL", name = "DB-6 Phase A, SQL surface", status = "done", landed = "2026-06-01", note = "SQLite EXPLAIN QUERY PLAN over read-path SQL, mutation-guarded HTTP endpoint." }, + { id = "DB-6A-KRL", name = "DB-6 Phase A, KRL surface", status = "done", landed = "2026-07-28", note = "PR #86: `explain` keyword, KRLExplainStmt, structured plan with indexed + selectivity. Selectivity is an honest stub; plan_is_costed() is false until DB-3." }, + { id = "DB-3", name = "Secondary indexes + column histograms", status = "not-started", note = "Issue #33. Blocks DB-6 Phase B: real selectivity cannot exist without it." }, + { id = "DB-6B", name = "DB-6 Phase B, cost-based reordering", status = "blocked", blocked-by = "DB-3", note = "Deliberately not attempted. Reordering against uniform stub estimates would be arbitrary while appearing principled." }, ] [blockers-and-issues] issues = [ - # No blockers recorded + { id = "GUIX-GATE", severity = "high", scope = "estate", summary = "governance / Guix primary / Nix fallback policy fails: repo has flake.nix and no Guix artefact. NOT locally fixable in good faith — the gate is presence-only (checks a filename exists, never reads it), so a stub guix.scm would buy green with a lie. Measured estate-wide: 163 stub / 43 placeholder / 40 wrong-identity guix.scm files all pass today. Recommendation is to fix the GATE first.", evidence = "dev-notes/guix-policy-gate-advice-2026-07-28.md" }, + { id = "RULESET-ADMIN", severity = "medium", scope = "repo", summary = "Every merge to main requires --admin: the ruleset carries code_coverage minimum 95 on a repo with no coverage tooling (unsatisfiable), a code_scanning requirement on Scorecard (which never runs on a PR head, so the context is phantom), and copilot_code_review. Routine --admin bypass is how a genuinely failing gate stops being noticed.", remedy = "dev-notes/quandledb-ruleset-fix-2026-07-27.md + quandledb-ruleset-fixed.json (one gh api -X PUT)" }, + { id = "DOC-DRIFT", severity = "low", scope = "repo", summary = "READINESS.md (grade D, assessed 2026-04-05) cites src/api/*.v — no .v files and no src/api/ exist; it also lists EXPLAINME / TEST-NEEDS / PROOF-NEEDS as missing, all of which now exist. ARCHITECTURE.md is scaffold boilerplate describing directories this repo does not have.", tracked = "issue #74" }, + { id = "UNGATED-TIERS", severity = "medium", scope = "repo", summary = "Idris2 (src/abi), Zig (src/ffi) and AffineScript (frontend) have no CI gate at all. The Julia, BEAM, Agda and TLA+ tiers do.", tracked = "issue #73 covers the BEAM half, now closed" }, ] [critical-next-actions] actions = [ - # No actions recorded + { order = 1, action = "Merge open PRs in order: #85 (unblocks red main) then #86 (DB-6 KRL surface).", owner = "human", note = "Both require --admin until RULESET-ADMIN is fixed." }, + { order = 2, action = "Apply the ruleset fix so merges stop requiring --admin.", owner = "human", command = "gh api -X PUT repos/hyperpolymath/quandledb/rulesets/18110611 --input dev-notes/quandledb-ruleset-fixed.json" }, + { order = 3, action = "Decide the Guix gate question at estate level before touching this repo's packaging.", owner = "human", note = "Writing a stub guix.scm here would pass CI and be a lie. See GUIX-GATE." }, + { order = 4, action = "DB-3 (issue #33): secondary indexes + column histograms.", owner = "either", note = "The single highest-value next build: it unblocks DB-6 Phase B and turns plan_is_costed() true." }, + { order = 5, action = "Re-assess READINESS.md against the tree as it now stands.", owner = "either", tracked = "issue #74" }, ] [maintenance-status] -last-run-utc = "2026-02-13T00:00:00Z" -last-result = "unknown" # unknown | pass | warn | fail +last-run-utc = "2026-07-28T19:45:00Z" +last-result = "warn" # unknown | pass | warn | fail +# warn, not pass: every gate the repo owns is green (KRL Verification incl. +# the full Julia suite, Agda --safe, TLC, QD-12, CodeQL, Hypatia, gitleaks). +# The single red check is the estate-wide Guix policy gate — see GUIX-GATE +# above. It is not green-able here in good faith, so it is reported as a warn +# rather than suppressed. +zero-known-broken-markers = true +# As of 2026-07-28 the test suites carry NO @test_broken markers. The last one +# (BR-5 quandle_key crossing-order invariance, 11/200 mismatches) cleared when +# KnotTheory.jl#52 fixed link normalisation. Every marker this campaign added +# was removed by the upstream fix it was tracking, which is the mechanism +# working as intended: a marker that survives is a lie waiting to be told. diff --git a/docs/db-6-explain-strategy.md b/docs/db-6-explain-strategy.md index 6999528..3e865a9 100644 --- a/docs/db-6-explain-strategy.md +++ b/docs/db-6-explain-strategy.md @@ -4,7 +4,25 @@ Copyright (c) Jonathan D.A. Jewell --> # DB-6: EXPLAIN strategy for read-only API queries -Status: **Phase A landed 2026-06-01.** Phases B + C deferred. +Status: **both Phase A surfaces landed.** SQL-side 2026-06-01; KRL-side +2026-07-28 (issue #34). Phases B + C deferred. + +> **Two surfaces, one issue number — read this first.** +> +> "DB-6 Phase A" has meant two different things in this repo, which caused a +> real mis-assessment (the issue was believed closable when half of it had +> never been built): +> +> | Surface | What it is | Where | Landed | +> |---|---|---|---| +> | **SQL-side** | SQLite `EXPLAIN QUERY PLAN` over the read-path SQL, exposed on an HTTP endpoint | `server/query_explain.jl`, `handle_explain` in `server/serve.jl` | 2026-06-01 (this document's original scope) | +> | **KRL-side** | `explain` as a KRL keyword returning a structured plan with `indexed` and selectivity per filter | `server/krl/ExplainPlan.jl`, `KRLExplainStmt` | 2026-07-28 | +> +> Issue #34's acceptance criteria describe the **KRL-side** surface. Until +> 2026-07-28 only the SQL-side existed: `explain` appeared in neither +> `server/krl/Lexer.jl` nor `server/krl/Parser.jl`, and there was no +> selectivity model anywhere — not even the stub the criteria permit. +> Both now exist and are independently gated in CI. ## Goal @@ -126,3 +144,69 @@ Once that lands, the wrapper for `handle_knots` becomes one-line. - [hyperpolymath/quandledb#34](https://github.com/hyperpolymath/quandledb/issues/34) — DB-6 parent - [hyperpolymath/quandledb#33](https://github.com/hyperpolymath/quandledb/issues/33) — DB-3 Phase B + C parent (Skein.jl gap is shared) - [hyperpolymath/quandledb#42](https://github.com/hyperpolymath/quandledb/pull/42) — DB-3 Phase A (indexes that Phase A test 4 exercises) + + +--- + +## KRL-side EXPLAIN (landed 2026-07-28) + +### Syntax + +`explain` prefixes a pipeline query. It returns the **plan**; it does not run +the query. + +```krl +explain from knots | filter colouring_count_3 = 9 and crossing < 8 | take 5 +``` + +### Plan shape + +``` +{"op" => "scan", "table" => "knots"} +{"op" => "filter", "column" => "colouring_count_3", "comparator" => "=", "value" => 9, + "indexed" => true, "selectivity_estimate" => 0.5, "selectivity_source" => "stub"} +{"op" => "filter", "column" => "crossing", "comparator" => "<", "value" => 8, + "indexed" => false, "selectivity_estimate" => 0.5, "selectivity_source" => "stub"} +{"op" => "take", "n" => 5} +``` + +A conjunction becomes **separate** filter operations. That is deliberate: it is +what makes the Phase B reorder meaningful, since a reorder can only permute +operations the plan actually distinguishes. + +### Design decisions worth knowing + +**`explain` parses to its own statement type.** `KRLExplainStmt` is distinct +from `KRLQueryStmt` rather than a flag on it, so every existing consumer of +`KRLQueryStmt` still means "this query will actually execute" and cannot be +handed a plan where it expected rows. + +**Selectivity is a stub, and says so.** There are no column histograms yet — +that is DB-3 (#33), and the DB-6 criteria explicitly permit a stub until it +lands. Every estimate is `SELECTIVITY_STUB` (0.5) carrying +`"selectivity_source" => "stub"`, and `plan_is_costed(plan)` returns `false` +while any stub remains. **That predicate is the guard that stops Phase B +optimising against invented numbers** — a cost-based reorder driven by +uniform 0.5 estimates would be arbitrary while looking principled. + +**`indexed` is driven by a short explicit list.** `INDEXED_COLUMNS` names only +columns that genuinely carry a secondary index. An over-claiming list would +make `indexed` a fake signal, which is worse than reporting `false`. Extend it +as DB-3 lands real indexes — not before. + +**Predicates the plan cannot describe are not mis-described.** Column-to-column +comparisons, nested booleans and calls report `"predicate" => ""` +with no `column` key, rather than being given a fabricated column. + +### What is deliberately NOT done + +Phase B (cost-based reordering) is not attempted. The plan is returned in +**execution order as written**. Phase B needs real selectivity, i.e. DB-3. + +### Tests + +`server/krl/test/explain_test.jl` — 25 assertions, in the dependency-free CI +step (so it runs before `Pkg.instantiate` and cannot be masked by a dependency +breakage). Two of its testsets assert the *honesty* properties above rather +than the happy path: that selectivity is labelled a stub with +`plan_is_costed == false`, and that an undescribable predicate stays opaque.