Research proof index

In the random DDH game, the CDH-to-DDH reduction only matches the target with the uniform baseline probability. The bijectivity assumption identifies scalar samples with uniformly sampled group elements in the subgroup generated by g.

The eager random oracle, averaged over a uniformly sampled seed, matches the fresh independent-query semantics of evalDist. This is because the pre-sampled seed values are i.i.d. uniform, exactly matching fresh oracle queries. This is the analog of seededOracle.evalDist_liftComp_generateSeed_bind_simulateQ_run' but for eagerRandomOracle (which falls...

When the computation is within its query bound, enforcement is transparent: the output distribution is identical to running without enforcement.

For a computation that is structurally within budget, the budget check in the counting semantics is redundant on the support.

Overwriting one coordinate of a uniform function table is measure-preserving. Drawing a value u uniformly from R, then a full function table g : D → R uniformly, and returning Function.update g t u yields the same distribution as drawing the table directly. This is the t-marginal independence of the uniform (product) distribution on D → R:...

Restricting a uniform function table to a subdomain along an injection is uniform. For an injection e : A → B between finite types, drawing a uniform table g : B → R and restricting it along e (i.e. g ∘ e) yields the uniform distribution on A → R. This is the marginalization of the uniform (product) distribution on B → R onto the block of...