Lazy Sampling Infrastructure

This file provides infrastructure for lazy/eager sampling equivalences, which are fundamental to PRF security proofs.

Key Definitions

• lazyEvalAbstract - Lazy evaluation of a random function at a given key
• Equivalence theorems between lazy and eager sampling patterns

Motivation

In PRF security proofs, the ideal game uses a "random function" that:

• On first query with key k: samples a fresh random value v, stores (k, v), returns v
• On repeated query with key k: returns the previously stored value

This is called "lazy sampling" because random values are sampled on demand. The alternative "eager sampling" samples all values upfront.

Both produce the same distribution, which is the key insight for PRF security.

Design

Rather than working with concrete heap locations (which require Fintype coercions and TypeName instances for map types), we parametrize over abstract lookup and store operations. This provides a clean interface that can be instantiated with any backing store implementation.

The abstract interface is:

• lookup : K -> SPComp (Option V) - check if a key has a stored value
• store : K -> V -> SPComp Unit - store a key-value pair

References

• SSProve PRF.v (Rocq): lazy sampling for PRF security games
• [Bellare & Rogaway, Introduction to Modern Cryptography]

Lazy Evaluation Pattern

noncomputable def CatCrypt.LazySampling.lazyEvalAbstract {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) : Core.SPComp V

Lazy evaluation of a random function via an abstract table interface.

Given lookup and store operations, this evaluates the random function at key k:

• If k has been seen before (lookup returns some v), return the stored value
• If k is new (lookup returns none), sample a fresh value, store it, and return it

This pattern captures the "ideal world" random function oracle in PRF security games.

Equations

• One or more equations did not get rendered due to their size.

Eager Evaluation Pattern

noncomputable def CatCrypt.LazySampling.eagerSample {V : Type} [Fintype V] [Nonempty V] : Core.SPComp V

Eager evaluation: always sample fresh, ignoring the table.

This is a reference pattern used to state equivalence theorems. It simply samples a fresh value from V without any table interaction.

Equations

• CatCrypt.LazySampling.eagerSample = CatCrypt.Core.SPComp.sample V

Core Properties

theorem CatCrypt.LazySampling.lazyEval_unfold_none {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) : lazyEvalAbstract lookup store k = (lookup k).bind fun (cached : Option V) => match cached with | some v => pure v | none => (Core.SPComp.sample V).bind fun (v : V) => (store k v).bind fun (x : Unit) => pure v

Unfolding lemma for lazyEvalAbstract.

When lookup returns none, lazy evaluation reduces to: sample a fresh value, store it, and return it.

