Merge branch 'v2.0' of gitlab.mpi-sws.org:FP/iris-coq into v2.0

5c232f1e · Ralf Jung · 83979416 · a39468f8 · 5c232f1e · 5c232f1e
Commit 5c232f1e authored Feb 01, 2016 by Ralf Jung
37 changed files
--- a/README
+++ b/README
@@ -7,10 +7,11 @@ This version is known to compile with:
 - Ssreflect 1.6
 - Autosubst 1.4

-For development, better make sure you have a version of Ssreflect that includes commit be724937
-(no such version has been released so far, you'll have to fetch the development branch yourself).
-Iris compiles fine even without this patch, but proof bullets will only be in 'strict' (enforcing)
-mode with the fixed version of Ssreflect.
+For development, better make sure you have a version of Ssreflect that includes
+commit be724937 (no such version has been released so far, you will have to
+fetch the development branch yourself). Iris compiles fine even without this
+patch, but proof bullets will only be in 'strict' (enforcing) mode with the
+fixed version of Ssreflect.
 
 BUILDING INSTRUCTIONS
 ---------------------

--- a/_CoqProject
+++ b/_CoqProject
@@ -36,6 +36,8 @@ prelude/list.v
 prelude/error.v
 modures/option.v
 modures/cmra.v
+modures/cmra_big_op.v
+modures/cmra_tactics.v
 modures/sts.v
 modures/auth.v
 modures/fin_maps.v
@@ -45,7 +47,6 @@ modures/base.v
 modures/dra.v
 modures/cofe_solver.v
 modures/agree.v
-modures/ra.v
 modures/excl.v
 iris/model.v
 iris/adequacy.v
@@ -56,14 +57,13 @@ iris/viewshifts.v
 iris/wsat.v
 iris/ownership.v
 iris/weakestpre.v
-iris/language.v
 iris/pviewshifts.v
 iris/resources.v
 iris/hoare.v
-iris/parameter.v
+iris/language.v
+iris/functor.v
 iris/tests.v
 barrier/heap_lang.v
-barrier/parameter.v
 barrier/lifting.v
 barrier/sugar.v
 barrier/tests.v
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -390,8 +390,10 @@ Section Language.
  Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
    ∃ K e1' e2', e1 = fill K e1' ∧ e2 = fill K e2' ∧
                 prim_step e1' σ1 e2' σ2 ef.
-
-  Global Program Instance heap_lang : Language expr value state := {|
+  Program Canonical Structure heap_lang : language := {|
+    language.expr := expr;
+    language.val := value;
+    language.state := state;
    of_val := v2e;
    to_val := e2v;
    language.atomic := atomic;

--- a/barrier/lifting.v
+++ b/barrier/lifting.v
 Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.parameter.
+Require Export iris.weakestpre barrier.heap_lang.
 Import uPred.

-(* TODO RJ: Figure out a way to to always use our Σ. *)
+Section lifting.
+Context {Σ : iFunctor}.
+Implicit Types P : iProp heap_lang Σ.
+Implicit Types Q : val heap_lang → iProp heap_lang Σ.

 (** Bind. *)
 Lemma wp_bind {E e} K Q :
-  wp (Σ:=Σ) E e (λ v, wp (Σ:=Σ) E (fill K (v2e v)) Q) ⊑ wp (Σ:=Σ) E (fill K e) Q.
-Proof.
-  by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx.
-Qed.
+  wp E e (λ v, wp E (fill K (v2e v)) Q) ⊑ wp E (fill K e) Q.
+Proof. apply (wp_bind (K:=fill K)), fill_is_ctx. Qed.

 (** Base axioms for core primitives of the language: Stateful reductions. *)

@@ -17,9 +18,9 @@ Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
  E1 ⊆ E2 → to_val e1 = None →
  reducible e1 σ1 →
  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → ef = None ∧ φ e2 σ2) →
-  pvs E2 E1 (ownP (Σ:=Σ) σ1 ★ ▷ ∀ e2 σ2, (■ φ e2 σ2 ∧ ownP (Σ:=Σ) σ2) -★
-    pvs E1 E2 (wp (Σ:=Σ) E2 e2 Q))
-  ⊑ wp (Σ:=Σ) E2 e1 Q.
+  pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2, (■ φ e2 σ2 ∧ ownP σ2) -★
+    pvs E1 E2 (wp E2 e2 Q))
+  ⊑ wp E2 e1 Q.
 Proof.
  intros ? He Hsafe Hstep.
  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
@@ -45,8 +46,8 @@ Qed.
   postcondition a predicate over a *location* *)
 Lemma wp_alloc_pst E σ e v Q :
  e2v e = Some v →
-  (ownP (Σ:=Σ) σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ) -★ Q (LocV l)))
-       ⊑ wp (Σ:=Σ) E (Alloc e) Q.
+  (ownP σ ★ ▷(∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
+       ⊑ wp E (Alloc e) Q.
 Proof.
  (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
  intros Hvl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
@@ -72,7 +73,7 @@ Qed.

 Lemma wp_load_pst E σ l v Q :
  σ !! l = Some v →
-  (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q v)) ⊑ wp (Σ:=Σ) E (Load (Loc l)) Q.
+  (ownP σ ★ ▷(ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
 Proof.
  intros Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
    (φ := λ e' σ', e' = v2e v ∧ σ' = σ); last first.
@@ -93,7 +94,7 @@ Qed.
 Lemma wp_store_pst E σ l e v v' Q :
  e2v e = Some v →
  σ !! l = Some v' →
-  (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp (Σ:=Σ) E (Store (Loc l) e) Q.
+  (ownP σ ★ ▷(ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
 Proof.
  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
    (φ := λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ); last first.
@@ -114,17 +115,12 @@ Qed.
 Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
  e2v e1 = Some v1 → e2v e2 = Some v2 →
  σ !! l = Some v' → v' <> v1 →
-  (ownP (Σ:=Σ) σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q.
+  (ownP σ ★ ▷(ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
-    (φ := λ e' σ', e' = LitFalse ∧ σ' = σ); last first.
-  - intros e2' σ2' ef Hstep. inversion_clear Hstep; first done.
-    (* FIXME this rewriting is rather ugly. *)
-    exfalso. rewrite Hvl in Hv1. case:Hv1=>?; subst v1. rewrite Hlookup in H.
-    case:H=>?; subst v'. done.
-  - do 3 eexists. eapply CasFailS; eassumption.
-  - reflexivity.
-  - reflexivity.
+    (φ := λ e' σ', e' = LitFalse ∧ σ' = σ) (E1:=E); auto; last first.
+  - by inversion_clear 1; simplify_map_equality.
+  - do 3 eexists; econstructor; eauto.
  - rewrite -pvs_intro.
    apply sep_mono; first done. apply later_mono.
    apply forall_intro=>e2'. apply forall_intro=>σ2'.
@@ -137,7 +133,7 @@ Qed.
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
  e2v e1 = Some v1 → e2v e2 = Some v2 →
  σ !! l = Some v1 →
-  (ownP (Σ:=Σ) σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp (Σ:=Σ) E (Cas (Loc l) e1 e2) Q.
+  (ownP σ ★ ▷(ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (σ1 := σ)
    (φ := λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ); last first.
@@ -162,7 +158,8 @@ Qed.
 (** Base axioms for core primitives of the language: Stateless reductions *)

 Lemma wp_fork E e :
-  ▷ wp (Σ:=Σ) coPset_all e (λ _, True) ⊑ wp (Σ:=Σ) E (Fork e) (λ v, ■(v = LitUnitV)).
+  ▷ wp coPset_all e (λ _, True : iProp heap_lang Σ)
+  ⊑ wp E (Fork e) (λ v, ■(v = LitUnitV)).
 Proof.
  etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e' ef, e' = LitUnit ∧ ef = Some e);
@@ -175,21 +172,16 @@ Proof.
    eapply ForkS.
  - reflexivity.
  - apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>ef.
-    apply impl_intro_l. apply const_elim_l. intros [-> ->].
-    (* FIXME RJ This is ridicolous. *)
-    transitivity (True ★ wp coPset_all e (λ _ : ival Σ, True))%I;
-      first by rewrite left_id.
-    apply sep_mono; last reflexivity.
-    rewrite -wp_value'; last reflexivity.
-    by apply const_intro.
+    apply forall_intro=>e2; apply forall_intro=>ef.
+    apply impl_intro_l, const_elim_l=>-[-> ->] /=; apply sep_intro_True_l; auto.
+    by rewrite -wp_value' //; apply const_intro.
 Qed.

 Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 :
  to_val e1 = None →
  (∀ σ1, reducible e1 σ1) →
  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ ef = None ∧ φ e2) →
-  (▷ ∀ e2, ■ φ e2 → wp (Σ:=Σ) E e2 Q) ⊑ wp (Σ:=Σ) E e1 Q.
+  (▷ ∀ e2, ■ φ e2 → wp E e2 Q) ⊑ wp E e1 Q.
 Proof.
  intros He Hsafe Hstep.
  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
@@ -209,7 +201,7 @@ Qed.

 Lemma wp_rec E ef e v Q :
  e2v e = Some v →
-  ▷wp (Σ:=Σ) E ef.[Rec ef, e /] Q ⊑ wp (Σ:=Σ) E (App (Rec ef) e) Q.
+  ▷wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
 Proof.
  etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = ef.[Rec ef, e /]); last first.
@@ -221,7 +213,7 @@ Proof.
 Qed.

 Lemma wp_plus n1 n2 E Q :
-  ▷Q (LitNatV (n1 + n2)) ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
+  ▷Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
  etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = LitNat (n1 + n2)); last first.
@@ -235,7 +227,7 @@ Qed.

 Lemma wp_le_true n1 n2 E Q :
  n1 ≤ n2 →
-  ▷Q LitTrueV ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
+  ▷Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
  intros Hle. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = LitTrue); last first.
@@ -250,7 +242,7 @@ Qed.

 Lemma wp_le_false n1 n2 E Q :
  n1 > n2 →
-  ▷Q LitFalseV ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
+  ▷Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
  intros Hle. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = LitFalse); last first.
@@ -265,7 +257,7 @@ Qed.

 Lemma wp_fst e1 v1 e2 v2 E Q :
  e2v e1 = Some v1 → e2v e2 = Some v2 →
-  ▷Q v1 ⊑ wp (Σ:=Σ) E (Fst (Pair e1 e2)) Q.
+  ▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
 Proof.
  intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e1); last first.
@@ -279,7 +271,7 @@ Qed.

 Lemma wp_snd e1 v1 e2 v2 E Q :
  e2v e1 = Some v1 → e2v e2 = Some v2 →
-  ▷Q v2 ⊑ wp (Σ:=Σ) E (Snd (Pair e1 e2)) Q.
+  ▷Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
 Proof.
  intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e2); last first.
@@ -293,7 +285,7 @@ Qed.

 Lemma wp_case_inl e0 v0 e1 e2 E Q :
  e2v e0 = Some v0 →
-  ▷wp (Σ:=Σ) E e1.[e0/] Q ⊑ wp (Σ:=Σ) E (Case (InjL e0) e1 e2) Q.
+  ▷wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
 Proof.
  intros Hv0. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e1.[e0/]); last first.
@@ -306,7 +298,7 @@ Qed.

 Lemma wp_case_inr e0 v0 e1 e2 E Q :
  e2v e0 = Some v0 →
-  ▷wp (Σ:=Σ) E e2.[e0/] Q ⊑ wp (Σ:=Σ) E (Case (InjR e0) e1 e2) Q.
+  ▷wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
 Proof.
  intros Hv0. etransitivity; last eapply wp_lift_pure_step with
    (φ := λ e', e' = e2.[e0/]); last first.
@@ -322,7 +314,7 @@ Qed.
 Lemma wp_le n1 n2 E P Q :
  (n1 ≤ n2 → P ⊑ ▷Q LitTrueV) →
  (n1 > n2 → P ⊑ ▷Q LitFalseV) →
-  P ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
+  P ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
  intros HPle HPgt.
  assert (Decision (n1 ≤ n2)) as Hn12 by apply _.
@@ -330,3 +322,4 @@ Proof.
  - rewrite -wp_le_true; auto.
  - assert (n1 > n2) by omega. rewrite -wp_le_false; auto.
 Qed.
+End lifting.
--- a/barrier/parameter.v
+++ b/barrier/parameter.v
-Require Export barrier.heap_lang.
-Require Import iris.parameter.
-
-Definition Σ := IParamConst heap_lang unitRA.
--- a/barrier/sugar.v
+++ b/barrier/sugar.v
@@ -16,10 +16,14 @@ Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
 Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1.
 Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]).

+Section suger.
+Context {Σ : iFunctor}.
+Implicit Types P : iProp heap_lang Σ.
+Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+
 (** Proof rules for the sugar *)
 Lemma wp_lam E ef e v Q :
-  e2v e = Some v →
-  ▷wp (Σ:=Σ) E ef.[e/] Q ⊑ wp (Σ:=Σ) E (App (Lam ef) e) Q.
+  e2v e = Some v → ▷wp E ef.[e/] Q ⊑ wp E (App (Lam ef) e) Q.
 Proof.
  intros Hv. rewrite -wp_rec; last eassumption.
  (* RJ: This pulls in functional extensionality. If that bothers us, we have
@@ -28,20 +32,20 @@ Proof.
 Qed.

 Lemma wp_let e1 e2 E Q :
-  wp (Σ:=Σ) E e1 (λ v, ▷wp (Σ:=Σ) E (e2.[v2e v/]) Q) ⊑ wp (Σ:=Σ) E (Let e1 e2) Q.
+  wp E e1 (λ v, ▷wp E (e2.[v2e v/]) Q) ⊑ wp E (Let e1 e2) Q.
 Proof.
  rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v.
  rewrite -wp_lam //. by rewrite v2v.
 Qed.

 Lemma wp_if_true e1 e2 E Q :
-  ▷wp (Σ:=Σ) E e1 Q ⊑ wp (Σ:=Σ) E (If LitTrue e1 e2) Q.
+  ▷wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q.
 Proof.
  rewrite -wp_case_inl //. by asimpl.
 Qed.

 Lemma wp_if_false e1 e2 E Q :
-  ▷wp (Σ:=Σ) E e2 Q ⊑ wp (Σ:=Σ) E (If LitFalse e1 e2) Q.
+  ▷wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q.
 Proof.
  rewrite -wp_case_inr //. by asimpl.
 Qed.
@@ -49,7 +53,7 @@ Qed.
 Lemma wp_lt n1 n2 E P Q :
  (n1 < n2 → P ⊑ ▷Q LitTrueV) →
  (n1 ≥ n2 → P ⊑ ▷Q LitFalseV) →
-  P ⊑ wp (Σ:=Σ) E (Lt (LitNat n1) (LitNat n2)) Q.
+  P ⊑ wp E (Lt (LitNat n1) (LitNat n2)) Q.
 Proof.
  intros HPlt HPge.
  rewrite -(wp_bind (LeLCtx EmptyCtx _)) -wp_plus -later_intro. simpl.
@@ -59,7 +63,7 @@ Qed.
 Lemma wp_eq n1 n2 E P Q :
  (n1 = n2 → P ⊑ ▷Q LitTrueV) →
  (n1 ≠ n2 → P ⊑ ▷Q LitFalseV) →
-  P ⊑ wp (Σ:=Σ) E (Eq (LitNat n1) (LitNat n2)) Q.
+  P ⊑ wp E (Eq (LitNat n1) (LitNat n2)) Q.
 Proof.
  intros HPeq HPne.
  rewrite -wp_let -wp_value' // -later_intro. asimpl.
@@ -72,3 +76,4 @@ Proof.
  - asimpl. rewrite -wp_case_inr // -later_intro -wp_value' //.
    apply HPne; omega.
 Qed.
+End suger.
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -25,16 +25,16 @@ Module LangTests.
  Qed.
 End LangTests.

-Module ParamTests.
-  Print Assumptions Σ.
-End ParamTests.
-
 Module LiftingTests.
+  Context {Σ : iFunctor}.
+  Implicit Types P : iProp heap_lang Σ.
+  Implicit Types Q : val heap_lang → iProp heap_lang Σ.
+
  (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
  Definition e3 := Load (Var 0).
  Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
  Definition e := Let (Alloc (LitNat 1)) e2.
-  Goal ∀ σ E, (ownP (Σ:=Σ) σ) ⊑ (wp (Σ:=Σ) E e (λ v, ■(v = LitNatV 2))).
+  Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = LitNatV 2))).
  Proof.
    move=> σ E. rewrite /e.
    rewrite -wp_let. rewrite -wp_alloc_pst; last done.
@@ -74,7 +74,7 @@ Module LiftingTests.

  Lemma FindPred_spec n1 n2 E Q :
    (■(n1 < n2) ∧ Q (LitNatV $ pred n2)) ⊑
-       wp (Σ:=Σ) E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
+       wp E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
  Proof.
    revert n1. apply löb_all_1=>n1.
    rewrite -wp_rec //. asimpl.
@@ -104,7 +104,7 @@ Module LiftingTests.
  Qed.

  Lemma Pred_spec n E Q :
-    ▷Q (LitNatV $ pred n) ⊑ wp (Σ:=Σ) E (App Pred (LitNat n)) Q.
+    ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
  Proof.
    rewrite -wp_lam //. asimpl.
    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
@@ -118,7 +118,9 @@ Module LiftingTests.
      + done.
  Qed.

-  Goal ∀ E, True ⊑ wp (Σ:=Σ) E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
+  Goal ∀ E,
+    (True : iProp heap_lang Σ)
+    ⊑ wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
  Proof.
    intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
    asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)

--- a/iris/adequacy.v
+++ b/iris/adequacy.v
@@ -7,9 +7,10 @@ Local Hint Extern 10 (✓{_} _) =>
  solve_validN.

 Section adequacy.
-Context {Σ : iParam}.
-Implicit Types e : iexpr Σ.
-Implicit Types Q : ival Σ → iProp Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types e : expr Λ.
+Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types m : iGst Λ Σ.
 Transparent uPred_holds.

 Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp coPset_all e Q) n r)).
@@ -46,7 +47,7 @@ Proof.
  * apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 ⋅ r2' :: rs2)).
    { rewrite /option_list right_id_L.
      apply Forall3_app, Forall3_cons; eauto using wptp_le.
-      apply uPred_weaken with r2 (k + n); eauto using @ra_included_l. }
+      apply uPred_weaken with r2 (k + n); eauto using cmra_included_l. }
    by rewrite -Permutation_middle /= big_op_app.
 Qed.
 Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 :
@@ -60,7 +61,7 @@ Proof.
  intros Hht ????; apply (nsteps_wptp [pvs coPset_all coPset_all ∘ Q] k n
    ([e1],σ1) (t2,σ2) [r1]); rewrite /big_op ?right_id; auto.
  constructor; last constructor.
-  apply Hht with r1 (k + n); eauto using @ra_included_unit.
+  apply Hht with r1 (k + n); eauto using cmra_included_unit.
  by destruct (k + n).
 Qed.
 Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
@@ -70,15 +71,16 @@ Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 :
  ∃ rs2 Qs', wptp 3 t2 ((λ v, pvs coPset_all coPset_all (Q v)) :: Qs') rs2 ∧
             wsat 3 coPset_all σ2 (big_op rs2).
 Proof.
-  intros Hv ? [k ?]%rtc_nsteps. eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
-  - by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN.
-  - exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m). split_ands.
-    + by rewrite /op /cmra_op /= /res_op /= !ra_empty_l ra_empty_r.
-    + by rewrite /uPred_holds /=.
-    + by apply ownG_spec.
+  intros Hv ? [k ?]%rtc_nsteps.
+  eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) m)); eauto; [|].
+  { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
+  exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ m); split_ands.
+  * by rewrite Res_op ?left_id ?right_id.
+  * by rewrite /uPred_holds /=.
+  * by apply ownG_spec.
 Qed.
 Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
-  ✓m →
+  ✓ m →
  {{ ownP σ1 ★ ownG m }} e @ E {{ λ v', ■ φ v' }} →
  rtc step ([e], σ1) (of_val v :: t2, σ2) →
  φ v.
@@ -92,7 +94,7 @@ Proof.
  by rewrite right_id_L.
 Qed.
 Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 :
-  ✓m →
+  ✓ m →
  {{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} →
  rtc step ([e1], σ1) (t2, σ2) →
  e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
@@ -106,7 +108,7 @@ Proof.
    rewrite ?right_id_L ?big_op_delete; auto.
 Qed.
 Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 :
-  ✓m →
+  ✓ m →
  {{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} →
  rtc step ([e1], σ1) (t2, σ2) →
  Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).

--- a/iris/functor.v
+++ b/iris/functor.v
+Require Export modures.cmra.
+
+Structure iFunctor := IFunctor {
+  ifunctor_car :> cofeT → cmraT;
+  ifunctor_empty A : Empty (ifunctor_car A);
+  ifunctor_identity A : CMRAIdentity (ifunctor_car A);
+  ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
+  ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
+  ifunctor_map_id {A : cofeT} (x : ifunctor_car A) : ifunctor_map cid x ≡ x;
+  ifunctor_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
+    ifunctor_map (g ◎ f) x ≡ ifunctor_map g (ifunctor_map f x);
+  ifunctor_map_mono {A B} (f : A -n> B) : CMRAMonotone (ifunctor_map f)
+}.
+Existing Instances ifunctor_empty ifunctor_identity.
+Existing Instances ifunctor_map_ne ifunctor_map_mono.
+
+Lemma ifunctor_map_ext (Σ : iFunctor) {A B} (f g : A -n> B) m :
+  (∀ x, f x ≡ g x) → ifunctor_map Σ f m ≡ ifunctor_map Σ g m.
+Proof.
+  by intros; apply equiv_dist=> n; apply ifunctor_map_ne=> ?; apply equiv_dist.
+Qed.
+
+Program Definition iFunctor_const (icmra : cmraT) {icmra_empty : Empty icmra}
+    {icmra_identity : CMRAIdentity icmra} : iFunctor :=
+  {| ifunctor_car A := icmra; ifunctor_map A B f := cid |}.
+Solve Obligations with done.
\ No newline at end of file
--- a/iris/hoare.v
+++ b/iris/hoare.v
 Require Export iris.weakestpre iris.viewshifts.

-Definition ht {Σ} (E : coPset) (P : iProp Σ)
-    (e : iexpr Σ) (Q : ival Σ → iProp Σ) : iProp Σ :=
+Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
+    (e : expr Λ) (Q : val Λ → iProp Λ Σ) : iProp Λ Σ :=
  (□ (P → wp E e (λ v, pvs E E (Q v))))%I.
-Instance: Params (@ht) 2.
+Instance: Params (@ht) 3.

 Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : uPred_scope.
@@ -11,27 +11,27 @@ Notation "{{ P } } e @ E {{ Q } }" := (True ⊑ ht E P e Q)
  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : C_scope.

 Section hoare.
-Context {Σ : iParam}.
-Implicit Types P : iProp Σ.
-Implicit Types Q : ival Σ → iProp Σ.
-Implicit Types v : ival Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types P : iProp Λ Σ.
+Implicit Types Q : val Λ → iProp Λ Σ.
+Implicit Types v : val Λ.
 Import uPred.

 Global Instance ht_ne E n :
-  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (@ht Σ E).
+  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
 Global Instance ht_proper E :
-  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Σ E).
+  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
 Lemma ht_mono E P P' Q Q' e :
  P ⊑ P' → (∀ v, Q' v ⊑ Q v) → {{ P' }} e @ E {{ Q' }} ⊑ {{ P }} e @ E {{ Q }}.
 Proof. by intros HP HQ; rewrite /ht -HP; setoid_rewrite HQ. Qed.
 Global Instance ht_mono' E :
