Skip to content

Commit

Permalink
conprog use the states in coneris paper
Browse files Browse the repository at this point in the history
  • Loading branch information
@hei411
hei411 committed Jan 17, 2025
1 parent 95edd74 commit 574dad2
Show file tree
Hide file tree
Showing 2 changed files with 320 additions and 536 deletions.
221 changes: 4 additions & 217 deletions theories/coneris/examples/parallel_add.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Local Open Scope Z.

Set Default Proof Using "Type*".


Section lemmas.
Context `{!inG Σ (excl_authR boolO)}.

Expand Down Expand Up @@ -33,7 +34,7 @@ Section lemmas.
{ by apply excl_auth_update. }
done.
Qed.

Local Lemma resource_nonneg (b:bool): (0 <= 1 - Rpower 2 (bool_to_nat b - 1))%R.
Proof.
destruct b as [|]; simpl.
Expand Down Expand Up @@ -134,7 +135,6 @@ Section lemmasfrac.
Qed.
End lemmasfrac.


Section simple_parallel_add.
Definition simple_parallel_add : expr :=
let: "r" := ref #0 in
Expand Down Expand Up @@ -542,221 +542,8 @@ Section attempt1.
Qed.
End attempt1.

(* A hocap style spec for half_FAA*)
Definition loc_nroot:=nroot.@"loc".
Definition both_nroot:=nroot.@"both".
(* Section attempt2. *)
(* Context `{!conerisGS Σ, !spawnG Σ, !hocap_errorGS Σ, !inG Σ (excl_authR ZR), !inG Σ (excl_authR (optionO boolO))}. *)

