Polynomial-time source calls with an explicit unary resource

The outer verifier computes its exponential clock once. Passing that clock as unary data makes each bounded source query a genuine PolyTimeFun, so matrix-column queries and attained-prefix scans can use the existing bounded map and fold combinators. No polynomial bound in the binary clock is claimed.

noncomputable def MIPRE.Introspection.ClockedQuery.run (U : Cost.ClockedUniversalMachine) : Cost.PolyTimeFun (Cost.Unary × Cost.Prog × Cost.Data) Cost.Data

Equations

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

@[simp]

theorem MIPRE.Introspection.ClockedQuery.run_apply (U : Cost.ClockedUniversalMachine) (budget : Cost.Unary) (source : Cost.Prog) (input : Cost.Data) : (run U).toFun (budget, source, input) = Cost.clockedResult source input (List.length budget)