Commit 3f3486af authored by Ralf Jung's avatar Ralf Jung

update dependencies; fix for std++ renames

parent 43b7c428
Pipeline #25337 passed with stage
in 28 minutes and 4 seconds
...@@ -10,8 +10,8 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/gpfsl.git" ...@@ -10,8 +10,8 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/gpfsl.git"
synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises" synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
depends: [ depends: [
"coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") } "coq-iris" { (= "dev.2020-03-18.0.b815eba9") | (= "dev") }
"coq-orc11" { (= "dev.2020-03-13.0.3a2bc1bd") | (= "dev") } "coq-orc11" { (= "dev.2020-03-18.0.9f7e8457") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
...@@ -170,12 +170,12 @@ Proof. ...@@ -170,12 +170,12 @@ Proof.
+ intros ? []. by rewrite (shift_nat_assoc _ 1). + intros ? []. by rewrite (shift_nat_assoc _ 1).
+ apply list_eq=>i. rewrite !list_lookup_fmap. + apply list_eq=>i. rewrite !list_lookup_fmap.
destruct (decide (i < n)%nat). destruct (decide (i < n)%nat).
rewrite !lookup_seq //. rewrite !lookup_seq_ge //; lia. } rewrite !lookup_seq_lt //. rewrite !lookup_seq_ge //; lia. }
rewrite monPred_at_big_sepL. rewrite monPred_at_big_sepL.
iCombine "Hists" "Hars" as "Hists". iCombine "Hists" "Haws" as "Hists". iCombine "Hists" "Hars" as "Hists". iCombine "Hists" "Haws" as "Hists".
iCombine "Hists" "Hnas" as "Hists". rewrite -3!big_sepL_sep. iCombine "Hists" "Hnas" as "Hists". rewrite -3!big_sepL_sep.
iApply (big_sepL_mono with "Hists"). iApply (big_sepL_mono with "Hists").
move => n1 n2 /lookup_seq_inv [/= -> Lt]. move => n1 n2 /lookup_seq [/= -> Lt].
destruct (lookup_lt_is_Some_2 𝑚s n1) as [𝑚 Eq𝑚]; destruct (lookup_lt_is_Some_2 𝑚s n1) as [𝑚 Eq𝑚];
first by rewrite (alloc_step_length _ _ _ _ _ _ _ ALLOC). first by rewrite (alloc_step_length _ _ _ _ _ _ _ ALLOC).
rewrite -(alloc_step_loc_eq _ _ _ _ _ _ _ ALLOC _ _ Eq𝑚) rewrite -(alloc_step_loc_eq _ _ _ _ _ _ _ ALLOC _ _ Eq𝑚)
......
...@@ -1165,7 +1165,7 @@ Section hist. ...@@ -1165,7 +1165,7 @@ Section hist.
apply auth_update_alloc, alloc_local_update; [|done]. apply auth_update_alloc, alloc_local_update; [|done].
apply to_atr_lookup_None, (closed_view_memory_None _ _ _ HN). apply to_atr_lookup_None, (closed_view_memory_None _ _ _ HN).
by apply (closed_na_view_list_addins _ _ _ _ INM NEXT). by apply (closed_na_view_list_addins _ _ _ _ INM NEXT).
* rewrite -(fmap_seq 0) big_sepL_fmap. * rewrite -(fmap_S_seq 0) big_sepL_fmap.
iApply (big_sepL_mono with "or'") => ? i ? /=. iApply (big_sepL_mono with "or'") => ? i ? /=.
rewrite (_: l >> 1 >> i = l >> Z.pos (Pos.of_succ_nat i)); [done|]. rewrite (_: l >> 1 >> i = l >> Z.pos (Pos.of_succ_nat i)); [done|].
rewrite shift_lblock_assoc. f_equal. lia. rewrite shift_lblock_assoc. f_equal. lia.
...@@ -1174,7 +1174,7 @@ Section hist. ...@@ -1174,7 +1174,7 @@ Section hist.
apply auth_update_alloc, (alloc_local_update (to_atw _)); [|done]. apply auth_update_alloc, (alloc_local_update (to_atw _)); [|done].
apply to_atw_lookup_None, (closed_view_memory_None _ _ _ HN). apply to_atw_lookup_None, (closed_view_memory_None _ _ _ HN).
by apply (closed_na_view_list_addins _ _ _ _ INM NEXT). by apply (closed_na_view_list_addins _ _ _ _ INM NEXT).
* rewrite -(fmap_seq 0) big_sepL_fmap. * rewrite -(fmap_S_seq 0) big_sepL_fmap.
iApply (big_sepL_mono with "owa'") => ? i ? /=. iApply (big_sepL_mono with "owa'") => ? i ? /=.
rewrite (_: l >> 1 >> i = l >> Z.pos (Pos.of_succ_nat i)); [done|]. rewrite (_: l >> 1 >> i = l >> Z.pos (Pos.of_succ_nat i)); [done|].
rewrite shift_lblock_assoc. f_equal. lia. rewrite shift_lblock_assoc. f_equal. lia.
...@@ -1183,7 +1183,7 @@ Section hist. ...@@ -1183,7 +1183,7 @@ Section hist.
apply auth_update_alloc, alloc_local_update; [|done]. apply auth_update_alloc, alloc_local_update; [|done].
apply to_nar_lookup_None, (closed_view_memory_None _ _ _ HN). apply to_nar_lookup_None, (closed_view_memory_None _ _ _ HN).
by apply (closed_na_view_list_addins _ _ _ _ INM NEXT). by apply (closed_na_view_list_addins _ _ _ _ INM NEXT).
* rewrite -(fmap_seq 0) big_sepL_fmap. * rewrite -(fmap_S_seq 0) big_sepL_fmap.
iApply (big_sepL_mono with "on'") => ? i ? /=. iApply (big_sepL_mono with "on'") => ? i ? /=.
rewrite (_: l >> 1 >> i = l >> Z.pos (Pos.of_succ_nat i)); [done|]. rewrite (_: l >> 1 >> i = l >> Z.pos (Pos.of_succ_nat i)); [done|].
rewrite shift_lblock_assoc. f_equal. lia. rewrite shift_lblock_assoc. f_equal. lia.
...@@ -1287,28 +1287,28 @@ Section hist. ...@@ -1287,28 +1287,28 @@ Section hist.
iAssert (( C, hist (l >> 0) 1 C) iAssert (( C, hist (l >> 0) 1 C)
[ list] i seq 0 (length 𝑚s), C, hist ((l >> 1) >> Z.of_nat i) 1 C)%I [ list] i seq 0 (length 𝑚s), C, hist ((l >> 1) >> Z.of_nat i) 1 C)%I
with "[ownl]" as "[hist ownl]". with "[ownl]" as "[hist ownl]".
{ rewrite Eqseq -fmap_seq big_sepL_cons. iDestruct "ownl" as "[$ ownl]". { rewrite Eqseq -fmap_S_seq big_sepL_cons. iDestruct "ownl" as "[$ ownl]".
rewrite big_sepL_fmap big_sepL_mono; [done|] => ? n ? /=. rewrite big_sepL_fmap big_sepL_mono; [done|] => ? n ? /=.
iDestruct 1 as (?) "?". iExists _. iDestruct 1 as (?) "?". iExists _.
rewrite shift_lblock_assoc -(Nat2Z.inj_add 1) //. } rewrite shift_lblock_assoc -(Nat2Z.inj_add 1) //. }
iAssert (( rs, atread (l >> 0) 1 rs) iAssert (( rs, atread (l >> 0) 1 rs)
[ list] i seq 0 (length 𝑚s), rs, atread ((l >> 1) >> Z.of_nat i) 1 rs)%I [ list] i seq 0 (length 𝑚s), rs, atread ((l >> 1) >> Z.of_nat i) 1 rs)%I
with "[oarl]" as "[atr oarl]". with "[oarl]" as "[atr oarl]".
{ rewrite Eqseq -fmap_seq big_sepL_cons. iDestruct "oarl" as "[$ oarl]". { rewrite Eqseq -fmap_S_seq big_sepL_cons. iDestruct "oarl" as "[$ oarl]".
rewrite big_sepL_fmap big_sepL_mono; [done|] => ? n ? /=. rewrite big_sepL_fmap big_sepL_mono; [done|] => ? n ? /=.
iDestruct 1 as (?) "?". iExists _. iDestruct 1 as (?) "?". iExists _.
rewrite shift_lblock_assoc -(Nat2Z.inj_add 1) //. } rewrite shift_lblock_assoc -(Nat2Z.inj_add 1) //. }
iAssert (( rs, atwrite (l >> 0) 1 rs) iAssert (( rs, atwrite (l >> 0) 1 rs)
[ list] i seq 0 (length 𝑚s), rs, atwrite ((l >> 1) >> Z.of_nat i) 1 rs)%I [ list] i seq 0 (length 𝑚s), rs, atwrite ((l >> 1) >> Z.of_nat i) 1 rs)%I
with "[oawl]" as "[atw oawl]". with "[oawl]" as "[atw oawl]".
{ rewrite Eqseq -fmap_seq big_sepL_cons. iDestruct "oawl" as "[$ oawl]". { rewrite Eqseq -fmap_S_seq big_sepL_cons. iDestruct "oawl" as "[$ oawl]".
rewrite big_sepL_fmap big_sepL_mono; [done|] => ? n ? /=. rewrite big_sepL_fmap big_sepL_mono; [done|] => ? n ? /=.
iDestruct 1 as (?) "?". iExists _. iDestruct 1 as (?) "?". iExists _.
rewrite shift_lblock_assoc -(Nat2Z.inj_add 1) //. } rewrite shift_lblock_assoc -(Nat2Z.inj_add 1) //. }
iAssert (( rs, naread (l >> 0) 1 rs) iAssert (( rs, naread (l >> 0) 1 rs)
[ list] i seq 0 (length 𝑚s), rs, naread ((l >> 1) >> Z.of_nat i) 1 rs)%I [ list] i seq 0 (length 𝑚s), rs, naread ((l >> 1) >> Z.of_nat i) 1 rs)%I
with "[onal]" as "[nar onal]". with "[onal]" as "[nar onal]".
{ rewrite Eqseq -fmap_seq big_sepL_cons. iDestruct "onal" as "[$ onal]". { rewrite Eqseq -fmap_S_seq big_sepL_cons. iDestruct "onal" as "[$ onal]".
rewrite big_sepL_fmap big_sepL_mono; [done|] => ? n ? /=. rewrite big_sepL_fmap big_sepL_mono; [done|] => ? n ? /=.
iDestruct 1 as (?) "?". iExists _. iDestruct 1 as (?) "?". iExists _.
rewrite shift_lblock_assoc -(Nat2Z.inj_add 1) //. } rewrite shift_lblock_assoc -(Nat2Z.inj_add 1) //. }
...@@ -1318,7 +1318,7 @@ Section hist. ...@@ -1318,7 +1318,7 @@ Section hist.
as (Vc' LE') "((own1&ownl) & (oar&oarl) & (oaw&oawl) & ona & onal)"; as (Vc' LE') "((own1&ownl) & (oar&oarl) & (oaw&oawl) & ona & onal)";
[|exact NEXT|done|]. [|exact NEXT|done|].
{ move => ???. rewrite shift_lblock_assoc -(Nat2Z.inj_add 1). by apply DMES. } { move => ???. rewrite shift_lblock_assoc -(Nat2Z.inj_add 1). by apply DMES. }
clear IH. rewrite Eqseq -fmap_seq. setoid_rewrite big_sepL_cons. clear IH. rewrite Eqseq -fmap_S_seq. setoid_rewrite big_sepL_cons.
iAssert ([ list] i (S <$> seq 0 (length 𝑚s)), iAssert ([ list] i (S <$> seq 0 (length 𝑚s)),
own hist_name ( {[l >> Z.of_nat i := (to_agree None, 1%Qp)]}))%I own hist_name ( {[l >> Z.of_nat i := (to_agree None, 1%Qp)]}))%I
with "[ownl]" as "$". with "[ownl]" as "$".
......
...@@ -381,10 +381,10 @@ Section na_props. ...@@ -381,10 +381,10 @@ Section na_props.
f_equiv. apply reflexive_eq, list_eq=>i. f_equiv. apply reflexive_eq, list_eq=>i.
destruct (decide (i < n1)%nat). destruct (decide (i < n1)%nat).
- rewrite lookup_app_l ?fmap_length ?seq_length // !list_lookup_fmap - rewrite lookup_app_l ?fmap_length ?seq_length // !list_lookup_fmap
!lookup_seq //. lia. !lookup_seq_lt //. lia.
- rewrite lookup_app_r ?fmap_length ?seq_length ?Nat.le_ngt // !list_lookup_fmap. - rewrite lookup_app_r ?fmap_length ?seq_length ?Nat.le_ngt // !list_lookup_fmap.
destruct (decide (i < n1 + n2)%nat). destruct (decide (i < n1 + n2)%nat).
+ rewrite !lookup_seq /= ?shift_nat_assoc; repeat f_equal; lia. + rewrite !lookup_seq_lt /= ?shift_nat_assoc; repeat f_equal; lia.
+ rewrite !lookup_seq_ge //; lia. + rewrite !lookup_seq_ge //; lia.
Qed. Qed.
......
...@@ -169,10 +169,10 @@ Lemma cb_escrows_list_alloc Ns γ q (ni: nat): ...@@ -169,10 +169,10 @@ Lemma cb_escrows_list_alloc Ns γ q (ni: nat):
Proof. Proof.
move => Le. iIntros "OL". move => Le. iIntros "OL".
iApply big_sepL_fupd. iApply big_sepL_fupd.
rewrite -2!fmap_seq -list_fmap_compose big_sepL_fmap. rewrite -2!fmap_S_seq -list_fmap_compose big_sepL_fmap.
iApply (big_sepL_mono with "OL"). iApply (big_sepL_mono with "OL").
iIntros (? i H) "ol". iIntros (? i H) "ol".
apply lookup_seq_inv in H as [H1 H2]. simpl in H1. subst k. apply lookup_seq in H as [H1 H2]. simpl in H1. subst k.
rewrite (_: Z.of_nat ((S S) i) = b + i `mod` Ns)%Z. rewrite (_: Z.of_nat ((S S) i) = b + i `mod` Ns)%Z.
- iApply (escrow_alloc with "[ol]"); [done|]. - iApply (escrow_alloc with "[ol]"); [done|].
iNext. by iExists _. iNext. by iExists _.
......
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