structure state : Type

The ambient state of the development. (Moved here from the former scratch Unsorted.lean so that the crypto layer doesn't depend on that file.)

• x : ℕ
• y : ℕ
• z : String

@[reducible, inline]

abbrev Variable (a : Type u_1) : Type u_1

A Variable is a lens into the ambient state.

Equations

• Variable a = GaudisCrypt.Lens a state

Random oracle primitives

The basic actors of the random oracle framework: the RO state lens, the two query primitives (lazy_query and random_oracle_query), and their respective initialisation routines (lazy_init and random_oracle_init).

convert and everything related to converting one to the other lives in PlonkLean.RO.Transfer. The scratch state variables used by the adversary-driven oracle loops live in PlonkLean.RO.OracleLoop.

opaque input : Type

opaque output : Type

instance instCountableState : Countable state

@[implicit_reducible]

instance instInhabitedInput : Inhabited input

Equations

• instInhabitedInput = sorry

@[implicit_reducible]

instance instFintypeInput : Fintype input

Equations

• instFintypeInput = sorry

@[implicit_reducible]

instance instInhabitedOutput : Inhabited output

Equations

• instInhabitedOutput = sorry

@[implicit_reducible]

instance instFintypeOutput : Fintype output

Equations

• instFintypeOutput = sorry

@[implicit_reducible]

noncomputable instance instDecidableEqOutput : DecidableEq output

Equations

• instDecidableEqOutput = Classical.decEq output

axiom random_oracle_state : Variable (input → Option output)

@[implicit_reducible]

instance instDecidableEqInput : DecidableEq input

Equations

• instDecidableEqInput = sorry

noncomputable def random_oracle_init : GaudisCrypt.ProgramDenotation state Unit

Sample the entire input → output function space uniformly and store it in the random oracle (as the eager initialisation).

Equations

• random_oracle_init = do let __discr ← GaudisCrypt.ProgramDenotation.uniform match __discr with | h => GaudisCrypt.ProgramDenotation.set random_oracle_state fun (x : input) => some (h x)

noncomputable def lazy_init : GaudisCrypt.ProgramDenotation state Unit

Initialise the random oracle with no cached entries (lazy initialisation).

Equations

• lazy_init = GaudisCrypt.ProgramDenotation.set random_oracle_state fun (x : input) => none

noncomputable def lazy_query (inp : input) : GaudisCrypt.ProgramDenotation state output

Lazy random-oracle query: return the cached output if present, otherwise sample uniformly and cache.

Equations

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

noncomputable def random_oracle_query (inp : input) : GaudisCrypt.ProgramDenotation state output

Eager random-oracle query: read the (pre-sampled) value at inp.

Equations

• random_oracle_query inp = do let h ← GaudisCrypt.ProgramDenotation.get random_oracle_state pure ((h inp).getD default)

theorem lazy_query_inFootprint_ro (inp : input) : (lazy_query inp).inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)

lazy_query only reads and writes random_oracle_state (probabilistic footprint form, countability-free).