Documentation

Complexity.Probability.Rewinding

The rewinding lemma #

A two-stage experiment runs a first stage with outcome s, draws a challenge t from challenge s, and lets a second stage answer t from s; it succeeds when a test ok s t a of the answer a passes. Rewinding keeps s and reruns the second stage on a fresh challenge, independent conditional on s. If every atom of challenge s has mass at most κ for every possible first-stage outcome, one-run success ε and two-run success with distinct challenges δ satisfy ε² − κ * ε ≤ δ (sq_sub_mul_le_twice) and ε ≤ κ + √δ (le_add_sqrt_twice). The atom bound is conditional on the saved state; a bound on the unconditional challenge distribution does not suffice.

This is an original extension of Boneh and Shoup's uniform-challenge rewinding lemma ([BS23], Lemma 19.2). For a uniform challenge among N possibilities, κ = 1 / N recovers ε² − ε / N ≤ δ (sq_sub_le_twice) and ε ≤ 1 / N + √δ (le_inv_add_sqrt_twice).

The second stage may use fresh randomness in each run. This generalizes the book's deterministic f(X, Y): averaging over the second stage's coins turns the indicator into a success probability p(s, t) ∈ [0, 1], and the proof needs only p ^ 2 ≤ p. The first stage and the answer may have infinitely many outcomes; the bounds assume a finite challenge type. These are exact statements about experiment laws, with no efficiency or sampler-realization claim.

The experiments are written in do notation for PMF, whose monad lives in a single universe; since they return a PMF Bool, the outcome, challenge and answer types are in Type.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Probability.Rewinding.once {S T A : Type} (first : PMF S) (challenge : S → PMF T) (answer : S → T → PMF A) (ok : S → T → A → Bool) :
PMF Bool

The law of one run of a two-stage experiment: the first stage, a challenge from the law chosen by that state, the second stage's answer, and its acceptance test.

Instances For
    source
    noncomputable def Cslib.Probability.Rewinding.twice {S T A : Type} [DecidableEq T] (first : PMF S) (challenge : S → PMF T) (answer : S → T → PMF A) (ok : S → T → A → Bool) :
    PMF Bool

    The law of rewinding: one first stage, then two challenges sampled independently from the same conditional law, and two answers with independent randomness. It succeeds when both answers pass their tests and the challenges are distinct.

    Instances For

      Proof of the rewinding lemma #

      Challenges with bounded atoms #

      source
      theorem Cslib.Probability.Rewinding.sq_sub_mul_le_twice {S T A : Type} [DecidableEq T] (first : PMF S) (challenge : S → PMF T) (answer : S → T → PMF A) (ok : S → T → A → Bool) [Finite T] {κ : ℝ} (hκ : ∀ s ∈ first.support, ∀ (t : T), ((challenge s) t).toReal ≤ κ) :
      ((once first challenge answer ok) true).toReal ^ 2 - κ * ((once first challenge answer ok) true).toReal ≤ ((twice first challenge answer ok) true).toReal

      Rewinding with bounded challenge atoms. If each conditional challenge law has atoms of mass at most κ, one-run success ε and two-run success at distinct challenges δ satisfy ε² − κ * ε ≤ δ. The bound is needed only on possible first-stage outcomes.

      This is an original extension of [BS23], Lemma 19.2, to biased challenges depending on the saved state. It concerns experiment laws, with no efficiency claim.

      source
      theorem Cslib.Probability.Rewinding.le_add_sqrt_twice {S T A : Type} [DecidableEq T] (first : PMF S) (challenge : S → PMF T) (answer : S → T → PMF A) (ok : S → T → A → Bool) [Finite T] {κ : ℝ} (hκ : ∀ s ∈ first.support, ∀ (t : T), ((challenge s) t).toReal ≤ κ) :
      ((once first challenge answer ok) true).toReal ≤ κ + √((twice first challenge answer ok) true).toReal

      The bounded-atom rewinding inequality solved for one-run success: ε ≤ κ + √δ. The conditional atom hypothesis implies κ ≥ 0; no separate sign assumption is needed.

      Uniform challenges #

      source
      theorem Cslib.Probability.Rewinding.sq_sub_le_twice {S T A : Type} [Fintype T] [DecidableEq T] (first : PMF S) (answer : S → T → PMF A) (ok : S → T → A → Bool) [Nonempty T] :
      ((once first (fun (x : S) => PMF.uniformOfFintype T) answer ok) true).toReal ^ 2 - ((once first (fun (x : S) => PMF.uniformOfFintype T) answer ok) true).toReal / ↑(Fintype.card T) ≤ ((twice first (fun (x : S) => PMF.uniformOfFintype T) answer ok) true).toReal

      Rewinding lemma ([BS23], Lemma 19.2): if one run succeeds with probability ε, then two runs sharing the first stage succeed with distinct challenges with probability at least ε ^ 2 - ε / N, where N is the number of uniform challenges.

      source
      theorem Cslib.Probability.Rewinding.le_inv_add_sqrt_twice {S T A : Type} [Fintype T] [DecidableEq T] (first : PMF S) (answer : S → T → PMF A) (ok : S → T → A → Bool) [Nonempty T] :
      ((once first (fun (x : S) => PMF.uniformOfFintype T) answer ok) true).toReal ≤ 1 / ↑(Fintype.card T) + √((twice first (fun (x : S) => PMF.uniformOfFintype T) answer ok) true).toReal

      The uniform rewinding lemma solved for the one-run probability ([BS23], from the proof of Theorem 19.1): ε ≤ 1 / N + √δ.