Lazy sampling of random permutations and the PRP/PRF switching lemma

A bidirectional permutation oracle (PermOracleSpec α) answers forward queries (.forward x) and inverse queries (.inverse y) on a finite type α. We provide two lazy stateful samplers over an association-list cache Cache α = List (α × α):

1. Exact without-replacement lazy permutation (RandomPermutation.answer): on a cache hit, return the recorded image or preimage; on a cache miss, sample uniformly from the remaining unused range elements (unusedRange cache) for a forward query or from the remaining unused domain elements (unusedDomain cache) for an inverse query. Using OracleComp.run_interpret_simulation_of_invariant and uniform completion complete over the set extPerms cache of permutations extending the partial bijection, we prove that adaptive execution against answer followed by complete has the exact same joint distribution as sampling π ← PMF.uniformOfFintype (Equiv.Perm α) eagerly (run_interpret_answer_complete, uniform_interpret_eq_lazy).
2. Forgetful with-replacement lazy permutation (RandomPermutation.forgetfulAnswer, [BS23], Section 4.7): on a cache miss, sample uniformly from all of α without domain or range exclusion. By coupling answer and forgetfulAnswer via resampling and OracleComp.IdenticalUntilBad, any Q-query adaptive distinguisher has distinguishing advantage at most Q.choose 2 / |α| between a uniformly random permutation π ← PMF.uniformOfFintype (Equiv.Perm α) and forgetfulAnswer (abs_sub_uniformPerm_forgetful_le). On forward-only programs (liftForward), forgetfulAnswer coincides with memoize (fun _ => PMF.uniformOfFintype α) and therefore with a uniformly random function f ← PMF.uniformOfFintype (α → α), yielding the classical PRP/PRF switching lemma (abs_sub_uniformPerm_uniformFunc_le, [BS23], Section 4.4, Theorem 4.4).

Main definitions

• Cslib.RandomPermutation.PermQuery, PermQuery.ofBoolProd, PermOracleSpec, evalPerm, liftForward, liftBoolProd: bidirectional permutation queries, oracle specification, deterministic evaluation, and query liftings.
• Cslib.RandomPermutation.Cache, invLookup, AgreesWith, IsPartialBijection, extPerms, unusedDomain, unusedRange: partial bijection caches and extension sets.
• Cslib.RandomPermutation.answer, complete, forgetfulAnswer: exact and forgetful lazy bidirectional permutation samplers and uniform completion.

Main results

• Cslib.RandomPermutation.answer_complete, Cslib.RandomPermutation.run_interpret_answer_complete, Cslib.RandomPermutation.uniform_interpret_eq_lazy: exact eager/lazy equivalence for bidirectional random permutations.
• Cslib.RandomPermutation.toOuterMeasure_bad_choose_two_le: quadratic union bound (n * size s + n.choose 2) * δ for bad events with linearly growing step probability.
• Cslib.RandomPermutation.uniformPerm_bind_apply_le_forgetful, Cslib.RandomPermutation.forgetfulAnswer_bind_apply_le_uniformPerm, Cslib.RandomPermutation.toOuterMeasure_forgetfulAnswer_le_pairwise_and_length_le_add, Cslib.RandomPermutation.abs_sub_uniformPerm_forgetful_le: bidirectional random-permutation switching bounds (Q.choose 2 / |α|).
• Cslib.RandomPermutation.abs_sub_uniformPerm_uniformFunc_le: the PRP/PRF switching lemma ([BS23], Section 4.4, Theorem 4.4).

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 4.4 and 4.7 (Theorems 4.4 and 4.7).

Bidirectional permutation query interface

inductive Cslib.RandomPermutation.PermQuery (α : Type) : Type

A bidirectional query to a permutation on α: either evaluate in the forward direction or evaluate the inverse permutation.

• forward {α : Type} (x : α) : PermQuery α

  Forward query x ↦ π(x).

• inverse {α : Type} (y : α) : PermQuery α

  Inverse query y ↦ π⁻¹(y).

@[instance_reducible]

instance Cslib.RandomPermutation.instDecidableEqPermQuery {α✝ : Type} [DecidableEq α✝] : DecidableEq (PermQuery α✝)

