Commit 37784f60 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent ef59f1b0
......@@ -13,7 +13,7 @@ Definition start_chan : val := λ: "f",
(** Camera setup *)
Class proto_chanG Σ := {
proto_chanG_chanG :> chanG Σ;
proto_chanG_authG :> auth_exclG (laterO (proto val (iPreProp Σ) (iPreProp Σ))) Σ;
proto_chanG_authG :> auth_exclG (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))) Σ;
}.
Definition proto_chanΣ := #[
......@@ -24,7 +24,7 @@ Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ → proto_chanG Σ.
Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
(** Types *)
Definition iProto Σ := proto val (iProp Σ) (iProp Σ).
Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
Delimit Scope proto_scope with proto.
Bind Scope proto_scope with iProto.
......@@ -160,7 +160,7 @@ Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : i
| [] => p1 iProto_dual p2
| v :: vs => pc p2',
p2 (proto_message Receive pc)%proto
( f : laterO (iProto Σ) -n> iProp Σ, f (Next p2') - pc v f)
( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2') - pc v f)
proto_interp vs p1 p2'
end%I.
Arguments proto_interp {_ _} _ _%proto _%proto : simpl nomatch.
......@@ -378,7 +378,7 @@ Section proto.
Lemma proto_interp_send v vs pc p1 p2 :
proto_interp vs (proto_message Send pc) p2 -
( f : laterO (iProto Σ) -n> iProp Σ, f (Next p1) - pc v f) -
( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p1) - pc v f) -
proto_interp (vs ++ [v]) p1 p2.
Proof.
iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
......@@ -395,7 +395,7 @@ Section proto.
Lemma proto_interp_recv v vs p1 pc :
proto_interp (v :: vs) p1 (proto_message Receive pc) - p2,
( f : laterO (iProto Σ) -n> iProp Σ, f (Next p2) - pc v f)
( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2) - pc v f)
proto_interp vs p1 p2.
Proof.
simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2".
......
......@@ -168,20 +168,20 @@ Section mapper.
let acc := from_option (λ '(i,y,w), [(i,y)]) [] in
let accv := from_option (λ '(i,y,w), SOMEV (#(i:Z),w)) NONEV in
ys []
Sorted RZB (iys_sorted ++ ((i,) <$> ys))
Sorted RZB (iys_sorted ++ ((i,.) <$> ys))
i iys_sorted.*1
{{{
llist (IB i) l (reverse ys)
csort sort_fg_tail_protocol IZB RZB iys (iys_sorted ++ ((i,) <$> ys))
csort sort_fg_tail_protocol IZB RZB iys (iys_sorted ++ ((i,.) <$> ys))
}}}
par_map_reduce_collect csort #i #l
{{{ ys' miy, RET accv miy;
Sorted RZB ((iys_sorted ++ ((i,) <$> ys ++ ys')) ++ acc miy)
Sorted RZB ((iys_sorted ++ ((i,.) <$> ys ++ ys')) ++ acc miy)
from_option (λ '(j,_,_), i j j iys_sorted.*1)
(iys_sorted ++ ((i,) <$> ys ++ ys') ≡ₚ iys) miy
(iys_sorted ++ ((i,.) <$> ys ++ ys') ≡ₚ iys) miy
llist (IB i) l (reverse (ys ++ ys'))
csort from_option (λ _, sort_fg_tail_protocol IZB RZB iys
((iys_sorted ++ ((i,) <$> ys ++ ys')) ++ acc miy)) END%proto miy
((iys_sorted ++ ((i,.) <$> ys ++ ys')) ++ acc miy)) END%proto miy
from_option (λ '(i,y,w), IB i y w) True miy
}}}.
Proof.
......@@ -258,7 +258,7 @@ Section mapper.
rewrite gmultiset_elements_disj_union gmultiset_elements_singleton.
rewrite group_snoc // reverse_Permutation.
rewrite !bind_app /= right_id_L -!assoc_L -(comm _ zs') !assoc_L.
apply (inj (++ _)).
apply (inj (.++ _)).
- wp_recv ([i ys] k) as (Hy) "Hk".
wp_apply (lprep_spec with "[$Hl $Hk]"); iIntros "[Hl _]".
wp_apply ("IH" with "[ ] [//] [//] Hl Hcsort Hcred HImiy"); first done.
......
......@@ -11,7 +11,7 @@ Definition auth_exclΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
#[GFunctor (authRF (optionURF (exclRF F)))].
Instance subG_auth_exclG (F : oFunctor) `{!oFunctorContractive F} {Σ} :
subG (auth_exclΣ F) Σ auth_exclG (F (iPreProp Σ) _) Σ.
subG (auth_exclΣ F) Σ auth_exclG (F (iPrePropO Σ) _) Σ.
Proof. solve_inG. Qed.
Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
......
......@@ -90,7 +90,7 @@ Section group.
first [by etrans|auto using group_insert_perm, group_nodup, group_insert_commute].
Qed.
Lemma group_fmap (i : K) xs : xs [] group ((i,) <$> xs) ≡ₚₚ [(i, xs)].
Lemma group_fmap (i : K) xs : xs [] group ((i,.) <$> xs) ≡ₚₚ [(i, xs)].
Proof.
induction xs as [|x1 [|x2 xs] IH]; intros; simplify_eq/=; try done.
etrans.
......@@ -105,7 +105,7 @@ Section group.
repeat (simplify_eq/= || case_decide); repeat constructor; by auto.
Qed.
Lemma group_snoc ixs j ys :
j ixs.*1 ys [] group (ixs ++ ((j,) <$> ys)) ≡ₚₚ group ixs ++ [(j,ys)].
j ixs.*1 ys [] group (ixs ++ ((j,.) <$> ys)) ≡ₚₚ group ixs ++ [(j,ys)].
Proof.
induction ixs as [|[i x] ixs IH]; csimpl; [by auto using group_fmap|].
rewrite ?not_elem_of_cons; intros [??]. etrans; [|by apply group_insert_snoc].
......
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