WIP.

theories/program_logic/weakestpre.v

 From iris.proofmode Require Import base tactics classes.
 From iris.base_logic.lib Require Export fancy_updates.
-From iris.program_logic Require Export language.
+From iris.program_logic Require Export language ectx_language.
 (* FIXME: If we import iris.bi.weakestpre earlier texan triples do not
    get pretty-printed correctly. *)
 From iris.bi Require Export weakestpre.
 Set Default Proof Using "Type".
 Import uPred.
 
-Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
+Class irisG (Λ : ectxLanguage) (Σ : gFunctors) := IrisG {
   iris_invG :> invG Σ;
 
   (** The state interpretation is an invariant that should hold in between each
@@ -15,7 +15,7 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
   the remaining observations, and [nat] is the number of forked-off threads
   (not the total number of threads, which is one higher because there is always
   a main thread). *)
-  state_interp : state Λ → list (observation Λ) → nat → iProp Σ;
+  state_interp : state Λ → list (observation Λ) → list (expr Λ) → iProp Σ;
 
   (** A fixed postcondition for any forked-off thread. For most languages, e.g.
   heap_lang, this will simply be [True]. However, it is useful if one wants to
@@ -24,30 +24,31 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
 }.
 Global Opaque iris_invG.
 
-Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
+Definition wp_pre `{!irisG Λ Σ} (s : stuckness) (i : nat)
     (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
     coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
-  | None => ∀ σ1 κ κs n,
-     state_interp σ1 (κ ++ κs) n ={E,∅}=∗
+  | None => ∀ σ1 κ κs es K,
+     ⌜ es !! i = Some (fill K e1) ⌝ -∗
+     state_interp σ1 (κ ++ κs) es ={E,∅}=∗
        ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
        ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
-         state_interp σ2 κs (length efs + n) ∗
+         state_interp σ2 κs (<[i:=fill K e2]> es ++ efs) ∗
          wp E e2 Φ ∗
          [∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
   end%I.
 
-Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
+Local Instance wp_pre_contractive `{!irisG Λ Σ} s i : Contractive (wp_pre s i).
 Proof.
   rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
-  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
+Definition wp_def `{!irisG Λ Σ} (si : stuckness * nat) :
+  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre si.1 si.2).
 Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
-Instance wp' `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
+Instance wp' `{!irisG Λ Σ} : Wp Λ (iProp Σ) (stuckness * nat) := wp_aux.(unseal).
 Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
 
 Section wp.
@@ -59,49 +60,49 @@ Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
 (* Weakest pre *)
-Lemma wp_unfold s E e Φ :
-  WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp (PROP:=iProp Σ)  s) E e Φ.
-Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
+Lemma wp_unfold s i E e Φ :
+  WP e @ (s,i); E {{ Φ }} ⊣⊢ wp_pre s i (wp (PROP:=iProp Σ)  (s,i)) E e Φ.
+Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s i)). Qed.
 
-Global Instance wp_ne s E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
+Global Instance wp_ne s i E e n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (wp (PROP:=iProp Σ) (s,i) E e).
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
   rewrite !wp_unfold /wp_pre.
   (* FIXME: figure out a way to properly automate this proof *)
   (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
   is very slow here *)
-  do 24 (f_contractive || f_equiv). apply IH; first lia.
+  do 27 (f_contractive || f_equiv). apply IH; first lia.
   intros v. eapply dist_le; eauto with lia.
 Qed.
-Global Instance wp_proper s E e :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) s E e).
+Global Instance wp_proper s i E e :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) (s,i) E e).
 Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
-Global Instance wp_contractive s E e n :
+Global Instance wp_contractive s i E e n :
   TCEq (to_val e) None →
-  Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) s E e).
+  Proper (pointwise_relation _ (dist_later n) ==> dist n) (wp (PROP:=iProp Σ) (s,i) E e).
 Proof.
   intros He Φ Ψ HΦ. rewrite !wp_unfold /wp_pre He.
   by repeat (f_contractive || f_equiv).
 Qed.
 
-Lemma wp_value' s E Φ v : Φ v ⊢ WP of_val v @ s; E {{ Φ }}.
+Lemma wp_value' s i E Φ v : Φ v ⊢ WP of_val v @ (s,i); E {{ Φ }}.
 Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
-Lemma wp_value_inv' s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}=∗ Φ v.
+Lemma wp_value_inv' s i E Φ v : WP of_val v @ (s,i); E {{ Φ }} ={E}=∗ Φ v.
 Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
 
-Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
+Lemma wp_strong_mono s1 s2 i E1 E2 e Φ Ψ :
   s1 ⊑ s2 → E1 ⊆ E2 →