-  Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Σ E).
+  Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E).
 Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.

 Lemma ht_val E v :
-  {{ True }} of_val v @ E {{ λ v', ■ (v = v') }}.
+  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', ■ (v = v') }}.
 Proof.
  apply (always_intro' _ _), impl_intro_l.
  by rewrite -wp_value -pvs_intro; apply const_intro.

--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -8,12 +8,14 @@ Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : C_scope.

 Section lifting.
-Context {Σ : iParam}.
-Implicit Types e : iexpr Σ.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types e : expr Λ.
+Implicit Types P : iProp Λ Σ.
+Implicit Types R : val Λ → iProp Λ Σ.
 Import uPred.

 Lemma ht_lift_step E1 E2
-    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P P' Q1 Q2 R e1 σ1 :
+    (φ : expr Λ → state Λ → option (expr Λ) → Prop) P P' Q1 Q2 R e1 σ1 :
  E1 ⊆ E2 → to_val e1 = None →
  reducible e1 σ1 →
  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -42,8 +44,7 @@ Proof.
  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
  by apply const_intro.
 Qed.
-Lemma ht_lift_atomic E
-    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P e1 σ1 :
+Lemma ht_lift_atomic E (φ : expr Λ → state Λ → option (expr Λ) → Prop) P e1 σ1 :
  atomic e1 →
  reducible e1 σ1 →
  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -68,7 +69,7 @@ Proof.
    rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
    by rewrite -always_and_sep_r'; apply and_intro;