Executable arithmetic for the introspection clock

One fixed program, for each constant exponent, reads binary λ and n and writes the unary budget 2^((λ*n+1)^k). The large output is constructed by proved unary arithmetic programs; it is never embedded in the program text.

def MIPRE.Introspection.ClockArithmetic.unaryCost (n : ℕ) : ℕ

Equations

• MIPRE.Introspection.ClockArithmetic.unaryCost n = (n.size + 2) * ((n + 1) * (4 * n + 14) + 7 * MIPRE.Cost.esize n + 8 * n + 90)

def MIPRE.Introspection.ClockArithmetic.bothUnary : Cost.Prog

Equations

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

theorem MIPRE.Introspection.ClockArithmetic.bothUnary_closed : Cost.Prog.WellScoped 1 bothUnary

theorem MIPRE.Introspection.ClockArithmetic.bothUnary_runs (a b : ℕ) : ∃ time ≤ unaryCost a + unaryCost b + Cost.esize a + Cost.esize b + 2 * a + 2 * b + 20, bothUnary.Runs (Cost.encode (a, b)) ((Cost.Data.ofNat a).cons (Cost.Data.ofNat b)) time

def MIPRE.Introspection.ClockArithmetic.powerCoeffs (k : ℕ) : List ℕ

Equations

• MIPRE.Introspection.ClockArithmetic.powerCoeffs k = List.replicate k 0 ++ [1]

theorem MIPRE.Introspection.ClockArithmetic.powerCoeffs_eval (k m : ℕ) : Cost.Data.polyEval (powerCoeffs k) m = m ^ k

noncomputable def MIPRE.Introspection.ClockArithmetic.powerBound (k : ℕ) : Polynomial ℕ

Equations

• MIPRE.Introspection.ClockArithmetic.powerBound k = ⋯.choose

theorem MIPRE.Introspection.ClockArithmetic.power_runs (k m : ℕ) : ∃ time ≤ Polynomial.eval m (powerBound k), (Cost.Prog.polyProg (powerCoeffs k)).Runs (Cost.Data.ofNat m) (Cost.Data.ofNat (m ^ k)) time

def MIPRE.Introspection.ClockArithmetic.mulCost (a b : ℕ) : ℕ

Equations

• MIPRE.Introspection.ClockArithmetic.mulCost a b = (b + 1) * ((a + 1) * (4 * a + 2 * (a * b) + 15) + 4 * a + 4 * (a * b) + 2 * b + 41) + 2 * b + 10

def MIPRE.Introspection.ClockArithmetic.uniformProg (k : ℕ) : Cost.Prog

Equations

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

theorem MIPRE.Introspection.ClockArithmetic.uniformProg_closed (k : ℕ) : Cost.Prog.WellScoped 1 (uniformProg k)

noncomputable def MIPRE.Introspection.ClockArithmetic.uniformCost (k lam n : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.ClockArithmetic.uniformProg_runs (k lam n : ℕ) : ∃ time ≤ uniformCost k lam n, (uniformProg k).Runs (Cost.encode (lam, n)) (Cost.Data.ofNat (ansBound k lam n)) time