Merge elementary-infinite into main

theories/eris/adequacy.v

@@ -195,11 +195,12 @@ Section adequacy.
       by iApply "IH".
   Qed.
 
-  Theorem wp_refRcoupl_step_fupdN (ε : nonnegreal) (e : expr) (σ : state) n φ :
-    state_interp σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
+  Theorem wp_refRcoupl_step_fupdN k (ε : nonnegreal) (e : expr) (σ : state) n φ :
+    (k + n < max_step)%nat →
+    state_interp k σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
     |={⊤,∅}=> |={∅}▷=>^n ⌜pgl (exec n (e, σ)) φ ε⌝.
   Proof.
-    iInduction n as [|n] "IH" forall (e σ ε); iIntros "((Hσh & Hσt) & Hε & Hwp)".
+    iInduction n as [|n] "IH" forall (k e σ ε); iIntros (Hlt) "(Hσ & Hε & Hwp)".
     - rewrite /exec /=.
       destruct (to_val e) eqn:Heq.
       + apply of_to_val in Heq as <-.
@@ -226,7 +227,9 @@ Section adequacy.
         apply (pgl_mon_grading _ _ 0); [apply cond_nonneg | ].
         apply pgl_dret; auto.
       + rewrite pgl_wp_unfold /pgl_wp_pre /= Heq.
