Executable canonical register and answer bounds

For R = 2^(lambda*n), the paper uses t = max 2 (lambda*n), m = 2^(size(c*t+1)-1), and log q = c*size(t-1)+1. Here size(t-1) is the integer ceiling of log₂ t. The universal even constant c is fixed; lambda and n are binary program inputs. The output is the binary pair (Q,R) with Q = 2^m * log q.

def MIPRE.Introspection.SourceCompiler.canonicalLog (lam n : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.canonicalLog lam n = max 2 (lam * n)

def MIPRE.Introspection.SourceCompiler.registerPower (c lam n : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.registerPower c lam n = 2 ^ ((c * MIPRE.Introspection.SourceCompiler.canonicalLog lam n + 1).size - 1)

def MIPRE.Introspection.SourceCompiler.fieldBits (c lam n : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.fieldBits c lam n = c * (MIPRE.Introspection.SourceCompiler.canonicalLog lam n - 1).size + 1

def MIPRE.Introspection.SourceCompiler.registerBits (c lam n : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.registerBits c lam n = 2 ^ MIPRE.Introspection.SourceCompiler.registerPower c lam n * MIPRE.Introspection.SourceCompiler.fieldBits c lam n

def MIPRE.Introspection.SourceCompiler.originalBound (lam n : ℕ) : ℕ

Equations

• MIPRE.Introspection.SourceCompiler.originalBound lam n = 2 ^ (lam * n)

theorem MIPRE.Introspection.SourceCompiler.originalBound_eq (lam n : ℕ) : originalBound lam n = (2 ^ n) ^ lam

noncomputable def MIPRE.Introspection.SourceCompiler.affineUnary (c : ℕ) : Cost.PolyTimeFun Cost.Unary Cost.Unary

Equations

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

@[simp]

theorem MIPRE.Introspection.SourceCompiler.affineUnary_apply (c : ℕ) (u : Cost.Unary) : (affineUnary c).toFun u = Cost.unary (c * List.length u + 1)

noncomputable def MIPRE.Introspection.SourceCompiler.clampLog : Cost.PolyTimeFun Cost.Unary Cost.Unary

Equations

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

theorem MIPRE.Introspection.SourceCompiler.clampLog_apply (u : Cost.Unary) : clampLog.toFun u = Cost.unary (max 2 (List.length u))

noncomputable def MIPRE.Introspection.SourceCompiler.unarySize : Cost.PolyTimeFun Cost.Unary Cost.Unary

Equations

• MIPRE.Introspection.SourceCompiler.unarySize = MIPRE.Cost.PolyTimeFun.length.comp (MIPRE.Cost.PolyTimeFun.natBits.comp MIPRE.Cost.PolyTimeFun.unaryToBin)

theorem MIPRE.Introspection.SourceCompiler.unarySize_apply (u : Cost.Unary) : unarySize.toFun u = Cost.unary (List.length u).size

noncomputable def MIPRE.Introspection.SourceCompiler.parameterSeed (c : ℕ) : Cost.PolyTimeFun Cost.Unary (Cost.Unary × Cost.Unary × Cost.Unary)

Prepare the binary-power exponent, the original logarithm, and the field bit length.

Equations

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

theorem MIPRE.Introspection.SourceCompiler.parameterSeed_apply (c : ℕ) (u : Cost.Unary) : (parameterSeed c).toFun u = (Cost.unary ((c * max 2 (List.length u) + 1).size - 1), u, Cost.unary (c * (max 2 (List.length u) - 1).size + 1))

def MIPRE.Introspection.SourceCompiler.powerUnaryProg : Cost.Prog

Equations

• MIPRE.Introspection.SourceCompiler.powerUnaryProg = MIPRE.Cost.Prog.expBitsProg.let_ MIPRE.Cost.Prog.toUnaryProg

theorem MIPRE.Introspection.SourceCompiler.powerUnaryProg_closed : Cost.Prog.WellScoped 1 powerUnaryProg

theorem MIPRE.Introspection.SourceCompiler.powerUnaryProg_runs (j : ℕ) : ∃ (t : ℕ), powerUnaryProg.Runs (Cost.Data.ofNat j) (Cost.Data.ofNat (2 ^ j)) t

noncomputable def MIPRE.Introspection.SourceCompiler.readUnary : Cost.PolyTimeFun Cost.Data Cost.Unary

Read a raw unary chain by its length; total on arbitrary data.

Equations

• MIPRE.Introspection.SourceCompiler.readUnary = MIPRE.Cost.PolyTimeFun.length.comp (MIPRE.Cost.PolyTimeFun.ofEncodeEq MIPRE.CL.Detyping.Program.rawList MIPRE.CL.Detyping.Program.encode_rawList)

theorem MIPRE.Introspection.SourceCompiler.readUnary_ofNat (n : ℕ) : readUnary.toFun (Cost.Data.ofNat n) = Cost.unary n

noncomputable def MIPRE.Introspection.SourceCompiler.parameterPost : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.registerSizeProg : Cost.PolyTimeFun Cost.Data ℕ

Shift the binary field bit length by the computed unary register power.

Equations

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

theorem MIPRE.Introspection.SourceCompiler.bitsVal_zeros (j : ℕ) (bs : Cost.BitStr) : Cost.bitsVal (List.replicate j false ++ bs) = 2 ^ j * Cost.bitsVal bs

theorem MIPRE.Introspection.SourceCompiler.registerSizeProg_apply (m k : ℕ) : registerSizeProg.toFun ((Cost.Data.ofNat m).cons (Cost.Data.ofNat k)) = 2 ^ m * k

noncomputable def MIPRE.Introspection.SourceCompiler.boundsPost : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.SourceCompiler.boundsProg (c : ℕ) : Cost.Prog

A fixed program computes the paper's binary (Q,R) from binary (lambda,n).

Equations

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

theorem MIPRE.Introspection.SourceCompiler.boundsProg_closed (c : ℕ) : Cost.Prog.WellScoped 1 (boundsProg c)

theorem MIPRE.Introspection.SourceCompiler.boundsProg_runs (c lam n : ℕ) : ∃ (time : ℕ), (boundsProg c).Runs (Cost.encode (lam, n)) (Cost.encode (registerBits c lam n, originalBound lam n)) time