Refactor semantics

_CoqProject

@@ -50,6 +50,11 @@ theories/Crypt/rhl_semantics/state_prob/StateTransfThetaDens.v
 # Prob rules
 theories/Crypt/rules/RulesProb.v
 
+# Decategorified semantics
+theories/Crypt/semantics/unary.v
+theories/Crypt/semantics/binary.v
+
+
 # Crypto
 theories/Crypt/rules/UniformDistrLemmas.v
 #theories/Crypt/rules/UniformDistr.v

theories/Crypt/package/pkg_core_definition.v

@@ -10,20 +10,18 @@
 From Coq Require Import Utf8.
 From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples.
 Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format".
-From mathcomp Require Import ssreflect eqtype choice seq ssrfun ssrbool.
+From mathcomp Require Import ssreflect eqtype choice seq ssrfun ssrbool distr reals.
 Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
 From extructures Require Import ord fset fmap.
-From Mon Require Import SPropBase.
-From Crypt Require Import Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph
+(* From Mon Require Import SPropBase. *)
+From Crypt Require Import Prelude Axioms (* ChoiceAsOrd RulesStateProb StateTransformingLaxMorph *)
      choice_type.
 
 Require Import Equations.Prop.DepElim.
 From Equations Require Import Equations.
 
 Set Equations With UIP.
 
-Import SPropNotations.
-
 Set Bullet Behavior "Strict Subproofs".
 Set Default Goal Selector "!".
 Set Primitive Projections.
@@ -72,17 +70,20 @@ Definition chtgt (v : opsig) : choice_type :=
 Definition tgt (v : opsig) : choiceType :=
   chtgt v.
 
-Section Translation.
+(* Section Translation. *)
+
+(*   Definition Prob_ops_collection := FreeProbProg.P_OP. *)
 
-  Definition Prob_ops_collection := FreeProbProg.P_OP.
+(*   Definition Prob_arities : Prob_ops_collection → choiceType := *)
+(*     FreeProbProg.P_AR. *)
 
-  Definition Prob_arities : Prob_ops_collection → choiceType :=
-    FreeProbProg.P_AR.
+(* End Translation. *)
 
-End Translation.
+(* Definition Op := Prob_ops_collection. *)
+(* Definition Arit := Prob_arities. *)
 
-Definition Op := Prob_ops_collection.
-Definition Arit := Prob_arities.
+Definition Op := ∑ (X : choice_type) , {distr (chElement X) / R}.
+Definition Arit : Op → choiceType := chElement \o (@projT1 _ _).
 
 Section FreeModule.
 
@@ -384,7 +385,7 @@ Section FreeModule.
 
   Open Scope package_scope.
 