def Cslib.RandomPermutation.instDecidableEqPermQuery.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : PermQuery α✝) : Decidable (x✝ = x✝¹)

@[reducible, inline]

abbrev Cslib.RandomPermutation.PermOracleSpec (α : Type) : OracleSpec (PermQuery α)

The oracle specification of a bidirectional permutation on α.

def Cslib.RandomPermutation.evalPerm {α : Type} (π : Equiv.Perm α) : PermQuery α → α

Deterministically answer a bidirectional permutation query using π : Equiv.Perm α.

@[simp]

theorem Cslib.RandomPermutation.evalPerm_forward {α : Type} (π : Equiv.Perm α) (x : α) : evalPerm π (PermQuery.forward x) = π x

Evaluating evalPerm π on a forward query .forward x applies π to x.

@[simp]

theorem Cslib.RandomPermutation.evalPerm_inverse {α : Type} (π : Equiv.Perm α) (y : α) : evalPerm π (PermQuery.inverse y) = (Equiv.symm π) y

Evaluating evalPerm π on an inverse query .inverse y applies π.symm to y.

def Cslib.RandomPermutation.liftForward {α β : Type} (program : OracleComp (fun (x : α) => α) β) : OracleComp (PermOracleSpec α) β

Lift a forward-only oracle program into a bidirectional permutation oracle program.

theorem Cslib.RandomPermutation.interpret_evalPerm_liftForward {α β : Type} (π : Equiv.Perm α) (program : OracleComp (fun (x : α) => α) β) : OracleComp.interpret (fun (q : PermQuery α) => PMF.pure (evalPerm π q)) (liftForward program) = OracleComp.interpret (fun (x : α) => PMF.pure (π x)) program

Interpreting liftForward program against evalPerm π is interpreting program against π.

theorem Cslib.RandomPermutation.isQueryBounded_liftForward {α β : Type} {program : OracleComp (fun (x : α) => α) β} {Q : ℕ} (hQ : program.IsQueryBounded Q) : (liftForward program).IsQueryBounded Q

Lifting a forward-only program preserves query bounds.

def Cslib.RandomPermutation.PermQuery.ofBoolProd {α : Type} : Bool × α → PermQuery α

Convert a boolean-tagged query (false, x) (forward) or (true, y) (inverse) into a PermQuery α.

@[simp]

theorem Cslib.RandomPermutation.PermQuery.ofBoolProd_false {α : Type} (x : α) : ofBoolProd (false, x) = forward x

Tag false converts (false, x) into the forward query .forward x.

@[simp]

theorem Cslib.RandomPermutation.PermQuery.ofBoolProd_true {α : Type} (y : α) : ofBoolProd (true, y) = inverse y

Tag true converts (true, y) into the inverse query .inverse y.

def Cslib.RandomPermutation.liftBoolProd {α β : Type} (program : OracleComp (fun (x : Bool × α) => α) β) : OracleComp (PermOracleSpec α) β

Lift a Bool × α bidirectional oracle program into a PermOracleSpec α program.

theorem Cslib.RandomPermutation.isQueryBounded_liftBoolProd {α β : Type} {program : OracleComp (fun (x : Bool × α) => α) β} {Q : ℕ} (hQ : program.IsQueryBounded Q) : (liftBoolProd program).IsQueryBounded Q

Lifting a Bool × α program preserves query bounds.

Partial bijection cache and lookup lemmas

@[reducible, inline]

abbrev Cslib.RandomPermutation.Cache (α : Type) : Type

A partial permutation table stored as a list of input-output pairs (x, y).

def Cslib.RandomPermutation.invLookup {α : Type} [DecidableEq α] (cache : Cache α) (y : α) : Option α

Lookup the preimage x of y in cache by searching (y, x) in cache.map Prod.swap.

@[simp]

theorem Cslib.RandomPermutation.invLookup_nil {α : Type} [DecidableEq α] (y : α) : invLookup [] y = none

Inverse lookup in the empty cache returns none.

