Evaluating the GGM tree

Starting from a secret root label, follow the query bits down a binary tree. Each expansion provides two labels of the current seed width. The evaluator is an ordinary word fold, and its polynomial-time certificate comes from the fold compiler.

Extra generator output is discarded. In particular, a generator of length 2 * n + 1 supplies both n-bit children even at n = 0, where the result is the empty word.

This module proves evaluation and size properties. Pseudorandomness requires the adaptive oracle hybrid argument in addition to these facts.

The functional construction is ported from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8; efficiency uses the existing tidy machine calculus.

Main definitions

• Cslib.Crypto.GGM.eval: evaluate a binary query by folding child selection over its bits.

Main results

• Cslib.Crypto.GGM.length_eval: evaluation preserves the seed width for full expansions.
• Cslib.Crypto.GGM.computableTidilyInPolyTime_eval: a uniform machine certificate without a cryptographic security hypothesis or an output-length hypothesis on the generator.

References

• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions, Section 3.2.

def Cslib.Crypto.GGM.selectChild (width : ℕ) (expansion : List Bool) (bit : Bool) : List Bool

Select one of the two consecutive child labels, discarding any surplus expansion bits.

theorem Cslib.Crypto.GGM.length_selectChild_le (width : ℕ) (expansion : List Bool) (bit : Bool) : (selectChild width expansion bit).length ≤ width

Each child fits in the declared width, even when the expansion is short.

@[simp]

theorem Cslib.Crypto.GGM.selectChild_take (width : ℕ) (expansion : List Bool) (bit : Bool) : selectChild width (List.take (2 * width) expansion) bit = selectChild width expansion bit

Child selection inspects only the first two labels.

def Cslib.Crypto.GGM.child (generator : List Bool → List Bool) (seed : List Bool) (bit : Bool) : List Bool

Expand a node and select the child indicated by one query bit.

def Cslib.Crypto.GGM.eval (generator : List Bool → List Bool) (seed query : List Bool) : List Bool

Follow a query from a root seed, reading its bits from left to right.

@[simp]

theorem Cslib.Crypto.GGM.eval_truncate (generator : List Bool → List Bool) : (eval fun (seed : List Bool) => List.take (2 * seed.length) (generator seed)) = eval generator

Tree evaluation uses only the first two labels of every generator output.

@[simp]

theorem Cslib.Crypto.GGM.eval_nil (generator : List Bool → List Bool) (seed : List Bool) : eval generator seed [] = seed

@[simp]

theorem Cslib.Crypto.GGM.eval_cons (generator : List Bool → List Bool) (seed : List Bool) (bit : Bool) (query : List Bool) : eval generator seed (bit :: query) = eval generator (child generator seed bit) query

theorem Cslib.Crypto.GGM.eval_append (generator : List Bool → List Bool) (seed path suffix : List Bool) : eval generator seed (path ++ suffix) = eval generator (eval generator seed path) suffix

A shared query prefix leads to the same intermediate node.

theorem Cslib.Crypto.GGM.eval_drop_succ (generator : List Bool → List Bool) (seed query : List Bool) (depth : ℕ) (hdepth : depth < query.length) : eval generator seed (List.drop depth query) = eval generator (child generator seed (query[depth]?.getD false)) (List.drop (depth + 1) query)

Expose the next edge of a nonempty suffix using its position in the original query.

theorem Cslib.Crypto.GGM.length_child_le (generator : List Bool → List Bool) (seed : List Bool) (bit : Bool) : (child generator seed bit).length ≤ seed.length

Truncation bounds intermediate labels even for an arbitrary generator.

theorem Cslib.Crypto.GGM.length_child {generator : List Bool → List Bool} (hlength : ∀ (seed : List Bool), 2 * seed.length ≤ (generator seed).length) (seed : List Bool) (bit : Bool) : (child generator seed bit).length = seed.length

A generator providing two full labels preserves the seed width on each edge.

theorem Cslib.Crypto.GGM.length_eval_le (generator : List Bool → List Bool) (seed query : List Bool) : (eval generator seed query).length ≤ seed.length

All labels encountered by tree evaluation fit in the original seed width.

theorem Cslib.Crypto.GGM.length_eval {generator : List Bool → List Bool} (hlength : ∀ (seed : List Bool), 2 * seed.length ≤ (generator seed).length) (seed query : List Bool) : (eval generator seed query).length = seed.length

Tree evaluation preserves the seed width at every depth when both children are full length.

theorem Cslib.Crypto.GGM.computableTidilyInPolyTime_selectChild {α : Type} {input : α ↪ List Bool} {width : α → ℕ} {expansion : α → List Bool} {bit : α → Bool} (hwidth : Turing.MultiTapeTM.ComputableTidilyInPolyTime width input Turing.MultiTapeTM.encUnary) (hexpansion : Turing.MultiTapeTM.ComputableTidilyInPolyTime expansion input Turing.MultiTapeTM.encBits) (hbit : Turing.MultiTapeTM.ComputableTidilyInPolyTime bit input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => selectChild (width a) (expansion a) (bit a)) input Turing.MultiTapeTM.encBits

Select a child using a computed unary width and ordinary bit-string slicing.

theorem Cslib.Crypto.GGM.computableTidilyInPolyTime_child {generator : List Bool → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × Bool) => child generator pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBits

Computing one child invokes the certified generator and slices its output.

theorem Cslib.Crypto.GGM.computableTidilyInPolyTime_eval {generator : List Bool → List Bool} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => eval generator pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

The GGM evaluator is polynomial time whenever its generator is. Its fold has no state growth, so this certificate needs no security or output-length assumption.