Replacing independent samples one coordinate at a time

sequenceHybrid draws an initial segment from a replacement source and the remaining segment from the original source. spliceTest samples the surrounding coordinates and inserts one challenge into the resulting list. Its adjacent-game laws expose the usual hybrid proof without tuple-index bookkeeping, and apply to arbitrary discrete sample types.

Main definitions

• Cslib.Crypto.sequenceHybrid: replace an initial segment of independent samples.
• Cslib.Crypto.spliceTest: insert one challenge between two independently sampled segments.
• Cslib.Crypto.sequenceTest: select one coordinate from a padded dyadic range.

Main results

• Cslib.Crypto.sequenceTest_gap: an exact signed gap with the dyadic sampling-range loss.
• Cslib.Crypto.sequenceTest_advantage: the corresponding exact unsigned loss, including count zero.
• Cslib.Crypto.isPPTOn_sequenceTest: a uniform strict PPT certificate, including padding indices.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 5, Games 3–5.

Adapted from Crypto/Computational/Hybrid/Sequence.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the current nonnegative game API.

def Cslib.Crypto.sequenceHybrid {α : Type} (replacement original : ProbComp α) (count split : ℕ) : ProbComp (List α)

Replace the initial split samples of an independent sequence.

def Cslib.Crypto.spliceTest {α : Type} (replacement original : ProbComp α) (before after : ℕ) (test : List α → ProbComp Bool) (challenge : α) : ProbComp Bool

Simulate all surrounding coordinates and insert the supplied challenge between them.

@[simp]

theorem Cslib.Crypto.sequenceHybrid_zero {α : Type} (replacement original : ProbComp α) (count : ℕ) : sequenceHybrid replacement original count 0 = OracleComp.replicate count original

@[simp]

theorem Cslib.Crypto.sequenceHybrid_self {α : Type} (replacement original : ProbComp α) (count : ℕ) : sequenceHybrid replacement original count count = OracleComp.replicate count replacement

theorem Cslib.Crypto.eval_spliceTest_original {α : Type} (replacement original : ProbComp α) (before after : ℕ) (test : List α → ProbComp Bool) : (original >>= spliceTest replacement original before after test).eval = (do let front ← OracleComp.replicate before replacement let back ← OracleComp.replicate (after + 1) original test (front ++ back)).eval

An original challenge supplies the first draw of the remaining original segment.

theorem Cslib.Crypto.eval_spliceTest_replacement {α : Type} (replacement original : ProbComp α) (before after : ℕ) (test : List α → ProbComp Bool) : (replacement >>= spliceTest replacement original before after test).eval = (do let front ← OracleComp.replicate (before + 1) replacement let back ← OracleComp.replicate after original test (front ++ back)).eval

A replacement challenge supplies the last draw of the replacement segment.

theorem Cslib.Crypto.eval_spliceTest_step_original {α : Type} (replacement original : ProbComp α) (count split : ℕ) (hsplit : split < count) (test : List α → ProbComp Bool) : (original >>= spliceTest replacement original split (count - split - 1) test).eval = (sequenceHybrid replacement original count split >>= test).eval

Inserting an original challenge gives the earlier adjacent hybrid.

theorem Cslib.Crypto.eval_spliceTest_step_replacement {α : Type} (replacement original : ProbComp α) (count split : ℕ) (test : List α → ProbComp Bool) : (replacement >>= spliceTest replacement original split (count - split - 1) test).eval = (sequenceHybrid replacement original count (split + 1) >>= test).eval

Inserting a replacement challenge gives the later adjacent hybrid.

noncomputable def Cslib.Crypto.sequenceTest {α : Type} (replacement original : ProbComp α) (count : ℕ) (test : List α → ProbComp Bool) (challenge : α) : ProbComp Bool

Sample a coordinate uniformly from a dyadic range and run its adjacent-hybrid test. Unused coordinates reject, so they contribute zero signed gap.

theorem Cslib.Crypto.sequenceTest_gap {α : Type} (replacement original : ProbComp α) (count : ℕ) (test : List α → ProbComp Bool) : ↑(Game.succProbability (OracleComp.replicate count original >>= test).eval) - ↑(Game.succProbability (OracleComp.replicate count replacement >>= test).eval) = ↑(Probability.dyadicSize count) * (↑(Game.succProbability (original >>= sequenceTest replacement original count test).eval) - ↑(Game.succProbability (replacement >>= sequenceTest replacement original count test).eval))

