Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions .github/workflows/krl-verification.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
55 changes: 47 additions & 8 deletions server/quandle_semantic.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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}()
Expand Down Expand Up @@ -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=<n>|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

Expand All @@ -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))
Expand Down
7 changes: 1 addition & 6 deletions server/test_quandle_axioms.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading