Derive lifting axioms for ectx languages

This required a new ectx axiom: Positivity of evaluation contexts. This axiom was
also present in the old Iris 1.1 development, back when it still derived lifting
axioms for ectx languages.

_CoqProject

@@ -71,6 +71,7 @@ program_logic/resources.v
 program_logic/hoare.v
 program_logic/language.v
 program_logic/ectx_language.v
+program_logic/ectx_weakestpre.v
 program_logic/ghost_ownership.v
 program_logic/global_functor.v
 program_logic/saved_prop.v

heap_lang/lang.v

@@ -584,7 +584,7 @@ Program Canonical Structure heap_ectx_lang :
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
   heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step,
   heap_lang.fill_inj', heap_lang.fill_not_val, heap_lang.atomic_fill,
-  heap_lang.step_by_val, fold_right_app.
+  heap_lang.step_by_val, fold_right_app, app_eq_nil.
 
 Canonical Structure heap_lang := ectx_lang heap_ectx_lang.
 

heap_lang/lifting.v

-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.program_logic Require Import lifting.
+From iris.program_logic Require Export ectx_weakestpre.
 From iris.program_logic Require Import ownership. (* for ownP *)
+From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 Import uPred.
-Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
+Local Hint Extern 0 (head_reducible _ _) => do_step eauto 2.
 
 Section lifting.
 Context {Σ : iFunctor}.
@@ -13,10 +12,10 @@ Implicit Types Φ : val → iProp heap_lang Σ.
 Implicit Types K : ectx.
 Implicit Types ef : option (expr []).
 
-(** Bind. *)
+(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
   WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
-Proof. apply: weakestpre.wp_bind. Qed.
+Proof. exact: wp_ectx_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Φ :
@@ -27,7 +26,7 @@ Proof.
   (* TODO: This works around ssreflect bug #22. *)
   intros. set (φ (e' : expr []) σ' ef := ∃ l,
     ef = None ∧ e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
-  rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
+  rewrite -(wp_lift_atomic_head_step (Alloc e) φ σ) // /φ;
     last (by intros; inv_step; eauto 8); last (by simpl; eauto).
   apply sep_mono, later_mono; first done.
   apply forall_intro=>v2; apply forall_intro=>σ2; apply forall_intro=>ef.
@@ -43,7 +42,7 @@ Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
   (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊢ WP Load (Loc l) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
+  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ None) ?right_id //;
     last (by intros; inv_step; eauto using to_of_val); simpl; by eauto.
 Qed.
 
@@ -52,7 +51,7 @@ Lemma wp_store_pst E σ l e v v' Φ :
   (▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit)))
   ⊢ WP Store (Loc l) e @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
+  intros. rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) None)
     ?right_id //; last (by intros; inv_step; eauto); simpl; by eauto.
 Qed.
 
@@ -61,7 +60,7 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
   (▷ ownP σ ★ ▷ (ownP σ -★ Φ (LitV $ LitBool false)))
   ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
+  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
     ?right_id //; last (by intros; inv_step; eauto);
     simpl; split_and?; by eauto.
 Qed.
@@ -71,7 +70,7 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
   (▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (LitV $ LitBool true)))
   ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true)
+  intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
     (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_step; eauto);
     simpl; split_and?; by eauto.
 Qed.
@@ -80,7 +79,7 @@ Qed.
 Lemma wp_fork E e Φ :
   (▷ Φ (LitV LitUnit) ★ ▷ WP e {{ λ _, True }}) ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
+  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) (Some e)) //=;
     last by intros; inv_step; eauto.
   rewrite later_sep -(wp_value _ _ (Lit _)) //.
 Qed.
@@ -90,7 +89,7 @@ Lemma wp_rec E f x e1 e2 v Φ :
   ▷ WP subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
   ⊢ WP App (Rec f x e1) e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (App _ _)
+  intros. rewrite -(wp_lift_pure_det_head_step (App _ _)
     (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
     intros; inv_step; eauto.
 Qed.
@@ -106,7 +105,7 @@ Lemma wp_un_op E op l l' Φ :
   un_op_eval op l = Some l' →
   ▷ Φ (LitV l') ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
+  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
     ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
@@ -114,21 +113,21 @@ Lemma wp_bin_op E op l1 l2 l' Φ :
   bin_op_eval op l1 l2 = Some l' →
   ▷ Φ (LitV l') ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
 Proof.
-  intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
+  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
     ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Φ :
   ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
+  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 None)
     ?right_id //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Φ :
   ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
 Proof.
-  rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
+  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 None)
     ?right_id //; intros; inv_step; eauto.
 Qed.
 
@@ -136,7 +135,7 @@ Lemma wp_fst E e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
+  intros. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 None)
     ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
@@ -144,7 +143,7 @@ Lemma wp_snd E e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
+  intros. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 None)
     ?right_id -?wp_value //; intros; inv_step; eauto.
 Qed.
 
