Reading and writing descriptions, in the ambient model

The two programs that move between a datum and its postorder serialization (Data.toBitsPost, Halting/Descriptions.lean):

• Prog.parseProg: the stack machine Data.stackRun on a bit string, returning the top of the final stack (Data.parse). The compressor's decider reads the description it was handed with it (Halting/Compressor.lean).
• Prog.serProg: the postorder serialization of a datum, by a loop over a list of pending items — a datum still to be written, or a marker for the closing 1 of a pair — accumulating the bits in reverse and reversing at the end. The compressor writes its output with it.

Both run in time quadratic in the size of their input: each step copies the remainder of the work list and the accumulator.

def MIPRE.Cost.Data.itemD : Option Data → Data

A pending item of the serializer: a datum to write (some d, as cons nil d) or the closing 1 of a pair (none, as nil).

Equations

• MIPRE.Cost.Data.itemD (some d) = MIPRE.Cost.Data.nil.cons d
• MIPRE.Cost.Data.itemD none = MIPRE.Cost.Data.nil

def MIPRE.Cost.Data.serItems : List (Option Data) → BitStr

The bits still to be written for a list of pending items.

Equations

• MIPRE.Cost.Data.serItems [] = []
• MIPRE.Cost.Data.serItems (some d :: r) = d.toBitsPost ++ MIPRE.Cost.Data.serItems r
• MIPRE.Cost.Data.serItems (none :: r) = true :: MIPRE.Cost.Data.serItems r

def MIPRE.Cost.Data.serMeasure : List (Option Data) → ℕ

The measure of a list of pending items, decreasing along the serializer's loop.

Equations

• MIPRE.Cost.Data.serMeasure [] = 0
• MIPRE.Cost.Data.serMeasure (some d :: r) = 3 * d.size + 1 + MIPRE.Cost.Data.serMeasure r
• MIPRE.Cost.Data.serMeasure (none :: r) = 1 + MIPRE.Cost.Data.serMeasure r

def MIPRE.Cost.Data.serMeasureD : Data → ℕ

The same measure, on the data of the pending list (for the loop invariant).

Equations

• MIPRE.Cost.Data.nil.serMeasureD = 0
• (MIPRE.Cost.Data.nil.cons r).serMeasureD = 1 + r.serMeasureD
• ((a.cons d).cons r).serMeasureD = 3 * d.size + 1 + r.serMeasureD

def MIPRE.Cost.Prog.tacticCost_omega₂ : Lean.ParserDescr

Close a cost bound after the run has been built, unfolding list encodings.

Equations

