Library SSProve.Crypt.examples.RandomOracle

From Stdlib Require Import Utf8.
Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect all_algebra reals distr realsum
  ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq.
Set Warnings "notation-overridden,ambiguous-paths".
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)

From extructures Require Import ord fset fmap.
From SSProve.Crypt Require Import Package.

Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".
Set Primitive Projections.

Import Num.Def.
Import Num.Theory.

Import PackageNotation.

Module Type ROParams.
  Parameter Query : finType.
  Parameter Random : finType.
End ROParams.

Module RO (π : ROParams).

  Import π.

  Definition chQuery := 'fin #|Query|.
  Definition chRandom := 'fin #|Random|.
  Notation " 'query " := chQuery (in custom pack_type at level 2).
  Notation " 'random " := chRandom (in custom pack_type at level 2).

  Definition i_random := #|Random|.
  Definition INIT : nat := 0.
  Definition QUERY : nat := 1.

  Definition queries_loc := mkloc 2 (emptym : {fmap chQuery → chRandom}).
  Definition RO_locs : Locations := [fmap queries_loc].

  Definition RO_exports :=
    [interface
      #val #[ INIT ] : 'unit → 'unit ;
      #val #[ QUERY ] : 'query → 'random
    ].

  Definition RO : package [interface] RO_exports :=
    [package RO_locs ;
      #def #[ INIT ] (_ : 'unit) : 'unit
      {
        #put queries_loc := emptym ;;
        ret tt
      } ;
      #def #[ QUERY ] (q : 'query) : 'random
      {
        queries ← get queries_loc ;;
        match queries q with
        | Some r ⇒
          ret r
        | None ⇒
          r ← sample uniform i_random ;;
          #put queries_loc := setm queries q r ;;
          ret r
        end
      }
    ].

End RO.