From 5f637d240933b58c45eef7284da13cb7ddfe7d9b Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Mon, 17 Jan 2022 22:00:42 +0100
Subject: [PATCH 1/7] Direct style definition of state+prob spec monad

---
 _CoqProject                      |   4 +
 theories/Crypt/semantics/unary.v | 147 +++++++++++++++++++++++++++++++
 2 files changed, 151 insertions(+)
 create mode 100644 theories/Crypt/semantics/unary.v

diff --git a/_CoqProject b/_CoqProject
index de0eb968..5ec254cf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -50,6 +50,10 @@ theories/Crypt/rhl_semantics/state_prob/StateTransfThetaDens.v
 # Prob rules
 theories/Crypt/rules/RulesProb.v
 
+# Decategorified semantics
+theories/Crypt/semantics/unary.v
+
+
 # Crypto
 theories/Crypt/rules/UniformDistrLemmas.v
 #theories/Crypt/rules/UniformDistr.v
diff --git a/theories/Crypt/semantics/unary.v b/theories/Crypt/semantics/unary.v
new file mode 100644
index 00000000..bf58b846
--- /dev/null
+++ b/theories/Crypt/semantics/unary.v
@@ -0,0 +1,147 @@
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From mathcomp Require Import all_ssreflect all_algebra distr reals realsum boolp.
+Set Warnings "notation-overridden,ambiguous-paths".
+From Crypt Require Import Axioms.
+
+Import Num.Theory Order.LTheory.
+
+Lemma distr_ext : forall (A : choiceType) (mu nu : {distr A/R}),
+    distr.mu mu =1 distr.mu nu -> mu = nu.
+Proof.
+  move=> A [mu +++] [nu +++] /= /boolp.funext mu_eq_nu.
+  rewrite {}mu_eq_nu; move=> *; f_equal.
+  all: apply proof_irrelevance.
+Qed.
+
+Lemma eq_dlet [A B : choiceType] (m : {distr A/R})
+      (f g : A -> {distr B /R}) :
+  f =1 g -> \dlet_(x <- m) f x = \dlet_(x <- m) g x.
+Proof.
+  move=> fg; apply: distr_ext=> i; rewrite 2!dletE.
+  apply: eq_psum=> a; f_equal; by rewrite fg.
+Qed.
+
+Section Def.
+  Context (S : choiceType).
+
+  Definition stsubdistr (A : choiceType) := S -> {distr (A * S) /R}.
+
+  Definition ret [A : choiceType] (a : A) : stsubdistr A :=
+    fun s => dunit (a,s).
+
+  Definition bind [A B : choiceType] (m : stsubdistr A) (f : A -> stsubdistr B) :=
+    fun s0 => \dlet_(p <- m s0) f p.1 p.2.
+
+  Lemma bind_ret [A B : choiceType] (a : A) (f : A -> stsubdistr B)
+    : bind (ret a) f = f a.
+  Proof.
+    extensionality s; apply: distr_ext ; apply: dlet_unit.
+  Qed.
+
+  Lemma ret_bind [A : choiceType] (m : stsubdistr A) : bind m (@ret _) = m.
+  Proof.
+    extensionality s ; apply: distr_ext=> a; rewrite /bind /ret.
+    under eq_dlet do rewrite -surjective_pairing.
+    apply: dlet_dunit_id.
+  Qed.
+
+  Lemma bind_bind [A B C : choiceType]
+        (m : stsubdistr A)
+        (f : A -> stsubdistr B)
+        (g : B -> stsubdistr C) :
+    bind m (fun a => bind (f a) g) = bind (bind m f) g.
+  Proof.
+    extensionality s; apply distr_ext=> a; rewrite /bind.
+    by rewrite dlet_dlet.
+  Qed.
+
+  (* Section Equality. *)
+  (*   Context [A : choiceType]. *)
+
+  (*   (* Definition stsubdistr_eq : rel (stsubdistr A) := *) *)
+  (*   (*   fun f g =>`[< f =2 g >]. *) *)
+
+  (*   (* Lemma stsubdistr_eq_axiom : Equality.axiom stsubdistr_eq. *) *)
+  (*   (* Proof. *) *)
+  (*   (*   move=> f g; apply (iffP idP). *) *)
+  (*   (*   - move=> /asboolP fg; extensionality s; apply: distr_ext=> a; apply: fg. *) *)
+  (*   (*   - move=> ->; apply/asboolP=> ??; reflexivity. *) *)
+  (*   (* Qed. *) *)
+
+  (*   (* Definition stsubdistr_eq_mixin := *) *)
+  (*   (*   @Equality.Mixin _ stsubdistr_eq stsubdistr_eq_axiom. *) *)
+  (*   Definition stsubdistr_eqType := EqType (stsubdistr A) *)
+  (*                                          (equality_mixin_of_Type (stsubdistr A)). *)
+  (*                                          (* stsubdistr_eq_mixin. *) *)
+  (*   Canonical stsubdistr_eqType. *)
+  (* End Equality. *)
+
+  Section Order.
+    Context [A : choiceType].
+
+    Canonical stsubdistr_eqType :=
+      EqType (stsubdistr A) (equality_mixin_of_Type (stsubdistr A)).
+    Canonical stsubdistr_choiceType := choice_of_Type (stsubdistr A).
+
+    Definition stsubdistr_le : rel (stsubdistr A) :=
+      fun d0 d1 =>
+        `[< forall s0 a s1, (mu (d0 s0) (a, s1) <= mu (d1 s0) (a, s1))%O>].
+
+    (* I don't think I really care about lt so let's put the tautological def *)
+    Definition stsubdistr_lt : rel (stsubdistr A) :=
+      fun d0 d1 => (d1 != d0) && stsubdistr_le d0 d1.
+
+    (* Lemma bool_equiv_eq (b1 b2 : bool) : b1 <-> b2 -> b1 = b2. *)
+    (* Proof. case: b1; case: b2=> //= -[h0 h1]; first symmetry; intuition. Qed. *)
+
+    (* Lemma stsubdistr_le_lt : forall x y, stsubdistr_lt x y = (x != y) && stsubdistr_le x y. *)
+    (* Proof. *)
+    (*   move=> f g; apply: bool_equiv_eq; split. *)
+    (*   - move=> /andP [? /asboolP [s0 [a [s1 h]]]]; apply/andP; split=> //. *)
+    (*     move: h; apply contraPneq. *)
+    (*     move=> ->; rewrite lt_def eq_refl //. *)
+    (*   - move=>/andP. *)
+
+    Lemma stsubdistr_le_refl : reflexive stsubdistr_le.
+    Proof. move=> g; apply/asboolP=> *; apply: le_refl. Qed.
+
+    Lemma stsubdistr_le_anti : antisymmetric stsubdistr_le.
+    Proof.
+      move=> f g /andP [] /asboolP fg /asboolP gf.
+      extensionality s; apply: distr_ext=> -[a s'].
+      apply: le_anti; rewrite fg gf //.
+    Qed.
+
+    Lemma stsubdistr_le_trans : transitive stsubdistr_le.
+    Proof.
+      move=> g f h /asboolP gf /asboolP fh; apply/asboolP=> *.
+      apply: le_trans; auto.
+    Qed.
+
+    Definition stsubdistr_porderMixin :=
+      @Order.POrder.Mixin _ _ stsubdistr_le stsubdistr_lt
+                          ltac:(reflexivity) stsubdistr_le_refl
+                          stsubdistr_le_anti stsubdistr_le_trans.
+
+    Canonical stsubdistr_porderType := POrderType ring_display (stsubdistr A) stsubdistr_porderMixin.
+
+    (* Lemma stsubdistr_distinct (d0 d1 : stsubdistr A) : d0 < d1 ->  exists s0 a s1, (mu (d0 s0) (a, s1) < mu (d1 s0) (a, s1))%O. *)
+
+  End Order.
+
+  Open Scope order_scope.
+
+  Lemma bind_monotone [A B : choiceType]
+        (m0 m1 : stsubdistr A) (f0 f1 : A -> stsubdistr B) :
+    m0 <= m1 -> (forall a, f0 a <= f1 a) -> bind m0 f0 <= bind m1 f1 :> stsubdistr B.
+  Proof.
+    move=> /asboolP m01 f01; apply/asboolP=> s0 b s1.
+    (* move: {f01}(f01 a) => /asboolP f01. *)
+    rewrite /bind 2!dletE.
+    apply: le_psum; last apply: summable_mlet.
+    move=> [a ?]; apply/andP;split.
+    - apply: mulr_ge0; apply: ge0_mu.
+    - apply: ler_pmul; try apply: ge0_mu; first apply: m01.
+      move: {f01}(f01 a)=> /asboolP //.
+  Qed.
+End Def.

From 4f3764c3e3dfd1b1df9f5f14e99ed936ce97a333 Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Mon, 17 Jan 2022 22:09:35 +0100
Subject: [PATCH 2/7] quick cleanup/comments

---
 theories/Crypt/semantics/unary.v | 51 ++++++++------------------------
 1 file changed, 13 insertions(+), 38 deletions(-)

diff --git a/theories/Crypt/semantics/unary.v b/theories/Crypt/semantics/unary.v
index bf58b846..c5cea409 100644
--- a/theories/Crypt/semantics/unary.v
+++ b/theories/Crypt/semantics/unary.v
@@ -5,10 +5,11 @@ From Crypt Require Import Axioms.
 
 Import Num.Theory Order.LTheory.
 
+(** Extensionality lemmas *)
 Lemma distr_ext : forall (A : choiceType) (mu nu : {distr A/R}),
     distr.mu mu =1 distr.mu nu -> mu = nu.
 Proof.
-  move=> A [mu +++] [nu +++] /= /boolp.funext mu_eq_nu.
+  move=> A [mu +++] [nu +++] /= /funext mu_eq_nu.
   rewrite {}mu_eq_nu; move=> *; f_equal.
   all: apply proof_irrelevance.
 Qed.
@@ -21,9 +22,13 @@ Proof.
   apply: eq_psum=> a; f_equal; by rewrite fg.
 Qed.
 
+(** Definition of the model for the unary semantics *)
+
 Section Def.
   Context (S : choiceType).
 
+  (* carrier for unary specifications /
+     model for single probabilistic programs with state space S *)
   Definition stsubdistr (A : choiceType) := S -> {distr (A * S) /R}.
 
   Definition ret [A : choiceType] (a : A) : stsubdistr A :=
@@ -32,11 +37,10 @@ Section Def.
   Definition bind [A B : choiceType] (m : stsubdistr A) (f : A -> stsubdistr B) :=
     fun s0 => \dlet_(p <- m s0) f p.1 p.2.
 
+  (* Monadic laws -- wrapper around existing lemmas *)
   Lemma bind_ret [A B : choiceType] (a : A) (f : A -> stsubdistr B)
     : bind (ret a) f = f a.
-  Proof.
-    extensionality s; apply: distr_ext ; apply: dlet_unit.
-  Qed.
+  Proof. extensionality s; apply: distr_ext ; apply: dlet_unit. Qed.
 
   Lemma ret_bind [A : choiceType] (m : stsubdistr A) : bind m (@ret _) = m.
   Proof.
@@ -55,53 +59,24 @@ Section Def.
     by rewrite dlet_dlet.
   Qed.
 
-  (* Section Equality. *)
-  (*   Context [A : choiceType]. *)
-
-  (*   (* Definition stsubdistr_eq : rel (stsubdistr A) := *) *)
-  (*   (*   fun f g =>`[< f =2 g >]. *) *)
-
-  (*   (* Lemma stsubdistr_eq_axiom : Equality.axiom stsubdistr_eq. *) *)
-  (*   (* Proof. *) *)
-  (*   (*   move=> f g; apply (iffP idP). *) *)
-  (*   (*   - move=> /asboolP fg; extensionality s; apply: distr_ext=> a; apply: fg. *) *)
-  (*   (*   - move=> ->; apply/asboolP=> ??; reflexivity. *) *)
-  (*   (* Qed. *) *)
-
-  (*   (* Definition stsubdistr_eq_mixin := *) *)
-  (*   (*   @Equality.Mixin _ stsubdistr_eq stsubdistr_eq_axiom. *) *)
-  (*   Definition stsubdistr_eqType := EqType (stsubdistr A) *)
-  (*                                          (equality_mixin_of_Type (stsubdistr A)). *)
-  (*                                          (* stsubdistr_eq_mixin. *) *)
-  (*   Canonical stsubdistr_eqType. *)
-  (* End Equality. *)
 
   Section Order.
     Context [A : choiceType].
 
+    (* The eqType and choiceType instances are given
+       by excluded-middle and the axiom of choice *)
     Canonical stsubdistr_eqType :=
       EqType (stsubdistr A) (equality_mixin_of_Type (stsubdistr A)).
     Canonical stsubdistr_choiceType := choice_of_Type (stsubdistr A).
 
+    (** Order between specifications *)
     Definition stsubdistr_le : rel (stsubdistr A) :=
-      fun d0 d1 =>
-        `[< forall s0 a s1, (mu (d0 s0) (a, s1) <= mu (d1 s0) (a, s1))%O>].
+      fun d0 d1 => `[< forall s0 a s1, (mu (d0 s0) (a, s1) <= mu (d1 s0) (a, s1))%O>].
 
     (* I don't think I really care about lt so let's put the tautological def *)
     Definition stsubdistr_lt : rel (stsubdistr A) :=
       fun d0 d1 => (d1 != d0) && stsubdistr_le d0 d1.
 
-    (* Lemma bool_equiv_eq (b1 b2 : bool) : b1 <-> b2 -> b1 = b2. *)
-    (* Proof. case: b1; case: b2=> //= -[h0 h1]; first symmetry; intuition. Qed. *)
-
-    (* Lemma stsubdistr_le_lt : forall x y, stsubdistr_lt x y = (x != y) && stsubdistr_le x y. *)
-    (* Proof. *)
-    (*   move=> f g; apply: bool_equiv_eq; split. *)
-    (*   - move=> /andP [? /asboolP [s0 [a [s1 h]]]]; apply/andP; split=> //. *)
-    (*     move: h; apply contraPneq. *)
-    (*     move=> ->; rewrite lt_def eq_refl //. *)
-    (*   - move=>/andP. *)
-
     Lemma stsubdistr_le_refl : reflexive stsubdistr_le.
     Proof. move=> g; apply/asboolP=> *; apply: le_refl. Qed.
 
@@ -131,12 +106,12 @@ Section Def.
 
   Open Scope order_scope.
 
+  (** Bind is monotone with respect to the order we endowed the specs with *)
   Lemma bind_monotone [A B : choiceType]
         (m0 m1 : stsubdistr A) (f0 f1 : A -> stsubdistr B) :
     m0 <= m1 -> (forall a, f0 a <= f1 a) -> bind m0 f0 <= bind m1 f1 :> stsubdistr B.
   Proof.
     move=> /asboolP m01 f01; apply/asboolP=> s0 b s1.
-    (* move: {f01}(f01 a) => /asboolP f01. *)
     rewrite /bind 2!dletE.
     apply: le_psum; last apply: summable_mlet.
     move=> [a ?]; apply/andP;split.

From 00ba8e209bd8c711e06b3cdd9b52eefa8a56f672 Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Wed, 19 Jan 2022 17:01:34 +0100
Subject: [PATCH 3/7] unary judgement basic rules

---
 theories/Crypt/package/pkg_core_definition.v |  27 +--
 theories/Crypt/package/pkg_heap.v            |  14 +-
 theories/Crypt/semantics/unary.v             | 201 ++++++++++++++++++-
 3 files changed, 219 insertions(+), 23 deletions(-)

diff --git a/theories/Crypt/package/pkg_core_definition.v b/theories/Crypt/package/pkg_core_definition.v
index c6070358..5013c41f 100644
--- a/theories/Crypt/package/pkg_core_definition.v
+++ b/theories/Crypt/package/pkg_core_definition.v
@@ -10,11 +10,11 @@
 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.
@@ -22,8 +22,6 @@ 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 : chUniverse) , {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 :=
diff --git a/theories/Crypt/package/pkg_heap.v b/theories/Crypt/package/pkg_heap.v
index ed71ab8e..85a99379 100644
--- a/theories/Crypt/package/pkg_heap.v
+++ b/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)
   }.
@@ -140,7 +139,6 @@ 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.
   unfold valid_heap.
   destruct map as [rh valid_rh].
   cbn - ["_ == _"].
@@ -264,4 +262,4 @@ Proof.
   intros s ℓ v ℓ' v' ne.
   apply heap_ext. destruct s as [h vh]. simpl.
   apply setmC. auto.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Crypt/semantics/unary.v b/theories/Crypt/semantics/unary.v
index c5cea409..273ba431 100644
--- a/theories/Crypt/semantics/unary.v
+++ b/theories/Crypt/semantics/unary.v
@@ -1,10 +1,20 @@
 Set Warnings "-notation-overridden,-ambiguous-paths".
 From mathcomp Require Import all_ssreflect all_algebra distr reals realsum boolp.
 Set Warnings "notation-overridden,ambiguous-paths".
-From Crypt Require Import Axioms.
+From extructures Require Import ord fset fmap.
+From Crypt Require Import Axioms chUniverse pkg_core_definition pkg_heap.
 
 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.
+
 (** Extensionality lemmas *)
 Lemma distr_ext : forall (A : choiceType) (mu nu : {distr A/R}),
     distr.mu mu =1 distr.mu nu -> mu = nu.
@@ -24,6 +34,7 @@ Qed.
 
 (** Definition of the model for the unary semantics *)
 
+Module Def.
 Section Def.
   Context (S : choiceType).
 
@@ -104,7 +115,7 @@ Section Def.
 
   End Order.
 
-  Open Scope order_scope.
+  #[local] Open Scope order_scope.
 
   (** Bind is monotone with respect to the order we endowed the specs with *)
   Lemma bind_monotone [A B : choiceType]
@@ -120,3 +131,189 @@ Section Def.
       move: {f01}(f01 a)=> /asboolP //.
   Qed.
 End Def.
+
+Arguments ret [_ _] _.
+Arguments bind [_ _ _] _ _.
+End Def.
+
+
+(** Semantic evaluation of code and commands *)
+Section Evaluation.
+  #[local] Open Scope fset.
+  #[local] Open Scope fset_scope.
+  Context (Loc : {fset Location}).
+  Context (import : Interface).
+
+  (* Local shorter names for code and semantics *)
+  Let C := code Loc import.
+  Let M := (Def.stsubdistr heap_choiceType).
+
+  (** Taking an interpretation of the imported operation as assumption *)
+  Context (import_eval : forall o, o \in import -> src o -> M (tgt o)).
+
+  (* Multiple attempts for evaluation. In the end it looks simpler
+     defining evaluation on raw_code, and providing the adequate
+     rules/hoare triples only on valid code.
+   *)
+  (* two helper functions for the convoy pattern (is there an idiomatic ssreflect/mathcomp way to do that ?) *)
+  Definition bool_depelim (X : Type) (b : bool) (htrue : b = true -> X) (hfalse : b = false -> X) : X :=
+    (if b as b0 return b = b0 -> X then htrue else hfalse) erefl.
+
+  Lemma bool_depelim_true (X : Type) (b : bool) (htrue : b = true -> X) (hfalse : b = false -> X) (e : b = true) : bool_depelim X b htrue hfalse = htrue e.
+  Proof. by depelim e. Qed.
+
+  Definition eval [A : choiceType] : raw_code A -> M A.
+  Proof.
+    elim.
+    - apply: Def.ret.
+    - move=> o x k ih.
+      apply: (bool_depelim _ (o \in import) _ (fun _ _=> dnull))=> oval.
+      exact (Def.bind (import_eval o oval x) ih).
+    - move=> l k ih.
+      exact (fun map => let v := get_heap map l in ih v map).
+    - move=> l v k ih.
+      exact (fun map => ih (set_heap map l v)).
+    - move=> [X sampleX] k ih.
+      exact (fun map => \dlet_(x <- sampleX) ih x map).
+  Defined.
+
+
+
+  (* Definition eval [A : choiceType] : C A -> M A. *)
+  (* Proof. *)
+  (*   move=> []; elim. *)
+  (*   - move=> a _ ; exact (ret _ a). *)
+  (*   - move=> o x k ih /inversion_valid_opr [oval kval]. *)
+  (*     exact (bind _ (import_eval o oval x) (fun v => ih v (kval v))). *)
+  (*   - move=> l k ih /inversion_valid_getr [lval kval]. *)
+  (*     exact (bind _ (fun map => dunit (get_heap map l, map)) *)
+  (*                 (fun v => ih v (kval v))). *)
+  (*   - move=> l v k ih /inversion_valid_putr[lval kval]. *)
+  (*     exact (bind _ (fun map => dunit (tt, set_heap map l v)) (fun=> ih kval)). *)
+  (*   - move=> [X sampleX] ++/inversion_valid_sampler. *)
+  (*     rewrite /Arit=> /=k ih kval. *)
+  (*     exact (bind _ (fun s => \dlet_(x <- sampleX) dunit (x, s)) (fun x => ih x (kval x))). *)
+  (* Defined. *)
+
+  (* Definition eval [A : choiceType] : C A -> M A. *)
+  (* Proof. *)
+  (*   move=> []; elim. *)
+  (*   - move=> a _ ; exact (Def.ret a). *)
+  (*   - move=> o x k ih /inversion_valid_opr [oval kval]. *)
+  (*     exact (Def.bind (import_eval o oval x) (fun v => ih v (kval v))). *)
+  (*   - move=> l k ih /inversion_valid_getr [lval kval]. *)
+  (*     exact (fun map => let v := get_heap map l in ih v (kval v) map). *)
+  (*   - move=> l v k ih /inversion_valid_putr[lval kval]. *)
+  (*     exact (fun map => ih kval (set_heap map l v)). *)
+  (*   - move=> [X sampleX] ++/inversion_valid_sampler. *)
+  (*     rewrite /Arit=> /=k ih kval. *)
+  (*     exact (fun map => \dlet_(x <- sampleX) ih x (kval x) map). *)
+  (* Defined. *)
+
+  (** Hoare triples *)
+
+  Definition precondition := pred heap.
+  Definition postcondition A := pred (A * heap).
+
+  Definition unary_judgement [A : choiceType] (pre : precondition) (c : C A) (post : postcondition A) : Prop :=
+    forall map, pre map -> forall p, (eval c map p <> 0)%R -> post p.
+
+  Declare Scope Rules_scope.
+
+  (* @théo Is there a binding key for the package_scope ?*)
+  Open Scope package_scope.
+
+  (* Is there a way to have a version with and without binder for the result in
+  parallel ? *)
+  (* Notation "⊨ ⦃ pre ⦄ c ⦃ post ⦄" := *)
+  (*   (unary_judgement pre {code c} (post)) *)
+  (*     : Rules_scope. *)
+
+  Notation "⊨ ⦃ pre ⦄ c ⦃ p , post ⦄" :=
+    (unary_judgement pre {code c} (fun p => post))
+      (p pattern) : Rules_scope.
+  Open Scope Rules_scope.
+
+
+  (** Ret rule *)
+
+  Lemma ret_rule [A : choiceType] (a : A) :
+    ⊨ ⦃ predT ⦄ ret a ⦃ (r,_), a == r ⦄.
+  Proof. move=> ? _ p /dinsuppP /in_dunit -> //. Qed.
+
+  (** Bind rule *)
+
+  (* Note: this rule is much simpler to express in CPS (no existential,
+     only composition of function) but is it worth the cost of encoding
+     specifications presented by pre/post condition.
+     Anyway the two versions could be developped in parallel *)
+
+  Notation bind_pre prem postm pref :=
+    (predI prem [pred map | `[<forall p, postm p ==> pref p.1 p.2>]]).
+  Notation bind_post postm postf :=
+    [pred pf | `[< exists p, postm p ==> postf p.1 pf >]].
+
+  (* the "difficult" part of the effect observation: commutation with bind *)
+  Lemma eval_bind [A B : choiceType] (m : C A) (f : A -> C B) :
+    eval {code bind m f} = Def.bind (eval m) (eval (A:=B) \o f).
+  Proof.
+    case: m=> []; elim=> //=.
+    - move=> ??; rewrite Def.bind_ret /comp; f_equal.
+    - move=> o?? ih /inversion_valid_opr [oval kval].
+      rewrite 2!bool_depelim_true -Def.bind_bind; f_equal.
+      extensionality x; apply: ih; apply: kval.
+    - move=> l k ih /inversion_valid_getr [lval kval].
+      extensionality map; rewrite (ih _ (kval _)) //.
+    - move=> l c k ih /inversion_valid_putr [lval kval].
+      extensionality map; rewrite (ih kval) //.
+    - move=> [X sampleX] k ih /inversion_valid_sampler kval.
+      extensionality map. rewrite /Def.bind.
+      apply: distr_ext=> z; rewrite dlet_dlet. do 2 f_equal.
+      extensionality x; rewrite (ih x _) //.
+  Qed.
+
+  (* Two helper lemmas *)
+  Lemma R_no0div : forall u v : R, (u * v <> 0 -> u <> 0 /\ v <> 0)%R.
+  Proof.
+    move=> u v uv; split; move: uv; apply contra_not=> ->; [apply: GRing.mul0r|apply: GRing.mulr0].
+  Qed.
+
+  Lemma bind_not_null [A B : choiceType] (m : M A) (f : A -> M B)
+    : forall map p, Def.bind m f map p <> 0%R -> exists p0, m map p0 <> 0%R /\ f p0.1 p0.2 p <> 0%R.
+  Proof.
+    move=> map p; rewrite /Def.bind dletE=> /neq0_psum [p0] /R_no0div ? ;by exists p0.
+  Qed.
+
+  Lemma bind_rule [A B : choiceType] (m : C A) (f : A -> C B) prem postm pref postf:
+    ⊨ ⦃ prem ⦄ m ⦃ p, postm p ⦄ ->
+    (forall a, ⊨ ⦃ pref a ⦄ f a ⦃ p, postf a p ⦄) ->
+    ⊨ ⦃ bind_pre prem postm pref ⦄ bind m f ⦃ p, bind_post postm postf p ⦄.
+  Proof.
+    move=> hm hf map /andP[/= hprem /asboolP hpostmpref].
+    rewrite eval_bind => p /bind_not_null [p0 [hevm hevf]].
+    apply/asboolP; exists p0. apply/implyP=> hpostm.
+    move: (hpostmpref p0); rewrite hpostm /= => hpref.
+    apply: (hf _ _ hpref)=> //.
+  Qed.
+
+
+  (** Weaken rule *)
+
+  Lemma weaken_rule
+        [A : choiceType]
+        [pre wkpre : precondition]
+        (c : C A)
+        [post wkpost : postcondition A] :
+    subpred wkpre pre ->
+    subpred post wkpost ->
+    ⊨ ⦃ pre ⦄ c ⦃ p, post p ⦄ ->
+    ⊨ ⦃ wkpre ⦄ c ⦃ p, wkpost p ⦄.
+  Proof.
+    move=> hsubpre hsubpost hc ? /hsubpre hpre ? ?; apply: hsubpost.
+    by apply: (hc _ hpre).
+  Qed.
+
+
+  (* To continue: get rule, put rule, sampling rule, rule for imported operations ? *)
+
+End Evaluation.

From 5d3532240d5413d6b845a0f26b0c6a034258589d Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Fri, 21 Jan 2022 18:04:40 +0100
Subject: [PATCH 4/7] setting up a relational judgement

---
 _CoqProject                       |   1 +
 theories/Crypt/semantics/binary.v | 200 ++++++++++++++++++++++++++++++
 theories/Crypt/semantics/unary.v  |  75 ++++++++---
 3 files changed, 258 insertions(+), 18 deletions(-)
 create mode 100644 theories/Crypt/semantics/binary.v

diff --git a/_CoqProject b/_CoqProject
index 5ec254cf..24c474e4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -52,6 +52,7 @@ theories/Crypt/rules/RulesProb.v
 
 # Decategorified semantics
 theories/Crypt/semantics/unary.v
+theories/Crypt/semantics/binary.v
 
 
 # Crypto
diff --git a/theories/Crypt/semantics/binary.v b/theories/Crypt/semantics/binary.v
new file mode 100644
index 00000000..99bd07c4
--- /dev/null
+++ b/theories/Crypt/semantics/binary.v
@@ -0,0 +1,200 @@
+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 chUniverse 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.
+  Context (Loc : {fset Location}).
+  Context (import : Interface).
+
+  (* Local shorter names for code and semantics *)
+  Let C := code Loc import.
+  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 ] }.
+
+  (** Taking an interpretation of the imported operation as assumption *)
+  Context (import_eval : forall o, o \in import -> src o -> M (tgt o)).
+
+  Let eval [A] := eval import import_eval (A:=A).
+
+  Definition prerelation := rel heap.
+  Definition postrelation A1 A2 := (A1 * heap) -> pred (A2 * heap).
+
+  Definition binary_judgement [A1 A2 : choiceType]
+             (pre : prerelation)
+             (c1 : C A1) (c2 : C A2)
+             (post : postrelation A1 A2) :=
+    forall map1 map2, pre map1 map2 ->
+                 exists d, d ~[eval c1 map1, eval c2 map2] /\
+                      forall p1 p2, d (p1,p2) <> 0%R -> post p1 p2.
+
+  Open Scope package_scope.
+
+  (* Bindings in the pre/postcondition looks annoying here *)
+  Notation "⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄" :=
+    (binary_judgement pre {code c1} {code 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 /eval 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.
diff --git a/theories/Crypt/semantics/unary.v b/theories/Crypt/semantics/unary.v
index 273ba431..7d435f90 100644
--- a/theories/Crypt/semantics/unary.v
+++ b/theories/Crypt/semantics/unary.v
@@ -32,6 +32,42 @@ Proof.
   apply: eq_psum=> a; f_equal; by rewrite fg.
 Qed.
 
+(* Lemma dlet_restr [A B : choiceType] (m : {distr A/R}) *)
+(*       (f : A -> {distr B /R}) : *)
+(*   \dlet_(x <- m) f x = \dlet_(x <- m) drestr [pred _ | m x != 0%R] (f x). *)
+(* Proof. *)
+(*   apply: distr_ext=> z; rewrite 2!dletE. *)
+(*   apply: eq_psum=> a; case E: (m a == 0)%R=> /=; last by rewrite drestrE. *)
+(*   move: E=> /eqP ->; by rewrite 2!GRing.mul0r. *)
+(* Qed. *)
+
+Lemma eq_dlet_partial [A B : choiceType] (m : {distr A/R})
+      (f g : A -> {distr B /R}) :
+  (forall x, m x <> 0%R -> f x = g x) -> \dlet_(x <- m) f x = \dlet_(x <- m) g x.
+Proof.
+  move=> fg; apply: distr_ext=> i; rewrite 2!dletE.
+  apply: eq_psum=> a; case E: (m a == 0)%R=> /=.
+  + move: E=> /eqP ->; by rewrite 2!GRing.mul0r.
+  + f_equal; rewrite fg=> //; apply/(_ =P _); exact (negbT E).
+Qed.
+
+
+
+
+(* two helper functions to help with convoy patterns on bool
+   (is there an idiomatic ssreflect/mathcomp way to do that ?) *)
+Definition bool_depelim (X : Type) (b : bool) (htrue : b = true -> X) (hfalse : b = false -> X) : X :=
+  (if b as b0 return b = b0 -> X then htrue else hfalse) erefl.
+
+Lemma bool_depelim_true (X : Type) (b : bool) (htrue : b = true -> X) (hfalse : b = false -> X) (e : b = true) : bool_depelim X b htrue hfalse = htrue e.
+Proof. by depelim e. Qed.
+
+(* helper lemma for multiplication of reals *)
+Lemma R_no0div : forall u v : R, (u * v <> 0 -> u <> 0 /\ v <> 0)%R.
+Proof.
+  move=> u v uv; split; move: uv; apply contra_not=> ->; [apply: GRing.mul0r|apply: GRing.mulr0].
+Qed.
+
 (** Definition of the model for the unary semantics *)
 
 Module Def.
@@ -71,6 +107,26 @@ Section Def.
   Qed.
 
 
+  Lemma bind_not_null [A B : choiceType] (m : stsubdistr A) (f : A -> stsubdistr B)
+    : forall map p, bind m f map p <> 0%R -> exists p0, m map p0 <> 0%R /\ f p0.1 p0.2 p <> 0%R.
+  Proof.
+    move=> map p; rewrite /bind dletE=> /neq0_psum [p0] /R_no0div ? ;by exists p0.
+  Qed.
+
+  Definition bind_restr [A B : choiceType] (m : stsubdistr A) (P : pred A) (f : forall (a : A), P a -> stsubdistr B) : stsubdistr B :=
+    let f' (a : A) := bool_depelim (stsubdistr B) (P a) (fun h => f a h) (fun _ _ => dnull) in
+    Def.bind m f'.
+
+  Lemma bind_restr_not_null [A B : choiceType] (m : stsubdistr A) (P : pred A) (f : forall (a : A), P a -> stsubdistr B)
+        (hP : forall map p, m map p <> 0%R -> P p.1) :
+    forall map p, bind_restr m P f map p <> 0%R -> exists p0, {hm : m map p0 <> 0%R | f p0.1 (hP _ _ hm) p0.2 p <> 0%R }.
+  Proof.
+    move=> map p /bind_not_null [p0 [hm0 hf0]].
+    exists p0; exists hm0; move: hf0.
+    rewrite bool_depelim_true; first apply: (hP _ _ hm0).
+    move=> hb; by rewrite (bool_irrelevance (hP _ _ _) hb).
+  Qed.
+
   Section Order.
     Context [A : choiceType].
 
@@ -155,12 +211,6 @@ Section Evaluation.
      defining evaluation on raw_code, and providing the adequate
      rules/hoare triples only on valid code.
    *)
-  (* two helper functions for the convoy pattern (is there an idiomatic ssreflect/mathcomp way to do that ?) *)
-  Definition bool_depelim (X : Type) (b : bool) (htrue : b = true -> X) (hfalse : b = false -> X) : X :=
-    (if b as b0 return b = b0 -> X then htrue else hfalse) erefl.
-
-  Lemma bool_depelim_true (X : Type) (b : bool) (htrue : b = true -> X) (hfalse : b = false -> X) (e : b = true) : bool_depelim X b htrue hfalse = htrue e.
-  Proof. by depelim e. Qed.
 
   Definition eval [A : choiceType] : raw_code A -> M A.
   Proof.
@@ -272,17 +322,6 @@ Section Evaluation.
       extensionality x; rewrite (ih x _) //.
   Qed.
 
-  (* Two helper lemmas *)
-  Lemma R_no0div : forall u v : R, (u * v <> 0 -> u <> 0 /\ v <> 0)%R.
-  Proof.
-    move=> u v uv; split; move: uv; apply contra_not=> ->; [apply: GRing.mul0r|apply: GRing.mulr0].
-  Qed.
-
-  Lemma bind_not_null [A B : choiceType] (m : M A) (f : A -> M B)
-    : forall map p, Def.bind m f map p <> 0%R -> exists p0, m map p0 <> 0%R /\ f p0.1 p0.2 p <> 0%R.
-  Proof.
-    move=> map p; rewrite /Def.bind dletE=> /neq0_psum [p0] /R_no0div ? ;by exists p0.
-  Qed.
 
   Lemma bind_rule [A B : choiceType] (m : C A) (f : A -> C B) prem postm pref postf:
     ⊨ ⦃ prem ⦄ m ⦃ p, postm p ⦄ ->
@@ -290,7 +329,7 @@ Section Evaluation.
     ⊨ ⦃ bind_pre prem postm pref ⦄ bind m f ⦃ p, bind_post postm postf p ⦄.
   Proof.
     move=> hm hf map /andP[/= hprem /asboolP hpostmpref].
-    rewrite eval_bind => p /bind_not_null [p0 [hevm hevf]].
+    rewrite eval_bind => p /Def.bind_not_null [p0 [hevm hevf]].
     apply/asboolP; exists p0. apply/implyP=> hpostm.
     move: (hpostmpref p0); rewrite hpostm /= => hpref.
     apply: (hf _ _ hpref)=> //.

From 47f4f7ac5ab0def70deea36920cf0bf68f77af9b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= <theo.winterhalter@gmail.com>
Date: Thu, 27 Jan 2022 11:30:58 +0100
Subject: [PATCH 5/7] Begin pass on new semantic files

---
 theories/Crypt/package/pkg_core_definition.v |   4 +-
 theories/Crypt/package/pkg_heap.v            |  56 +++--
 theories/Crypt/semantics/binary.v            |   2 +-
 theories/Crypt/semantics/unary.v             | 204 ++++++++++++-------
 4 files changed, 155 insertions(+), 111 deletions(-)

diff --git a/theories/Crypt/package/pkg_core_definition.v b/theories/Crypt/package/pkg_core_definition.v
index 5013c41f..d68d3e0b 100644
--- a/theories/Crypt/package/pkg_core_definition.v
+++ b/theories/Crypt/package/pkg_core_definition.v
@@ -82,8 +82,8 @@ Definition tgt (v : opsig) : choiceType :=
 (* Definition Op := Prob_ops_collection. *)
 (* Definition Arit := Prob_arities. *)
 
-Definition Op := ∑ (X : chUniverse) , {distr (chElement X) / R}.
-Definition Arit : Op -> choiceType := chElement \o (@projT1 _ _).
+Definition Op := ∑ (X : choice_type) , {distr (chElement X) / R}.
+Definition Arit : Op → choiceType := chElement \o (@projT1 _ _).
 
 Section FreeModule.
 
diff --git a/theories/Crypt/package/pkg_heap.v b/theories/Crypt/package/pkg_heap.v
index 85a99379..d35c92db 100644
--- a/theories/Crypt/package/pkg_heap.v
+++ b/theories/Crypt/package/pkg_heap.v
@@ -135,46 +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.
+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.
diff --git a/theories/Crypt/semantics/binary.v b/theories/Crypt/semantics/binary.v
index 99bd07c4..3d58b2a1 100644
--- a/theories/Crypt/semantics/binary.v
+++ b/theories/Crypt/semantics/binary.v
@@ -2,7 +2,7 @@ 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 chUniverse pkg_core_definition pkg_heap unary.
+From Crypt Require Import Axioms choice_type pkg_core_definition pkg_heap unary.
 
 Import Num.Theory Order.LTheory.
 
diff --git a/theories/Crypt/semantics/unary.v b/theories/Crypt/semantics/unary.v
index 7d435f90..88e368a2 100644
--- a/theories/Crypt/semantics/unary.v
+++ b/theories/Crypt/semantics/unary.v
@@ -1,8 +1,9 @@
+From Coq Require Import Utf8.
 Set Warnings "-notation-overridden,-ambiguous-paths".
 From mathcomp Require Import all_ssreflect all_algebra distr reals realsum boolp.
 Set Warnings "notation-overridden,ambiguous-paths".
 From extructures Require Import ord fset fmap.
-From Crypt Require Import Axioms chUniverse pkg_core_definition pkg_heap.
+From Crypt Require Import Axioms choice_type pkg_core_definition pkg_heap.
 
 Import Num.Theory Order.LTheory.
 
@@ -16,20 +17,27 @@ Set Default Goal Selector "!".
 Set Primitive Projections.
 
 (** Extensionality lemmas *)
-Lemma distr_ext : forall (A : choiceType) (mu nu : {distr A/R}),
-    distr.mu mu =1 distr.mu nu -> mu = nu.
+
+Lemma distr_ext :
+  ∀ (A : choiceType) (mu nu : {distr A/R}),
+    distr.mu mu =1 distr.mu nu →
+    mu = nu.
 Proof.
   move=> A [mu +++] [nu +++] /= /funext mu_eq_nu.
-  rewrite {}mu_eq_nu; move=> *; f_equal.
+  rewrite {}mu_eq_nu. move=> *. f_equal.
   all: apply proof_irrelevance.
 Qed.
 
-Lemma eq_dlet [A B : choiceType] (m : {distr A/R})
-      (f g : A -> {distr B /R}) :
-  f =1 g -> \dlet_(x <- m) f x = \dlet_(x <- m) g x.
+Lemma eq_dlet [A B : choiceType] :
+  ∀ (m : {distr A/R}) (f g : A -> {distr B /R}),
+    f =1 g →
+    \dlet_(x <- m) f x = \dlet_(x <- m) g x.
 Proof.
-  move=> fg; apply: distr_ext=> i; rewrite 2!dletE.
-  apply: eq_psum=> a; f_equal; by rewrite fg.
+  intros m f g fg.
+  apply distr_ext. intro i.
+  rewrite 2!dletE.
+  apply eq_psum. intro a.
+  f_equal. rewrite fg. reflexivity.
 Qed.
 
 (* Lemma dlet_restr [A B : choiceType] (m : {distr A/R}) *)
@@ -41,14 +49,18 @@ Qed.
 (*   move: E=> /eqP ->; by rewrite 2!GRing.mul0r. *)
 (* Qed. *)
 
-Lemma eq_dlet_partial [A B : choiceType] (m : {distr A/R})
-      (f g : A -> {distr B /R}) :
-  (forall x, m x <> 0%R -> f x = g x) -> \dlet_(x <- m) f x = \dlet_(x <- m) g x.
+Lemma eq_dlet_partial [A B : choiceType] :
+  ∀ (m : {distr A/R}) (f g : A -> {distr B /R}),
+    (∀ x, m x ≠ 0%R → f x = g x) →
+    \dlet_(x <- m) f x = \dlet_(x <- m) g x.
 Proof.
-  move=> fg; apply: distr_ext=> i; rewrite 2!dletE.
-  apply: eq_psum=> a; case E: (m a == 0)%R=> /=.
-  + move: E=> /eqP ->; by rewrite 2!GRing.mul0r.
-  + f_equal; rewrite fg=> //; apply/(_ =P _); exact (negbT E).
+  intros m f g h.
+  apply distr_ext. intro i.
+  rewrite 2!dletE. apply eq_psum. intro a.
+  destruct (m a == 0)%R eqn:e.
+  - move: e => /eqP e. rewrite e. rewrite 2!GRing.mul0r. reflexivity.
+  - f_equal. rewrite h. 2:{ apply /eqP. rewrite e. reflexivity. }
+    reflexivity.
 Qed.
 
 
@@ -56,78 +68,110 @@ Qed.
 
 (* two helper functions to help with convoy patterns on bool
    (is there an idiomatic ssreflect/mathcomp way to do that ?) *)
-Definition bool_depelim (X : Type) (b : bool) (htrue : b = true -> X) (hfalse : b = false -> X) : X :=
-  (if b as b0 return b = b0 -> X then htrue else hfalse) erefl.
-
-Lemma bool_depelim_true (X : Type) (b : bool) (htrue : b = true -> X) (hfalse : b = false -> X) (e : b = true) : bool_depelim X b htrue hfalse = htrue e.
-Proof. by depelim e. Qed.
+Definition bool_depelim (X : Type) (b : bool)
+  (htrue : b = true → X) (hfalse : b = false → X) : X :=
+  (if b as b0 return b = b0 → X then htrue else hfalse) erefl.
+
+Lemma bool_depelim_true :
+  ∀ (X : Type) (b : bool) (htrue : b = true → X) (hfalse : b = false → X)
+    (e : b = true),
+    bool_depelim X b htrue hfalse = htrue e.
+Proof.
+  intros. subst. reflexivity.
+Qed.
 
 (* helper lemma for multiplication of reals *)
-Lemma R_no0div : forall u v : R, (u * v <> 0 -> u <> 0 /\ v <> 0)%R.
+Lemma R_no0div : ∀ (u v : R), (u * v ≠ 0 → u ≠ 0 ∧ v ≠ 0)%R.
 Proof.
-  move=> u v uv; split; move: uv; apply contra_not=> ->; [apply: GRing.mul0r|apply: GRing.mulr0].
+  intros u v h.
+  split. all: revert h. all: apply contra_not. all: intro h. all: subst.
+  - apply GRing.mul0r.
+  - apply GRing.mulr0.
 Qed.
 
 (** Definition of the model for the unary semantics *)
 
 Module Def.
+
 Section Def.
+
   Context (S : choiceType).
 
   (* carrier for unary specifications /
      model for single probabilistic programs with state space S *)
-  Definition stsubdistr (A : choiceType) := S -> {distr (A * S) /R}.
+  Definition stsubdistr (A : choiceType) := S → {distr (A * S) / R}.
 
   Definition ret [A : choiceType] (a : A) : stsubdistr A :=
-    fun s => dunit (a,s).
+    λ s, dunit (a,s).
 
-  Definition bind [A B : choiceType] (m : stsubdistr A) (f : A -> stsubdistr B) :=
-    fun s0 => \dlet_(p <- m s0) f p.1 p.2.
+  Definition bind [A B : choiceType] (m : stsubdistr A) (f : A → stsubdistr B) :=
+    λ s₀, \dlet_(p <- m s₀) f p.1 p.2.
 
   (* Monadic laws -- wrapper around existing lemmas *)
-  Lemma bind_ret [A B : choiceType] (a : A) (f : A -> stsubdistr B)
-    : bind (ret a) f = f a.
-  Proof. extensionality s; apply: distr_ext ; apply: dlet_unit. Qed.
+  Lemma bind_ret [A B : choiceType] :
+    ∀ (a : A) (f : A → stsubdistr B),
+      bind (ret a) f = f a.
+  Proof.
+    intros a f.
+    extensionality s. apply distr_ext. apply: dlet_unit.
+  Qed.
 
-  Lemma ret_bind [A : choiceType] (m : stsubdistr A) : bind m (@ret _) = m.
+  Lemma ret_bind [A : choiceType] :
+    ∀ (m : stsubdistr A), bind m (@ret _) = m.
   Proof.
-    extensionality s ; apply: distr_ext=> a; rewrite /bind /ret.
+    intros m.
+    extensionality s. apply distr_ext. intro a.
+    rewrite /bind /ret.
     under eq_dlet do rewrite -surjective_pairing.
-    apply: dlet_dunit_id.
+    apply dlet_dunit_id.
   Qed.
 
-  Lemma bind_bind [A B C : choiceType]
-        (m : stsubdistr A)
-        (f : A -> stsubdistr B)
-        (g : B -> stsubdistr C) :
-    bind m (fun a => bind (f a) g) = bind (bind m f) g.
+  Lemma bind_bind [A B C : choiceType] :
+    ∀ (m : stsubdistr A)
+      (f : A → stsubdistr B)
+      (g : B → stsubdistr C),
+      bind m (λ a, bind (f a) g) = bind (bind m f) g.
   Proof.
-    extensionality s; apply distr_ext=> a; rewrite /bind.
-    by rewrite dlet_dlet.
+    intros m f g.
+    extensionality s. apply distr_ext. intro a.
+    rewrite /bind. rewrite dlet_dlet. reflexivity.
   Qed.
 
-
-  Lemma bind_not_null [A B : choiceType] (m : stsubdistr A) (f : A -> stsubdistr B)
-    : forall map p, bind m f map p <> 0%R -> exists p0, m map p0 <> 0%R /\ f p0.1 p0.2 p <> 0%R.
+  Lemma bind_not_null [A B : choiceType] :
+    ∀ (m : stsubdistr A) (f : A → stsubdistr B) map p,
+      bind m f map p ≠ 0%R →
+      ∃ p₀, m map p₀ ≠ 0%R ∧ f p₀.1 p₀.2 p ≠ 0%R.
   Proof.
-    move=> map p; rewrite /bind dletE=> /neq0_psum [p0] /R_no0div ? ;by exists p0.
+    intros m f map p.
+    unfold bind. rewrite dletE.
+    move /neq0_psum => [p₀]. move /R_no0div => h.
+    exists p₀. assumption.
   Qed.
 
-  Definition bind_restr [A B : choiceType] (m : stsubdistr A) (P : pred A) (f : forall (a : A), P a -> stsubdistr B) : stsubdistr B :=
-    let f' (a : A) := bool_depelim (stsubdistr B) (P a) (fun h => f a h) (fun _ _ => dnull) in
+  Definition bind_restr [A B : choiceType]
+    (m : stsubdistr A) (P : pred A) (f : ∀ (a : A), P a → stsubdistr B) :
+    stsubdistr B :=
+    let f' (a : A) :=
+      bool_depelim (stsubdistr B) (P a) (λ h, f a h) (λ _ _, dnull)
+    in
     Def.bind m f'.
 
-  Lemma bind_restr_not_null [A B : choiceType] (m : stsubdistr A) (P : pred A) (f : forall (a : A), P a -> stsubdistr B)
-        (hP : forall map p, m map p <> 0%R -> P p.1) :
-    forall map p, bind_restr m P f map p <> 0%R -> exists p0, {hm : m map p0 <> 0%R | f p0.1 (hP _ _ hm) p0.2 p <> 0%R }.
+  Lemma bind_restr_not_null [A B : choiceType] :
+    ∀ (m : stsubdistr A) (P : pred A) (f : ∀ (a : A), P a → stsubdistr B)
+      (hP : ∀ map p, m map p ≠ 0%R → P p.1) map p,
+      bind_restr m P f map p ≠ 0%R →
+      ∃ p₀, { hm : m map p₀ ≠ 0%R | f p₀.1 (hP _ _ hm) p₀.2 p ≠ 0%R }.
   Proof.
-    move=> map p /bind_not_null [p0 [hm0 hf0]].
-    exists p0; exists hm0; move: hf0.
-    rewrite bool_depelim_true; first apply: (hP _ _ hm0).
-    move=> hb; by rewrite (bool_irrelevance (hP _ _ _) hb).
+    intros m P f hP map p.
+    move => /bind_not_null [p₀ [hm₀ hf₀]].
+    exists p₀, hm₀.
+    revert hf₀. rewrite bool_depelim_true.
+    1:{ eapply hP. eassumption. }
+    intro hb. rewrite (bool_irrelevance (hP _ _ _) hb). auto.
   Qed.
 
   Section Order.
+
     Context [A : choiceType].
 
     (* The eqType and choiceType instances are given
@@ -138,20 +182,24 @@ Section Def.
 
     (** Order between specifications *)
     Definition stsubdistr_le : rel (stsubdistr A) :=
-      fun d0 d1 => `[< forall s0 a s1, (mu (d0 s0) (a, s1) <= mu (d1 s0) (a, s1))%O>].
+      λ d₀ d₁, `[< ∀ s₀ a s₁, (mu (d₀ s₀) (a, s₁) <= mu (d₁ s₀) (a, s₁))%O >].
 
     (* I don't think I really care about lt so let's put the tautological def *)
     Definition stsubdistr_lt : rel (stsubdistr A) :=
-      fun d0 d1 => (d1 != d0) && stsubdistr_le d0 d1.
+      λ d₀ d₁, (d₁ != d₀) && stsubdistr_le d₀ d₁.
 
     Lemma stsubdistr_le_refl : reflexive stsubdistr_le.
-    Proof. move=> g; apply/asboolP=> *; apply: le_refl. Qed.
+    Proof.
+      intros g.
+      apply /asboolP. intros.
+      apply le_refl.
+    Qed.
 
     Lemma stsubdistr_le_anti : antisymmetric stsubdistr_le.
     Proof.
       move=> f g /andP [] /asboolP fg /asboolP gf.
-      extensionality s; apply: distr_ext=> -[a s'].
-      apply: le_anti; rewrite fg gf //.
+      extensionality s. apply: distr_ext => -[a s'].
+      apply: le_anti. rewrite fg gf //.
     Qed.
 
     Lemma stsubdistr_le_trans : transitive stsubdistr_le.
@@ -165,7 +213,8 @@ Section Def.
                           ltac:(reflexivity) stsubdistr_le_refl
                           stsubdistr_le_anti stsubdistr_le_trans.
 
-    Canonical stsubdistr_porderType := POrderType ring_display (stsubdistr A) stsubdistr_porderMixin.
+    Canonical stsubdistr_porderType :=
+      POrderType ring_display (stsubdistr A) stsubdistr_porderMixin.
 
     (* Lemma stsubdistr_distinct (d0 d1 : stsubdistr A) : d0 < d1 ->  exists s0 a s1, (mu (d0 s0) (a, s1) < mu (d1 s0) (a, s1))%O. *)
 
@@ -174,10 +223,13 @@ Section Def.
   #[local] Open Scope order_scope.
 
   (** Bind is monotone with respect to the order we endowed the specs with *)
-  Lemma bind_monotone [A B : choiceType]
-        (m0 m1 : stsubdistr A) (f0 f1 : A -> stsubdistr B) :
-    m0 <= m1 -> (forall a, f0 a <= f1 a) -> bind m0 f0 <= bind m1 f1 :> stsubdistr B.
+  Lemma bind_monotone [A B : choiceType] :
+    ∀ (m₀ m₁ : stsubdistr A) (f₀ f₁ : A → stsubdistr B),
+      m₀ <= m₁ →
+      (∀ a, f₀ a <= f₁ a) →
+      bind m₀ f₁ <= bind m₁ f₁ :> stsubdistr B.
   Proof.
+    intros m₀ m₁ f₀ f₁.
     move=> /asboolP m01 f01; apply/asboolP=> s0 b s1.
     rewrite /bind 2!dletE.
     apply: le_psum; last apply: summable_mlet.
@@ -186,49 +238,51 @@ Section Def.
     - apply: ler_pmul; try apply: ge0_mu; first apply: m01.
       move: {f01}(f01 a)=> /asboolP //.
   Qed.
+
 End Def.
 
 Arguments ret [_ _] _.
 Arguments bind [_ _ _] _ _.
+
 End Def.
 
 
 (** Semantic evaluation of code and commands *)
 Section Evaluation.
+
   #[local] Open Scope fset.
   #[local] Open Scope fset_scope.
+
   Context (Loc : {fset Location}).
   Context (import : Interface).
 
   (* Local shorter names for code and semantics *)
   Let C := code Loc import.
-  Let M := (Def.stsubdistr heap_choiceType).
+  Let M := Def.stsubdistr heap_choiceType.
 
   (** Taking an interpretation of the imported operation as assumption *)
-  Context (import_eval : forall o, o \in import -> src o -> M (tgt o)).
+  Context (import_eval : ∀ o, o \in import → src o → M (tgt o)).
 
   (* Multiple attempts for evaluation. In the end it looks simpler
      defining evaluation on raw_code, and providing the adequate
      rules/hoare triples only on valid code.
    *)
 
-  Definition eval [A : choiceType] : raw_code A -> M A.
+  Definition eval [A : choiceType] : raw_code A → M A.
   Proof.
     elim.
     - apply: Def.ret.
-    - move=> o x k ih.
-      apply: (bool_depelim _ (o \in import) _ (fun _ _=> dnull))=> oval.
+    - intros o x k ih.
+      apply: (bool_depelim _ (o \in import) _ (λ _ _, dnull)) => oval.
       exact (Def.bind (import_eval o oval x) ih).
-    - move=> l k ih.
-      exact (fun map => let v := get_heap map l in ih v map).
-    - move=> l v k ih.
-      exact (fun map => ih (set_heap map l v)).
-    - move=> [X sampleX] k ih.
-      exact (fun map => \dlet_(x <- sampleX) ih x map).
+    - intros l k ih.
+      exact (λ map, let v := get_heap map l in ih v map).
+    - intros l v k ih.
+      exact (λ map, ih (set_heap map l v)).
+    - intros [X sampleX] k ih.
+      exact (λ map, \dlet_(x <- sampleX) ih x map).
   Defined.
 
-
-
   (* Definition eval [A : choiceType] : C A -> M A. *)
   (* Proof. *)
   (*   move=> []; elim. *)

From bd874bc0c8b4e3cab085c27ded0ae616e59f411c Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Fri, 28 Jan 2022 10:58:45 +0100
Subject: [PATCH 6/7] unary/binary judgements defined directly on raw code

---
 theories/Crypt/semantics/binary.v |  12 +--
 theories/Crypt/semantics/unary.v  | 151 ++++++++++--------------------
 2 files changed, 55 insertions(+), 108 deletions(-)

diff --git a/theories/Crypt/semantics/binary.v b/theories/Crypt/semantics/binary.v
index 3d58b2a1..a8958a10 100644
--- a/theories/Crypt/semantics/binary.v
+++ b/theories/Crypt/semantics/binary.v
@@ -87,20 +87,17 @@ End BindCoupling.
 Section Def.
   #[local] Open Scope fset.
   #[local] Open Scope fset_scope.
-  Context (Loc : {fset Location}).
-  Context (import : Interface).
 
   (* Local shorter names for code and semantics *)
-  Let C := code Loc import.
+  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 ] }.
 
-  (** Taking an interpretation of the imported operation as assumption *)
-  Context (import_eval : forall o, o \in import -> src o -> M (tgt o)).
+  Context (eval_op : forall o, src o -> M (tgt o)).
 
-  Let eval [A] := eval import import_eval (A:=A).
+  Let eval [A] := eval eval_op (A:=A).
 
   Definition prerelation := rel heap.
   Definition postrelation A1 A2 := (A1 * heap) -> pred (A2 * heap).
@@ -113,11 +110,10 @@ Section Def.
                  exists d, d ~[eval c1 map1, eval c2 map2] /\
                       forall p1 p2, d (p1,p2) <> 0%R -> post p1 p2.
 
-  Open Scope package_scope.
 
   (* Bindings in the pre/postcondition looks annoying here *)
   Notation "⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄" :=
-    (binary_judgement pre {code c1} {code c2} post) : Rules_scope.
+    (binary_judgement pre c1 c2 post) : Rules_scope.
   Open Scope Rules_scope.
 
   (** Ret rule *)
diff --git a/theories/Crypt/semantics/unary.v b/theories/Crypt/semantics/unary.v
index 88e368a2..dd20d7ff 100644
--- a/theories/Crypt/semantics/unary.v
+++ b/theories/Crypt/semantics/unary.v
@@ -40,15 +40,6 @@ Proof.
   f_equal. rewrite fg. reflexivity.
 Qed.
 
-(* Lemma dlet_restr [A B : choiceType] (m : {distr A/R}) *)
-(*       (f : A -> {distr B /R}) : *)
-(*   \dlet_(x <- m) f x = \dlet_(x <- m) drestr [pred _ | m x != 0%R] (f x). *)
-(* Proof. *)
-(*   apply: distr_ext=> z; rewrite 2!dletE. *)
-(*   apply: eq_psum=> a; case E: (m a == 0)%R=> /=; last by rewrite drestrE. *)
-(*   move: E=> /eqP ->; by rewrite 2!GRing.mul0r. *)
-(* Qed. *)
-
 Lemma eq_dlet_partial [A B : choiceType] :
   ∀ (m : {distr A/R}) (f g : A -> {distr B /R}),
     (∀ x, m x ≠ 0%R → f x = g x) →
@@ -101,6 +92,8 @@ Section Def.
      model for single probabilistic programs with state space S *)
   Definition stsubdistr (A : choiceType) := S → {distr (A * S) / R}.
 
+  Definition stsubnull (A : choiceType) : stsubdistr A := fun _ => dnull.
+
   Definition ret [A : choiceType] (a : A) : stsubdistr A :=
     λ s, dunit (a,s).
 
@@ -148,28 +141,12 @@ Section Def.
     exists p₀. assumption.
   Qed.
 
-  Definition bind_restr [A B : choiceType]
-    (m : stsubdistr A) (P : pred A) (f : ∀ (a : A), P a → stsubdistr B) :
-    stsubdistr B :=
-    let f' (a : A) :=
-      bool_depelim (stsubdistr B) (P a) (λ h, f a h) (λ _ _, dnull)
-    in
-    Def.bind m f'.
-
-  Lemma bind_restr_not_null [A B : choiceType] :
-    ∀ (m : stsubdistr A) (P : pred A) (f : ∀ (a : A), P a → stsubdistr B)
-      (hP : ∀ map p, m map p ≠ 0%R → P p.1) map p,
-      bind_restr m P f map p ≠ 0%R →
-      ∃ p₀, { hm : m map p₀ ≠ 0%R | f p₀.1 (hP _ _ hm) p₀.2 p ≠ 0%R }.
-  Proof.
-    intros m P f hP map p.
-    move => /bind_not_null [p₀ [hm₀ hf₀]].
-    exists p₀, hm₀.
-    revert hf₀. rewrite bool_depelim_true.
-    1:{ eapply hP. eassumption. }
-    intro hb. rewrite (bool_irrelevance (hP _ _ _) hb). auto.
-  Qed.
+  Lemma bind_ext [A B : choiceType] (m : stsubdistr A) (f g : A -> stsubdistr B) :
+    f =1 g -> bind m f = bind m g.
+  Proof. move=> fg; f_equal; extensionality x; apply: fg. Qed.
 
+
+  (* Actually unused for now... *)
   Section Order.
 
     Context [A : choiceType].
@@ -249,32 +226,18 @@ End Def.
 
 (** Semantic evaluation of code and commands *)
 Section Evaluation.
+  #[local]
+  Notation M := (Def.stsubdistr heap_choiceType).
 
-  #[local] Open Scope fset.
-  #[local] Open Scope fset_scope.
-
-  Context (Loc : {fset Location}).
-  Context (import : Interface).
-
-  (* Local shorter names for code and semantics *)
-  Let C := code Loc import.
-  Let M := Def.stsubdistr heap_choiceType.
-
-  (** Taking an interpretation of the imported operation as assumption *)
-  Context (import_eval : ∀ o, o \in import → src o → M (tgt o)).
-
-  (* Multiple attempts for evaluation. In the end it looks simpler
-     defining evaluation on raw_code, and providing the adequate
-     rules/hoare triples only on valid code.
-   *)
+  (** Assume an interpretation of operations *)
+  Context (eval_op : ∀ o, src o → M (tgt o)).
 
   Definition eval [A : choiceType] : raw_code A → M A.
   Proof.
     elim.
     - apply: Def.ret.
     - intros o x k ih.
-      apply: (bool_depelim _ (o \in import) _ (λ _ _, dnull)) => oval.
-      exact (Def.bind (import_eval o oval x) ih).
+      exact (Def.bind (eval_op o x) ih).
     - intros l k ih.
       exact (λ map, let v := get_heap map l in ih v map).
     - intros l v k ih.
@@ -283,50 +246,17 @@ Section Evaluation.
       exact (λ map, \dlet_(x <- sampleX) ih x map).
   Defined.
 
-  (* Definition eval [A : choiceType] : C A -> M A. *)
-  (* Proof. *)
-  (*   move=> []; elim. *)
-  (*   - move=> a _ ; exact (ret _ a). *)
-  (*   - move=> o x k ih /inversion_valid_opr [oval kval]. *)
-  (*     exact (bind _ (import_eval o oval x) (fun v => ih v (kval v))). *)
-  (*   - move=> l k ih /inversion_valid_getr [lval kval]. *)
-  (*     exact (bind _ (fun map => dunit (get_heap map l, map)) *)
-  (*                 (fun v => ih v (kval v))). *)
-  (*   - move=> l v k ih /inversion_valid_putr[lval kval]. *)
-  (*     exact (bind _ (fun map => dunit (tt, set_heap map l v)) (fun=> ih kval)). *)
-  (*   - move=> [X sampleX] ++/inversion_valid_sampler. *)
-  (*     rewrite /Arit=> /=k ih kval. *)
-  (*     exact (bind _ (fun s => \dlet_(x <- sampleX) dunit (x, s)) (fun x => ih x (kval x))). *)
-  (* Defined. *)
-
-  (* Definition eval [A : choiceType] : C A -> M A. *)
-  (* Proof. *)
-  (*   move=> []; elim. *)
-  (*   - move=> a _ ; exact (Def.ret a). *)
-  (*   - move=> o x k ih /inversion_valid_opr [oval kval]. *)
-  (*     exact (Def.bind (import_eval o oval x) (fun v => ih v (kval v))). *)
-  (*   - move=> l k ih /inversion_valid_getr [lval kval]. *)
-  (*     exact (fun map => let v := get_heap map l in ih v (kval v) map). *)
-  (*   - move=> l v k ih /inversion_valid_putr[lval kval]. *)
-  (*     exact (fun map => ih kval (set_heap map l v)). *)
-  (*   - move=> [X sampleX] ++/inversion_valid_sampler. *)
-  (*     rewrite /Arit=> /=k ih kval. *)
-  (*     exact (fun map => \dlet_(x <- sampleX) ih x (kval x) map). *)
-  (* Defined. *)
 
   (** Hoare triples *)
 
   Definition precondition := pred heap.
   Definition postcondition A := pred (A * heap).
 
-  Definition unary_judgement [A : choiceType] (pre : precondition) (c : C A) (post : postcondition A) : Prop :=
+  Definition unary_judgement [A : choiceType] (pre : precondition) (c : raw_code A) (post : postcondition A) : Prop :=
     forall map, pre map -> forall p, (eval c map p <> 0)%R -> post p.
 
   Declare Scope Rules_scope.
 
-  (* @théo Is there a binding key for the package_scope ?*)
-  Open Scope package_scope.
-
   (* Is there a way to have a version with and without binder for the result in
   parallel ? *)
   (* Notation "⊨ ⦃ pre ⦄ c ⦃ post ⦄" := *)
@@ -334,7 +264,7 @@ Section Evaluation.
   (*     : Rules_scope. *)
 
   Notation "⊨ ⦃ pre ⦄ c ⦃ p , post ⦄" :=
-    (unary_judgement pre {code c} (fun p => post))
+    (unary_judgement pre c (fun p => post))
       (p pattern) : Rules_scope.
   Open Scope Rules_scope.
 
@@ -358,26 +288,21 @@ Section Evaluation.
     [pred pf | `[< exists p, postm p ==> postf p.1 pf >]].
 
   (* the "difficult" part of the effect observation: commutation with bind *)
-  Lemma eval_bind [A B : choiceType] (m : C A) (f : A -> C B) :
-    eval {code bind m f} = Def.bind (eval m) (eval (A:=B) \o f).
+  Lemma eval_bind [A B : choiceType] (m : raw_code A) (f : A -> raw_code B) :
+    eval (bind m f) = Def.bind (eval m) (eval (A:=B) \o f).
   Proof.
-    case: m=> []; elim=> //=.
-    - move=> ??; rewrite Def.bind_ret /comp; f_equal.
-    - move=> o?? ih /inversion_valid_opr [oval kval].
-      rewrite 2!bool_depelim_true -Def.bind_bind; f_equal.
-      extensionality x; apply: ih; apply: kval.
-    - move=> l k ih /inversion_valid_getr [lval kval].
-      extensionality map; rewrite (ih _ (kval _)) //.
-    - move=> l c k ih /inversion_valid_putr [lval kval].
-      extensionality map; rewrite (ih kval) //.
-    - move=> [X sampleX] k ih /inversion_valid_sampler kval.
-      extensionality map. rewrite /Def.bind.
+    elim: m=> //=.
+    - move=> ?; rewrite Def.bind_ret /comp; f_equal.
+    - move=> o?? ih; rewrite -Def.bind_bind; apply: Def.bind_ext=> x; apply: ih.
+    - move=> l k ih; extensionality map; rewrite (ih _) //.
+    - move=> l c k ih; extensionality map; rewrite ih //.
+    - move=> [X sampleX] k ih; extensionality map. rewrite /Def.bind.
       apply: distr_ext=> z; rewrite dlet_dlet. do 2 f_equal.
-      extensionality x; rewrite (ih x _) //.
+      extensionality x; rewrite (ih x) //.
   Qed.
 
 
-  Lemma bind_rule [A B : choiceType] (m : C A) (f : A -> C B) prem postm pref postf:
+  Lemma bind_rule [A B : choiceType] (m : raw_code A) (f : A -> raw_code B) prem postm pref postf:
     ⊨ ⦃ prem ⦄ m ⦃ p, postm p ⦄ ->
     (forall a, ⊨ ⦃ pref a ⦄ f a ⦃ p, postf a p ⦄) ->
     ⊨ ⦃ bind_pre prem postm pref ⦄ bind m f ⦃ p, bind_post postm postf p ⦄.
@@ -395,7 +320,7 @@ Section Evaluation.
   Lemma weaken_rule
         [A : choiceType]
         [pre wkpre : precondition]
-        (c : C A)
+        (c : raw_code A)
         [post wkpost : postcondition A] :
     subpred wkpre pre ->
     subpred post wkpost ->
@@ -410,3 +335,29 @@ Section Evaluation.
   (* To continue: get rule, put rule, sampling rule, rule for imported operations ? *)
 
 End Evaluation.
+
+
+Section ScopedImportEval.
+  #[local] Open Scope fset.
+  #[local] Open Scope fset_scope.
+
+  #[local]
+  Notation M := (Def.stsubdistr heap_choiceType).
+
+  Context (import : Interface).
+
+  (** Taking an interpretation of the imported operation as assumption *)
+  Context (import_eval : ∀ o, o \in import → src o → M (tgt o)).
+
+  Definition eval_op : forall o, src o -> M (tgt o) :=
+    fun o => bool_depelim _ (o \in import) (fun oval => import_eval o oval) (fun _ _ => Def.stsubnull _ _).
+
+  Let eval := (eval eval_op).
+
+  (* Problem: the notation for the judgement is parametrized by eval, how can I
+  have access to this notation instantiated with eval without redefining it ?
+  Use a functor ?*)
+
+  (* TODO: Add spec and Rule for imported operations *)
+
+End ScopedImportEval.

From a2ee83fee2a81a5fbe3f2835b08ff56252235803 Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Fri, 28 Jan 2022 12:11:17 +0100
Subject: [PATCH 7/7] move interpretation of operations to a typeclass,
 notations for judgements moved into modules, tentative rule for operations

---
 theories/Crypt/semantics/binary.v | 26 +++++++---
 theories/Crypt/semantics/unary.v  | 80 +++++++++++++++++++++++++------
 2 files changed, 85 insertions(+), 21 deletions(-)

diff --git a/theories/Crypt/semantics/binary.v b/theories/Crypt/semantics/binary.v
index a8958a10..205bef00 100644
--- a/theories/Crypt/semantics/binary.v
+++ b/theories/Crypt/semantics/binary.v
@@ -95,21 +95,25 @@ Section Def.
   Definition stsubdistr_rel [A1 A2 : choiceType] : M A1 -> M A2 -> Type :=
     fun d1 d2 => forall map1 map2, { d |  d ~[ d1 map1 , d2 map2 ] }.
 
-  Context (eval_op : forall o, src o -> M (tgt o)).
-
-  Let eval [A] := eval eval_op (A:=A).
+  Context `{EvalOp}.
 
   Definition prerelation := rel heap.
   Definition postrelation A1 A2 := (A1 * heap) -> pred (A2 * heap).
 
-  Definition binary_judgement [A1 A2 : choiceType]
+  Definition relspec_valid [A1 A2 : choiceType]
              (pre : prerelation)
-             (c1 : C A1) (c2 : C A2)
+             (m1 : M A1) (m2 : M A2)
              (post : postrelation A1 A2) :=
     forall map1 map2, pre map1 map2 ->
-                 exists d, d ~[eval c1 map1, eval c2 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 ⦄" :=
@@ -180,7 +184,7 @@ Section Def.
     set df' := fun x => bool_depelim _ (P x) (fun hx => df (exist _ x hx))
                                     (fun _ => dnull).
     exists (bind_coupling dm df'); split.
-    + rewrite /eval 2!eval_bind /Def.bind.
+    + rewrite 2!eval_bind /Def.bind.
       apply: bind_coupling_partial_prop=> //.
       move=> p1' p2' /(hpostm _ _).
       move: (hpostmpref p1' p2')=> /implyP/[apply] hpref.
@@ -194,3 +198,11 @@ Section Def.
   Qed.
 
 End Def.
+
+Module BinaryNotations.
+  Notation "⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄" :=
+    (binary_judgement pre c1 c2 post) : Rules_scope.
+  Open Scope Rules_scope.
+End BinaryNotations.
+
+
diff --git a/theories/Crypt/semantics/unary.v b/theories/Crypt/semantics/unary.v
index dd20d7ff..473ba62b 100644
--- a/theories/Crypt/semantics/unary.v
+++ b/theories/Crypt/semantics/unary.v
@@ -71,6 +71,14 @@ Proof.
   intros. subst. reflexivity.
 Qed.
 
+Lemma bool_depelim_false :
+  ∀ (X : Type) (b : bool) (htrue : b = true → X) (hfalse : b = false → X)
+    (e : b = false),
+    bool_depelim X b htrue hfalse = hfalse e.
+Proof.
+  intros. subst. reflexivity.
+Qed.
+
 (* helper lemma for multiplication of reals *)
 Lemma R_no0div : ∀ (u v : R), (u * v ≠ 0 → u ≠ 0 ∧ v ≠ 0)%R.
 Proof.
@@ -223,6 +231,8 @@ Arguments bind [_ _ _] _ _.
 
 End Def.
 
+Class EvalOp :=
+  eval_interface_operations : forall o, src o -> Def.stsubdistr heap_choiceType (tgt o).
 
 (** Semantic evaluation of code and commands *)
 Section Evaluation.
@@ -230,14 +240,14 @@ Section Evaluation.
   Notation M := (Def.stsubdistr heap_choiceType).
 
   (** Assume an interpretation of operations *)
-  Context (eval_op : ∀ o, src o → M (tgt o)).
+  Context `{EvalOp}.
 
   Definition eval [A : choiceType] : raw_code A → M A.
   Proof.
     elim.
     - apply: Def.ret.
     - intros o x k ih.
-      exact (Def.bind (eval_op o x) ih).
+      exact (Def.bind (eval_interface_operations o x) ih).
     - intros l k ih.
       exact (λ map, let v := get_heap map l in ih v map).
     - intros l v k ih.
@@ -252,8 +262,10 @@ Section Evaluation.
   Definition precondition := pred heap.
   Definition postcondition A := pred (A * heap).
 
-  Definition unary_judgement [A : choiceType] (pre : precondition) (c : raw_code A) (post : postcondition A) : Prop :=
-    forall map, pre map -> forall p, (eval c map p <> 0)%R -> post p.
+  Definition spec_valid [A : choiceType] (pre : precondition) (m : M A) (post : postcondition A) : Prop :=
+    forall map, pre map -> forall p, (m map p <> 0)%R -> post p.
+
+  Definition unary_judgement [A : choiceType] (pre : precondition) (c : raw_code A) (post : postcondition A) : Prop := spec_valid pre (eval c) post.
 
   Declare Scope Rules_scope.
 
@@ -336,6 +348,18 @@ Section Evaluation.
 
 End Evaluation.
 
+Module UnaryNotations.
+  Notation "⊨ ⦃ pre ⦄ c ⦃ p , post ⦄" :=
+    (unary_judgement pre c (fun p => post))
+      (p pattern) : Rules_scope.
+  Open Scope Rules_scope.
+End UnaryNotations.
+
+
+(** Default interpretation for operations *)
+Definition eval_op_null : EvalOp :=
+  fun o _ => Def.stsubnull _ _.
+
 
 Section ScopedImportEval.
   #[local] Open Scope fset.
@@ -349,15 +373,43 @@ Section ScopedImportEval.
   (** Taking an interpretation of the imported operation as assumption *)
   Context (import_eval : ∀ o, o \in import → src o → M (tgt o)).
 
-  Definition eval_op : forall o, src o -> M (tgt o) :=
-    fun o => bool_depelim _ (o \in import) (fun oval => import_eval o oval) (fun _ _ => Def.stsubnull _ _).
-
-  Let eval := (eval eval_op).
-
-  (* Problem: the notation for the judgement is parametrized by eval, how can I
-  have access to this notation instantiated with eval without redefining it ?
-  Use a functor ?*)
-
-  (* TODO: Add spec and Rule for imported operations *)
+  #[local]
+  Instance eval_op : EvalOp :=
+    fun o => bool_depelim _ (o \in import)
+                       (fun oval => import_eval o oval)
+                       (fun _ _ => Def.stsubnull _ _).
+
+  Import UnaryNotations.
+
+  Context (op_precondition : forall o, o \in import -> src o -> precondition)
+          (op_postcondition : forall o, o \in import -> src o -> postcondition (tgt o))
+          (import_eval_valid : forall o (oval : o \in import) (s : src o),
+              spec_valid (op_precondition o oval s)
+                         (import_eval o oval s)
+                         (op_postcondition o oval s)).
+
+  Definition op_pre : forall o, src o -> precondition :=
+    fun o s => bool_depelim _ (o \in import)
+                         (fun oval => op_precondition o oval s)
+                         (fun _ => pred0).
+
+  Definition op_post : forall o, src o -> postcondition (tgt o) :=
+    fun o s => bool_depelim _ (o \in import)
+                         (fun oval => op_postcondition o oval s)
+                         (fun _ => predT).
+
+  Lemma opr_rule [A : choiceType] (post : postcondition A) :
+    forall o (s : src o) (k : tgt o -> raw_code A)
+    (spec_k : forall r, ⊨ ⦃ [pred map | op_post o s (r, map)] ⦄ k r ⦃ p , post p ⦄),
+      ⊨ ⦃ op_pre o s ⦄ opr o s k ⦃ p , post p ⦄.
+  Proof.
+    move=> o s k; case oval: (o \in import); rewrite /op_pre /op_post.
+    2: move=> _; by rewrite bool_depelim_false.
+    rewrite !bool_depelim_true // => spec_k map hpre p /=.
+    move=> /Def.bind_not_null [[r map0] []].
+    rewrite /eval_interface_operations/eval_op bool_depelim_true=> ??.
+    apply: (spec_k r map0)=> //=.
+    apply: import_eval_valid; first apply: hpre; move => //.
+  Qed.
 
 End ScopedImportEval.