fix rand counter

theories/coneris/examples/random_counter/impl1.v

@@ -172,9 +172,7 @@ Section impl1.
         wp_update E (∃ n, T (n) ∗ α◯↪N (3%nat; ns++[n]) @ γ2).
   Proof.
     iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag".
-    rewrite wp_update_unfold.
-    iIntros (?? Hv) "Hcnt".
-    rewrite {2}pgl_wp_unfold /pgl_wp_pre /= Hv.
+    iApply wp_update_state_step_coupl.
     iIntros (σ ε) "((Hheap&Htapes)&Hε)".
     iMod (inv_acc with "Hinv") as "[>(% & % & % & % & H1 & H2 & H3 & H4 & -> & H5 & H6) Hclose]"; [done|].
     iDestruct (hocap_tapes_agree with "[$][$]") as "%".
@@ -186,7 +184,7 @@ Section impl1.
     iDestruct (ec_supply_bound with "[$][$]") as "%".
     iMod (ec_supply_decrease with "[$][$]") as (ε1' ε_rem -> Hε1') "Hε_supply". subst.
     iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'".
-    iApply glm_state_adv_comp_con_prob_lang; first done.
+    iApply state_step_coupl_state_adv_comp_con_prob_lang; first done.
     unshelve iExists (λ x, mknonnegreal (ε2 ε1' x) _).
     { apply Hpos. apply cond_nonneg. }
     iSplit.
@@ -197,11 +195,10 @@ Section impl1.
 
     destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' sample))%R 1%R) as [Hdec|Hdec]; last first.
     { apply Rnot_lt_ge, Rge_le in Hdec.
-      iLeft.
-      iPureIntro.
+      iApply state_step_coupl_ret_err_ge_1.
       simpl. simpl in *. lra.
     }
-    iRight.
+    iApply state_step_coupl_ret.
     unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 ε1' sample) _) with "Hε_supply") as "[Hε_supply Hε]".
     { apply Hpos. apply cond_nonneg. }
     { simpl. done. }
@@ -214,10 +211,8 @@ Section impl1.
     { iNext. iSplit; last done.
       rewrite big_sepM_insert_delete; iFrame.
     }
-    iSpecialize ("Hcnt" with "[$]").
-    setoid_rewrite pgl_wp_unfold.
-    rewrite /pgl_wp_pre /= Hv.
-    iApply ("Hcnt" $! (state_upd_tapes <[α:= (3%nat; ns' ++[sample]):tape]> σ) with "[$]").
+    iApply fupd_mask_intro_subseteq; first set_solver.
+    iFrame.
   Qed. 
 
   Lemma read_counter_spec1 N E c γ1 γ2 γ3 P Q:

theories/coneris/examples/random_counter/impl2.v

@@ -263,9 +263,7 @@ Section impl2.
         wp_update E (∃ n, T (n) ∗ α◯↪N (true, 3%nat; ns++[n]) @ γ2).
   Proof.
     iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag".
-    rewrite wp_update_unfold.
-    iIntros (?? Hv) "Hcnt".
-    rewrite {2}pgl_wp_unfold /pgl_wp_pre /= Hv.
+    iApply wp_update_state_step_coupl.
     iIntros (σ ε) "((Hheap&Htapes)&Hε)".
     iMod (inv_acc with "Hinv") as "[>(% & % & % & % & H1 & H2 & H3 & H4 & -> & H5 & H6) Hclose]"; [done|].
     iDestruct (hocap_tapes_agree' with "[$][$]") as "%".
@@ -277,7 +275,7 @@ Section impl2.
     iDestruct (ec_supply_bound with "[$][$]") as "%".
     iMod (ec_supply_decrease with "[$][$]") as (ε1' ε_rem -> Hε1') "Hε_supply". subst.
     iApply fupd_mask_intro; [set_solver|]; iIntros "Hclose'".
-    iApply (glm_iterM_state_adv_comp_con_prob_lang 2%nat); first done.
+    iApply (state_step_coupl_iterM_state_adv_comp_con_prob_lang 2%nat); first done.
     pose (f (l:list (fin 2)) := (match l with
                                        | x::[x'] => 2*fin_to_nat x + fin_to_nat x'
                                        | _ => 0
@@ -302,11 +300,10 @@ Section impl2.
     iIntros (sample ?).
     destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' (f sample)))%R 1%R) as [Hdec|Hdec]; last first.
     { apply Rnot_lt_ge, Rge_le in Hdec.
-      iLeft.
-      iPureIntro.
+      iApply state_step_coupl_ret_err_ge_1.
       simpl. simpl in *. lra.
     }
-    iRight.
+    iApply state_step_coupl_ret.
     unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2 ε1' (f sample)) _) with "Hε_supply") as "[Hε_supply Hε]".
     { apply Hpos. apply cond_nonneg. }
     { simpl. done. }
@@ -344,14 +341,11 @@ Section impl2.
       simpl. rewrite !fin_to_nat_to_fin.
       rewrite /expander bind_app -/(expander ns). simpl. by rewrite H1. 
     }
-    iSpecialize ("Hcnt" with "[$]").
-    setoid_rewrite pgl_wp_unfold.
-    rewrite /pgl_wp_pre /= Hv.
+    iApply fupd_mask_intro_subseteq; first set_solver.
     rewrite K.
-    iApply ("Hcnt" $! (state_upd_tapes <[α:= (1%nat; ns' ++ sample):tape]> σ) with "[$]").
+    iFrame. 
   Qed.
 
-
   Lemma read_counter_spec2 N E c γ1 γ2 γ3 P Q:
     ↑N ⊆ E ->
     {{{  inv N (counter_inv_pred2 c γ1 γ2 γ3) ∗

theories/coneris/weakestpre.v

@@ -873,21 +873,19 @@ Proof.
 Qed.
 
 Lemma state_step_coupl_pgl_wp E e Φ s :
-  (∀ σ1 ε1, state_interp σ1 ∗ err_interp ε1 -∗
+  (∀ σ1 ε1, state_interp σ1 ∗ err_interp ε1 ={E, ∅}=∗
             state_step_coupl σ1 ε1
-              (λ σ2 ε2, |={E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e @ s ; E {{Φ}})) -∗
+              (λ σ2 ε2, |={∅, E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e @ s ; E {{Φ}})) -∗
   WP e @ s ; E {{ Φ }}.
 Proof.
   iIntros "H".
   erewrite pgl_wp_unfold. rewrite /pgl_wp_pre.
   iIntros (??) "[??]". 
-  iApply fupd_mask_intro; first set_solver.
-  iIntros "Hclose".
   iSpecialize ("H" with "[$]").
-  iApply (state_step_coupl_bind with "[Hclose][$]").
+  iMod "H". iModIntro.
+  iApply (state_step_coupl_bind with "[][$]").
   iIntros (??) "H".
   iApply fupd_state_step_coupl.
-  iMod "Hclose" as "_".
   iMod "H" as "(?&?&H)".
   rewrite pgl_wp_unfold/pgl_wp_pre.
   iApply "H". iFrame.

theories/coneris/wp_update.v

@@ -85,8 +85,30 @@ Section wp_update.
      (∀ e Φ, ⌜TCEq (to_val e) None⌝ -∗ (P -∗ WP e @ E {{ Φ }}) -∗ WP e @ E {{ Φ }}).
   Proof.
     by rewrite wp_update_unseal.
-  Qed. 
-
+  Qed.
+
+  Lemma wp_update_state_step_coupl P E:
+    (∀ σ1 ε1, state_interp σ1 ∗ err_interp ε1 ={E, ∅}=∗
+            state_step_coupl σ1 ε1
+              (λ σ2 ε2, |={∅, E}=> state_interp σ2 ∗ err_interp ε2 ∗ P))
+    -∗ wp_update E P.
+  Proof.
+    iIntros "H".
+    rewrite wp_update_unseal/wp_update_def.
+    iIntros (???) "H'".
+    iApply state_step_coupl_pgl_wp.
+    iIntros (??) "[??]".
+    iMod ("H" with "[$]") as "H".
+    iModIntro.
+    iApply (state_step_coupl_bind with "[H']"); last done.
+    simpl.
+    iIntros (??) "H".
+    iApply state_step_coupl_ret.
+    iMod "H" as "(?&?&?)".
+    iFrame.
+    by iApply "H'".
+  Qed.
+
   Global Instance from_modal_wp_update_wp_update P E :
     FromModal True modality_id (wp_update E P) (wp_update E P) P.
   Proof. iIntros (_) "HP /=". by iApply wp_update_ret. Qed.