Research proof index

Support characterization for lazy random-oracle simulation. A value a can appear as the output of the random-oracle simulation from cache iff some total answer function agreeing with cache evaluates the computation to a. The final cache produced by the simulation is existentially quantified away.

Taking the first component of the WriterT output recovers the original computation, when the query implementation preserves the underlying oracle behavior (hso).

The number of uniform-oracle calls made by generateSeed spec qc js is exactly (js.map fun j => qc j * sampleCost j).sum, with each of the qc j samples at oracle j costing sampleCost j.

Predicate-targeted analogue of isTotalQueryBound_iff_counting_total_le: a counting-oracle filtered-sum bound characterizes the structural IsQueryBoundP bound.

Soundness: any path of the counting-oracle simulation of a p-bounded computation has sum of per-index counts over p-indices at most n.

Predicate-targeted query bounds are preserved by lifting along a SubSpec when the target predicate agrees with the source predicate on lifted queries. No LawfulSubSpec assumption is needed: query bounds only inspect query indices, not the distribution of responses.