Normalizing the total binary natural-number decoder

DefinitionNormalization of a raw binary natural-number payload#✓fully proved

Canonicalize a raw payload without enumerating its decoded value.

def normalizeNat (bits : List Bool) : List Bool :=
  if bits.getLast? = some false then bits ++ [true] else bits

Used by 17

Used byList canonicalizer normalizes a sequence of framed payloads · List canonicalizer normalizes one element · List canonicalizer fails on malformed input · List canonicalizer runs in linear time on decodable input · Payload normalization is polynomial-time · Read phase of the payload normalizer consumes each bit once · Linear step bound for the payload normalizer machine · Re-encoded decoded list of naturals is linear in raw input · Re-encoding decoded payloads normalizes each one · Normalizing framed number payloads at most triples the length · Number normalizer restores its work stacks and prepends its answer · Payload normalization adds at most one bit · Payload normalization fixes canonical encodings · Payload normalization agrees with decode-then-encode · Canonical payloads of a decoded pair are bounded by the raw input · Number-pair projector normalizes both fields of a raw pair frame · Number-pair projector yields both canonical payloads on success

TheoremPayload normalization agrees with decode-then-encode#✓fully proved

Normalization agrees with the existing total decoder on every payload, not just canonical encodings.

theorem normalizeNat_eq_encode_decode (bits : List Bool) :
    normalizeNat bits = encodeNat (decodeNat bits)

Uses 1 · Used by 4

Statement usesNormalization of a raw binary natural-number payload

Used byRe-encoding decoded payloads normalizes each one · Payload normalization fixes canonical encodings · Canonical payloads of a decoded pair are bounded by the raw input · Number-pair projector yields both canonical payloads on success

TheoremPayload normalization adds at most one bit#✓fully proved

Normalization adds at most one bit.

theorem length_normalizeNat_le (bits : List Bool) :
    (normalizeNat bits).length ≤ bits.length + 1

Uses 1 · Used by 5

Statement usesNormalization of a raw binary natural-number payload

Used byList canonicalizer normalizes one element · Linear step bound for the payload normalizer machine · Normalizing framed number payloads at most triples the length · Number normalizer restores its work stacks and prepends its answer · Canonical payloads of a decoded pair are bounded by the raw input

TheoremPayload normalization fixes canonical encodings#✓fully proved

Canonical encodings are unchanged.

@[simp] theorem normalizeNat_encodeNat (n : ℕ) :
    normalizeNat (encodeNat n) = encodeNat n

Uses 2

Statement usesNormalization of a raw binary natural-number payload

Proof usesPayload normalization agrees with decode-then-encode

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.