Commit 51cbbe95 authored by Hai Dang's avatar Hai Dang

bump iris (changes in auth)

parent 60b7e7b9
Pipeline #16976 passed with stage
in 15 minutes and 42 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-05-20.1.eb3117bd") | (= "dev") }
"coq-iris" { (= "dev.2019-05-24.5.cdb90fa2") | (= "dev") }
]
......@@ -341,13 +341,13 @@ Section flock.
- iDestruct "Hst" as ">[Hlocked Hactives]".
(* We can now show that the proposition `ρ` is *not* active *)
iDestruct (own_valid_2 with "Haprops Hρ")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
as %[Hfoo%to_props_map_singleton_included _]%auth_both_valid.
iAssert (fa !! ρ = None)%I with "[-]" as %Hbar.
{ remember (fa !! ρ) as faρ. destruct faρ as [π|]; last done.
symmetry in Heqfaρ.
iCombine "Hactives Hρ" as "H".
iDestruct (own_valid with "H") as %Hbaz.
exfalso. apply auth_own_valid in Hbaz. simpl in *.
exfalso. apply auth_frag_valid in Hbaz. simpl in *.
specialize (Hbaz ρ). revert Hbaz.
rewrite lookup_op Heqfaρ lookup_singleton.
rewrite -Some_op Some_valid.
......@@ -379,11 +379,11 @@ Section flock.
- iDestruct "Hst" as ">Hfactive".
iAssert (fa = ∅⌝)%I with "[-]" as %->.
{ iDestruct (own_valid_2 with "Haactive Hfactive")
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
as %[Hfoo%Excl_included _]%auth_both_valid.
iPureIntro. by unfold_leibniz. }
rewrite /from_active fmap_empty /= right_id.
iDestruct (own_valid_2 with "Haprops Hρ")
as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
as %[Hfoo%to_props_map_singleton_included _]%auth_both_valid.
iMod (own_update_2 with "Haprops Hρ") as "Haprops".
{ apply auth_update_dealloc, (delete_singleton_local_update _ ρ _). }
rewrite /all_tokens (big_sepM_delete _ fp ρ _) //.
......@@ -473,13 +473,11 @@ Section flock.
Proof.
iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
iMod (own_alloc ( (Excl' Unlocked) (Excl' Unlocked)))
as (γ_state) "[Hauth Hfrag]"; first done.
as (γ_state) "[Hauth Hfrag]"; first by apply auth_both_valid.
iMod (own_alloc ( to_props_map )) as (γ_props) "Hprops".
{ apply auth_valid_discrete. simpl.
split; last done. apply ucmra_unit_least. }
{ by apply auth_auth_valid. }
iMod (own_alloc (( Excl' ) ( Excl' ))) as (γ_ac_props) "[Hacprops1 Hacprops2]".
{ apply auth_valid_discrete. simpl.
split; last done. by rewrite left_id. }
{ by apply auth_both_valid. }
iApply (newlock_spec lockN (own γ_state ( (Excl' Unlocked))) with "Hfrag").
iNext. iIntros (lk γ_lock) "#Hlock".
pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
......@@ -549,11 +547,11 @@ Section flock.
"(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl";
last first.
- iDestruct (own_valid_2 with "Hstate Hflkd")
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
as %[Hfoo%Excl_included _]%auth_both_valid.
fold_leibniz. inversion Hfoo.
- iDestruct "Hst" as ">[Hlocked Hactives]".
iDestruct (own_valid_2 with "Haactive Hfactive")
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
as %[Hfoo%Excl_included _]%auth_both_valid.
fold_leibniz. simplify_eq/=.
(* Locked ~~> Unlocked *)
......@@ -609,7 +607,7 @@ Section flock.
- iDestruct "Hst" as ">Hfactive".
iAssert (fa = ∅⌝)%I with "[-]" as %->.
{ iDestruct (own_valid_2 with "Haactive Hfactive")
as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
as %[Hfoo%Excl_included _]%auth_both_valid.
iPureIntro. by unfold_leibniz. }
rewrite /from_active fmap_empty /= right_id.
......@@ -647,7 +645,7 @@ Section flock.
(* I' ≼ fp *)
iDestruct (own_valid_2 with "Haprops HI")
as %[Hfoo _]%auth_valid_discrete_2.
as %[Hfoo _]%auth_both_valid.
(* TODO: RK, can this proof script be simplified? The idea is not complicated. *)
(* We are going to separate the active resources I out of the fp map *)
......
......@@ -215,9 +215,9 @@ Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
(|==> _ : locking_heapG Σ, full_locking_heap )%I.
Proof.
iMod (own_alloc ( to_locking_heap )) as (γ1) "Hh1".
{ apply: auth_auth_valid. exact: to_locking_heap_valid. }
{ by apply auth_auth_valid. }
iMod (own_alloc ( to_heap_block_info )) as (γ2) "Hh2".
{ apply: auth_auth_valid. exact: to_heap_block_info_valid. }
{ by apply auth_auth_valid. }
iModIntro. iExists (LHeapG Σ _ _ γ1 γ2), . iFrame; auto 10.
Qed.
......@@ -237,8 +237,8 @@ Section properties.
Proof.
rewrite mapsto_eq /mapsto_def.
iDestruct 1 as (lv1 ??) "Hl1". iDestruct 1 as (lv2 ? _) "Hl2".
iDestruct (own_valid_2 with "Hl1 Hl2") as %Ho%auth_own_valid. iPureIntro.
revert Ho. rewrite /= op_singleton singleton_valid. by intros [_ ?%agree_op_invL'].
iDestruct (own_valid_2 with "Hl1 Hl2") as %Ho. iPureIntro.
revert Ho. rewrite auth_frag_valid op_singleton singleton_valid. by intros [_ ?%agree_op_invL'].
Qed.
Lemma mapsto_combine lv lv' cl q q' v :
......@@ -390,7 +390,7 @@ Section properties.
iDestruct 1 as ([] []%lvl_included _) "Hl".
iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
iDestruct (own_valid_2 with "Hfull Hl")
as %[[[] [[]%lvl_included Hl]]%heap_singleton_included _]%auth_valid_discrete_2; auto.
as %[[[] [[]%lvl_included Hl]]%heap_singleton_included _]%auth_both_valid; auto.
Qed.
Lemma full_locking_heap_unlocked σ cl v q :
......@@ -410,7 +410,7 @@ Section properties.
rewrite mapsto_eq /mapsto_def /full_locking_heap.
iDestruct 1 as (lv _ _) "Hl". iDestruct 1 as (τ Hτ) "[Hfull Hmap]".
iDestruct (own_valid_2 with "Hfull Hl")
as %[[y [? ?]]%heap_singleton_included _]%auth_valid_discrete_2; eauto.
as %[[y [? ?]]%heap_singleton_included _]%auth_both_valid; eauto.
Qed.
Lemma full_locking_heap_load_upd cl lv q v σ :
......@@ -423,7 +423,7 @@ Section properties.
iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ & H)".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ??) "Hl".
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_both_valid.
move: (Hσ). rewrite Hτ; last by eauto.
intros ([k lvvs|?]&?&Hi)%bind_Some; simplify_eq/=.
iDestruct (big_sepM_lookup_acc with "H") as "[H Hclose]"; first done.
......@@ -448,7 +448,7 @@ Section properties.
iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ & H)".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ??) "Hl".
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_both_valid.
move: (Hσ). rewrite Hτ; last by eauto.
intros ([k lvvs|?]&Hτl&Hi)%bind_Some; simplify_eq/=.
iDestruct (big_sepM_delete with "H") as "[Hcl H]"; first done.
......@@ -643,14 +643,14 @@ Section properties.
rewrite block_info_eq /block_info_def; iIntros "(Hoff & % & Hinfo) Hcl".
iDestruct "Hoff" as %Hoff.
iDestruct (own_valid_2 with "Hτ Hinfo")
as %[(b&Hb&?)%block_info_singleton_included _]%auth_valid_discrete_2.
as %[(b&Hb&?)%block_info_singleton_included _]%auth_both_valid.
iDestruct (big_sepM_delete with "H") as "[Hb H]"; first done.
destruct b as [k' lvvs|k' n]; simplify_eq/=; last first.
{ destruct vs as [|v vs]; simplify_eq/=.
rewrite /mapsto_list mapsto_eq /mapsto_def; iDestruct "Hcl" as "[Hcl _]".
iDestruct "Hcl" as (lv' _ _) "Hcl". rewrite cloc_plus_0.
iDestruct (own_valid_2 with "Hσ Hcl")
as %[(lv''&_&Hcl)%heap_singleton_included ?]%auth_valid_discrete_2.
as %[(lv''&_&Hcl)%heap_singleton_included ?]%auth_both_valid.
contradict Hcl. rewrite Hτ ?Hoff //. by rewrite /heap_blocks_lookup Hb. }
iDestruct "Hb" as (ll) "[Hll %]".
iAssert vs = lvvs.*2 %I as %->.
......@@ -659,7 +659,7 @@ Section properties.
iDestruct (big_sepL_lookup with "Hcl") as "Hcl"; first done.
iDestruct "Hcl" as (lv' _ _) "Hcl".
iDestruct (own_valid_2 with "Hσ Hcl")
as %[(lv''&_&Hcl)%heap_singleton_included ?]%auth_valid_discrete_2.
as %[(lv''&_&Hcl)%heap_singleton_included ?]%auth_both_valid.
iPureIntro; move: Hcl.
rewrite Hτ /heap_blocks_lookup /cloc_plus /= ?Hoff; last lia.
rewrite Hb /= Z.add_0_r Nat2Z.id.
......@@ -703,7 +703,7 @@ Section properties.
iDestruct 1 as (τ [Hnat Hτ]) "(Hσ & Hτ &H)".
rewrite mapsto_eq /mapsto_def; iDestruct 1 as (lv' ??) "Hl".
iDestruct (own_valid_2 with "Hσ Hl")
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_valid_discrete_2.
as %[(lv''&?&Hσ)%heap_singleton_included _]%auth_both_valid.
move: (Hσ); rewrite Hτ; last by eauto.
intros ([k lvvs|?]&Hτl&Hi)%bind_Some; simplify_eq/=.
iDestruct (big_sepM_delete with "H") as "[Hcl H]"; first done.
......
......@@ -22,7 +22,8 @@ Section par_inc.
CWP par_inc (cloc_to_val cl) @ R {{ v, v = #2 cl C #(2 + n) }}.
Proof.
iIntros "Hl". iApply cwp_fun; simpl.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [done|].
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]";
[by apply auth_both_valid|].
set (par_inc_inv := ( n' : nat, cl C #(n' + n) own γ (! n'))%I).
iApply (cwp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
{ iExists 0%nat. iFrame. }
......
......@@ -9,9 +9,9 @@ we verify the following program:
#include <stdlib.h>
#include <stdio.h>
int storeme(int * l) { *l = 10; return 10; }
int main() {
int * l = calloc(sizeof(int), 1);
int r = storeme(l) + ( *l = 11 );
......@@ -61,12 +61,12 @@ Section test.
Proof.
iIntros "H1 H2".
by iDestruct (own_valid_2 with "H2 H1")
as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma gnew : (|==> γ, gauth γ false γ false)%I.
Proof.
iMod (own_alloc ( (Excl' false) (Excl' false)))%I as (γ) "[H1 H2]";
first done;
first by apply auth_both_valid.
eauto with iFrame.
Qed.
Lemma gupdate b3 γ b1 b2 :
......
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