diff --git a/.github/workflows/krl-verification.yml b/.github/workflows/krl-verification.yml index f465747..14177ed 100644 --- a/.github/workflows/krl-verification.yml +++ b/.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 diff --git a/server/quandle_semantic.jl b/server/quandle_semantic.jl index f0a779b..21342d7 100644 --- a/server/quandle_semantic.jl +++ b/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( diff --git a/server/test_quandle_axioms.jl b/server/test_quandle_axioms.jl index cafc31b..6a88384 100644 --- a/server/test_quandle_axioms.jl +++ b/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)