Writing symbols as fixed-width blocks

A proof for a constraint graph is an assignment written out, one fixed-width block per vertex. This module supplies the block: any finite alphabet small enough is written as its index in binary, at a width the caller chooses.

The codec need not be computable — a verifier's decision has to be polynomial-time, but the correspondence between symbols and blocks is only used to state what the decision means.

Main definitions

• Complexity.symEnc, Complexity.symDec — the block of a symbol, and back

Main results

• Complexity.symDec_symEnc — the codec round-trips
• Complexity.length_symEnc — blocks have the chosen width

noncomputable def Complexity.symEnc (α : Type) [Fintype α] (w : ℕ) (s : α) : List Bool

The block a symbol occupies: its index, in binary, at width w.

Equations

• Complexity.symEnc α w s = Complexity.bitsOfLenLE w ↑((Fintype.equivFin α) s)

noncomputable def Complexity.symDec (α : Type) [Fintype α] [Inhabited α] (u : List Bool) : α

The symbol a block names.

Equations

• Complexity.symDec α u = if h : Complexity.binValLE u < Fintype.card α then (Fintype.equivFin α).symm ⟨Complexity.binValLE u, h⟩ else default

@[simp]

theorem Complexity.length_symEnc {α : Type} [Fintype α] (w : ℕ) (s : α) : (symEnc α w s).length = w

theorem Complexity.symDec_symEnc {α : Type} [Fintype α] [Inhabited α] {w : ℕ} (h : Fintype.card α ≤ 2 ^ w) (s : α) : symDec α (symEnc α w s) = s

The codec round-trips, as long as the width holds the alphabet.