-  WP e @ s1; E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 {{ Ψ }}.
+  WP e @ (s1,i); E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ (s2,i); E2 {{ Ψ }}.
 Proof.
   iIntros (? HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
   rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
-  iMod ("H" with "[$]") as "[% H]".
+  iIntros (σ1 κ κs es K ?) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
+  iMod ("H" with "[//] [$]") as "[% H]".
   iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!> !>".
   iMod "H" as "(Hσ & H & Hefs)".
@@ -111,78 +112,86 @@ Proof.
     iIntros "H". iApply ("IH" with "[] H"); auto.
 Qed.
 
-Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}.
+Lemma fupd_wp s i E e Φ : (|={E}=> WP e @ (s,i); E {{ Φ }}) ⊢ WP e @ (s,i); E {{ Φ }}.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
-  iIntros (σ1 κ κs n) "Hσ1". iMod "H". by iApply "H".
+  iIntros (σ1 κ κs es K ?) "Hσ1". iMod "H". by iApply "H".
 Qed.
-Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
-Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
+Lemma wp_fupd s i E e Φ : WP e @ (s,i); E {{ v, |={E}=> Φ v }} ⊢ WP e @ (s,i); E {{ Φ }}.
+Proof. iIntros "H". iApply (wp_strong_mono s s i E with "H"); auto. Qed.
 
-Lemma wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
-  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
+Lemma wp_atomic s i E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
+  (|={E1,E2}=> WP e @ (s,i); E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ (s,i); E1 {{ Φ }}.
 Proof.
   iIntros "H". rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
-  iIntros (σ1 κ κs n) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iIntros (σ1 κ κs es K ?) "Hσ". iMod "H".
+  iMod ("H" $! σ1 with "[//] Hσ") as "[$ H]".
   iModIntro. iIntros (e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!>!>".
   iMod "H" as "(Hσ & H & Hefs)". destruct s.
   - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
-    + iMod ("H" $! _ [] with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
+    + iMod ("H" $! _ [] with "[%] [$]") as "[H _]".
+      { apply lookup_app_l_Some.
+        rewrite list_lookup_insert //; eauto using lookup_lt_Some. }
+      iDestruct "H" as %(? & ? & ? & ? & ?).
       by edestruct (atomic _ _ _ _ _ Hstep).
   - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
     iMod (wp_value_inv' with "H") as ">H".
     iModIntro. iFrame "Hσ Hefs". by iApply wp_value'.
 Qed.
 
-Lemma wp_step_fupd s E1 E2 e P Φ :
+Lemma wp_step_fupd s i E1 E2 e P Φ :
   to_val e = None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
+  (|={E1,E2}▷=> P) -∗ WP e @ (s,i); E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ (s,i); E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
-  iIntros (σ1 κ κs n) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
+  iIntros (σ1 κ κs es K ?) "Hσ". iMod "HR". iMod ("H" with "[//] [$]") as "[$ H]".
   iIntros "!>" (e2 σ2 efs Hstep). iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
   iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
   iMod "HR". iModIntro. iFrame "Hσ Hefs".
-  iApply (wp_strong_mono s s E2 with "H"); [done..|].
+  iApply (wp_strong_mono s s i E2 with "H"); [done..|].
   iIntros (v) "H". by iApply "H".
 Qed.
 
-Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
-  WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} ⊢ WP K e @ s; E {{ Φ }}.
+Lemma wp_bind (K : ectx Λ) s i E e Φ :
+  WP e @ (s,i); E {{ v, WP fill K (of_val v) @ (s,i); E {{ Φ }} }}
+  ⊢ WP fill K e @ (s,i); E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
   rewrite wp_unfold /wp_pre fill_not_val //.
-  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
-  { iPureIntro. destruct s; last done.
-    unfold reducible in *. naive_solver eauto using fill_step. }
+  iIntros (σ1 κ κs es K'). rewrite fill_comp.
+  iIntros (?) "Hσ". iMod ("H" with "[//] [$]") as "[% H]".
+  iModIntro; iSplit.
+  { iPureIntro. destruct s; eauto using fill_reducible. }
   iIntros (e2 σ2 efs Hstep).
-  destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
+  destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); [done..|].
   iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
   iMod "H" as "(Hσ & H & Hefs)".
-  iModIntro. iFrame "Hσ Hefs". by iApply "IH".
+  iModIntro. rewrite fill_comp. iFrame "Hσ Hefs". by iApply "IH".
 Qed.
 
-Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
-  WP K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
+(* NO LONGER HOLDS
+Lemma wp_bind_inv (K : ectx Λ) s i E e Φ :
+  WP fill K e @ (s,i); E {{ Φ }} ⊢
+  WP e @ (s,i); E {{ v, WP fill K (of_val v) @ (s,i); E {{ Φ }} }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
   rewrite fill_not_val //.
-  iIntros (σ1 κ κs n) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
+  iIntros (σ1 κ κs es K' ?) "Hσ". iMod ("H" with "[] [$]") as "[% H]". iModIntro; iSplit.
   { destruct s; eauto using reducible_fill. }
   iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
   iIntros "!>!>". iMod "H" as "(Hσ & H & Hefs)".
   iModIntro. iFrame "Hσ Hefs". by iApply "IH".
-Qed.
+Qed. *)
 
 (** * Derived rules *)
 Lemma wp_mono s E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.