From 22b341b000813adc84c42e0e879290a906e8fc4c Mon Sep 17 00:00:00 2001 From: Hei Li Date: Fri, 27 Sep 2024 13:39:36 +0200 Subject: [PATCH] fix spec of incr_counter_tape_spec_some --- .../coneris/examples/random_counter/impl1.v | 46 ++++++-------- .../examples/random_counter/random_counter.v | 61 +++++++++++-------- 2 files changed, 55 insertions(+), 52 deletions(-) diff --git a/theories/coneris/examples/random_counter/impl1.v b/theories/coneris/examples/random_counter/impl1.v index 15bee9d8..2414dfa3 100644 --- a/theories/coneris/examples/random_counter/impl1.v +++ b/theories/coneris/examples/random_counter/impl1.v @@ -8,8 +8,8 @@ Section impl1. Context `{H:conerisGS Σ, r1:@rand_spec Σ H, L:randG Σ, !inG Σ (frac_authR natR)}. Definition new_counter1 : val:= λ: "_", ref #0. - Definition allocate_tape1 : val := λ: "_", rand_allocate_tape #3. - Definition incr_counter_tape1 :val := λ: "l" "α", let: "n" := rand_tape "α" #3 in (FAA "l" "n", "n"). + Definition allocate_tape1 : val := λ: "_", rand_allocate_tape #3%nat. + Definition incr_counter_tape1 :val := λ: "l" "α", let: "n" := rand_tape "α" #3%nat in (FAA "l" "n", "n"). Definition read_counter1 : val := λ: "l", !"l". Class counterG1 Σ := CounterG1 { counterG1_randG : randG Σ; counterG1_frac_authR:: inG Σ (frac_authR natR) }. @@ -91,38 +91,31 @@ Section impl1. ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ rand_tapes_frag (L:=L) γ1 α (3%nat, []) }}}. Proof. - Admitted. - (* iIntros (Hsubset Φ) "#Hinv HΦ". *) - (* rewrite /allocate_tape1. *) - (* wp_pures. *) - (* wp_alloctape α as "Hα". *) - (* iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) - (* iDestruct (hocap_tapes_notin 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]. *) - (* } *) - (* iApply "HΦ". *) - (* by iFrame. *) - (* Qed. *) + iIntros (Hsubset Φ) "[#Hinv #Hinv'] HΦ". + rewrite /allocate_tape1. + wp_pures. + wp_apply rand_allocate_tape_spec; [by eapply nclose_subseteq'|done..]. + Qed. Lemma incr_counter_tape_spec_some1 N E c γ1 γ2 (Q:nat->nat -> list nat -> iProp Σ) (α:loc) : ↑N⊆E -> {{{ is_counter1 N c γ1 γ2 ∗ - (∀ (z:nat), own γ2 (●F z) ={E∖ ↑N, ∅}=∗ - ∃ n ns, rand_tapes_frag (L:=L) γ1 α (3%nat, n::ns) ∗ - (rand_tapes_frag (L:=L) γ1 α (3%nat, ns) ={∅, E∖↑N}=∗ - own γ2 (●F (z+n)%nat) ∗ Q z n ns) + ( |={E∖ ↑N, ∅}=> + ∃ n ns, rand_tapes_frag (L:=L) γ1 α (3, n::ns) ∗ + (rand_tapes_frag (L:=L) γ1 α (3, ns) ={∅, E∖↑N}=∗ + ∀ (z:nat), own γ2 (●F z) + ={E∖↑N}=∗ + own γ2 (●F (z+n)) ∗ Q z n ns) ) }}} incr_counter_tape1 c #lbl:α @ E {{{ (z n:nat), RET (#z, #n); ∃ ns, Q z n ns}}}. Proof. - Admitted. - (* iIntros (Hsubset Φ) "(#Hinv & #Hvs & HP & Hα) HΦ". *) - (* rewrite /incr_counter_tape1. *) - (* wp_pures. *) + iIntros (Hsubset Φ) "([#Hinv #Hinv'] & Hvs) HΦ". + rewrite /incr_counter_tape1. + wp_pures. + wp_apply (rand_tape_spec_some with "[Hvs]"); [by eapply nclose_subseteq'|iSplit; first done|..]. + (* - iSplit *) (* wp_bind (rand(_) _)%E. *) (* iInv N as ">(%ε & %m & %l & %z & H1 & H2 & H3 & H4 & -> & H5 & H6)" "Hclose". *) (* iDestruct (hocap_tapes_agree with "[$][$]") as "%". *) @@ -153,7 +146,8 @@ Section impl1. (* iModIntro. wp_pures. *) (* iApply "HΦ". *) (* by iFrame. *) - (* Qed. *) + (* Qed. *) + Admitted. Lemma counter_presample_spec1 NS E T γ1 γ2 c: ↑NS ⊆ E -> diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v index 54051f64..d7885d8f 100644 --- a/theories/coneris/examples/random_counter/random_counter.v +++ b/theories/coneris/examples/random_counter/random_counter.v @@ -77,10 +77,12 @@ Class random_counter `{!conerisGS Σ} := RandCounter incr_counter_tape_spec_some {L: counterG Σ} N E c γ1 γ2 (Q:nat->nat->list nat->iProp Σ) (α:loc) : ↑N⊆E -> {{{ is_counter (L:=L) N c γ1 γ2 ∗ - (∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖ ↑N, ∅}=∗ + ( |={E∖ ↑N, ∅}=> ∃ n ns, counter_tapes_frag (L:=L) γ1 α (n::ns) ∗ (counter_tapes_frag (L:=L) γ1 α ns ={∅, E∖↑N}=∗ - counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ns) + ∀ (z:nat), counter_content_auth (L:=L) γ2 z + ={E∖↑N}=∗ + counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ns) ) }}} incr_counter_tape c #lbl:α @ E @@ -121,14 +123,15 @@ Section lemmas. ↯ ε ∗ counter_tapes_frag (L:=L) γ1 α [] ∗ ⌜(∀ n, 0<=ε2 n)%R⌝ ∗ ⌜(((ε2 0%nat) + (ε2 1%nat)+ (ε2 2%nat)+ (ε2 3%nat))/4 <= ε)%R⌝ ∗ - (∀ n, ↯ (ε2 n) ∗ counter_tapes_frag (L:=L) γ1 α [n] ={∅,E∖↑N}=∗ - ∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖↑N, ∅}=∗ - counter_tapes_frag (L:=L) γ1 α [n]∗ - (counter_tapes_frag (L:=L) γ1 α []={∅, E∖↑N}=∗ - counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ε ε2 + (∀ n, ↯ (ε2 n) ∗ counter_tapes_frag (L:=L) γ1 α [n] ={∅, E∖↑N}=∗ + |={E∖↑N, ∅}=> + counter_tapes_frag (L:=L) γ1 α [n] ∗ + (counter_tapes_frag (L:=L) γ1 α [] ={∅,E∖↑N}=∗ + ∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖↑N}=∗ + counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ε ε2 + ) ) - ) - ) + ) }}} incr_counter_tape c #lbl:α @ E {{{ (z n:nat), RET (#z, #n); ∃ ε ε2, Q z n ε ε2 }}}. @@ -138,13 +141,15 @@ Section lemmas. (λ ε α' ε2 num ns ns', ∃ n ε2', ⌜num=1%nat⌝ ∗ ⌜α'=α⌝ ∗ ⌜ns=[]⌝ ∗ ⌜ns'=[n]⌝ ∗ - ⌜(ε2' = λ x, ε2 [x])%R⌝ ∗ - (∀ z : nat, - counter_content_auth γ2 z ={E ∖ ↑N,∅}=∗ - counter_tapes_frag γ1 α [n] ∗ - (counter_tapes_frag γ1 α [] ={∅,E ∖ ↑N}=∗ - counter_content_auth γ2 (z + n) ∗ Q z n ε ε2')) - )%I with "[//][-HΦ]") as "(%ε & % & %ε2 & %num & %ns & %ns' & %n & %ε2' & -> & -> & -> & -> & -> & Hrest)"; try done. + ⌜(ε2' = λ x, ε2 [x])%R⌝ ∗ + ( |={E∖ ↑N, ∅}=> + counter_tapes_frag (L:=L) γ1 α [n] ∗ + (counter_tapes_frag (L:=L) γ1 α [] ={∅, E∖↑N}=∗ + ∀ (z:nat), counter_content_auth (L:=L) γ2 z + ={E∖↑N}=∗ + counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ε ε2') + ) + )%I with "[//][-HΦ]") as "(%ε & % & %ε2 & %num & %ns & %ns' & %n & %ε2' & -> & -> & -> & -> & -> & Hrest)"; first done. - iMod "Hvs" as "(%ε & %ε2 & Herr & Hfrag & %Hpos & %Hineq & Hrest)". iFrame. iModIntro. iExists (λ l, match l with |[x] => ε2 x | _ => 1 end)%R, 1%nat. @@ -157,17 +162,19 @@ Section lemmas. * apply NoDup_fmap_2; last apply NoDup_enum_uniform_fin_list. apply list_fmap_eq_inj, fin_to_nat_inj. + iIntros (ns') "[Herr Hfrag]". destruct (ns') as [|n[|??]]; [by iDestruct (ec_contradict with "[$]") as "%"| |by iDestruct (ec_contradict with "[$]") as "%"]. - iMod ("Hrest" $! n with "[$]"). - iFrame. - by iPureIntro. + iMod ("Hrest" $! n with "[$]") as "?". + iModIntro. + by iFrame. - wp_apply (incr_counter_tape_spec_some _ _ _ _ _ (λ z n ns, ∃ ε ε2, Q z n ε ε2)%I with "[Hrest]"); first exact. + iSplit; first done. - iIntros (z) "Hauth". - iMod ("Hrest" with "[$]") as "[Hfrag Hrest]". + iMod "Hrest" as "[? Hrest]". iFrame. iModIntro. - iIntros "Hfrag". - iMod ("Hrest" with "[$]") as "[Hauth HQ]". + iIntros. + iMod ("Hrest" with "[$]") as "Hrest". + iModIntro. + iIntros (z) "Hauth". + iMod ("Hrest" with "[$]") as "[??]". by iFrame. + iIntros (??) "(%&%&%&HQ)". iApply "HΦ". @@ -211,18 +218,20 @@ Section lemmas. + iIntros (n) "[Herr Hfrag]". iMod "Hclose" as "_". iModIntro. - iIntros (z') "Hauth". iApply fupd_mask_intro; first set_solver. iIntros "Hclose". rewrite /ε2'. case_match eqn:H; last by (iDestruct (ec_contradict with "[$]") as "%"). iFrame. iIntros "Hfrag'". - iDestruct (counter_content_less_than with "[$][$]") as "%". - iMod (counter_content_update with "[$][$]") as "[??]". iMod "Hclose" as "_". iFrame. apply leb_complete in H. + iModIntro. + iIntros (z') "Hauth". + iDestruct (counter_content_less_than with "[$][$]") as "%". + iMod (counter_content_update with "[$][$]") as "[??]". + iFrame. iPureIntro; repeat split; try done; lia. - iIntros (z' n) "(%ε' & %ε2'' & % & % &-> & -> & Herr & Hfrag & Hfrag')". iApply "HΦ".