Coneris hocap

theories/coneris/adequacy.v

@@ -63,13 +63,22 @@ Section adequacy.
     iRevert (σ ε) "H".
     iApply state_step_coupl_ind.
     iModIntro.
-    iIntros (??) "[%|[>(_&_&%)|(%R&%μ&%&%&%Herasable&%&%Hineq&%Hpgl&H)]]".
+    iIntros (??) "[%|[>(_&_&%)|[H|(%R&%μ&%&%&%Herasable&%&%Hineq&%Hpgl&H)]]]".
     - iPureIntro. by apply pgl_1.
     - iApply fupd_mask_intro; first done.
       iIntros "_".
       iPureIntro.
       erewrite sch_exec_is_final; last done.
       eapply pgl_mon_grading; last apply pgl_dret; auto.
+    - iApply (fupd_mono _ _ (⌜_⌝)%I).
+      { iPureIntro.
+        intros H'.
+        apply pgl_epsilon_limit; last exact.
+        by apply Rle_ge. 
+      }
+      iIntros (ε' ?).
+      unshelve iDestruct ("H" $! (mknonnegreal ε' _) with "[]") as "[H _]"; [|done..].
+      pose proof cond_nonneg ε. lra.
     - erewrite <-Herasable; last done.
       iApply (fupd_mono _ _ (⌜_⌝)%I).
       { iPureIntro.
@@ -91,11 +100,20 @@ Section adequacy.
   Proof.
     iRevert (σ ε).
     iApply state_step_coupl_ind.
-    iIntros "!>" (σ ε) "[%|[?|(%&%μ&%&%&%Herasable&%&%&%&H)]] Hcont".
+    iIntros "!>" (σ ε) "[%|[?|[H|(%&%μ&%&%&%Herasable&%&%&%&H)]]] Hcont".
     - iApply step_fupdN_intro; first done.
       iPureIntro.
       by apply pgl_1.
     - by iMod ("Hcont" with "[$]").
+    - iApply (step_fupdN_mono _ _ _ (⌜(∀ ε', _)⌝)).
+      { iPureIntro.
+        intros.
+        apply pgl_epsilon_limit; [simpl; by apply Rle_ge|done].
+      }
+      iIntros (ε' ?).
+      unshelve iDestruct ("H" $! (mknonnegreal ε' _) with "[]") as "[H _]";
+        [pose proof cond_nonneg ε; simpl in *; lra|done|simpl].
+      iApply ("H" with "[$]").
     - rewrite -Herasable.
       iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
       { iPureIntro.
@@ -121,11 +139,20 @@ Section adequacy.
     intros ???.
     iRevert (σ ε).
     iApply state_step_coupl_ind.
-    iIntros "!>" (σ ε) "[%|[?|(%&%μ&%&%&%&%&%&%&H)]] Hcont".
+    iIntros "!>" (σ ε) "[%|[?|[H|(%&%μ&%&%&%&%&%&%&H)]]] Hcont".
     - iApply step_fupdN_intro; first done.
       iPureIntro.
       by apply pgl_1.
     - by iMod ("Hcont" with "[$]").
+    - iApply (step_fupdN_mono _ _ _ (⌜(∀ ε', _)⌝)).
+      { iPureIntro.
+        intros.
+        apply pgl_epsilon_limit; [simpl; by apply Rle_ge|done].
+      }
+      iIntros (ε' ?).
+      unshelve iDestruct ("H" $! (mknonnegreal ε' _) with "[]") as "[H _]";
+        [pose proof cond_nonneg ε; simpl in *; lra|done|simpl].
+      iApply ("H" with "[$]").
     - unshelve erewrite (Rcoupl_eq_elim _ _ (prim_coupl_step_prim_sch_erasable _ _ _ _ _ _ _ μ _ _ _ _)); [done..|].
       iApply (step_fupdN_mono _ _ _ (⌜pgl _ _ (_+_)⌝)%I).
       { iPureIntro.
@@ -329,5 +356,3 @@ Proof.
   intros.
   by eapply wp_pgl.
 Qed.
-
-(* TODO limit stronger adequacy*)

theories/coneris/ectx_lifting.v

@@ -17,7 +17,6 @@ Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
 Local Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd {E Φ} e1 s :
-  to_val e1 = None →
   (∀ σ1 ε1,
     state_interp σ1 ∗ err_interp ε1
     ={E,∅}=∗
@@ -38,7 +37,7 @@ Lemma wp_lift_head_step_fupd {E Φ} e1 s :
   )
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd_glm; [done|].
+  iIntros "H". iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "Hσε".
   iMod ("H" with "Hσε") as "[% H]"; iModIntro; auto.
 Qed.

theories/coneris/error_rules.v

@@ -162,7 +162,7 @@ Lemma wp_rand_err (N : nat) (z : Z) (m : fin (S N)) E Φ s :
   ⊢ WP rand #z @ s; E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -214,7 +214,7 @@ Lemma wp_rand_err_nat (N : nat) (z : Z) (m : nat) E Φ s :
   ⊢ WP rand #z @ s; E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -262,7 +262,7 @@ Lemma wp_rand_err_list_nat (N : nat) (z : Z) (ns : list nat) E Φ :
   ⊢ WP rand #z @ E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -308,7 +308,7 @@ Lemma wp_rand_err_list_int (N : nat) (z : Z) (zs : list Z) E Φ :
   ⊢ WP rand #z @ E {{ Φ }}.
 Proof.
   iIntros (->) "[Herr Hwp]".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -407,7 +407,7 @@ Lemma wp_couple_rand_adv_comp (N : nat) z E (ε1 : R) (ε2 : fin (S N) -> R) :
   {{{ ↯ ε1 }}} rand #z @ E {{{ n, RET #n; ↯ (ε2 n) }}}.
 Proof.
   iIntros (-> Hineq (r & Hε2) Hε1 Ψ) "Herr HΨ".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε_now) "[Hσ Hε]".
   iApply fupd_mask_intro; [set_solver|].
   iIntros "Hclose'".
@@ -1020,13 +1020,12 @@ Proof.
 Qed. 
 
 Lemma wp_presample (N : nat) E e 𝛼 Φ ns :
-  to_val e = None →
   ▷ 𝛼 ↪N (N;ns) ∗
   (∀ n, 𝛼 ↪N (N; ns ++ [n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (He) "(>H𝛼&Hwp)".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iIntros "(>H𝛼&Hwp)".
+  iApply wp_lift_step_fupd_glm.
   iIntros (𝜎 ε) "((Hheap&Htapes)&Hε)".
   iDestruct "H𝛼" as (ns') "(%Hmap & H𝛼)".
   iDestruct (ghost_map_lookup with "Htapes H𝛼") as %Hlookup.
@@ -1045,7 +1044,7 @@ Proof.
   iMod "Hclose'" as "_".
   iSpecialize ("Hwp" $! (fin_to_nat n) with "[H𝛼]").
   { iExists _. iFrame. iPureIntro. rewrite fmap_app; by f_equal. }
-  rewrite !pgl_wp_unfold /pgl_wp_pre /= He.
+  rewrite !pgl_wp_unfold /pgl_wp_pre /=.
   iSpecialize ("Hwp" $! (state_upd_tapes <[𝛼:=(N; ns' ++ [n]):tape]> 𝜎) ε).
   iMod ("Hwp" with "[Hheap Htapes Hε]") as "Hwp".
   { replace (nnreal_zero + ε)%NNR with ε by (apply nnreal_ext; simpl; lra).
@@ -1059,16 +1058,15 @@ Qed.
 
 
 Lemma wp_presample_adv_comp (N : nat) E e α Φ ns (ε1 : R) (ε2 : fin (S N) -> R) :
-  to_val e = None →
   (∀ n, 0<=ε2 n)%R ->
   (SeriesC (λ n, (1 / (S N)) * ε2 n)%R <= ε1)%R →
   ▷α ↪N (N; ns) ∗
   ↯ ε1 ∗
   (∀ n, ↯ (ε2 n) ∗ α ↪N (N; ns ++ [fin_to_nat n]) -∗ WP e @ E {{ Φ }})
   ⊢ WP e @ E {{ Φ }}.
 Proof.
-  iIntros (Hσ_red Hpos Hsum) "(>Hα & Hε & Hwp)".
-  iApply wp_lift_step_fupd_glm; [done|].
+  iIntros (Hpos Hsum) "(>Hα & Hε & Hwp)".
+  iApply wp_lift_step_fupd_glm.
   iIntros (σ1 ε_now) "[(Hheap&Htapes) Hε_supply]".
   iDestruct "Hα" as (ns') "(%Hmap & Hα)".
   iDestruct (ghost_map_lookup with "Htapes Hα") as "%Hlookup".
@@ -1093,7 +1091,7 @@ Proof.
   rewrite pgl_wp_unfold /pgl_wp_pre.
   simpl.
   remember {| heap := heap (σ1); tapes := (<[α:=(N; ns' ++ [sample])]> (tapes σ1)) |} as σ2.
-  rewrite /= Hσ_red /=.
+  rewrite /=.
   iSpecialize ("Hwp" with "[Hε Hα]"); first iFrame.
   { iPureIntro. rewrite fmap_app; by f_equal. }
   iSpecialize ("Hwp" $! σ2 _).
@@ -1110,9 +1108,8 @@ Qed.
     α ↪N (N; ns) -∗ wp_update E (∃ n, α ↪N (N; ns ++ [n])).
   Proof.
     rewrite wp_update_unseal.
-    iIntros "Hα" (e Φ Hv) "Hwp".
+    iIntros "Hα" (e Φ) "Hwp".
     iApply wp_presample.
-    { rewrite Hv //. }
     iFrame. iIntros (n) "Hα".
     iApply ("Hwp" with "[$Hα]").
   Qed.
@@ -1123,8 +1120,8 @@ Qed.
     α ↪N (N; ns) ∗ ↯ ε1 -∗ wp_update E (∃ n, α ↪N (N; ns ++ [fin_to_nat n]) ∗ ↯ (ε2 n)).
   Proof.
     rewrite wp_update_unseal.
-    iIntros (? ?) "[Hα Hε1]". iIntros (e Φ Hv) "Hwp".
-    iApply (wp_presample_adv_comp _ _ _ _ _ _ _ ε2); [rewrite Hv//|done|done|..].
+    iIntros (? ?) "[Hα Hε1]". iIntros (e Φ) "Hwp".
+    iApply (wp_presample_adv_comp _ _ _ _ _ _ _ ε2); [done|done|..].
     iFrame. iIntros (n) "[Hα Hε2]".
     iApply ("Hwp" with "[$Hα $Hε2]").
   Qed.

theories/coneris/examples/parallel_add.v

@@ -817,12 +817,12 @@ Section attempt3.
     { iFrame. }
     iDestruct "Hfrag_loc" as "[Hfrac_a Hfrac_b]".
     (** presample *)
-    wp_apply (wp_presample_bool_adv_comp _ _ _ _ _ _ (λ b, if b then nnreal_half else nnreal_one)); [done|..]; last iFrame "Hα Herr".
+    wp_apply (wp_presample_bool_adv_comp _ _ _ _ _ _ (λ b, if b then nnreal_half else nnreal_one)); last iFrame "Hα Herr".
     { intros; case_match; simpl; lra. }
     { simpl; lra. }
     iIntros ([|]) "[Herr Hα]"; last first.
     { iExFalso. by iApply ec_contradict. }
-    wp_apply (wp_presample_bool_adv_comp _ _ _ _ _ _ (λ b, if b then nnreal_zero else nnreal_one)); [done|..]; last iFrame "Hα' Herr".
+    wp_apply (wp_presample_bool_adv_comp _ _ _ _ _ _ (λ b, if b then nnreal_zero else nnreal_one)); last iFrame "Hα' Herr".
     { intros; case_match; simpl; lra. }
     { simpl; lra. }
     iIntros ([|]) "[? Hα']"; last first.

theories/coneris/examples/random_counter/impl1.v

@@ -251,8 +251,8 @@ Program Definition random_counter1 `{!conerisGS Σ}: random_counter :=
     is_counter _ N c γ1 γ2 γ3 := inv N (counter_inv_pred1 c γ1 γ2 γ3);
     counter_error_auth _ γ x := ●↯ x @ γ;
     counter_error_frag _ γ x := ◯↯ x @ γ;
-    counter_tapes_auth _ γ m := (●m@γ)%I;
-    counter_tapes_frag _ γ α N ns := (α◯↪N (N;ns) @ γ)%I;
+    counter_tapes_auth _ γ m := (●((λ ns, (3, ns))<$>m)@γ)%I;
+    counter_tapes_frag _ γ α ns := (α◯↪N (3%nat;ns) @ γ)%I;
     counter_content_auth _ γ z := own γ (●F z);
     counter_content_frag _ γ f z := own γ (◯F{f} z);
     new_counter_spec _ := new_counter_spec1;
@@ -297,18 +297,23 @@ Next Obligation.
 Qed.
 Next Obligation.
   simpl. 
-  iIntros (?????????) "H1 H2".
+  iIntros (???????) "H1 H2".
   iDestruct (ghost_map_elem_frac_ne with "[$][$]") as "%"; last done.
   rewrite dfrac_op_own dfrac_valid_own. by intro.
 Qed.
 Next Obligation.
   simpl.
   iIntros.
-  iApply (hocap_tapes_agree with "[$][$]").
+  iDestruct (hocap_tapes_agree with "[$][$]") as "%H".
+  iPureIntro.
+  rewrite lookup_fmap_Some in H. destruct H as (?&?&?).
+  by simplify_eq.
 Qed.
 Next Obligation.
   iIntros.
-  iApply (hocap_tapes_presample with "[$][$]").
+  iMod (hocap_tapes_presample with "[$][$]") as "[??]".
+  iModIntro. iFrame.
+  by rewrite fmap_insert. 
 Qed.
 Next Obligation.
   simpl.