Unary arithmetic by loops

The routines the pipeline's parameter computations need, whose running time is polynomial in the value of their input rather than its size: writing a binary number in unary (toUnaryProg) and raising a unary number to a binary power (powProg). Both are whileProg loops (MIPRE/Foundations/Cost/While) of polynomial-time steps.

noncomputable def MIPRE.Pipeline.readUnary : Cost.PolyTimeFun Cost.Data Cost.Unary

A unary numeral, read off its encoding.

Equations

• MIPRE.Pipeline.readUnary = (MIPRE.Cost.PolyTimeFun.const ()).map.comp (MIPRE.Cost.PolyTimeFun.ofEncodeEq MIPRE.CL.Detyping.Program.rawList MIPRE.CL.Detyping.Program.encode_rawList)

theorem MIPRE.Pipeline.rawList_encode {α : Type u_1} [Cost.SizedEncoding α] (l : List α) : CL.Detyping.Program.rawList (Cost.encode l) = List.map Cost.encode l

@[simp]

theorem MIPRE.Pipeline.readUnary_encode (u : Cost.Unary) : readUnary.toFun (Cost.encode u) = u

Binary to unary

noncomputable def MIPRE.Pipeline.toUnaryStep : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

One step of the conversion, on (x, acc): stop with acc at x = 0, else move one unit.

Equations

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

theorem MIPRE.Pipeline.toUnaryStep_zero (acc : Cost.Unary) : toUnaryStep.toFun (Cost.encode (0, acc)) = (false, Cost.encode acc)

theorem MIPRE.Pipeline.toUnaryStep_succ (x : ℕ) (acc : Cost.Unary) : toUnaryStep.toFun (Cost.encode (x + 1, acc)) = (true, Cost.encode (x, () :: acc))

noncomputable def MIPRE.Pipeline.toUnaryProg : Cost.Prog

Binary to unary: encode x ↦ encode (unary x).

Equations

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

theorem MIPRE.Pipeline.toUnaryProg_closed : Cost.Prog.WellScoped 1 toUnaryProg

theorem MIPRE.Pipeline.toUnaryProg_runs (x : ℕ) : ∃ (t : ℕ), toUnaryProg.Runs (Cost.encode x) (Cost.encode (Cost.unary x)) t

Powers

noncomputable def MIPRE.Pipeline.powStep : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

One step of the power, on (e, acc, b): stop with acc at e = 0, else multiply by b.

Equations

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

theorem MIPRE.Pipeline.powStep_zero (acc b : Cost.Unary) : powStep.toFun (Cost.encode (0, acc, b)) = (false, Cost.encode acc)

theorem MIPRE.Pipeline.powStep_succ (e : ℕ) (acc b : Cost.Unary) : powStep.toFun (Cost.encode (e + 1, acc, b)) = (true, Cost.encode (e, Cost.unary (List.length acc * List.length b), b))

noncomputable def MIPRE.Pipeline.powProg : Cost.Prog

The power: encode (b, e) ↦ encode (unary (|b|^e)).

Equations

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

theorem MIPRE.Pipeline.powProg_closed : Cost.Prog.WellScoped 1 powProg

theorem MIPRE.Pipeline.powProg_runs (b : Cost.Unary) (e : ℕ) : ∃ (t : ℕ), powProg.Runs (Cost.encode (b, e)) (Cost.encode (Cost.unary (List.length b ^ e))) t

Stages

noncomputable def MIPRE.Pipeline.stageProg (pre : Cost.PolyTimeFun Cost.Data Cost.Data) (p : Cost.Prog) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) : Cost.Prog

A stage of a routine: split the input into an argument and a context, run p on the argument, and combine the context with its answer.

Equations

• MIPRE.Pipeline.stageProg pre p post = MIPRE.Cost.seqProg pre.code (p.callWithContext post)

theorem MIPRE.Pipeline.stageProg_closed (pre : Cost.PolyTimeFun Cost.Data Cost.Data) {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) : Cost.Prog.WellScoped 1 (stageProg pre p post)

theorem MIPRE.Pipeline.stageProg_runs (pre : Cost.PolyTimeFun Cost.Data Cost.Data) {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (X a ctx r : Cost.Data) (t : ℕ) (hpre : pre.toFun X = a.cons ctx) (hr : p.Runs a r t) : ∃ (t' : ℕ), (stageProg pre p post).Runs X (post.toFun (ctx, r)) t'