Deciding a cost budget

Machine.runForD runs a program for a step budget, and that is all the tabulation of a game needs: a program obeying a time bound halts, so one long-enough run settles what it returns. Obligation O3 needs the other question — whether a program halts within a given cost — and needs it both ways, because Obligations.sem_spec is an equivalence: the semidecider has to halt on every string whose verifier violates its time bound, and on no other.

That question is not answered by a step budget. A derivation of cost t takes at most 3 t machine steps (Machine.eval_steps_count), but a step is not a unit of cost: reading a variable or a constant is charged the size of the value (Machine.stepCost), so a run of 3 k steps can cost far more than k, and runForD returning a value says only that the program halted — not that it halted in budget.

So this file carries the cost along the run. Machine.stepCostD is Machine.stepCost on encoded configurations — the same seven program tags and four frame tags that Machine.stepEv and Machine.stepRet dispatch on — and Machine.costStep is the step function paired with the running total. Then

• Machine.evalForCostD p x k iterates it 3 k + 1 times and returns the result only if the configuration reached is final and the accumulated cost is at most k;
• Machine.haltsWithin_iff_evalForCostD is its correctness, in both directions: the budget 3 k + 1 is enough for every run of cost at most k (eval_steps_count), and the cost the iteration accumulates at a final configuration is the cost of the derivation that reached it (eval_of_steps, with costSum_final absorbing the steps after the end);
• Machine.primrec_haltsWithinB and Cost.decidableHaltsWithin are what comes out: Prog.HaltsWithin is a primitive recursive predicate of the program, the input and the budget, hence decidable. This is the noncomputable Cost.evalWithin made computable, as runForD is for Machine.evalData.

The file lives under Halting/ only because it needs Data.primrec_size, which Halting/Descriptions.lean proves; nothing in it knows about verifiers or descriptions.

The cost charged at a step, on encoded configurations

def MIPRE.Cost.Machine.stepCostEvD (p env : Data) : ℕ

The cost charged at an "evaluate p" step with environment env: the tags are those of Prog.toData, so 0 is var (charged the size of the value read), 5 is loop (free, its rules being charged when the body's value is dispatched), 6 and above are const (charged the size of the constant), and 1–4 are the remaining rules, each charged one.

Equations

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

def MIPRE.Cost.Machine.stepCostRetD (kont : Data) : ℕ

The cost charged at a "return" step: one when the frame on top is a loop1 (tag 3), and nothing otherwise — in particular nothing at a final configuration, whose stack is empty.

Equations

• MIPRE.Cost.Machine.stepCostRetD kont = if kont = MIPRE.Cost.Data.nil then 0 else if kont.left.left.unaryToNat = 3 then 1 else 0

def MIPRE.Cost.Machine.stepCostD (d : Data) : ℕ

Machine.stepCost on encoded configurations.

Equations

• MIPRE.Cost.Machine.stepCostD d = if d.left.left = MIPRE.Cost.Data.nil then MIPRE.Cost.Machine.stepCostEvD d.left.right d.right.left else MIPRE.Cost.Machine.stepCostRetD d.right.right

theorem MIPRE.Cost.Machine.stepCostD_toData (c : Cfg) : stepCostD c.toData = stepCost c

theorem MIPRE.Cost.Machine.primrec_stepCostEv : Primrec fun (q : Data × Data) => stepCostEvD q.1 q.2

theorem MIPRE.Cost.Machine.primrec_stepCostRet : Primrec stepCostRetD

theorem MIPRE.Cost.Machine.primrec_stepCostD : Primrec stepCostD

The run with its accumulated cost

def MIPRE.Cost.Machine.costStep (q : Data × ℕ) : Data × ℕ

One step of the machine, carrying the cost accumulated so far.

Equations

• MIPRE.Cost.Machine.costStep q = (MIPRE.Cost.Machine.stepData q.1, q.2 + MIPRE.Cost.Machine.stepCostD q.1)

theorem MIPRE.Cost.Machine.primrec_costStep : Primrec costStep

theorem MIPRE.Cost.Machine.costStep_iterate (c : Cfg) (s n : ℕ) : costStep^[n] (c.toData, s) = ((step^[n] c).toData, s + costSum c n)

def MIPRE.Cost.Machine.costRun (pd x : Data) (k : ℕ) : Data × ℕ

The configuration reached after 3 k + 1 cost-carrying steps, with the cost accumulated along the way.

Equations

• MIPRE.Cost.Machine.costRun pd x k = MIPRE.Cost.Machine.costStep^[3 * k + 1] (MIPRE.Cost.Machine.initData pd x, 0)

theorem MIPRE.Cost.Machine.costRun_eq (p : Prog) (x : Data) (k : ℕ) : costRun (encode p) x k = ((step^[3 * k + 1] { ctrl := Ctrl.ev p, env := [x], kont := [] }).toData, costSum { ctrl := Ctrl.ev p, env := [x], kont := [] } (3 * k + 1))

def MIPRE.Cost.Machine.evalForCostD (pd x : Data) (k : ℕ) : Option Data

Running p on x under a cost budget k: iterate the cost-carrying step 3 k + 1 times and read off the result if the configuration reached is final and the accumulated cost is within the budget. Total and primitive recursive.

Equations

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

theorem MIPRE.Cost.Machine.evalForCostD_eq_some {p : Prog} {x r : Data} {t k : ℕ} (h : p.Runs x r t) (hk : t ≤ k) : evalForCostD (encode p) x k = some r

Completeness. A run of cost at most the budget is found.

theorem MIPRE.Cost.Machine.haltsWithin_of_evalForCostD {p : Prog} {x r : Data} {k : ℕ} (h : evalForCostD (encode p) x k = some r) : HaltsWithin p x k

Soundness. Whatever is found is a genuine run of cost at most the budget.

theorem MIPRE.Cost.Machine.haltsWithin_iff_evalForCostD (p : Prog) (x : Data) (k : ℕ) : HaltsWithin p x k ↔ (evalForCostD (encode p) x k).isSome = true

The decision procedure. Halting within a cost budget is exactly what the cost-carrying iteration reports.

Computability

theorem MIPRE.Cost.Machine.primrec_costRun : Primrec fun (q : (Data × Data) × ℕ) => costRun q.1.1 q.1.2 q.2

theorem MIPRE.Cost.Machine.primrec_evalForCostD : Primrec fun (q : (Data × Data) × ℕ) => evalForCostD q.1.1 q.1.2 q.2

def MIPRE.Cost.Machine.haltsWithinB (pd x : Data) (k : ℕ) : Bool

Halting within a cost budget, as a Bool.

Equations

• MIPRE.Cost.Machine.haltsWithinB pd x k = (MIPRE.Cost.Machine.evalForCostD pd x k).isSome

theorem MIPRE.Cost.Machine.primrec_haltsWithinB : Primrec fun (q : (Data × Data) × ℕ) => haltsWithinB q.1.1 q.1.2 q.2

theorem MIPRE.Cost.Machine.haltsWithinB_iff (p : Prog) (x : Data) (k : ℕ) : haltsWithinB (encode p) x k = true ↔ HaltsWithin p x k

@[instance_reducible]

instance MIPRE.Cost.decidableHaltsWithin (p : Prog) (x : Data) (k : ℕ) : Decidable (HaltsWithin p x k)

Halting within a cost budget is decidable.

Equations

• MIPRE.Cost.decidableHaltsWithin p x k = decidable_of_iff (MIPRE.Cost.Machine.haltsWithinB (MIPRE.Cost.encode p) x k = true) ⋯