Commit c6235271 authored by Ralf Jung's avatar Ralf Jung

update dependencies

parent b4038b7b
Pipeline #42839 passed with stage
in 21 minutes and 7 seconds
......@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
"coq-iris" { (= "dev.2021-02-14.0.842fb394") | (= "dev") }
"coq-iris" { (= "dev.2021-02-16.0.8ee71fff") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -178,7 +178,7 @@ Lemma wp_read_na E l q v :
Proof.
iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ) as "Hclose"; first set_solver.
iMod (fupd_mask_subseteq ) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
......@@ -211,7 +211,7 @@ Proof.
iIntros (<- Φ) ">Hv HΦ".
iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
iMod (fupd_intro_mask' _ ) as "Hclose"; first set_solver.
iMod (fupd_mask_subseteq ) as "Hclose"; first set_solver.
iModIntro; iSplit; first by eauto.
iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
iModIntro. iFrame "Hσ". iSplit; last done.
......
......@@ -64,7 +64,7 @@ Section frac_bor.
- iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
- iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
iApply fupd_intro_mask. set_solver. done.
iApply fupd_mask_intro_subseteq. set_solver. done.
Qed.
Local Lemma frac_bor_trade1 γ κ' q :
......
......@@ -128,7 +128,7 @@ Proof.
iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]".
solve_ndisj. by rewrite lookup_fmap EQB.
iDestruct ("HPP'" with "HP'") as "$".
iMod fupd_intro_mask' as "Hclose"; last iIntros "!>HP'". solve_ndisj.
iMod fupd_mask_subseteq as "Hclose"; last iIntros "!>HP'". solve_ndisj.
iDestruct ("HPP'" with "HP'") as "HP".
iMod "Hclose" as "_". iMod (slice_fill _ _ true with "Hs HP Hbox") as "Hbox".
solve_ndisj. by rewrite lookup_insert. iFrame.
......@@ -140,7 +140,7 @@ Proof.
iMod ("Hclose'" with "[-Hbor]") as "_".
+ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+ iMod (lft_incl_dead with "Hle H†"). done. iFrame.
iApply fupd_intro_mask'. solve_ndisj.
iApply fupd_mask_subseteq. solve_ndisj.
Qed.
(** Basic borrows *)
......@@ -234,7 +234,7 @@ Proof.
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
iMod fupd_intro_mask' as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
iMod fupd_mask_subseteq as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
......@@ -259,6 +259,6 @@ Proof.
iMod ("Hclose'" with "[-Hbor]") as "_".
+ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+ iMod (lft_incl_dead with "Hle H†") as "$". done.
iApply fupd_intro_mask'. solve_ndisj.
iApply fupd_mask_subseteq. solve_ndisj.
Qed.
End accessors.
......@@ -91,7 +91,7 @@ Section arc.
{ apply disjoint_union_l. split; solve_ndisj. }
iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
iMod "H" as "#Hν".
iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
{ set_solver-. }
iIntros "{$Hν} !>".
iMod "Hclose2" as "_". iApply "Hclose". auto.
......@@ -486,7 +486,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
......@@ -529,7 +529,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
......@@ -574,7 +574,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros (q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
......@@ -618,7 +618,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
......@@ -662,7 +662,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
(* Finish up the proof. *)
......@@ -709,7 +709,7 @@ Section arc.
with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
{ iIntros "!# Hα".
iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
- (* Finish up the proof (sucess). *)
......
......@@ -151,7 +151,7 @@ Section code.
(* FIXME: This should work: iIntros (?? R). *) intros ?? R.
iIntros "#LFT #Hshr #Hlincl !# Htok".
iMod (at_bor_acc_tok with "LFT Hshr Htok") as "[Hproto Hclose1]"; [done..|].
iMod (fupd_intro_mask') as "Hclose2"; last iModIntro; first solve_ndisj.
iMod (fupd_mask_subseteq) as "Hclose2"; last iModIntro; first solve_ndisj.
iFrame. iIntros "Hproto". iMod "Hclose2" as "_".
iMod ("Hclose1" with "Hproto") as "$". done.
Qed.
......
......@@ -298,7 +298,7 @@ Section code.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†".
iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
{ set_solver-. }
iMod "Hclose2" as "_". iModIntro.
iMod ("Hclose" with "[Hst $Hna]") as "$"; first by iExists _; iFrame.
......@@ -313,7 +313,7 @@ Section code.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†".
iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
{ set_solver-. }
iMod "Hclose2" as "_". iModIntro.
iMod (own_update_2 with "Hst Htok") as "Hst".
......@@ -334,7 +334,7 @@ Section code.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
iModIntro. iNext. iMod "H†".
iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
{ set_solver-. }
iMod "Hclose2" as "_". iModIntro.
iMod ("Hclose" with "[Hst $Hna Hl1 Hl2]") as "$";
......
......@@ -203,7 +203,7 @@ Section refcell_functions.
iSplitR "Htok2".
+ iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
iNext. iMod "Hν".
iMod fupd_intro_mask' as "Hclose"; last iMod ("Hh" with "[Hν]") as "$".
iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "[Hν]") as "$".
{ set_solver-. }
* rewrite -lft_dead_or. auto.
* done.
......@@ -283,7 +283,7 @@ Section refcell_functions.
iModIntro. iMod ("Hclose''" with "[Hlx Hownst Hbh Htok1] Hna") as "[Hβtok Hna]".
{ iExists _. iFrame. iNext. iSplitL "Hbh".
- iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
iMod fupd_intro_mask' as "Hclose"; last iMod ("Hbh" with "[Hν]") as "$".
iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hbh" with "[Hν]") as "$".
{ set_solver-. }
* rewrite -lft_dead_or. auto.
* done.
......
......@@ -101,7 +101,7 @@ Section rwlockreadguard_functions.
{ (* FIXME [solve_ndisj] fails. *)
apply: disjoint_difference_r1. done. }
iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
iMod fupd_intro_mask' as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
{ set_solver-. }
iMod "Hclose" as "_". iIntros "!> Hlx". iExists None. iFrame.
iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
......
......@@ -42,7 +42,7 @@ Section util.
iModIntro. iNext. iMod "Hdelay" as "[Hb Htok]".
iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
iApply "Hclose". auto.
- iMod fupd_intro_mask' as "Hclose'"; first solve_ndisj. iModIntro.
- iMod fupd_mask_subseteq as "Hclose'"; first solve_ndisj. iModIntro.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
Qed.
......@@ -65,7 +65,7 @@ Section util.
iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]"; first solve_ndisj.
{ iApply bor_shorten; done. }
iMod ("Hclose" with "[]") as "_"; auto.
- iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first solve_ndisj.
- iMod fupd_mask_subseteq as "Hclose'"; last iModIntro; first solve_ndisj.
iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
Qed.
End util.
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