theorem Cslib.RandomPermutation.invLookup_cons {α : Type} [DecidableEq α] (e : α × α) (cache : Cache α) (y : α) : invLookup (e :: cache) y = match y == e.2 with | true => some e.1 | false => invLookup cache y

Unfolding invLookup on a non-empty cache e :: cache.

theorem Cslib.RandomPermutation.mem_of_lookup_eq_some {α : Type} [DecidableEq α] {cache : Cache α} {x y : α} (h : List.lookup x cache = some y) : (x, y) ∈ cache

If cache.lookup x = some y, then the pair (x, y) belongs to cache.

theorem Cslib.RandomPermutation.mem_of_invLookup_eq_some {α : Type} [DecidableEq α] {cache : Cache α} {y x : α} (h : invLookup cache y = some x) : (x, y) ∈ cache

If invLookup cache y = some x, then the pair (x, y) belongs to cache.

theorem Cslib.RandomPermutation.lookup_eq_none_iff {α : Type} [DecidableEq α] {cache : Cache α} {x : α} : List.lookup x cache = none ↔ ∀ e ∈ cache, e.1 ≠ x

Forward lookup of x in cache returns none iff no entry in cache has first component x.

theorem Cslib.RandomPermutation.invLookup_eq_none_iff {α : Type} [DecidableEq α] {cache : Cache α} {y : α} : invLookup cache y = none ↔ ∀ e ∈ cache, e.2 ≠ y

Inverse lookup of y in cache returns none iff no entry in cache has second component y.

def Cslib.RandomPermutation.AgreesWith {α : Type} (cache : Cache α) (π : Equiv.Perm α) : Prop

A permutation π : Equiv.Perm α agrees with cache if π e.1 = e.2 for all e ∈ cache.

@[instance_reducible]

instance Cslib.RandomPermutation.decidableAgreesWith {α : Type} [DecidableEq α] (cache : Cache α) (π : Equiv.Perm α) : Decidable (AgreesWith cache π)

Decidability of AgreesWith cache π.

@[simp]

theorem Cslib.RandomPermutation.agreesWith_nil {α : Type} (π : Equiv.Perm α) : AgreesWith [] π

Every permutation agrees with the empty cache.

@[simp]

theorem Cslib.RandomPermutation.agreesWith_cons {α : Type} (e : α × α) (cache : Cache α) (π : Equiv.Perm α) : AgreesWith (e :: cache) π ↔ π e.1 = e.2 ∧ AgreesWith cache π

A permutation π agrees with e :: cache iff π e.1 = e.2 and π agrees with cache.

theorem Cslib.RandomPermutation.AgreesWith.apply_of_lookup_eq_some {α : Type} [DecidableEq α] {cache : Cache α} {π : Equiv.Perm α} (hπ : AgreesWith cache π) {x y : α} (h : List.lookup x cache = some y) : π x = y

If π agrees with cache and cache.lookup x = some y, then π x = y.

theorem Cslib.RandomPermutation.AgreesWith.symm_apply_of_invLookup_eq_some {α : Type} [DecidableEq α] {cache : Cache α} {π : Equiv.Perm α} (hπ : AgreesWith cache π) {y x : α} (h : invLookup cache y = some x) : (Equiv.symm π) y = x

If π agrees with cache and invLookup cache y = some x, then π.symm y = x.

theorem Cslib.RandomPermutation.AgreesWith.invLookup_apply_eq_none {α : Type} [DecidableEq α] {cache : Cache α} {π : Equiv.Perm α} (hπ : AgreesWith cache π) {x : α} (hx : List.lookup x cache = none) : invLookup cache (π x) = none

If π agrees with cache and x is not in the domain of cache, then π x is not in the range of cache.

theorem Cslib.RandomPermutation.AgreesWith.lookup_symm_apply_eq_none {α : Type} [DecidableEq α] {cache : Cache α} {π : Equiv.Perm α} (hπ : AgreesWith cache π) {y : α} (hy : invLookup cache y = none) : List.lookup ((Equiv.symm π) y) cache = none

If π agrees with cache and y is not in the range of cache, then π.symm y is not in the domain of cache.

