Commit 3f6aecf9 authored by Ralf Jung's avatar Ralf Jung
Browse files

update to latest Iris

parent 72528bbe
Pipeline #4356 passed with stage
in 14 minutes and 39 seconds
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq bfe7dd4c44d609088acadf40e1be500f76388a73
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea42f9947c8498292a0b02a3f901f0826b80ea63
......@@ -177,11 +177,11 @@ Section RCU.
:= λ t, match t with (l,h,w,r,t) => mkRCUGhost l h w r t end.
Global Instance RCUGhost_EqDec : EqDecision RCUGhost :=
injective_dec_eq RCUGhost_to_tuple (Some tuple_to_RCUGhost) _.
inj_dec_eq RCUGhost_to_tuple (Some tuple_to_RCUGhost) _.
Proof. by destruct 0. Qed.
Global Instance RCUGhost_Countable: Countable RCUGhost :=
injective_countable RCUGhost_to_tuple (Some tuple_to_RCUGhost) _.
inj_countable RCUGhost_to_tuple (Some tuple_to_RCUGhost) _.
Proof. by destruct 0. Qed.
(* There are n+1 pieces, n for readers, and 1 for writer *)
......@@ -242,9 +242,9 @@ Section RCU.
Qed.
Instance own_cmra_sep_homomorphism t:
WeakMonoidHomomorphism (op: Op coPset_disjC) (op: Op rcuTokR) (singletonM t).
WeakMonoidHomomorphism (op: Op coPset_disjC) (op: Op rcuTokR) () (singletonM t).
Proof.
split. apply _. move => ? ? i. rewrite lookup_op.
split; [apply _..|]. move => ? ? i. rewrite lookup_op.
case (decide (t = i)) => [->|NEq].
- by rewrite !lookup_singleton.
- by rewrite !lookup_singleton_ne.
......@@ -3495,4 +3495,4 @@ Section RCU.
End proof.
End RCU.
\ No newline at end of file
End RCU.
......@@ -28,11 +28,11 @@ Section RCUData.
end.
Global Instance AbsLoc_eqdec : EqDecision AbsLoc :=
injective_dec_eq AbsLoc_to_sum (Some sum_to_AbsLoc) _.
inj_dec_eq AbsLoc_to_sum (Some sum_to_AbsLoc) _.
Proof. by destruct 0. Qed.
Global Instance AbsLoc_countable: Countable AbsLoc
:= injective_countable AbsLoc_to_sum (Some sum_to_AbsLoc) _.
:= inj_countable AbsLoc_to_sum (Some sum_to_AbsLoc) _.
Proof. by destruct 0. Qed.
Definition RCUInfo : Type := list (aloc * loc * gname).
......
......@@ -43,7 +43,7 @@ Section Fractor.
Proof.
iIntros "[Info1 Info2]".
iCombine "Info1" "Info2" as "Info".
rewrite -auth_frag_op op_singleton pair_op.
rewrite op_singleton pair_op.
iDestruct (own_valid with "Info") as %Valid.
apply singleton_valid in Valid.
destruct Valid as [_ Valid2]. simpl in Valid2.
......@@ -193,4 +193,4 @@ Section Fractor.
iMod ("HClose" with "Inv"). by iApply "HT".
Qed.
End Fractor.
\ No newline at end of file
End Fractor.
......@@ -335,7 +335,7 @@ Section Fractional.
iDestruct (own_valid with "ex") as %Val%auth_valid_discrete.
move: Val => [_ /= /dec_agree_op_inv Eqe].
inversion Eqe. subst.
iDestruct "ex" as "[ex1 ex2]".
iDestruct "ex" as "[ex1 ex2]". rewrite dec_agree_idemp.
iSplitL "ex1"; iFrame.
Qed.
......@@ -376,4 +376,4 @@ Arguments GPS_FP_splitjoin [_ _ _ _ _ _ _ _ _ _ _ _].
Notation "'[FP' l 'in' s | p ]_ q" :=
(vGPS_FP p l s q)
(at level 0,
format "[FP l in s | p ]_ q").
\ No newline at end of file
format "[FP l in s | p ]_ q").
......@@ -146,13 +146,13 @@ Proof.
intros ? ? H1 ? ? H2 ? ? H3 ? ? H4.
unfold ProtoInv. subst. apply uPred.sep_proper.
- unfold BE_Inv, sEx, sBE.
rewrite big_opS_proper.
+ f_equiv; set_solver.
rewrite big_opS_proper; last first.
+ intros ??. apply H1.
- rewrite /All_Inv.
rewrite big_opS_proper.
+ f_equiv; set_solver.
- rewrite /All_Inv.
rewrite big_opS_proper; last first.
+ intros ??. apply H1.
+ f_equiv; set_solver.
Qed.
Global Instance gps_inv_proper {Σ fG Prtcl PF gpsG}:
......@@ -362,4 +362,4 @@ Section Example.
iIntros "?".
rewrite !(unf_int int).
Abort.
End Example.
\ No newline at end of file
End Example.
......@@ -45,13 +45,13 @@ Section STS.
Global Instance gsetR_singleton `{Countable T} : Singleton T (gsetR T).
Proof. unfold gsetR. intros x. unfold cmra_car. apply {[x]}. Defined.
Global Instance stateR_FromOp (S1 S2 : stR) :
@FromOp stateR ( ( S1 S2)) ( ( S1)) ( ( S2)) := _.
Global Instance stateR_IsOp (S1 S2 : stR) :
@IsOp stateR ( ( S1 S2)) ( ( S1)) ( ( S2)) := _.
Global Instance stateR_FromOp_ (S1 S2 : stR) :
@FromOp stateR ( (Auth (ExclBot') )) ( ( S1)) ( ( S2)).
Global Instance stateR_IsOp_ (S1 S2 : stR) :
@IsOp stateR ( (Auth (ExclBot') )) ( ( S1)) ( ( S2)).
Proof.
unfold FromOp. rewrite -auth_frag_op. done.
unfold IsOp. rewrite -auth_frag_op. done.
Qed.
Definition st_prst : pr_state Prtcl * (Z * View) -> _ := fst.
......@@ -386,4 +386,4 @@ Section Setup.
End Agreement.
End Assertions.
End Setup.
\ No newline at end of file
End Setup.
......@@ -32,7 +32,7 @@ Proof.
- right. rewrite Eq. left.
Qed.
Definition injective_dec_eq
Definition inj_dec_eq
`{H : x y : A, Decision (x = y)} {B : Type}
f (g : A -> option B) (Inj : x, g (f x) = Some x)
: x y : B, Decision (x = y).
......@@ -825,7 +825,7 @@ Qed.
(* gmap instances *)
Instance gmap_countable `{Countable K} `{Countable A} : Countable (gmap K A) :=
injective_countable (map_to_list : _ -> list (K * A))
inj_countable (map_to_list : _ -> list (K * A))
((λ l : list (_ * _), Some (map_of_list l)) : list _ -> option _) _.
Proof.
intros. f_equal. exact: map_of_to_list.
......
......@@ -86,7 +86,7 @@ Section Persistor.
iCombine "PerOwn1" "PerOwn2" as "PerOwn".
iDestruct (own_valid with "PerOwn") as %Valid.
move: Valid.
rewrite -auth_frag_op op_singleton
rewrite op_singleton
=> /singleton_valid /dec_agree_op_inv Valid.
inversion Valid. subst.
iExists X2. iFrame. iFrame "Inv2". by iSplit.
......@@ -106,7 +106,7 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & #oP2)".
iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid.
rewrite -auth_frag_op op_singleton in Valid.
rewrite op_singleton in Valid.
apply singleton_valid, dec_agree_op_inv in Valid.
inversion Valid. subst.
iExists X2. iFrame "P1 P2 Inv1 oP1 PC1".
......@@ -121,7 +121,7 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & #oP2)".
iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid.
rewrite -auth_frag_op op_singleton in Valid.
rewrite op_singleton in Valid.
apply singleton_valid, dec_agree_op_inv in Valid.
inversion Valid. subst.
iExists X2. iFrame "P1 P2 Inv2 oP1 PC1".
......@@ -136,7 +136,7 @@ Section Persistor.
iDestruct "P2" as (X2) "(P2 & #Inv2 & #PC2 & >#oP2)".
iCombine "oP1" "oP2" as "oP".
iDestruct (own_valid with "oP") as %Valid.
rewrite -auth_frag_op op_singleton in Valid.
rewrite op_singleton in Valid.
apply singleton_valid, dec_agree_op_inv in Valid.
inversion Valid. subst.
iExists X2. iModIntro. iFrame "P1 P2 Inv1 oP1 PC1".
......@@ -241,4 +241,3 @@ Proof.
iNext. rewrite /persistor_inv. iExists _. iFrame.
by rewrite big_sepM_empty.
Qed.
......@@ -142,8 +142,8 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
saved_prop_own i Ψ1 saved_prop_own i Ψ2 ( v V, Ψ1 v V Ψ2 v V).
Proof.
iIntros "(Saved1 & Saved2)".
iDestruct (saved_prop_agree i with "[$Saved1 $Saved2]") as "#Eq".
by do 2 setoid_rewrite cofe_funC_equivI.
iDestruct (saved_prop_agree i with "Saved1 Saved2") as "#Eq".
by do 2 setoid_rewrite ofe_funC_equivI.
Qed.
Lemma rsl_saved_pred_unfold_big_sepS
......@@ -1478,4 +1478,4 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
End RSL_SplitJoin.
Close Scope I.
End proof.
\ No newline at end of file
End proof.
......@@ -35,17 +35,17 @@ Section Definitions.
Definition val_to_sum : Val -> _ := λ v, match v with | A => inl () | D => inr (inl ()) | VInj v => inr (inr v) end.
Definition sum_to_val : _ -> Val := λ s, match s with | inl () => A | inr (inl ()) => D | inr (inr v) => VInj v end.
Global Instance Val_dec_eq : v1 v2 : Val, Decision (v1 = v2) :=
injective_dec_eq val_to_sum (Some sum_to_val) _.
inj_dec_eq val_to_sum (Some sum_to_val) _.
Proof. by destruct 0. Qed.
Global Instance Val_countable : Countable Val :=
injective_countable val_to_sum (Some sum_to_val) _.
inj_countable val_to_sum (Some sum_to_val) _.
Proof. by destruct 0. Qed.
Global Instance msg_dec_eq : x y : message, Decision (x = y) :=
injective_dec_eq msg_to_tuple (Some tuple_to_msg) _.
inj_dec_eq msg_to_tuple (Some tuple_to_msg) _.
Proof. by destruct 0. Qed.
Global Instance msg_countable : Countable message :=
injective_countable msg_to_tuple (Some tuple_to_msg) _.
inj_countable msg_to_tuple (Some tuple_to_msg) _.
Proof. by destruct 0. Qed.
Global Instance message_dec_eq : (m1 m2 : message), Decision (m1 = m2) := _.
......@@ -91,10 +91,10 @@ Section Definitions.
Definition sum_to_acc : _ -> access
:= λ s, match s with | inl () => na | inr () => at_hack end.
Global Instance access_dec_eq : EqDecision access | 20 :=
injective_dec_eq acc_to_sum (Some sum_to_acc) _.
inj_dec_eq acc_to_sum (Some sum_to_acc) _.
Proof. by destruct 0. Qed.
Global Instance access_countable : Countable access | 20 :=
injective_countable acc_to_sum (Some sum_to_acc) _.
inj_countable acc_to_sum (Some sum_to_acc) _.
Proof. by destruct 0. Qed.
End Glue.
......@@ -106,4 +106,4 @@ Global Instance View_Extension : Extension View | 0 := _.
Notation "'<' x → v @ t , R >" :=
(mkMessage x v t R)
(at level 20, format "< x → v @ t , R >",
x at level 21, v at level 21, t at level 21, R at level 21).
\ No newline at end of file
x at level 21, v at level 21, t at level 21, R at level 21).
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