The running time of the output indicator

The time bound of L* (eq:time_bound_L*, II:8516) in the relative-cost reading: on an encoded input (n, x, y, a, b), the output indicator lstarProg prm L LP halts within lstarBound, an explicit function of the time T (|d| + 1)^k of the calls of L and LP on inputs (n, d), of the size of the input, and of the time bound of the check, polynomial in the size of the state it reads (lstarProg_halts). So it accepts what it accepts within that bound (lstar_acceptsWithin), the form in which the describer of lem:ar-window-describer reads it. The check is polynomial in its input and its input holds the answers a and b, so the bound is polynomial in their lengths: on the honest answers, in 2^ℓ and 2^◇.

noncomputable def MIPRE.Tailored.AnsRed.lstarBound (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) (T k S Z : ℕ) : ℕ

The explicit bound on the running time of the output indicator on an encoded input of size S, from the time T Z^k of a call whose argument has size less than Z.

Equations

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

theorem MIPRE.Tailored.AnsRed.lstarProg_halts (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {L P : Cost.Prog} (hL : Cost.Prog.WellScoped 1 L) (hP : Cost.Prog.WellScoped 1 P) {n T k : ℕ} (hLt : ∀ (d : Cost.Data), Cost.HaltsWithin L ((Cost.encode n).cons d) (T * (d.size + 1) ^ k)) (hPt : ∀ (d : Cost.Data), Cost.HaltsWithin P ((Cost.encode n).cons d) (T * (d.size + 1) ^ k)) (i : DIn) (hi : i.1 = n) : Cost.HaltsWithin (lstarProg prm L P) (Cost.encode i) (lstarBound prm T k (Cost.esize i) (2 * Cost.esize i + 2))

The output indicator halts within lstarBound on an encoded input of index n, when L and LP halt within T (|d| + 1)^k on every input (n, d): every call's argument is a component of the input, of size at most twice its size.

theorem MIPRE.Tailored.AnsRed.lstar_acceptsWithin (prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)) {ℓ : ℕ} (V : TailoredVerifier ℓ) {n T k : ℕ} (hLt : V.len.TimeBoundAt n T k) (hPt : V.lp.TimeBoundAt n T k) {x y a b : Cost.BitStr} (h : (lstar prm V).Accepts n x y a b) : (lstar prm V).AcceptsWithin n x y a b (lstarBound prm T k (Cost.esize (n, x, y, a, b)) (2 * Cost.esize (n, x, y, a, b) + 2))

The output indicator accepts within lstarBound whatever it accepts, on a tailored verifier whose two programs halt within T (|d| + 1)^k on every input (n, d).