-        iMod ("Hwp" with "[$]") as "Hlift".
+        iMod ("Hwp" $! k with "[$]") as "Hlift".
+        iDestruct "Hlift" as "[%|Hlift]".
+        { exfalso. simpl in Hlt. lia. }
         iModIntro.
         iPoseProof
           (glm_mono _ (λ '(e2, σ2) ε', |={∅}▷=>^(S n)
@@ -235,7 +238,8 @@ Section adequacy.
         { apply Rle_refl. }
         { iIntros ([] ?) "H !> !>".
           iMod "H" as "(Hstate & Herr_auth & Hwp)".
-          iMod ("IH" with "[$]") as "H".
+          iMod ("IH" $! (S k) with "[] [$]") as "H".
+          { iPureIntro. simpl in Hlt. lia.  }
           iModIntro. done. }
         assert ((prim_step e σ) = (step (e, σ))) as h => //.
         rewrite h. clear h.
@@ -448,11 +452,12 @@ Section adequacy.
       by iApply "IH".
   Qed.
 
-  Theorem wp_safety_fupdN (ε : nonnegreal) (e : expr) (σ : state) n φ  :
-    state_interp σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
+  Theorem wp_safety_fupdN k (ε : nonnegreal) (e : expr) (σ : state) n φ  :
+    (k + n < max_step)%nat →
+    state_interp k σ ∗ err_interp (ε) ∗ WP e {{ v, ⌜φ v⌝ }} ⊢
     |={⊤,∅}=> |={∅}▷=>^n ⌜SeriesC (pexec n (e, σ)) >= 1 - ε⌝.
   Proof.
-    iInduction n as [|n] "IH" forall (e σ ε); iIntros "((Hσh & Hσt) & Hε & Hwp)".
+    iInduction n as [|n] "IH" forall (k e σ ε); iIntros (Hlt) "(Hσ & Hε & Hwp)".
     - rewrite /=.
       iApply fupd_mask_intro; [set_solver|]; iIntros.
       iPureIntro.
@@ -487,7 +492,8 @@ Section adequacy.
                    etrans; last eapply (SeriesC_singleton' (of_val v, σ)).
                    apply SeriesC_ext.
                    intros. case_bool_decide; subst; simpl.
-                   --- rewrite IHn. rewrite step_or_final_is_final; first rewrite dret_1_1; [lra|done|].
+                   --- rewrite IHn; last by lia.
+                       rewrite step_or_final_is_final; first rewrite dret_1_1; [lra|done|].
                        rewrite /is_final. simpl. done.
                    --- simpl. rewrite step_or_final_is_final; last by rewrite /is_final.
                        rewrite dret_0; last done. lra.
@@ -503,13 +509,15 @@ Section adequacy.
              ++ intros. simpl. rewrite /dbind/dbind_pmf{1}/pmf/=.
                 apply SeriesC_0.
                 intros. destruct (decide (x = (of_val v, σ))).
-                ** subst. rewrite IHn; try done. lra.
+                ** subst. rewrite IHn; try done; try lia. lra.
                 ** rewrite step_or_final_is_final; last by rewrite /is_final.
                    rewrite dret_0; last done.
                    lra.
         * rewrite SeriesC_singleton. lra.
       + rewrite pgl_wp_unfold /pgl_wp_pre /= Heq.
-        iMod ("Hwp" with "[$]") as "Hlift".
+        iMod ("Hwp" $! k with "[$]") as "Hlift".
+        iDestruct "Hlift" as "[%Hlt'|Hlift]".
+        { exfalso. simpl in Hlt. lia. }
         iModIntro.
         iPoseProof
           (glm_mono _ (λ '(e2, σ2) ε', |={∅}▷=>^(S n)
@@ -518,7 +526,8 @@ Section adequacy.
         { apply Rle_refl. }
         { iIntros ([] ?) "H !> !>".
           iMod "H" as "(Hstate & Herr_auth & Hwp)".
-          iMod ("IH" with "[$]") as "H".
+          iMod ("IH" $! (S k)%nat with "[] [$]") as "H".
+          { iPureIntro. simpl in Hlt; lia. }
           iModIntro. done. }
         by iApply (glm_erasure_safety with "H").
   Qed.
@@ -530,12 +539,14 @@ Class erisGpreS Σ := ErisGpreS {
   erisGpreS_iris  :: invGpreS Σ;
   erisGpreS_heap  :: ghost_mapG Σ loc val;
   erisGpreS_tapes :: ghost_mapG Σ loc tape;
+  erisGpreS_steps :: mono_natG Σ;
   erisGpreS_err   :: ecGpreS Σ;
 }.
 
 Definition erisΣ : gFunctors :=
   #[invΣ; ghost_mapΣ loc val;
     ghost_mapΣ loc tape;
+    mono_natΣ;
     GFunctor (authR nonnegrealUR)].
 Global Instance subG_erisGPreS {Σ} : subG erisΣ Σ → erisGpreS Σ.
 Proof. solve_inG. Qed.
@@ -562,8 +573,10 @@ Proof.
     eapply Rle_trans; [eapply prob_le_1|done]. }
   set ε' := mknonnegreal _ Hε.
   iMod (ec_alloc ε') as (?) "[? ?]"; [done|].
-  set (HclutchGS := HeapG Σ _ _ _ γH γT _).
-  iApply (wp_refRcoupl_step_fupdN ε').
+  iMod (mono_nat_own_alloc O) as (γS) "[? ?]".
+  set (HclutchGS := HeapG Σ _ _ _ _ γH γT γS _ (S n)).
+  iApply (wp_refRcoupl_step_fupdN 0 ε' _ _ n).
+  { simpl. lia. }
   iFrame.
   iApply Hwp.
   done.
@@ -627,8 +640,11 @@ Proof.
     - simpl. lra. }
   set ε' := mknonnegreal _ Hε.
   iMod (ec_alloc ε') as (?) "[? ?]"; [done|].
-  set (HclutchGS := HeapG Σ _ _ _ γH γT _).
-  iApply (wp_safety_fupdN ε'). iFrame.
+  iMod (mono_nat_own_alloc O) as (γS) "[? ?]".
+  set (HclutchGS := HeapG Σ _ _ _ _ γH γT γS _ (S n)).
+  iApply (wp_safety_fupdN 0 ε').
+  { simpl. lia. }
+  iFrame.
   iApply Hwp. done.
 Qed.
 

theories/eris/ectx_lifting.v

@@ -17,28 +17,47 @@ Local Hint Resolve head_stuck_stuck : core.
 
 Lemma wp_lift_head_step_fupd_couple {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1 ε1,
-    state_interp σ1 ∗ err_interp ε1
+  (∀ n σ1 ε1,
+    state_interp n σ1 ∗ err_interp ε1
     ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     glm e1 σ1 ε1 (λ '(e2, σ2) ε2,
-      ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E {{ Φ }}))
+      ▷ |={∅,E}=> state_interp (S n) σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E {{ Φ }}))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_step_fupd_glm; [done|].
-  iIntros (σ1 ε) "Hσε".
+  iIntros (n σ1 ε) "Hσε".
   iMod ("H" with "Hσε") as "[% H]"; iModIntro; auto.
 Qed.
 
 Lemma wp_lift_head_step {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E,∅}=∗
+  (∀ n σ1, state_interp n σ1 ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ s; E {{ Φ }})
+      state_interp (S n) σ2 ∗ WP e2 @ s; E {{ Φ }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (??) "Hσ".
+  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
+  iSplit.
+  { iPureIntro. by eapply head_prim_reducible. }
+  iIntros (???) "!> !>". iApply "H"; auto.
+Qed.
+
+Lemma wp_lift_head_step' {E Φ} e1 s :
+  to_val e1 = None →
+  (∀ n σ1, state_interp (S n) σ1 ={E,∅}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗
+      state_interp (S n) σ2 ∗ WP e2 @ s; E {{ Φ }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (??) "Hσ".
+  iMod (fupd_mask_subseteq ∅) as "Hclose".
+  { set_solver+. }
+  iMod (state_interp_mono with "Hσ") as "Hσ".
+  iMod "Hclose".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by eapply head_prim_reducible. }
@@ -47,15 +66,15 @@ Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {E1 E2 Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E1}=∗
+  (∀ n σ1, state_interp n σ1 ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E1}[E2]▷=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
-  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (n σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by apply head_prim_reducible. }
   iIntros (e2 σ2 Hstep).
@@ -64,15 +83,37 @@ Qed.
 
 Lemma wp_lift_atomic_head_step {E Φ} e1 s :
   to_val e1 = None →
-  (∀ σ1, state_interp σ1 ={E}=∗
+  (∀ n σ1, state_interp n σ1 ={E}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗
+      state_interp (S n) σ2 ∗
+      from_option Φ False (to_val e2))
+  ⊢ WP e1 @ s; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
+  iIntros (n σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iSplit.
+  { iPureIntro. by apply head_prim_reducible. }
+  iNext. iIntros (e2 σ2 Hstep).
+  iApply "H"; eauto.
+Qed.
+
+Lemma wp_lift_atomic_head_step' {E Φ} e1 s :
+  to_val e1 = None →
+  (∀ n σ1, state_interp (S n) σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗
-      state_interp σ2 ∗
+      state_interp (S n) σ2 ∗
       from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
-  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iIntros (n σ1) "Hσ1".
+  iMod (fupd_mask_subseteq ∅) as "Hclose".
+  { set_solver+. }
+  iMod (state_interp_mono with "Hσ1") as "Hσ1".
+  iMod "Hclose".
+  iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
   iSplit.
   { iPureIntro. by apply head_prim_reducible. }
   iNext. iIntros (e2 σ2 Hstep).