diff --git a/external/proba/basic/bigop_ext.v b/external/proba/basic/bigop_ext.v
index 626ee501..be154c20 100644
--- a/external/proba/basic/bigop_ext.v
+++ b/external/proba/basic/bigop_ext.v
@@ -469,7 +469,8 @@ Proof.
   intros HP.
   rewrite -(sum_index_ordinal_P_aux f l r P''); last first.
   {
-    intros i Hlt. rewrite /P'' //=. destruct lt_dec as [?|n] => //=.
+    intros i Hlt. rewrite /P'' //=.
+    destruct lt_dec as [?|n] => //= ; eauto.
     exfalso; apply n. apply /ltP. done.
   }
   rewrite /P'' //=.
diff --git a/external/proba/prob/rearrange.v b/external/proba/prob/rearrange.v
index 225ee61f..7d7b916d 100644
--- a/external/proba/prob/rearrange.v
+++ b/external/proba/prob/rearrange.v
@@ -749,7 +749,9 @@ Proof.
   {
       intros n. rewrite /countable_sum/σ'//=.
       destruct pickle_inv as [s|] => //=.
-      { destruct Req_EM_T as [Heq0|Hneq0] => //=. }
+      { destruct Req_EM_T as [Heq0|Hneq0] => //= ;
+          rewrite //= ; eapply EQ.
+      }
   }
   cut (is_series (countable_sum (λ n, Rabs (oapp a R0 (σ' n)))) v ∧
        is_series (countable_sum (λ n, oapp a R0 (σ' n))) (Series (countable_sum a))).
diff --git a/theories/app_rel_logic/adequacy.v b/theories/app_rel_logic/adequacy.v
index 3fc57fda..40759a6d 100644
--- a/theories/app_rel_logic/adequacy.v
+++ b/theories/app_rel_logic/adequacy.v
@@ -6,9 +6,9 @@ From iris.prelude Require Import options.
 
 From clutch.prelude Require Import stdpp_ext iris_ext.
 From clutch.prob_lang Require Import erasure notation.
-From clutch.program_logic Require Import language weakestpre.
+From clutch.common Require Import language.
 From clutch.ub_logic Require Import error_credits.
-From clutch.rel_logic Require Import spec_ra.
+From clutch.app_rel_logic Require Import spec_ra.
 From clutch.app_rel_logic Require Import app_weakestpre primitive_laws.
 From clutch.prob Require Import distribution couplings_app.
 Import uPred.
@@ -36,20 +36,20 @@ Section adequacy.
     to_val e1 = None →
     reducible e1 σ1 ->
     exec_coupl e1 σ1 e1' σ1' (λ '(e2, σ2) '(e2', σ2') ε',
-        |={∅}▷=>^(S n) ⌜ARcoupl (exec_val n (e2, σ2)) (lim_exec_val (e2', σ2')) φ ε'⌝) ε
-    ⊢ |={∅}▷=>^(S n) ⌜ARcoupl (exec_val (S n) (e1, σ1)) (lim_exec_val (e1', σ1')) φ ε⌝.
+        |={∅}▷=>^(S n) ⌜ARcoupl (exec n (e2, σ2)) (lim_exec (e2', σ2')) φ ε'⌝) ε
+    ⊢ |={∅}▷=>^(S n) ⌜ARcoupl (exec (S n) (e1, σ1)) (lim_exec (e1', σ1')) φ ε⌝.
   Proof.
     iIntros (Hv Hred) "Hexec".
     iAssert (⌜to_val e1 = None⌝)%I as "-#H"; [done|]. iRevert "Hexec H".
     rewrite /exec_coupl /exec_coupl'.
     set (Φ := (λ '(((e1, σ1),(e1', σ1')),ε'),
                 (⌜to_val e1 = None⌝ ={∅}▷=∗^(S n)
-                 ⌜ARcoupl (exec_val (S n) (e1, σ1)) (lim_exec_val (e1', σ1')) φ ε'⌝)%I) :
+                 ⌜ARcoupl (exec (S n) (e1, σ1)) (lim_exec (e1', σ1')) φ ε'⌝)%I) :
            prodO (prodO cfgO cfgO) NNRO  → iPropI Σ).
     assert (NonExpansive Φ).
     { intros m (((?&?)&(?&?))&?) (((?&?)&(?&?))&?) [[[[=] [=]] [[=] [=]]] [=] ]. by simplify_eq. }
     set (F := (exec_coupl_pre (λ '(e2, σ2) '(e2', σ2') ε',
-                   |={∅}▷=>^(S n) ⌜ARcoupl (exec_val n (e2, σ2)) (lim_exec_val (e2', σ2')) φ ε'⌝)%I)).
+                   |={∅}▷=>^(S n) ⌜ARcoupl (exec n (e2, σ2)) (lim_exec (e2', σ2')) φ ε'⌝)%I)).
     iPoseProof (least_fixpoint_iter F Φ with "[]") as "H"; last first.
     { iIntros "Hfix %".
       by iMod ("H" $! ((_, _)) with "Hfix [//]").
@@ -57,8 +57,8 @@ Section adequacy.
     clear.
     iIntros "!#" ([[[e1 σ1] [e1' σ1']] ε'']). rewrite /exec_coupl_pre.
     iIntros "[(%R & %ε1 & %ε2 & %Hleq & % & %Hcpl & H) | [(%R & %ε1 & %ε2 & %Hleq & % & %Hcpl & H) | [(%R & %m & %ε1 & %ε2 & %Hleq & %Hcpl & H) | [H | [H | H]]]]] %Hv".
-    - rewrite exec_val_Sn_not_val; [|done].
-      rewrite lim_exec_val_prim_step.
+    - rewrite exec_Sn_not_final; [|eauto].
+      rewrite lim_exec_step.
       iApply step_fupdN_mono.
       { apply pure_mono.
         eapply ARcoupl_mon_grading; eauto. }
@@ -75,32 +75,32 @@ Section adequacy.
           -- iPureIntro; apply cond_nonneg.
           -- iPureIntro; apply cond_nonneg.
           -- iPureIntro.
-             rewrite -(Rplus_0_r ε1).
+             pose proof (Rplus_0_r ε1) as h. simpl in h. rewrite -h. clear h.
              apply (ARcoupl_eq_trans_r _ dzero); [apply cond_nonneg | lra | eauto |].
              apply ARcoupl_dzero; lra.
           -- iIntros ([e3 σ3] [e3' σ3']) "HR".
              by iMod ("H" $! (e3,σ3) (e3',σ3') with "HR").
-      + rewrite prim_step_or_val_no_val; [|done].
+      + rewrite step_or_final_no_final; [|eauto].
         iApply (ARcoupl_dbind' _ _ _ _ R); auto.
         * iPureIntro; apply cond_nonneg.
         * iPureIntro; apply cond_nonneg.
         * iIntros ([] [] HR). by iMod ("H" with "[//]").
-    - rewrite exec_val_Sn_not_val; [|done].
+    - rewrite exec_Sn_not_final; [|eauto].
       iApply step_fupdN_mono.
       { apply pure_mono.
         eapply ARcoupl_mon_grading; eauto. }
-      rewrite -(dret_id_left (lim_exec_val)).
+      rewrite -(dret_id_left (lim_exec)).
       iApply ARcoupl_dbind'.
       * iPureIntro; apply cond_nonneg.
       * iPureIntro; apply cond_nonneg.
       * iPureIntro. by apply ARcoupl_pos_R in Hcpl.
       * iIntros ([] [] (?&?& [= -> ->]%dret_pos)).
         by iMod ("H"  with "[//]").
-    - rewrite -(dret_id_left (exec_val _)).
+    - rewrite -(dret_id_left (exec _)).
       iApply step_fupdN_mono.
       { apply pure_mono.
         eapply ARcoupl_mon_grading; eauto. }
-      rewrite (lim_exec_val_exec m).
+      rewrite (lim_exec_pexec m).
       iApply ARcoupl_dbind'.
       + iPureIntro; apply cond_nonneg.
       + iPureIntro; apply cond_nonneg.
@@ -109,13 +109,13 @@ Section adequacy.
           by iMod ("H"  with "[//] [//]").
     - iDestruct (big_orL_mono _ (λ _ _,
                      |={∅}▷=>^(S n)
-                       ⌜ARcoupl (exec_val (S n) (e1, σ1))
-                                  (lim_exec_val (e1', σ1')) φ ε''⌝)%I
+                       ⌜ARcoupl (exec (S n) (e1, σ1))
+                                  (lim_exec (e1', σ1')) φ ε''⌝)%I
                   with "H") as "H".
       { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hleq & % & %Hcpl & H)".
         iApply (step_fupdN_mono _ _ _
-                  (⌜∀ e2 σ2 σ2', R2 (e2, σ2) σ2' → ARcoupl (exec_val n (e2, σ2))
-                                                             (lim_exec_val (e1', σ2')) φ ε2⌝)%I).
+                  (⌜∀ e2 σ2 σ2', R2 (e2, σ2) σ2' → ARcoupl (exec n (e2, σ2))
+                                                             (lim_exec (e1', σ2')) φ ε2⌝)%I).
         - iIntros (?). iPureIntro.
           eapply ARcoupl_mon_grading; eauto.
           rewrite /= /get_active in Hα.
@@ -130,13 +130,13 @@ Section adequacy.
       by iApply "IH".
     - iDestruct (big_orL_mono _ (λ _ _,
                      |={∅}▷=>^(S n)
-                       ⌜ARcoupl (exec_val (S n) (e1, σ1))
-                                  (lim_exec_val (e1', σ1')) φ ε''⌝)%I
+                       ⌜ARcoupl (exec (S n) (e1, σ1))
+                                  (lim_exec (e1', σ1')) φ ε''⌝)%I
                   with "H") as "H".
       { iIntros (i α' Hα'%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hleq & %Hcpl & H)".
         iApply (step_fupdN_mono _ _ _
-                  (⌜∀ σ2 e2' σ2', R2 σ2 (e2', σ2') → ARcoupl (exec_val (S n) (e1, σ2))
-                                                               (lim_exec_val (e2', σ2')) φ ε2⌝)%I).
+                  (⌜∀ σ2 e2' σ2', R2 σ2 (e2', σ2') → ARcoupl (exec (S n) (e1, σ2))
+                                                               (lim_exec (e2', σ2')) φ ε2⌝)%I).
         - iIntros (?). iPureIntro.
           rewrite /= /get_active in Hα'.
           apply elem_of_elements, elem_of_dom in Hα' as [].
@@ -149,17 +149,18 @@ Section adequacy.
       rewrite big_orL_cons.
       iDestruct "H" as "[H | Ht]"; [done|].
       by iApply "IH".
-    - rewrite exec_val_Sn_not_val; [|done].
+    - rewrite exec_Sn_not_final; [|eauto].
       iDestruct (big_orL_mono _ (λ _ _,
                      |={∅}▷=>^(S n)
-                       ⌜ARcoupl (prim_step e1 σ1 ≫= exec_val n)
-                                  (lim_exec_val (e1', σ1')) φ ε''⌝)%I
+                       ⌜ARcoupl (prim_step e1 σ1 ≫= exec n)
+                                  (lim_exec (e1', σ1')) φ ε''⌝)%I
                   with "H") as "H".
       { iIntros (i [α1 α2] [Hα1 Hα2]%elem_of_list_lookup_2%elem_of_list_prod_1) "(% & %ε1 & %ε2 & %Hleq & %Hcpl & H)".
-        rewrite -exec_val_Sn_not_val; [|done].
+        replace (prim_step e1 σ1) with (step (e1, σ1)) => //.
+        rewrite -exec_Sn_not_final; [|eauto].
         iApply (step_fupdN_mono _ _ _
-                  (⌜∀ σ2 σ2', R2 σ2 σ2' → ARcoupl (exec_val (S n) (e1, σ2))
-                                                    (lim_exec_val (e1', σ2')) φ ε2⌝)%I).
+                  (⌜∀ σ2 σ2', R2 σ2 σ2' → ARcoupl (exec (S n) (e1, σ2))
+                                                    (lim_exec (e1', σ2')) φ ε2⌝)%I).
         - iIntros (?). iPureIntro.
           rewrite /= /get_active in Hα1, Hα2.
           apply elem_of_elements, elem_of_dom in Hα1 as [], Hα2 as [].
@@ -178,10 +179,10 @@ Section adequacy.
 
   Theorem wp_ARcoupl_step_fupdN (e e' : expr) (σ σ' : state) n φ (ε : nonnegreal) :
     state_interp σ ∗ spec_interp (e', σ') ∗ spec_ctx ∗ err_interp ε ∗ WP e {{ v, ∃ v', ⤇ Val v' ∗ ⌜φ v v'⌝ }} ⊢
-    |={⊤,∅}=> |={∅}▷=>^n ⌜ARcoupl (exec_val n (e, σ)) (lim_exec_val (e', σ')) φ ε⌝.
+    |={⊤,∅}=> |={∅}▷=>^n ⌜ARcoupl (exec n (e, σ)) (lim_exec (e', σ')) φ ε⌝.
   Proof.
     iInduction n as [|n] "IH" forall (e σ e' σ' ε); iIntros "([Hh Ht] & HspecI_auth & #Hctx & Herr & Hwp)".
-    - rewrite /exec_val /=.
+    - rewrite /exec /=.
       destruct (to_val e) eqn:Heq.
       + apply of_to_val in Heq as <-.
         rewrite wp_value_fupd.
@@ -190,7 +191,7 @@ Section adequacy.
         iDestruct (spec_interp_auth_frag_agree with "HspecI_auth HspecI_frag") as %<-.
         iDestruct (spec_prog_auth_frag_agree with "Hspec_auth Hspec_frag") as %->.
         iApply fupd_mask_intro; [set_solver|]; iIntros "_".
-        erewrite lim_exec_val_exec_det; [|done].
+        erewrite lim_exec_det_final ; last first ; eauto.
         iPureIntro.
         rewrite /dmap.
         apply (ARcoupl_mon_grading _ _ _ 0); [apply cond_nonneg | ].
@@ -198,7 +199,7 @@ Section adequacy.
       + iApply fupd_mask_intro; [set_solver|]; iIntros "_".
         iPureIntro.
         apply ARcoupl_dzero, cond_nonneg.
-    - rewrite exec_val_Sn /prim_step_or_val /=.
+    - rewrite exec_Sn /step_or_final /=.
       destruct (to_val e) eqn:Heq.
       + apply of_to_val in Heq as <-.
         rewrite wp_value_fupd.
@@ -209,17 +210,18 @@ Section adequacy.
         iApply fupd_mask_intro; [set_solver|]; iIntros "_".
         iApply step_fupdN_intro; [done|]. do 4 iModIntro.
         iPureIntro.
-        rewrite exec_val_unfold dret_id_left /=.
-        erewrite lim_exec_val_exec_det; [|done].
+        rewrite exec_unfold dret_id_left /=.
+        erewrite lim_exec_det_final; do 2 eauto.
         apply (ARcoupl_mon_grading _ _ _ 0); [apply cond_nonneg | ].
         by apply ARcoupl_dret.
       + rewrite wp_unfold /wp_pre /= Heq.
         iMod ("Hwp" with "[$]") as "(%Hred & Hcpl)".
         iModIntro.
-        rewrite -exec_val_Sn_not_val; [|done].
+        assert ((prim_step e σ) = (step (e, σ))) as h => //. rewrite h. clear h.
+        rewrite -exec_Sn_not_final ; [|auto].
         iPoseProof
           (exec_coupl_mono _ (λ '(e2, σ2) '(e2', σ2') ε', |={∅}▷=>^(S n)
-             ⌜ARcoupl (exec_val n (e2, σ2)) (lim_exec_val (e2', σ2')) φ ε'⌝)%I
+             ⌜ARcoupl (exec n (e2, σ2)) (lim_exec (e2', σ2')) φ ε'⌝)%I
             with "[] Hcpl") as "H".
         { iIntros ([] [] ?) "H !> !>".
           iMod "H" as "(Hstate & HspecI_auth & Hwp)".
@@ -250,7 +252,7 @@ Proof. solve_inG. Qed.
 
 Theorem wp_aRcoupl Σ `{app_clutchGpreS Σ} (e e' : expr) (σ σ' : state) n (ε : nonnegreal) φ :
   (∀ `{app_clutchGS Σ}, ⊢ spec_ctx -∗ ⤇ e' -∗ € ε -∗ WP e {{ v, ∃ v', ⤇ Val v' ∗ ⌜φ v v'⌝ }} ) →
-  ARcoupl (exec_val n (e, σ)) (lim_exec_val (e', σ')) φ ε.
+  ARcoupl (exec n (e, σ)) (lim_exec (e', σ')) φ ε.
 Proof.
   intros Hwp.
   eapply (step_fupdN_soundness_no_lc _ n 0).
@@ -267,7 +269,7 @@ Proof.
   set (HspecGS := CfgSG Σ _ γsi _ γp _ _ γHs γTs).
   set (HclutchGS := HeapG Σ _ _ _ γH γT HspecGS _).
   iMod (inv_alloc specN ⊤ spec_inv with "[Hsi_frag Hprog_auth Hh_spec Ht_spec]") as "#Hctx".
-  { iModIntro. iExists _, _, _, O. iFrame. rewrite exec_O dret_1_1 //.
+  { iModIntro. iExists _, _, _, O. iFrame. rewrite pexec_O dret_1_1 //.
   }
   iApply wp_ARcoupl_step_fupdN.
   iFrame. iFrame "Hctx".
@@ -277,19 +279,19 @@ Qed.
 
 Theorem wp_aRcoupl_lim Σ `{app_clutchGpreS Σ} (e e' : expr) (σ σ' : state) (ε : nonnegreal) φ :
   (∀ `{app_clutchGS Σ}, ⊢ spec_ctx -∗ ⤇ e' -∗ € ε -∗ WP e {{ v, ∃ v', ⤇ Val v' ∗ ⌜φ v v'⌝ }} ) →
-  ARcoupl (lim_exec_val (e, σ)) (lim_exec_val (e', σ')) φ ε.
+  ARcoupl (lim_exec (e, σ)) (lim_exec (e', σ')) φ ε.
 Proof.
   intros Hwp.
-  rewrite {1}/lim_exec_val/=.
+  rewrite {1}/lim_exec/=.
   intros f g Hf Hg Hfg.
   assert (forall n,
-    SeriesC (λ a, exec_val n (e, σ) a * f a) <=
-         SeriesC (λ b, lim_exec_val (e', σ') b * g b) + ε) as Haux2.
+    SeriesC (λ a, exec n (e, σ) a * f a) <=
+         SeriesC (λ b, lim_exec (e', σ') b * g b) + ε) as Haux2.
   {
    intro. eapply wp_aRcoupl; eauto.
   }
   assert (forall a,
-             Rbar.is_finite (Lim_seq.Sup_seq (λ n : nat, Rbar.Finite (exec_val n (e, σ) a)))) as Hfin.
+             Rbar.is_finite (Lim_seq.Sup_seq (λ n : nat, Rbar.Finite (exec n (e, σ) a)))) as Hfin.
   {
     intro a.
     apply (is_finite_bounded 0 1).
@@ -298,17 +300,17 @@ Proof.
     - by apply upper_bound_ge_sup; intro; simpl.
   }
   setoid_rewrite lim_distr_pmf at 1.
-  transitivity (Rbar.real (Lim_seq.Sup_seq (λ n : nat, Rbar.Finite (SeriesC (λ a : val, exec_val n (e, σ) a * f a))))).
+  transitivity (Rbar.real (Lim_seq.Sup_seq (λ n : nat, Rbar.Finite (SeriesC (λ a : val, exec n (e, σ) a * f a))))).
   - right.
     setoid_rewrite (rbar_scal_r); auto.
     setoid_rewrite <- Sup_seq_scal_r; [ | apply Hf].
     simpl.
     eapply MCT_seriesC.
     + intros n a; auto. specialize (Hf a); real_solver.
-    + intros n a. apply Rmult_le_compat_r; [apply Hf | apply exec_val_mon].
+    + intros n a. apply Rmult_le_compat_r; [apply Hf | apply (exec_mono (e,σ))].
     + intro a; exists 1; intro n. specialize (Hf a); real_solver.
     + intro n. apply SeriesC_correct.
-      apply (ex_seriesC_le _ (exec_val n (e, σ))); auto.
+      apply (ex_seriesC_le _ (exec n (e, σ))); auto.
       intro a; specialize (Hf a). split; [ real_solver |].
       rewrite <- Rmult_1_r. real_solver.
     + rewrite rbar_finite_real_eq; last first.
@@ -320,7 +322,7 @@ Proof.
         case_match; real_solver.
       - apply upper_bound_ge_sup; intro; simpl.
         etrans.
-        + apply (SeriesC_le _ (exec_val n (e, σ))); auto.
+        + apply (SeriesC_le _ (exec n (e, σ))); auto.
           intro a; specialize (Hf a). split; [ real_solver |].
           rewrite <- Rmult_1_r. real_solver.
         + auto.
diff --git a/theories/app_rel_logic/app_weakestpre.v b/theories/app_rel_logic/app_weakestpre.v
index fad2a42f..79646e09 100644
--- a/theories/app_rel_logic/app_weakestpre.v
+++ b/theories/app_rel_logic/app_weakestpre.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 
 From clutch.prelude Require Import stdpp_ext iris_ext NNRbar.
 From clutch.prob Require Export couplings_app distribution.
-From clutch.program_logic Require Export exec language.
+From clutch.common Require Export language.
 
 Import uPred.
 
@@ -44,7 +44,7 @@ Section exec_coupl.
             ∀ ρ2, ⌜R ρ2 (e1', σ1')⌝ ={∅}=∗ Z ρ2 (e1', σ1') ε2) ∨
       (* an arbitrary amount of [prim_step]s on the right *)
       (∃ R n (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗
-          ⌜ARcoupl (dret (e1, σ1)) (exec n (e1', σ1')) R ε1⌝ ∗
+          ⌜ARcoupl (dret (e1, σ1)) (pexec n (e1', σ1')) R ε1⌝ ∗
             ∀ e2' σ2', ⌜R (e1, σ1) (e2', σ2')⌝ ={∅}=∗ Φ (((e1, σ1), (e2', σ2')), ε2)) ∨
       (* [prim_step] on the left, [state_step] on the right *)
       ([∨ list] α' ∈ get_active σ1',
@@ -129,7 +129,7 @@ Section exec_coupl.
             ⌜ARcoupl (prim_step e1 σ1) (dret (e1', σ1')) R ε1⌝ ∗
             ∀ ρ2, ⌜R ρ2 (e1', σ1')⌝ ={∅}=∗ Z ρ2 (e1', σ1') ε2) ∨
       (∃ R n (ε1 ε2 : nonnegreal), ⌜ (ε1 + ε2 <= ε)%R ⌝ ∗
-          ⌜ARcoupl (dret (e1, σ1)) (exec n (e1', σ1')) R ε1⌝ ∗
+          ⌜ARcoupl (dret (e1, σ1)) (pexec n (e1', σ1')) R ε1⌝ ∗
             ∀ e2' σ2', ⌜R (e1, σ1) (e2', σ2')⌝ ={∅}=∗ exec_coupl e1 σ1 e2' σ2' Z ε2) ∨
       (* [prim_step] on the left, [state_step] on the right *)
       ([∨ list] α' ∈ get_active σ1',
@@ -301,7 +301,7 @@ Section exec_coupl.
       iSplit; [done | ].
       iSplit.
       { iPureIntro.
-        rewrite -(dret_id_right (exec _ _)).
+        rewrite -(dret_id_right (pexec _ _)).
         rewrite -(dret_id_left (λ ρ, dret (K ρ.1, ρ.2)) (_, σ)).
         rewrite <- Rplus_0_r.
         eapply ARcoupl_dbind; eauto.
@@ -387,7 +387,7 @@ Section exec_coupl.
   Qed.
 
   Lemma exec_coupl_exec_r e1 σ1 e1' σ1' Z (ε ε' : nonnegreal) :
-    (∃ R n, ⌜ARcoupl (dret (e1, σ1)) (exec n (e1', σ1')) R ε⌝ ∗
+    (∃ R n, ⌜ARcoupl (dret (e1, σ1)) (pexec n (e1', σ1')) R ε⌝ ∗
             ∀ e2' σ2', ⌜R (e1, σ1) (e2', σ2')⌝ ={∅}=∗ exec_coupl e1 σ1 e2' σ2' Z ε')
     ⊢ exec_coupl e1 σ1 e1' σ1' Z (nnreal_plus ε ε').
   Proof.
@@ -497,7 +497,7 @@ Section exec_coupl.
 *)
 
   Lemma exec_coupl_det_r n e1 σ1 e1' σ1' e2' σ2' Z (ε : nonnegreal) :
-    exec n (e1', σ1') (e2', σ2') = 1 →
+    pexec n (e1', σ1') (e2', σ2') = 1 →
     exec_coupl e1 σ1 e2' σ2' Z ε -∗
     exec_coupl e1 σ1 e1' σ1' Z ε.
   Proof.
@@ -541,13 +541,13 @@ Proof.
 Qed.
 
 (* TODO: get rid of stuckness in notation [iris/bi/weakestpre.v] so that we don't have to do this *)
-Local Definition wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
-  λ (s : stuckness), fixpoint (wp_pre).
+Local Definition wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) () :=
+  {| wp := λ _ : (), fixpoint (wp_pre); wp_default := () |}.
 Local Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).
 Global Arguments wp' {Λ Σ _}.
 Global Existing Instance wp'.
-Local Lemma wp_unseal `{!irisGS Λ Σ} : wp = @wp_def Λ Σ _.
+Local Lemma wp_unseal `{!irisGS Λ Σ} : wp = (@wp_def Λ Σ _).(wp).
 Proof. rewrite -wp_aux.(seal_eq) //. Qed.
 
 Section wp.
@@ -604,11 +604,11 @@ Qed.
 Lemma wp_value_fupd' s E Φ v : WP of_val v @ s; E {{ Φ }} ⊣⊢ |={E}=> Φ v.
 Proof. rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
 
-Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
-  s1 ⊑ s2 → E1 ⊆ E2 →
-  WP e @ s1; E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 {{ Ψ }}.
+Lemma wp_strong_mono E1 E2 e Φ Ψ s :
+  E1 ⊆ E2 →
+  WP e @ s ; E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s ; E2 {{ Ψ }}.
 Proof.
-  iIntros (? HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
+  iIntros (HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
   rewrite !wp_unfold /wp_pre /=.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
@@ -632,7 +632,7 @@ Proof.
   iIntros (σ1 e1' σ1' ε) "Hi". iMod "H". by iApply "H".
 Qed.
 Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
-Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
+Proof. iIntros "H". iApply (wp_strong_mono E with "H"); auto. Qed.
 
 Lemma wp_atomic s E1 E2 e Φ `{!Atomic WeaklyAtomic e} :
   (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
@@ -679,7 +679,7 @@ Proof.
   iMod "H" as "(Hσ & Hρ & Hε & H)".
   iMod "HR".
   iFrame "Hσ Hρ Hε".
-  iApply (wp_strong_mono s s E2 with "H"); [done..|].
+  iApply (wp_strong_mono E2 with "H"); [done..|].
   iIntros "!>" (v) "H". by iApply "H".
 Qed.
 
@@ -726,12 +726,6 @@ Proof.
   iIntros (HΦ) "H"; iApply (wp_strong_mono with "H"); auto.
   iIntros (v) "?". by iApply HΦ.
 Qed.
-Lemma wp_stuck_mono s1 s2 E e Φ :
-  s1 ⊑ s2 → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
-Proof. iIntros (?) "H". iApply (wp_strong_mono with "H"); auto. Qed.
-Lemma wp_stuck_weaken s E e Φ :
-  WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
-Proof. apply wp_stuck_mono. by destruct s. Qed.
 Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
 Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
 Global Instance wp_mono' s E e :
diff --git a/theories/app_rel_logic/coupling_rules.v b/theories/app_rel_logic/coupling_rules.v
index 1d29a21e..d7b4b8a3 100644
--- a/theories/app_rel_logic/coupling_rules.v
+++ b/theories/app_rel_logic/coupling_rules.v
@@ -73,7 +73,7 @@ Section rules.
     iMod ("Hclose" with "[Hauth Hheap Hspec0 Htapes]") as "_".
     { iModIntro. rewrite /spec_inv.
       iExists _, _, (state_upd_tapes _ _), 0. simpl.
-      iFrame. rewrite exec_O dret_1_1 //. }
+      iFrame. rewrite pexec_O dret_1_1 //. }
     (* Our [WP] assumption with the updated resources now suffices to prove the goal *)
     iSpecialize ("Hwp" $! n m nm with "[$Hα $Hαₛ]").
     rewrite !wp_unfold /wp_pre /= He.
@@ -139,7 +139,7 @@ Section rules.
     iMod ("Hclose" with "[Hauth Hheap Hspec0 Htapes]") as "_".
     { iModIntro. rewrite /spec_inv.
       iExists _, _, (state_upd_tapes _ _), 0. simpl.
-      iFrame. rewrite exec_O dret_1_1 //. }
+      iFrame. rewrite pexec_O dret_1_1 //. }
     (* Our [WP] assumption with the updated resources now suffices to prove the goal *)
     iSpecialize ("Hwp" $! n m nm with "[$Hα $Hαₛ]").
     rewrite !wp_unfold /wp_pre /= He.
@@ -154,7 +154,7 @@ Section rules.
     nclose specN ⊆ E →
     spec_ctx ⊢
     {{{ € ε }}}
-      rand #z from #() @ E
+      rand #z @ E
       {{{ (n : fin (S N)), RET #n; ⌜ n ≠ t ⌝ }}}.
   Proof.
     iIntros (Nz Nε ?) "#Hinv %Φ !> Hε Hwp".
@@ -192,7 +192,7 @@ Section rules.
     iMod ("Hclose" with "[Hauth Hheap Hspec0 Htapes]") as "_".
     { iModIntro. rewrite /spec_inv.
       iExists _, _, _, 0. simpl.
-      iFrame. rewrite exec_O dret_1_1 //. }
+      iFrame. rewrite pexec_O dret_1_1 //. }
     (* Our [WP] assumption with the updated resources now suffices to prove the goal *)
     iSpecialize ("Hwp" $! n with "[]"). 1: easy.
     rewrite !wp_unfold /wp_pre /=.
@@ -207,12 +207,12 @@ Section rules.
     nclose specN ⊆ E →
     (N <= M)%R ->
     (((S M - S N) / S N) = ε)%R →
-    refines_right K (rand #w from #()) ∗
+    refines_right K (rand #w) ∗
     € ε ∗
     ▷ (∀ (n : fin (S N)) (m : fin (S M)),
         ⌜(fin_to_nat n = m)⌝ →
         refines_right K #m  -∗ WP (Val #n) @ E {{ Φ }})
-    ⊢ WP rand #z from #() @ E {{ Φ }}.
+    ⊢ WP rand #z @ E {{ Φ }}.
   Proof.
     iIntros (-> -> ? HNM Hε) "([#Hinv Hr ] & Hε & Hwp)".
     iApply wp_lift_step_fupd_couple; [done|].
@@ -255,7 +255,7 @@ Section rules.
     iMod ("Hclose" with "[Hauth Hheap Hspec0 Htapes]") as "_".
     { iModIntro. rewrite /spec_inv.
       iExists _, _, _, 0. simpl.
-      iFrame. rewrite exec_O dret_1_1 //. }
+      iFrame. rewrite pexec_O dret_1_1 //. }
     iModIntro. iFrame.
     iApply "Hwp"; eauto.
     iSplit; done.
@@ -271,11 +271,11 @@ Section rules.
     nclose specN ⊆ E →
     (M <= N)%R ->
     (((S N - S M) / S N) = ε)%R →
-    refines_right K (rand #w from #()) ∗
+    refines_right K (rand #w) ∗
     € ε ∗
     ▷ (∀ (m : fin (S M)),
         refines_right K #m  -∗ WP (Val #(f m)) @ E {{ Φ }})
-    ⊢ WP rand #z from #() @ E {{ Φ }}.
+    ⊢ WP rand #z @ E {{ Φ }}.
   Proof.
     iIntros (Hdom Hinj).
     set g := (λ m : fin (S M), Fin.of_nat_lt (Hdom m (fin_to_nat_lt m))).
@@ -327,7 +327,7 @@ Section rules.
     iMod ("Hclose" with "[Hauth Hheap Hspec0 Htapes]") as "_".
     { iModIntro. rewrite /spec_inv.
       iExists _, _, _, 0. simpl.
-      iFrame. rewrite exec_O dret_1_1 //. }
+      iFrame. rewrite pexec_O dret_1_1 //. }
     iModIntro. iFrame.
     assert (#(g b) = #(f b)) as ->.
     {
diff --git a/theories/app_rel_logic/ectx_lifting.v b/theories/app_rel_logic/ectx_lifting.v
index c2e6b4a9..efc92e3a 100644
--- a/theories/app_rel_logic/ectx_lifting.v
+++ b/theories/app_rel_logic/ectx_lifting.v
@@ -1,6 +1,6 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.proofmode Require Import proofmode.
-From clutch.program_logic Require Import ectx_language.
+From clutch.common Require Import ectx_language.
 From clutch.app_rel_logic Require Export app_weakestpre lifting.
 From iris.prelude Require Import options.
 
diff --git a/theories/app_rel_logic/examples/prfprp.v b/theories/app_rel_logic/examples/prfprp.v
index 6a65b173..2f4ec915 100644
--- a/theories/app_rel_logic/examples/prfprp.v
+++ b/theories/app_rel_logic/examples/prfprp.v
@@ -19,7 +19,7 @@ Section prf_prp.
       match: get hm "v" with
       | SOME "b" => "b"
       | NONE =>
-          let: "b" := (rand #val_size from #()) in
+          let: "b" := (rand #val_size) in
           set hm "v" "b";;
           "b"
       end.
@@ -28,7 +28,7 @@ Section prf_prp.
       match: get "hm" "v" with
       | SOME "b" => "b"
       | NONE =>
-          let: "b" := (rand #val_size from #()) in
+          let: "b" := (rand #val_size) in
           set "hm" "v" "b";;
           "b"
       end.
@@ -154,7 +154,7 @@ Section prf_prp.
       | SOME "n" => "n"
       | NONE =>
           let: "ln" := list_length !fv in
-          let: "n" := (rand ("ln" - #1) from #()) in
+          let: "n" := (rand ("ln" - #1)) in
           (match: list_remove_nth !fv "n" with
           | SOME "p" =>
               set hm "v" (Fst "p");;
@@ -171,7 +171,7 @@ Section prf_prp.
       | SOME "n" => "n"
       | NONE =>
           let: "ln" := list_length !"fv" in
-          let: "n" := (rand ("ln" - #1) from #()) in
+          let: "n" := (rand ("ln" - #1)) in
           (match: list_remove_nth !"fv" "n" with
           | SOME "p" =>
               set "hm" "v" (Fst "p");;
@@ -440,7 +440,7 @@ Section prf_prp.
      do 3 f_equal; lia.
     }
 
-    tp_bind (rand _ from _ )%E.
+    tp_bind (rand _)%E.
     iEval (rewrite refines_right_bind) in "HK".
     set f := (λ n : nat, if (n <=? vl) then Z.to_nat (nth n sr 0) else n + val_size).
     wp_apply (wp_couple_rand_rand_rev_inj val_size vl f val_size vl).
@@ -557,7 +557,7 @@ Definition test_prf: val :=
   letrec: "aux" "f" "i" :=
     (if: "i" ≤ #0
      then  "f"
-     else let: "x" := rand #val_size from #() in
+     else let: "x" := rand #val_size in
           "f" "x";;
           "aux" "f" ("i" - #1)) in
     "aux" "f" "n".
@@ -569,7 +569,7 @@ Definition test_prp: val :=
   letrec: "aux" "f" "i" :=
     (if: "i" ≤ #0
      then  "f"
-     else let: "x" := rand #val_size from #() in
+     else let: "x" := rand #val_size in
           "f" "x";;
           "aux" "f" ("i" - #1)) in
     "aux" "f" "n".
@@ -610,10 +610,10 @@ Definition test_prp: val :=
      iExists _,_,_. iFrame.
 
    - wp_pures.
-     wp_bind (rand _ from _)%E.
+     wp_bind (rand _)%E.
 
      tp_pures.
-     tp_bind (rand _ from _)%E.
+     tp_bind (rand _)%E.
      iEval (rewrite refines_right_bind) in "HK".
 
      iMod (ec_zero).
diff --git a/theories/app_rel_logic/primitive_laws.v b/theories/app_rel_logic/primitive_laws.v
index b111e700..604da63f 100644
--- a/theories/app_rel_logic/primitive_laws.v
+++ b/theories/app_rel_logic/primitive_laws.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Export ghost_map.
 From clutch.app_rel_logic Require Export app_weakestpre ectx_lifting.
 From clutch.prob_lang Require Export class_instances.
 From clutch.prob_lang Require Import tactics lang notation.
-From clutch.rel_logic Require Import spec_ra.
+From clutch.app_rel_logic Require Import spec_ra.
 From iris.prelude Require Import options.
 From clutch.ub_logic Require Export error_credits.
 
@@ -121,7 +121,7 @@ Qed.
 
 Lemma wp_rand (N : nat) (z : Z) E :
   TCEq N (Z.to_nat z) →
-  {{{ True }}} rand #z from #() @ E {{{ (n : fin (S N)), RET #n; True }}}.
+  {{{ True }}} rand #z @ E {{{ (n : fin (S N)), RET #n; True }}}.
 Proof.
   iIntros (-> Φ) "_ HΦ".
   iApply wp_lift_atomic_head_step; [done|].
@@ -151,7 +151,7 @@ Qed.
 
 Lemma wp_rand_tape N α n ns z E :
   TCEq N (Z.to_nat z) →
-  {{{ ▷ α ↪ (N; n :: ns) }}} rand #z from #lbl:α @ E {{{ RET #(LitInt n); α ↪ (N; ns) }}}.
+  {{{ ▷ α ↪ (N; n :: ns) }}} rand(#lbl:α) #z @ E {{{ RET #(LitInt n); α ↪ (N; ns) }}}.
 Proof.
   iIntros (-> Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
@@ -167,7 +167,7 @@ Qed.
 
 Lemma wp_rand_tape_empty N z α E :
   TCEq N (Z.to_nat z) →
-  {{{ ▷ α ↪ (N; []) }}} rand #z from #lbl:α @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }}}.
+  {{{ ▷ α ↪ (N; []) }}} rand(#lbl:α) #z @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }}}.
 Proof.
   iIntros (-> Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
@@ -183,7 +183,7 @@ Qed.
 Lemma wp_rand_tape_wrong_bound N M z α E ns :
   TCEq N (Z.to_nat z) →
   N ≠ M →
-  {{{ ▷ α ↪ (M; ns) }}} rand #z from #lbl:α @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }}}.
+  {{{ ▷ α ↪ (M; ns) }}} rand(#lbl:α) #z @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }}}.
 Proof.
   iIntros (-> ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
diff --git a/theories/app_rel_logic/proofmode.v b/theories/app_rel_logic/proofmode.v
index a8f68484..a989b8fc 100644
--- a/theories/app_rel_logic/proofmode.v
+++ b/theories/app_rel_logic/proofmode.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 From iris.proofmode Require Export tactics.
 From iris.program_logic Require Import atomic.
 
-From clutch.program_logic Require Import language ectx_language weakestpre.
+From clutch.common Require Import language ectx_language.
 From clutch.prob_lang Require Import lang notation class_instances tactics.
 From clutch.app_rel_logic Require Import primitive_laws.
 From iris.prelude Require Import options.
diff --git a/theories/app_rel_logic/spec_ra.v b/theories/app_rel_logic/spec_ra.v
index cc9ca09e..5471560c 100644
--- a/theories/app_rel_logic/spec_ra.v
+++ b/theories/app_rel_logic/spec_ra.v
@@ -5,7 +5,7 @@ From iris.algebra Require Import auth excl.
 From iris.base_logic.lib Require Import invariants ghost_map.
 From iris.prelude Require Import options.
 From iris.proofmode Require Import proofmode.
-From clutch.program_logic Require Import language ectxi_language exec.
+From clutch.common Require Import language ectxi_language.
 From clutch.prob_lang Require Import locations lang.
 
 Definition specN := nroot .@ "spec".
@@ -124,7 +124,7 @@ Section spec_ctx.
   Definition spec_inv : iProp Σ :=
     (∃ ρ e σ n,
         spec_interp_frag ρ ∗
-        ⌜exec n ρ (e, σ) = 1%R⌝ ∗
+        ⌜pexec n ρ (e, σ) = 1%R⌝ ∗
         spec_prog_auth e ∗
         spec_heap_auth σ.(heap) ∗
         spec_tapes_auth σ.(tapes))%I.
diff --git a/theories/app_rel_logic/spec_rules.v b/theories/app_rel_logic/spec_rules.v
index 4c8b2aed..51c0eaff 100644
--- a/theories/app_rel_logic/spec_rules.v
+++ b/theories/app_rel_logic/spec_rules.v
@@ -3,8 +3,8 @@ From stdpp Require Import namespaces.
 From iris.proofmode Require Import proofmode.
 From clutch.prelude Require Import stdpp_ext.
 From clutch.app_rel_logic Require Import lifting ectx_lifting.
-From clutch.prob_lang Require Import lang notation tactics metatheory.
-From clutch.rel_logic Require Export spec_ra.
+From clutch.prob_lang Require Import lang notation tactics metatheory exec_lang.
+From clutch.app_rel_logic Require Export spec_ra.
 From clutch.app_rel_logic Require Export app_weakestpre primitive_laws.
 
 Section rules.
@@ -118,7 +118,7 @@ Section rules.
   Lemma step_rand E K l N z n ns :
     TCEq N (Z.to_nat z) →
     nclose specN ⊆ E →
-    spec_ctx ∗ ⤇ fill K (rand #z from #lbl:l) ∗ l ↪ₛ (N; n :: ns)
+    spec_ctx ∗ ⤇ fill K (rand(#lbl:l) #z) ∗ l ↪ₛ (N; n :: ns)
     ={E}=∗ spec_ctx ∗ ⤇ fill K #n ∗ l ↪ₛ (N; ns).
   Proof.
     iIntros (-> ?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
@@ -146,7 +146,7 @@ Section rules.
     to_val e = None →
     (∀ σ1, reducible e σ1) →
     nclose specN ⊆ E →
-    spec_ctx ∗ ⤇ fill K (rand #z from #()) ∗
+    spec_ctx ∗ ⤇ fill K (rand #z) ∗
     (∀ n : fin (S N), ⤇ fill K #n -∗ WP e @ E {{ Φ }})
     ⊢ WP e @ E {{ Φ }}.
   Proof.
@@ -165,10 +165,10 @@ Section rules.
     iExists (λ _ '(e2', σ2'), ∃ n : fin (S (Z.to_nat z)), (e2', σ2') = (fill K #n, σ0')), 1.
     iSplit.
     { iPureIntro.
-      rewrite exec_1.
+      rewrite pexec_1.
       replace nnreal_zero with (nnreal_plus nnreal_zero nnreal_zero)
                                by by apply nnreal_ext => /= ; lra.
-      rewrite prim_step_or_val_no_val /=; [|by apply fill_not_val].
+      rewrite step_or_final_no_final /=; [|by apply to_final_None_2, fill_not_val].
       rewrite -(dret_id_right (dret _)) fill_dmap //.
       eapply ARcoupl_dbind => /=.
       1,2: simpl ; lra.
@@ -183,7 +183,7 @@ Section rules.
     iMod ("Hclose" with "[Hauth Hheap Hspec0 Htapes]") as "_".
     { iModIntro. rewrite /spec_inv.
       iExists _, _, _, 0. simpl.
-      iFrame. rewrite exec_O dret_1_1 //. }
+      iFrame. rewrite pexec_O dret_1_1 //. }
     iSpecialize ("Hwp" with "Hj").
     rewrite !wp_unfold /wp_pre /= He.
     iMod ("Hwp" $! _ with "[$Hh1 $Hspec $Ht1 $Herr]") as "Hwp".
@@ -200,7 +200,7 @@ Section rules.
     to_val e = None →
     (∀ σ1, reducible e σ1) →
     nclose specN ⊆ E →
-    spec_ctx ∗ ⤇ fill K (rand #z from #lbl:α) ∗ α ↪ₛ (N; []) ∗
+    spec_ctx ∗ ⤇ fill K (rand(#lbl:α) #z) ∗ α ↪ₛ (N; []) ∗
     ((α ↪ₛ (N; []) ∗ spec_ctx ∗ ∃ n : fin (S N), ⤇ fill K #n) -∗ WP e @ E {{ Φ }})
     ⊢ WP e @ E {{ Φ }}.
   Proof.
@@ -221,10 +221,10 @@ Section rules.
     iExists (λ _ '(e2', σ2'), ∃ n : fin (S _), (e2', σ2') = (fill K #n, σ0')), 1.
     iSplit.
     { iPureIntro.
-      rewrite exec_1.
+      rewrite pexec_1.
       replace nnreal_zero with (nnreal_plus nnreal_zero nnreal_zero)
                                by by apply nnreal_ext => /= ; lra.
-      rewrite prim_step_or_val_no_val /=; [|by apply fill_not_val].
+      rewrite step_or_final_no_final /=; [|by apply to_final_None_2, fill_not_val].
       rewrite -(dret_id_right (dret _)) fill_dmap //.
       eapply ARcoupl_dbind => /=.
       1,2: simpl; lra.
@@ -239,7 +239,7 @@ Section rules.
     iMod ("Hclose" with "[Hauth Hheap Hspec0 Htapes]") as "_".
     { iModIntro. rewrite /spec_inv.
       iExists _, _, _, 0. simpl.
-      iFrame. rewrite exec_O dret_1_1 //. }
+      iFrame. rewrite pexec_O dret_1_1 //. }
     iSpecialize ("Hwp" with "[$Hα $Hinv Hj]"); [eauto|].
     rewrite !wp_unfold /wp_pre /= He.
     iMod ("Hwp" $! _ with "[$Hh1 $Hspec $Ht1 $Herr]") as "Hwp".
@@ -257,7 +257,7 @@ Section rules.
     to_val e = None →
     (∀ σ1, reducible e σ1) →
     nclose specN ⊆ E →
-    spec_ctx ∗ ⤇ fill K (rand #z from #lbl:α) ∗ α ↪ₛ (M; ns) ∗
+    spec_ctx ∗ ⤇ fill K (rand(#lbl:α) #z) ∗ α ↪ₛ (M; ns) ∗
     ((α ↪ₛ (M; ns) ∗ spec_ctx ∗ ∃ n : fin (S N), ⤇ fill K #n) -∗ WP e @ E {{ Φ }})
     ⊢ WP e @ E {{ Φ }}.
   Proof.
@@ -278,10 +278,10 @@ Section rules.
     iExists (λ _ '(e2', σ2'), ∃ n : fin (S _), (e2', σ2') = (fill K #n, σ0')), 1.
     iSplit.
     { iPureIntro.
-      rewrite exec_1.
+      rewrite pexec_1.
       replace nnreal_zero with (nnreal_plus nnreal_zero nnreal_zero)
                                by by apply nnreal_ext => /= ; lra.
-      rewrite prim_step_or_val_no_val /=; [|by apply fill_not_val].
+      rewrite step_or_final_no_final /=; [|by apply to_final_None_2, fill_not_val].
       rewrite -(dret_id_right (dret _)) fill_dmap //.
       eapply ARcoupl_dbind => /=.
       1,2: simpl; lra.
@@ -297,7 +297,7 @@ Section rules.
     iMod ("Hclose" with "[Hauth Hheap Hspec0 Htapes]") as "_".
     { iModIntro. rewrite /spec_inv.
       iExists _, _, _, 0. simpl.
-      iFrame. rewrite exec_O dret_1_1 //. }
+      iFrame. rewrite pexec_O dret_1_1 //. }
     iSpecialize ("Hwp" with "[$Hα $Hinv Hj]"); [eauto|].
     rewrite !wp_unfold /wp_pre /= He.
     iMod ("Hwp" $! _ with "[$Hh1 $Hspec $Ht1 $Herr]") as "Hwp".
@@ -323,7 +323,7 @@ Section rules.
     TCEq N (Z.to_nat z) →
     nclose specN ⊆ E →
     l ↪ₛ (N; n :: ns) -∗
-    refines_right K (rand #z from #lbl:l) ={E}=∗ refines_right K #n ∗ l ↪ₛ (N; ns).
+    refines_right K (rand(#lbl:l) #z ) ={E}=∗ refines_right K #n ∗ l ↪ₛ (N; ns).
   Proof.
     iIntros (??) "? (?&?)".
     iMod (step_rand with "[$]") as "(?&?&?)"; [done|].
diff --git a/theories/app_rel_logic/spec_tactics.v b/theories/app_rel_logic/spec_tactics.v
index ac2d87c1..aa43e265 100644
--- a/theories/app_rel_logic/spec_tactics.v
+++ b/theories/app_rel_logic/spec_tactics.v
@@ -3,10 +3,10 @@ From iris.base_logic.lib Require Import invariants.
 From iris.proofmode Require Import
      coq_tactics ltac_tactics
      reduction.
-From clutch.program_logic Require Import language ectx_language ectxi_language exec weakestpre lifting.
+From clutch.common Require Import language ectx_language ectxi_language.
 From clutch.prob_lang Require Import locations notation tactics metatheory lang
   class_instances.
-From clutch.app_rel_logic Require Import spec_ra spec_rules.
+From clutch.app_rel_logic Require Import spec_ra spec_rules lifting.
 Set Default Proof Using "Type".
 
 (** ** bind *)
@@ -345,7 +345,7 @@ Lemma tac_tp_rand `{app_clutchGS Σ} k Δ1 Δ2 E1 i1 i2 K' e e2 (l : loc) N z n
   TCEq N (Z.to_nat z) →
   nclose specN ⊆ E1 →
   envs_lookup_delete false i1 Δ1 = Some (false, refines_right k e, Δ2)%I →
-  e = fill K' (rand #z from #lbl:l) →
+  e = fill K' (rand(#lbl:l) #z) →
   envs_lookup i2 Δ2 = Some (false, l ↪ₛ (N; n::ns))%I →
   e2 = fill K' (of_val #n) →
   match envs_simple_replace i2 false
@@ -392,7 +392,7 @@ Tactic Notation "tp_rand" :=
 (*   to_val t = None → *)
 (*   nclose specN ⊆ E → *)
 (*   envs_lookup i1 Δ1 = Some (false, refines_right k e)%I → *)
-(*   e = fill K' (rand #z from #()) → *)
+(*   e = fill K' (rand #z) → *)
 (*   (forall (b : bool), exists e2, *)
 (*       e2 = fill K' (of_val #b) /\ *)
 (*       match envs_simple_replace i1 false *)
diff --git a/theories/typing/exec.v b/theories/common/exec.v
similarity index 100%
rename from theories/typing/exec.v
rename to theories/common/exec.v
diff --git a/theories/ctx_logic/spec_rules.v b/theories/ctx_logic/spec_rules.v
index fb4763db..ad872ff1 100644
--- a/theories/ctx_logic/spec_rules.v
+++ b/theories/ctx_logic/spec_rules.v
@@ -3,38 +3,9 @@ From stdpp Require Import namespaces.
 From iris.proofmode Require Import proofmode.
 From clutch.prelude Require Import stdpp_ext.
 From clutch.ctx_logic Require Import lifting ectx_lifting. 
-From clutch.prob_lang Require Import lang notation tactics metatheory.
+From clutch.prob_lang Require Import lang notation tactics metatheory exec_lang.
 From clutch.ctx_logic Require Export primitive_laws spec_ra. 
 
-Lemma exec_det_step_ctx K `{!LanguageCtx K} n ρ (e1 e2 : expr) σ1 σ2 :
-  prim_step e1 σ1 (e2, σ2) = 1%R →
-  pexec n ρ (K e1, σ1) = 1%R →
-  pexec (S n) ρ (K e2, σ2) = 1%R.
-Proof.
-  intros. eapply pexec_det_step; [|done].
-  rewrite -fill_step_prob //.
-  eapply (val_stuck _ σ1 (e2, σ2)).  
-  rewrite H. lra.
-Qed.
-
-Lemma exec_PureExec_ctx K `{!LanguageCtx K} (P : Prop) m n ρ (e e' : expr) σ :
-  P →
-  PureExec P n e e' →
-  pexec m ρ (K e, σ) = 1 →
-  pexec (m + n) ρ (K e', σ) = 1.
-Proof.
-  move=> HP /(_ HP).
-  destruct ρ as [e0 σ0].
-  revert e e' m. induction n=> e e' m.
-  { rewrite -plus_n_O. by inversion 1. }
-  intros (e'' & Hsteps & Hpstep)%nsteps_inv_r Hdet.
-  specialize (IHn _ _ m Hsteps Hdet).
-  rewrite -plus_n_Sm.
-  eapply exec_det_step_ctx; [done| |done].
-  apply Hpstep.
-Qed.
-
-
 Section rules.
   Context `{!clutchGS Σ}.
   Implicit Types P Q : iProp Σ.
diff --git a/theories/examples/app_rel/avoid_collision_rel.v b/theories/examples/app_rel/avoid_collision_rel.v
index 7bcb3c87..68db1e61 100644
--- a/theories/examples/app_rel/avoid_collision_rel.v
+++ b/theories/examples/app_rel/avoid_collision_rel.v
@@ -58,7 +58,7 @@ Section wp_refinement.
     (€ ε ∗
        refines_right [] (of_val #false))
       ⊢ WP
-      (let: "x" := rand #z from #() in "x" = #t)
+      (let: "x" := rand #z in "x" = #t)
       {{ v , ∃ v', ⤇ v' ∗ ⌜v = v'⌝ }}.
   Proof.
     iIntros (? Nε Nz) "(ε & #hs & hj)".
@@ -101,7 +101,7 @@ Section wp_refinement.
     (⊢ spec_ctx
      -∗ ⤇ (fill [] (of_val #false))
      -∗ € ε
-     -∗ WP (let: "x" := rand #z from #() in "x" = #t)
+     -∗ WP (let: "x" := rand #z in "x" = #t)
         {{ v , ∃ v', ⤇ v' ∗ ⌜v = v'⌝ }}).
   Proof.
     iIntros. iApply ref_no_coll_l ; eauto. iFrame. done.
@@ -116,15 +116,15 @@ Section opsem_refinement.
       ((1 / S N) = ε)%R →
       N = Z.to_nat z →
       ARcoupl
-        (lim_exec_val ((let: "x" := rand #z from #() in "x" = #t)%E, σ))
-        (lim_exec_val (Val #false, σ'))
+        (lim_exec ((let: "x" := rand #z in "x" = #t)%E, σ))
+        (lim_exec (Val #false, σ'))
         (λ v v' : val, v = v')
         ε.
   Proof.
     intros Npos Nε Nz.
     epose proof
       (wp_aRcoupl_lim _
-         (let: "x" := rand #z from #() in "x" = #t)%E
+         (let: "x" := rand #z in "x" = #t)%E
          #false σ σ' ε (λ v v', v = v')) as adequacy.
     assert (TCEq N (Z.to_nat z)) by by rewrite Nz.
     assert (TCEq (1 / S N)%R ε) by by rewrite Nε.
diff --git a/theories/examples/quicksort.v b/theories/examples/quicksort.v
index 6460b516..46cab625 100644
--- a/theories/examples/quicksort.v
+++ b/theories/examples/quicksort.v
@@ -31,7 +31,7 @@ Section quicksort.
     rec: "qs" "l" :=
       let: "n" := list_length "l" in
       if: "n" < #1 then "l" else
-        let: "ip" := rand ("n" - #1) from #() in
+        let: "ip" := rand ("n" - #1) in
         let, ("p", "r") := list_remove_nth_unsafe "l" "ip" in
         let, ("le", "gt") := partition "r" "p" in
         let, ("les", "gts") := ("qs" "le", "qs" "gt") in
diff --git a/theories/program_logic/generic_adequacy.v b/theories/generic/generic_adequacy.v
similarity index 81%
rename from theories/program_logic/generic_adequacy.v
rename to theories/generic/generic_adequacy.v
index 1347926a..27228949 100644
--- a/theories/program_logic/generic_adequacy.v
+++ b/theories/generic/generic_adequacy.v
@@ -1,10 +1,12 @@
 From iris.proofmode Require Import base proofmode.
-From iris.bi Require Export weakestpre fixpoint big_op.
+(* From iris.bi Require Export weakestpre fixpoint big_op. *)
 From iris.algebra Require Import auth excl.
 From iris.base_logic.lib Require Export ghost_map invariants fancy_updates.
 From clutch.prelude Require Import stdpp_ext iris_ext.
-From clutch.prob Require Import distribution.
-From clutch.program_logic Require Export language weakestpre generic_weakestpre.
+From clutch.prob Require Import distribution couplings.
+(* From clutch.bi Require Import weakestpre. *)
+From clutch.common Require Export language.
+From clutch.generic Require Export generic_weakestpre.
 From clutch.prob_lang Require Export class_instances.
 From clutch.prob_lang Require Import tactics lang notation erasure.
 From iris.prelude Require Import options.
@@ -63,20 +65,20 @@ Section adequacy.
   Lemma exec_ub_erasure (e : expr) (σ : state) (n : nat) φ  :
     to_val e = None →
     exec_mlift M e σ (λ '(e2, σ2),
-        |={∅}▷=>^(S n) ⌜ M.(mlift_funct)(exec_val n (e2, σ2)) φ ⌝)
-    ⊢ |={∅}▷=>^(S n) ⌜M.(mlift_funct) (exec_val (S n) (e, σ)) φ ⌝.
+        |={∅}▷=>^(S n) ⌜ M.(mlift_funct) (exec n (e2, σ2)) φ ⌝)
+    ⊢ |={∅}▷=>^(S n) ⌜M.(mlift_funct) (exec (S n) (e, σ)) φ ⌝.
   Proof.
     iIntros (Hv) "Hexec".
     iAssert (⌜to_val e = None⌝)%I as "-#H"; [done|]. iRevert "Hexec H".
     rewrite /exec_mlift /exec_mlift'.
     set (Φ := (λ '(e1, σ1),
                 (⌜to_val e1 = None⌝ ={∅}▷=∗^(S n)
-                 ⌜M.(mlift_funct) (exec_val (S n) (e1, σ1)) φ ⌝)%I) :
+                 ⌜M.(mlift_funct) (exec (S n) (e1, σ1)) φ ⌝)%I) :
            cfgO → iPropI Σ).
     assert (NonExpansive Φ).
     { intros m (?&?) (?&?) [[=] [=]]. by simplify_eq. }
     set (F := (exec_mlift_pre M (λ '(e2, σ2),
-                   |={∅}▷=>^(S n) ⌜M.(mlift_funct) (exec_val n (e2, σ2)) φ⌝)%I)).
+                   |={∅}▷=>^(S n) ⌜M.(mlift_funct) (exec n (e2, σ2)) φ⌝)%I)).
     iPoseProof (least_fixpoint_iter F Φ with "[]") as "H"; last first.
     { iIntros "Hfix %".
       by iMod ("H" $! ((_, _)) with "Hfix [//]").
@@ -84,20 +86,21 @@ Section adequacy.
     clear.
     iIntros "!#" ([e1 σ1]). rewrite /Φ/F/exec_mlift_pre.
     iIntros "[ (%R & %Hlift & H)| H] %Hv".
-    - rewrite exec_val_Sn_not_val; [|done].
+    - rewrite exec_Sn_not_final; [|eauto].
       iApply ub_lift_dbind'.
       + iPureIntro; apply Hlift.
       + iIntros ([] ?).
         by iMod ("H"  with "[//]").
-    - rewrite exec_val_Sn_not_val; [|done].
+    - rewrite exec_Sn_not_final; [|eauto].
       iDestruct (big_orL_mono _ (λ _ _,
                      |={∅}▷=>^(S n)
-                       ⌜M.(mlift_funct) (prim_step e1 σ1 ≫= exec_val n) φ ⌝)%I
+                       ⌜M.(mlift_funct) (prim_step e1 σ1 ≫= exec n) φ ⌝)%I
                   with "H") as "H".
       { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %Hlift & H)".
-        rewrite -exec_val_Sn_not_val; [|done].
+        replace (prim_step e1 σ1) with (step (e1, σ1)) by easy.
+        rewrite -exec_Sn_not_final ; [|eauto].
         iApply (step_fupdN_mono _ _ _
-                  (⌜∀ σ2 , R2 σ2 → M.(mlift_funct) (exec_val (S n) (e1, σ2)) φ ⌝)%I).
+                  (⌜∀ σ2 , R2 σ2 → M.(mlift_funct) (exec (S n) (e1, σ2)) φ ⌝)%I).
         - iIntros (?). iPureIntro.
           rewrite /= /get_active in Hα.
           apply elem_of_elements, elem_of_dom in Hα as [bs Hα].
@@ -110,14 +113,16 @@ Section adequacy.
       by iApply "IH".
   Qed.
 
+  Import generic_weakestpre.
+
   (* TODO: Fix notation to get rid of the mask *)
-  Theorem wp_refRcoupl_step_fupdN (e : expr) (σ : state) n φ  :
+  Theorem wp_refRcoupl_step_fupdN (e : expr prob_lang) (σ : state prob_lang) n φ  :
     state_interp σ ∗ WP e @ M ; ⊤ {{ v, ⌜φ v⌝ }} ⊢
-    |={⊤,∅}=> |={∅}▷=>^n ⌜M.(mlift_funct) (exec_val n (e, σ)) φ ⌝.
+    |={⊤,∅}=> |={∅}▷=>^n ⌜M.(mlift_funct) (exec n (e, σ)) φ ⌝.
   Proof.
     iInduction n as [|n] "IH" forall (e σ); iIntros "((Hσh & Hσt) & Hwp)".
     - rewrite /exec_val /=.
-      destruct (to_val e) eqn:Heq.
+      destruct (prob_lang.to_val e) eqn:Heq.
       + apply of_to_val in Heq as <-.
         rewrite mlift_wp_value_fupd.
         iMod (fupd_mask_subseteq _); [set_solver |].
@@ -128,15 +133,15 @@ Section adequacy.
       + iApply fupd_mask_intro; [set_solver|]; iIntros "_".
         iPureIntro.
         apply M.(mlift_dzero).
-    - rewrite exec_val_Sn /prim_step_or_val /=.
-      destruct (to_val e) eqn:Heq.
-      + apply of_to_val in Heq as <-.
+    - rewrite exec_Sn /step_or_final /=.
+      destruct (prob_lang.to_val e) eqn:Heq.
+      + apply prob_lang.of_to_val in Heq as <-.
         rewrite mlift_wp_value_fupd.
         iMod "Hwp" as "%".
         iApply fupd_mask_intro; [set_solver|]; iIntros "_".
         iApply step_fupdN_intro; [done|]. do 4 iModIntro.
         iPureIntro.
-        rewrite exec_val_unfold dret_id_left /=.
+        rewrite exec_unfold dret_id_left /=.
         apply M.(mlift_unit); auto.
       + rewrite mlift_wp_unfold /mlift_wp_pre /= Heq.
         iMod ("Hwp" with "[$]") as "(%Hexec_ub & Hlift)".
@@ -178,9 +183,11 @@ Definition clutchΣ : gFunctors :=
 Global Instance subG_clutchGPreS {Σ} : subG clutchΣ Σ → clutchGpreS Σ.
 Proof. solve_inG. Qed.
 
-Theorem wp_mlift Σ `{clutchGpreS Σ} (M : mlift) (e : expr) (σ : state) n φ :
+Import generic_weakestpre.
+
+Theorem wp_mlift Σ `{clutchGpreS Σ} (M : mlift) (e : expr prob_lang) (σ : state prob_lang) n φ :
   (∀ `{clutchGS Σ}, ⊢ WP e @ M ; ⊤ {{ v, ⌜φ v⌝ }}) →
-  M.(mlift_funct) (exec_val n (e, σ)) φ.
+  M.(mlift_funct) (exec n (e, σ)) φ.
 Proof.
   intros Hwp.
   eapply (step_fupdN_soundness_no_lc _ n 0).
diff --git a/theories/program_logic/generic_weakestpre.v b/theories/generic/generic_weakestpre.v
similarity index 99%
rename from theories/program_logic/generic_weakestpre.v
rename to theories/generic/generic_weakestpre.v
index 469322bf..faf506cc 100644
--- a/theories/program_logic/generic_weakestpre.v
+++ b/theories/generic/generic_weakestpre.v
@@ -6,7 +6,8 @@ From iris.prelude Require Import options.
 
 From clutch.prelude Require Import stdpp_ext NNRbar.
 From clutch.prob Require Export generic_lifting distribution.
-From clutch.program_logic Require Export exec language.
+From clutch.common Require Export exec language.
+From iris.bi Require Export weakestpre.
 
 Import uPred.
 
@@ -322,7 +323,6 @@ Section exec_mlift.
 End exec_mlift.
 
 
-
 (** * The weakest precondition  *)
 Definition mlift_wp_pre `{!irisGS Λ Σ} (M : mlift)
     (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
@@ -350,8 +350,7 @@ Qed.
 
 
 (* We use the extra argument to pass the mlift to the Wp *)
-Local Definition mlift_wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) mlift :=
-  λ (M : mlift), fixpoint (mlift_wp_pre M).
+Local Definition mlift_wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) mlift := λ M0, fixpoint (mlift_wp_pre M0).
 Local Definition mlift_wp_aux : seal (@mlift_wp_def). Proof. by eexists. Qed.
 Definition mlift_wp' := mlift_wp_aux.(unseal).
 Global Arguments mlift_wp' {Λ Σ _}.
diff --git a/theories/prob/markov.v b/theories/prob/markov.v
index 83144105..7cec2318 100644
--- a/theories/prob/markov.v
+++ b/theories/prob/markov.v
@@ -525,6 +525,64 @@ Section markov.
       apply (sup_is_upper_bound (λ m, exec m a b) n).
   Qed.
 
+  Lemma lim_exec_continuous_prob a ϕ r :
+    (∀ n, prob (exec n a) ϕ <= r) →
+    prob (lim_exec a) ϕ <= r.
+  Proof.
+    intro Hm.
+    rewrite /prob.
+    erewrite SeriesC_ext; last first.
+    { intro; rewrite lim_exec_unfold; auto. }
+    assert
+      (forall v, (if ϕ v then real (Sup_seq (λ n0 : nat, exec n0 a v)) else 0) =
+                 (real (Sup_seq (λ n0 : nat, if ϕ v then exec n0 a v else 0)))) as Haux.
+    { intro v.
+      destruct (ϕ v); auto.
+      rewrite sup_seq_const //.
+    }
+    assert
+      (is_finite (Sup_seq (λ n0 : nat, SeriesC (λ v, if ϕ v then exec n0 a v else 0)))) as Hfin.
+    {
+      apply (Rbar_le_sandwich 0 1).
+      + apply (Sup_seq_minor_le _ _ 0%nat); simpl.
+        apply SeriesC_ge_0'.
+        intro v; destruct (ϕ v); auto.
+        lra.
+      + apply upper_bound_ge_sup; intro; simpl; auto.
+        apply (Rle_trans _ (SeriesC (exec n a))); auto.
+        apply (SeriesC_le _ (exec n a)); auto.
+        intro v; destruct (ϕ v); real_solver.
+    }
+    erewrite SeriesC_ext; last first.
+    {
+      intro; rewrite Haux //.
+    }
+    erewrite (MCT_seriesC _ (λ n, SeriesC (λ v, if ϕ v then exec n a v else 0))
+                (Sup_seq (λ n0 : nat, SeriesC (λ v, if ϕ v then exec n0 a v else 0))));
+      auto.
+    - apply finite_rbar_le; auto.
+      apply upper_bound_ge_sup; auto.
+    - intros n v.
+      destruct (ϕ v); auto.
+      lra.
+    - intros n v.
+      destruct (ϕ v); [ apply exec_mono | lra].
+    - intro v; destruct (ϕ v); exists 1; intro; auto; lra.
+    - intros n.
+      apply SeriesC_correct; auto.
+      apply (ex_seriesC_le _ (exec n a)); auto.
+      intro v; destruct (ϕ v); real_solver.
+    - rewrite (Rbar_le_sandwich 0 1); auto.
+      + apply (Sup_seq_correct (λ n0 : nat, SeriesC (λ v, if ϕ v then exec n0 a v else 0))).
+      + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
+        apply SeriesC_ge_0'.
+        intro v; destruct (ϕ v); real_solver.
+      + apply upper_bound_ge_sup; intro; simpl; auto.
+        apply (Rle_trans _ (SeriesC (exec n a))); auto.
+        apply (SeriesC_le _ (exec n a)); auto.
+        intro v; destruct (ϕ v); real_solver.
+  Qed.
+
 End markov.
 
 #[global] Arguments pexec {_} _ _ : simpl never.
diff --git a/theories/prob_lang/class_instances.v b/theories/prob_lang/class_instances.v
index 51762c79..912f19ca 100644
--- a/theories/prob_lang/class_instances.v
+++ b/theories/prob_lang/class_instances.v
@@ -154,7 +154,7 @@ End pure_exec.
 
 (** * Instances of the [reducible] class *)
 
-Global Instance reducible_rand_no_tape (z : Z) σ : reducible (rand #z from #()) σ.
+Global Instance reducible_rand_no_tape (z : Z) σ : reducible (rand #z) σ.
 Proof.
   eapply head_prim_reducible ; eauto with head_step.
 Qed.
diff --git a/theories/prob_lang/erasure.v b/theories/prob_lang/erasure.v
index f3b4075a..a2bd68e1 100644
--- a/theories/prob_lang/erasure.v
+++ b/theories/prob_lang/erasure.v
@@ -416,10 +416,10 @@ Lemma ARcoupl_erasure e1 σ1 e1' σ1' α α' R Φ ε ε' m bs bs':
   σ1'.(tapes) !! α' = Some bs' →
   ARcoupl (state_step σ1 α) (state_step σ1' α') R ε →
   (∀ σ2 σ2', R σ2 σ2' →
-             ARcoupl (exec_val m (e1, σ2))
-               (lim_exec_val (e1', σ2')) Φ  ε' ) →
-  ARcoupl (exec_val m (e1, σ1))
-    (lim_exec_val (e1', σ1')) Φ (ε + ε').
+             ARcoupl (exec m (e1, σ2))
+               (lim_exec (e1', σ2')) Φ  ε' ) →
+  ARcoupl (exec m (e1, σ1))
+    (lim_exec (e1', σ1')) Φ (ε + ε').
 Proof.
   intros Hε Hε' Hα Hα' HR Hcont.
   rewrite -(Rplus_0_l (ε + ε')).
@@ -455,13 +455,13 @@ Lemma ARcoupl_erasure_r (e1 : expr) σ1 e1' σ1' α' R Φ ε ε' m bs':
   to_val e1 = None →
   σ1'.(tapes) !! α' = Some bs' →
   ARcoupl (prim_step e1 σ1) (state_step σ1' α') R ε →
-  (∀ e2 σ2 σ2', R (e2, σ2) σ2' → ARcoupl (exec_val m (e2, σ2)) (lim_exec_val (e1', σ2')) Φ ε' ) →
-  ARcoupl (exec_val (S m) (e1, σ1)) (lim_exec_val (e1', σ1')) Φ (ε + ε').
+  (∀ e2 σ2 σ2', R (e2, σ2) σ2' → ARcoupl (exec m (e2, σ2)) (lim_exec (e1', σ2')) Φ ε' ) →
+  ARcoupl (exec (S m) (e1, σ1)) (lim_exec (e1', σ1')) Φ (ε + ε').
 Proof.
   intros Hε Hε' He1 Hα' HR Hcont.
-  rewrite exec_val_Sn_not_val //.
+  rewrite exec_Sn_not_final; [|eauto].
   rewrite -(Rplus_0_r (ε + ε')).
-  eapply (ARcoupl_eq_trans_r _ (state_step σ1' α' ≫= (λ σ2', lim_exec_val (e1', σ2')))); try lra.
+  eapply (ARcoupl_eq_trans_r _ (state_step σ1' α' ≫= (λ σ2', lim_exec (e1', σ2')))); try lra.
   - eapply ARcoupl_dbind; try lra; auto; [| apply HR].
     intros [] ??. by apply Hcont.
   - eapply ARcoupl_from_eq_Rcoupl; [lra | ].
@@ -491,30 +491,30 @@ Lemma ARcoupl_erasure_l (e1 e1' : expr) σ1 σ1' α R Φ ε ε' m bs :
   0 <= ε' ->
   σ1.(tapes) !! α = Some bs →
   ARcoupl (state_step σ1 α) (prim_step e1' σ1') R ε →
-  (∀ σ2 e2' σ2', R σ2 (e2', σ2') → ARcoupl (exec_val m (e1, σ2)) (lim_exec_val (e2', σ2')) Φ ε') →
-  ARcoupl (exec_val m (e1, σ1)) (lim_exec_val (e1', σ1')) Φ (ε + ε').
+  (∀ σ2 e2' σ2', R σ2 (e2', σ2') → ARcoupl (exec m (e1, σ2)) (lim_exec (e2', σ2')) Φ ε') →
+  ARcoupl (exec m (e1, σ1)) (lim_exec (e1', σ1')) Φ (ε + ε').
 Proof.
   intros Hε Hε' Hα HR Hcont.
   destruct (to_val e1') eqn:Hval.
   - assert (prim_step e1' σ1' = dzero) as Hz by by apply val_stuck_dzero.
     rewrite /= (val_stuck_dzero e1') in HR; [|eauto].
     rewrite -(Rplus_0_l (ε + ε')).
-    eapply (ARcoupl_eq_trans_l _ (state_step σ1 α ≫= (λ σ2, exec_val m (e1, σ2)))); [lra| lra | | ].
+    eapply (ARcoupl_eq_trans_l _ (state_step σ1 α ≫= (λ σ2, exec m (e1, σ2)))); [lra| lra | | ].
     + apply ARcoupl_from_eq_Rcoupl; [lra |].
       by eapply prim_coupl_step_prim.
-    + rewrite lim_exec_val_prim_step.
-      rewrite prim_step_or_val_is_val //.
+    + rewrite lim_exec_step.
+      rewrite step_or_final_is_final; [|eauto].
       eapply ARcoupl_dbind; [lra|lra| | ]; last first.
       * rewrite -(Rplus_0_r ε).
         eapply ARcoupl_eq_trans_r; [lra|lra| | apply ARcoupl_dzero; lra ].
         eauto.
       * intros ? [] ?. by apply Hcont.
   - rewrite -(Rplus_0_l (ε + ε')).
-    eapply (ARcoupl_eq_trans_l _ (state_step σ1 α ≫= (λ σ2, exec_val m (e1, σ2)))); [lra| lra | | ].
+    eapply (ARcoupl_eq_trans_l _ (state_step σ1 α ≫= (λ σ2, exec m (e1, σ2)))); [lra| lra | | ].
     + apply ARcoupl_from_eq_Rcoupl; [lra |].
       by eapply prim_coupl_step_prim.
-    + rewrite lim_exec_val_prim_step.
-      rewrite prim_step_or_val_no_val //.
+    + rewrite lim_exec_step.
+      rewrite step_or_final_no_final; [|eauto].
       eapply ARcoupl_dbind; [lra|lra| | apply HR].
       intros ? [] ?. by apply Hcont.
 Qed.
diff --git a/theories/prob_lang/exec_lang.v b/theories/prob_lang/exec_lang.v
new file mode 100644
index 00000000..dd2b9fa4
--- /dev/null
+++ b/theories/prob_lang/exec_lang.v
@@ -0,0 +1,32 @@
+(* TODO move into metatheory.v ? *)
+
+From Coq Require Export Reals Psatz.
+From clutch.prob_lang Require Import lang.
+
+Lemma exec_det_step_ctx K `{!LanguageCtx K} n ρ (e1 e2 : expr) σ1 σ2 :
+  prim_step e1 σ1 (e2, σ2) = 1%R →
+  pexec n ρ (K e1, σ1) = 1%R →
+  pexec (S n) ρ (K e2, σ2) = 1%R.
+Proof.
+  intros. eapply pexec_det_step; [|done].
+  rewrite -fill_step_prob //.
+  eapply (val_stuck _ σ1 (e2, σ2)).
+  rewrite H. lra.
+Qed.
+
+Lemma exec_PureExec_ctx K `{!LanguageCtx K} (P : Prop) m n ρ (e e' : expr) σ :
+  P →
+  PureExec P n e e' →
+  pexec m ρ (K e, σ) = 1 →
+  pexec (m + n) ρ (K e', σ) = 1.
+Proof.
+  move=> HP /(_ HP).
+  destruct ρ as [e0 σ0].
+  revert e e' m. induction n=> e e' m.
+  { rewrite -plus_n_O. by inversion 1. }
+  intros (e'' & Hsteps & Hpstep)%nsteps_inv_r Hdet.
+  specialize (IHn _ _ m Hsteps Hdet).
+  rewrite -plus_n_Sm.
+  eapply exec_det_step_ctx; [done| |done].
+  apply Hpstep.
+Qed.
diff --git a/theories/prob_lang/metatheory.v b/theories/prob_lang/metatheory.v
index 7762955f..29be0aed 100644
--- a/theories/prob_lang/metatheory.v
+++ b/theories/prob_lang/metatheory.v
@@ -469,8 +469,8 @@ Lemma ARcoupl_rand_rand (N M : nat) z w σ1 σ1' (ε : nonnegreal) :
   N = Z.to_nat z →
   M = Z.to_nat w →
   ARcoupl
-    (prim_step (rand #z from #()) σ1)
-    (prim_step (rand #w from #()) σ1')
+    (prim_step (rand #z) σ1)
+    (prim_step (rand #w) σ1')
     (λ ρ2 ρ2', ∃ (n : fin (S N)) (m : fin (S M)),
         (fin_to_nat n = m) ∧
         ρ2 = (Val #n, σ1) ∧ ρ2' = (Val #m, σ1'))
@@ -500,8 +500,8 @@ Lemma ARcoupl_rand_rand_inj (N M : nat) f `{Inj (fin (S N)) (fin (S M)) (=) (=)
   N = Z.to_nat z →
   M = Z.to_nat w →
   ARcoupl
-    (prim_step (rand #z from #()) σ1)
-    (prim_step (rand #w from #()) σ1')
+    (prim_step (rand #z) σ1)
+    (prim_step (rand #w) σ1')
     (λ ρ2 ρ2', ∃ (n : fin (S N)),
         ρ2 = (Val #n, σ1) ∧ ρ2' = (Val #(f n), σ1'))
    ε.
@@ -531,8 +531,8 @@ Lemma ARcoupl_rand_rand_rev (N M : nat) z w σ1 σ1' (ε : nonnegreal) :
   N = Z.to_nat z →
   M = Z.to_nat w →
   ARcoupl
-    (prim_step (rand #z from #()) σ1)
-    (prim_step (rand #w from #()) σ1')
+    (prim_step (rand #z) σ1)
+    (prim_step (rand #w) σ1')
     (λ ρ2 ρ2', ∃ (n : fin (S N)) (m : fin (S M)),
         (fin_to_nat n = m) ∧
         ρ2 = (Val #n, σ1) ∧ ρ2' = (Val #m, σ1'))
@@ -563,8 +563,8 @@ Lemma ARcoupl_rand_rand_rev_inj (N M : nat) f `{Inj (fin (S M)) (fin (S N)) (=)
   N = Z.to_nat z →
   M = Z.to_nat w →
   ARcoupl
-    (prim_step (rand #z from #()) σ1)
-    (prim_step (rand #w from #()) σ1')
+    (prim_step (rand #z) σ1)
+    (prim_step (rand #w) σ1')
     (λ ρ2 ρ2', ∃ (m : fin (S M)),
         ρ2 = (Val #(f m), σ1) ∧ ρ2' = (Val #m, σ1'))
    ε.
@@ -652,7 +652,7 @@ Lemma ARcoupl_rand_r N z (ρ1 : cfg) σ1' :
   N = Z.to_nat z →
   ARcoupl
     (dret ρ1)
-    (prim_step (rand #z from #()) σ1')
+    (prim_step (rand #z) σ1')
     (λ ρ2 ρ2', ∃ (n : fin (S N)), ρ2 = ρ1 ∧ ρ2' = (Val #n, σ1')) (nnreal_zero).
 Proof.
   intros ?.
@@ -665,7 +665,7 @@ Lemma ARcoupl_rand_empty_r N z (ρ1 : cfg) σ1' α' :
   tapes σ1' !! α' = Some (N; []) →
   ARcoupl
     (dret ρ1)
-    (prim_step (rand #z from #lbl:α') σ1')
+    (prim_step (rand(#lbl:α') #z) σ1')
     (λ ρ2 ρ2', ∃ (n : fin (S N)), ρ2 = ρ1 ∧ ρ2' = (Val #n, σ1')) (nnreal_zero).
 Proof.
   intros ??.
@@ -679,7 +679,7 @@ Lemma ARcoupl_rand_wrong_r N M z ns (ρ1 : cfg) σ1' α' :
   tapes σ1' !! α' = Some (M; ns) →
   ARcoupl
     (dret ρ1)
-    (prim_step (rand #z from #lbl:α') σ1')
+    (prim_step (rand(#lbl:α') #z) σ1')
     (λ ρ2 ρ2', ∃ (n : fin (S N)), ρ2 = ρ1 ∧ ρ2' = (Val #n, σ1')) (nnreal_zero).
 Proof.
   intros ???.
@@ -692,7 +692,7 @@ Lemma wp_couple_rand_no_coll_l N z (σ : state) (ρₛ1 : cfg) (x : Fin.t (S N))
   ((1 / S N) = ε)%R →
   N = Z.to_nat z →
   ARcoupl
-    (prim_step (rand #z from #()) σ)
+    (prim_step (rand #z) σ)
     (dret ρₛ1)
     (λ ρ ρₛ2, ∃ n : fin (S N),
         ρ = (Val #n, σ) ∧ (n ≠ x) ∧ ρₛ2 = ρₛ1)
@@ -715,7 +715,7 @@ Lemma wp_couple_rand_no_coll_r N z (σₛ : state) (ρ1 : cfg) (x : Fin.t (S N))
   N = Z.to_nat z →
   ARcoupl
     (dret ρ1)
-    (prim_step (rand #z from #()) σₛ)
+    (prim_step (rand #z) σₛ)
     (λ ρ2 ρₛ, ∃ n : fin (S N),
         ρ2 = ρ1 ∧ ρₛ = (Val #n, σₛ) ∧ (n ≠ x))
     ε.
diff --git a/theories/program_logic/exec.v b/theories/program_logic/exec.v
deleted file mode 100644
index 7c418725..00000000
--- a/theories/program_logic/exec.v
+++ /dev/null
@@ -1,477 +0,0 @@
-From Coq Require Import Reals Psatz.
-From Coquelicot Require Import Rcomplements Rbar Lim_seq.
-From stdpp Require Import relations.
-From clutch.common Require Import language.
-From clutch.prob Require Import distribution couplings.
-
-(** Distribution for [n]-step partial evaluation *)
-Section exec.
-  Context {Λ : language}.
-  Implicit Types ρ : cfg Λ.
-  Implicit Types e : expr Λ.
-  Implicit Types σ : state Λ.
-
-  Definition prim_step_or_val (ρ : cfg Λ) : distr (cfg Λ) :=
-    match to_val ρ.1 with
-    | Some v => dret ρ
-    | None => prim_step ρ.1 ρ.2
-    end.
-
-  Lemma prim_step_or_val_no_val e σ :
-    to_val e = None → prim_step_or_val (e, σ) = prim_step e σ.
-  Proof. rewrite /prim_step_or_val /=. by intros ->. Qed.
-
-  Lemma prim_step_or_val_is_val e σ :
-    is_Some (to_val e) → prim_step_or_val (e, σ) = dret (e, σ).
-  Proof. rewrite /prim_step_or_val /=. by intros [? ->]. Qed.
-
-  Definition exec (n : nat) ρ : distr (cfg Λ) := iterM n prim_step_or_val ρ.
-
-  Lemma exec_O ρ :
-    exec 0 ρ = dret ρ.
-  Proof. done. Qed.
-
-  Lemma exec_Sn ρ n :
-    exec (S n) ρ = prim_step_or_val ρ ≫= exec n.
-  Proof. done. Qed.
-
-  Lemma exec_plus ρ n m :
-    exec (n + m) ρ = exec n ρ ≫= exec m.
-  Proof. rewrite /exec iterM_plus //.  Qed.
-
-  Lemma exec_1 :
-    exec 1 = prim_step_or_val.
-  Proof.
-    extensionality ρ; destruct ρ as [e σ].
-    rewrite exec_Sn /exec /= dret_id_right //.
-  Qed.
-
-  Lemma exec_Sn_r e σ n :
-    exec (S n) (e, σ) = exec n (e, σ) ≫= prim_step_or_val.
-  Proof.
-    assert (S n = n + 1)%nat as -> by lia.
-    rewrite exec_plus exec_1 //.
-  Qed.
-
-  Lemma exec_det_step n ρ e1 e2 σ1 σ2 :
-    prim_step e1 σ1 (e2, σ2) = 1 →
-    exec n ρ (e1, σ1) = 1 →
-    exec (S n) ρ (e2, σ2) = 1.
-  Proof.
-    destruct ρ as [e0 σ0].
-    rewrite exec_Sn_r.
-    intros H ->%pmf_1_eq_dret.
-    rewrite dret_id_left /=.
-    case_match; [|done].
-    assert (to_val e1 = None); [|simplify_eq].
-    eapply val_stuck. erewrite H. lra.
-  Qed.
-
-  Lemma exec_det_step_ctx K `{!LanguageCtx K} n ρ e1 e2 σ1 σ2 :
-    prim_step e1 σ1 (e2, σ2) = 1 →
-    exec n ρ (K e1, σ1) = 1 →
-    exec (S n) ρ (K e2, σ2) = 1.
-  Proof.
-    intros. eapply exec_det_step; [|done].
-    rewrite -fill_step_prob //.
-    eapply (val_stuck _ σ1 (e2, σ2)). lra.
-  Qed.
-
-  Lemma exec_PureExec_ctx K `{!LanguageCtx K} (P : Prop) m n ρ e e' σ :
-    P →
-    PureExec P n e e' →
-    exec m ρ (K e, σ) = 1 →
-    exec (m + n) ρ (K e', σ) = 1.
-  Proof.
-    move=> HP /(_ HP).
-    destruct ρ as [e0 σ0].
-    revert e e' m. induction n=> e e' m.
-    { rewrite -plus_n_O. by inversion 1. }
-    intros (e'' & Hsteps & Hpstep)%nsteps_inv_r Hdet.
-    specialize (IHn _ _ m Hsteps Hdet).
-    rewrite -plus_n_Sm.
-    eapply exec_det_step_ctx; [done| |done].
-    apply Hpstep.
-  Qed.
-
-End exec.
-
-Global Arguments exec {_} _ _ : simpl never.
-
-(** Distribution for evaluation ending in a value in less than [n]-step *)
-Section exec_val.
-  Context {Λ : language}.
-  Implicit Types ρ : cfg Λ.
-  Implicit Types e : expr Λ.
-  Implicit Types v : val Λ.
-  Implicit Types σ : state Λ.
-
-  Fixpoint exec_val (n : nat) (ρ : cfg Λ) {struct n} : distr (val Λ) :=
-    match to_val ρ.1, n with
-      | Some v, _ => dret v
-      | None, 0 => dzero
-      | None, S n => prim_step ρ.1 ρ.2 ≫= exec_val n
-    end.
-
-  Lemma exec_val_unfold (n : nat) :
-    exec_val n = λ ρ,
-      match to_val ρ.1, n with
-      | Some v, _ => dret v
-      | None, 0 => dzero
-      | None, S n => prim_step ρ.1 ρ.2 ≫= exec_val n
-      end.
-  Proof. by destruct n. Qed.
-
-  Lemma exec_val_is_val v e σ n :
-    to_val e = Some v → exec_val n (e, σ) = dret v.
-  Proof. destruct n; simpl; by intros ->. Qed.
-
-  Lemma exec_val_Sn (ρ : cfg Λ) (n: nat) :
-    exec_val (S n) ρ = prim_step_or_val ρ ≫= exec_val n.
-  Proof.
-    destruct ρ as [e σ].
-    rewrite /prim_step_or_val /=.
-    destruct (to_val e) eqn:Hv=>/=; [|done].
-    rewrite dret_id_left -/exec_val.
-    fold exec_val.
-    erewrite exec_val_is_val; eauto.
-  Qed.
-
-  Lemma exec_val_mon ρ n v :
-    exec_val n ρ v <= exec_val (S n) ρ v.
-  Proof.
-    apply refRcoupl_eq_elim.
-    move : ρ.
-    induction n.
-    - intros.
-      apply refRcoupl_from_leq.
-      intros w. rewrite /distr_le /=.
-      by case_match.
-    - intros; do 2 rewrite exec_val_Sn.
-      eapply refRcoupl_dbind; [|apply refRcoupl_eq_refl].
-      by intros ? ? ->.
-  Qed.
-
-  Lemma exec_val_mon' ρ n m v :
-    n ≤ m → exec_val n ρ v <= exec_val m ρ v.
-  Proof.
-    eapply (mon_succ_to_mon (λ x, exec_val x ρ v)); intro; apply exec_val_mon.
-  Qed.
-
-  Lemma exec_val_Sn_not_val e σ n :
-    to_val e = None →
-    exec_val (S n) (e, σ) = prim_step e σ ≫= exec_val n.
-  Proof. intros ?. rewrite exec_val_Sn prim_step_or_val_no_val //. Qed.
-
-  Lemma exec_exec_val_le n ρ v σ :
-    exec n ρ (of_val v, σ) <= exec_val n ρ v.
-  Proof.
-    revert ρ. induction n; intros [e σ'].
-    - rewrite exec_O.
-      destruct (decide ((e, σ') = (of_val v, σ))) as [[= -> ->]|].
-      + rewrite (exec_val_is_val v); [|auto using to_of_val].
-        rewrite !dret_1_1 //.
-      + rewrite dret_0 //.
-    - rewrite exec_Sn exec_val_Sn.
-      destruct (to_val e) as [w|] eqn:Heq.
-      + rewrite prim_step_or_val_is_val //.
-        rewrite 2!dret_id_left -/exec_val.
-        apply IHn.
-      + rewrite prim_step_or_val_no_val //.
-        rewrite /pmf /= /dbind_pmf.
-        eapply SeriesC_le.
-        * intros ρ. split.
-          { by apply Rmult_le_pos. }
-          apply Rmult_le_compat; by auto.
-        * eapply pmf_ex_seriesC_mult_fn.
-          exists 1. by intros ρ.
-  Qed.
-
-  Lemma exec_exec_val_det n ρ v σ :
-    exec n ρ (of_val v, σ) = 1 → exec_val n ρ v = 1.
-  Proof.
-    intros ?.
-    pose proof (exec_exec_val_le n ρ v σ).
-    pose proof (pmf_le_1 (exec_val n ρ) v).
-    lra.
-  Qed.
-
-  Lemma exec_exec_val_neq_le n m ρ v v' σ :
-    v ≠ v' → exec_val m ρ v' + exec n ρ (of_val v, σ) <= 1.
-  Proof.
-    intros Hneq.
-    eapply Rle_trans; [apply Rplus_le_compat_l, exec_exec_val_le | ].
-    eapply Rle_trans; [apply Rplus_le_compat_l,
-        (exec_val_mon' _ n (n `max` m)), Nat.le_max_l | ].
-    eapply Rle_trans; [apply Rplus_le_compat_r,
-        (exec_val_mon' _ m (n `max` m)), Nat.le_max_r | ].
-    eapply Rle_trans; [ | apply (pmf_SeriesC (exec_val (n `max` m) ρ)) ].
-    apply pmf_plus_neq_SeriesC; auto.
-  Qed.
-
-  Lemma exec_exec_val_det_neg n m ρ v v' σ :
-    exec n ρ (of_val v, σ) = 1 →
-    v ≠ v' →
-    exec_val m ρ v' = 0.
-  Proof.
-    intros Hexec Hv.
-    pose proof (exec_exec_val_neq_le n m ρ v v' σ Hv) as H.
-    rewrite Hexec in H.
-    pose proof (pmf_pos (exec_val m ρ) v').
-    lra.
-  Qed.
-
-End exec_val.
-
-(** Limit of [prim_exec]  *)
-Section prim_exec_lim.
-  Context {Λ : language}.
-  Implicit Types ρ : cfg Λ.
-  Implicit Types e : expr Λ.
-  Implicit Types v : val Λ.
-  Implicit Types σ : state Λ.
-
-  Definition lim_exec_val (ρ : cfg Λ) : distr (val Λ):=
-    lim_distr (λ n, exec_val n ρ) (exec_val_mon ρ).
-
-  Lemma lim_exec_val_rw (ρ : cfg Λ) v :
-    lim_exec_val ρ v = Sup_seq (λ n, (exec_val n ρ) v).
-  Proof.
-    rewrite lim_distr_pmf; auto.
-  Qed.
-
-  Lemma lim_exec_val_prim_step (ρ : cfg Λ) :
-    lim_exec_val ρ = prim_step_or_val ρ ≫= lim_exec_val.
-  Proof.
-   apply distr_ext.
-   intro v.
-   rewrite lim_exec_val_rw/=.
-   rewrite {2}/pmf/=/dbind_pmf.
-   setoid_rewrite lim_exec_val_rw.
-   assert
-     (SeriesC (λ a : cfg Λ, prim_step_or_val ρ a * Sup_seq (λ n : nat, exec_val n a v)) =
-     SeriesC (λ a : cfg Λ, Sup_seq (λ n : nat, prim_step_or_val ρ a * exec_val n a v))) as ->.
-   { apply SeriesC_ext; intro v'.
-     apply eq_rbar_finite.
-     rewrite rmult_finite.
-     rewrite (rbar_finite_real_eq (Sup_seq (λ n : nat, exec_val n v' v))); auto.
-     - rewrite <- (Sup_seq_scal_l (prim_step_or_val ρ v') (λ n : nat, exec_val n v' v)); auto.
-     - apply (Rbar_le_sandwich 0 1).
-       + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-       + apply upper_bound_ge_sup; intro; simpl; auto.
-   }
-   rewrite (MCT_seriesC _ (λ n, exec_val (S n) ρ v) (lim_exec_val ρ v)); auto.
-   - intros; apply Rmult_le_pos; auto.
-   - intros.
-     apply Rmult_le_compat; auto; [apply Rle_refl | apply exec_val_mon]; auto.
-   - intro.
-     exists (prim_step_or_val ρ a); intro.
-     rewrite <- Rmult_1_r.
-     apply Rmult_le_compat_l; auto.
-   - intro n.
-     rewrite exec_val_Sn.
-     rewrite {3}/pmf/=/dbind_pmf.
-     apply SeriesC_correct; auto.
-     apply (ex_seriesC_le _ (prim_step_or_val ρ)); auto.
-     intro; split; auto.
-     + apply Rmult_le_pos; auto.
-     + rewrite <- Rmult_1_r.
-       apply Rmult_le_compat_l; auto.
-   - rewrite lim_exec_val_rw.
-     rewrite mon_sup_succ.
-     + rewrite (Rbar_le_sandwich 0 1); auto.
-       * apply (Sup_seq_correct (λ n : nat, exec_val (S n) ρ v)).
-       * apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-       * apply upper_bound_ge_sup; intro; simpl; auto.
-     + intro; apply exec_val_mon.
-  Qed.
-
-  Lemma lim_exec_val_exec n (ρ : cfg Λ) :
-    lim_exec_val ρ = exec n ρ ≫= lim_exec_val.
-  Proof.
-    move : ρ.
-    induction n; intro ρ.
-    - rewrite exec_O.
-      rewrite dret_id_left; auto.
-    - rewrite exec_Sn -dbind_assoc/=.
-      rewrite lim_exec_val_prim_step.
-      apply dbind_eq; [|done].
-      intros ??. apply IHn.
-  Qed.
-
-  Lemma lim_exec_val_exec_det n ρ (v : val Λ) σ :
-    exec n ρ (of_val v, σ) = 1 →
-    lim_exec_val ρ = dret v.
-  Proof.
-    intro Hv.
-    apply distr_ext.
-    intro v'.
-    rewrite lim_exec_val_rw.
-    rewrite {2}/pmf/=/dret_pmf.
-    assert (is_finite (Sup_seq (λ n, exec_val n ρ v'))) as Haux.
-    {
-      apply (Rbar_le_sandwich 0 1).
-      + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-      + apply upper_bound_ge_sup; intro; simpl; auto.
-    }
-    case_bool_decide; simplify_eq.
-    - apply Rle_antisym.
-      + apply finite_rbar_le; auto.
-        apply upper_bound_ge_sup.
-        intro; simpl; auto.
-      + apply rbar_le_finite; auto.
-        apply (Sup_seq_minor_le _ _ n); simpl; auto.
-        destruct ρ as (e2 & σ2).
-        eapply exec_exec_val_det in Hv.
-        rewrite Hv //.
-    - rewrite -(sup_seq_const 0).
-      f_equal. apply Sup_seq_ext=> m.
-      f_equal. by eapply exec_exec_val_det_neg.
-  Qed.
-
-  Lemma lim_exec_val_continous ρ1 v r :
-    (∀ n, exec_val n ρ1 v <= r) → lim_exec_val ρ1 v <= r.
-  Proof.
-    intro Hexec.
-    rewrite lim_exec_val_rw.
-    assert (is_finite (Sup_seq (λ n : nat, exec_val n ρ1 v))) as Haux.
-    {
-      apply (Rbar_le_sandwich 0 1); auto.
-      + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-      + apply upper_bound_ge_sup; intro; simpl; auto.
-    }
-    apply finite_rbar_le; auto.
-    apply upper_bound_ge_sup.
-    intro; simpl; auto.
-  Qed.
-
-Lemma lim_exec_positive_ast n ρ :
-  SeriesC (exec_val n ρ) = 1 →
-  lim_exec_val ρ = exec_val n ρ.
-Proof.
-    intro Hv.
-    apply distr_ext.
-    intro v.
-    rewrite lim_exec_val_rw.
-    assert (is_finite (Sup_seq (λ n, exec_val n ρ v))) as Haux.
-    {
-      apply (Rbar_le_sandwich 0 1).
-      + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-      + apply upper_bound_ge_sup; intro; simpl; auto.
-    }
-    assert (forall m, (n <= m)%nat -> exec_val m ρ v = exec_val n ρ v ) as Haux2.
-    {
-      intros m Hleq.
-      apply Rle_antisym; [ | apply exec_val_mon'; auto ].
-      destruct (decide (exec_val m ρ v <= exec_val n ρ v)) as [Hdec | Hdec]; auto.
-      apply Rnot_le_lt in Hdec.
-      exfalso.
-      assert (1 < SeriesC (exec_val m ρ)); last first.
-      - assert (SeriesC (exec_val m ρ) <= 1); auto; lra.
-      - rewrite <- Hv.
-        apply SeriesC_lt; eauto.
-        intro v'; split; [ | apply exec_val_mon']; auto.
-    }
-    apply Rle_antisym.
-    - apply finite_rbar_le; auto.
-      (* Why does pmf unfold here? *)
-      rewrite -/pmf.
-      apply upper_bound_ge_sup; intro n'.
-      destruct (decide (n <= n')) as [Hdec | Hdec].
-      + right. apply Haux2.
-        apply INR_le; auto.
-      + apply exec_val_mon'.
-        apply Rnot_le_lt in Hdec.
-        apply INR_le.
-        auto with arith.
-        left; auto.
-    - apply rbar_le_finite; auto.
-      (* It seems Coq cannot infer the first argument because of the order in which the n0 is used *)
-      apply (sup_is_upper_bound (λ n0 : nat, exec_val n0 ρ v) n).
-Qed.
-
-Lemma lim_exec_continous_mass a r :
-    (∀ n, SeriesC (exec_val n a) <= r) →
-    SeriesC (lim_exec_val a) <= r.
-Proof.
-  intro Hm.
-  erewrite SeriesC_ext; last first.
-  { intro; rewrite lim_exec_val_rw; auto. }
-  assert (is_finite (Sup_seq (λ n : nat, SeriesC (exec_val n a)))) as Haux.
-  {
-    apply (Rbar_le_sandwich 0 1).
-    + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-    + apply upper_bound_ge_sup; intro; simpl; auto.
-  }
-  erewrite (MCT_seriesC _ (λ n, SeriesC (exec_val n a)) (Sup_seq (λ n : nat, SeriesC (exec_val n a)))); auto.
-  - apply finite_rbar_le; auto.
-    apply upper_bound_ge_sup; auto.
-  - apply exec_val_mon.
-  - intro; exists 1; intro; auto.
-  - intros.
-    apply SeriesC_correct; auto.
-  - rewrite (Rbar_le_sandwich 0 1); auto.
-    + apply (Sup_seq_correct (λ n : nat, SeriesC (exec_val n a))).
-    + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-    + apply upper_bound_ge_sup; intro; simpl; auto.
-Qed.
-
-Lemma lim_exec_continous_prob a ϕ r :
-    (∀ n, prob (exec_val n a) ϕ <= r) →
-    prob (lim_exec_val a) ϕ <= r.
-Proof.
-  intro Hm.
-  rewrite /prob.
-  erewrite SeriesC_ext; last first.
-  { intro; rewrite lim_exec_val_rw; auto. }
-  assert
-    (forall v, (if ϕ v then real (Sup_seq (λ n0 : nat, exec_val n0 a v)) else 0) =
-          (real (Sup_seq (λ n0 : nat, if ϕ v then exec_val n0 a v else 0)))) as Haux.
-  { intro v.
-    destruct (ϕ v); auto.
-    rewrite sup_seq_const //.
-  }
-  assert
-    (is_finite (Sup_seq (λ n0 : nat, SeriesC (λ v, if ϕ v then exec_val n0 a v else 0)))) as Hfin.
-  {
-    apply (Rbar_le_sandwich 0 1).
-    + apply (Sup_seq_minor_le _ _ 0%nat); simpl.
-      apply SeriesC_ge_0'.
-      intro v; destruct (ϕ v); auto.
-      lra.
-    + apply upper_bound_ge_sup; intro; simpl; auto.
-      apply (Rle_trans _ (SeriesC (exec_val n a))); auto.
-      apply (SeriesC_le _ (exec_val n a)); auto.
-      intro v; destruct (ϕ v); real_solver.
-  }
-  erewrite SeriesC_ext; last first.
-  {
-    intro; rewrite Haux //.
-  }
-  erewrite (MCT_seriesC _ (λ n, SeriesC (λ v, if ϕ v then exec_val n a v else 0))
-              (Sup_seq (λ n0 : nat, SeriesC (λ v, if ϕ v then exec_val n0 a v else 0))));
-    auto.
-  - apply finite_rbar_le; auto.
-    apply upper_bound_ge_sup; auto.
-  - intros n v.
-    destruct (ϕ v); auto.
-    lra.
-  - intros n v.
-    destruct (ϕ v); [ apply exec_val_mon | lra].
-  - intro v; destruct (ϕ v); exists 1; intro; auto; lra.
-  - intros n.
-    apply SeriesC_correct; auto.
-    apply (ex_seriesC_le _ (exec_val n a)); auto.
-    intro v; destruct (ϕ v); real_solver.
-  - rewrite (Rbar_le_sandwich 0 1); auto.
-    + apply (Sup_seq_correct (λ n0 : nat, SeriesC (λ v, if ϕ v then exec_val n0 a v else 0))).
-    + apply (Sup_seq_minor_le _ _ 0%nat); simpl; auto.
-      apply SeriesC_ge_0'.
-      intro v; destruct (ϕ v); real_solver.
-    + apply upper_bound_ge_sup; intro; simpl; auto.
-      apply (Rle_trans _ (SeriesC (exec_val n a))); auto.
-      apply (SeriesC_le _ (exec_val n a)); auto.
-      intro v; destruct (ϕ v); real_solver.
-Qed.
-
-End prim_exec_lim.
diff --git a/theories/tpref_logic/lifting.v b/theories/tpref_logic/lifting.v
index 50fa43cf..a8c5c59d 100644
--- a/theories/tpref_logic/lifting.v
+++ b/theories/tpref_logic/lifting.v
@@ -32,7 +32,7 @@ Proof.
   iIntros (σ1 a1) "[Hσ1 Ha1]".
   iMod ("H" with "[$]") as "[%Hred H]".
   iModIntro.
-  iApply rwp_coupl_prim_step_l; [done| |].
+  iApply rwp_coupl_prim_step_l.
   { eapply Rcoupl_pos_R, Rcoupl_trivial.
     - apply prim_step_mass. eauto.
     - apply dret_mass. }
@@ -100,7 +100,6 @@ Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
   iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
   iApply rwp_lift_pure_det_step.
-  - intros σ. specialize (Hsafe σ). eauto using reducible_not_val.
   - intros σ1 e2' σ2 Hpstep.
     by injection (pmf_1_supp_eq _ _ _ (pure_step_det σ1) Hpstep).
   - by iApply "IH".
@@ -201,7 +200,7 @@ Lemma rswp_lift_pure_det_step e1 e2 k E E' Φ a :
   (∀ σ1 e2' σ2 , prim_step e1 σ1 (e2', σ2) > 0%R → σ2 = σ1 ∧ e2' = e2) →
   (|={E}[E']▷=>^k WP e2 @ a; E {{ Φ }}) ⊢ RSWP e1 at k @ a; E ⟨⟨ Φ ⟩⟩.
 Proof.
-  iIntros (? Hpuredet) "H". iApply (rswp_lift_pure_step k E); [done| |].
+  iIntros (? Hpuredet) "H". iApply (rswp_lift_pure_step k E).
   { naive_solver. }
   iModIntro. iApply (step_fupdN_wand with "H"); iIntros "H".
   by iIntros (e' σ [_ ->]%Hpuredet).
diff --git a/theories/tpref_logic/primitive_laws.v b/theories/tpref_logic/primitive_laws.v
index 9d5ae5f8..4a51440e 100644
--- a/theories/tpref_logic/primitive_laws.v
+++ b/theories/tpref_logic/primitive_laws.v
@@ -118,8 +118,6 @@ Section rwp.
     iApply rswp_lift_atomic_head_step.
     iIntros (σ1) "Hσ !#".
     iSplit; [eauto with head_step|].
-    Unshelve.
-    2 : { apply 0%fin . }
     iIntros "!>" (e2 σ2 Hs).
     inv_head_step.
     iFrame.
@@ -166,9 +164,7 @@ Section rwp.
     iApply rswp_lift_atomic_head_step.
     iIntros (σ1) "(Hh & Ht) !#".
     iDestruct (ghost_map_lookup with "Ht Hl") as %?.
-    iSplit; [by eauto with head_step|].
-    Unshelve.
-    2 : { apply 0%fin. }
+    iSplit ; [by eauto with head_step|].
     iIntros "!>" (e2 σ2 Hs).
     inv_head_step.
     iFrame.
@@ -185,8 +181,6 @@ Section rwp.
     iIntros (σ1) "(Hh & Ht) !#".
     iDestruct (ghost_map_lookup with "Ht Hl") as %?.
     iSplit; [by eauto with head_step|].
-    Unshelve.
-    2 : { apply 0%fin. }
     iIntros "!>" (e2 σ2 Hs).
     inv_head_step.
     iFrame.
@@ -286,7 +280,6 @@ Section coupl.
       apply head_step_support_equiv_rel.
       by eapply (RandNoTapeS _ _ 0%fin). }
     iApply (rwp_coupl_steps (λ '(e2, σ2) a2, ∃ (n : fin _), e2 = Val #n ∧ σ2 = σ1 ∧ R n a2)).
-    { by apply head_prim_reducible. }
     { rewrite /= head_prim_step_eq //=.
       rewrite -(dret_id_right (step _)).
       eapply Rcoupl_dbind; [|done].
diff --git a/theories/tpref_logic/weakestpre.v b/theories/tpref_logic/weakestpre.v
index 231bdfb5..2b8d597c 100644
--- a/theories/tpref_logic/weakestpre.v
+++ b/theories/tpref_logic/weakestpre.v
@@ -727,7 +727,7 @@ Proof.
   rewrite rswp_unfold rwp_unfold /rwp_pre /rswp_step.
   iIntros (->) "Hswp". iIntros (σ1 m) "[Ha Hσ]".
   iMod ("Hswp" with "[$]") as "(% & % & % & Hswp)". iModIntro.
-  iApply rwp_coupl_prim_step_l; [done|done|].
+  iApply rwp_coupl_prim_step_l; [done|].
   iIntros ([e2 σ2] HR) "!>".
   by iMod ("Hswp" with "[//]").
 Qed.
@@ -744,7 +744,7 @@ Proof.
   iApply rwp_coupl_det_r; [done|].
   iApply (step_fupdN_mono with "Hswp").
   iIntros "(% & % & % & H)".
-  iApply rwp_coupl_prim_step_l; [done|done|].
+  iApply rwp_coupl_prim_step_l; [done|].
   iIntros ([e2 σ2] HR) "!>".
   by iMod ("H" with "[//]").
 Qed.
diff --git a/theories/typing/contextual_refinement_alt.v b/theories/typing/contextual_refinement_alt.v
index dc01b45e..8b6000c5 100644
--- a/theories/typing/contextual_refinement_alt.v
+++ b/theories/typing/contextual_refinement_alt.v
@@ -1,8 +1,8 @@
 From Coq Require Import Reals Psatz.
 From Coquelicot Require Import Rcomplements Rbar Lim_seq.
-From clutch.common Require Import language ectx_language.
+From clutch.common Require Import language ectx_language exec.
 From clutch.prob_lang Require Import lang notation metatheory.
-From clutch.typing Require Import types exec contextual_refinement.
+From clutch.typing Require Import types contextual_refinement.
 From clutch.prob Require Import distribution.
 
 (** Alternative formulation of contextual refinement without restricting to
@@ -183,7 +183,7 @@ Proof.
   rewrite lim_exec_val_rw.
   rewrite mon_sup_succ.
   - erewrite <-sup_seq_const. do 2 f_equal. apply functional_extensionality_dep.
-    intros n. simpl. rewrite head_prim_step_eq => /=.
+    intros n. simpl. erewrite head_prim_step_eq => /=.
     2: { eexists (_, _). destruct b;
         eapply head_step_support_equiv_rel;
         by econstructor.
@@ -205,7 +205,7 @@ Proof.
   - simpl. destruct H.
     apply of_to_val in H as H1. rewrite -H1. rewrite -H1 in H0.
     clear H H1.
-    destruct x eqn:H2; rewrite head_prim_step_eq.
+    destruct x eqn:H2; erewrite head_prim_step_eq.
     + destruct b, l => /=; try (rewrite dret_id_left; destruct n => /=; done).
       all: rewrite bool_decide_eq_false_2;[rewrite dret_id_left; by destruct n|].
       all: intro; apply H0; by rewrite H.
@@ -280,9 +280,7 @@ Proof.
   destruct n.
   - simpl. destruct x; auto.
   - rewrite /loop. simpl. rewrite head_prim_step_eq; last first.
-    + eexists _. erewrite det_head_step_singleton; [|by econstructor]. simpl.
-      rewrite dret_1_1; [|done]. lra.
-    + simpl. rewrite dret_id_left -/exec_val. apply Hn. lia.
+    simpl. rewrite dret_id_left -/exec_val. apply Hn. lia.
 Qed.
 
 Lemma lim_exec_val_of_val_true_one (e : expr) σ :
@@ -294,8 +292,7 @@ intros ->.
   rewrite mon_sup_succ.
   - erewrite <-sup_seq_const. do 2 f_equal. apply functional_extensionality_dep.
     intros n. simpl. rewrite head_prim_step_eq => /=.
-    + rewrite dret_id_left; destruct n => /=; by rewrite dret_1_1.
-    + eexists (_, _). eapply head_step_support_equiv_rel; by econstructor.
+    rewrite dret_id_left; destruct n => /=; by rewrite dret_1_1.
   - intro. apply exec_val_mon.
 Qed.
 
@@ -317,8 +314,7 @@ Proof.
     { destruct l.
       2: { destruct b; [exfalso; by apply H0|].
            rewrite head_prim_step_eq => /=; last first.
-           + eexists (_, _). eapply head_step_support_equiv_rel; by econstructor.
-           + rewrite dret_id_left -/ exec_val. rewrite loop_zero_mass //. }
+           rewrite dret_id_left -/ exec_val. rewrite loop_zero_mass //. }
       all: replace (_≫=_) with (dzero ≫= exec_val (Λ := prob_lang) n); [by rewrite dbind_dzero|f_equal].
       all: apply distr_ext => s; replace (dzero s) with 0 by done.
       all: rewrite /prim_step => /=; rewrite decomp_unfold => /=.
@@ -389,13 +385,7 @@ Proof.
          { destruct l.
            2: { destruct b;
                 rewrite head_prim_step_eq => /=; last first.
-                + eexists (_, _).
-                  eapply head_step_support_equiv_rel;
-                    by econstructor.
                 + rewrite dret_id_left -/ exec_val. rewrite loop_zero_mass. f_equal.
-                + eexists (_, _).
-                  eapply head_step_support_equiv_rel;
-                    by econstructor.
                 + rewrite dret_id_left -/ exec_val.
                   destruct n => /=; f_equal; by apply dret_0.
            }
diff --git a/theories/ub_logic/adequacy.v b/theories/ub_logic/adequacy.v
index e9d934ec..d81ca8b6 100644
--- a/theories/ub_logic/adequacy.v
+++ b/theories/ub_logic/adequacy.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 
 From clutch.prelude Require Import stdpp_ext iris_ext.
 From clutch.prob_lang Require Import erasure notation.
-From clutch.program_logic Require Export language weakestpre.
+From clutch.common Require Export language.
 From clutch.ub_logic Require Import error_credits ub_weakestpre primitive_laws.
 From clutch.prob Require Import distribution.
 Import uPred.
@@ -49,20 +49,20 @@ Section adequacy.
   Lemma exec_ub_erasure (e : expr) (σ : state) (n : nat) φ (ε : nonnegreal) :
     to_val e = None →
     exec_ub e σ (λ ε' '(e2, σ2),
-        |={∅}▷=>^(S n) ⌜ub_lift (exec_val n (e2, σ2)) φ ε'⌝) ε
-    ⊢ |={∅}▷=>^(S n) ⌜ub_lift (exec_val (S n) (e, σ)) φ ε⌝.
+        |={∅}▷=>^(S n) ⌜ub_lift (exec n (e2, σ2)) φ ε'⌝) ε
+    ⊢ |={∅}▷=>^(S n) ⌜ub_lift (exec (S n) (e, σ)) φ ε⌝.
   Proof.
     iIntros (Hv) "Hexec".
     iAssert (⌜to_val e = None⌝)%I as "-#H"; [done|]. iRevert "Hexec H".
     rewrite /exec_ub /exec_ub'.
     set (Φ := (λ '(ε'', (e1, σ1)),
                 (⌜to_val e1 = None⌝ ={∅}▷=∗^(S n)
-                 ⌜ub_lift (exec_val (S n) (e1, σ1)) φ ε''⌝)%I) :
+                 ⌜ub_lift (exec (S n) (e1, σ1)) φ ε''⌝)%I) :
            prodO NNRO cfgO → iPropI Σ).
     assert (NonExpansive Φ).
     { intros m (?&(?&?)) (?&(?&?)) [[=] [[=] [=]]]. by simplify_eq. }
     set (F := (exec_ub_pre (λ ε' '(e2, σ2),
-                   |={∅}▷=>^(S n) ⌜ub_lift (exec_val n (e2, σ2)) φ ε'⌝)%I)).
+                   |={∅}▷=>^(S n) ⌜ub_lift (exec n (e2, σ2)) φ ε'⌝)%I)).
     iPoseProof (least_fixpoint_iter F Φ with "[]") as "H"; last first.
     { iIntros "Hfix %".
       by iMod ("H" $! ((_, _)) with "Hfix [//]").
@@ -73,7 +73,7 @@ Section adequacy.
     - iApply step_fupdN_mono.
       { apply pure_mono.
         eapply UB_mon_grading; eauto. }
-      rewrite exec_val_Sn_not_val; [|done].
+      rewrite exec_Sn_not_final; [|eauto].
       iApply ub_lift_dbind'.
       1,2 : iPureIntro; apply cond_nonneg.
       + done.
@@ -82,26 +82,27 @@ Section adequacy.
     - iApply step_fupdN_mono.
       { apply pure_mono.
         eapply UB_mon_grading; eauto. }
-      rewrite exec_val_Sn_not_val; [|done].
+      rewrite exec_Sn_not_final; [|eauto].
       iApply ub_lift_dbind_adv'.
       + iPureIntro; apply cond_nonneg.
       + iPureIntro. exists r. split; auto. apply cond_nonneg.
       + done.
       + iIntros ([] ?).
         by iMod ("H"  with "[//]").
-    - rewrite exec_val_Sn_not_val; [|done].
+    - rewrite exec_Sn_not_final; [|eauto].
       iDestruct (big_orL_mono _ (λ _ _,
                      |={∅}▷=>^(S n)
-                       ⌜ub_lift (prim_step e1 σ1 ≫= exec_val n) φ ε''⌝)%I
+                       ⌜ub_lift (prim_step e1 σ1 ≫= exec n) φ ε''⌝)%I
                   with "H") as "H".
       { iIntros (i α Hα%elem_of_list_lookup_2) "(% & %ε1 & %ε2 & %Hleq & %Hlift & H)".
-        rewrite -exec_val_Sn_not_val; [|done].
+        replace (prim_step e1 σ1) with (step (e1, σ1)) => //.
+        rewrite -exec_Sn_not_final; [|eauto].
         iApply (step_fupdN_mono _ _ _
-                  (⌜∀ σ2 , R2 σ2 → ub_lift (exec_val (S n) (e1, σ2)) φ ε2 ⌝)%I).
+                  (⌜∀ σ2 , R2 σ2 → ub_lift (exec (S n) (e1, σ2)) φ ε2 ⌝)%I).
         - iIntros (?). iPureIntro.
           rewrite /= /get_active in Hα.
           apply elem_of_elements, elem_of_dom in Hα as [bs Hα].
-          apply (UB_mon_grading _ _ (ε1 + ε2)); [lra | ].
+          apply (UB_mon_grading _ _ (ε1 + ε2)) => //.
           erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim _ _ _ _ _ Hα)); eauto.
           eapply ub_lift_dbind; eauto; [apply cond_nonneg | ].
           apply cond_nonneg.
@@ -114,10 +115,10 @@ Section adequacy.
 
   Theorem wp_refRcoupl_step_fupdN (e : expr) (σ : state) (ε : nonnegreal) n φ  :
     state_interp σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
-    |={⊤,∅}=> |={∅}▷=>^n ⌜ub_lift (exec_val n (e, σ)) φ ε⌝.
+    |={⊤,∅}=> |={∅}▷=>^n ⌜ub_lift (exec n (e, σ)) φ ε⌝.
   Proof.
     iInduction n as [|n] "IH" forall (e σ ε); iIntros "((Hσh & Hσt) & Hε & Hwp)".
-    - rewrite /exec_val /=.
+    - rewrite /exec /=.
       destruct (to_val e) eqn:Heq.
       + apply of_to_val in Heq as <-.
         rewrite ub_wp_value_fupd.
@@ -131,7 +132,7 @@ Section adequacy.
         apply ub_lift_dzero,
         Rle_ge,
         cond_nonneg.
-    - rewrite exec_val_Sn /prim_step_or_val /=.
+    - rewrite exec_Sn /step_or_final /=.
       destruct (to_val e) eqn:Heq.
       + apply of_to_val in Heq as <-.
         rewrite ub_wp_value_fupd.
@@ -139,7 +140,7 @@ Section adequacy.
         iApply fupd_mask_intro; [set_solver|]; iIntros "_".
         iApply step_fupdN_intro; [done|]. do 4 iModIntro.
         iPureIntro.
-        rewrite exec_val_unfold dret_id_left /=.
+        rewrite exec_unfold dret_id_left /=.
         apply (UB_mon_grading _ _ 0); [apply cond_nonneg | ].
         apply ub_lift_dret; auto.
       + rewrite ub_wp_unfold /ub_wp_pre /= Heq.
@@ -147,16 +148,18 @@ Section adequacy.
         iModIntro.
         iPoseProof
           (exec_ub_mono _ (λ ε' '(e2, σ2), |={∅}▷=>^(S n)
-             ⌜ub_lift (exec_val n (e2, σ2)) φ ε'⌝)%I
+             ⌜ub_lift (exec n (e2, σ2)) φ ε'⌝)%I
             with "[%] [] Hlift") as "H".
         { apply Rle_refl. }
         { iIntros (? []) "H !> !>".
           iMod "H" as "(Hstate & Herr_auth & Hwp)".
           iMod ("IH" with "[$]") as "H".
           iModIntro. done. }
-        rewrite -exec_val_Sn_not_val; [|done].
+        assert ((prim_step e σ) = (step (e, σ))) as h => //.
+        rewrite h. clear h.
+        rewrite -exec_Sn_not_final; [|eauto].
         iAssert
-          (|={∅}▷=> |={∅}▷=>^n ⌜ub_lift (exec_val (S n) (e, σ)) φ ε⌝)%I
+          (|={∅}▷=> |={∅}▷=>^n ⌜ub_lift (exec (S n) (e, σ)) φ ε⌝)%I
           with "[H]" as "Haux"; last first.
         {  iMod "Haux".
            do 2 iModIntro.
@@ -187,7 +190,7 @@ Proof. solve_inG. Qed.
 
 Theorem wp_union_bound Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) n (ε : nonnegreal) φ :
   (∀ `{ub_clutchGS Σ}, ⊢ € ε -∗ WP e {{ v, ⌜φ v⌝ }}) →
-  ub_lift (exec_val n (e, σ)) φ ε.
+  ub_lift (exec n (e, σ)) φ ε.
 Proof.
   intros Hwp.
   eapply (step_fupdN_soundness_no_lc _ n 0).
@@ -203,22 +206,21 @@ Proof.
 Qed.
 
 Lemma ub_lift_closed_lim (e : expr) (σ : state) (ε : nonnegreal) φ :
-  (forall n, ub_lift (exec_val n (e, σ)) φ ε ) ->
-  ub_lift (lim_exec_val (e, σ)) φ ε .
+  (forall n, ub_lift (exec n (e, σ)) φ ε ) ->
+  ub_lift (lim_exec (e, σ)) φ ε .
 Proof.
   intros Hn P HP.
-  apply lim_exec_continous_prob; auto.
+  apply lim_exec_continuous_prob; auto.
   intro n.
   apply Hn; auto.
 Qed.
 
 Theorem wp_union_bound_lim Σ `{ub_clutchGpreS Σ} (e : expr) (σ : state) (ε : nonnegreal) φ :
   (∀ `{ub_clutchGS Σ}, ⊢ € ε -∗ WP e {{ v, ⌜φ v⌝ }}) →
-  ub_lift (lim_exec_val (e, σ)) φ ε.
+  ub_lift (lim_exec (e, σ)) φ ε.
 Proof.
   intros.
   apply ub_lift_closed_lim.
   intro n.
   apply (wp_union_bound Σ); auto.
 Qed.
-
diff --git a/theories/ub_logic/ectx_lifting.v b/theories/ub_logic/ectx_lifting.v
index 2224535c..a7fbf08c 100644
--- a/theories/ub_logic/ectx_lifting.v
+++ b/theories/ub_logic/ectx_lifting.v
@@ -1,6 +1,6 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.proofmode Require Import proofmode.
-From clutch.program_logic Require Import ectx_language.
+From clutch.common Require Import ectx_language.
 From clutch.ub_logic Require Import ub_weakestpre lifting.
 From iris.prelude Require Import options.
 
diff --git a/theories/ub_logic/hash.v b/theories/ub_logic/hash.v
index a69a5840..c12163fa 100644
--- a/theories/ub_logic/hash.v
+++ b/theories/ub_logic/hash.v
@@ -17,7 +17,7 @@ Module simple_bit_hash.
       match: get hm "v" with
       | SOME "b" => "b"
       | NONE =>
-          let: "b" := (rand #val_size from #()) in
+          let: "b" := (rand #val_size) in
           set hm "v" "b";;
           "b"
       end.
@@ -26,7 +26,7 @@ Module simple_bit_hash.
       match: get "hm" "v" with
       | SOME "b" => "b"
       | NONE =>
-          let: "b" := (rand #val_size from #()) in
+          let: "b" := (rand #val_size) in
           set "hm" "v" "b";;
           "b"
       end.
@@ -139,7 +139,7 @@ Module simple_bit_hash.
     wp_apply (wp_get with "[$]").
     iIntros (vret) "(Hhash&->)".
     rewrite lookup_fmap Hlookup /=. wp_pures.
-    wp_bind (rand _ from #())%E.
+    wp_bind (rand _)%E.
     wp_apply (wp_rand_err_list_int _ val_size (map (λ p, snd p) (gmap_to_list m))); auto.
     rewrite map_length.
     iFrame.
diff --git a/theories/ub_logic/noproph.v b/theories/ub_logic/noproph.v
index c6ada3cf..993976e0 100644
--- a/theories/ub_logic/noproph.v
+++ b/theories/ub_logic/noproph.v
@@ -28,7 +28,7 @@ Module counter_example.
 
   Definition bad : expr :=
     let: "p" := NewProph #() in
-    let: "x" := (rand #99 from #()) in
+    let: "x" := (rand #99) in
     (ResolveProph "p" "x").
 
   Lemma falso :
diff --git a/theories/ub_logic/primitive_laws.v b/theories/ub_logic/primitive_laws.v
index 215854a6..fcd170f0 100644
--- a/theories/ub_logic/primitive_laws.v
+++ b/theories/ub_logic/primitive_laws.v
@@ -125,7 +125,7 @@ Qed.
 
 Lemma wp_rand (N : nat) (z : Z) E :
   TCEq N (Z.to_nat z) →
-  {{{ True }}} rand #z from #() @ E {{{ (n : fin (S N)), RET #n; True }}}.
+  {{{ True }}} rand #z @ E {{{ (n : fin (S N)), RET #n; True }}}.
 Proof.
   iIntros (-> Φ) "_ HΦ".
   iApply wp_lift_atomic_head_step; [done|].
@@ -156,7 +156,7 @@ Qed.
 
 Lemma wp_rand_tape N α n ns z E :
   TCEq N (Z.to_nat z) →
-  {{{ ▷ α ↪ (N; n :: ns) }}} rand #z from #lbl:α @ E {{{ RET #(LitInt n); α ↪ (N; ns) }}}.
+  {{{ ▷ α ↪ (N; n :: ns) }}} rand(#lbl:α) #z @ E {{{ RET #(LitInt n); α ↪ (N; ns) }}}.
 Proof.
   iIntros (-> Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
@@ -172,7 +172,7 @@ Qed.
 
 Lemma wp_rand_tape_empty N z α E :
   TCEq N (Z.to_nat z) →
-  {{{ ▷ α ↪ (N; []) }}} rand #z from #lbl:α @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }}}.
+  {{{ ▷ α ↪ (N; []) }}} rand(#lbl:α) #z @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }}}.
 Proof.
   iIntros (-> Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
@@ -188,7 +188,7 @@ Qed.
 Lemma wp_rand_tape_wrong_bound N M z α E ns :
   TCEq N (Z.to_nat z) →
   N ≠ M →
-  {{{ ▷ α ↪ (M; ns) }}} rand #z from #lbl:α @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }}}.
+  {{{ ▷ α ↪ (M; ns) }}} rand(#lbl:α) #z @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }}}.
 Proof.
   iIntros (-> ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step; [done|].
diff --git a/theories/ub_logic/proofmode.v b/theories/ub_logic/proofmode.v
index fa8db3cd..37585ea4 100644
--- a/theories/ub_logic/proofmode.v
+++ b/theories/ub_logic/proofmode.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 From iris.proofmode Require Export tactics.
 From iris.program_logic Require Import atomic.
 
-From clutch.program_logic Require Import language ectx_language.
+From clutch.common Require Import language ectx_language.
 From clutch.prob_lang Require Import lang notation class_instances tactics.
 From clutch.ub_logic Require Import ub_weakestpre primitive_laws.
 From iris.prelude Require Import options.
diff --git a/theories/ub_logic/ub_examples.v b/theories/ub_logic/ub_examples.v
index 6e875452..1d03b1e3 100644
--- a/theories/ub_logic/ub_examples.v
+++ b/theories/ub_logic/ub_examples.v
@@ -5,7 +5,7 @@ Local Open Scope R.
 Context `{!ub_clutchGS Σ}.
 
 Definition foo N (m : nat) : expr :=
-  let: "n" := rand #N from #() in
+  let: "n" := rand #N in
   if: "n" = #m then #false else #true.
 
 
@@ -16,7 +16,7 @@ Lemma wp_foo (N : nat) m E :
 Proof.
   iIntros (Φ) "Herr HΦ".
   rewrite /foo/=.
-  wp_bind (rand _ from #())%E.
+  wp_bind (rand _)%E.
   wp_apply (wp_rand_err_nat _ _ m).
   iFrame.
   iIntros.
@@ -28,8 +28,8 @@ Qed.
 
 
 Definition bar N : expr :=
-  let: "m" := rand #N from #() in
-  let: "n" := rand #N from #() in
+  let: "m" := rand #N in
+  let: "n" := rand #N in
   if: "n" = "m" then #false else #true.
 
 
@@ -40,7 +40,7 @@ Definition wp_bar (N : nat) E :
 Proof.
   iIntros (Φ) "Herr HΦ".
   rewrite /bar/=.
-  wp_bind (rand _ from #())%E.
+  wp_bind (rand _)%E.
   wp_apply (wp_rand); auto.
   iIntros "%m ?".
   wp_pures.
@@ -56,7 +56,7 @@ Qed.
 
 Definition baz : expr :=
   rec: "baz" "x" :=
-    let: "n" := rand #2 from #() in
+    let: "n" := rand #2 in
     (if: "n" < #2
       then "n"
       else "baz" #() ).
diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v
index db6d0a01..8b6f6f55 100644
--- a/theories/ub_logic/ub_rules.v
+++ b/theories/ub_logic/ub_rules.v
@@ -16,7 +16,7 @@ Section metatheory.
 Lemma ub_lift_rand_trivial N z σ1 :
   N = Z.to_nat z →
   ub_lift
-    (prim_step (rand #z from #()) σ1)
+    (prim_step (rand #z) σ1)
     (λ ρ2, ∃ (n : fin (S N)),
         ρ2 = (Val #n, σ1)) 0.
 Proof.
@@ -37,7 +37,7 @@ Qed.
 Lemma ub_lift_rand_err N z σ1 (m : fin (S N)):
   N = Z.to_nat z →
   ub_lift
-    (prim_step (rand #z from #()) σ1)
+    (prim_step (rand #z) σ1)
     (λ ρ2, ∃ (n : fin (S N)),
         (n ≠ m)%fin /\ ρ2 = (Val #n, σ1)) (1/(N+1)).
 Proof.
@@ -65,7 +65,7 @@ Qed.
 Lemma ub_lift_rand_err_nat N z σ1 (m : nat):
   N = Z.to_nat z →
   ub_lift
-    (prim_step (rand #z from #()) σ1)
+    (prim_step (rand #z) σ1)
     (λ ρ2, ∃ (n : fin (S N)),
         (fin_to_nat n ≠ m)%fin /\ ρ2 = (Val #n, σ1)) (1/(N+1)).
 Proof.
@@ -94,7 +94,7 @@ Qed.
 Lemma ub_lift_rand_err_list_nat N z σ1 (ms : list nat):
   N = Z.to_nat z →
   ub_lift
-    (prim_step (rand #z from #()) σ1)
+    (prim_step (rand #z) σ1)
     (λ ρ2, ∃ (n : fin (S N)),
         Forall (λ m, (fin_to_nat n ≠ m)%fin) ms /\ ρ2 = (Val #n, σ1)) ((length ms)/(N+1)).
 Proof.
@@ -122,7 +122,7 @@ Qed.
 Lemma ub_lift_rand_err_list_int N z σ1 (ms : list Z):
   N = Z.to_nat z →
   ub_lift
-    (prim_step (rand #z from #()) σ1)
+    (prim_step (rand #z) σ1)
     (λ ρ2, ∃ (n : fin (S N)),
         Forall (λ m, (Z.of_nat (fin_to_nat n) ≠ m)%fin) ms /\ ρ2 = (Val #n, σ1)) ((length ms)/(N+1)).
 Proof.
@@ -161,7 +161,7 @@ Lemma wp_rand_err (N : nat) (z : Z) (m : fin (S N)) E Φ :
   TCEq N (Z.to_nat z) →
   € (nnreal_inv(nnreal_nat(N+1))) ∗
   (∀ x, ⌜x ≠ m⌝ -∗ Φ #x)
-  ⊢ WP rand #z from #() @ E {{ Φ }}.
+  ⊢ WP rand #z @ E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
   iApply wp_lift_step_fupd_exec_ub; [done|].
@@ -217,7 +217,7 @@ Lemma wp_rand_err_nat (N : nat) (z : Z) (m : nat) E Φ :
   TCEq N (Z.to_nat z) →
   € (nnreal_inv(nnreal_nat(N+1))) ∗
   (∀ x, ⌜x ≠ m⌝ -∗ Φ #x)
-  ⊢ WP rand #z from #() @ E {{ Φ }}.
+  ⊢ WP rand #z @ E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
   iApply wp_lift_step_fupd_exec_ub; [done|].
@@ -272,7 +272,7 @@ Lemma wp_rand_err_list_nat (N : nat) (z : Z) (ns : list nat) E Φ :
   TCEq N (Z.to_nat z) →
   € (nnreal_div (nnreal_nat (length ns)) (nnreal_nat(N+1))) ∗
   (∀ x, ⌜Forall (λ m, x ≠ m) ns⌝ -∗ Φ #x)
-  ⊢ WP rand #z from #() @ E {{ Φ }}.
+  ⊢ WP rand #z @ E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
   iApply wp_lift_step_fupd_exec_ub; [done|].
@@ -327,7 +327,7 @@ Lemma wp_rand_err_list_int (N : nat) (z : Z) (zs : list Z) E Φ :
   TCEq N (Z.to_nat z) →
   € (nnreal_div (nnreal_nat (length zs)) (nnreal_nat(N+1))) ∗
   (∀ x : Z , ⌜Forall (λ m, x ≠ m) zs⌝ -∗ Φ #x)
-  ⊢ WP rand #z from #() @ E {{ Φ }}.
+  ⊢ WP rand #z @ E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
   iApply wp_lift_step_fupd_exec_ub; [done|].
@@ -382,7 +382,7 @@ Lemma wp_couple_rand_adv_comp (N : nat) z E Φ (ε1 : nonnegreal) (ε2 : fin (S
   TCEq N (Z.to_nat z) →
   (exists r, ∀ n, (ε2 n <= r)%R) →
   SeriesC (λ n, (1 / (S N)) * ε2 n)%R = (nonneg ε1) →
-  {{{ € ε1 }}} rand #z from #() @ E {{{ n, RET #n; € (ε2 n) }}}.
+  {{{ € ε1 }}} rand #z @ E {{{ n, RET #n; € (ε2 n) }}}.
 Proof.
   iIntros (-> (r & Hε2) Hε1 Ψ) "Herr HΨ".
   iApply wp_lift_step_fupd_exec_ub; [done|].
diff --git a/theories/ub_logic/ub_tactics.v b/theories/ub_logic/ub_tactics.v
index d46c4d36..100f0a06 100644
--- a/theories/ub_logic/ub_tactics.v
+++ b/theories/ub_logic/ub_tactics.v
@@ -3,10 +3,10 @@ From iris.proofmode Require Import
      coq_tactics ltac_tactics
      reduction.
 From clutch.prelude Require Import stdpp_ext.
-From clutch.program_logic Require Import language ectxi_language.
+From clutch.common Require Import language ectxi_language.
 From clutch.prob_lang Require Import locations class_instances notation tactics lang.
-From clutch.rel_logic Require Import primitive_laws model rel_rules proofmode.
-From clutch.rel_logic Require Export spec_tactics.
+From clutch.ctx_logic Require Import primitive_laws model rel_rules proofmode.
+From clutch.ctx_logic Require Export spec_tactics.
 
 (** * General-purpose tactics *)
 Lemma tac_rel_bind_l `{!clutchRGS Σ} e' K ℶ E e t A :
@@ -486,7 +486,7 @@ Tactic Notation "rel_alloctape_l" :=
 
 Lemma tac_rel_rand_l `{!clutchRGS Σ} K ℶ1 ℶ2 i1 (α : loc) N z n ns e t tres A E :
   TCEq N (Z.to_nat z) →
-  t = fill K (rand #z from #lbl:α) →
+  t = fill K (rand(#lbl:α) #z) →
   envs_lookup i1 ℶ1 = Some (false, α ↪ (N; n::ns))%I →
   envs_simple_replace i1 false (Esnoc Enil i1 (α ↪ (N; ns))) ℶ1 = Some ℶ2 →
   tres = fill K (of_val #n) →
@@ -506,7 +506,7 @@ Qed.
 
 Lemma tac_rel_rand_r `{!clutchRGS Σ} K ℶ1 ℶ2 E i1 (α : loc) N z n ns e t tres A :
   TCEq N (Z.to_nat z) →
-  t = fill K (rand #z from (#lbl:α)) →
+  t = fill K (rand(#lbl:α) #z) →
   nclose specN ⊆ E →
   envs_lookup i1 ℶ1 = Some (false, α ↪ₛ (N; n::ns))%I →
   envs_simple_replace i1 false (Esnoc Enil i1 (α ↪ₛ (N; ns))) ℶ1 = Some ℶ2 →
diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v
index 553eb9ad..9afd876e 100644
--- a/theories/ub_logic/ub_weakestpre.v
+++ b/theories/ub_logic/ub_weakestpre.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 
 From clutch.prelude Require Import stdpp_ext NNRbar.
 From clutch.prob Require Export couplings distribution union_bounds.
-From clutch.program_logic Require Export exec language.
+From clutch.common Require Export language.
 
 Import uPred.
 
@@ -406,14 +406,14 @@ Section exec_ub.
             ∀ ρ2, ⌜ R ρ2 ⌝ ={∅}=∗ Z (ε2 ρ2) ρ2 )
     ⊢ exec_ub e1 σ1 Z ε.
   Proof.
-    iIntros "(% & % & % & % & % & H)".
+    iIntros "(% & % & % & %Hε & % & H)".
     rewrite {1}exec_ub_unfold.
     iRight; iLeft.
     iExists _,nnreal_zero,_.
     iSplit; [done|].
     iSplit.
     { iPureIntro.
-      simpl. lra.
+      simpl. rewrite Hε. lra.
     }
     iSplit; done.
   Qed.
@@ -570,13 +570,13 @@ Qed.
 
 
 (* TODO: get rid of stuckness in notation [iris/bi/weakestpre.v] so that we don't have to do this *)
-Local Definition ub_wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
-  λ (s : stuckness), fixpoint (ub_wp_pre).
+Local Definition ub_wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) () :=
+  {| wp := λ _ : (), fixpoint (ub_wp_pre); wp_default := () |}.
 Local Definition ub_wp_aux : seal (@ub_wp_def). Proof. by eexists. Qed.
 Definition ub_wp' := ub_wp_aux.(unseal).
 Global Arguments ub_wp' {Λ Σ _}.
 Global Existing Instance ub_wp'.
-Local Lemma ub_wp_unseal `{!irisGS Λ Σ} : wp = @ub_wp_def Λ Σ _.
+Local Lemma ub_wp_unseal `{!irisGS Λ Σ} : wp = (@ub_wp_def Λ Σ _).(wp).
 Proof. rewrite -ub_wp_aux.(seal_eq) //. Qed.
 
 Section ub_wp.
@@ -630,11 +630,11 @@ Qed.
 Lemma ub_wp_value_fupd' s E Φ v : WP of_val v @ s; E {{ Φ }} ⊣⊢ |={E}=> Φ v.
 Proof. rewrite ub_wp_unfold /ub_wp_pre to_of_val. auto. Qed.
 
-Lemma ub_wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
-  s1 ⊑ s2 → E1 ⊆ E2 →
-  WP e @ s1; E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 {{ Ψ }}.
+Lemma ub_wp_strong_mono E1 E2 e Φ Ψ s :
+  E1 ⊆ E2 →
+  WP e @ s ; E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s ; E2 {{ Ψ }}.
 Proof.
-  iIntros (? HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
+  iIntros (HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
   rewrite !ub_wp_unfold /ub_wp_pre /=.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
@@ -642,7 +642,7 @@ Proof.
   iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[% H]".
   iModIntro.
-  iSplit; [by destruct s1,s2 | ].
+  iSplit; [done | ].
   iApply (exec_ub_mono_pred with "[Hclose HΦ] H").
   iIntros (? [e2 σ2]) "H".
   iModIntro.
@@ -658,7 +658,7 @@ Proof.
   iIntros (σ1 ε) "Hi". iMod "H". by iApply "H".
 Qed.
 Lemma ub_wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
-Proof. iIntros "H". iApply (ub_wp_strong_mono s s E with "H"); auto. Qed.
+Proof. iIntros "H". iApply (ub_wp_strong_mono E with "H"); auto. Qed.
 
 Lemma ub_wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
   (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
@@ -703,7 +703,7 @@ Proof.
   iMod "H" as "(Hσ & Hρ & H)".
   iMod "HR".
   iFrame "Hσ Hρ".
-  iApply (ub_wp_strong_mono s s E2 with "H"); [done..|].
+  iApply (ub_wp_strong_mono E2 with "H"); [done..|].
   iIntros "!>" (v) "H". by iApply "H".
 Qed.
 
@@ -752,12 +752,6 @@ Proof.
   iIntros (HΦ) "H"; iApply (ub_wp_strong_mono with "H"); auto.
   iIntros (v) "?". by iApply HΦ.
 Qed.
-Lemma ub_wp_stuck_mono s1 s2 E e Φ :
-  s1 ⊑ s2 → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
-Proof. iIntros (?) "H". iApply (ub_wp_strong_mono with "H"); auto. Qed.
-Lemma ub_wp_stuck_weaken s E e Φ :
-  WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
-Proof. apply ub_wp_stuck_mono. by destruct s. Qed.
 Lemma ub_wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
 Proof. iIntros (?) "H"; iApply (ub_wp_strong_mono with "H"); auto. Qed.
 Global Instance ub_wp_mono' s E e :
@@ -852,7 +846,7 @@ Section proofmode_classes.
   Qed.
 
   Global Instance elim_modal_fupd_ub_wp_atomic p s E1 E2 e P Φ :
-    ElimModal (Atomic (stuckness_to_atomicity s) e) p false
+    ElimModal (Atomic WeaklyAtomic e) p false
             (|={E1,E2}=> P) P
             (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof.
@@ -866,7 +860,7 @@ Section proofmode_classes.
   Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_ub_wp. Qed.
 
   Global Instance elim_acc_ub_wp_atomic {X} E1 E2 α β γ e s Φ :
-    ElimAcc (X:=X) (Atomic (stuckness_to_atomicity s) e)
+    ElimAcc (X:=X) (Atomic WeaklyAtomic e)
             (fupd E1 E2) (fupd E2 E1)
             α β γ (WP e @ s; E1 {{ Φ }})
             (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I | 100.