Size bounds along machine runs

Along the run of the evaluation machine that simulates a derivation Eval env p r t, every configuration stays bounded (CfgBound): values have size at most V (where t ≤ V and the initial values are at most V, since every value produced is the result of a sub-derivation of cost at most t), environments have length at most L + 2 t, programs are subterms of the initial ones, and the stack gains at most t frames (eval_steps_bound). Consequently the data encoding of every configuration along the run has size polynomial in the sizes of the program, the input and the cost (size_toData_le). This is what bounds the cost of the self-interpreter.

Bounds on configurations

def MIPRE.Cost.Machine.FrameBound (V L P : ℕ) : Frame → Prop

Bounds on a frame: values of size at most V, an environment of length at most L, a program of size at most P.

Equations

• MIPRE.Cost.Machine.FrameBound V L P (MIPRE.Cost.Machine.Frame.cons1 t env) = (MIPRE.Cost.esize t ≤ P ∧ List.length env ≤ L ∧ ∀ v ∈ env, v.size ≤ V)
• MIPRE.Cost.Machine.FrameBound V L P (MIPRE.Cost.Machine.Frame.cons2 a) = (a.size ≤ V)
• MIPRE.Cost.Machine.FrameBound V L P (MIPRE.Cost.Machine.Frame.let1 b env) = (MIPRE.Cost.esize b ≤ P ∧ List.length env ≤ L ∧ ∀ v ∈ env, v.size ≤ V)
• MIPRE.Cost.Machine.FrameBound V L P (MIPRE.Cost.Machine.Frame.loop1 b env) = (MIPRE.Cost.esize b ≤ P ∧ List.length env ≤ L ∧ ∀ v ∈ env, v.size ≤ V)

structure MIPRE.Cost.Machine.CfgBound (V L P K : ℕ) (c : Cfg) : Prop

Bounds on a configuration: values of size at most V, environments of length at most L, programs of size at most P, a stack of length at most K.

• ctrl_val (v : Data) : c.ctrl = Ctrl.ret v → v.size ≤ V
• ctrl_prog (p : Prog) : c.ctrl = Ctrl.ev p → esize p ≤ P
• env_len : List.length c.env ≤ L
• env_val (v : Data) : v ∈ c.env → v.size ≤ V
• kont_len : c.kont.length ≤ K
• frames (f : Frame) : f ∈ c.kont → FrameBound V L P f

theorem MIPRE.Cost.Machine.FrameBound.mono {V L P V' L' P' : ℕ} (hV : V ≤ V') (hL : L ≤ L') (hP : P ≤ P') {f : Frame} (h : FrameBound V L P f) : FrameBound V' L' P' f

theorem MIPRE.Cost.Machine.CfgBound.mono {V L P K V' L' P' K' : ℕ} (hV : V ≤ V') (hL : L ≤ L') (hP : P ≤ P') (hK : K ≤ K') {c : Cfg} (h : CfgBound V L P K c) : CfgBound V' L' P' K' c

Program subterms

theorem MIPRE.Cost.Machine.esize_cons_left (h t : Prog) : esize h ≤ esize (h.cons t)

theorem MIPRE.Cost.Machine.esize_cons_right (h t : Prog) : esize t ≤ esize (h.cons t)

theorem MIPRE.Cost.Machine.esize_elim_left (i : ℕ) (n c : Prog) : esize n ≤ esize (Prog.elim i n c)

theorem MIPRE.Cost.Machine.esize_elim_right (i : ℕ) (n c : Prog) : esize c ≤ esize (Prog.elim i n c)

theorem MIPRE.Cost.Machine.esize_let_left (e b : Prog) : esize e ≤ esize (e.let_ b)

theorem MIPRE.Cost.Machine.esize_let_right (e b : Prog) : esize b ≤ esize (e.let_ b)

theorem MIPRE.Cost.Machine.esize_loop (b : Prog) : esize b ≤ esize b.loop

theorem MIPRE.Cost.Machine.size_const_le (d : Data) : d.size ≤ esize (Prog.const d)

Chaining bounds along runs

theorem MIPRE.Cost.Machine.bound_chain {B : Cfg → Prop} {c₁ c₂ : Cfg} {m₁ m₂ : ℕ} (h₁ : step^[m₁] c₁ = c₂) (hb₁ : ∀ n ≤ m₁, B (step^[n] c₁)) (hb₂ : ∀ n ≤ m₂, B (step^[n] c₂)) (n : ℕ) : n ≤ m₁ + m₂ → B (step^[n] c₁)

