Writing out an encoded bit list

DataEncode serializes a list of booleans as a substitution cipher inside one pair of brackets: false becomes 01 and true becomes 0011. Producing that is a fold over the list, which recFoldClamp runs in polynomial time.

Since a natural number is encoded as its Nat.bits, this is also the last step of encoding a number: count the value out in binary, drop the trailing zeros, and run the cipher.

Main definitions

• Complexity.boolBits — the two-symbol cipher

Main results

• Complexity.bitstringEncode_list — the cipher describes the encoding
• Complexity.flatBitsFn_mem_FP — running it is polynomial time
• Complexity.natEncodeFn_eq — a number's encoding, from its value in unary

def Complexity.boolBits (b : Bool) : List Bool

The serialization of a single boolean.

Equations

• Complexity.boolBits b = if b = true then [false, false, true, true] else [false, true]

theorem Complexity.boolBits_eq (b : Bool) : boolBits b = (DataEncode.encode b).toBits

@[simp]

theorem Complexity.length_boolBits (b : Bool) : (boolBits b).length ≤ 4

theorem Complexity.bitstringEncode_list (l : List Bool) : DataEncode.bitstringEncode l = false :: List.flatMap boolBits l ++ [true]

The cipher describes the encoding.

Running the cipher

def Complexity.blitZero (z : List Bool) : List Bool

The fold step on a zero.

Equations

• Complexity.blitZero z = [false, true] ++ Complexity.pairSnd (Complexity.pairFst z)

def Complexity.blitOne (z : List Bool) : List Bool

The fold step on a one.

Equations

• Complexity.blitOne z = [false, false, true, true] ++ Complexity.pairSnd (Complexity.pairFst z)

theorem Complexity.blitZero_mem_FP : blitZero ∈ FP

theorem Complexity.blitOne_mem_FP : blitOne ∈ FP

theorem Complexity.length_flatMap_boolBits (l : List Bool) : (List.flatMap boolBits l).length ≤ 4 * l.length

theorem Complexity.recFoldClamp_flatBits (bound : ℕ) (W l : List Bool) : 4 * l.length ≤ bound → Cobham.recFoldClamp blitZero blitOne bound [] W l = List.flatMap boolBits l

def Complexity.flatBitsFn (z : List Bool) : List Bool

The cipher applied to pairSnd z.

Equations

• Complexity.flatBitsFn z = Complexity.Cobham.recFoldClamp Complexity.blitZero Complexity.blitOne (4 * z.length) [] (Complexity.pairFst z) (Complexity.pairSnd z)

theorem Complexity.flatBitsFn_mem_FP : flatBitsFn ∈ FP

theorem Complexity.flatBitsFn_eq (z : List Bool) : flatBitsFn z = List.flatMap boolBits (pairSnd z)

def Complexity.encodeListFn (z : List Bool) : List Bool

The encoding of a bit list, in polynomial time.

Equations

• Complexity.encodeListFn z = false :: Complexity.flatBitsFn z ++ [true]

theorem Complexity.encodeListFn_mem_FP : encodeListFn ∈ FP

theorem Complexity.encodeListFn_eq (z : List Bool) : encodeListFn z = DataEncode.bitstringEncode (pairSnd z)

A number's own encoding

noncomputable def Complexity.natEncodeFn (z : List Bool) : List Bool

The encoding of a natural number, from a width and a value both given in unary.

Equations

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

theorem Complexity.natEncodeFn_mem_FP : natEncodeFn ∈ FP

theorem Complexity.natEncodeFn_eq {z : List Bool} (h : (pairSnd z).length < 2 ^ (pairFst z).length) : natEncodeFn z = DataEncode.bitstringEncode (pairSnd z).length

It really is the number's encoding, whenever the width holds the value.