Support sequential languages.

_CoqProject

@@ -93,6 +93,11 @@ theories/program_logic/ectxi_language.v
 theories/program_logic/ectx_lifting.v
 theories/program_logic/gen_heap.v
 theories/program_logic/ownp.v
+theories/sequential/slanguage.v
+theories/sequential/weakestpre.v
+theories/sequential/lifting.v
+theories/sequential/adequacy.v
+theories/sequential/ownp.v
 theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v

theories/sequential/adequacy.v

+From iris.base_logic Require Import big_op soundness wsat.
+From iris.program_logic Require Import adequacy.
+From iris.sequential Require Import weakestpre slanguage.
+From iris.proofmode Require Import tactics.
+
+Record adequate {Λ} (p : bool) (ρ1 : cfg Λ) (φ : val Λ → Prop) := {
+  adequate_result σ2 v2 : rtc step ρ1 (of_val v2, σ2) → φ v2;
+  adequate_safe ρ2 : p → rtc step ρ1 ρ2 → progress ρ2
+}.
+
+Section adequacy.
+Context `{irisG Λ Σ} (p : bool).
+Implicit Types P : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Implicit Types σ : state Λ.
+
+Notation sworld σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
+Notation swp e Φ := (SWP e @ p; ⊤ {{ Φ }})%I.
+
+Notation world σ := (wsat ∗ ownE ∅ ∗ state_interp σ)%I.
+Notation wp e Φ := (WP e @ p; ∅ {{ v, |={∅,⊤}=> Φ v }})%I.
+
+Lemma swp_start σ e Φ : sworld σ ∗ swp e Φ ==∗ ◇ (world σ ∗ wp e Φ).
+Proof.
+  rewrite swp_eq /swp_def; iIntros "[(Hw&HE&?) H] /="; rewrite fupd_eq.
+  by iMod ("H" with "[Hw HE]") as ">($&$&?)"; iFrame.
+Qed.
+
+Lemma swp_stop σ v Φ : world σ ∗ wp (of_val v) Φ ==∗ ◇ (sworld σ ∗ Φ v).
+Proof.
+  iIntros "[(Hw&HE&?) H]"; rewrite wp_value_inv fupd_trans fupd_eq.
+  by iMod ("H" with "[Hw HE]") as ">(?&?&?)"; iFrame.
+Qed.
+
+Lemma swp_steps n e1 σ1 e2 σ2 Φ :
+  nsteps step n (e1, σ1) (e2, σ2) →
+  sworld σ1 ∗ swp e1 Φ  ⊢
+  Nat.iter (S n) (λ P, |==> ▷ P) (world σ2 ∗ wp e2 Φ).
+Proof.
+  rewrite swp_start.
+  revert e1 e2 σ1 σ2; simpl; induction n as [|n IH]=> e1 e2 σ1 σ2 /=.
+  { by inversion_clear 1; iIntros ">>H"; iFrame. }
+  iIntros (Hsteps) "H"; inversion_clear Hsteps as [|?? [e1' σ1']].
+  iMod "H" as ">H"; iMod (wp_step with "H"); first by constructor.
+  by rewrite big_sepL_nil uPred.sep_True; iApply IH.
+Qed.
+
+Lemma swp_result n e1 σ1 v2 σ2 φ :
+  nsteps step n (e1, σ1) (of_val v2, σ2) →
+  sworld σ1 ∗ SWP e1 @ p; ⊤ {{ v, ⌜φ v⌝ }} ⊢
+  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ v2⌝.
+Proof.
+  intros; rewrite swp_steps //.
+  rewrite (Nat_iter_S_r (S n)); apply bupd_iter_mono.
+  by rewrite swp_stop; iMod 1 as ">(?&?)"; iFrame.
+Qed.
+
+Lemma swp_safe n e1 σ1 e2 σ2 Φ :
+  nsteps step n (e1, σ1) (e2, σ2) →
+  sworld σ1 ∗ swp e1 Φ ⊢
+  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜if p then progress (e2, σ2) else True⌝.
+Proof.
+  intros ?; rewrite swp_steps //.
+  rewrite (Nat_iter_S_r (S n)); apply bupd_iter_mono; rewrite wp_safe.
+  by destruct p; first rewrite seq_progress.
+Qed.
+
+Lemma swp_invariance' n e1 σ1 e2 σ2 φ Φ :
+  nsteps step n (e1, σ1) (e2, σ2) →
+  (state_interp σ2 ={∅}=∗ ⌜φ⌝) ∗ sworld σ1 ∗ swp e1 Φ
+  ⊢ Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ⌝.
+Proof.
+  intros ?; rewrite swp_steps //.
+  rewrite (Nat_iter_S_r (S n)) !bupd_iter_frame_l; apply bupd_iter_mono.
+  iIntros "[Hobs ((Hw&HE&Hσ)&Hwp)]"; rewrite fupd_eq.
+  by iMod ("Hobs" with "Hσ [$Hw $HE]") as ">(_&_&$)".
+Qed.
+End adequacy.
+
+Theorem swp_adequacy Σ Λ `{invPreG Σ} p e σ φ :
+  (∀ `{Hinv : invG Σ},
+     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ ∗ SWP e @ p; ⊤ {{ v, ⌜φ v⌝ }}) →
+  adequate p (e, σ) φ.
+Proof.
+  intros Hwp; split.
+  - intros σ2 v2 [n ?]%rtc_nsteps.
+    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
+    rewrite Nat_iter_S; iMod wsat_alloc as (Hinv) "[Hw HE]".
+    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    iDestruct "Hwp" as (Istate) "[HI Hwp]"; iModIntro; iNext.
+    iApply (@swp_result _ _ (IrisG _ _ Hinv Istate)); eauto.
+    by iFrame; iApply Hwp.
+  - destruct p; last done; intros [σ2 e2] Hp [n ?]%rtc_nsteps.
+    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
+    rewrite Nat_iter_S; iMod wsat_alloc as (Hinv) "[Hw HE]".
+    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+    iDestruct "Hwp" as (Istate) "[HI Hwp]"; iModIntro; iNext.
+    iApply (@swp_safe _ _ (IrisG _ _ Hinv Istate) true); eauto.
+    by iFrame.
+Qed.
+
+Theorem swp_invariance Σ Λ `{invPreG Σ} p e1 σ1 e2 σ2 φ Φ :
+  (∀ `{Hinv : invG Σ},
+     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ1 ∗ SWP e1 @ p; ⊤ {{ Φ }} ∗ (stateI σ2 ={∅}=∗ ⌜φ⌝)) →
+  rtc step (e1, σ1) (e2, σ2) →
+  φ.
+Proof.
+  intros Hwp [n ?]%rtc_nsteps.
+  eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros.
+  rewrite Nat_iter_S; iMod wsat_alloc as (Hinv) "[Hw HE]".
+  rewrite {1}fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+  iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
+  iModIntro. iNext. iApply (@swp_invariance' _ _ (IrisG _ _ Hinv Istate)); eauto.
+  by iFrame.
+Qed.

theories/sequential/lifting.v

+From iris.program_logic Require Import lifting.
+From iris.sequential Require Import slanguage weakestpre.
+From iris.proofmode Require Import tactics.
+
+Section lifting.
+Context `{irisG Λ Σ}.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Implicit Types σ : state Λ.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+
+Lemma swp_lift_step p E1 E2 Φ e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E1,∅}=∗
+    ⌜reducible (e1, σ1)⌝ ∗
+    ▷ ∀ e2 σ2, ⌜step (e1, σ1) (e2, σ2) ⌝ ={∅,E1}=∗
+      state_interp σ2 ∗ SWP e2 @ p; E1,E2 {{ Φ }})
+  ⊢ SWP e1 @ p; E1,E2 {{ Φ }}.
+Proof.
+  iIntros (?) "H"; rewrite swp_eq /swp_def -wp_lift_step //.
+  iMod (fupd_intro_mask' _ ∅) as "Hclose"; first (by set_solver); iModIntro.
+  iIntros (?) "Hσ"; iMod "Hclose" as "_"; iMod ("H" $! _ with "Hσ") as "(%&H)".
+  iModIntro; iSplit; first (by rewrite -seq_reducible); iNext; iIntros (e2 σ2 efs) "#Hstep".
+  iDestruct "Hstep" as %[->Hstep]; rewrite big_sepL_nil uPred.sep_True.
+  by iMod ("H" $! _ _ with "[%]") as "[? ?]"; first done; iFrame.
+Qed.
+
+Lemma swp_lift_stuck E1 E2 Φ e :
+  to_val e = None →
+  (∀ σ, state_interp σ ={E1,∅}=∗ ⌜¬ progress (e, σ)⌝)
+  ⊢ SWP e @ E1, E2 ?{{ Φ }}.
+Proof.
+  iIntros (?) "H"; rewrite swp_eq /swp_def -wp_lift_stuck //.
+  iMod (fupd_intro_mask' _ ∅) as "Hclose"; first (by set_solver); iModIntro.
+  by iIntros (?) "?"; rewrite -seq_progress; iMod "Hclose"; iApply "H".
+Qed.
+
+(** Derived lifting lemmas. *)
+Lemma swp_lift_pure_step `{Inhabited (state Λ)} p E1 E2 Φ e1 :
+  (∀ σ1, reducible (e1, σ1)) →
+  (∀ σ1 e2 σ2, step (e1, σ1) (e2, σ2) → σ1 = σ2) →
+  (▷ ∀ e2 σ, ⌜step (e1, σ) (e2, σ)⌝ → SWP e2 @ p; E1,E2 {{ Φ }})
+  ⊢ SWP e1 @ p; E1,E2 {{ Φ }}.
+Proof.
+  iIntros (Hsafe Hstep) "H"; iApply swp_lift_step.
+  { by eapply reducible_not_val, (Hsafe inhabitant). }
+  iIntros (σ1) "?"; iMod (fupd_intro_mask' E1 ∅) as "Hclose"; first set_solver.
+  iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 ?).
+  destruct (Hstep σ1 e2 σ2); first done; subst.
+  by iMod "Hclose"; iModIntro; iFrame; iApply "H".
+Qed.
+
+Lemma swp_lift_pure_stuck `{Inhabited (state Λ)} E1 E2 Φ e :
+  (∀ σ, ¬ progress (e, σ)) →
+  True ⊢ SWP e @ E1,E2 ?{{ Φ }}.
+Proof.
+  iIntros (Hstuck) "". iApply swp_lift_stuck.
+  - destruct(to_val e) as [v|] eqn:He; last done.
+    by exfalso; apply (Hstuck inhabitant); left; exists v.
+  - iIntros (σ) "_"; iMod (fupd_intro_mask' E1 ∅) as "_"; first set_solver.
+    by iModIntro; iPureIntro; apply Hstuck.
+Qed.
+
+Lemma wp_lift_atomic_step {p E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜reducible (e1, σ1)⌝ ∗
+    ▷ ∀ e2 σ2, ⌜step (e1, σ1) (e2, σ2)⌝ ={E}=∗
+      state_interp σ2 ∗ default False (to_val e2) Φ)
+  ⊢ SWP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply swp_lift_step =>//; iIntros (σ1) "Hσ1".
+  iMod ("H" $! _ with "Hσ1") as "[$ H]".
+  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+  iModIntro; iNext; iIntros (e2 σ2) "%"; iMod "Hclose" as "_".
+  iMod ("H" $! _ _ with "[#]") as "($ & HΦ)"; first done.
+  destruct (to_val e2) eqn:?; last by iExFalso.
+  by iApply swp_value.
+Qed.
+
+(* PDS: swp_lift_atomic_det_step went away. *)
+
+Lemma swp_lift_pure_det_step `{Inhabited (state Λ)} p E1 E2 Φ e1 e2 :
+  (∀ σ1, reducible (e1, σ1)) →
+  (∀ σ1 e2' σ2, step (e1, σ1) (e2', σ2) → σ1 = σ2 ∧ e2 = e2') →
+  ▷ SWP e2 @ p; E1,E2 {{ Φ }}
+  ⊢ SWP e1 @ p; E1,E2 {{ Φ }}.
+Proof.
+  iIntros (? Hpuredet) "?"; iApply swp_lift_pure_step; first done.
+  - by intros; eapply Hpuredet.
+  - by iNext; iIntros (e' σ (_&->)%Hpuredet).
+Qed.
+End lifting.

theories/sequential/ownp.v

+From iris.algebra Require Import auth.
+From iris.program_logic Require Import ownp.
+From iris.sequential Require Import slanguage weakestpre lifting adequacy.
+From iris.proofmode Require Import tactics.
+
+(*
+	This is basically a copy of ../program_logic/ownp.v. Perhaps
+	we should refactor, or rethink state interpretations.
+*)
+Notation ownPG Λ Σ := (ownPG' (state Λ) Σ).
+Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
+
+(* Adequacy *)
+Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} p e σ φ :
+  (∀ `{ownPG Λ Σ}, ownP σ ⊢ SWP e @ p; ⊤ {{ v, ⌜φ v⌝ }}) →
+  adequate p (e, σ) φ.
+Proof.
+  intros Hwp; apply (swp_adequacy  Σ _).
+  iIntros (?) ""; iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ)))
+    as (γσ) "[Hσ Hσf]"; first done.
+  iModIntro; iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))); iFrame "Hσ".
+  by iApply (Hwp (OwnPG _ _ _ _ γσ)); rewrite /ownP.
+Qed.
+
+Theorem ownP_invariance Σ `{ownPPreG Λ Σ} p e1 σ1 e2 σ2 φ Φ :
+  (∀ `{ownPG Λ Σ},
+    ownP σ1 ={⊤}=∗ SWP e1 @ p; ⊤ {{ Φ }} ∗ |={∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+  rtc step (e1, σ1) (e2, σ2) →
+  φ σ2.
+Proof.
+  intros Hwp Hsteps; eapply (swp_invariance Σ Λ p e1 σ1 e2 σ2 _ Φ)=> //.
+  iIntros (?); iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
+    as (γσ) "[Hσ Hσf]"; first done.
+  iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))); iFrame "Hσ".
+  iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
+  iIntros "!> Hσ"; iMod "H" as (σ2') "[Hσf %]"; rewrite /ownP.
+  by iDestruct (own_valid_2 with "Hσ Hσf")
+    as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2; auto.
+Qed.
+
+Section lifting.
+Context `{ownPG Λ Σ}.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Implicit Types σ : state Λ.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+
+Lemma ownP_lift_step p E1 E2 Φ e1 :
+  (|={E1,∅}=> ∃ σ1, ⌜reducible (e1, σ1)⌝ ∗ ▷ ownP σ1 ∗
+    ▷ ∀ e2 σ2, ⌜step (e1, σ1) (e2, σ2)⌝ ∗ ownP σ2
+          ={∅,E1}=∗ SWP e2 @ p; E1,E2 {{ Φ }})
+  ⊢ SWP e1 @ p; E1,E2 {{ Φ }}.
+Proof.
+  iIntros "H"; destruct (to_val e1) as [v|] eqn:EQe1.
+  - apply of_to_val in EQe1 as <-. iApply fupd_swp.
+    iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val.
+    move: Hred; by rewrite to_of_val.
+  - iApply swp_lift_step; [done|]; iIntros (σ1) "Hσ".
+    iMod "H" as (σ1') "(% & >Hσf & H)"; rewrite /ownP.
+    iDestruct (own_valid_2 with "Hσ Hσf")
+      as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+    iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 Hstep).
+    iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
+    { by apply auth_update, option_local_update,
+        (exclusive_local_update _ (Excl σ2)). }
+    by iFrame "Hσ"; iApply ("H" $! _ _ with "[$Hσf]").
+Grab Existential Variables.	(* PDS: Huh? *)
+  by exists(coPLeaf true).
+Qed.
+
+Lemma ownP_lift_stuck E1 E2 Φ e :
+  (|={E1,∅}=> ∃ σ, ⌜¬ progress (e, σ)⌝ ∗ ▷ ownP σ)
+  ⊢ SWP e @ E1,E2 ?{{ Φ }}.
+Proof.
+  iIntros "H"; destruct (to_val e) as [v|] eqn:EQe.
+  - apply of_to_val in EQe as <-; iApply fupd_swp.
+    iMod "H" as (σ1) "[#H _]"; iDestruct "H" as %Hstuck; exfalso.
+    by apply Hstuck; left; rewrite to_of_val; exists v.
+  - iApply swp_lift_stuck; [done|]; iIntros (σ1) "Hσ".
+    iMod "H" as (σ1') "(% & >Hσf)"; rewrite /ownP.
+    by iDestruct (own_valid_2 with "Hσ Hσf")
+      as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+Grab Existential Variables.	(* PDS: Huh? *)
+  by exists(coPLeaf true).
+Qed.
+
+Lemma ownP_lift_pure_step `{Inhabited (state Λ)} p E1 E2 Φ e1 :
+  (∀ σ1, reducible (e1, σ1)) →
+  (∀ σ1 e2 σ2, step (e1, σ1) (e2, σ2) → σ1 = σ2) →
+  (▷ ∀ e2 σ, ⌜step (e1, σ) (e2, σ)⌝ → SWP e2 @ p; E1,E2 {{ Φ }})
+  ⊢ SWP e1 @ p; E1,E2 {{ Φ }}.
+Proof.
+  iIntros (Hsafe Hstep) "H"; iApply swp_lift_step.
+  { eapply reducible_not_val, (Hsafe inhabitant). }
+  iIntros (σ1) "Hσ"; iMod (fupd_intro_mask' E1 ∅) as "Hclose"; first set_solver.
+  iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 ?).
+  destruct (Hstep σ1 e2 σ2); first done; subst.
+  by iMod "Hclose"; iModIntro; iFrame "Hσ"; iApply "H".
+Qed.
+
+(** Derived lifting lemmas. *)
+Lemma ownP_lift_atomic_step {p E Φ} e1 σ1 :
+  reducible (e1, σ1) →
+  (▷ ownP σ1 ∗ ▷ ∀ e2 σ2, ⌜step (e1, σ1) (e2, σ2) ⌝ ∗ ownP σ2 -∗
+    default False (to_val e2) Φ)
+  ⊢ SWP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (?) "[? H]"; iApply ownP_lift_step.
+  iMod (fupd_intro_mask' _ ∅) as "Hclose"; first (by set_solver); iModIntro.
+  iExists σ1; iFrame; iSplit; first done; iNext; iIntros (e2 σ2) "[% Hσ]".
+  iSpecialize ("H" $! _ _ with "[Hσ]"); first by iFrame.
+  destruct (to_val e2) eqn:?; last by iExFalso.
+  by iMod "Hclose"; iApply swp_value; auto using to_of_val.
+Qed.
+
+Lemma ownP_lift_atomic_det_step {p E Φ e1} σ1 v2 σ2 :
+  reducible (e1, σ1) →
+  (∀ e2' σ2', step (e1, σ1) (e2', σ2') → σ2 = σ2' ∧ to_val e2' = Some v2) →
+  ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2)
+  ⊢ SWP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (? Hdet) "[Hσ1 Hσ2]"; iApply ownP_lift_atomic_step; first done.
+  iFrame; iNext; iIntros (e2' σ2') "[% Hσ2']".
+  by edestruct Hdet as (->&Hval); first done; rewrite Hval; iApply "Hσ2".
+Qed.
+
+Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {p E1 E2 Φ} e1 e2 :
+  (∀ σ1, reducible (e1, σ1)) →
+  (∀ σ1 e2' σ2, step (e1, σ1) (e2', σ2) → σ1 = σ2 ∧ e2 = e2') →
+  ▷ SWP e2 @ p; E1,E2 {{ Φ }}
+  ⊢ SWP e1 @ p; E1,E2 {{ Φ }}.
+Proof.
+  iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step; first done.
+  - by intros; eapply Hpuredet.
+  - by iNext; iIntros (e' σ (_&->)%Hpuredet).
+Qed.
+End lifting.

theories/sequential/slanguage.v

+From iris.algebra Require Import ofe.
+From iris.program_logic Require language.
+
+Structure slanguage := Slanguage {
+  expr : Type;
+  val : Type;
+  state : Type;
+  of_val : val → expr;
+  to_val : expr → option val;
+  step : relation (expr * state);
+  to_of_val v : to_val (of_val v) = Some v;
+  of_to_val e v : to_val e = Some v → of_val v = e;
+  val_stuck e σ e' σ' : step (e, σ) (e', σ') → to_val e = None
+}.
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
+Bind Scope expr_scope with expr.
+Bind Scope expr_scope with val.
+Arguments of_val {_} _.
+Arguments to_val {_} _.
+Arguments step {_} _ _.
+Arguments to_of_val {_} _.
+Arguments of_to_val {_} _ _ _.
+Arguments val_stuck {_} {_ _ _ _} _.
+
+Canonical Structure stateC Λ := leibnizC (state Λ).
+Canonical Structure valC Λ := leibnizC (val Λ).
+Canonical Structure exprC Λ := leibnizC (expr Λ).
+
+Definition cfg (Λ : slanguage) := (expr Λ * state Λ)%type.
+
+Section slanguage.
+  Context {Λ : slanguage}.
+  Implicit Types v : val Λ.
+
+  Definition reducible (ρ : cfg Λ) := ∃ ρ', step ρ ρ'.
+  Definition progress (ρ : cfg Λ) := is_Some (to_val (ρ.1)) ∨ reducible ρ.
+
+  Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
+  Proof. by intros <-; rewrite to_of_val. Qed.
+  Lemma reducible_not_val e σ : reducible (e, σ) → to_val e = None.
+  Proof. by intros ([? ?]&?); eauto using val_stuck. Qed.
+  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
+  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
+End slanguage.
+
+Class SlanguageCtx (Λ : slanguage) (K : expr Λ → expr Λ) := {
+  fill_not_val e :
+    to_val e = None → to_val (K e) = None;
+  fill_step e1 σ1 e2 σ2 :
+    step (e1, σ1) (e2, σ2) →
+    step (K e1, σ1) (K e2, σ2);
+  fill_step_inv e1' σ1 e2 σ2 :
+    to_val e1' = None → step (K e1', σ1) (e2, σ2) →
+    ∃ e2', e2 = K e2' ∧ step (e1', σ1) (e2', σ2)
+}.
+Arguments fill_step {_ _ _} {_ _ _ _} _.
+Arguments fill_step_inv {_ _ _} {_ _ _ _} _ _.
+
+(** An slanguage is a language that doesn't fork. *)
+Section language.
+  Context {Λ : slanguage}.
+  Implicit Types (e : expr Λ) (σ : state Λ) (efs : list (expr Λ)).
+
+  Inductive seq_step e1 σ1 e2 σ2 efs : Prop :=
+    Seq_step of efs = [] & step (e1, σ1) (e2, σ2).
+
+  Lemma seq_val_stuck e1 σ1 e2 σ2 efs :
+    seq_step e1 σ1 e2 σ2 efs → to_val e1 = None.
+  Proof. by intros [_ ?]; eauto using val_stuck. Qed.
+
+  Canonical Structure seq_lang : language.language := {|
+    language.expr := expr Λ; language.val := val Λ; language.state := state Λ;
+    language.of_val := of_val; language.to_val := to_val;
+    language.prim_step := seq_step;
+    language.to_of_val := to_of_val; language.of_to_val := of_to_val;
+    language.val_stuck := seq_val_stuck
+  |}.
+
+  Lemma seq_reducible e σ : reducible (e, σ) ↔ language.reducible e σ.
+  Proof.
+    split; last by intros (e'&σ'&_&[_ Hstep]); exists (e', σ').
+    by intros ([e' σ']&Hstep); exists e', σ', []; constructor.
+  Qed.
+  Lemma seq_progress e σ : progress (e, σ) ↔ language.progress e σ.
+  Proof. by rewrite /progress seq_reducible. Qed.
+
+  Context `{!SlanguageCtx Λ K}.
+
+  Lemma seq_fill_step e1 σ1 e2 σ2 efs :
+    seq_step e1 σ1 e2 σ2 efs →
+    seq_step (K e1) σ1 (K e2) σ2 efs.
+  Proof. by intros [-> ?]; constructor; eauto using fill_step. Qed.
+
+  Lemma seq_fill_step_inv e1' σ1 e2 σ2 efs :
+    to_val e1' = None → seq_step (K e1') σ1 e2 σ2 efs →
+    ∃ e2', e2 = K e2' ∧ seq_step e1' σ1 e2' σ2 efs.
+  Proof.
+    intros Hnv [-> Hstep]; destruct (fill_step_inv Hnv Hstep) as (e'&?&?).
+    by exists e'; split; last constructor.
+  Qed.
+
+  Global Instance seq_lang_ctx : language.LanguageCtx seq_lang K := {|
+    language.fill_not_val := fill_not_val;
+    language.fill_step := seq_fill_step;
+    language.fill_step_inv := seq_fill_step_inv
+  |}.
+End language.

theories/sequential/weakestpre.v

+From iris.base_logic Require Import base_logic.
+From iris.base_logic.lib Require Import fancy_updates.
+From iris.program_logic Require Import language weakestpre.
+From iris.sequential Require Import slanguage.
+From iris.proofmode Require Import tactics classes.
+
+Notation irisG Λ Σ := (irisG' (state Λ) Σ).
+
+Definition swp_def `{irisG Λ Σ} :
+    bool -c> coPset -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ p E1 E2 e Φ, (
+  |={E1,∅}=> WP e @ p; ∅ {{ v, |={∅,E2}=> Φ v }})%I.
+Definition swp_aux : { x | x = @swp_def }. by eexists. Qed.
+Definition swp := proj1_sig swp_aux.
+Definition swp_eq : @swp = @swp_def := proj2_sig swp_aux.
+
+Arguments swp {_ _ _} _ _ _ _%E _.
+Instance: Params (@swp) 7.
+
+Notation "'SWP' e @ p ; E1 , E2 {{ Φ } }" := (swp p E1 E2 e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'SWP'  e  @  p ;  E1 , E2  {{  Φ  } }") : uPred_scope.
+Notation "'SWP' e @ p ; E {{ Φ } }" := (swp p E E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'SWP'  e  @  p ;  E  {{  Φ  } }") : uPred_scope.
+Notation "'SWP' e @ E1 , E2 {{ Φ } }" := (swp true E1 E2 e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'SWP'  e  @  E1 , E2  {{  Φ  } }") : uPred_scope.
+Notation "'SWP' e @ E {{ Φ } }" := (swp true E E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'SWP'  e  @  E  {{  Φ  } }") : uPred_scope.
+Notation "'SWP' e {{ Φ } }" := (swp true ⊤ ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'SWP'  e  {{  Φ  } }") : uPred_scope.
+Notation "'SWP' e @ E1 , E2 ? {{ Φ } }" := (swp false E1 E2 e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'SWP'  e  @  E1 , E2  ? {{  Φ  } }") : uPred_scope.
+Notation "'SWP' e @ E ? {{ Φ } }" := (swp false E E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'SWP'  e  @  E  ? {{  Φ  } }") : uPred_scope.
+Notation "'SWP' e ? {{ Φ } }" := (swp false ⊤ ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'SWP'  e  ? {{  Φ  } }") : uPred_scope.
+
+Notation "'SWP' e @ p ; E1 , E2 {{ v , Q } }" := (swp p E1 E2 e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'SWP'  e  @  p ;  E1 , E2  {{  v ,  Q  } }") : uPred_scope.
+Notation "'SWP' e @ p ; E {{ v , Q } }" := (swp p E E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'SWP'  e  @  p ;  E  {{  v ,  Q  } }") : uPred_scope.
+Notation "'SWP' e @ E1 , E2 {{ v , Q } }" := (swp true E1 E2 e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'SWP'  e  @  E1 , E2  {{  v ,  Q  } }") : uPred_scope.
+Notation "'SWP' e @ E {{ v , Q } }" := (swp true E E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'SWP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
+Notation "'SWP' e {{ v , Q } }" := (swp true ⊤ ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'SWP'  e  {{  v ,  Q  } }") : uPred_scope.
+Notation "'SWP' e @ E1 , E2 ? {{ v , Q } }" := (swp false E1 E2 e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'SWP'  e  @  E1 , E2  ? {{  v ,  Q  } }") : uPred_scope.
+Notation "'SWP' e @ E ? {{ v , Q } }" := (swp false E E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'SWP'  e  @  E  ? {{  v ,  Q  } }") : uPred_scope.
+Notation "'SWP' e ? {{ v , Q } }" := (swp false ⊤ ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'SWP'  e  ? {{  v ,  Q  } }") : uPred_scope.
+
+Section swp.
+Context `{irisG Λ Σ}.
+Implicit Types P : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+
+(* Weakest pre *)
+Global Instance swp_ne p E1 E2 e n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@swp Λ Σ _ p E1 E2 e).
+Proof.
+  intros Φ Ψ HΦ; rewrite !swp_eq /swp_def.
+  by apply fupd_ne, wp_ne=> v; apply fupd_ne.
+Qed.
+Global Instance swp_proper p E1 E2 e :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@swp Λ Σ _ p E1 E2 e).
+Proof.
+  by intros Φ Φ' ?; apply equiv_dist=>n; apply swp_ne=>v; apply equiv_dist.
+Qed.
+
+Lemma swp_value' p E Φ v : Φ v ⊢ SWP of_val v @ p; E {{ Φ }}.
+Proof.
+  iIntros "HΦ"; rewrite swp_eq /swp_def.
+  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+  by iModIntro; iApply wp_value'; iFrame.
+Qed.
+Lemma swp_value_inv p E1 E2 Φ v : SWP of_val v @ p; E1,E2 {{ Φ }} ={E1,E2}=∗ Φ v.
+Proof.
+  rewrite swp_eq /swp_def wp_value_inv.
+  by iIntros ">>>$"; iModIntro.
+Qed.
+
+Lemma swp_strong_mono p E1 E2 E3 e Φ Ψ :
+  (∀ v, Φ v ={E2,E3}=∗ Ψ v) ∗ SWP e @ p; E1,E2 {{ Φ }} ⊢ SWP e @ p; E1,E3 {{ Ψ }}.
+Proof.
+  rewrite swp_eq /swp_def; iIntros "[HΦ >H]"; iModIntro.
+  iApply (wp_strong_mono p ∅); first done; iSplitR "H"; last done.
+  by iIntros (?) "Hv"; iModIntro; iMod ("HΦ" $! _ with "Hv").
+Qed.
+
+Lemma swp_mask_mono p E1 E2 E3 e Φ :
+  E1 ⊆ E2 → SWP e @ p; E1,E3 {{ Φ }} ⊢ SWP e @ p; E2,E3 {{ Φ }}.
+Proof.
+  rewrite swp_eq /swp_def; iIntros (?) "?".
+  by iMod (fupd_intro_mask' _ E1).
+Qed.
+
+Lemma swp_forget_progress E1 E2 e Φ :
+  SWP e @ E1,E2 {{ Φ }} ⊢ SWP e @ E1,E2 ?{{ Φ }}.
+Proof.
+  by rewrite swp_eq /swp_def wp_forget_progress.
+Qed.
+
+Lemma fupd_swp p E1 E2 E3 e Φ :
+  (|={E1,E2}=> SWP e @ p; E2,E3 {{ Φ }}) ⊢ SWP e @ p; E1,E3 {{ Φ }}.
+Proof.
+  by rewrite swp_eq /swp_def; iIntros ">>?"; iModIntro.
+Qed.
+
+Lemma swp_fupd_step p E1 E2 E3 e P Φ :
+  to_val e = None →
+  ▷ P -∗ SWP e @ p; E1,E2 {{ v, P ={E2,E3}=∗ Φ v }} -∗ SWP e @ p; E1,E3 {{ Φ }}.
+Proof.
+  rewrite swp_eq /swp_def; iIntros (?) "HR >H"; iModIntro.
+  iRevert "HR H"; rewrite (step_fupd_intro ∅ ∅ P); last done.
+  rewrite wp_mono; first by iApply wp_fupd_step.
+  by iIntros (?) "H Hp"; iModIntro; iMod "H"; iApply ("H" with "Hp").
+Qed.
+
+Lemma swp_bind K `{!SlanguageCtx Λ K} p E1 E2 E3 e Φ :
+  SWP e @ p; E1,E2 {{ v, SWP K (of_val v) @ p; E2,E3 {{ Φ }} }} ⊢ SWP K e @ p; E1,E3 {{ Φ }}.
+Proof.
+  rewrite swp_eq /swp_def; iIntros ">H"; iModIntro.
+  iApply wp_bind; iApply wp_mono; last by iApply "H".
+  by iIntros (?) "?"; rewrite fupd_trans; iApply fupd_wp.
+Qed.
+
+(** * Derived rules *)
+Lemma swp_fupd p E1 E2 E3 e Φ :
+  SWP e @ p; E1,E2 {{ v, |={E2,E3}=> Φ v }} ⊢ SWP e @ p; E1,E3 {{ Φ }}.
+Proof.
+  by iIntros "?"; iApply swp_strong_mono; iFrame; auto.
+Qed.
+Lemma swp_atomic p E1 E2 E3 E4 e Φ :	(* cf. wp_atomic *)
+  (|={E1,E2}=> SWP e @ p; E2,E3 {{ v, |={E3,E4}=> Φ v }}) ⊢ SWP e @ p; E1,E4 {{ Φ }}.
+Proof. by rewrite fupd_swp swp_fupd. Qed.
+
+Lemma swp_mono p E1 E2 e Φ Ψ :
+  (∀ v, Φ v ⊢ Ψ v) → SWP e @ p; E1,E2 {{ Φ }} ⊢ SWP e @ p; E1,E2 {{ Ψ }}.
+Proof.
+  iIntros (HΦ) "H"; iApply swp_strong_mono; iSplitR "H"; last iExact "H".
+  by iIntros (v) "?"; iApply HΦ.
+Qed.
+Global Instance swp_mono' p E1 E2 e :
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@swp Λ Σ _ p E1 E2 e).
+Proof. by intros Φ Φ' ?; apply swp_mono. Qed.
+
+Lemma swp_value p E Φ e v : to_val e = Some v → Φ v ⊢ SWP e @ p; E {{ Φ }}.
+Proof. by intros; rewrite -(of_to_val e v); first apply swp_value'. Qed.
+Lemma swp_value_fupd' p E Φ v : (|={E}=> Φ v) ⊢ SWP of_val v @ p; E {{ Φ }}.
+Proof. by rewrite -swp_fupd; rewrite <- swp_value'. Qed.
+Lemma swp_value_fupd p E Φ e v :
+  to_val e = Some v → (|={E}=> Φ v) ⊢ SWP e @ p; E {{ Φ }}.
+Proof. by intros; rewrite -swp_fupd; rewrite <- swp_value. Qed.
+
+Lemma swp_frame_l p E1 E2 e Φ R : R ∗ SWP e @ p; E1,E2 {{ Φ }} ⊢ SWP e @ p; E1,E2 {{ v, R ∗ Φ v }}.
+Proof. by iIntros "[??]"; iApply (swp_strong_mono p E1 E2 _ _ Φ); try iFrame; eauto. Qed.
+Lemma swp_frame_r p E1 E2 e Φ R : SWP e @ p; E1,E2 {{ Φ }} ∗ R ⊢ SWP e @ p; E1,E2 {{ v, Φ v ∗ R }}.
+Proof. by iIntros "[??]"; iApply (swp_strong_mono p E1 E2 _ _ Φ); try iFrame; eauto. Qed.
+
+Lemma swp_frame_step_l p E1 E2 e Φ R :
+  to_val e = None →
+  ▷ R ∗ SWP e @ p; E1,E2 {{ Φ }} ⊢ SWP e @ p; E1,E2 {{ v, R ∗ Φ v }}.
+Proof.
+  iIntros (?) "[Hu Hwp]"; iApply (swp_fupd_step with "Hu"); first done.
+  by iApply (swp_mono with "Hwp"); iIntros (?) "$$".
+Qed.
+Lemma swp_frame_step_r p E1 E2 e Φ R :
+  to_val e = None →
+  SWP e @ p; E1,E2 {{ Φ }} ∗ ▷ R ⊢ SWP e @ p; E1,E2 {{ v, Φ v ∗ R }}.
+Proof.
+  rewrite [(SWP _ @ _; _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R).
+  by apply swp_frame_step_l.
+Qed.
+
+Lemma swp_wand p E1 E2 e Φ Ψ :
+  SWP e @ p; E1,E2 {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ SWP e @ p; E1,E2 {{ Ψ }}.
+Proof.
+  iIntros "? H"; iApply (swp_strong_mono p E1 E2).
+  by iFrame; iIntros (?) "?"; iApply "H".
+Qed.
+Lemma swp_wand_l p E1 E2 e Φ Ψ :
+  (∀ v, Φ v -∗ Ψ v) ∗ SWP e @ p; E1,E2 {{ Φ }} ⊢ SWP e @ p; E1,E2 {{ Ψ }}.
+Proof. by iIntros "[H Hwp]"; iApply (swp_wand with "Hwp H"). Qed.
+Lemma swp_wand_r p E1 E2 e Φ Ψ :
+  SWP e @ p; E1,E2 {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ SWP e @ p; E1,E2 {{ Ψ }}.
+Proof. by iIntros "[Hwp H]"; iApply (swp_wand with "Hwp H"). Qed.
+End swp.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{irisG Λ Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : val Λ → iProp Σ.
+
+  Global Instance frame_swp p E1 E2 e R Φ Ψ :
+    (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (SWP e @ p; E1,E2 {{ Φ }}) (SWP e @ p; E1,E2 {{ Ψ }}).
+  Proof. by rewrite /Frame=> HR; rewrite swp_frame_l; apply swp_mono, HR. Qed.
+
+  Global Instance is_except_0_swp p E1 E2 e Φ : IsExcept0 (SWP e @ p; E1,E2 {{ Φ }}).
+  Proof. by rewrite /IsExcept0 -{2}fupd_swp -except_0_fupd; rewrite <- fupd_intro. Qed.
+
+  Global Instance elim_modal_bupd_swp p E1 E2 e P Φ :
+    ElimModal (|==> P) P (SWP e @ p; E1,E2 {{ Φ }}) (SWP e @ p; E1,E2 {{ Φ }}).
+  Proof. by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r uPred.wand_elim_r fupd_swp. Qed.
+
+  Global Instance elim_modal_fupd_swp p E1 E2 E3 e P Φ :
+    ElimModal (|={E1,E2}=> P) P (SWP e @ p; E1,E3 {{ Φ }}) (SWP e @ p; E2,E3 {{ Φ }}).
+  Proof. by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_swp. Qed.
+End proofmode_classes.
+
+Hint Extern 0 (atomic _) => assumption : typeclass_instances.
+
+(* We can trivially frame (|={E1,E2}▷=> R) around steps. *)
+Section note.
+Context `{irisG Λ Σ}.
+Implicit Types P : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+
+Lemma swp_fupd_step' p E1 E2 e P Φ :
+  to_val e = None → E2 ⊆ E1 →
+  (|={E1,E2}▷=> P) -∗ SWP e @ p; E2 {{ v, P ={E1}=∗ Φ v }} -∗ SWP e @ p; E1 {{ Φ }}.
+Proof.
+  iIntros (??) ">HR Hwp"; iApply (swp_fupd_step with "HR"); first done.
+  by iApply (swp_mono with "Hwp"); iIntros (?) "H >HR"; iApply ("H" with "HR").
+Qed.
+Lemma swp_frame_step_l' p E1 E2 e Φ R :
+  to_val e = None → E2 ⊆ E1 →
+  (|={E1,E2}▷=> R) ∗ SWP e @ p; E2 {{ Φ }} ⊢ SWP e @ p; E1 {{ v, R ∗ Φ v }}.
+Proof.
+  iIntros (??) "[>HR Hwp]". iApply (swp_fupd_step with "HR"); first done.
+  by iApply (swp_mono with "Hwp"); iIntros (?) "Hv >HR"; iFrame.
+Qed.
+Lemma swp_frame_step_r' p E1 E2 e Φ R :
+  to_val e = None → E2 ⊆ E1 →
+  SWP e @ p; E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ SWP e @ p; E1 {{ v, Φ v ∗ R }}.
+Proof.
+  rewrite [(SWP _ @ _; _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R).
+  by apply swp_frame_step_l'.
+Qed.
+End note.