structure Hex.GraphIso.ReplayLimits : Type

Limits on certificate and permutation replay.

• maxKernelSteps : Nat

  The largest number of checker steps performed before exhaustion. One step is charged for each proof-rule record, vertex or permutation entry inspected, and dense adjacency word inspected.

def Hex.GraphIso.instDecidableEqReplayLimits.decEq (x✝ x✝¹ : ReplayLimits) : Decidable (x✝ = x✝¹)

Equations

• Hex.GraphIso.instDecidableEqReplayLimits.decEq { maxKernelSteps := a } { maxKernelSteps := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.GraphIso.instDecidableEqReplayLimits : DecidableEq ReplayLimits

Equations

• Hex.GraphIso.instDecidableEqReplayLimits = Hex.GraphIso.instDecidableEqReplayLimits.decEq

def Hex.GraphIso.checkCost (n : Nat) : Nat

The step charge of one permutation check: each vertex colour and each vertex pair inspected.

Equations

• Hex.GraphIso.checkCost n = n + n * n

def Hex.GraphIso.checkIso? {n k : Nat} (replay : ReplayLimits) (G H : Colored n k) (p : Perm n) : Option Bool

Bounded isomorphism check. none is replay exhaustion.

Equations

• Hex.GraphIso.checkIso? replay G H p = if Hex.GraphIso.checkCost n ≤ replay.maxKernelSteps then some (Hex.GraphIso.checkIso G H p) else none

theorem Hex.GraphIso.checkIso?_some {n k : Nat} {replay : ReplayLimits} {G H : Colored n k} {p : Perm n} {b : Bool} (h : checkIso? replay G H p = some b) : b = true ↔ IsIso G H p