• MIPRE.Cost.Prog.tacticCost_omega₂ = Lean.ParserDescr.node `MIPRE.Cost.Prog.tacticCost_omega₂ 1024 (Lean.ParserDescr.nonReservedSymbol "cost_omega₂" false)

The parser

def MIPRE.Cost.Prog.parseBody : Prog

Body of parseProg, on the state cons bits stack: at the end, stop with the top of the stack (nil if empty); on a 0, push nil; on a 1, pop two entries and push their pair, leaving a stack with fewer than two entries alone.

Equations

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

def MIPRE.Cost.Prog.parseProg : Prog

parseProg on an encoded bit string x computes parse x.

Equations

• MIPRE.Cost.Prog.parseProg = ((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).let_ MIPRE.Cost.Prog.parseBody.loop

theorem MIPRE.Cost.Prog.parseBody_wellScoped : WellScoped 1 parseBody

theorem MIPRE.Cost.Prog.parseProg_wellScoped : WellScoped 1 parseProg

theorem MIPRE.Cost.Prog.parseBody_stop (s : List Data) : ∃ t ≤ (Data.list s).size + 20, Eval [(encode []).cons (Data.list s)] parseBody (Data.nil.cons (s.headD Data.nil)) t

theorem MIPRE.Cost.Prog.parseBody_false (x : BitStr) (s : List Data) : ∃ t ≤ (encode x).size + (Data.list s).size + 20, Eval [(encode (false :: x)).cons (Data.list s)] parseBody ((Data.nil.cons Data.nil).cons ((encode x).cons (Data.list (Data.stackStep s false)))) t

theorem MIPRE.Cost.Prog.parseBody_true (x : BitStr) (s : List Data) : ∃ t ≤ (encode x).size + (Data.list s).size + 20, Eval [(encode (true :: x)).cons (Data.list s)] parseBody ((Data.nil.cons Data.nil).cons ((encode x).cons (Data.list (Data.stackStep s true)))) t

theorem MIPRE.Cost.Prog.size_list_stackStep (s : List Data) (b : Bool) : (Data.list (Data.stackStep s b)).size ≤ (Data.list s).size + 2

The stack size grows by at most two per step.

theorem MIPRE.Cost.Prog.parseLoop_runs (x : BitStr) (s : List Data) (env : Env) (S : ℕ) (hS : (encode x).size + (Data.list s).size + 2 * List.length x ≤ S) : ∃ t ≤ (List.length x + 1) * (S + 21), Eval ((encode x).cons (Data.list s) :: env) parseBody.loop ((Data.stackRun x s).headD Data.nil) t

The parsing loop computes the top of the final stack, in time (|x| + 1) · (S + 21) for S dominating the sizes along the run.

theorem MIPRE.Cost.Prog.parseProg_runs (x : BitStr) : ∃ t ≤ (List.length x + 2) * ((encode x).size + 2 * List.length x + 25), parseProg.Runs (encode x) (Data.parse x) t

parseProg reads a serialization back.

The serializer

def MIPRE.Cost.Prog.serBody : Prog

Body of serProg, on the state cons pending acc: at the end, stop with acc; a marker writes a 1; the datum nil writes a 0; a pair cons a b schedules a, b and a marker.

Equations

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

def MIPRE.Cost.Prog.serProg : Prog

serProg on d computes encode d.toBitsPost.

Equations

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

theorem MIPRE.Cost.Prog.serBody_wellScoped : WellScoped 1 serBody

theorem MIPRE.Cost.Prog.serProg_wellScoped : WellScoped 1 serProg

theorem MIPRE.Cost.Prog.serBody_stop (acc : BitStr) : ∃ t ≤ (encode acc).size + 20, Eval [(Data.list []).cons (encode acc)] serBody (Data.nil.cons (encode acc)) t

theorem MIPRE.Cost.Prog.serBody_marker (rest : List Data) (acc : BitStr) : ∃ t ≤ (Data.list rest).size + (encode acc).size + 20, Eval [(Data.list (Data.nil :: rest)).cons (encode acc)] serBody ((Data.nil.cons Data.nil).cons ((Data.list rest).cons (encode (true :: acc)))) t

theorem MIPRE.Cost.Prog.serBody_datanil (rest : List Data) (acc : BitStr) : ∃ t ≤ (Data.list rest).size + (encode acc).size + 20, Eval [(Data.list (Data.nil.cons Data.nil :: rest)).cons (encode acc)] serBody ((Data.nil.cons Data.nil).cons ((Data.list rest).cons (encode (false :: acc)))) t

theorem MIPRE.Cost.Prog.serBody_datacons (a b : Data) (rest : List Data) (acc : BitStr) : ∃ t ≤ a.size + b.size + (Data.list rest).size + (encode acc).size + 30, Eval [(Data.list (Data.nil.cons (a.cons b) :: rest)).cons (encode acc)] serBody ((Data.nil.cons Data.nil).cons ((Data.list (Data.nil.cons a :: Data.nil.cons b :: Data.nil :: rest)).cons (encode acc))) t

theorem MIPRE.Cost.Prog.serLoop_runs (d : Data) (env : Env) : ∃ t ≤ (3 * d.size + 2) * (16 * d.size + 42), Eval ((Data.list [Data.itemD (some d)]).cons (encode []) :: env) serBody.loop (encode (List.reverse d.toBitsPost)) t

The serializer's loop, by the invariant "acc.reverse ++ serItems items is the target", with the measure serMeasure and the size bound S₀.

theorem MIPRE.Cost.Prog.serProg_runs (d : Data) : ∃ t ≤ (3 * d.size + 2) * (16 * d.size + 42) + (d.size + 2) * (5 * d.size + 30), serProg.Runs d (encode d.toBitsPost) t

serProg writes the postorder serialization.