One uniform single-sample distinguisher captures the entire sequence gap, with the linear dyadic-range loss. The identity also covers zero repetitions.

theorem Cslib.Crypto.sequenceTest_advantage {α : Type} (replacement original : ProbComp α) (count : ℕ) (test : List α → ProbComp Bool) : Game.advantage (OracleComp.replicate count original >>= test).eval (OracleComp.replicate count replacement >>= test).eval = ↑(Probability.dyadicSize count) * Game.advantage (original >>= sequenceTest replacement original count test).eval (replacement >>= sequenceTest replacement original count test).eval

The exact unsigned sequence-hybrid loss, including the empty sequence.

theorem Cslib.Crypto.isPPTOn_sequenceHybrid {α Param : Type} {input : Param ↪ List Bool} {sample : α ↪ List Bool} {replacement original : Param → ProbComp α} {count split : Param → ℕ} (hreplacement : Probability.IsPPTOn input sample replacement) (horiginal : Probability.IsPPTOn input sample original) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hsplit : Turing.MultiTapeTM.ComputableTidilyInPolyTime split input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input (Turing.MultiTapeTM.encList sample) fun (a : Param) => sequenceHybrid (replacement a) (original a) (count a) (split a)

Efficient source programs and counts give an efficient independent hybrid sequence.

theorem Cslib.Crypto.isPPTOn_spliceTest {α Param : Type} {input : Param ↪ List Bool} {sample : α ↪ List Bool} {replacement original : Param → ProbComp α} {before after : Param → ℕ} {test : Param → List α → ProbComp Bool} {challenge : Param → α} (hreplacement : Probability.IsPPTOn input sample replacement) (horiginal : Probability.IsPPTOn input sample original) (hbefore : Turing.MultiTapeTM.ComputableTidilyInPolyTime before input Turing.MultiTapeTM.encUnary) (hafter : Turing.MultiTapeTM.ComputableTidilyInPolyTime after input Turing.MultiTapeTM.encUnary) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encList sample)) Turing.MultiTapeTM.encBool fun (pair : Param × List α) => test pair.1 pair.2) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime challenge input sample) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : Param) => spliceTest (replacement a) (original a) (before a) (after a) (test a) (challenge a)

The inserted challenge and every simulated coordinate are charged by the strict PPT certificate. The test may capture the complete original input.

theorem Cslib.Crypto.isPPTOn_sequenceTest {α Param : Type} {input : Param ↪ List Bool} {sample : α ↪ List Bool} {replacement original : Param → ProbComp α} {count : Param → ℕ} {test : Param → List α → ProbComp Bool} {challenge : Param → α} (hreplacement : Probability.IsPPTOn input sample replacement) (horiginal : Probability.IsPPTOn input sample original) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encList sample)) Turing.MultiTapeTM.encBool fun (pair : Param × List α) => test pair.1 pair.2) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime challenge input sample) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : Param) => sequenceTest (replacement a) (original a) (count a) (test a) (challenge a)

Random-coordinate hybrid reduction is uniformly strict PPT, including zero repetitions and all rejected padding indices.

theorem Cslib.Crypto.ComputationallyIndistinguishable.replicate_bind {orig repl : ℕ → ProbComp (List Bool)} (horig : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits orig) (hrepl : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits repl) (h : ComputationallyIndistinguishable (fun (n : ℕ) => (orig n).eval) fun (n : ℕ) => (repl n).eval) {count : ℕ → ℕ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {process : ℕ → List (List Bool) → ProbComp (List Bool)} (hprocess : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × List (List Bool)) => process p.1 p.2) : ComputationallyIndistinguishable (fun (n : ℕ) => (OracleComp.replicate (count n) (orig n) >>= process n).eval) fun (n : ℕ) => (OracleComp.replicate (count n) (repl n) >>= process n).eval

Repeating two computationally indistinguishable PPT samplers a polynomially bounded number of times and applying an efficient postprocessor preserves computational indistinguishability.