Size bounds for the canonical framed codecs

TheoremDecoded block count is at most the input length#✓fully proved

Each decoded block consumes at least its delimiter bit.

theorem blocks_length_le {fuel : Nat} {x : List Bool}
    {blocks : List (List Bool)}
    (h : undelimitBlocksAux fuel x = some blocks) :
    blocks.length ≤ x.length

Uses 4 · Used by 1

Statement usesBounded parsing of self-delimiting blocks

Proof usesParsing a self-delimiting block · Self-delimiting form of a bitstring · Parsing one self-delimiting block

Used byDecoded list has at most one element per input bit

TheoremDecoded list has at most one element per input bit#✓fully proved

A successfully decoded list has at most one element per input bit. No canonicality assumption on the element payloads is needed.

theorem decoded_list_length_le {α : Type} [BitstringEncoding α]
    {x : List Bool} {as : List α}
    (h : bitDecode x = some as) : as.length ≤ x.length

Uses 9 · Used by 2

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesDecoded block count is at most the input length

Used byLength bound for a list in the first field of a decoded pair · Length bound for a list in the second field of a decoded pair

TheoremDecoded pair exposes its raw component payloads#✓fully proved

Successful pair decoding exposes the exact raw component payloads. This includes payloads which are not canonical encodings.

theorem decoded_pair_parts {α β : Type}
    [BitstringEncoding α] [BitstringEncoding β]
    {x : List Bool} {a : α} {b : β}
    (h : bitDecode x = some (a, b)) :
    ∃ p r, x = delimit p ++ r ∧
      bitDecode p = some a ∧ bitDecode r = some b

Uses 7 · Used by 8

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block

Proof usesParsing a self-delimiting block

Used byFour-output decoder output is at most twice the input length · Four-output decoder emits four canonical outputs on success · Canonical payloads of a decoded pair are bounded by the raw input · Number-pair projector yields both canonical payloads on success · Raw field projection agrees with the pair decoder · Length bound for a list in the first field of a decoded pair · Length bound for the middle list of a decoded triple · Length bound for a list in the second field of a decoded pair

TheoremLength bound for a list in the first field of a decoded pair#✓fully proved

A list in the first field of a decoded pair is raw-input bounded.

theorem decoded_fst_list_length_le {α β : Type}
    [BitstringEncoding α] [BitstringEncoding β]
    {x : List Bool} {as : List α} {b : β}
    (h : bitDecode x = some (as, b)) : as.length ≤ x.length

Uses 10 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesDecoded list has at most one element per input bit · Decoded pair exposes its raw component payloads

Used byLength bound for the middle list of a decoded triple

TheoremLength bound for a list in the second field of a decoded pair#✓fully proved

A list in the second field of a decoded pair is raw-input bounded.

theorem decoded_snd_list_length_le {α β : Type}
    [BitstringEncoding α] [BitstringEncoding β]
    {x : List Bool} {a : α} {bs : List β}
    (h : bitDecode x = some (a, bs)) : bs.length ≤ x.length

Uses 10

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesDecoded list has at most one element per input bit · Decoded pair exposes its raw component payloads

TheoremLength bound for the middle list of a decoded triple#✓fully proved

The middle list of a right-associated triple is raw-input bounded. Used for TSP matrix rows and SET COVER set occurrences.

theorem decoded_middle_list_length_le {α β γ : Type}
    [BitstringEncoding α] [BitstringEncoding β] [BitstringEncoding γ]
    {x : List Bool} {a : α} {bs : List β} {c : γ}
    (h : bitDecode x = some (a, bs, c)) : bs.length ≤ x.length

Uses 10

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesLength bound for a list in the first field of a decoded pair · Decoded pair exposes its raw component payloads

TheoremFramed length bound for lists of \(m\)-bit naturals#✓fully proved

A list of binary naturals with at most m bits per entry has the stated framed length bound.

theorem list_nat_encode_length_le (as : List Nat) (m : Nat)
    (h : ∀ a ∈ as, a.size ≤ m) :
    (bitEncode as).length ≤ as.length * (2 * m + 1)

Uses 8 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Used byQuadratic encoding bound for vertex lists below \(n\)

TheoremQuadratic encoding bound for vertex lists below \(n\)#✓fully proved

Lists of vertices below n have a quadratic certificate bound when their length is at most n; no unary Nat encoding is used.

theorem bounded_nat_list_encode_length_le (as : List Nat) (n : Nat)
    (hlen : as.length ≤ n) (h : ∀ a ∈ as, a < n) :
    (bitEncode as).length ≤ n * (2 * n + 1)

Uses 9

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesFramed length bound for lists of \(m\)-bit naturals

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.