@[reducible, inline]

abbrev state : Type 1

The ambient state of the development: the globals of a program state.

Equations

• state = GaudisCrypt.VariableAssignment

@[reducible, inline]

abbrev Variable (a : Type u_1) : Type (max u_1 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

@[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

noncomputable def random_oracle_state : GaudisCrypt.Lens (input → Option output) GaudisCrypt.VariableAssignment

Equations

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

instance instIsGlobalVarForallInputOptionOutputRandom_oracle_stateMk : random_oracle_state.IsGlobalVar { name := "random_oracle_state", type := input → Option output, nonempty := ⋯, key := 713378399182275658285732131237853839843770282773904064106845643925946252434248071926136423511862240783368323187, keyCorrect := ⋯ }

@[implicit_reducible]

instance instDecidableEqInput : DecidableEq input

Equations

• instDecidableEqInput = sorry

noncomputable def random_oracle_init : GaudisCrypt.ProgramDenotation GaudisCrypt.VariableAssignment 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 random_oracle_state.footprint

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