List-backed affine-cover tree data

AffineCover.CoverTree uses a function Fin arity → CoverTree m for the children of a branch. That representation is convenient for the checker and its soundness proof, but awkward for generated certificate files. This module provides a small passive input type whose branch children are ordinary lists.

Decoding is a fuelled structural traversal and returns an Option. Consequently no claim about an external emitter or parser enters the trusted argument: under-fuelled data is rejected, and an accepted value is first converted to the already-proved CoverTree checker. An emitter may use any easy upper bound on tree depth, such as the number of witness commands.

inductive Utilities.Certificate.AffineCover.CoverTreeData : Type

Passive, emitter-friendly covering-tree data with list-backed branches.

• leaf (farkas : FarkasData) : CoverTreeData
• empty (cone : ℕ) : CoverTreeData
• skip (cone form : ℕ) (next : CoverTreeData) : CoverTreeData
• branch (cone : ℕ) (children : List CoverTreeData) : CoverTreeData

def Utilities.Certificate.AffineCover.CoverTreeData.decodeFuel (m a✝ : ℕ) : CoverTreeData → Option (CoverTree m)

Fuelled structural conversion from list-backed data to the function-backed trusted tree. Every recursive child conversion consumes one unit of fuel.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.AffineCover.CoverTreeData.decodeFuel m 0 x✝ = none

def Utilities.Certificate.AffineCover.CoverTreeData.decode (data : CoverTreeData) (m fuel : ℕ) : Option (CoverTree m)

Attempt to decode list-backed data using the advertised depth bound.

Equations

• data.decode m fuel = Utilities.Certificate.AffineCover.CoverTreeData.decodeFuel m fuel data

def Utilities.Certificate.AffineCover.CoverTreeData.ValidActive {m : ℕ} (cones : List (List (AffineForm m))) (active : List (AffineForm m)) : ℕ → CoverTreeData → Prop

Direct propositional validity of list-backed data under the currently active rows. Fuel is consumed once at every level, exactly as in decodeFuel, but no intermediate function-backed tree is constructed.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.AffineCover.CoverTreeData.ValidActive cones active 0 x✝ = False
• Utilities.Certificate.AffineCover.CoverTreeData.ValidActive cones active _fuel.succ (Utilities.Certificate.AffineCover.CoverTreeData.leaf farkas) = farkas.Valid active

def Utilities.Certificate.AffineCover.CoverTreeData.checkActive {m : ℕ} (cones : List (List (AffineForm m))) (active : List (AffineForm m)) : ℕ → CoverTreeData → Bool

Direct Boolean replay of list-backed data. This deliberately fuses decoding and checking: generated trees remain ordinary lists all the way down, so kernel reduction never materializes a large function-backed tree.

Equations

• One or more equations did not get rendered due to their size.
• Utilities.Certificate.AffineCover.CoverTreeData.checkActive cones active 0 x✝ = false
• Utilities.Certificate.AffineCover.CoverTreeData.checkActive cones active _fuel.succ (Utilities.Certificate.AffineCover.CoverTreeData.leaf farkas) = farkas.check active

def Utilities.Certificate.AffineCover.CoverTreeData.Valid {m : ℕ} (data : CoverTreeData) (fuel : ℕ) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) : Prop

Propositional validity of list-backed data, stated directly on the passive representation checked by the kernel.

Equations

• data.Valid fuel base cones = Utilities.Certificate.AffineCover.CoverTreeData.ValidActive cones base fuel data

def Utilities.Certificate.AffineCover.CoverTreeData.check {m : ℕ} (data : CoverTreeData) (fuel : ℕ) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) : Bool

Executable checker for list-backed covering data.

Equations

• data.check fuel base cones = Utilities.Certificate.AffineCover.CoverTreeData.checkActive cones base fuel data

@[simp]

theorem Utilities.Certificate.AffineCover.CoverTreeData.check_eq_true_iff {m : ℕ} (data : CoverTreeData) (fuel : ℕ) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) : data.check fuel base cones = true ↔ data.Valid fuel base cones

The list-backed checker implements exactly CoverTreeData.Valid.

theorem Utilities.Certificate.AffineCover.CoverTreeData.covers_of_check_eq_true {m : ℕ} (data : CoverTreeData) (fuel : ℕ) (base : List (AffineForm m)) (cones : List (List (AffineForm m))) (hCheck : data.check fuel base cones = true) : Covers base cones

Soundness of the passive list-backed layer: accepted data proves integral coverage through the existing CoverTree soundness theorem.

A small closed example

def Utilities.Certificate.AffineCover.Examples.strictPartitionTreeData : CoverTreeData

List-backed spelling of the strict two-cone partition example from AffineCover. Child-list position is the corresponding cone-form index.

Equations

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

theorem Utilities.Certificate.AffineCover.Examples.strictPartitionTreeData_check : strictPartitionTreeData.check 3 [] strictPartitionCones = true

theorem Utilities.Certificate.AffineCover.Examples.strictPartitionTreeData_underFuel_rejected : strictPartitionTreeData.check 2 [] strictPartitionCones = false

Decoding is fail-closed when the advertised depth bound is too small.

theorem Utilities.Certificate.AffineCover.Examples.badConeIndex_rejected : (CoverTreeData.empty 2).check 1 [] strictPartitionCones = false

An out-of-range cone index is rejected before it can use getD's default empty cone.

theorem Utilities.Certificate.AffineCover.Examples.badFormIndex_rejected : (CoverTreeData.skip 0 1 (CoverTreeData.empty 0)).check 2 [] strictPartitionCones = false

An out-of-range form index is rejected before it can use getD's default zero form.

theorem Utilities.Certificate.AffineCover.Examples.strictPartitionDataCovers : Covers [] strictPartitionCones

Kernel-checked coverage obtained through the list-backed data layer.