theorem Cslib.RandomPermutation.AgreesWith.trans_swap_of_lookup_eq_none {α : Type} [DecidableEq α] {cache : Cache α} {π : Equiv.Perm α} (hπ : AgreesWith cache π) {x y : α} (hx : List.lookup x cache = none) (hy : invLookup cache y = none) : AgreesWith ((x, y) :: cache) (Equiv.trans π (Equiv.swap (π x) y))

Post-composing a permutation agreeing with cache by Equiv.swap (π x) y extends agreement to (x, y) :: cache when x and y are fresh.

theorem Cslib.RandomPermutation.AgreesWith.swap_trans_of_invLookup_eq_none {α : Type} [DecidableEq α] {cache : Cache α} {π : Equiv.Perm α} (hπ : AgreesWith cache π) {x y : α} (hx : List.lookup x cache = none) (hy : invLookup cache y = none) : AgreesWith ((x, y) :: cache) (Equiv.trans (Equiv.swap ((Equiv.symm π) y) x) π)

Pre-composing a permutation agreeing with cache by Equiv.swap (π.symm y) x extends agreement to (x, y) :: cache when x and y are fresh.

def Cslib.RandomPermutation.IsPartialBijection {α : Type} (cache : Cache α) : Prop

A cache is a partial bijection when at least one permutation on α extends it.

theorem Cslib.RandomPermutation.isPartialBijection_nil {α : Type} : IsPartialBijection []

The empty cache is a partial bijection, witnessed by the identity permutation.

theorem Cslib.RandomPermutation.IsPartialBijection.cons_of_lookup_eq_none {α : Type} [DecidableEq α] {cache : Cache α} (h : IsPartialBijection cache) {x y : α} (hx : List.lookup x cache = none) (hy : invLookup cache y = none) : IsPartialBijection ((x, y) :: cache)

Extending a partial bijection cache with a fresh domain element x and fresh range element y yields a partial bijection.

Finite domain/range complements and extension finsets

def Cslib.RandomPermutation.unusedDomain {α : Type} [DecidableEq α] [Fintype α] (cache : Cache α) : Finset α

Elements of α not yet present in the domain of cache.

def Cslib.RandomPermutation.unusedRange {α : Type} [DecidableEq α] [Fintype α] (cache : Cache α) : Finset α

Elements of α not yet present in the range of cache.

def Cslib.RandomPermutation.extPerms {α : Type} [DecidableEq α] [Fintype α] (cache : Cache α) : Finset (Equiv.Perm α)

Permutations π : Equiv.Perm α that agree with every entry in cache.

@[simp]

theorem Cslib.RandomPermutation.mem_unusedDomain_iff {α : Type} [DecidableEq α] [Fintype α] {cache : Cache α} {x : α} : x ∈ unusedDomain cache ↔ List.lookup x cache = none

An element x belongs to unusedDomain cache iff cache.lookup x = none.

@[simp]

theorem Cslib.RandomPermutation.mem_unusedRange_iff {α : Type} [DecidableEq α] [Fintype α] {cache : Cache α} {y : α} : y ∈ unusedRange cache ↔ invLookup cache y = none

An element y belongs to unusedRange cache iff invLookup cache y = none.

@[simp]

theorem Cslib.RandomPermutation.mem_extPerms_iff {α : Type} [DecidableEq α] [Fintype α] {cache : Cache α} {π : Equiv.Perm α} : π ∈ extPerms cache ↔ AgreesWith cache π

A permutation π belongs to extPerms cache iff AgreesWith cache π.

@[simp]

theorem Cslib.RandomPermutation.extPerms_nil {α : Type} [DecidableEq α] [Fintype α] : extPerms [] = Finset.univ

Every permutation extends the empty cache.

theorem Cslib.RandomPermutation.extPerms_nonempty_iff {α : Type} [DecidableEq α] [Fintype α] {cache : Cache α} : (extPerms cache).Nonempty ↔ IsPartialBijection cache

The extension finset extPerms cache is nonempty iff cache is a partial bijection.

