Canonicalization of the concrete binary List Nat codec

TheoremSuccessful block parsing reconstructs the input#✓fully proved

Successful block parsing reconstructs the entire input.

theorem blocks_decode_sound {fuel : Nat} {x : List Bool}
    {bs : List (List Bool)} (h : undelimitBlocksAux fuel x = some bs) :
    x = (bs.map delimit).flatten

Uses 4 · Used by 5

Statement usesSelf-delimiting form of a bitstring · Bounded parsing of self-delimiting blocks

Proof usesParsing a self-delimiting block · Parsing one self-delimiting block

Used byList canonicalizer runs in linear time on decodable input · Projected pair lists total at most four times the input length · Pair-list projector yields canonical weight and value lists · Re-encoded decoded list of naturals is linear in raw input · Frame counter counts every successfully decoded list of naturals

TheoremDecoding natural-number payloads never fails#✓fully proved

Nat payload decoding never fails, including on noncanonical bits.

theorem mapM_decode_nat (bs : List (List Bool)) :
    bs.mapM (bitDecode (α := Nat)) = some (bs.map decodeNat)

Uses 2 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding

Used byDecoding a list of naturals is block parsing then number decoding

TheoremDecoding a list of naturals is block parsing then number decoding#✓fully proved

List Nat decoding is precisely framed-payload parsing followed by the existing total Nat decoder.

theorem decode_list_nat (x : List Bool) :
    bitDecode (α := List Nat) x =
      (undelimitBlocks x).map (List.map decodeNat)

Uses 9 · Used by 5

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 usesDecoding natural-number payloads never fails

Used byList canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Re-encoded decoded list of naturals is linear in raw input · Frame counter fails on malformed list framing · Frame counter counts every successfully decoded list of naturals

TheoremRe-encoding decoded payloads normalizes each one#✓fully proved

Canonical re-encoding normalizes each payload without changing list order or multiplicity.

theorem encode_decoded_nat_blocks (bs : List (List Bool)) :
    bitEncode (bs.map decodeNat) =
      (bs.map (fun p => delimit (normalizeNat p))).flatten

Uses 10 · Used by 2

Statement usesNormalization of a raw binary natural-number payload · Bitstring 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 usesPayload normalization agrees with decode-then-encode

Used byList canonicalizer runs in linear time on decodable input · Re-encoded decoded list of naturals is linear in raw input

TheoremNormalizing framed number payloads at most triples the length#✓fully proved

Normalizing every framed Nat payload increases length by at most threefold, even for noncanonical input.

theorem normalized_nat_blocks_length_le (bs : List (List Bool)) :
    ((bs.map (fun p => delimit (normalizeNat p))).flatten).length ≤
      3 * ((bs.map delimit).flatten).length

Uses 3 · Used by 2

Statement usesNormalization of a raw binary natural-number payload · Self-delimiting form of a bitstring

Proof usesPayload normalization adds at most one bit

Used byList canonicalizer runs in linear time on decodable input · Re-encoded decoded list of naturals is linear in raw input

TheoremRe-encoded decoded list of naturals is linear in raw input#✓fully proved

Re-encoding a successfully decoded List Nat is linear in the raw input, not in the decoded numeric values.

theorem decoded_list_nat_encode_length_le {x : List Bool} {as : List Nat}
    (h : bitDecode x = some as) : (bitEncode as).length ≤ 3 * x.length

Uses 13 · 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 usesNormalization of a raw binary natural-number payload · Successful block parsing reconstructs the input · Decoding a list of naturals is block parsing then number decoding · Re-encoding decoded payloads normalizes each one · Normalizing framed number payloads at most triples the length

Used byRaw-input PARTITION membership machine runs in quadratic time

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.