structure Hex.GraphIso.Nauty.Sparse.CertCandidate (n : Nat) : Type

Untrusted sparse certificate data, including the production search's literal canonical label. The key and every tree record must pass replay.

• tree : CertNode
• key : Key n
• lab : Array Nat

def Hex.GraphIso.Nauty.Sparse.produceCand {n k : Nat} (G : Sparse.Colored n k) : Option (CertCandidate n)

Run the optimized search once, then expand proof subtrees against its installed key. The native label and tie order are retained literally.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.produceCand_eq {n k : Nat} (G : Sparse.Colored n k) : produceCand G = some { tree := produceRoot G (canonSpecKey G), key := canonSpecKey G, lab := (runColored G).canonlab }

The unlimited producer succeeds with the actual production label and the proved canonical maximum. This uses unconditional production correctness.

theorem Hex.GraphIso.Nauty.Sparse.produceCand_isSome {n k : Nat} (G : Sparse.Colored n k) : (produceCand G).isSome = true

theorem Hex.GraphIso.Nauty.Sparse.produceCand_replays {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} (h : produceCand G = some c) : checkKey G c.tree c.key = true

theorem Hex.GraphIso.Nauty.Sparse.produceCand_key {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} (h : produceCand G = some c) : c.key = canonSpecKey G

theorem Hex.GraphIso.Nauty.Sparse.produceCand_label {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} (h : produceCand G = some c) : c.lab = (runColored G).canonlab

def Hex.GraphIso.Nauty.Sparse.validateKey? {n k : Nat} (G : Sparse.Colored n k) (c : CertCandidate n) : Option (Key n)

Validate an untrusted candidate through a single native sparse replay.

Equations

• Hex.GraphIso.Nauty.Sparse.validateKey? G c = if Hex.GraphIso.Nauty.Sparse.checkKey G c.tree c.key = true then some c.key else none

theorem Hex.GraphIso.Nauty.Sparse.validateKey?_sound {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} {B : Key n} (h : validateKey? G c = some B) : canonSpecKey G = B

def Hex.GraphIso.Nauty.Sparse.certifyKey? {n k : Nat} (G : Sparse.Colored n k) : Option (Key n)

Produce and check a sparse key. No-limit failure is excluded by the producer completeness theorem, independently of any trust in compiled code.

Equations

• Hex.GraphIso.Nauty.Sparse.certifyKey? G = (Hex.GraphIso.Nauty.Sparse.produceCand G).bind (Hex.GraphIso.Nauty.Sparse.validateKey? G)

theorem Hex.GraphIso.Nauty.Sparse.certifyKey?_eq {n k : Nat} (G : Sparse.Colored n k) : certifyKey? G = some (canonSpecKey G)