Documentation

Complexity.Computability.BitString.Padding

Self-delimiting padding of bounded words #

The machine calculus's existing frame encoding makes bounded words equally long without identifying distinct words. Words longer than the bound retain their complete frame. This representation bridge is separate from the pure bit-string foundations and from its polynomial-time certificate in Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean.

Main definitions #

Main results #

References #

Adapted from Computability/Probabilistic/BitString.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing tidy machine frame encoding.

source
def Cslib.BitString.padWord (bound : ℕ) (word : List Bool) :
List Bool

Pad a framed word to 2 * bound + 1 bits when it fits. Longer words are not truncated.

Instances For
    source
    theorem Cslib.BitString.word_eq_of_padWord_eq {bound bound' : ℕ} {word word' : List Bool} (h : padWord bound word = padWord bound' word') :
    word = word'

    Padding never identifies distinct words, even when their bounds differ.

    source
    theorem Cslib.BitString.length_padWord {bound : ℕ} {word : List Bool} (h : word.length ≤ bound) :
    (padWord bound word).length = 2 * bound + 1

    Every word within the supplied bound has the same padded length.

    source
    theorem Cslib.BitString.length_flatten_padWord (bound : ℕ) (words : List (List Bool)) (hbound : ∀ word ∈ words, word.length ≤ bound) :
    (List.map (padWord bound) words).flatten.length = words.length * (2 * bound + 1)

    Concatenating bounded, padded words has a length determined solely by their count.

    source
    theorem Cslib.BitString.word_eq_of_paddedBits_eq {bound : ℕ} {left right : List Bool} (hleft : left.length ≤ bound) (hright : right.length ≤ bound) (h : ofList (2 * bound + 1) (padWord bound left) = ofList (2 * bound + 1) (padWord bound right)) :
    left = right

    Padding embeds bounded words into a fixed finite bit-string space.