Commit 977b763b authored by Joshua Yanovski's avatar Joshua Yanovski
Browse files

Bump Iris version to match LambdaRust-Coq.

parent d8a0d882
coq-iris 01d12014855abe6adaea20bbb35b1e9beadff14e
coq-iris 398bae9d092b6568cf8d504ca98d8810979eea33
......@@ -2,7 +2,6 @@
From iris.base_logic Require Export fancy_updates.
From iris.program_logic Require Export hoare weakestpre.
From iris.prelude Require Export coPset.
Import uPred.
Section atomic.
......@@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris_atomic Require Import atomic.
From iris.proofmode Require Import tactics.
From iris.prelude Require Import coPset.
From iris.heap_lang.lib Require Import par.
Section incr.
......@@ -166,7 +166,7 @@ Section proof.
subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
{ iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
iRight. iExists x5, v. iFrame. iExists Q. iFrame. }
iApply "HΦ". iFrame.
iApply "HΦ". iFrame. done.
* iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
- destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
......@@ -207,7 +207,7 @@ Section proof.
{ iFrame. iFrame "#". }
iNext. iIntros "HRf".
wp_seq. wp_proj. iApply (IHxs with "[-HΦ]")=>//.
iFrame "#"; first by iFrame. eauto.
iFrame "#"; first by iFrame.
Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
......@@ -282,7 +282,7 @@ Section proof.
iIntros (P Q x) "#Hf".
iIntros "!# Hp". wp_let. wp_bind (install _ _ _).
iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
{ iFrame. iFrame "#". eauto. }
{ iFrame. iFrame "#". }
iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
wp_let. wp_bind (loop _ _ _).
iApply (loop_spec with "[-Hx HoQ]")=>//.
......@@ -290,13 +290,13 @@ Section proof.
iNext. iIntros (? ?) "Hs".
iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
destruct (decide (x = a)) as [->|Hneq].
- iDestruct (saved_prop_agree with "[HoQ HoQ']") as "Heq"; first by iFrame.
- iDestruct (saved_prop_agree with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
- iExFalso. iCombine "Hx" "Hx'" as "Hx".
iDestruct (own_valid with "Hx") as %[_ H1].
rewrite pair_op //= in H1=>//. apply to_agree_comp_valid in H1.
fold_leibniz. done.
rewrite //= in H1.
by apply agree_op_inv' in H1.
End proof.
......@@ -3,7 +3,6 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap agree.
From iris.prelude Require Import countable.
From iris.base_logic Require Import big_op auth fractional.
Import uPred.
......@@ -36,8 +35,9 @@ Section heap_extra.
~((q1 + q2)%Qp 1%Qp)%Qc
p {q1} a p {q2} b False.
iIntros (?) "Hp".
iDestruct (@mapsto_valid_2 with "Hp") as %H'. done.
iIntros (?) "Hp".
iDestruct "Hp" as "[Hl Hr]".
iDestruct (@mapsto_valid_2 with "Hl Hr") as %H'. done.
End heap_extra.
......@@ -81,6 +81,6 @@ Section pair.
iIntros "[Ho Ho']".
iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
subst. iCombine "Ho" "Ho'" as "Ho".
rewrite pair_op frac_op' agree_idemp. by iFrame.
by iFrame.
End pair.
......@@ -54,7 +54,7 @@ Section proofs.
{ iFrame. iExists [], l.
iFrame. simpl. eauto. }
iMod (inv_alloc N _ ( xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
iApply "HΦ". iFrame "#".
iApply "HΦ". iFrame "#". done.
Lemma push_spec (s: loc) (x: val):
......@@ -33,7 +33,7 @@ Section syncer.
iSpecialize ("Hf" with "[R HP]"); first by iFrame.
iApply wp_wand_r. iSplitL "Hf"; first done.
iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
iApply (release_spec with "[$HR $Hl $Hlocked]").
iApply (release_spec with "[$Hl $HR $Hlocked]").
iNext. iIntros "_". by wp_seq.
End syncer.
......@@ -64,17 +64,17 @@ Section proof.
simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
iExFalso. iDestruct "Hxs" as (?) "Hhd'".
(* FIXME: If I dont use the @ here and below through this file, it loops. *)
by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
- induction ys as [|y ys' IHys'].
+ iIntros (hd) "(Hxs & Hys)".
iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
iDestruct "Hys" as (?) "Hhd'".
by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
+ iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %[= Heq].
iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
by subst.
......@@ -173,9 +173,9 @@ Section proof.
{ iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
destruct xs as [|x' xs''].
- simpl. iDestruct "Hhd''" as (?) "H".
iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1 $H]") as %?.
iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?.
- simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
iDestruct (@mapsto_agree with "[$Hhd1 $Hhd'']") as %[=].
iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=].
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done).
Supports Markdown
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