-  Import SPropAxioms. Import FunctionalExtensionality.
+  (* Import SPropAxioms. Import FunctionalExtensionality. *)
 
   (* TODO: NEEDED? *)
   (* Program Definition rFree : ord_relativeMonad choice_incl :=

theories/Crypt/package/pkg_heap.v

@@ -20,14 +20,13 @@ From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings
 Require Import Equations.Prop.DepElim.
 From Equations Require Import Equations.
 
-(* Must come after importing Equations.Equations, who knows why. *)
-From Crypt Require Import FreeProbProg.
+(* (* Must come after importing Equations.Equations, who knows why. *) *)
+(* From Crypt Require Import FreeProbProg. *)
 
 Set Equations With UIP.
 Set Equations Transparent.
 
-Import SPropNotations.
-Import PackageNotation.
+(* Import PackageNotation. *)
 Import RSemanticNotation.
 
 Set Bullet Behavior "Strict Subproofs".
@@ -71,7 +70,7 @@ Definition heap_choiceType := [choiceType of heap].
 
 Lemma heap_ext :
   ∀ (h₀ h₁ : heap),
-    h₀ ∙1 = h₁ ∙1 →
+    val h₀ = val h₁ →
     h₀ = h₁.
 Proof.
   intros [h₀ v₀] [h₁ v₁] e. simpl in e. subst.
@@ -127,7 +126,7 @@ Proof.
 Qed.
 
 Equations? get_heap (map : heap) (ℓ : Location) : Value ℓ.π1 :=
-  get_heap map ℓ with inspect (map ∙1 ℓ) := {
+  get_heap map ℓ with inspect (val map ℓ) := {
   | @exist (Some p) e => cast_pointed_value p _
   | @exist None e => heap_init (ℓ.π1)
   }.
@@ -136,47 +135,36 @@ Proof.
   eapply get_heap_helper. all: eauto.
 Defined.
 
-Program Definition set_heap (map : heap) (l : Location) (v : Value l.π1)
-: heap :=
-  setm map l (l.π1 ; v).
-Next Obligation.
-  intros map l v.
+Equations? set_heap (map : heap) (l : Location) (v : Value l.π1) : heap :=
+  set_heap map l v := exist _ (setm (val map) l (l.π1 ; v)) _.
+Proof.
   unfold valid_heap.
   destruct map as [rh valid_rh].
   cbn - ["_ == _"].
-  apply /eqP.
-  apply eq_fset.
-  move => x.
-  rewrite domm_set.
-  rewrite in_fset_filter.
+  apply /eqP. apply eq_fset. intro x.
+  rewrite domm_set. rewrite in_fset_filter.
   destruct ((x \in l |: domm rh)) eqn:Heq.
   - rewrite andbC. cbn.
     symmetry. apply /idP.
-    unfold valid_location.
-    rewrite setmE.
+    unfold valid_location. rewrite setmE.
     destruct (x == l) eqn:H.
-    + cbn. move: H. move /eqP => H. subst. apply choice_type_refl.
-    + move: Heq. move /idP /fsetU1P => Heq.
-      destruct Heq.
-      * move: H. move /eqP => H. contradiction.
-      * destruct x, l. rewrite mem_domm in H0.
-        unfold isSome in H0.
-        destruct (rh (x; s)) eqn:Hrhx.
-        ** cbn. unfold valid_heap in valid_rh.
-            move: valid_rh. move /eqP /eq_fset => valid_rh.
-            specialize (valid_rh (x; s)).
-            rewrite in_fset_filter in valid_rh.
-            rewrite mem_domm in valid_rh.
-            assert (valid_location rh (x;s)) as Hvl.
-            { rewrite Hrhx in valid_rh. cbn in valid_rh.
-              rewrite andbC in valid_rh. cbn in valid_rh.
-              rewrite -valid_rh. auto. }
-            unfold valid_location in Hvl.
-            rewrite Hrhx in Hvl.
-            cbn in Hvl.
-            assumption.
-        ** assumption.
-  - rewrite andbC. auto.
+    + cbn. move: H => /eqP H. subst. apply choice_type_refl.
+    + move: Heq => /idP /fsetU1P Heq.
+      destruct Heq as [| H0].
+      1:{ move: H => /eqP H. contradiction. }
+      destruct x, l.
+      rewrite mem_domm in H0. unfold isSome in H0.
+      destruct (rh (x ; s)) eqn:Hrhx. 2: discriminate.
+      cbn. unfold valid_heap in valid_rh.
+      move: valid_rh => /eqP /eq_fset valid_rh.
+      specialize (valid_rh (x; s)).
+      rewrite in_fset_filter in valid_rh.
+      rewrite mem_domm in valid_rh.
+      rewrite Hrhx in valid_rh. simpl in valid_rh.
+      rewrite andbC in valid_rh. simpl in valid_rh. symmetry in valid_rh.
+      unfold valid_location in valid_rh. rewrite Hrhx in valid_rh.
+      assumption.
+  - rewrite andbC. reflexivity.
 Qed.
 
 #[program] Definition empty_heap : heap := emptym.
@@ -264,4 +252,4 @@ Proof.
   intros s ℓ v ℓ' v' ne.
   apply heap_ext. destruct s as [h vh]. simpl.
   apply setmC. auto.
-Qed.
+Qed.

theories/Crypt/semantics/binary.v

@@ -0,0 +1,208 @@
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From mathcomp Require Import all_ssreflect all_algebra boolp reals realsum distr.
+Set Warnings "notation-overridden,ambiguous-paths".
+From extructures Require Import ord fset fmap.
+From Crypt Require Import Axioms choice_type pkg_core_definition pkg_heap unary.
+
+Import Num.Theory Order.LTheory.
+
+Require Import Equations.Prop.DepElim.
+From Equations Require Import Equations.
+
+Set Equations With UIP.
+
+Set Bullet Behavior "Strict Subproofs".
+Set Default Goal Selector "!".
+Set Primitive Projections.
+
+Section Coupling.
+  Context [A1 A2 : choiceType].
+  Context (d : {distr (A1 * A2) /R}) (d1 : {distr A1 /R}) (d2 : {distr A2/R}).
+
+  Definition coupling := dfst d = d1 /\ dsnd d = d2.
+
+  Context (is_coupling : coupling).
+
+  (* Lemma dlet_coupling [X : choiceType] (f : A1 * A2 -> {distr X /R}) : *)
+  (*   \dlet_(a <- d) f a = \dlet_(a1 <- d1) \dlet_(a2 <- d2) f (a1, a2). *)
+  (* Proof. *)
+  (*   case: is_coupling=> <- <- /=; rewrite /dmargin. *)
+  (*   apply: distr_ext=> z; rewrite dlet_dlet. *)
+
+  (*   apply: distr_ext=> z; rewrite 2!dletE psum_pair; last apply: summable_mlet. *)
+  (*   apply: eq_psum=> x1; rewrite dletE -psumZ; last apply: ge0_mu. *)
+  (*   apply: eq_psum=> x2 /=. *)
+  (*   case: is_coupling=> <- <- /=. *)
+  (*   etransitivity. *)
+  (*   1: apply: eq_dlet=> a; exact (f_equal f (surjective_pairing a)). *)
+  (*   move=> /=. *)
+
+End Coupling.
+
+Module CouplingNotation.
+Notation "d ~[ d1 , d2 ]" := (coupling d d1 d2) (at level 70) : type_scope.
+End CouplingNotation.
+
+Import CouplingNotation.
+
+Section RetCoupling.
+  Context [A1 A2 : choiceType].
+  Definition ret_coupling (a1 : A1) (a2 : A2) : {distr (A1 * A2) /R} := dunit (a1, a2).
+
+  Lemma ret_coupling_prop a1 a2 : ret_coupling a1 a2 ~[dunit a1, dunit a2].
+  Proof. split; apply: distr_ext=> x /=; rewrite dmargin_dunit //. Qed.
+End RetCoupling.
+
+Section BindCoupling.
+  Context [A1 A2 B1 B2 : choiceType].
+  Context (m1 : {distr A1 /R}) (m2: {distr A2/R}) dm (hdm : dm ~[m1, m2]).
+  Context (f1 : A1 -> {distr B1 /R}) (f2: A2 -> {distr B2/R})
+          (df : A1 * A2 -> {distr (B1 * B2) /R}).
+
+  Definition bind_coupling : {distr (B1 * B2) / R} :=
+    \dlet_(a <- dm) df a.
+
+  Lemma bind_coupling_prop
+   (hdf : forall a1 a2, df (a1,a2) ~[f1 a1, f2 a2]) :
+    bind_coupling ~[\dlet_(x1 <- m1) f1 x1, \dlet_(x2 <- m2) f2 x2].
+  Proof.
+    case: hdm=> [<- <-]; split; apply: distr_ext=> z.
+    all: rewrite dmargin_dlet /bind_coupling dlet_dmargin /=; erewrite eq_dlet; first reflexivity.
+    all: move=> [a1 a2] /=; by case: (hdf a1 a2).
+  Qed.
+
+  (* Almost the same lemma but with a superficially weaker hypothesis
+     on the coupling of the continuations *)
+  Lemma bind_coupling_partial_prop
+   (hdf : forall a1 a2, dm (a1,a2) <> 0%R -> df (a1,a2) ~[f1 a1, f2 a2]) :
+    bind_coupling ~[\dlet_(x1 <- m1) f1 x1, \dlet_(x2 <- m2) f2 x2].
+  Proof.
+    case: hdm=> [<- <-]; split; apply: distr_ext=> z.
+    all: rewrite dmargin_dlet /bind_coupling dlet_dmargin /=; erewrite eq_dlet_partial; first reflexivity.
+    all: move=> [a1 a2] h /=; by case: (hdf a1 a2 h).
+  Qed.
+End BindCoupling.
+
+
+Section Def.
+  #[local] Open Scope fset.
+  #[local] Open Scope fset_scope.
+
+  (* Local shorter names for code and semantics *)
+  Let C := raw_code.
+  Let M := (Def.stsubdistr heap_choiceType).
+
+  Definition stsubdistr_rel [A1 A2 : choiceType] : M A1 -> M A2 -> Type :=
+    fun d1 d2 => forall map1 map2, { d |  d ~[ d1 map1 , d2 map2 ] }.
+
+  Context `{EvalOp}.
+
+  Definition prerelation := rel heap.
+  Definition postrelation A1 A2 := (A1 * heap) -> pred (A2 * heap).
+
+  Definition relspec_valid [A1 A2 : choiceType]
+             (pre : prerelation)
+             (m1 : M A1) (m2 : M A2)
+             (post : postrelation A1 A2) :=
+    forall map1 map2, pre map1 map2 ->
+                 exists d, d ~[m1 map1, m2 map2] /\
+                      forall p1 p2, d (p1,p2) <> 0%R -> post p1 p2.
+
+  Definition binary_judgement [A1 A2 : choiceType]
+             (pre : prerelation)
+             (c1 : C A1) (c2 : C A2)
+             (post : postrelation A1 A2) :=
+    relspec_valid pre (eval c1) (eval c2) post.
+
+
+  (* Bindings in the pre/postcondition looks annoying here *)
+  Notation "⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄" :=
+    (binary_judgement pre c1 c2 post) : Rules_scope.
+  Open Scope Rules_scope.
+
+  (** Ret rule *)
+
+  Lemma ret_rel_rule [A1 A2 : choiceType] (a1 : A1) (a2 : A2) :
+    ⊨ ⦃ fun _ _ => true ⦄ ret a1 ≈ ret a2 ⦃ fun p1 p2 => (p1.1 == a1) && (p2.1 == a2) ⦄.
+  Proof.
+    move=> map1 map2 _; exists (dunit ((a1, map1), (a2, map2))); split.
+    1: split; apply: distr_ext=> x /=; rewrite dmargin_dunit //.
+    move=> p1 p2 /dinsuppP/in_dunit[= -> ->] /=; by rewrite 2!eq_refl.
+  Qed.
+
+  (** Weaken rule *)
+
+  Lemma weaken_rule [A1 A2 : choiceType]
+        (wkpre : prerelation) (wkpost : postrelation A1 A2)
+        (pre : prerelation) (c1 : C A1) (c2 : C A2) (post : postrelation A1 A2) :
+    subrel wkpre pre ->
+    (forall p1, subpred (post p1) (wkpost p1)) ->
+    ⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄ ->
+    ⊨ ⦃ wkpre ⦄ c1 ≈ c2 ⦃ wkpost ⦄.
+  Proof.
+    move=> hsubpre hsubpost hrel map1 map2 /hsubpre/(hrel map1 map2)[d [? hpost]].
+    exists d; split=> // ???; apply: hsubpost; by apply: hpost.
+  Qed.
+
+  (** Bind rule *)
+
+  Notation bind_prerel prem postm pref :=
+    [rel map1 map2 | prem map1 map2 && `[< forall p1 p2, postm p1 p2 ==> pref p1.1 p2.1 p1.2 p2.2 >]].
+  Notation bind_postrel postm postf :=
+    (fun pf1 pf2 => `[< exists p1 p2, postm p1 p2 ==> postf p1.1 p2.1 pf1 pf2 >]).
+
+
+  Lemma bind_rule [A1 A2 B1 B2 : choiceType]
+        (prem : prerelation) (m1 : C A1) (m2 : C A2) (postm : postrelation A1 A2)
+        (pref: A1 -> A2 -> prerelation) (f1 : A1 -> C B1) (f2 : A2 -> C B2)
+        (postf : A1 -> A2 -> postrelation B1 B2) :
+    ⊨ ⦃ prem ⦄ m1 ≈ m2 ⦃ postm ⦄ ->
+    (forall a1 a2, ⊨ ⦃ pref a1 a2 ⦄ f1 a1 ≈ f2 a2 ⦃ postf a1 a2 ⦄) ->
+    ⊨ ⦃ bind_prerel prem postm pref ⦄ bind m1 f1 ≈ bind m2 f2 ⦃ bind_postrel postm postf ⦄.
+  Proof.
+    move=> hm hf map1 map2 /andP[/= /(hm _)[dm [dmcoupling hpostm]]
+                                   /asboolP hpostmpref].
+    (* 2 difficulties:
+       - we only have merely a coupling between the distributions for the
+         continuations when we need to provide the coupling witness
+         so we use choice at this pointed
+         (functional choice should be enough;
+          a more radical move would be to have proof relevant relational proofs)
+       - we need to incorporate the precondition of the continuation when
+         building the coupling witness; this forces an annoying yoga of
+         currying/uncurrying
+     *)
+    set X := (A1 * heap) * (A2 * heap).
+    (* set P : pred X := fun '((a1, map1), (a2, map2)) => pref a1 a2 map1 map2. *)
+    set P := fun x : X => pref x.1.1 x.2.1 x.1.2 x.2.2.
+    have/schoice[df hdf]: forall (z : { x : X | P x }), _
+      (* Arghh...*)
+      := fun z => hf (val z).1.1 (val z).2.1 (val z).1.2 (val z).2.2 (valP z).
+      (* := fun z => let '((a1, map1), (a2, map2)) := val z in *)
+      (*     hf a1 a2 map1 map2 (valP z). *)
+
+    set df' := fun x => bool_depelim _ (P x) (fun hx => df (exist _ x hx))
+                                    (fun _ => dnull).
+    exists (bind_coupling dm df'); split.
+    + rewrite 2!eval_bind /Def.bind.
+      apply: bind_coupling_partial_prop=> //.
+      move=> p1' p2' /(hpostm _ _).
+      move: (hpostmpref p1' p2')=> /implyP/[apply] hpref.
+      case: (hdf (exist _ (p1', p2') hpref))=> ? _.
+      by rewrite /df' bool_depelim_true.
+    + move=> p1 p2 /dinsuppP/dinsupp_dlet[[p1' p2'] /dinsuppP hinm hinf].
+      apply/asboolP; exists p1', p2'; apply/implyP.
+      move: (hpostmpref p1' p2')=> /implyP/[apply] hpref.
+      case: (hdf (exist _ (p1', p2') hpref))=> _ h; apply: h.
+      move: hinf; by rewrite /df' bool_depelim_true=> /(_ =P _).
+  Qed.
+
+End Def.
+
+Module BinaryNotations.
+  Notation "⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄" :=
+    (binary_judgement pre c1 c2 post) : Rules_scope.
+  Open Scope Rules_scope.
+End BinaryNotations.
+
+