Library SSProve.Crypt.examples.interpreter_test

From Stdlib Require Import Utf8.
Set Warnings "-notation-overridden,-ambiguous-paths".
From mathcomp Require Import all_ssreflect.
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 pkg_interpreter.

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

Section Test.
  Import PackageNotation.
  #[local] Open Scope package_scope.

  #[local] Definition loc := mkloc 1 (0 : nat).
  #[local] Definition locs : Locations := [fmap loc].

  #[local] Definition test_prog_sub (x : nat):
    code emptym [interface] 'nat :=
    {code
       k ← sample uniform 20 ;;
       let y := (x + k)%N in
       ret y
    }.

  #[local] #[program] Definition test_prog (x : nat):
    code locs [interface] 'nat :=
    {code
       k ← test_prog_sub x ;;
       #put loc := k ;;
       k' ← get loc ;;
       ret k'
    }.
  Next Obligation.
    intros. ssprove_valid.
  Defined.

  Goal (nat_ch (ch_nat 'unit tt) 'unit) = Some tt.
    vm_compute.
    reflexivity.
  Qed.
  Goal (Run sampler (test_prog 2) 54) = Some 16.
    simpl. vm_compute.
    reflexivity.
  Qed.

  Lemma interpretation_test1:
    ∀ seed input,
      (Run sampler (test_prog input) seed) = Some (input + seed %% 20)%N.
  Proof.
    done.
  Qed.

  #[local] Definition E :=
    [interface
       #val #[ 0 ] : 'nat → 'nat
    ].

  #[local] Definition test_pack:
    package [interface] E :=
    [package locs ;
       #def #[ 0 ] (x : 'nat) : 'nat
       {
         k ← sample uniform 20 ;;
         let y := (x + k)%N in
         #put loc := y ;;
         y' ← get loc ;;
         ret y'
       }
    ].

End Test.