@@ -152,7 +151,7 @@ Lemma wp_case_inl E e0 v0 e1 e2 Φ :
   to_val e0 = Some v0 →
   ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
+  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
     (App e1 e0) None) ?right_id //; intros; inv_step; eauto.
 Qed.
 
@@ -160,7 +159,7 @@ Lemma wp_case_inr E e0 v0 e1 e2 Φ :
   to_val e0 = Some v0 →
   ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
+  intros. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
     (App e2 e0) None) ?right_id //; intros; inv_step; eauto.
 Qed.
 

heap_lang/tactics.v

@@ -13,14 +13,6 @@ Ltac inv_step :=
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
   | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
-  | H : prim_step _ _ _ _ _ _ |- _ => destruct H; subst
-  | H : _ = fill ?K ?e |- _ =>
-     destruct K as [|[]];
-     simpl in H; first [subst e|discriminate H|injection H as H]
-     (* ensure that we make progress for each subgoal *)
-  | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
-    apply val_stuck, (fill_not_val K) in H;
-    by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
   | H : head_step ?e _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if e is a variable
      and can thus better be avoided. *)
@@ -77,16 +69,14 @@ and [head_step] by performing a reduction step and uses [tac] to solve any
 side-conditions generated by individual steps. In case of goals of the shape
 [reducible] and [prim_step], it will try to decompose to expression on the LHS
 into an evaluation context and head-redex. *)
-Ltac do_step tac :=
-  try match goal with |- language.reducible _ _ => eexists _, _, _ end;
+Tactic Notation "do_step" tactic3(tac) :=
+  try match goal with |- head_reducible _ _ => eexists _, _, _ end;
   simpl;
   match goal with
-  | |- prim_step _ ?e1 ?σ1 ?e2 ?σ2 ?ef =>
-     reshape_expr e1 ltac:(fun K e1' =>
-       eapply Ectx_step with K e1' _; [reflexivity|reflexivity|];
-       first [apply alloc_fresh|econstructor; try reflexivity; simpl_subst];
-       rewrite ?to_of_val; tac; fail)
   | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
      first [apply alloc_fresh|econstructor];
-     rewrite ?to_of_val; tac; fail
+     (* If there is at least one goal left now, then do the last
+        goal last -- it may rely on evars being instantiaed elsewhere. *)
+     first [ fail
+           | rewrite ?to_of_val; [tac..|]; tac; fast_done ]
   end.

program_logic/ectx_language.v

@@ -21,6 +21,12 @@ Class ectx_language (expr val ectx state : Type) := EctxLanguage {
   fill_inj K e1 e2 : fill K e1 = fill K e2 → e1 = e2;
   fill_not_val K e : to_val e = None → to_val (fill K e) = None;
 
+  (* There are a whole lot of sensible axioms we could demand for comp_ectx
+     and empty_ectx. However, this one is enough. *)
+  ectx_positive K1 K2 :
+    empty_ectx = comp_ectx K1 K2 →
+    K1 = empty_ectx ∧ K2 = empty_ectx;
+
   step_by_val K K' e1 e1' σ1 e2 σ2 ef :
     fill K e1 = fill K' e1' →
     to_val e1 = None →
@@ -52,6 +58,7 @@ Arguments fill_empty {_ _ _ _ _} _.
 Arguments fill_comp {_ _ _ _ _} _ _ _.
 Arguments fill_inj {_ _ _ _ _} _ _ _ _.
 Arguments fill_not_val {_ _ _ _ _} _ _ _.
+Arguments ectx_positive {_ _ _ _ _} _ _ _.
 Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
 Arguments atomic_not_val {_ _ _ _ _} _ _.
 Arguments atomic_step {_ _ _ _ _} _ _ _ _ _ _ _.
@@ -59,9 +66,12 @@ Arguments atomic_fill {_ _ _ _ _} _ _ _ _.
 
 (* From an ectx_language, we can construct a language. *)
 Section Language.
-  Context {expr val ectx state : Type} (Λ : ectx_language expr val ectx state).
+  Context {expr val ectx state : Type} {Λ : ectx_language expr val ectx state}.
   Implicit Types (e : expr) (K : ectx).
 
+  Definition head_reducible (e : expr) (σ : state) :=
+    ∃ e' σ' ef, head_step e σ e' σ' ef.
+
   Inductive prim_step (e1 : expr) (σ1 : state)
     (e2 : expr) (σ2: state) (ef: option expr) : Prop :=
   Ectx_step K e1' e2' :
@@ -89,6 +99,27 @@ Section Language.
     language.atomic_step := atomic_prim_step
   |}.
 
