Running a program under a cost budget, computably

Machine.evalData runs a program to completion and is only partial recursive; and Cost.evalWithin, which reads off the result of a run within a budget, is noncomputable — it picks a witness out of an existential with Classical.choice. Neither can be used to compute anything, and the tabulation of a verifier's game (blueprint rem:compression-abstract, item 3) has to compute: it runs the decider on every answer tuple under the decider's own time bound and fills in an acceptance table.

Machine.runForD p x k is the computable version: iterate the machine's step function 3 k times from the initial configuration and read off the result if the configuration reached is final. Three facts make it right:

• a derivation of cost t is a machine run of at most 3 t steps (Machine.eval_steps_count — the free steps, entering a loop and returning to a cons or let frame, are each matched with a paid one), so the budget 3 k is enough for every run of cost at most k;
• final configurations are fixed by the step function (Machine.step_final), so iterating past the end is harmless and no exact step count is needed;
• the step function is primitive recursive on the encoded configurations (Machine.primrec_stepData), so the whole is (Machine.primrec_runForD).

runForD_eq_some and runs_of_runForD are the two directions of its correctness, and runForD_isSome_iff the decision procedure they add up to: for a program that halts within the budget on the input, whether it returns a given value is decidable, which is what boundedness buys the tabulation.

def MIPRE.Cost.Machine.isFinalB (d : Data) : Bool

Finality of a configuration as a Bool, so that the budgeted run is a plain branch.

Equations

• MIPRE.Cost.Machine.isFinalB d = decide (MIPRE.Cost.Machine.IsFinalD d)

@[simp]

theorem MIPRE.Cost.Machine.isFinalB_iff (d : Data) : isFinalB d = true ↔ IsFinalD d

theorem MIPRE.Cost.Machine.primrec_isFinalB : Primrec isFinalB

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

Running p on x under a cost budget k: iterate the step function 3 k times and read off the result if the configuration reached is final. Total and computable.

Equations

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

theorem MIPRE.Cost.Machine.stepData_iterate (c : Cfg) (n : ℕ) : stepData^[n] c.toData = (step^[n] c).toData

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

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

theorem MIPRE.Cost.Machine.runs_of_runForD {p : Prog} {x r : Data} {k : ℕ} (h : runForD (encode p) x k = some r) : ∃ (t : ℕ), p.Runs x r t

Soundness. Whatever is found is a genuine run.

theorem MIPRE.Cost.Machine.runForD_eq_some_iff {p : Prog} {x r : Data} {k : ℕ} (hb : HaltsWithin p x k) : runForD (encode p) x k = some r ↔ ∃ (t : ℕ), p.Runs x r t

The decision procedure. For a program that halts within the budget, whether it returns a given value is decidable.

Computability

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