theorem MIPRE.Cost.Machine.bound_one {B : Cfg → Prop} {c : Cfg} (h₀ : B c) (h₁ : B (step c)) (n : ℕ) : n ≤ 1 → B (step^[n] c)

theorem MIPRE.Cost.Machine.eval_steps_bound {env : Env} {p : Prog} {r : Data} {t : ℕ} (h : Eval env p r t) (k : List Frame) (V L P K : ℕ) : CfgBound V L P K { ctrl := Ctrl.ev p, env := env, kont := k } → t ≤ V → ∃ (N : ℕ) (env' : Env), Steps { ctrl := Ctrl.ev p, env := env, kont := k } N { ctrl := Ctrl.ret r, env := env', kont := k } t ∧ ∀ n ≤ N, CfgBound V (L + 2 * t) P (K + t) (step^[n] { ctrl := Ctrl.ev p, env := env, kont := k })

Every configuration along the machine run of a derivation is bounded.

Size of the encoded configurations

theorem MIPRE.Cost.Machine.sumSize_le_of_forall {V : ℕ} (l : List Data) : (∀ v ∈ l, v.size ≤ V) → Data.sumSize l ≤ l.length * V

theorem MIPRE.Cost.Machine.size_list_le_of_forall {V L : ℕ} (l : List Data) (hl : l.length ≤ L) (h : ∀ v ∈ l, v.size ≤ V) : (Data.list l).size ≤ L * V + L + 1

theorem MIPRE.Cost.Machine.frame_size_le {V L P : ℕ} {f : Frame} (h : FrameBound V L P f) : f.toData.size ≤ V + P + L * V + L + 10

def MIPRE.Cost.Machine.cfgSizeBound (V L P K : ℕ) : ℕ

Size of the encoding of a configuration satisfying CfgBound V L P K.

Equations

• MIPRE.Cost.Machine.cfgSizeBound V L P K = V + P + L * V + L + K * (V + P + L * V + L + 10) + K + 8

theorem MIPRE.Cost.Machine.size_toData_le {V L P K : ℕ} {c : Cfg} (h : CfgBound V L P K c) : c.toData.size ≤ cfgSizeBound V L P K

Runs from the empty stack are bounded forever

theorem MIPRE.Cost.Machine.step_final (r : Data) (e : Env) (n : ℕ) : step^[n] { ctrl := Ctrl.ret r, env := e, kont := [] } = { ctrl := Ctrl.ret r, env := e, kont := [] }

theorem MIPRE.Cost.Machine.eval_steps_bound_forever {env : Env} {p : Prog} {r : Data} {t : ℕ} (h : Eval env p r t) (V L P K : ℕ) (hb : CfgBound V L P K { ctrl := Ctrl.ev p, env := env, kont := [] }) (ht : t ≤ V) : ∃ (N : ℕ) (env' : Env), Steps { ctrl := Ctrl.ev p, env := env, kont := [] } N { ctrl := Ctrl.ret r, env := env', kont := [] } t ∧ ∀ (n : ℕ), CfgBound V (L + 2 * t) P (K + t) (step^[n] { ctrl := Ctrl.ev p, env := env, kont := [] })

Along the run of a derivation from the empty stack, every configuration — also after the final one, which is fixed — is bounded.

The number of steps of a run

theorem MIPRE.Cost.Machine.eval_steps_count {env : Env} {p : Prog} {r : Data} {t : ℕ} (h : Eval env p r t) (k : List Frame) : ∃ (N : ℕ) (env' : Env), Steps { ctrl := Ctrl.ev p, env := env, kont := k } N { ctrl := Ctrl.ret r, env := env', kont := k } t ∧ N ≤ 3 * t

The machine run of a derivation of cost t has at most 3 t steps (the free steps — entering a loop, and returning to a cons/let frame — are each matched with a paid one).

Cost sums

theorem MIPRE.Cost.Machine.costSum_succ (c : Cfg) (n : ℕ) : costSum c (n + 1) = costSum c n + stepCost (step^[n] c)

theorem MIPRE.Cost.Machine.costSum_le_of_le (c : Cfg) {m n : ℕ} (h : m ≤ n) : costSum c m ≤ costSum c n

theorem MIPRE.Cost.Machine.stepCost_final (r : Data) (e : Env) : stepCost { ctrl := Ctrl.ret r, env := e, kont := [] } = 0

theorem MIPRE.Cost.Machine.costSum_final (r : Data) (e : Env) (n : ℕ) : costSum { ctrl := Ctrl.ret r, env := e, kont := [] } n = 0