+  (* Some lemmas about this language *)
+  Lemma head_prim_reducible e σ :
+    head_reducible e σ → reducible e σ.
+  Proof.
+    intros (e'&?&?&?). do 3 eexists.
+    eapply Ectx_step with (K:=empty_ectx); rewrite ?fill_empty; done.
+  Qed.
+
+  Lemma head_reducible_prim_step e1 σ1 e2 σ2 ef :
+    head_reducible e1 σ1 → prim_step e1 σ1 e2 σ2 ef →
+    head_step e1 σ1 e2 σ2 ef.
+  Proof.
+    intros Hred Hstep. destruct Hstep as [? ? ? ? ? Hstep]; subst.
+    rename e1' into e1. rename e2' into e2.
+    destruct Hred as (e2'&σ2'&ef'&HstepK).
+    destruct (step_by_val K empty_ectx e1 (fill K e1) σ1 e2' σ2' ef')
+      as [K' [-> _]%ectx_positive];
+      eauto using fill_empty, fill_not_val, val_stuck.
+    by rewrite !fill_empty.
+  Qed.
+
   (* Every evaluation context is a context. *)
   Global Instance ectx_lang_ctx K : LanguageCtx ectx_lang (fill K).
   Proof.
@@ -104,6 +135,7 @@ Section Language.
   Qed.
 End Language.
   
+Arguments ectx_lang {_ _ _ _} _ : clear implicits.
 
 
 

program_logic/ectx_weakestpre.v

+(** Some derived lemmas for ectx-based languages *)
+From iris.program_logic Require Export ectx_language weakestpre lifting.
+From iris.program_logic Require Import ownership.
+
+Section wp.
+Context {expr val ectx state: Type} {Λ : ectx_language expr val ectx state}
+        {Σ : iFunctor}.
+Implicit Types P : iProp (ectx_lang Λ) Σ.
+Implicit Types Φ : val → iProp (ectx_lang Λ) Σ.
+Implicit Types v : val.
+Implicit Types e : expr.
+
+Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I.
+
+Lemma wp_ectx_bind {E e} K Φ :
+  WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+Proof. apply: weakestpre.wp_bind. Qed.
+
+Lemma wp_lift_head_step E1 E2
+    (φ : expr → state → option expr → Prop) Φ e1 σ1 :
+  E2 ⊆ E1 → to_val e1 = None →
+  head_reducible e1 σ1 →
+  (∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  (|={E1,E2}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef,
+    (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E2,E1}=> WP e2 @ E1 {{ Φ }} ★ wp_fork ef)
+  ⊢ WP e1 @ E1 {{ Φ }}.
+Proof.
+  intros. apply wp_lift_step;
+            eauto using head_prim_reducible, head_reducible_prim_step.
+Qed.
+
+Lemma wp_lift_pure_head_step E (φ : expr → option expr → Prop) Φ e1 :
+  to_val e1 = None →
+  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1 e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
+  (▷ ∀ e2 ef, ■ φ e2 ef → WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  intros. apply wp_lift_pure_step;
+            eauto using head_prim_reducible, head_reducible_prim_step.
+Qed.
+
+Lemma wp_lift_atomic_head_step {E Φ} e1
+    (φ : expr → state → option expr → Prop) σ1 :
+  atomic e1 →
+  head_reducible e1 σ1 →
+  (∀ e2 σ2 ef,
+    head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  (▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
+  ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  intros. apply wp_lift_atomic_step;
+            eauto using head_prim_reducible, head_reducible_prim_step.
+Qed.
+
+Lemma wp_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 ef :
+  atomic e1 →
+  head_reducible e1 σ1 →
+  (∀ e2' σ2' ef', head_step e1 σ1 e2' σ2' ef' →
+    σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
+  (▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  intros. apply wp_lift_atomic_det_step;
+            eauto using head_prim_reducible, head_reducible_prim_step.
+Qed.
+
+Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 ef :
+  to_val e1 = None →
+  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1 e2' σ2 ef', head_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
+  ▷ (WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
+Proof.
+  intros. apply wp_lift_pure_det_step;
+            eauto using head_prim_reducible, head_reducible_prim_step.
+Qed.
+
+End wp.

tests/heap_lang.v

@@ -5,13 +5,13 @@ Import uPred.
 
 Section LangTests.
   Definition add : expr [] := (#21 + #21)%E.
-  Goal ∀ σ, prim_step heap_ectx_lang add σ (#42) σ None.
+  Goal ∀ σ, head_step add σ (#42) σ None.
   Proof. intros; do_step done. Qed.
   Definition rec_app : expr [] := ((rec: "f" "x" := '"f" '"x") #0)%E.
-  Goal ∀ σ, prim_step heap_ectx_lang rec_app σ rec_app σ None.
-  Proof. intros. rewrite /rec_app. do_step done. Qed.
+  Goal ∀ σ, head_step rec_app σ rec_app σ None.
+  Proof. intros. rewrite /rec_app. do_step simpl_subst. Qed.
   Definition lam : expr [] := (λ: "x", '"x" + #21)%E.
-  Goal ∀ σ, prim_step heap_ectx_lang (lam #21)%E σ add σ None.
+  Goal ∀ σ, head_step (lam #21)%E σ add σ None.
   Proof. intros. rewrite /lam. do_step done. Qed.
 End LangTests.