theorem Cslib.RandomPermutation.IsPartialBijection.unusedRange_nonempty {α : Type} [DecidableEq α] [Fintype α] {cache : Cache α} (h : IsPartialBijection cache) {x : α} (hx : List.lookup x cache = none) : (unusedRange cache).Nonempty

When cache is a partial bijection and x is outside its domain, unusedRange cache is nonempty.

theorem Cslib.RandomPermutation.IsPartialBijection.unusedDomain_nonempty {α : Type} [DecidableEq α] [Fintype α] {cache : Cache α} (h : IsPartialBijection cache) {y : α} (hy : invLookup cache y = none) : (unusedDomain cache).Nonempty

When cache is a partial bijection and y is outside its range, unusedDomain cache is nonempty.

theorem Cslib.RandomPermutation.card_extPerms_eq_card_unusedRange_mul {α : Type} [DecidableEq α] [Fintype α] {cache : Cache α} {x y : α} (hx : List.lookup x cache = none) (hy : y ∈ unusedRange cache) : (extPerms cache).card = (unusedRange cache).card * (extPerms ((x, y) :: cache)).card

Partitioning extPerms cache by the image π x of a fresh input x shows that all fibers over unusedRange cache have equal size.

theorem Cslib.RandomPermutation.card_extPerms_eq_card_unusedDomain_mul {α : Type} [DecidableEq α] [Fintype α] {cache : Cache α} {x y : α} (hx : x ∈ unusedDomain cache) (hy : invLookup cache y = none) : (extPerms cache).card = (unusedDomain cache).card * (extPerms ((x, y) :: cache)).card

Partitioning extPerms cache by the preimage π.symm y of a fresh output y shows that all fibers over unusedDomain cache have equal size.

Exact lazy bidirectional permutation sampler and eager/lazy equivalence

noncomputable def Cslib.RandomPermutation.answer {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] (q : PermQuery α) : StateT (Cache α) PMF α

Exact without-replacement lazy bidirectional permutation oracle: return cached answers on hits, and sample uniformly from unusedRange cache (for .forward) or unusedDomain cache (for .inverse) on misses.

noncomputable def Cslib.RandomPermutation.complete {α : Type} [DecidableEq α] [Fintype α] (cache : Cache α) : PMF (Equiv.Perm α)

Uniformly sample a full permutation π : Equiv.Perm α extending cache.

@[simp]

theorem Cslib.RandomPermutation.complete_nil {α : Type} [DecidableEq α] [Fintype α] : complete [] = Probability.PMF.uniformOfFintype (Equiv.Perm α)

Completing the empty cache samples a uniformly random permutation on α.

theorem Cslib.RandomPermutation.answer_preserve_isPartialBijection {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] (q : PermQuery α) (cache : Cache α) (hcache : IsPartialBijection cache) (a : α) (cache' : Cache α) (hmem : (a, cache') ∈ (answer q cache).support) : IsPartialBijection cache'

answer preserves IsPartialBijection on every supported transition.

theorem Cslib.RandomPermutation.answer_complete {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] (q : PermQuery α) (cache : Cache α) (hcache : IsPartialBijection cache) : ((answer q cache).bind fun (x : α × Cache α) => match x with | (a, cache') => PMF.map (fun (x : Equiv.Perm α) => (a, x)) (complete cache')) = PMF.map (fun (π : Equiv.Perm α) => (evalPerm π q, π)) (complete cache)

Answering one bidirectional query lazily and then completing the partial bijection has the exact same joint distribution on (answer, π) as completing first and evaluating evalPerm π q.

theorem Cslib.RandomPermutation.run_interpret_answer_complete {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] {β : Type} (program : OracleComp (PermOracleSpec α) β) (cache : Cache α) (hcache : IsPartialBijection cache) : (do let __x ← (OracleComp.interpret answer program).run cache match __x with | (result, cache') => PMF.map (fun (x : Equiv.Perm α) => (result, x)) (complete cache')) = do let π ← complete cache PMF.map (fun (x : β) => (x, π)) (OracleComp.interpret (fun (q : PermQuery α) => PMF.pure (evalPerm π q)) program)

Eager/lazy equivalence for bidirectional permutations: running an adaptive program against answer from any partial bijection cache and then completing cache' to a full permutation gives the same joint distribution on (result, π) as completing cache first and answering queries via evalPerm π.

