From 547516c7ae9fe2a1f1f1606a517b2fc5cb5c60a0 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 16 Sep 2024 12:50:38 +0200 Subject: [PATCH 01/10] new_counter_spec3 --- .../coneris/examples/random_counter/impl3.v | 37 ++++++++++++++++++- 1 file changed, 35 insertions(+), 2 deletions(-) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index e6c7c8ad..6f7f23c5 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -5,7 +5,7 @@ From clutch.coneris Require Import coneris hocap random_counter. Set Default Proof Using "Type*". Section filter. - Definition filter_f (n:fin 4%nat):= bool_decide (fin_to_nat n<4)%nat. + Definition filter_f (n:nat):= bool_decide (n<4)%nat. Definition filtered_list (l:list _) := filter filter_f l. End filter. @@ -24,5 +24,38 @@ Section impl3. counterG2_frac_authR:: inG Σ (frac_authR natR) }. Context `{!conerisGS Σ, !hocap_errorGS Σ, !hocap_tapesGS Σ, !inG Σ (frac_authR natR)}. - + Definition counter_inv_pred3 (c:val) γ1 γ2 γ3:= + (∃ (ε:R) (m:gmap loc (nat * list nat)) (l:loc) (z:nat), + ↯ ε ∗ ●↯ ε @ γ1 ∗ + ([∗ map] α ↦ t ∈ m, ∃ (ls:list nat), ⌜ (filter filter_f ls) = t.2⌝ ∗ α ↪N ( 4%nat ; ls) ) + ∗ ●m@γ2 ∗ + ⌜c=#l⌝ ∗ l ↦ #z ∗ own γ3 (●F z) + )%I. + + Lemma new_counter_spec3 E ε N: + {{{ ↯ ε }}} + new_counter3 #() @ E + {{{ (c:val), RET c; + ∃ γ1 γ2 γ3, inv N (counter_inv_pred3 c γ1 γ2 γ3) ∗ + ◯↯ε @ γ1 ∗ own γ3 (◯F 0%nat) + }}}. + Proof. + rewrite /new_counter3. + iIntros (Φ) "Hε HΦ". + wp_pures. + wp_alloc l as "Hl". + iDestruct (ec_valid with "[$]") as "%". + unshelve iMod (hocap_error_alloc (mknonnegreal ε _)) as "[%γ1 [H1 H2]]". + { lra. } + simpl. + iMod (hocap_tapes_alloc (∅:gmap _ _)) as "[%γ2 [H3 H4]]". + iMod (own_alloc (●F 0%nat ⋅ ◯F 0%nat)) as "[%γ3[H5 H6]]". + { by apply frac_auth_valid. } + replace (#0) with (#0%nat) by done. + iMod (inv_alloc N _ (counter_inv_pred3 (#l) γ1 γ2 γ3) with "[$Hε $Hl $H1 $H3 $H5]") as "#Hinv". + { iSplit; last done. by iApply big_sepM_empty. } + iApply "HΦ". + iExists _, _, _. by iFrame. + Qed. + End impl3. From 8d5895d613516a3606c717b25c5bbb70b4984f66 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 16 Sep 2024 14:27:37 +0200 Subject: [PATCH 02/10] allocate_tape_spec3 --- .../coneris/examples/random_counter/impl3.v | 39 ++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index 6f7f23c5..0ddf9607 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -9,6 +9,19 @@ Section filter. Definition filtered_list (l:list _) := filter filter_f l. End filter. +Section lemmas. + Context `{!conerisGS Σ}. + Lemma hocap_tapes_notin3 α N ns (m:gmap loc (nat*list nat)) : + α ↪N (N; ns) -∗ ([∗ map] α↦t ∈ m,∃ (ls:list nat), ⌜ (filter filter_f ls) = t.2⌝ ∗ α ↪N ( 4%nat ; ls)) -∗ ⌜m!!α=None ⌝. + Proof. + destruct (m!!α) eqn:Heqn; last by iIntros. + iIntros "Hα Hmap". + iDestruct (big_sepM_lookup with "[$]") as "(%&%&?)"; first done. + iExFalso. + iApply (tapeN_tapeN_contradict with "[$][$]"). + Qed. +End lemmas. + Section impl3. Definition new_counter3 : val:= λ: "_", ref #0. @@ -56,6 +69,30 @@ Section impl3. { iSplit; last done. by iApply big_sepM_empty. } iApply "HΦ". iExists _, _, _. by iFrame. - Qed. + Qed. + + Lemma allocate_tape_spec3 N E c γ1 γ2 γ3: + ↑N ⊆ E-> + {{{ inv N (counter_inv_pred3 c γ1 γ2 γ3) }}} + allocate_tape3 #() @ E + {{{ (v:val), RET v; + ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ α ◯↪N (3%nat; []) @ γ2 + }}}. + Proof. + iIntros (Hsubset Φ) "#Hinv HΦ". + rewrite /allocate_tape3. + wp_pures. + wp_alloctape α as "Hα". + iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + iDestruct (hocap_tapes_notin3 with "[$][$]") as "%". + iMod (hocap_tapes_new with "[$]") as "[H4 H7]"; first done. + iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Hα]") as "_". + { iNext. iSplitL; last done. + rewrite big_sepM_insert; [simpl; iFrame|done]. + by rewrite filter_nil. + } + iApply "HΦ". + by iFrame. + Qed. End impl3. From 97d84b03858fa7a34b73dee8e5ec5d8deb1423a5 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 16 Sep 2024 14:38:14 +0200 Subject: [PATCH 03/10] read_counter_spec3 --- .../coneris/examples/random_counter/impl3.v | 125 ++++++++++++++++++ 1 file changed, 125 insertions(+) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index 0ddf9607..a5b6d1d1 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -94,5 +94,130 @@ Section impl3. iApply "HΦ". by iFrame. Qed. + + Lemma incr_counter_tape_spec_some3 N E c γ1 γ2 γ3 (P: iProp Σ) (Q:nat->iProp Σ) (α:loc) (n:nat) ns: + ↑N⊆E -> + {{{ inv N (counter_inv_pred3 c γ1 γ2 γ3) ∗ + □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗ + own γ3 (●F(z+n)%nat)∗ Q z) ∗ + P ∗ α ◯↪N (3%nat; n::ns) @ γ2 + }}} + incr_counter_tape3 c #lbl:α @ E + {{{ (z:nat), RET (#z, #n); Q z ∗ α ◯↪N (3%nat; ns) @ γ2}}}. + Proof. + iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP & Hα) HΦ". + Admitted. + (* rewrite /incr_counter_tape3. *) + (* wp_pures. *) + (* wp_bind (rand(_) _)%E. *) + (* iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) + (* iDestruct (hocap_tapes_agree with "[$][$]") as "%". *) + (* erewrite <-(insert_delete m) at 1; last done. *) + (* rewrite big_sepM_insert; last apply lookup_delete. *) + (* simpl. *) + (* iDestruct "H3" as "[Htape H3]". *) + (* wp_apply (wp_rand_tape with "[$]"). *) + (* iIntros "[Htape %]". *) + (* iMod (hocap_tapes_pop with "[$][$]") as "[H4 Hα]". *) + (* iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". *) + (* { iSplitL; last done. *) + (* erewrite <-(insert_delete m) at 2; last done. *) + (* iNext. *) + (* rewrite insert_insert. *) + (* rewrite big_sepM_insert; last apply lookup_delete. iFrame. *) + (* } *) + (* iModIntro. *) + (* wp_pures. *) + (* clear -Hsubset. *) + (* wp_bind (FAA _ _). *) + (* iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) + (* wp_faa. *) + (* iMod ("Hvs" with "[$]") as "[H6 HQ]". *) + (* replace (#(z+n)) with (#(z+n)%nat); last first. *) + (* { by rewrite Nat2Z.inj_add. } *) + (* iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. *) + (* iModIntro. wp_pures. *) + (* iApply "HΦ". *) + (* by iFrame. *) + (* Qed. *) + + Lemma counter_presample_spec3 NS E ns α + (ε2 : R -> nat -> R) + (P : iProp Σ) T γ1 γ2 γ3 c: + ↑NS ⊆ E -> + (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> + (∀ (ε:R), 0<= ε ->SeriesC (λ n, if (bool_decide (n≤3%nat)) then 1 / (S 3%nat) * ε2 ε n else 0%R)%R <= ε)%R-> + inv NS (counter_inv_pred3 c γ1 γ2 γ3) -∗ + (□∀ (ε:R) n, (P ∗ ●↯ ε@ γ1) ={E∖↑NS}=∗ + (⌜(1<=ε2 ε n)%R⌝ ∨(●↯ (ε2 ε n) @ γ1 ∗ T (n)))) + -∗ + P -∗ α ◯↪N (3%nat; ns) @ γ2 -∗ + wp_update E (∃ n, T (n) ∗ α◯↪N (3%nat; ns++[n]) @ γ2). + Proof. + iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". + Admitted. + (* 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 "%". *) + (* erewrite <-(insert_delete m) at 1; last done. *) + (* rewrite big_sepM_insert; last apply lookup_delete. *) + (* simpl. *) + (* iDestruct "H3" as "[Htape H3]". *) + (* iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%)". *) + (* 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 state_step_coupl_state_adv_comp_con_prob_lang; first done. *) + (* unshelve iExists (λ x, mknonnegreal (ε2 ε1' x) _). *) + (* { apply Hpos. apply cond_nonneg. } *) + (* iSplit. *) + (* { iPureIntro. *) + (* unshelve epose proof (Hineq ε1' _) as H1; first apply cond_nonneg. *) + (* by rewrite SeriesC_nat_bounded_fin in H1. } *) + (* iIntros (sample). *) + + (* destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' sample))%R 1%R) as [Hdec|Hdec]; last first. *) + (* { apply Rnot_lt_ge, Rge_le in Hdec. *) + (* iApply state_step_coupl_ret_err_ge_1. *) + (* simpl. simpl in *. lra. *) + (* } *) + (* 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. } *) + (* iMod (tapeN_update_append _ _ _ _ sample with "[$][$]") as "[Htapes Htape]". *) + (* iMod (hocap_tapes_presample _ _ _ _ _ (fin_to_nat sample) with "[$][$]") as "[H4 Hfrag]". *) + (* iMod "Hclose'" as "_". *) + (* iMod ("Hvs" with "[$]") as "[%|[H2 HT]]". *) + (* { iExFalso. iApply (ec_contradict with "[$]"). exact. } *) + (* iMod ("Hclose" with "[$Hε $H2 Htape H3 $H4 $H5 $H6]") as "_". *) + (* { iNext. iSplit; last done. *) + (* rewrite big_sepM_insert_delete; iFrame. *) + (* } *) + (* iApply fupd_mask_intro_subseteq; first set_solver. *) + (* iFrame. *) + (* Qed. *) + + Lemma read_counter_spec3 N E c γ1 γ2 γ3 P Q: + ↑N ⊆ E -> + {{{ inv N (counter_inv_pred3 c γ1 γ2 γ3) ∗ + □ (∀ (z:nat), P ∗ own γ3 (●F z) ={E∖↑N}=∗ + own γ3 (●F z)∗ Q z) + ∗ P + }}} + read_counter3 c @ E + {{{ (n':nat), RET #n'; Q n' + }}}. + Proof. + iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP) HΦ". + rewrite /read_counter3. + wp_pure. + iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + wp_load. + iMod ("Hvs" with "[$]") as "[H6 HQ]". + iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]"); first done. + iApply ("HΦ" with "[$]"). + Qed. End impl3. From 1d4ccf61298d98c54ffc6edb2dfd116d478ec559 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 16 Sep 2024 14:42:48 +0200 Subject: [PATCH 04/10] instantiate impl3 as random_counter --- .../coneris/examples/random_counter/impl3.v | 107 ++++++++++++++++++ 1 file changed, 107 insertions(+) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index a5b6d1d1..ef6f5e80 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -221,3 +221,110 @@ Section impl3. Qed. End impl3. + + +Program Definition random_counter3 `{!conerisGS Σ}: random_counter := + {| new_counter := new_counter3; + allocate_tape:= allocate_tape3; + incr_counter_tape := incr_counter_tape3; + read_counter:=read_counter3; + counterG := counterG3; + error_name := gname; + tape_name := gname; + counter_name :=gname; + is_counter _ N c γ1 γ2 γ3 := inv N (counter_inv_pred3 c γ1 γ2 γ3); + counter_error_auth _ γ x := ●↯ x @ γ; + counter_error_frag _ γ x := ◯↯ x @ γ; + 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_spec3; + allocate_tape_spec _ :=allocate_tape_spec3; + incr_counter_tape_spec_some _ :=incr_counter_tape_spec_some3; + counter_presample_spec _ :=counter_presample_spec3; + read_counter_spec _ :=read_counter_spec3 + |}. +Next Obligation. + simpl. + iIntros (??????) "(%&<-&H1)(%&<-&H2)". + iCombine "H1 H2" gives "%H". by rewrite excl_auth.excl_auth_auth_op_valid in H. +Qed. +Next Obligation. + simpl. + iIntros (??????) "(%&<-&H1)(%&<-&H2)". + iCombine "H1 H2" gives "%H". by rewrite excl_auth.excl_auth_frag_op_valid in H. +Qed. +Next Obligation. + simpl. + iIntros (?????) "H". + iApply (hocap_error_auth_pos with "[$]"). +Qed. +Next Obligation. + simpl. + iIntros (?????) "H". + iApply (hocap_error_frag_pos with "[$]"). +Qed. +Next Obligation. + simpl. + iIntros (??????) "H1 H2". + iApply (hocap_error_agree with "[$][$]"). +Qed. +Next Obligation. + simpl. iIntros (???????) "??". + iApply (hocap_error_update with "[$][$]"). +Qed. +Next Obligation. + simpl. + iIntros (??????) "H1 H2". + by iDestruct (ghost_map_auth_valid_2 with "[$][$]") as "[%H _]". +Qed. +Next Obligation. + simpl. + 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. + iDestruct (hocap_tapes_agree with "[$][$]") as "%H". + iPureIntro. + rewrite lookup_fmap_Some in H. destruct H as (?&?&?). + by simplify_eq. +Qed. +Next Obligation. + iIntros. + iMod (hocap_tapes_presample with "[$][$]") as "[??]". + iModIntro. iFrame. + by rewrite fmap_insert. +Qed. +Next Obligation. + simpl. + iIntros (??????) "H1 H2". + iCombine "H1 H2" gives "%H". by rewrite auth_auth_op_valid in H. +Qed. +Next Obligation. + simpl. iIntros (???? z z' ?) "H1 H2". + iCombine "H1 H2" gives "%H". + apply frac_auth_included_total in H. iPureIntro. + by apply nat_included. +Qed. +Next Obligation. + simpl. + iIntros (????????). + rewrite frac_auth_frag_op. by rewrite own_op. +Qed. +Next Obligation. + simpl. iIntros (??????) "H1 H2". + iCombine "H1 H2" gives "%H". + iPureIntro. + by apply frac_auth_agree_L in H. +Qed. +Next Obligation. + simpl. iIntros (????????) "H1 H2". + iMod (own_update_2 _ _ _ (_ ⋅ _) with "[$][$]") as "[$$]"; last done. + apply frac_auth_update. + apply nat_local_update. lia. +Qed. + From 5aa3d88690156bac15358b6ea850adf2a70eff70 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 16 Sep 2024 15:06:32 +0200 Subject: [PATCH 05/10] incr_counter_tape_spec_some3 --- .../coneris/examples/random_counter/impl3.v | 89 ++++++++++++------- 1 file changed, 55 insertions(+), 34 deletions(-) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index ef6f5e80..55baabd4 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -106,40 +106,61 @@ Section impl3. {{{ (z:nat), RET (#z, #n); Q z ∗ α ◯↪N (3%nat; ns) @ γ2}}}. Proof. iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP & Hα) HΦ". - Admitted. - (* rewrite /incr_counter_tape3. *) - (* wp_pures. *) - (* wp_bind (rand(_) _)%E. *) - (* iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) - (* iDestruct (hocap_tapes_agree with "[$][$]") as "%". *) - (* erewrite <-(insert_delete m) at 1; last done. *) - (* rewrite big_sepM_insert; last apply lookup_delete. *) - (* simpl. *) - (* iDestruct "H3" as "[Htape H3]". *) - (* wp_apply (wp_rand_tape with "[$]"). *) - (* iIntros "[Htape %]". *) - (* iMod (hocap_tapes_pop with "[$][$]") as "[H4 Hα]". *) - (* iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". *) - (* { iSplitL; last done. *) - (* erewrite <-(insert_delete m) at 2; last done. *) - (* iNext. *) - (* rewrite insert_insert. *) - (* rewrite big_sepM_insert; last apply lookup_delete. iFrame. *) - (* } *) - (* iModIntro. *) - (* wp_pures. *) - (* clear -Hsubset. *) - (* wp_bind (FAA _ _). *) - (* iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) - (* wp_faa. *) - (* iMod ("Hvs" with "[$]") as "[H6 HQ]". *) - (* replace (#(z+n)) with (#(z+n)%nat); last first. *) - (* { by rewrite Nat2Z.inj_add. } *) - (* iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. *) - (* iModIntro. wp_pures. *) - (* iApply "HΦ". *) - (* by iFrame. *) - (* Qed. *) + rewrite /incr_counter_tape3. + iLöb as "IH". + wp_pures. + wp_bind (rand(_) _)%E. + iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + iDestruct (hocap_tapes_agree with "[$][$]") as "%". + erewrite <-(insert_delete m) at 1; last done. + rewrite big_sepM_insert; last apply lookup_delete. + simpl. + iDestruct "H3" as "[(%ls & %Hls & Htape) H3]". + destruct ls as [|x ls]. + { rewrite filter_nil in Hls. simplify_eq. } + wp_apply (wp_rand_tape with "[$]") as "[Htape %Hineq]". + rewrite Nat.le_lteq in Hineq. + destruct Hineq as [? | ->]. + - (* first value is valid *) + iMod (hocap_tapes_pop with "[$][$]") as "[H4 Hα]". + rewrite filter_cons /filter_f in Hls. + rewrite bool_decide_eq_true_2 in Hls; last done. simpl in *. + simplify_eq. + iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". + { iSplitL; last done. + erewrite <-(insert_delete m) at 2; last done. + iNext. + rewrite insert_insert. + rewrite big_sepM_insert; last apply lookup_delete. by iFrame. + } + iModIntro. + wp_pures. + rewrite bool_decide_eq_true_2; last lia. + clear -Hsubset. + wp_pures. + wp_bind (FAA _ _). + iInv N as ">(%ε & %m & % & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". + wp_faa. + iMod ("Hvs" with "[$]") as "[H6 HQ]". + replace (#(z+n)) with (#(z+n)%nat); last first. + { by rewrite Nat2Z.inj_add. } + iMod ("Hclose" with "[$H1 $H2 $H3 $H4 $H5 $H6]") as "_"; first done. + iModIntro. wp_pures. + iApply "HΦ". + by iFrame. + - (* we get a 5, do iLöb induction *) + rewrite filter_cons /filter_f in Hls. + rewrite bool_decide_eq_false_2 in Hls; last lia. simpl in *. + iMod ("Hclose" with "[$H1 $H2 H3 $H4 $H5 $H6 Htape]") as "_". + { iSplitL; last done. + erewrite <-(insert_delete m) at 2; last done. + iNext. + rewrite big_sepM_insert; last apply lookup_delete. by iFrame. + } + iModIntro. + do 4 wp_pure. + by iApply ("IH" with "[$][$]"). + Qed. Lemma counter_presample_spec3 NS E ns α (ε2 : R -> nat -> R) From 0741e0aab86cd6bba1d0772147c489e0cf6131cd Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 16 Sep 2024 15:17:57 +0200 Subject: [PATCH 06/10] NIT --- theories/coneris/examples/random_counter/impl3.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index 55baabd4..4e845736 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -176,6 +176,8 @@ Section impl3. wp_update E (∃ n, T (n) ∗ α◯↪N (3%nat; ns++[n]) @ γ2). Proof. iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". + (** why cant i do iMod? *) + (* iMod wp_update_epsilon_err as "H". *) Admitted. (* iApply wp_update_state_step_coupl. *) (* iIntros (σ ε) "((Hheap&Htapes)&Hε)". *) From 15d2ce0de32e7d7e6005c1fd202c07ffda6f5e2e Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 16 Sep 2024 15:32:05 +0200 Subject: [PATCH 07/10] nit --- theories/coneris/examples/random_counter/impl3.v | 3 +-- theories/coneris/wp_update.v | 6 ++++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index 4e845736..03648420 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -176,8 +176,7 @@ Section impl3. wp_update E (∃ n, T (n) ∗ α◯↪N (3%nat; ns++[n]) @ γ2). Proof. iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". - (** why cant i do iMod? *) - (* iMod wp_update_epsilon_err as "H". *) + iMod wp_update_epsilon_err as "H". Admitted. (* iApply wp_update_state_step_coupl. *) (* iIntros (σ ε) "((Hheap&Htapes)&Hε)". *) diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v index c183bffa..4626fc0a 100644 --- a/theories/coneris/wp_update.v +++ b/theories/coneris/wp_update.v @@ -137,6 +137,12 @@ Section wp_update. ElimModal True false false (wp_update E P) P (wp_update E Q) (wp_update E Q). Proof. iIntros (?) "[HP Hcnt]". by iApply (wp_update_bind with "[$]"). Qed. + Global Instance elim_modal_wp_update_wp_update' P Q E : + ElimModal True true false (wp_update E P) P (wp_update E Q) (wp_update E Q). + Proof. iIntros (?) "[HP Hcnt]". iApply (wp_update_bind with "[HP $Hcnt]"). + by iApply bi.intuitionistically_elim. + Qed. + Global Instance frame_wp_update p E R P Q: Frame p R P Q → Frame p R (wp_update E P) (wp_update E Q). Proof. From d80f8b5a6b7d25fed5eb1e0d8d8e9eed4f5dea4d Mon Sep 17 00:00:00 2001 From: Hei Li Date: Mon, 16 Sep 2024 15:45:38 +0200 Subject: [PATCH 08/10] NIT --- theories/coneris/wp_update.v | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/theories/coneris/wp_update.v b/theories/coneris/wp_update.v index 4626fc0a..e3472ce7 100644 --- a/theories/coneris/wp_update.v +++ b/theories/coneris/wp_update.v @@ -133,15 +133,13 @@ Section wp_update. FromModal True modality_id (wp_update E P) (wp_update E P) P. Proof. iIntros (_) "HP /=". by iApply wp_update_ret. Qed. - Global Instance elim_modal_wp_update_wp_update P Q E : - ElimModal True false false (wp_update E P) P (wp_update E Q) (wp_update E Q). - Proof. iIntros (?) "[HP Hcnt]". by iApply (wp_update_bind with "[$]"). Qed. - - Global Instance elim_modal_wp_update_wp_update' P Q E : - ElimModal True true false (wp_update E P) P (wp_update E Q) (wp_update E Q). - Proof. iIntros (?) "[HP Hcnt]". iApply (wp_update_bind with "[HP $Hcnt]"). - by iApply bi.intuitionistically_elim. - Qed. + Global Instance elim_modal_wp_update_wp_update b P Q E : + ElimModal True b false (wp_update E P) P (wp_update E Q) (wp_update E Q). + Proof. iIntros (?) "[HP Hcnt]". + destruct b. + - iApply (wp_update_bind); iFrame. + by iApply bi.intuitionistically_elim. + - by iApply (wp_update_bind with "[$]"). Qed. Global Instance frame_wp_update p E R P Q: Frame p R P Q → Frame p R (wp_update E P) (wp_update E Q). From b565698bbb3b55289cb9cce042fa3aa8bc8fc808 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 17 Sep 2024 10:24:50 +0200 Subject: [PATCH 09/10] Progress with counter_presample_spec3 --- .../coneris/examples/random_counter/impl3.v | 133 ++++++++++++------ 1 file changed, 90 insertions(+), 43 deletions(-) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index 03648420..aef9b112 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -176,50 +176,97 @@ Section impl3. wp_update E (∃ n, T (n) ∗ α◯↪N (3%nat; ns++[n]) @ γ2). Proof. iIntros (Hsubset Hpos Hineq) "#Hinv #Hvs HP Hfrag". - iMod wp_update_epsilon_err as "H". + iMod wp_update_epsilon_err as "(%epsilon_err&%H&?)". + iApply wp_update_state_step_coupl. + iRevert "HP Hfrag". + iApply (ec_ind_amp _ 5%R with "[][$]"); [done|lra|]. + iModIntro. + clear epsilon_err H. + iIntros (epsilon_err ?) "#IH Hepsilon_err HP Hfrag". + iIntros (σ ε) "((Hheap&Htapes)&Hε)". + iMod (inv_acc with "Hinv") as "[>(%ε0 & % & % & % & H1 & H2 & H3 & H4 & -> & H5 & H6) Hclose]"; [done|]. + iDestruct (hocap_tapes_agree with "[$][$]") as "%". + erewrite <-(insert_delete m) at 1; last done. + rewrite big_sepM_insert; last apply lookup_delete. + simpl. + iDestruct "H3" as "[(%ls & %Hls & Htape) H3]". + iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%)". + iDestruct (ec_valid with "H1") as "%". + iDestruct (ec_combine with "[$]") as "Htotal". + 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'". + pose (ε2' := λ (x:nat), (if bool_decide (x<=3)%nat then ε2 ε0 x else + if bool_decide (x=4)%nat then ε0 + 5 * epsilon_err + else 0)%R + ). + iApply state_step_coupl_state_adv_comp_con_prob_lang; first done. + assert (forall x, 0<=ε2' x)%R. + { intros. rewrite /ε2'. repeat case_bool_decide; try done; first naive_solver. + apply Rplus_le_le_0_compat; simpl; [naive_solver|lra]. } + unshelve iExists (λ x, mknonnegreal (ε2' x) _); auto. + simpl. + iSplit. + { admit. + (* iPureIntro. *) + (* unshelve epose proof (Hineq ε1' _) as H1; first apply cond_nonneg. *) + (* by rewrite SeriesC_nat_bounded_fin in H1. *) } + iIntros (sample). + simpl. + destruct (Rlt_decision (nonneg ε_rem + (ε2' sample))%R 1%R) as [Hdec|Hdec]; last first. + { apply Rnot_lt_ge, Rge_le in Hdec. + iApply state_step_coupl_ret_err_ge_1. + simpl. simpl in *. lra. + } + destruct (Nat.lt_total (fin_to_nat sample) 4%nat) as [|[|]]. + - (* we sample a value less than 4*) + iApply state_step_coupl_ret. + unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2' sample) _) with "Hε_supply") as "[Hε_supply Hε]"; auto. + iMod (tapeN_update_append _ _ _ _ sample with "[$][$]") as "[Htapes Htape]". + iMod (hocap_tapes_presample _ _ _ _ _ (fin_to_nat sample) with "[$][$]") as "[H4 Hfrag]". + iMod "Hclose'" as "_". + iMod ("Hvs" $! _ (fin_to_nat sample)%nat with "[$]") as "[%|[H2 HT]]". + { iExFalso. iApply (ec_contradict with "[$]"). + simpl. + rewrite /ε2'. + by rewrite bool_decide_eq_true_2; last lia. + } + simpl. + iMod ("Hclose" with "[$Hε H2 Htape H3 $H4 $H5 $H6]") as "_". + { iNext. + rewrite /ε2'. rewrite bool_decide_eq_true_2; last lia. + iFrame. + rewrite big_sepM_insert_delete; iFrame. simpl. iPureIntro. + split; last done. + rewrite filter_app. f_equal. + rewrite filter_cons. + rewrite decide_True; first done. + rewrite /filter_f. by apply bool_decide_pack. + } + iApply fupd_mask_intro_subseteq; first set_solver. + iFrame. + - (* we sampled a 4, and hence löb *) + unshelve iMod (ec_supply_increase _ (mknonnegreal (ε2' sample) _) with "Hε_supply") as "[Hε_supply Hε]"; auto. + iMod (tapeN_update_append _ _ _ _ sample with "[$][$]") as "[Htapes Htape]". + iMod "Hclose'" as "_". + simpl. + rewrite {2}/ε2'. + rewrite bool_decide_eq_false_2; last lia. + rewrite bool_decide_eq_true_2; last lia. + iDestruct (ec_split with "[$]") as "[Hε Hampl]"; simpl; [naive_solver|lra|]. + simpl. + iMod ("Hclose" with "[$Hε $H2 Htape H3 $H4 $H5 $H6]") as "_". + { iNext. + rewrite (big_sepM_delete _ m); [iFrame|done]. + simpl. iPureIntro; split; last done. + rewrite filter_app filter_cons decide_False; simpl. + - by rewrite filter_nil app_nil_r. + - rewrite /filter_f. case_bool_decide; [lia|auto]. + } + iDestruct ("IH" with "[$][$][$]") as "IH'". + by iMod ("IH'" $! (state_upd_tapes <[_:=_]> _) with "[$]") as "IH'". + - pose proof fin_to_nat_lt sample; lia. Admitted. - (* 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 "%". *) - (* erewrite <-(insert_delete m) at 1; last done. *) - (* rewrite big_sepM_insert; last apply lookup_delete. *) - (* simpl. *) - (* iDestruct "H3" as "[Htape H3]". *) - (* iDestruct (tapeN_lookup with "[$][$]") as "(%&%&%)". *) - (* 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 state_step_coupl_state_adv_comp_con_prob_lang; first done. *) - (* unshelve iExists (λ x, mknonnegreal (ε2 ε1' x) _). *) - (* { apply Hpos. apply cond_nonneg. } *) - (* iSplit. *) - (* { iPureIntro. *) - (* unshelve epose proof (Hineq ε1' _) as H1; first apply cond_nonneg. *) - (* by rewrite SeriesC_nat_bounded_fin in H1. } *) - (* iIntros (sample). *) - - (* destruct (Rlt_decision (nonneg ε_rem + (ε2 ε1' sample))%R 1%R) as [Hdec|Hdec]; last first. *) - (* { apply Rnot_lt_ge, Rge_le in Hdec. *) - (* iApply state_step_coupl_ret_err_ge_1. *) - (* simpl. simpl in *. lra. *) - (* } *) - (* 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. } *) - (* iMod (tapeN_update_append _ _ _ _ sample with "[$][$]") as "[Htapes Htape]". *) - (* iMod (hocap_tapes_presample _ _ _ _ _ (fin_to_nat sample) with "[$][$]") as "[H4 Hfrag]". *) - (* iMod "Hclose'" as "_". *) - (* iMod ("Hvs" with "[$]") as "[%|[H2 HT]]". *) - (* { iExFalso. iApply (ec_contradict with "[$]"). exact. } *) - (* iMod ("Hclose" with "[$Hε $H2 Htape H3 $H4 $H5 $H6]") as "_". *) - (* { iNext. iSplit; last done. *) - (* rewrite big_sepM_insert_delete; iFrame. *) - (* } *) - (* iApply fupd_mask_intro_subseteq; first set_solver. *) - (* iFrame. *) - (* Qed. *) Lemma read_counter_spec3 N E c γ1 γ2 γ3 P Q: ↑N ⊆ E -> From d6bf6939ea5d7bf8ce19047dcd010927a9373dd0 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Tue, 17 Sep 2024 10:34:32 +0200 Subject: [PATCH 10/10] impl3 --- .../coneris/examples/random_counter/impl3.v | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/theories/coneris/examples/random_counter/impl3.v b/theories/coneris/examples/random_counter/impl3.v index aef9b112..0abb395d 100644 --- a/theories/coneris/examples/random_counter/impl3.v +++ b/theories/coneris/examples/random_counter/impl3.v @@ -205,12 +205,17 @@ Section impl3. { intros. rewrite /ε2'. repeat case_bool_decide; try done; first naive_solver. apply Rplus_le_le_0_compat; simpl; [naive_solver|lra]. } unshelve iExists (λ x, mknonnegreal (ε2' x) _); auto. - simpl. iSplit. - { admit. - (* iPureIntro. *) - (* unshelve epose proof (Hineq ε1' _) as H1; first apply cond_nonneg. *) - (* by rewrite SeriesC_nat_bounded_fin in H1. *) } + { iPureIntro. + unshelve epose proof (Hineq ε0 _) as H'; first (by naive_solver). + rewrite SeriesC_nat_bounded_fin in H'. + replace (INR 5%nat) with 5%R by (simpl; lra). + replace (INR 4%nat) with 4%R in H' by (simpl; lra). + rewrite /=/ε2' Hε1'. + rewrite SeriesC_finite_foldr/=. + rewrite SeriesC_finite_foldr/= in H'. + lra. + } iIntros (sample). simpl. destruct (Rlt_decision (nonneg ε_rem + (ε2' sample))%R 1%R) as [Hdec|Hdec]; last first. @@ -266,7 +271,7 @@ Section impl3. iDestruct ("IH" with "[$][$][$]") as "IH'". by iMod ("IH'" $! (state_upd_tapes <[_:=_]> _) with "[$]") as "IH'". - pose proof fin_to_nat_lt sample; lia. - Admitted. + Qed. Lemma read_counter_spec3 N E c γ1 γ2 γ3 P Q: ↑N ⊆ E ->