(* Definition loc_inv (l:loc) γ:= *)
(* inv loc_nroot (∃ (z:Z), l↦#z ∗ own γ (●E z)). *)
(* Lemma wp_half_FAA E *)
(* (ε2 : R -> bool -> R) *)
(* (P Q : iProp Σ) (T : bool -> iProp Σ) γ1 γ2 (l:loc): *)
(* ↑hocap_error_nroot ⊆ E -> *)
(* ↑loc_nroot ⊆ E -> *)
(* (∀ ε b, 0<= ε -> 0<= ε2 ε b)%R-> *)
(* (∀ (ε:R), 0<=ε -> (((ε2 ε true) + (ε2 ε false))/2 <= (ε)))%R → *)
(* {{{ error_inv γ1 ∗ loc_inv l γ2 ∗ *)
(* □(∀ (ε:R) (b : bool), P ∗ ●↯ ε @ γ1 ={E∖↑hocap_error_nroot}=∗ (⌜(1<=ε2 ε b)%R⌝∨●↯ (ε2 ε b) @ γ1 ∗ T b) ) ∗ *)
(* □ (∀ (b:bool) (z:Z), T b ∗ own γ2 (●E z) ={E∖↑loc_nroot}=∗ *)
(* if b then own γ2 (●E(z+1)%Z)∗ Q else own γ2 (●E(z))∗ Q ) ∗ *)
(* P }}} half_FAA l @ E {{{ (v: val), RET v; Q }}}. *)
(* Proof. *)
(* iIntros (Hsubset1 Hsubset2 ? Hineq Φ) "(#Hinv1 & #Hinv2 & #Hchange1 & #Hchange2 & HP) HΦ". *)
(* rewrite /half_FAA. *)
(* wp_apply (wp_hocap_flip_adv_comp _ ε2 P with "[-HΦ]"); [done|..]. *)
(* - intros. naive_solver. *)
(* - simpl. intros; naive_solver. *)
(* - by repeat iSplit. *)
(* - iIntros. destruct b. *)
(* + wp_pures. iInv "Hinv2" as "(%&?&?)" "Hclose". *)
(* wp_faa. *)
(* iMod ("Hchange2" with "[$]") as "[??]". *)
(* iMod ("Hclose" with "[$]"). *)
(* by iApply "HΦ". *)
(* + iInv "Hinv2" as "(%&?&?)" "Hclose". *)
(* wp_pure. *)
(* iMod ("Hchange2" with "[$]") as "[??]". *)
(* iMod ("Hclose" with "[$]"). *)
(* by iApply "HΦ". *)
(* Qed. *)

(* Lemma parallel_add_spec'': *)
(* {{{ ↯ (3/4) }}} *)
(* parallel_add *)
(* {{{ (z:Z), RET #z; ⌜(z=2)⌝ }}}. *)
(* Proof. *)
(* iIntros (Φ) "Herr HΦ". *)
(* rewrite /parallel_add. *)
(* wp_alloc l as "Hl". *)
(* wp_pures. *)
(* rewrite -/(half_FAA l). *)
(* (** Allocate hocap error*) *)
(* unshelve iMod (hocap_error_alloc (mknonnegreal (3/4) _)) as "(%γ1 & Hεauth & Hεfrag)". *)
(* { lra. } *)
(* simpl. *)
(* (** Allocate hocap heap *) *)
(* iMod (own_alloc ((●E 0) ⋅ (◯E 0))) as "[%γ2 [Hauth_loc Hfrag_loc]]". *)
(* { by apply excl_auth_valid. } *)
(* (** Allocate hocap for tracking contributions *) *)
(* iMod (own_alloc ((●E None) ⋅ (◯E None))) as "[%γ3 [Hauth_a Hfrag_a]]". *)
(* { by apply excl_auth_valid. } *)
(* iMod (own_alloc ((●E None) ⋅ (◯E None))) as "[%γ4 [Hauth_b Hfrag_b]]". *)
(* { by apply excl_auth_valid. } *)
(* (** Allocate error invariants *) *)
(* iMod (inv_alloc hocap_error_nroot _ ((∃ (ε:R), ↯ ε ∗ ●↯ ε @ γ1)) with "[Herr Hεauth]") as "#Hεinv". *)
(* { iExists (mknonnegreal (3/4) _); iFrame. *)
(* Unshelve. lra. } *)
(* (** Allocate location inv *) *)
(* iMod (inv_alloc loc_nroot _ (∃ (z:Z), l↦#z ∗ own γ2 (●E z) *)
(* ) with "[Hl Hauth_loc]") as "#Hlocinv". *)
(* { iFrame. } *)
(* iMod (inv_alloc both_nroot _ *)
(* (∃ (z:Z) (a b:option bool), own γ2 (◯E z) ∗ *)
(* own γ3 (●E a) ∗ *)
(* own γ4 (●E b) ∗ *)
(* ⌜(z=bool_to_Z (is_Some_true a) + bool_to_Z (is_Some_true b))%Z⌝ ∗ *)
(* ◯↯ (1-Rpower 2 (IZR (bool_to_Z (bool_decide (is_Some a)))+IZR (bool_to_Z (bool_decide (is_Some b)))-2))%R@ γ1) *)
(* with "[Hfrag_loc Hεfrag Hauth_a Hauth_b]") as "#Hinvboth". *)
(* { iFrame. simpl. iModIntro. iSplitR; first by iPureIntro. *)
(* replace (1-_)%R with (3/4)%R; first done. *)
(* replace (Rpower _ _) with (1/4)%R; try lra. *)
(* replace (0+0-2)%R with (-2)%R by lra. *)
(* rewrite Rpower_Ropp/ Rpower. replace (IPR 2) with (INR 2); last done. *)
(* rewrite -ln_pow; last lra. *)
(* rewrite exp_ln; lra. *)
(* } *)
(* wp_apply (wp_par (λ _, own γ3 (◯E (Some true)))(λ _, own γ4 (◯E (Some true))) with "[Hfrag_a][Hfrag_b]"). *)
(* - (* first branch *) *)
(* wp_apply (wp_half_FAA _ (λ x b, *)
(* match ClassicalEpsilon.excluded_middle_informative (1/2<=x)%R *)
(* with *)
(* | left P => if b then (2*x - 1)%R else 1%R *)
(* | _ => x *)
(* end ) (own γ3 (◯E None)) *)
(* (own γ3 (◯E (Some true))) *)
(* (λ b, ⌜b=true⌝ ∗ (own γ3 (◯E (Some false))))%I γ1 γ2 l with "[$Hfrag_a]"); [done|done|..]. *)
(* + intros; repeat case_match; lra. *)
(* + intros. case_match; simpl; lra. *)
(* + repeat iSplit. *)
(* * done. *)
(* * done. *)
(* * iModIntro. iIntros (ε res) "[Hfrag_a Hεauth]". *)
(* iInv both_nroot as ">(%z & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". *)
(* iDestruct (hocap_error_agree with "[$][$]") as "%K". *)
(* iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". *)
(* simpl in *. *)
(* case_match; last first. *)
(* { exfalso. apply n. *)
(* simpl in *. *)
(* rewrite K. *)
(* assert (Rpower 2 (0+IZR (bool_to_Z (bool_decide (is_Some b))) - 2) <= 1/2)%R; try lra. *)
(* replace (_/_)%R with (/2) by lra. *)
(* rewrite -{3}(Rpower_1 2); last lra. *)
(* rewrite -Rpower_Ropp. *)
(* apply Rle_Rpower; first lra. *)
(* case_bool_decide; simpl; lra. *)
(* } *)
(* iMod (ghost_var_update' _ (Some false) with "[$Hauth_a][$]") as "[Hauth_a Hfrag_a]". *)
(* iMod (hocap_error_update _ (mknonnegreal _ _)with "[$][$]") as "[Hεauth Hεfrag]". *)
(* simpl. *)
(* iMod ("Hclose" with "[Hloc_frag Hauth_a Hauth_b Hεfrag]"); iFrame; first done. *)
(* simpl. case_match; last first. *)
(* { iLeft. done. } *)
(* iRight. iFrame. iModIntro; iSplitL; last done. *)
(* simpl. rewrite K. *)
(* iApply (hocap_error_irrel with "[$]"). *)
(* rewrite !Rpower_plus Rpower_O; last lra. *)
(* rewrite Rpower_1; lra. *)
(* * iModIntro. *)
(* iIntros (??) "[[-> Hfrag_a] Hauth_loc]". *)
(* iInv both_nroot as ">(% & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". *)
(* iDestruct (ghost_var_agreeZ with "[$][$]") as "->". *)
(* iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". *)
(* iMod (ghost_var_updateZ with "[$][$]") as "[Hauth_loc Hfrag_loc]". *)
(* iMod (ghost_var_update' _ (Some true) with "[$Hauth_a][$]") as "[Hauth_a Hfrag_a]". *)
(* simpl. *)
(* iMod ("Hclose" with "[$Hfrag_loc $Hauth_a $Hauth_b $Hεfrag]") as "_"; first done. *)
(* iFrame. simpl. *)
(* iModIntro. *)
(* replace (0+_+1)%Z with (1+bool_to_Z (is_Some_true b)); [done|lia]. *)
(* + iIntros. done. *)
(* - (* first branch *) *)
(* wp_apply (wp_half_FAA _ (λ x b, *)
(* match ClassicalEpsilon.excluded_middle_informative (1/2<=x)%R *)
(* with *)
(* | left P => if b then (2*x - 1)%R else 1%R *)
(* | _ => x *)
(* end ) (own γ4 (◯E None)) *)
(* (own γ4 (◯E (Some true))) *)
(* (λ b, ⌜b=true⌝ ∗ (own γ4 (◯E (Some false))))%I γ1 γ2 l with "[$Hfrag_b]"); [done|done|..]. *)
(* + intros; repeat case_match; lra. *)
(* + intros. case_match; simpl; lra. *)
(* + repeat iSplit. *)
(* * done. *)
(* * done. *)
(* * iModIntro. iIntros (ε res) "[Hfrag_b Hεauth]". *)
(* iInv both_nroot as ">(%z & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". *)
(* iDestruct (hocap_error_agree with "[$][$]") as "%K". *)
(* iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". *)
(* simpl in *. *)
(* case_match; last first. *)
(* { exfalso. apply n. *)
(* simpl in *. *)
(* rewrite K. *)
(* assert (Rpower 2 (IZR (bool_to_Z (bool_decide (is_Some a)))+0 - 2) <= 1/2)%R; try lra. *)
(* replace (_/_)%R with (/2) by lra. *)
(* rewrite -{3}(Rpower_1 2); last lra. *)
(* rewrite -Rpower_Ropp. *)
(* apply Rle_Rpower; first lra. *)
(* case_bool_decide; simpl; lra. *)
(* } *)
(* iMod (ghost_var_update' _ (Some false) with "[$Hauth_b][$]") as "[Hauth_b Hfrag_b]". *)
(* iMod (hocap_error_update _ (mknonnegreal _ _)with "[$][$]") as "[Hεauth Hεfrag]". *)
(* simpl. *)
(* iMod ("Hclose" with "[Hloc_frag Hauth_a Hauth_b Hεfrag]"); iFrame; first done. *)
(* simpl. case_match; last first. *)
(* { iLeft. done. } *)
(* iRight. iFrame. iModIntro; iSplitL; last done. *)
(* simpl. rewrite K. *)
(* iApply (hocap_error_irrel with "[$]"). *)
(* rewrite !Rpower_plus Rpower_O; last lra. *)
(* rewrite Rpower_1; lra. *)
(* * iModIntro. *)
(* iIntros (??) "[[-> Hfrag_a] Hauth_loc]". *)
(* iInv both_nroot as ">(% & %a & %b & Hloc_frag & Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose". *)
(* iDestruct (ghost_var_agreeZ with "[$][$]") as "->". *)
(* iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". *)
(* iMod (ghost_var_updateZ with "[$][$]") as "[Hauth_loc Hfrag_loc]". *)
(* iMod (ghost_var_update' _ (Some true) with "[$Hauth_b][$]") as "[Hauth_b Hfrag_b]". *)
(* simpl. *)
(* iMod ("Hclose" with "[$Hfrag_loc $Hauth_a $Hauth_b $Hεfrag]") as "_"; first done. *)
(* iFrame. simpl. *)
(* iModIntro. *)
(* replace (_+0+1)%Z with (bool_to_Z (is_Some_true a)+1); [done|lia]. *)
(* + iIntros. done. *)
(* - iIntros (??) "[Hfrag_a Hfrag_b]". iModIntro. wp_pures. *)
(* iInv loc_nroot as ">(%&Hl&Hloc_auth)" "Hclose". *)
(* iInv both_nroot as ">(%&%&%&Hloc_frag&Hauth_a & Hauth_b & -> & Hεfrag)" "Hclose'". *)
(* iDestruct (ghost_var_agreeZ with "[$][$]") as "->". *)
(* iDestruct (ghost_var_agree' with "[$Hauth_a][$]") as "->". *)
(* iDestruct (ghost_var_agree' with "[$Hauth_b][$]") as "->". *)
(* simpl. *)
(* wp_load. *)
(* iMod ("Hclose'" with "[$Hloc_frag $Hauth_a $Hauth_b $Hεfrag]"); first done. *)
(* iModIntro. *)
(* iMod ("Hclose" with "[Hl Hloc_auth]"); first by iFrame. *)
(* by iApply "HΦ". *)
(* Unshelve. *)
(* all: simpl; try lra. *)
(* + replace (1+_-2)%R with (INR (bool_to_nat (bool_decide (is_Some b)))-1)%R; first apply resource_nonneg. *)
(* case_bool_decide; simpl; lra. *)
(* + replace (_+1-2)%R with (INR (bool_to_nat (bool_decide (is_Some a)))-1)%R; first apply resource_nonneg. *)
(* case_bool_decide; simpl; lra. *)
(* Qed. *)
(* End attempt2. *)

Definition loc_nroot:=nroot.@"loc".
Definition both_nroot:=nroot.@"both".

Definition half_FAA' (l:loc) α:=
(if: flipL #lbl:α then FAA #l #1 else #())%E.
Expand Down
Loading

0 comments on commit 574dad2

Please sign in to comment.