theorem Cslib.RandomPermutation.uniform_interpret_eq_lazy {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] {β : Type} (program : OracleComp (PermOracleSpec α) β) : (do let π ← Probability.PMF.uniformOfFintype (Equiv.Perm α) OracleComp.interpret (fun (q : PermQuery α) => PMF.pure (evalPerm π q)) program) = PMF.map Prod.fst ((OracleComp.interpret answer program).run [])

Uniform random permutation equals lazy bidirectional sampling: sampling a uniform permutation π ← PMF.uniformOfFintype (Equiv.Perm α) and answering bidirectional queries via evalPerm π has the exact same output distribution as running answer from the empty cache [].

Forgetful lazy permutation sampler and bidirectional switching bound

noncomputable def Cslib.RandomPermutation.forgetfulAnswer {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] (q : PermQuery α) : StateT (Cache α) PMF α

Forgetful lazy bidirectional permutation oracle ([BS23], Section 4.7): return the cached image/preimage on a hit, and sample uniformly from all of α (with replacement) on a miss.

theorem Cslib.RandomPermutation.run_interpret_forgetfulAnswer_liftForward {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] {β : Type} (program : OracleComp (fun (x : α) => α) β) (cache : Cache α) : (OracleComp.interpret forgetfulAnswer (liftForward program)).run cache = (OracleComp.interpret (memoize fun (x : α) => Probability.PMF.uniformOfFintype α) program).run cache

On forward-only programs (liftForward), forgetfulAnswer never queries invLookup, so its joint result and cache distribution is identical to memoize (fun _ => PMF.uniformOfFintype α).

Quadratic union bound for linearly growing collision sets

theorem Cslib.RandomPermutation.toOuterMeasure_bad_choose_two_le {ι σ β : Type} {spec : ι → Type} {handler : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} (size : σ → ℕ) (δ : ENNReal) (hstep : ∀ (q : ι) (s : σ), ¬bad s → (handler q s).toOuterMeasure {x : spec q × σ | bad x.2} ≤ ↑(size s) * δ) (hgrow : ∀ (q : ι) (s : σ), ¬bad s → ∀ x ∈ (handler q s).support, ¬bad x.2 → size x.2 ≤ size s + 1) {program : OracleComp spec β} {n : ℕ} (hn : program.IsQueryBounded n) {s : σ} (hs : ¬bad s) : ((OracleComp.interpret handler program).run s).toOuterMeasure {x : β × σ | bad x.2} ≤ ↑(n * size s + n.choose 2) * δ

If each oracle call from a good state s turns bad with probability at most size s * δ and increases size by at most 1, then an adaptive program making at most n queries reaches a bad state from s with probability at most (n * size s + n.choose 2) * δ.

theorem Cslib.RandomPermutation.uniformPerm_bind_apply_le_forgetful {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] {β γ : Type} {program : OracleComp (PermOracleSpec α) β} {Q : ℕ} (hQ : program.IsQueryBounded Q) (next : β → PMF γ) (c : γ) : ((do let π ← Probability.PMF.uniformOfFintype (Equiv.Perm α) OracleComp.interpret (fun (q : PermQuery α) => PMF.pure (evalPerm π q)) program).bind next) c ≤ ((PMF.map Prod.fst ((OracleComp.interpret forgetfulAnswer program).run [])).bind next) c + ↑(Q.choose 2) * (↑(Fintype.card α))⁻¹

Bidirectional random-permutation switching inequality (ℝ≥0∞, one-sided): for any Q-query adaptive program, evaluating against a uniform permutation accepts within Q.choose 2 * |α|⁻¹ of evaluating against forgetfulAnswer.

theorem Cslib.RandomPermutation.forgetfulAnswer_bind_apply_le_uniformPerm {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] {β γ : Type} {program : OracleComp (PermOracleSpec α) β} {Q : ℕ} (hQ : program.IsQueryBounded Q) (next : β → PMF γ) (c : γ) : ((PMF.map Prod.fst ((OracleComp.interpret forgetfulAnswer program).run [])).bind next) c ≤ ((do let π ← Probability.PMF.uniformOfFintype (Equiv.Perm α) OracleComp.interpret (fun (q : PermQuery α) => PMF.pure (evalPerm π q)) program).bind next) c + ↑(Q.choose 2) * (↑(Fintype.card α))⁻¹

