Self-delimiting blocks

To concatenate binary strings into a single binary string, each piece must announce its own end. This file defines the library's single framing operation and its parsers:

• delimit frames a payload: each payload bit is doubled (false ↦ [false, false], true ↦ [true, true]) and the block is terminated by the separator [false, true], which no run of doubled bits can produce.
• unpair? parses one block off the front of the input, returning the payload and the remaining suffix (none on malformed input). It is named for its role in the pairing codec Complexity.pair (see Complexitylib.Encoding.Pairing), which is pair x y = delimit x ++ y.
• undelimitBlock, takeFirstBlock, hasBlock, tagBlock, and undelimitBlocks are the total helper functions machines compute when working with framed data.

This file deliberately has no dependency on the machine or complexity-class layers, so the machine-input pairing codec (Complexitylib.Encoding.Pairing) can build on it without import cycles.

def Complexity.delimit (x : List Bool) : List Bool

Frame a binary string as a self-delimiting block: each payload bit is doubled (false ↦ [false, false], true ↦ [true, true]) and the block is terminated by the separator [false, true], which no run of doubled bits can produce.

Equations

• Complexity.delimit x = List.flatMap (fun (b : Bool) => [b, b]) x ++ [false, true]

@[simp]

theorem Complexity.delimit_nil : delimit [] = [false, true]

@[simp]

theorem Complexity.delimit_cons (b : Bool) (l : List Bool) : delimit (b :: l) = b :: b :: delimit l

@[simp]

theorem Complexity.delimit_length (l : List Bool) : (delimit l).length = 2 * l.length + 2

def Complexity.unpair? : List Bool → Option (List Bool × List Bool)

Parse one self-delimiting block off the front of the input. It scans doubled bits until the first separator [false, true], returning the decoded payload together with the remaining suffix. Invalid doubled prefixes return none.

Equations

• Complexity.unpair? [] = none
• Complexity.unpair? (false :: true :: y) = some ([], y)
• Complexity.unpair? (false :: false :: z) = Option.map (fun (xy : List Bool × List Bool) => (false :: xy.fst, xy.snd)) (Complexity.unpair? z)
• Complexity.unpair? (true :: true :: z) = Option.map (fun (xy : List Bool × List Bool) => (true :: xy.fst, xy.snd)) (Complexity.unpair? z)
• Complexity.unpair? x✝ = none

@[simp]

theorem Complexity.unpair?_delimit_append (x y : List Bool) : unpair? (delimit x ++ y) = some (x, y)

unpair? reads back the framing written by delimit: parsing one block off the front of any input recovers the payload and the remaining suffix.

theorem Complexity.eq_delimit_append_of_unpair?_eq_some {z x y : List Bool} : unpair? z = some (x, y) → z = delimit x ++ y

Soundness of the parser: a successful parse decomposes the input as the parsed payload's framing followed by the leftover suffix.

def Complexity.undelimitBlock : List Bool → List Bool

Strip the framing of a single self-delimiting block, returning its payload. On delimit P this returns P. Unlike unpair?, this is total: it ignores any data trailing the first block and maps malformed input to [].

Equations

• Complexity.undelimitBlock (false :: true :: tail) = []
• Complexity.undelimitBlock (false :: false :: rest) = false :: Complexity.undelimitBlock rest
• Complexity.undelimitBlock (true :: head :: rest) = true :: Complexity.undelimitBlock rest
• Complexity.undelimitBlock x✝ = []

@[simp]

theorem Complexity.undelimitBlock_delimit (P : List Bool) : undelimitBlock (delimit P) = P

def Complexity.takeFirstBlock : List Bool → List Bool

Keep the leading self-delimiting block of a bitstring, dropping everything after it. On a pair encoding delimit x ++ w this returns delimit x.

Equations

• Complexity.takeFirstBlock (false :: true :: tail) = [false, true]
• Complexity.takeFirstBlock (false :: false :: rest) = false :: false :: Complexity.takeFirstBlock rest
• Complexity.takeFirstBlock (true :: head :: rest) = true :: head :: Complexity.takeFirstBlock rest
• Complexity.takeFirstBlock x✝ = x✝

@[simp]

theorem Complexity.takeFirstBlock_delimit_append (P Q : List Bool) : takeFirstBlock (delimit P ++ Q) = delimit P

def Complexity.hasBlock : List Bool → Bool

Does the bitstring begin with a well-formed self-delimiting block?

Equations

• Complexity.hasBlock (false :: true :: tail) = true
• Complexity.hasBlock (false :: false :: rest) = Complexity.hasBlock rest
• Complexity.hasBlock (true :: true :: rest) = Complexity.hasBlock rest
• Complexity.hasBlock x✝ = false

theorem Complexity.hasBlock_eq_isSome_unpair? (l : List Bool) : hasBlock l = (unpair? l).isSome

def Complexity.tagBlock (l : List Bool) : List Bool

Tag a bitstring with a leading true if it begins with a well-formed self-delimiting block, and return the empty bitstring otherwise. On pair encodings this computes encode ∘ decode.

Equations

• Complexity.tagBlock l = bif Complexity.hasBlock l then true :: l else []

def Complexity.undelimitBlocksAux : ℕ → List Bool → Option (List (List Bool))

Parse a sequence of self-delimiting blocks, using fuel to bound the number of blocks.

This is the auxiliary, fuel-carrying implementation of undelimitBlocks; since every block is nonempty, input.length is always enough fuel.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.undelimitBlocksAux x✝ [] = some []
• Complexity.undelimitBlocksAux 0 (head :: tail) = none

def Complexity.undelimitBlocks (input : List Bool) : Option (List (List Bool))

Parse a sequence of self-delimiting blocks off the front of the input.

Since every block is nonempty, input.length bounds the number of blocks, so it always suffices as fuel for undelimitBlocksAux.

Equations

• Complexity.undelimitBlocks input = Complexity.undelimitBlocksAux input.length input

theorem Complexity.length_le_length_flatten_delimit (l : List (List Bool)) : l.length ≤ (List.map delimit l).flatten.length

theorem Complexity.undelimitBlocks_flatten_delimit (l : List (List Bool)) : undelimitBlocks (List.map delimit l).flatten = some l