Size-aware encodings

Interface between ordinary types and the ambient model: a SizedEncoding α renders a : α as a value encode a : Data, and esize a is its size (the length of its preorder serialization Data.toBits), an honest bit-length up to a constant factor. All polynomial-time statements (Cost.PolyTime) are relative to these encodings.

Conventions:

• bits are false ↦ nil and true ↦ cons nil nil;
• lists are cons-chains ending in nil, so a bit string of length n has size between 2n + 1 and 4n + 1;
• natural numbers are encoded in binary (LSB first, Nat.bits), so esize n ≤ 4 · Nat.size n + 1;
• pairs are cons: esize (a, b) = esize a + esize b + 1 — length-additive pairing, with no separators;
• programs are their tree encoding Prog.toData, a length-faithful serialization (this, not any numeric Gödel numbering, is how programs occur as data).

This deliberately does not reuse Mathlib's Encodable/Primcodable: those encode into ℕ via the quadratic pairing Nat.pair, whose iterated use distorts lengths exponentially.

class MIPRE.Cost.SizedEncoding (α : Type u_1) : Type u_1

A size-faithful encoding of α as data, with decode inverting encode.

• encode : α → Data

  Encoding of a value.

• decode : Data → Option α

  Decoding; must invert encode (on well-formed data).

• decode_encode (a : α) : decode (encode a) = some a

def MIPRE.Cost.esize {α : Type u_1} [SizedEncoding α] (a : α) : ℕ

The size of a value: the number of nodes of its encoding.

Equations

• MIPRE.Cost.esize a = (MIPRE.Cost.encode a).size

theorem MIPRE.Cost.esize_pos {α : Type u_1} [SizedEncoding α] (a : α) : 0 < esize a

theorem MIPRE.Cost.encode_injective {α : Type u_1} [SizedEncoding α] : Function.Injective encode

@[reducible, inline]

abbrev MIPRE.Cost.BitStr : Type

Binary strings, the {0,1}* of the paper.

Equations

• MIPRE.Cost.BitStr = List Bool

def MIPRE.Cost.Data.ofBool : Bool → Data

Bits: false ↦ nil, true ↦ cons nil nil.

Equations

• MIPRE.Cost.Data.ofBool false = MIPRE.Cost.Data.nil
• MIPRE.Cost.Data.ofBool true = MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil

def MIPRE.Cost.Data.toBool? : Data → Option Bool

Reading a bit back.

Equations

• MIPRE.Cost.Data.nil.toBool? = some false
• (MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).toBool? = some true
• (a.cons a_1).toBool? = none

@[simp]

theorem MIPRE.Cost.Data.toBool?_ofBool (b : Bool) : (ofBool b).toBool? = some b

theorem MIPRE.Cost.Data.size_ofBool (b : Bool) : (ofBool b).size ≤ 3

def MIPRE.Cost.Data.ofList {α : Type u_1} (f : α → Data) : List α → Data

Lists: cons-chains ending in nil.

Equations

• MIPRE.Cost.Data.ofList f [] = MIPRE.Cost.Data.nil
• MIPRE.Cost.Data.ofList f (a :: l) = (f a).cons (MIPRE.Cost.Data.ofList f l)

def MIPRE.Cost.Data.toList? {α : Type u_1} (g : Data → Option α) : Data → Option (List α)

Reading a list back, elementwise.

Equations

• MIPRE.Cost.Data.toList? g MIPRE.Cost.Data.nil = some []
• MIPRE.Cost.Data.toList? g (a.cons d) = do let x ← g a let l ← MIPRE.Cost.Data.toList? g d pure (x :: l)

theorem MIPRE.Cost.Data.toList?_ofList {α : Type u_1} {f : α → Data} {g : Data → Option α} (hfg : ∀ (a : α), g (f a) = some a) (l : List α) : toList? g (ofList f l) = some l

theorem MIPRE.Cost.Data.size_ofList_le {α : Type u_1} {f : α → Data} {B : ℕ} (hf : ∀ (a : α), (f a).size ≤ B) (l : List α) : (ofList f l).size ≤ (B + 1) * l.length + 1

theorem MIPRE.Cost.Data.length_le_size_ofList {α : Type u_1} (f : α → Data) (l : List α) : l.length ≤ (ofList f l).size

@[instance_reducible]

instance MIPRE.Cost.instSizedEncodingBool : SizedEncoding Bool

Equations

• MIPRE.Cost.instSizedEncodingBool = { encode := MIPRE.Cost.Data.ofBool, decode := MIPRE.Cost.Data.toBool?, decode_encode := MIPRE.Cost.Data.toBool?_ofBool }