Reverse bidirectional random-permutation switching inequality (ℝ≥0∞, one-sided): for any Q-query adaptive program, evaluating against forgetfulAnswer accepts within Q.choose 2 * |α|⁻¹ of evaluating against a uniform permutation.

theorem Cslib.RandomPermutation.toOuterMeasure_forgetfulAnswer_le_pairwise_and_length_le_add {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] {β : Type} {program : OracleComp (PermOracleSpec α) β} {Q : ℕ} (hQ : program.IsQueryBounded Q) (P : Cache α → Prop) : ((OracleComp.interpret forgetfulAnswer program).run []).toOuterMeasure {x : β × Cache α | P x.2} ≤ ((OracleComp.interpret forgetfulAnswer program).run []).toOuterMeasure {x : β × Cache α | (List.Pairwise (fun (a b : α × α) => a.1 ≠ b.1) x.2 ∧ List.Pairwise (fun (a b : α × α) => a.2 ≠ b.2) x.2 ∧ List.length x.2 ≤ Q) ∧ P x.2} + ↑(Q.choose 2) * (↑(Fintype.card α))⁻¹

Any final-cache event P under forgetfulAnswer on a Q-query-bounded program has probability at most that of (c.Pairwise (fun a b => a.1 ≠ b.1) ∧ c.Pairwise (fun a b => a.2 ≠ b.2) ∧ c.length ≤ Q) ∧ P c plus the Q.choose 2 * |α|⁻¹ collision probability of forgetfulWithBad.

theorem Cslib.RandomPermutation.abs_sub_uniformPerm_forgetful_le {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] {β γ : Type} {program : OracleComp (PermOracleSpec α) β} {Q : ℕ} (hQ : program.IsQueryBounded Q) (next : β → PMF γ) (c : γ) : |(((do let π ← Probability.PMF.uniformOfFintype (Equiv.Perm α) OracleComp.interpret (fun (q : PermQuery α) => PMF.pure (evalPerm π q)) program).bind next) c).toReal - (((PMF.map Prod.fst ((OracleComp.interpret forgetfulAnswer program).run [])).bind next) c).toReal| ≤ ↑(Q.choose 2) * (↑(Fintype.card α))⁻¹

Bidirectional random-permutation switching bound (ℝ, two-sided, [BS23], Section 4.7): for any Q-query adaptive program, the output distributions under a uniform permutation π ← PMF.uniformOfFintype (Equiv.Perm α) and under the forgetful lazy sampler forgetfulAnswer differ in probability on every event by at most Q.choose 2 / |α|.

theorem Cslib.RandomPermutation.abs_sub_uniformPerm_uniformFunc_le {α : Type} [DecidableEq α] [Fintype α] [Nonempty α] {β γ : Type} {program : OracleComp (fun (x : α) => α) β} {Q : ℕ} (hQ : program.IsQueryBounded Q) (next : β → PMF γ) (c : γ) : |(((do let π ← Probability.PMF.uniformOfFintype (Equiv.Perm α) OracleComp.interpret (fun (x : α) => PMF.pure (π x)) program).bind next) c).toReal - (((do let f ← Probability.PMF.uniformOfFintype (α → α) OracleComp.interpret (fun (x : α) => PMF.pure (f x)) program).bind next) c).toReal| ≤ ↑(Q.choose 2) * (↑(Fintype.card α))⁻¹

The PRP/PRF switching lemma (ℝ, two-sided, [BS23], Section 4.4, Theorem 4.4): for any Q-query forward-only adaptive program program : OracleComp (fun _ : α => α) β, the acceptance probabilities under a uniformly random permutation π ← PMF.uniformOfFintype (Equiv.Perm α) and under a uniformly random function f ← PMF.uniformOfFintype (α → α) differ by at most Q.choose 2 / |α|.