diff --git a/_CoqProject b/_CoqProject
index de0eb968..24c474e4 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/Crypt/package/pkg_core_definition.v b/theories/Crypt/package/pkg_core_definition.v
index c6070358..d68d3e0b 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 : 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 :=
diff --git a/theories/Crypt/package/pkg_heap.v b/theories/Crypt/package/pkg_heap.v
index ed71ab8e..d35c92db 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)
   }.
@@ -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.
\ No newline at end of file
+Qed.
diff --git a/theories/Crypt/semantics/binary.v b/theories/Crypt/semantics/binary.v
new file mode 100644
index 00000000..205bef00
--- /dev/null
+++ b/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.
+
+
diff --git a/theories/Crypt/semantics/unary.v b/theories/Crypt/semantics/unary.v
new file mode 100644
index 00000000..473ba62b
--- /dev/null
+++ b/theories/Crypt/semantics/unary.v
@@ -0,0 +1,415 @@
+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 choice_type 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 :
+  ∀ (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.
+  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.
+  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 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.
+  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.
+
+
+
+
+(* 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.
+  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.
+  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 stsubnull (A : choiceType) : stsubdistr A := fun _ => dnull.
+
+  Definition ret [A : choiceType] (a : A) : stsubdistr A :=
+    λ s, dunit (a,s).
+
+  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.
+    intros a f.
+    extensionality s. apply distr_ext. apply: dlet_unit.
+  Qed.
+
+  Lemma ret_bind [A : choiceType] :
+    ∀ (m : stsubdistr A), bind m (@ret _) = m.
+  Proof.
+    intros m.
+    extensionality s. apply distr_ext. intro 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 (λ a, bind (f a) g) = bind (bind m f) g.
+  Proof.
+    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) map p,
+      bind m f map p ≠ 0%R →
+      ∃ p₀, m map p₀ ≠ 0%R ∧ f p₀.1 p₀.2 p ≠ 0%R.
+  Proof.
+    intros m f map p.
+    unfold bind. rewrite dletE.
+    move /neq0_psum => [p₀]. move /R_no0div => h.
+    exists p₀. assumption.
+  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].
+
+    (* 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) :=
+      λ 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) :=
+      λ d₀ d₁, (d₁ != d₀) && stsubdistr_le d₀ d₁.
+
+    Lemma stsubdistr_le_refl : reflexive stsubdistr_le.
+    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 //.
+    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.
+
+  #[local] Open Scope order_scope.
+
+  (** Bind is monotone with respect to the order we endowed the specs with *)
+  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.
+    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.
+
+Arguments ret [_ _] _.
+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.
+  #[local]
+  Notation M := (Def.stsubdistr heap_choiceType).
+
+  (** Assume an interpretation of operations *)
+  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_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.
+      exact (λ map, ih (set_heap map l v)).
+    - intros [X sampleX] k ih.
+      exact (λ map, \dlet_(x <- sampleX) ih x map).
+  Defined.
+
+
+  (** Hoare triples *)
+
+  Definition precondition := pred heap.
+  Definition postcondition A := pred (A * heap).
+
+  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.
+
+  (* 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 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 : raw_code A) (f : A -> raw_code B) :
+    eval (bind m f) = Def.bind (eval m) (eval (A:=B) \o f).
+  Proof.
+    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) //.
+  Qed.
+
+
+  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 ⦄.
+  Proof.
+    move=> hm hf map /andP[/= hprem /asboolP hpostmpref].
+    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)=> //.
+  Qed.
+
+
+  (** Weaken rule *)
+
+  Lemma weaken_rule
+        [A : choiceType]
+        [pre wkpre : precondition]
+        (c : raw_code 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.
+
+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.
+  #[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)).
+
+  #[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.