Commit 06edc222 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (C→O rename).

parent 43371d2a
Pipeline #17768 failed with stage
in 15 minutes and 45 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-06-13.0.860bd8e4") | (= "dev") }
"coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -6,16 +6,16 @@ From iris.proofmode Require Import tactics.
From iris_examples.barrier Require Import proof specification.
Set Default Proof Using "Type".
Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ) _).
Definition one_shotR (Σ : gFunctors) (F : oFunctor) :=
csumR (exclR unitO) (agreeR $ laterO $ F (iPreProp Σ) _).
Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.
Definition Shot {Σ} {F : oFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
Cinr $ to_agree $ Next $ oFunctor_map F (iProp_fold, iProp_unfold) x.
Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
Class oneShotG (Σ : gFunctors) (F : oFunctor) :=
one_shot_inG :> inG Σ (one_shotR Σ F).
Definition oneShotΣ (F : cFunctor) : gFunctors :=
#[ GFunctor (csumRF (exclRF unitC) (agreeRF ( F))) ].
Definition oneShotΣ (F : oFunctor) : gFunctors :=
#[ GFunctor (csumRF (exclRF unitO) (agreeRF ( F))) ].
Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ oneShotG Σ F.
Proof. solve_inG. Qed.
......@@ -59,12 +59,12 @@ Proof.
iAssert ( (x x'))%I as "Hxx".
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI bi.later_equivI /=.
rewrite -{2}[x]cFunctor_id -{2}[x']cFunctor_id.
assert (HF : cFunctor_map F (cid, cid) cFunctor_map F (iProp_fold (Σ:=Σ) iProp_unfold, iProp_fold (Σ:=Σ) iProp_unfold)).
rewrite -{2}[x]oFunctor_id -{2}[x']oFunctor_id.
assert (HF : oFunctor_map F (cid, cid) oFunctor_map F (iProp_fold (Σ:=Σ) iProp_unfold, iProp_fold (Σ:=Σ) iProp_unfold)).
{ apply ne_proper; first by apply _.
by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
rewrite (HF x). rewrite (HF x').
rewrite !cFunctor_compose. iNext. by iRewrite "Hγ2". }
rewrite !oFunctor_compose. iNext. by iRewrite "Hγ2". }
iNext. iRewrite -"Hxx" in "Hx'".
iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
Qed.
......
......@@ -18,7 +18,7 @@ Lemma barrier_spec (N : namespace) :
( l P Q, recv l (P Q) ={N}=> recv l P recv l Q)
( l P Q, (P - Q) - recv l P - recv l Q).
Proof.
exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
exists (λ l, OfeMor (recv N l)), (λ l, OfeMor (send N l)).
split_and?; simpl.
- iIntros (P) "!# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
iNext. eauto.
......
......@@ -36,8 +36,8 @@ Section stacks.
iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
Qed.
Definition is_list_pre (P : val iProp Σ) (F : val -c> iProp Σ) :
val -c> iProp Σ := λ v,
Definition is_list_pre (P : val iProp Σ) (F : val -d> iProp Σ) :
val -d> iProp Σ := λ v,
(v NONEV (l : loc) (h t : val), v SOMEV #l l {-} (h, t)%V P h F t)%I.
Local Instance is_list_contr (P : val iProp Σ) : Contractive (is_list_pre P).
......
......@@ -246,8 +246,8 @@ Section stack_works.
iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
Qed.
Definition is_list_pre (P : val iProp Σ) (F : val -c> iProp Σ) :
val -c> iProp Σ := λ v,
Definition is_list_pre (P : val iProp Σ) (F : val -d> iProp Σ) :
val -d> iProp Σ := λ v,
(v NONEV (l : loc) (h t : val), v SOMEV #l l {-} (h, t)%V P h F t)%I.
Local Instance is_list_contr (P : val iProp Σ) : Contractive (is_list_pre P).
......
......@@ -38,9 +38,9 @@ Definition popBag : val := λ: "b",
release "l";;
"v".
Canonical Structure valmultisetC := leibnizC (gmultiset valC).
Canonical Structure valmultisetO := leibnizO (gmultiset valO).
Class bagG Σ := BagG
{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetC));
{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetO));
lock_bagG :> lockG Σ
}.
......
......@@ -14,7 +14,7 @@ Set Default Proof Using "Type".
SET_RES v = the result of the task has been computed and it is v
FIN v = the task has been completed with the result v *)
(* We use this RA to verify the Task.run() method *)
Definition saR := csumR fracR (csumR (prodR fracR (agreeR valC)) (agreeR valC)).
Definition saR := csumR fracR (csumR (prodR fracR (agreeR valO)) (agreeR valO)).
Class saG Σ := { sa_inG :> inG Σ saR }.
Definition INIT `{saG Σ} γ (q: Qp) := own γ (Cinl q%Qp).
Definition SET_RES `{saG Σ} γ (q: Qp) (v: val) := own γ (Cinr (Cinl (q%Qp, to_agree v))).
......@@ -189,7 +189,7 @@ Section contents.
Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv).
Program Definition pre_runner (γ : name Σ b) (P: val iProp Σ) (Q: val val iProp Σ) :
(valC -n> iProp Σ) -n> (valC -n> iProp Σ) := λne R r,
(valO -n> iProp Σ) -n> (valO -n> iProp Σ) := λne R r,
( (body bag : val), r = (body, bag)%V
bagS b (N.@"bag") (λ x y, γ γ', isTask (body,x) γ γ' y P Q) γ bag
r a: val, (R r P a - WP body r a {{ v, Q a v }}))%I.
......@@ -200,7 +200,7 @@ Section contents.
Proof. unfold pre_runner. solve_contractive. Qed.
Definition runner (γ: name Σ b) (P: val iProp Σ) (Q: val val iProp Σ) :
valC -n> iProp Σ :=
valO -n> iProp Σ :=
(fixpoint (pre_runner γ P Q))%I.
Lemma runner_unfold γ r P Q :
......
......@@ -34,9 +34,9 @@ Definition popBag : val := rec: "pop" "b" :=
else "pop" "b"
end.
Canonical Structure valmultisetC := leibnizC (gmultiset valC).
Canonical Structure valmultisetO := leibnizO (gmultiset valO).
Class bagG Σ := BagG
{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetC));
{ bag_bagG :> inG Σ (prodR fracR (agreeR valmultisetO));
}.
(** Generic specification for the bag, using view shifts. *)
......
......@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
(** We are going to need the oneshot RA to verify the
Task.Join() method *)
Definition oneshotR := csumR fracR (agreeR valC).
Definition oneshotR := csumR fracR (agreeR valO).
Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ oneshotG Σ.
......
......@@ -59,12 +59,12 @@ Section monotone_counter.
*)
(*
To tell Coq we wish to use such a discrete CMRA we use the constructor leibnizC.
To tell Coq we wish to use such a discrete CMRA we use the constructor leibnizO.
This takes a Coq type and makes it an instance of an OFE (a step-indexed generalization of sets).
This is not the place do describe Canonical Structures.
A very good introduction is available at https://hal.inria.fr/hal-00816703v1/document
*)
Canonical Structure mcounterRAC := leibnizC mcounterRAT.
Canonical Structure mcounterRAC := leibnizO mcounterRAT.
(* To make the type mcounterRAT into an RA we need an operation. This is
defined in the standard way, except we use the typeclass Op so we can reuse
......
......@@ -46,7 +46,7 @@ Notation iProp := (iProp Σ).
(* First we define the is_list representation predicate via a guarded fixed
point of the functional is_list_pre. Note the use of the later modality. The
arrows -c> express that the arrow is an arrow in the category of COFE's,
arrows -d> express that the arrow is an arrow in the category of COFE's,
i.e., it is a non-expansive function. To fully understand the meaning of this
it is necessary to understand the model of Iris.
......@@ -55,7 +55,7 @@ Notation iProp := (iProp Σ).
but in more complex examples the domain of the predicate we are defining will
not be a discrete type, and the condition will be meaningful and necessary.
*)
Definition is_list_pre (Φ : val -c> list val -c> iProp): val -c> list val -c> iProp := λ hd xs,
Definition is_list_pre (Φ : val -d> list val -d> iProp): val -d> list val -d> iProp := λ hd xs,
match xs with
[] => hd = NONEV
| (x::xs) => ( ( : loc) (hd' : val), hd = SOMEV #ℓ⌝ (x,hd') Φ hd' xs)
......
......@@ -9,7 +9,7 @@ From iris.bi.lib Require Import fractional.
From iris.heap_lang.lib Require Import par.
Definition cntCmra : cmraT := (prodR fracR (agreeR (leibnizC Z))).
Definition cntCmra : cmraT := (prodR fracR (agreeR (leibnizO Z))).
Class cntG Σ := CntG { CntG_inG :> inG Σ cntCmra }.
Definition cntΣ : gFunctors := #[GFunctor cntCmra ].
......
......@@ -90,10 +90,10 @@ Definition cinc : val :=
(** ** Proof setup *)
Definition flagUR := authR $ optionUR $ exclR boolC.
Definition numUR := authR $ optionUR $ exclR ZC.
Definition tokenUR := exclR unitC.
Definition one_shotUR := csumR (exclR unitC) (agreeR unitC).
Definition flagUR := authR $ optionUR $ exclR boolO.
Definition numUR := authR $ optionUR $ exclR ZO.
Definition tokenUR := exclR unitO.
Definition one_shotUR := csumR (exclR unitO) (agreeR unitO).
Class cincG Σ := ConditionalIncrementG {
cinc_flagG :> inG Σ flagUR;
......
......@@ -138,10 +138,10 @@ auth invariant. *)
(** The CMRA & functor we need. *)
Class hocapG Σ := HocapG {
hocap_stateG :> inG Σ (authR (optionUR $ exclR (listC valC)));
hocap_stateG :> inG Σ (authR (optionUR $ exclR (listO valO)));
}.
Definition hocapΣ : gFunctors :=
#[GFunctor (exclR unitC); GFunctor (authR (optionUR $ exclR (listC valC)))].
#[GFunctor (exclR unitO); GFunctor (authR (optionUR $ exclR (listO valO)))].
Instance subG_hocapΣ {Σ} : subG hocapΣ Σ hocapG Σ.
Proof. solve_inG. Qed.
......
......@@ -13,11 +13,11 @@ heap. *)
(** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class stackG Σ := StackG {
stack_tokG :> inG Σ (exclR unitC);
stack_stateG :> inG Σ (authR (optionUR $ exclR (listC valC)));
stack_tokG :> inG Σ (exclR unitO);
stack_stateG :> inG Σ (authR (optionUR $ exclR (listO valO)));
}.
Definition stackΣ : gFunctors :=
#[GFunctor (exclR unitC); GFunctor (authR (optionUR $ exclR (listC valC)))].
#[GFunctor (exclR unitO); GFunctor (authR (optionUR $ exclR (listO valO)))].
Instance subG_stackΣ {Σ} : subG stackΣ Σ stackG Σ.
Proof. solve_inG. Qed.
......
......@@ -6,7 +6,7 @@ From iris_examples.logatom.flat_combiner Require Import sync misc.
(** The simple syncer spec in [sync.v] implies a logically atomic spec. *)
Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
Definition syncR := prodR fracR (agreeR valO). (* track the local knowledge of ghost state *)
Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
......@@ -15,8 +15,8 @@ Proof. solve_inG. Qed.
Section atomic_sync.
Context `{EqDecision A, !heapG Σ, !lockG Σ}.
Canonical AC := leibnizC A.
Context `{!inG Σ (prodR fracR (agreeR AC))}.
Canonical AO := leibnizO A.
Context `{!inG Σ (prodR fracR (agreeR AO))}.
(* TODO: Rename and make opaque; the fact that this is a half should not be visible
to the user. *)
......@@ -56,7 +56,7 @@ Section atomic_sync.
iSplitL "Hg2"; first done. iIntros "!#".
iIntros (f). iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
iIntros (f') "#Hsynced {Hsyncer}".
iAlways. iIntros (α β x) "#Hseq". change (ofe_car AC) with A.
iAlways. iIntros (α β x) "#Hseq". change (ofe_car AO) with A.
iIntros (Φ') "?".
(* TODO: Why can't I iApply "Hsynced"? *)
iSpecialize ("Hsynced" $! _ Φ' x).
......
......@@ -46,7 +46,7 @@ Definition mk_flat : val :=
let: "r" := loop "p" "s" "lk" in
"r".
Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *)
Definition reqR := prodR fracR (agreeR valO). (* request x should be kept same *)
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Class flatG Σ := FlatG {
req_G :> inG Σ reqR;
......
......@@ -20,7 +20,7 @@ Section lemmas.
End lemmas.
Section excl.
Context `{!inG Σ (exclR unitC)}.
Context `{!inG Σ (exclR unitO)}.
Lemma excl_falso γ Q':
own γ (Excl ()) own γ (Excl ()) Q'.
Proof.
......
......@@ -70,14 +70,14 @@ Definition read_with_proph : val :=
(** The CMRA & functor we need. *)
Definition timestampUR := gmapUR Z $ agreeR valC.
Definition timestampUR := gmapUR Z $ agreeR valO.
Class atomic_snapshotG Σ := AtomicSnapshotG {
atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valC;
atomic_snapshot_stateG :> inG Σ $ authR $ optionUR $ exclR $ valO;
atomic_snapshot_timestampG :> inG Σ $ authR $ timestampUR
}.
Definition atomic_snapshotΣ : gFunctors :=
#[GFunctor (authR $ optionUR $ exclR $ valC); GFunctor (authR timestampUR)].
#[GFunctor (authR $ optionUR $ exclR $ valO); GFunctor (authR timestampUR)].
Instance subG_atomic_snapshotΣ {Σ} : subG atomic_snapshotΣ Σ atomic_snapshotG Σ.
Proof. solve_inG. Qed.
......
......@@ -58,10 +58,10 @@ Definition pop_stack : val :=
(** * Definition of the required camera *************************************)
Class stackG Σ := StackG {
stack_tokG :> inG Σ (authR (optionUR (exclR (listC valC)))) }.
stack_tokG :> inG Σ (authR (optionUR (exclR (listO valO)))) }.
Definition stackΣ : gFunctors :=
#[GFunctor (authR (optionUR (exclR (listC valC))))].
#[GFunctor (authR (optionUR (exclR (listO valO))))].
Instance subG_stackΣ {Σ} : subG stackΣ Σ stackG Σ.
Proof. solve_inG. Qed.
......
......@@ -11,7 +11,7 @@ Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next leve
Section fundamental.
Context `{irisG F_mu_lang Σ}.
Notation D := (valC -n> iProp Σ).
Notation D := (valO -n> iProp Σ).
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (wp_bind (fill[ctx]));
......
......@@ -167,9 +167,9 @@ Module F_mu.
fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
Canonical Structure stateO := leibnizO state.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
End F_mu.
(** Language *)
......
......@@ -7,57 +7,57 @@ Import uPred.
(** interp : is a unary logical relation. *)
Section logrel.
Context `{irisG F_mu_lang Σ}.
Notation D := (valC -n> iProp Σ).
Notation D := (valO -n> iProp Σ).
Implicit Types τi : D.
Implicit Types Δ : listC D.
Implicit Types interp : listC D D.
Implicit Types Δ : listO D.
Implicit Types interp : listO D D.
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper.
Definition interp_unit : listC D -n> D := λne Δ w, (w = UnitV)%I.
Definition interp_unit : listO D -n> D := λne Δ w, (w = UnitV)%I.
Program Definition interp_prod
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
( w1 w2, w = PairV w1 w2 interp1 Δ w1 interp2 Δ w2)%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_sum
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
(( w1, w = InjLV w1 interp1 Δ w1) ( w2, w = InjRV w2 interp2 Δ w2))%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_arrow
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
( v, interp1 Δ v WP App (# w) (# v) {{ interp2 Δ }})%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_forall
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
(interp : listO D -n> D) : listO D -n> D := λne Δ w,
( τi : D,
⌜∀ v, Persistent (τi v) WP TApp (# w) {{ interp (τi :: Δ) }})%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Definition interp_rec1
(interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
(interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne w,
( ( v, w = FoldV v interp (τi :: Δ) v))%I.
Global Instance interp_rec1_contractive
(interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
(interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
Proof. by solve_contractive. Qed.
Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
fixpoint (interp_rec1 interp Δ) x interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
Next Obligation.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
Qed.
Fixpoint interp (τ : type) : listC D -n> D :=
Fixpoint interp (τ : type) : listO D -n> D :=
match τ return _ with
| TUnit => interp_unit
| TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2)
......@@ -70,11 +70,11 @@ Section logrel.
Notation "⟦ τ ⟧" := (interp τ).
Definition interp_env (Γ : list type)
(Δ : listC D) (vs : list val) : iProp Σ :=
(Δ : listO D) (vs : list val) : iProp Σ :=
(length Γ = length vs [] zip_with (λ τ, τ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
Definition interp_expr (τ : type) (Δ : listO D) (e : expr) : iProp Σ :=
WP e {{ τ Δ }}%I.
Class env_Persistent Δ :=
......@@ -116,7 +116,7 @@ Section logrel.
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
......@@ -135,11 +135,11 @@ Section logrel.
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..].
case EQ: (x - length Δ1) => [|n]; simpl.
{ symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
- intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
Qed.
......
......@@ -10,7 +10,7 @@ Notation "Γ ⊨ e : τ" := (log_typed Γ e τ) (at level 74, e, τ at next leve
Section fundamental.
Context `{heapG Σ}.
Notation D := (valC -n> iProp Σ).
Notation D := (valO -n> iProp Σ).
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) uconstr(Hp) :=
iApply (wp_bind (fill [ctx]));
......
......@@ -6,7 +6,7 @@ From iris_examples.logrel.F_mu_ref Require Import rules_binary.
Section bin_log_def.
Context `{heapG Σ,cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Notation D := (prodO valO valO -n> iProp Σ).
Definition bin_log_related (Γ : list type) (e e' : expr) (τ : type) :=
Δ vvs (ρ : cfg F_mu_ref_lang), env_Persistent Δ
......@@ -19,9 +19,9 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" :=
Section fundamental.
Context `{heapG Σ,cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Notation D := (prodO valO valO -n> iProp Σ).
Implicit Types e : expr.
Implicit Types Δ : listC D.
Implicit Types Δ : listO D.
Hint Resolve to_of_val.
Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
......
......@@ -214,9 +214,9 @@ Module F_mu_ref.
fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
Canonical Structure stateO := leibnizO state.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
End F_mu_ref.
Canonical Structure F_mu_ref_ectxi_lang := EctxiLanguage F_mu_ref.lang_mixin.
......
......@@ -9,52 +9,52 @@ Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *)
Section logrel.
Context `{heapG Σ}.
Notation D := (valC -n> iProp Σ).
Notation D := (valO -n> iProp Σ).
Implicit Types τi : D.
Implicit Types Δ : listC D.
Implicit Types interp : listC D D.
Implicit Types Δ : listO D.
Implicit Types interp : listO D D.
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper.
Definition interp_unit : listC D -n> D := λne Δ w, w = UnitV%I.
Definition interp_unit : listO D -n> D := λne Δ w, w = UnitV%I.
Program Definition interp_prod
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
( w1 w2, w = PairV w1 w2 interp1 Δ w1 interp2 Δ w2)%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_sum
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
(( w1, w = InjLV w1 interp1 Δ w1) ( w2, w = InjRV w2 interp2 Δ w2))%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_arrow
(interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
(interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w,
( v, interp1 Δ v WP App (# w) (# v) {{ interp2 Δ }})%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Program Definition interp_forall
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
(interp : listO D -n> D) : listO D -n> D := λne Δ w,
( τi : D,
( v, Persistent (τi v)) WP TApp (# w) {{ interp (τi :: Δ) }})%I.
Solve Obligations with repeat intros ?; simpl; solve_proper.
Definition interp_rec1
(interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
(interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne w,
( ( v, w = FoldV v interp (τi :: Δ) v))%I.
Global Instance interp_rec1_contractive
(interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
(interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
Proof. by solve_contractive. Qed.
Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
fixpoint (interp_rec1 interp Δ) x interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.
Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
fixpoint (interp_rec1 interp Δ).
Next Obligation.
intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper.
......@@ -65,11 +65,11 @@ Section logrel.
Solve Obligations with solve_proper.
Program Definition interp_ref
(interp : listC D -n> D) : listC D -n> D := λne Δ w,
(interp : listO D -n> D) : listO D -n> D := λne Δ w,
( l, w = LocV l inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I.
Solve Obligations with solve_proper.
Fixpoint interp (τ : type) : listC D -n> D :=
Fixpoint interp (τ : type) : listO D -n> D :=
match τ return _ with
| TUnit => interp_unit
| TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2)
......@@ -83,11 +83,11 @@ Section logrel.
Notation "⟦ τ ⟧" := (interp τ).
Definition interp_env (Γ : list type)
(Δ : listC D) (vs : list val) : iProp Σ :=
(Δ : listO D) (vs : list val) : iProp Σ :=
(length Γ = length vs [] zip_with (λ τ, τ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
Definition interp_expr (τ : type) (Δ : listO D) (e : expr) : iProp Σ :=
WP e {{ τ Δ }}%I.
Class env_Persistent Δ :=
......@@ -129,7 +129,7 @@ Section logrel.