@[instance_reducible]

instance MIPRE.Cost.instSizedEncodingBitStr : SizedEncoding BitStr

Bit strings encode as lists of bits.

Equations

• MIPRE.Cost.instSizedEncodingBitStr = { encode := MIPRE.Cost.Data.ofList MIPRE.Cost.Data.ofBool, decode := MIPRE.Cost.Data.toList? MIPRE.Cost.Data.toBool?, decode_encode := ⋯ }

theorem MIPRE.Cost.esize_bitStr_le (x : BitStr) : esize x ≤ 4 * List.length x + 1

theorem MIPRE.Cost.length_le_esize_bitStr (x : BitStr) : List.length x ≤ esize x

theorem MIPRE.Cost.Nat.foldr_bit_bits (n : ℕ) : List.foldr Nat.bit 0 n.bits = n

Folding Nat.bit over the binary digits of n recovers n.

@[instance_reducible]

instance MIPRE.Cost.instSizedEncodingNat : SizedEncoding ℕ

Natural numbers encode in binary (LSB first): the bit string n.bits. This is the encoding under which indices "n in binary" enter succinct descriptions (blueprint def:succinct).

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Cost.esize_nat_le (n : ℕ) : esize n ≤ 4 * n.size + 1

theorem MIPRE.Cost.size_le_esize_nat (n : ℕ) : n.size ≤ esize n

@[instance_reducible]

instance MIPRE.Cost.instSizedEncodingProd {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] : SizedEncoding (α × β)

Length-additive pairing: encode (a, b) = cons (encode a) (encode b).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.esize_prod {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (a : α) (b : β) : esize (a, b) = esize a + esize b + 1

theorem MIPRE.Cost.encode_prod {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (a : α) (b : β) : encode (a, b) = (encode a).cons (encode b)

Programs as data

def MIPRE.Cost.Prog.toData : Prog → Data

Programs as data: a unary tag (0–6) paired with the fields.

Equations

• (MIPRE.Cost.Prog.var i).toData = (MIPRE.Cost.Data.ofNat 0).cons (MIPRE.Cost.Data.ofNat i)
• MIPRE.Cost.Prog.nil.toData = (MIPRE.Cost.Data.ofNat 1).cons MIPRE.Cost.Data.nil
• (h.cons t).toData = (MIPRE.Cost.Data.ofNat 2).cons (h.toData.cons t.toData)
• (MIPRE.Cost.Prog.elim i n c).toData = (MIPRE.Cost.Data.ofNat 3).cons ((MIPRE.Cost.Data.ofNat i).cons (n.toData.cons c.toData))
• (e.let_ b).toData = (MIPRE.Cost.Data.ofNat 4).cons (e.toData.cons b.toData)
• b.loop.toData = (MIPRE.Cost.Data.ofNat 5).cons b.toData
• (MIPRE.Cost.Prog.const d).toData = (MIPRE.Cost.Data.ofNat 6).cons d

def MIPRE.Cost.Prog.ofData : Data → Option Prog

Reading a program back from its data (ofData_toData).

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Cost.Prog.ofData (MIPRE.Cost.Data.nil.cons i) = Option.map MIPRE.Cost.Prog.var i.toNat?
• MIPRE.Cost.Prog.ofData ((MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).cons MIPRE.Cost.Data.nil) = some MIPRE.Cost.Prog.nil
• MIPRE.Cost.Prog.ofData x✝ = none

theorem MIPRE.Cost.Prog.ofData_toData (p : Prog) : ofData p.toData = some p

@[instance_reducible]

instance MIPRE.Cost.Prog.instSizedEncoding : SizedEncoding Prog

Equations

• MIPRE.Cost.Prog.instSizedEncoding = { encode := MIPRE.Cost.Prog.toData, decode := MIPRE.Cost.Prog.ofData, decode_encode := MIPRE.Cost.Prog.ofData_toData }

theorem MIPRE.Cost.Prog.esize_eq_size_toData (p : Prog) : esize p = p.toData.size

theorem MIPRE.Cost.Prog.two_le_esize (p : Prog) : 2 ≤ esize p

Every program has size at least two. Prog.toData is a Data.cons whatever the constructor, so no program encodes to nil. Small, and load-bearing: it is what forces 2 ≤ λ in Verifier.IsBounded (Verifier.IsBounded.two_le), and so what puts the index of the halting reduction inside the range where IsBounded's time clauses say anything.