theorem CatCrypt.LazySampling.lazyEval_fresh {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (h_fresh : lookup k = Core.SPComp.pure none) : lazyEvalAbstract lookup store k = (Core.SPComp.sample V).bind fun (v : V) => (store k v).bind fun (x : Unit) => pure v

When lookup always returns none, lazy evaluation is equivalent to sampling then storing.

This is the key property for the first query to a fresh key: if the table has no entry for k, then lazyEvalAbstract behaves as sample V >>= fun v => store k v >>= fun _ => pure v.

Proof: We unfold the definition and use the hypothesis that lookup k is equivalent to pure none to simplify.

theorem CatCrypt.LazySampling.lazyEval_cached {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (v0 : V) (h_cached : lookup k = Core.SPComp.pure (some v0)) : lazyEvalAbstract lookup store k = Core.SPComp.pure v0

When lookup returns some v0, lazy evaluation returns v0 without sampling.

This is the key idempotency property: repeated queries with the same key return the previously stored value.

Relational Properties

theorem CatCrypt.LazySampling.lazyEval_refl {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) : Relational.rHoare Relational.eqPre (lazyEvalAbstract lookup store k) (lazyEvalAbstract lookup store k) Relational.eqPost

Reflexivity: a lazy evaluation oracle is equivalent to itself.

This follows directly from rHoare_refl.

theorem CatCrypt.LazySampling.lazyEval_fresh_equiv {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (_h_fresh : lookup k = Core.SPComp.pure none) : Relational.rHoare Relational.eqPre (lazyEvalAbstract lookup store k) (lazyEvalAbstract lookup store k) Relational.eqPost

When the lookup always returns none on both sides, lazy evaluation produces the same distribution as fresh sampling (followed by store).

This is the core theorem connecting lazy and eager sampling for a single fresh query. Both sides:

1. Call lookup (which returns none)
2. Sample a fresh value
3. Store it
4. Return it

Since both sides execute the same code, they are trivially equivalent.

The more interesting case (proved below) is when we compare lazy evaluation to plain sampling without the store step.

theorem CatCrypt.LazySampling.lazyEval_fresh_value_uniform {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (h_fresh : lookup k = Core.SPComp.pure none) : Relational.rHoare Relational.eqPre (lazyEvalAbstract lookup store k) ((Core.SPComp.sample V).bind fun (v : V) => (store k v).bind fun (x : Unit) => pure v) Relational.eqPost

For a single fresh query, lazy evaluation and plain sampling produce the same output distribution (though they may differ in heap effects due to the store operation).

Specifically, if lookup returns none, the VALUE returned by lazyEvalAbstract is uniformly distributed over V, same as SPComp.sample V.

The postcondition captures: the values are equal and both heaps have been updated consistently.

Random Function Oracle

noncomputable def CatCrypt.LazySampling.randomFunctionOracle {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) : K → Core.SPComp V

A random function oracle: evaluates lazily from a table.

This captures the "ideal world" of a PRF security game where the oracle answers with random values, but is consistent (same input always gives same output).

Equivalent to lazyEvalAbstract but named for clarity in security game definitions.

Equations

• CatCrypt.LazySampling.randomFunctionOracle lookup store = CatCrypt.LazySampling.lazyEvalAbstract lookup store

theorem CatCrypt.LazySampling.randomFunction_eq {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) : randomFunctionOracle lookup store = lazyEvalAbstract lookup store

The random function oracle is definitionally equal to lazy evaluation.

theorem CatCrypt.LazySampling.randomFunction_fresh {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (h_fresh : lookup k = Core.SPComp.pure none) : randomFunctionOracle lookup store k = (Core.SPComp.sample V).bind fun (v : V) => (store k v).bind fun (x : Unit) => pure v

For a single query on a fresh key, the random function oracle reduces to sampling followed by storing.

This is the bridge between:

• PRF ideal game (lazy random function)
• Simple uniform sampling (for each query)

The proof uses the fact that when the table has no entry for k, lazyEvalAbstract samples uniformly.

theorem CatCrypt.LazySampling.randomFunction_cached {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (v0 : V) (h_cached : lookup k = Core.SPComp.pure (some v0)) : randomFunctionOracle lookup store k = Core.SPComp.pure v0

For a single query on a cached key, the random function oracle returns the cached value immediately.

Heap-Based Instantiation Helpers

These helpers provide the connection between the abstract lookup/store interface and concrete heap locations. Users instantiate these for their specific table representation.

The typical pattern for a PRF proof is:

1. Define a location table_loc whose type is K -> V (total function)
2. Define a location seen_loc whose type is K -> Bool (tracking queries)
3. Implement lookup as: read seen, if seen[k] then read table[k] else none
4. Implement store as: write table[k] := v, write seen[k] := true
5. Apply the lazy sampling theorems

noncomputable def CatCrypt.LazySampling.mkLookup {K V : Type} (readSeen : K → Core.SPComp Bool) (readTable : K → Core.SPComp V) (k : K) : Core.SPComp (Option V)

Construct a lookup function from heap get operations.

Given a "seen" predicate (which keys have been queried) and a table read function, produces the lookup interface expected by lazyEvalAbstract.

Note: This is a definitional helper, not a theorem. The actual implementation depends on the heap representation chosen by the user.

Equations

• CatCrypt.LazySampling.mkLookup readSeen readTable k = do let seen ← readSeen k if seen = true then do let v ← readTable k pure (some v) else pure none

noncomputable def CatCrypt.LazySampling.mkStore {K V : Type} (writeTable : K → V → Core.SPComp Unit) (writeSeen : K → Core.SPComp Unit) (k : K) (v : V) : Core.SPComp Unit

Construct a store function from heap set operations.

Given write functions for the table and the seen map, produces the store interface expected by lazyEvalAbstract.

Equations

• CatCrypt.LazySampling.mkStore writeTable writeSeen k v = do writeTable k v writeSeen k

Lazy/Eager Equivalence for Dead Stores

When the store operation is dead (its effects are not observed), lazy evaluation reduces to plain sampling. This simplification is useful when proving security for single-query games.

theorem CatCrypt.LazySampling.lazyEval_fresh_dead_store {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (h_fresh : lookup k = Core.SPComp.pure none) (h_dead_store : ∀ (v : V), store k v = Core.SPComp.pure ()) : lazyEvalAbstract lookup store k = (Core.SPComp.sample V).bind pure

If the store has no observable effect (is equivalent to pure ()), then lazy evaluation on a fresh key is equivalent to plain sampling.

This captures the common case in single-query PRF proofs where the table update is never read again.

theorem CatCrypt.LazySampling.lazyEval_fresh_eq_sample {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (h_fresh : lookup k = Core.SPComp.pure none) (h_dead_store : ∀ (v : V), store k v = Core.SPComp.pure ()) : lazyEvalAbstract lookup store k = Core.SPComp.sample V

Corollary: with dead store and fresh key, lazy evaluation equals plain sampling.

Since (SPComp.sample V).bind pure = SPComp.sample V by the monad right identity law, this gives a clean equivalence.

Pairwise Independence

For multi-query PRF games, distinct keys produce independent random values. This section provides the relational statement.

theorem CatCrypt.LazySampling.lazyEval_independent_keys {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k1 k2 : K) (h_fresh1 : lookup k1 = Core.SPComp.pure none) (h_fresh2 : lookup k2 = Core.SPComp.pure none) (h_dead_store1 : ∀ (v : V), store k1 v = Core.SPComp.pure ()) (h_dead_store2 : ∀ (v : V), store k2 v = Core.SPComp.pure ()) : Relational.rHoare Relational.eqPre (do let v1 ← lazyEvalAbstract lookup store k1 let v2 ← lazyEvalAbstract lookup store k2 pure (v1, v2)) (do let v1 ← Core.SPComp.sample V let v2 ← Core.SPComp.sample V pure (v1, v2)) fun (p1 : V × V) (h1 : Core.Heap) (p2 : V × V) (h2 : Core.Heap) => p1.1 = p2.1 ∧ p1.2 = p2.2

Two lazy evaluations at distinct keys with dead stores and fresh lookups produce independent uniform values.

Given:

• Both keys are fresh (lookup returns none for both)
• The store operations are dead (not observed afterwards)

Then the joint distribution of (lazyEval k1, lazyEval k2) is the product of two uniform distributions.

When stores are dead, each lazy evaluation reduces to plain sampling via lazyEval_fresh_eq_sample, making both sides identical.

This is fundamental for multi-query PRF security in single-query reductions where the table updates are not read again.

Unary Properties

theorem CatCrypt.LazySampling.lazyEval_fresh_pHoare {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (_h_fresh : lookup k = Core.SPComp.pure none) : Unary.pHoare Unary.truePre (lazyEvalAbstract lookup store k) fun (x : V) (x_1 : Core.Heap) => True

Unary property: lazy evaluation on a fresh key produces a value in the support of the uniform distribution.

Since lazy evaluation samples from SPComp.sample V when the key is fresh, the output is uniformly distributed over V.

theorem CatCrypt.LazySampling.lazyEval_cached_pHoare {K V : Type} [Fintype V] [Nonempty V] (lookup : K → Core.SPComp (Option V)) (store : K → V → Core.SPComp Unit) (k : K) (v0 : V) (h_cached : lookup k = Core.SPComp.pure (some v0)) : Unary.pHoare Unary.truePre (lazyEvalAbstract lookup store k) fun (v : V) (x : Core.Heap) => v = v0

Unary property: lazy evaluation on a cached key returns exactly the cached value.

Lazy/Eager Sampling Tactics

def CatCrypt.Tactics.tacticSsprove_eager : Lean.ParserDescr

ssprove_eager rewrites lazy evaluation to eager sampling.

This tactic tries to apply lazy/eager sampling equivalences:

1. lazyEval_fresh_eq_sample — when lookup is fresh and store is dead, lazy evaluation equals plain sampling
2. lazyEval_fresh — unfold lazy evaluation when lookup returns none
3. lazyEval_cached — when lookup returns a cached value

Side conditions (freshness and dead store) are discharged by rfl and simp.

Example:

-- Goal contains: lazyEvalAbstract lookup store k
-- After ssprove_eager (with fresh key and dead store):
-- Goal contains: SPComp.sample V

Equations

• CatCrypt.Tactics.tacticSsprove_eager = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_eager 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_eager" false)

def CatCrypt.Tactics.tacticSsprove_lazy_unfold : Lean.ParserDescr

ssprove_lazy_unfold unfolds the lazy evaluation abstraction and simplifies.

This is useful when you need to reason about the internal structure of lazyEvalAbstract rather than using the high-level equivalence theorems.

Equations

• CatCrypt.Tactics.tacticSsprove_lazy_unfold = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_lazy_unfold 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_lazy_unfold" false)