Lazily-Sampled Random Oracle with a Heap-Resident Query Log

A random oracle whose query log lives in a single heap cell at a GLocation. The log is an association list, so it grows by one entry per fresh query; its type List (D × R) carries no Fintype instance and therefore cannot be the value type of a CatCrypt.Core.Location.

Because the log is state rather than a threaded argument, the oracle has type SPComp R — the type of any other stateful computation — so it can be composed with, and handed to, an arbitrary SPComp adversary.

Main definitions

• logFind — lookup in a query log
• logLoc — the heap cell holding the log
• query — the lazily-sampled oracle
• program — reprogram the oracle at one point

Main results

• query_apply_cached — a repeated query is deterministic and leaves the log alone
• query_apply_fresh — a fresh query samples uniformly and appends one entry
• query_answer_uniform — the answer to a fresh query is uniform on R, whatever the log holds
• query_consistent — two successive queries on the same point agree
• query_after_program — a programmed point answers with the programmed value
• preservesOutside_query — the oracle writes only its own cell
• msgLog_no_fintype — the log type of a random oracle on arbitrary-length bit strings is not finite

Query logs

@[reducible, inline]

abbrev CatCrypt.Core.RandomOracle.Log (D R : Type) : Type

Query log: an association list of query/response pairs.

Equations

• CatCrypt.Core.RandomOracle.Log D R = List (D × R)

def CatCrypt.Core.RandomOracle.logFind {D R : Type} [DecidableEq D] (x : D) : Log D R → Option R

Lookup in a query log; the leftmost entry for x wins.

Equations

• CatCrypt.Core.RandomOracle.logFind x [] = none
• CatCrypt.Core.RandomOracle.logFind x ((y, r) :: t) = if y = x then some r else CatCrypt.Core.RandomOracle.logFind x t

@[simp]

theorem CatCrypt.Core.RandomOracle.logFind_nil {D R : Type} [DecidableEq D] (x : D) : logFind x [] = none

@[simp]

theorem CatCrypt.Core.RandomOracle.logFind_cons_self {D R : Type} [DecidableEq D] (x : D) (r : R) (T : Log D R) : logFind x ((x, r) :: T) = some r

theorem CatCrypt.Core.RandomOracle.logFind_cons_of_ne {D R : Type} [DecidableEq D] {x y : D} (hne : y ≠ x) (r : R) (T : Log D R) : logFind x ((y, r) :: T) = logFind x T

The oracle

@[reducible]

def CatCrypt.Core.RandomOracle.logLoc (D R : Type) [Countable D] [Fintype R] (id : ℕ) : GLocation

Heap cell holding the random-oracle log.

Equations

• CatCrypt.Core.RandomOracle.logLoc D R id = { id := id, ty := CatCrypt.Core.RandomOracle.Log D R, countable := ⋯, inhabited := instInhabitedList }

