diff --git a/.github/workflows/krl-verification.yml b/.github/workflows/krl-verification.yml index 64098c4..1c46128 100644 --- a/.github/workflows/krl-verification.yml +++ b/.github/workflows/krl-verification.yml @@ -38,11 +38,14 @@ jobs: - name: Checkout uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 - - name: Install Julia 1.10 + # Julia >= 1.11 is required: server/Project.toml uses a [sources] table + # (path-resolved sibling deps), which Pkg 1.10 silently ignores — the + # instantiate then fails with "expected package … to be registered". + - name: Install Julia 1.12 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 + sh "$RUNNER_TEMP/juliaup-init.sh" --yes --default-channel 1.12 echo "$HOME/.juliaup/bin" >> "$GITHUB_PATH" - name: Julia version diff --git a/server/quandle_semantic.jl b/server/quandle_semantic.jl index daaf6a9..f0a779b 100644 --- a/server/quandle_semantic.jl +++ b/server/quandle_semantic.jl @@ -142,7 +142,7 @@ Two presentations produce the same canonical form iff they represent the same presentation up to generator renaming. This is the basis for `canonical_presentation_blob`'s fingerprint. """ -function canonicalize_presentation(p::QuandlePresentation)::QuandlePresentation +function _canonicalize_pass(p::QuandlePresentation)::QuandlePresentation sorted_rel = sort(p.relations, by = r -> (r.lhs, r.rhs, r.out, r.is_inverse ? 1 : 0)) mapping = Dict{Int, Int}() @@ -172,6 +172,51 @@ function canonicalize_presentation(p::QuandlePresentation)::QuandlePresentation QuandlePresentation(p.generator_count, canon_rel) end +""" + canonicalize_presentation(p::QuandlePresentation) -> QuandlePresentation + +Idempotent canonicalisation. A single relabel-and-resort pass is not +idempotent: it relabels by first appearance in the *old* ordering and then +re-sorts under the *new* labels, so a second pass can see a different order +and relabel again. Iterating the pass from any start eventually enters a +cycle (finite deterministic orbit); every member of that cycle reaches the +same cycle again, so returning the cycle's lexicographically-minimal +serialisation is a true fixpoint: canonicalize(canonicalize(p)) == +canonicalize(p). Where the single pass was already stable (the common case, +and everything previously stored) the result is unchanged. +""" +function canonicalize_presentation(p::QuandlePresentation)::QuandlePresentation + order = String[] + states = Dict{String, QuandlePresentation}() + cur = p + while true + cur = _canonicalize_pass(cur) + s = _presentation_serial(cur) + if haskey(states, s) + i = findfirst(==(s), order) + cycle = order[i:end] + return states[minimum(cycle)] + end + push!(order, s) + states[s] = cur + end +end + +""" + _presentation_serial(c::QuandlePresentation) -> String + +Serialise a presentation as `qpres-v1|g=|r=lhs,rhs,out,sign;...` without +hashing. `canonical_presentation_blob` hashes this for canonical forms. +""" +function _presentation_serial(c::QuandlePresentation)::String + rel_tokens = String[] + for r in c.relations + sign_flag = r.is_inverse ? -1 : 1 + push!(rel_tokens, string(r.lhs, ",", r.rhs, ",", r.out, ",", sign_flag)) + end + string("qpres-v1|g=", c.generator_count, "|r=", join(rel_tokens, ";")) +end + """ canonical_presentation_blob(p::QuandlePresentation) -> String @@ -184,13 +229,7 @@ generator renaming). This blob is the input to SHA-256 fingerprinting in `quandle_descriptor`. """ function canonical_presentation_blob(p::QuandlePresentation)::String - c = canonicalize_presentation(p) - rel_tokens = String[] - for r in c.relations - sign_flag = r.is_inverse ? -1 : 1 - push!(rel_tokens, string(r.lhs, ",", r.rhs, ",", r.out, ",", sign_flag)) - end - blob = string("qpres-v1|g=", c.generator_count, "|r=", join(rel_tokens, ";")) + blob = _presentation_serial(canonicalize_presentation(p)) # Compute BLAKE3 hash of the blob ctx = Blake3Hash.Blake3Ctx() Blake3Hash.update!(ctx, Vector{UInt8}(blob)) diff --git a/server/test_quandle_axioms.jl b/server/test_quandle_axioms.jl index 97535d0..cafc31b 100644 --- a/server/test_quandle_axioms.jl +++ b/server/test_quandle_axioms.jl @@ -209,12 +209,7 @@ end d_canonical = quandle_descriptor(trefoil_canonical) @test d_simplified.colouring_count_3 == d_canonical.colouring_count_3 - # KNOWN-BROKEN (upstream): KnotTheory.jl r2_simplify removes the bigon - # without re-splicing the severed arcs, leaving 4 arc labels that occur - # only once; the extracted presentation then has 5 generators instead - # of 3 and c5 comes out 25 instead of 5. Flips to "unexpected pass" - # (forcing removal of this marker) once the upstream fix lands. - @test_broken d_simplified.colouring_count_5 == d_canonical.colouring_count_5 + @test d_simplified.colouring_count_5 == d_canonical.colouring_count_5 end end