hyperpolymath · hyperpolymath · Jul 29, 2026 · Jul 29, 2026
diff --git 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
@@ -4,7 +4,25 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # 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" => "<expression>"`
+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.
diff --git a/server/test_br5_fuzz.jl b/server/test_br5_fuzz.jl
@@ -120,23 +120,13 @@ end
 
 @testset "BR-5: crossing-order invariance on random braid words" begin
     rng = MersenneTwister(BR5_SEED + 1)
-    # 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.
+    # Crossing-order invariance of quandle_key, including its polynomial
+    # segments. This was @test_broken at 11/200: every mismatch was a
+    # multi-component LINK (knots were already invariant at 0/102). Upstream
+    # KnotTheory.jl#51/#52 fixed both causes — an exponent window that could
+    # not be canonicalised for odd spans, and a Conway expansion that emitted
+    # even powers of z for links that require odd ones. Measured after that
+    # merge: 0 mismatches over 200 trials, links and knots alike.
     quandle_key_mismatches = 0
     for trial in 1:BR5_TRIALS
         nstrands = rand(rng, 3:4)
@@ -156,8 +146,8 @@ end
         end
     end
     quandle_key_mismatches > 0 &&
-        @info "BR-5 quandle_key order-sensitivity (known-broken)" quandle_key_mismatches BR5_TRIALS
-    @test_broken quandle_key_mismatches == 0
+        @info "BR-5 quandle_key order-sensitivity" quandle_key_mismatches BR5_TRIALS
+    @test quandle_key_mismatches == 0
 end
 
 # ---------------------------------------------------------------------------