noncomputable def CatCrypt.Core.RandomOracle.queryStep (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (T : Log D R) : SPComp R

One oracle step, given the current log: return the cached answer, or sample a fresh one and append it.

Equations

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

noncomputable def CatCrypt.Core.RandomOracle.query (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) : SPComp R

The lazily-sampled random oracle: read the log from the heap, answer, write back.

Equations

• CatCrypt.Core.RandomOracle.query D R id x = (CatCrypt.Core.SPComp.gget (CatCrypt.Core.RandomOracle.logLoc D R id)).bind (CatCrypt.Core.RandomOracle.queryStep D R id x)

theorem CatCrypt.Core.RandomOracle.queryStep_of_cached (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] {id : ℕ} {x : D} {T : Log D R} {r : R} (hc : logFind x T = some r) : queryStep D R id x T = SPComp.pure r

theorem CatCrypt.Core.RandomOracle.queryStep_of_fresh (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] {id : ℕ} {x : D} {T : Log D R} (hc : logFind x T = none) : queryStep D R id x T = (SPComp.sample R).bind fun (r : R) => (SPComp.gset (logLoc D R id) ((x, r) :: T)).bind fun (x : Unit) => SPComp.pure r

theorem CatCrypt.Core.RandomOracle.query_apply (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (h : Heap) : query D R id x h = queryStep D R id x (h.gget (logLoc D R id)) h

A cached query is deterministic

theorem CatCrypt.Core.RandomOracle.query_apply_cached (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (h : Heap) (r : R) (hc : logFind x (h.gget (logLoc D R id)) = some r) : query D R id x h = Prob.SDistr.pure (r, h)

A query already in the log is answered from the log, leaving the heap untouched.

A fresh query samples uniformly

theorem CatCrypt.Core.RandomOracle.query_apply_fresh (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (h : Heap) (hc : logFind x (h.gget (logLoc D R id)) = none) : query D R id x h = (Prob.SDistr.uniform R).bind fun (r : R) => Prob.SDistr.pure (r, h.gset (logLoc D R id) ((x, r) :: h.gget (logLoc D R id)))

A query absent from the log samples uniformly on R and appends one entry.

theorem CatCrypt.Core.RandomOracle.query_answer_uniform (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (h : Heap) (hc : logFind x (h.gget (logLoc D R id)) = none) : ((query D R id x h).bind fun (p : R × Heap) => Prob.SDistr.pure p.1) = Prob.SDistr.uniform R

The answer to a fresh query is uniform on R, independently of the log contents. This is the marginal of query on its result component.

theorem CatCrypt.Core.RandomOracle.query_empty_uniform (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) : ((query D R id x Heap.empty).bind fun (p : R × Heap) => Prob.SDistr.pure p.1) = Prob.SDistr.uniform R

Every query is fresh on the empty heap, so the freshness hypothesis of query_answer_uniform is satisfiable.

theorem CatCrypt.Core.RandomOracle.query_answer_uniform_indep (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (h₁ h₂ : Heap) (hc₁ : logFind x (h₁.gget (logLoc D R id)) = none) (hc₂ : logFind x (h₂.gget (logLoc D R id)) = none) : ((query D R id x h₁).bind fun (p : R × Heap) => Prob.SDistr.pure p.1) = (query D R id x h₂).bind fun (p : R × Heap) => Prob.SDistr.pure p.1

Two heaps on which x is fresh give the same answer distribution: the marginal does not depend on the log.

The log makes the oracle consistent

theorem CatCrypt.Core.RandomOracle.logFind_after_fresh (D R : Type) [DecidableEq D] [Countable D] [Fintype R] (id : ℕ) (x : D) (r : R) (h : Heap) : logFind x ((h.gset (logLoc D R id) ((x, r) :: h.gget (logLoc D R id))).gget (logLoc D R id)) = some r

After a fresh query, the point is cached: the freshly written log answers x.

theorem CatCrypt.Core.RandomOracle.query_consistent (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) : ((query D R id x).bind fun (r₁ : R) => (query D R id x).bind fun (r₂ : R) => SPComp.pure (r₁, r₂)) = (query D R id x).bind fun (r : R) => SPComp.pure (r, r)

Querying the same point twice returns the same value. The second query reads the entry the first one wrote, so this holds on every heap.

Programming the oracle

noncomputable def CatCrypt.Core.RandomOracle.program (D R : Type) [Countable D] [Fintype R] (id : ℕ) (x : D) (r : R) : SPComp Unit

Reprogram the oracle at x to answer r.

Equations

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

theorem CatCrypt.Core.RandomOracle.query_after_program (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (r : R) : ((program D R id x r).bind fun (x_1 : Unit) => query D R id x) = (program D R id x r).bind fun (x : Unit) => SPComp.pure r

A programmed point answers with the programmed value.

theorem CatCrypt.Core.RandomOracle.logFind_program_of_ne (D R : Type) [DecidableEq D] [Countable D] [Fintype R] (id : ℕ) {x y : D} (hne : x ≠ y) (r : R) (h : Heap) : logFind y ((h.gset (logLoc D R id) ((x, r) :: h.gget (logLoc D R id))).gget (logLoc D R id)) = logFind y (h.gget (logLoc D R id))

Programming a point the oracle has not yet been asked about does not change the answers already fixed at other points.

Footprint

theorem CatCrypt.Core.RandomOracle.preservesOutside_mono {α : Type} {c : SPComp α} {L L' : LocSet} (hc : Relational.PreservesOutside c L) (hsub : L ⊆ L') : Relational.PreservesOutside c L'

Monotonicity of PreservesOutside in the footprint.

theorem CatCrypt.Core.RandomOracle.preservesOutside_query (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) : Relational.PreservesOutside (query D R id x) {id}

The oracle writes only its own cell.

pRHL

The judgment is CatCrypt.Relational.rHoare over the same two Heaps as for any other computation, and the core frame rule applies to the oracle unchanged.

theorem CatCrypt.Core.RandomOracle.rHoare_query_after_program (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (r : R) : Relational.rHoare Relational.eqPre ((program D R id x r).bind fun (x_1 : Unit) => query D R id x) ((program D R id x r).bind fun (x : Unit) => SPComp.pure r) Relational.eqPost

The reprogramming step as a pRHL judgment: after programming x to r, the oracle and the constant r are related on equal heaps.

theorem CatCrypt.Core.RandomOracle.rHoare_query_frame (D R : Type) [DecidableEq D] [Countable D] [Fintype R] [Nonempty R] (id : ℕ) (x : D) (l : Location) (v : l.ty) (hne : l.id ≠ id) : Relational.rHoare (Relational.eqPre ⋀ Relational.leftHas l v) (query D R id x) (query D R id x) fun (a : R) (h₁ : Heap) (b : R) (h₂ : Heap) => Relational.eqPost a h₁ b h₂ ∧ Relational.leftHas l v h₁ h₂

The core frame rule applies to the oracle: an assertion about a finite-typed location at a different id survives the oracle's step.

The log type is outside the range of Location

A random oracle on arbitrary-length bit strings is the shape FDH and Fiat–Shamir need. Neither its log type nor its domain is finite, so neither can be the value type of a CatCrypt.Core.Location.

def CatCrypt.Core.RandomOracle.boundedTableLoc (D R : Type) [Fintype D] [DecidableEq D] [Fintype R] (id : ℕ) : Location

For a finite query domain the total table D → Option R is itself finite, so a bounded-domain oracle table is already a legal Location value type. The cases the Fintype bound excludes are the log-shaped state and the unbounded query domain.

Equations

• CatCrypt.Core.RandomOracle.boundedTableLoc D R id = { id := id, ty := D → Option R, fintype := Pi.instFintype, inhabited := Pi.instInhabited }

@[instance_reducible]

def CatCrypt.Core.RandomOracle.instFintypeBitVec (w : ℕ) : Fintype (BitVec w)

BitVec w is equivalent to Fin (2 ^ w). This toolchain's Mathlib ships no Fintype (BitVec w) instance.

Equations

• CatCrypt.Core.RandomOracle.instFintypeBitVec w = Fintype.ofEquiv (Fin (2 ^ w)) { toFun := BitVec.ofFin, invFun := BitVec.toFin, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

abbrev CatCrypt.Core.RandomOracle.MsgLog : Type

Log of a random oracle from arbitrary-length bit strings to 256-bit digests.

Equations

• CatCrypt.Core.RandomOracle.MsgLog = CatCrypt.Core.RandomOracle.Log (List Bool) (BitVec 256)

theorem CatCrypt.Core.RandomOracle.msgLog_no_fintype : ¬Nonempty (Fintype MsgLog)

theorem CatCrypt.Core.RandomOracle.msgDomain_no_fintype : ¬Nonempty (Fintype (List Bool))

@[reducible]

def CatCrypt.Core.RandomOracle.msgLogLoc (id : ℕ) : GLocation

The heap cell for that oracle's log.

Equations

• CatCrypt.Core.RandomOracle.msgLogLoc id = CatCrypt.Core.RandomOracle.logLoc (List Bool) (BitVec 256) id

noncomputable def CatCrypt.Core.RandomOracle.msgQuery (id : ℕ) (x : List Bool) : SPComp (BitVec 256)

The oracle on arbitrary-length bit strings.

Equations

• CatCrypt.Core.RandomOracle.msgQuery id x = CatCrypt.Core.RandomOracle.query (List Bool) (BitVec 256) id x

theorem CatCrypt.Core.RandomOracle.msgQuery_consistent (id : ℕ) (x : List Bool) : ((msgQuery id x).bind fun (r₁ : BitVec 256) => (msgQuery id x).bind fun (r₂ : BitVec 256) => SPComp.pure (r₁, r₂)) = (msgQuery id x).bind fun (r : BitVec 256) => SPComp.pure (r, r)