Uniform Selection Over a Type #
This file defines a typeclass SampleableType β for types β with a canonical uniform selection
operation, using the ProbComp monad.
Unlike HasUniformSelect, the class certifies full support and the uniform output measure.
All points have the same mass under a canonical uniform sampler.
Every element of a uniform sample over a Fintype has output probability card⁻¹.
Pushing a uniform sample through a bijection of α preserves each output probability.
Pushing forward uniform sampling along a bijection preserves output probabilities.
Binding after pushing forward uniform sampling along a bijection preserves output probabilities.
Left-translation by a constant in AddGroup α preserves the uniform output distribution,
since (m + ·) is a bijection on α with inverse (-m + ·).
Left-translating the bound variable of a uniform sample by a constant in AddGroup α
preserves the output distribution of the subsequent computation.
Right-translation analogue of probOutput_add_left_uniform: right-adding a constant to a
uniform sample in AddGroup α preserves the output distribution, since (· + m) is a bijection
on α with inverse (· + (-m)).
Right-translating the bound variable of a uniform sample by a constant in AddGroup α
preserves the output distribution of the subsequent computation.
Right-translation analogue of evalSPMF_add_left_uniform: right-adding a constant to a
uniform sample in AddGroup α preserves the full evaluation distribution.
Pushing forward uniform sampling via a bijection preserves the full evaluation distribution.
Bijective uniform + right-translation gives uniform. Sampling x ← $ᵗ α, transporting
through a bijection f : α → β, and right-adding any fixed m : β yields the same distribution
as sampling y ← $ᵗ β directly, as observed by any continuation cont : β → ProbComp γ.
This is the "one-time pad" fact underlying many cryptographic reductions: bijective transport
makes f x uniform on β, and in any AddGroup β right-translation (· + m) is a bijection
on the uniform measure, so the sum is again uniform.
Constant-irrelevance form of evalSPMF_bind_bijective_add_right_uniform: sampling through a
bijection and right-adding a constant has a distribution independent of the constant. Any two
offsets produce the same evaluation distribution.
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: the value
at coordinate t is uniform and independent of the others, so replacing it with a fresh
independent uniform draw leaves the joint distribution unchanged. It is the marginalization step
behind eager-sampling reformulations of oracle responses.
The first coordinate of a uniform pair is uniform.
Mapping the uniform distribution on α × β through Prod.fst yields the uniform distribution on
α: the Prod.fst-marginal of a uniform (product) distribution is uniform.
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
coordinates indexed by Set.range e: those coordinates are jointly uniform and independent of
the rest, and e reindexes the block by A. It underlies eager-sampling reformulations that
project a fine-grained random-oracle table onto a coarser one.
Patch a uniform function table at every point of a list l, drawing one fresh uniform value
per list entry. With l = [] the table is returned unchanged; with l = d :: ds the tail is
patched first and the head point d is then overwritten with a fresh uniform draw.
This is the iterated form of Function.update used by evalSPMF_uniformSample_patchList: the
outermost update is at the head, so the list is consumed head-first.
Instances For
Patching a uniform table at a finite list of coordinates with independent uniform draws preserves its output measure. Repeated coordinates are allowed.
Patching a uniform function table at finitely many points preserves uniformity.
Drawing a uniform table g : D → R and then patchTable l g — overwriting g at every point of
l with independent fresh uniform draws — yields the same distribution as drawing the table
directly. The points of l need not be distinct: each Function.update is the outermost
operation of its recursion step, so evalSPMF_uniformSample_bind_update applies regardless of
overlap. This is the marginalization step behind trace-conditioned eager-table reformulations,
where the patched points are determined only after the table is sampled.
Given an independent probabilistic computation ob : ProbComp Bool, the probability that its
output b' differs from a uniformly chosen boolean b is the same as the probability that they
are equal. In other words, P(b ≠ b') = P(b = b') where b is uniform.
Guessing a uniformly random bit after branching between real and rand decomposes into
the difference of the branch success probabilities.
If the distribution of f b is independent of b, then guessing a uniformly random
bit by running f has success probability exactly 1/2.
This is the core lemma behind "all-random hybrid has probability 1/2" arguments.
Uniformly sampling a response has the same distribution as issuing the corresponding query to a uniform oracle specification.
Uniformly sampling a response and issuing the corresponding uniform-oracle query assign the same probability to every output.
Uniformly sampling a response and issuing the corresponding uniform-oracle query assign the same probability to every event.