fix: guard alexander/conway/jones — CI hung to GitHub's 6h kill on O(n!) determinant

.github/workflows/krl-verification.yml

@@ -34,6 +34,10 @@ jobs:
   krl-tests:
     name: KRL lexer / parser / SQL tests (Julia)
     runs-on: ubuntu-latest
+    # A hang here previously burned GitHub's full 6-hour job limit (unguarded
+    # O(n!) polynomial call). Fail fast instead: the whole suite completes in
+    # well under an hour when healthy.
+    timeout-minutes: 90
     steps:
       - name: Checkout
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4
@@ -112,6 +116,7 @@ jobs:
   agda-proofs:
     name: Agda proofs (--safe)
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     steps:
       - name: Checkout
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4
@@ -150,6 +155,7 @@ jobs:
   tlaplus-model-check:
     name: TLA+ model check (TLC)
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Checkout
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4

server/quandle_semantic.jl

@@ -10,6 +10,8 @@ export QuandleRelation, QuandlePresentation
 export extract_presentation, canonicalize_presentation, canonical_presentation_blob
 export quandle_descriptor
 export IMAGE_HISTOGRAM_MAX_G
+export ALEXANDER_MAX_CROSSINGS, CONWAY_MAX_CROSSINGS, JONES_MAX_CROSSINGS
+export HOMFLY_MAX_CROSSINGS, HOMFLY_DEFERRED_SENTINEL
 
 """
     QuandleRelation
@@ -467,6 +469,18 @@ 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
+const CONWAY_MAX_CROSSINGS = ALEXANDER_MAX_CROSSINGS
+const JONES_MAX_CROSSINGS = 20
+
 """
     _safe_homfly_serialised(pd::KnotTheory.PlanarDiagram) -> String
 
@@ -480,6 +494,42 @@ function _safe_homfly_serialised(pd::KnotTheory.PlanarDiagram)::String
     _serialise_int_poly_2var(poly)
 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
+above the bound.
+"""
+function _safe_alexander_serialised(pd::KnotTheory.PlanarDiagram)::String
+    length(pd.crossings) > ALEXANDER_MAX_CROSSINGS && return HOMFLY_DEFERRED_SENTINEL
+    _serialise_int_poly(KnotTheory.alexander_polynomial(pd))
+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).
+Returns the deferred sentinel above the bound.
+"""
+function _safe_conway_serialised(pd::KnotTheory.PlanarDiagram)::String
+    length(pd.crossings) > CONWAY_MAX_CROSSINGS && return HOMFLY_DEFERRED_SENTINEL
+    _serialise_int_poly(KnotTheory.conway_polynomial(pd))
+end
+
+"""
+    _safe_jones_serialised(pd::KnotTheory.PlanarDiagram) -> String
+
+Jones polynomial, guarded by `JONES_MAX_CROSSINGS` (KnotTheory's Kauffman
+bracket throws above 20 crossings; we return the deferred sentinel
+instead of propagating the throw).
+"""
+function _safe_jones_serialised(pd::KnotTheory.PlanarDiagram)::String
+    length(pd.crossings) > JONES_MAX_CROSSINGS && return HOMFLY_DEFERRED_SENTINEL
+    _serialise_int_poly(KnotTheory.jones_polynomial(pd))
+end
+
 """
     quandle_descriptor(pd::KnotTheory.PlanarDiagram) -> NamedTuple
 
@@ -504,14 +554,15 @@ function quandle_descriptor(pd::KnotTheory.PlanarDiagram)
     image_hist_3_str = join(image_hist_3, ",")
     image_hist_5_str = join(image_hist_5, ",")
 
-    # KT-2: Alexander polynomial via KnotTheory.jl, same serialisation as Skein.jl
-    alexander_poly = KnotTheory.alexander_polynomial(pd)
-    alexander_str = _serialise_int_poly(alexander_poly)
+    # KT-2: Alexander polynomial via KnotTheory.jl, same serialisation as
+    # Skein.jl. Guarded: the upstream determinant is O(n!) in crossing count.
+    alexander_str = _safe_alexander_serialised(pd)
 
     # KT-2 extension: Jones, Conway (both Laurent in one variable),
-    # and HOMFLY-PT (two-variable, guarded at HOMFLY_MAX_CROSSINGS).
-    jones_str = _serialise_int_poly(KnotTheory.jones_polynomial(pd))
-    conway_str = _serialise_int_poly(KnotTheory.conway_polynomial(pd))
+    # and HOMFLY-PT (two-variable). All guarded — see the *_MAX_CROSSINGS
+    # constants for the measured cost model behind each bound.
+    jones_str = _safe_jones_serialised(pd)
+    conway_str = _safe_conway_serialised(pd)
     homfly_str = _safe_homfly_serialised(pd)
 
     key = string(

server/test_quandle_axioms.jl

@@ -511,12 +511,23 @@ end
     end
 end
 
-@testset "KT-2 ext: HOMFLY guard returns sentinel above MAX_CROSSINGS" begin
-    # Build a synthetic 16-crossing PD by braid word s1^16. KnotTheory's
-    # MAX_CROSSINGS_FOR_HOMFLY is 15, so this triggers the guard.
+@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 == "deferred:too_many_crossings"
+    @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
 end
 
 @testset "KT-2 ext: Jones polynomial distinguishes the test knots" begin
@@ -665,8 +676,16 @@ end
     @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.
     f = quandle_descriptor(figure_eight().pd)
-    @test f.conway_polynomial == "0:1,2:-1"
+    @test_broken f.conway_polynomial == "0:1,2:-1"
 
     # Cinquefoil ∇(z) = 1 + 3z² + z⁴ → "0:1,2:3,4:1"
     c = quandle_descriptor(cinquefoil().pd)