Commit e3601a05 authored by Ralf Jung's avatar Ralf Jung

bump Iris, update for frac_auth notation

parent 2d178e1e
Pipeline #17672 canceled with stage
in 2 minutes and 38 seconds
...@@ -131,7 +131,7 @@ Section proof3. ...@@ -131,7 +131,7 @@ Section proof3.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (frac_authR natR)}. Context `{!heapG Σ, !spawnG Σ, !inG Σ (frac_authR natR)}.
Definition parallel_add_inv_3 (r : loc) (γ : gname) : iProp Σ := Definition parallel_add_inv_3 (r : loc) (γ : gname) : iProp Σ :=
( n : nat, r #n own γ (! n))%I. ( n : nat, r #n own γ (F n))%I.
(** *Exercise*: finish the missing cases of the proof. *) (** *Exercise*: finish the missing cases of the proof. *)
Lemma parallel_add_spec_3 : Lemma parallel_add_spec_3 :
...@@ -139,17 +139,17 @@ Section proof3. ...@@ -139,17 +139,17 @@ Section proof3.
Proof. Proof.
iIntros (Φ) "_ Post". iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let. unfold parallel_add. wp_alloc r as "Hr". wp_let.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]". iMod (own_alloc (F 0%nat F 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
{ by apply auth_both_valid. } { by apply auth_both_valid. }
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]"). wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *) { (* exercise *)
admit. } admit. }
iIntros (l) "#Hl". wp_let. iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat)) wp_apply (wp_par (λ _, own γ (F{1/2} 2%nat)) (λ _, own γ (F{1/2} 2%nat))
with "[Hγ1◯] [Hγ2◯]"). with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]". - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store. wp_seq. wp_load. wp_op. wp_store.
iMod (own_update_2 _ _ _ (! (n+2) !{1/2}2)%nat with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]". iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2)%nat with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]".
{ rewrite (comm plus). { rewrite (comm plus).
by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. } by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. }
wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto]. wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto].
......
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [] # This repo does not install install: [] # This repo does not install
remove: [] remove: []
depends: [ depends: [
"coq-iris" { (= "dev.2019-05-24.0.c9984c7f") | (= "dev") } "coq-iris" { (= "dev.2019-06-11.8.a51fa3cf") | (= "dev") }
] ]
...@@ -144,7 +144,7 @@ Section proof3. ...@@ -144,7 +144,7 @@ Section proof3.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (frac_authR natR)}. Context `{!heapG Σ, !spawnG Σ, !inG Σ (frac_authR natR)}.
Definition parallel_add_inv_3 (r : loc) (γ : gname) : iProp Σ := Definition parallel_add_inv_3 (r : loc) (γ : gname) : iProp Σ :=
( n : nat, r #n own γ (! n))%I. ( n : nat, r #n own γ (F n))%I.
(** *Exercise*: finish the missing cases of the proof. *) (** *Exercise*: finish the missing cases of the proof. *)
Lemma parallel_add_spec_3 : Lemma parallel_add_spec_3 :
...@@ -152,16 +152,16 @@ Section proof3. ...@@ -152,16 +152,16 @@ Section proof3.
Proof. Proof.
iIntros (Φ) "_ Post". iIntros (Φ) "_ Post".
unfold parallel_add. wp_alloc r as "Hr". wp_let. unfold parallel_add. wp_alloc r as "Hr". wp_let.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]". iMod (own_alloc (F 0%nat F 0%nat)) as (γ) "[Hγ● [Hγ1◯ Hγ2◯]]".
{ by apply auth_both_valid. } { by apply auth_both_valid. }
wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]"). wp_apply (newlock_spec (parallel_add_inv_3 r γ) with "[Hr Hγ●]").
{ (* exercise *) iExists 0%nat. iFrame. } { (* exercise *) iExists 0%nat. iFrame. }
iIntros (l) "#Hl". wp_let. iIntros (l) "#Hl". wp_let.
wp_apply (wp_par (λ _, own γ (!{1/2} 2%nat)) (λ _, own γ (!{1/2} 2%nat)) wp_apply (wp_par (λ _, own γ (F{1/2} 2%nat)) (λ _, own γ (F{1/2} 2%nat))
with "[Hγ1◯] [Hγ2◯]"). with "[Hγ1◯] [Hγ2◯]").
- wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]". - wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store. wp_seq. wp_load. wp_op. wp_store.
iMod (own_update_2 _ _ _ (! (n+2) !{1/2}2)%nat with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]". iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2)%nat with "Hγ● Hγ1◯") as "[Hγ● Hγ1◯]".
{ rewrite (comm plus). { rewrite (comm plus).
by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. } by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. }
wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto]. wp_apply (release_spec with "[$Hl Hr Hγ●]"); [|by auto].
...@@ -169,7 +169,7 @@ Section proof3. ...@@ -169,7 +169,7 @@ Section proof3.
- (* exercise *) - (* exercise *)
wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]". wp_apply (acquire_spec with "Hl"). iDestruct 1 as (n) "[Hr Hγ●]".
wp_seq. wp_load. wp_op. wp_store. wp_seq. wp_load. wp_op. wp_store.
iMod (own_update_2 _ _ _ (! (n+2) !{1/2}2)%nat with "Hγ● Hγ2◯") as "[Hγ● Hγ2◯]". iMod (own_update_2 _ _ _ (F (n+2) F{1/2}2)%nat with "Hγ● Hγ2◯") as "[Hγ● Hγ2◯]".
{ rewrite (comm plus). { rewrite (comm plus).
by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. } by apply frac_auth_update, (op_local_update_discrete n 0 2)%nat. }
wp_apply (release_spec with "[- $Hl Hγ2◯]"); [|by auto]. wp_apply (release_spec with "[- $Hl Hγ2◯]"); [|by auto].
......
...@@ -54,23 +54,23 @@ Section proof2. ...@@ -54,23 +54,23 @@ Section proof2.
(* Rules for fractional ghost variables (* Rules for fractional ghost variables
(proved from generic principles) *) (proved from generic principles) *)
Lemma frac_auth_alloc n : Lemma frac_auth_alloc n :
(|==> γ, own γ (! n) own γ (!{1} n))%I. (|==> γ, own γ (F n) own γ (F{1} n))%I.
Proof. Proof.
by iMod (own_alloc (! n ! n)) by iMod (own_alloc (F n F n))
as (γ) "[??]"; eauto with iFrame. as (γ) "[??]"; eauto with iFrame.
Qed. Qed.
Lemma frac_auth_update n n1 n2 q γ : Lemma frac_auth_update n n1 n2 q γ :
own γ (! n1) - own γ (F n1) -
own γ (!{q} n2) - |==> own γ (F{q} n2) - |==>
own γ (! (n1 + n)%nat) own γ (!{q} (n2 + n)%nat). own γ (F (n1 + n)%nat) own γ (F{q} (n2 + n)%nat).
Proof. Proof.
iIntros "H H'". iMod (own_update_2 with "H H'") as "[$ $]"; last done. iIntros "H H'". iMod (own_update_2 with "H H'") as "[$ $]"; last done.
apply frac_auth_update, nat_local_update. lia. apply frac_auth_update, nat_local_update. lia.
Qed. Qed.
Lemma frac_auth_agree n n' γ : Lemma frac_auth_agree n n' γ :
own γ (! n) - own γ (!{1} n') - n = n'. own γ (F n) - own γ (F{1} n') - n = n'.
Proof. Proof.
iIntros "H H'". iIntros "H H'".
by iDestruct (own_valid_2 with "H H'") as %->%frac_auth_agreeL. by iDestruct (own_valid_2 with "H H'") as %->%frac_auth_agreeL.
...@@ -78,13 +78,13 @@ Section proof2. ...@@ -78,13 +78,13 @@ Section proof2.
(* The invariant that we use *) (* The invariant that we use *)
Definition proof2_inv (γ : gname) (l : loc) : iProp Σ := Definition proof2_inv (γ : gname) (l : loc) : iProp Σ :=
( n : nat, own γ (! n) l #n)%I. ( n : nat, own γ (F n) l #n)%I.
(* Proof of the threads *) (* Proof of the threads *)
Lemma par_inc_FAA_spec n n' γ l q : Lemma par_inc_FAA_spec n n' γ l q :
{{{ inv N (proof2_inv γ l) own γ (!{q} n) }}} {{{ inv N (proof2_inv γ l) own γ (F{q} n) }}}
FAA #l #n' FAA #l #n'
{{{ m, RET #m; own γ (!{q} (n + n'))%nat }}}. {{{ m, RET #m; own γ (F{q} (n + n'))%nat }}}.
Proof. Proof.
iIntros (Φ) "[#Hinv Hγ] Post". iInv N as (m) ">[Hauth Hl]" "Hclose". iIntros (Φ) "[#Hinv Hγ] Post". iInv N as (m) ">[Hauth Hl]" "Hclose".
wp_faa. wp_faa.
...@@ -103,8 +103,8 @@ Section proof2. ...@@ -103,8 +103,8 @@ Section proof2.
iDestruct "Hγ" as "[Hγ1 Hγ2]". iDestruct "Hγ" as "[Hγ1 Hγ2]".
iMod (inv_alloc _ _ (proof2_inv γ l) with "[Hl Hauth]") as "#Hinv". iMod (inv_alloc _ _ (proof2_inv γ l) with "[Hl Hauth]") as "#Hinv".
{ iNext. iExists 0%nat. iFrame. } { iNext. iExists 0%nat. iFrame. }
wp_apply (wp_par (λ _, own γ (!{1/2} 2%nat)) wp_apply (wp_par (λ _, own γ (F{1/2} 2%nat))
(λ _, own γ (!{1/2} 2%nat)) with "[Hγ1] [Hγ2]"). (λ _, own γ (F{1/2} 2%nat)) with "[Hγ1] [Hγ2]").
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto. - iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto. - iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- iIntros (v1 v2) "[Hγ1 Hγ2] !>". iCombine "Hγ1 Hγ2" as "Hγ". simpl. - iIntros (v1 v2) "[Hγ1 Hγ2] !>". iCombine "Hγ1 Hγ2" as "Hγ". simpl.
...@@ -117,9 +117,9 @@ Section proof2. ...@@ -117,9 +117,9 @@ Section proof2.
Qed. Qed.
Lemma par_incN_helper_spec n γ l q : Lemma par_incN_helper_spec n γ l q :
{{{ inv N (proof2_inv γ l) own γ (!{q} 0%nat) }}} {{{ inv N (proof2_inv γ l) own γ (F{q} 0%nat) }}}
par_incN_helper #n #l par_incN_helper #n #l
{{{ v, RET v; own γ (!{q} (n * 2))%nat }}}. {{{ v, RET v; own γ (F{q} (n * 2))%nat }}}.
Proof. Proof.
iIntros (Φ) "[#? Hγ] Post /=". iIntros (Φ) "[#? Hγ] Post /=".
iInduction n as [|n] "IH" forall (q Φ). iInduction n as [|n] "IH" forall (q Φ).
...@@ -127,8 +127,8 @@ Section proof2. ...@@ -127,8 +127,8 @@ Section proof2.
rewrite Nat2Z.inj_succ. do 2 wp_let. rewrite Nat2Z.inj_succ. do 2 wp_let.
wp_op. case_bool_decide; first lia. wp_if. wp_op. case_bool_decide; first lia. wp_if.
iDestruct "Hγ" as "[Hγ1 Hγ2]". iDestruct "Hγ" as "[Hγ1 Hγ2]".
wp_apply (wp_par (λ _, own γ (!{q/2} 2%nat)) wp_apply (wp_par (λ _, own γ (F{q/2} 2%nat))
(λ _, own γ (!{q/2} (n * 2)%nat)) with "[Hγ1] [Hγ2]"). (λ _, own γ (F{q/2} (n * 2)%nat)) with "[Hγ1] [Hγ2]").
- iApply (par_inc_FAA_spec 0 2 with "[$]"); auto. - iApply (par_inc_FAA_spec 0 2 with "[$]"); auto.
- wp_op. rewrite (_ : Z.succ n - 1 = n); last lia. - wp_op. rewrite (_ : Z.succ n - 1 = n); last lia.
iApply ("IH" with "Hγ2"); auto. iApply ("IH" with "Hγ2"); auto.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment