Machine-facing encoding of width-five branching programs

This file defines a deterministic, proof-free bit format for the width-5 permutation branching programs produced by Barrington's theorem. Permutations are represented by their rank in the computable S₅ enumeration, using seven bits because |S₅| = 120 < 2^7. Variable indices and the instruction count use the existing terminated-unary circuit codec.

An instruction is encoded as its variable field followed by two fixed-width permutation fields. A program starts with its instruction count, so exact decoding rejects truncation and trailing garbage.

def Complexity.BPCode.Perm5.bitWidth : ℕ

Number of bits in the canonical rank encoding of an S₅ permutation.

Equations

• Complexity.BPCode.Perm5.bitWidth = 7

def Complexity.BPCode.Perm5.table : List (Equiv.Perm (Fin 5))

The fixed computable table used to rank and unrank S₅.

Equations

• Complexity.BPCode.Perm5.table = Complexity.allPermutationsFin 5

def Complexity.BPCode.Perm5.index (permutation : Equiv.Perm (Fin 5)) : ℕ

The canonical table position of a permutation.

Equations

• Complexity.BPCode.Perm5.index permutation = List.idxOf permutation Complexity.BPCode.Perm5.table

def Complexity.BPCode.Perm5.encode (permutation : Equiv.Perm (Fin 5)) : List Bool

Encode an S₅ permutation by its seven-bit table position.

Equations

• Complexity.BPCode.Perm5.encode permutation = Complexity.BPCode.Perm5.bitWidth.toBits (Complexity.BPCode.Perm5.index permutation)

def Complexity.BPCode.Perm5.decodePrefix? (bits : List Bool) : Option (Equiv.Perm (Fin 5) × List Bool)

Decode one fixed-width permutation field and return the unused suffix.

Equations

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

def Complexity.BPCode.Instr.encode (instruction : BPInstr 5) : List Bool

Encode one width-5 instruction as a terminated-unary variable followed by its two seven-bit permutation ranks.

Equations

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

def Complexity.BPCode.Instr.decodePrefix? (bits : List Bool) : Option (BPInstr 5 × List Bool)

Decode one instruction prefix and return the unused suffix.

Equations

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

def Complexity.BPCode.Program.decodeInstructions? : ℕ → List Bool → Option (BP 5 × List Bool)

Decode exactly count instruction prefixes and return the unused suffix.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BPCode.Program.decodeInstructions? 0 x✝ = some ([], x✝)

def Complexity.BPCode.Program.encode (program : BP 5) : List Bool

Canonically encode a width-5 branching program.

Equations

• Complexity.BPCode.Program.encode program = Complexity.CircuitCode.NatCode.encode (List.length program) ++ List.flatMap Complexity.BPCode.Instr.encode program

def Complexity.BPCode.Program.decodePrefix? (bits : List Bool) : Option (BP 5 × List Bool)

Decode one complete program prefix and return the unused suffix.

Equations

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

def Complexity.BPCode.Program.decode? (bits : List Bool) : Option (BP 5)

Decode exactly one width-5 branching program. Trailing bits are rejected.

Equations

• Complexity.BPCode.Program.decode? bits = match Complexity.BPCode.Program.decodePrefix? bits with | some (program, []) => some program | x => none