CHANGELOG.md

@@ -63,7 +63,8 @@ lemma.
   and `HasNoLc`, that allow opting for either later credits or `BiFUpdPlainly`.
   The soundness lemmas for the fancy update modality are available in two versions,
   with later credits (suffix `_lc`) and without later credits (suffix `_no_lc`).
-  The lemma `step_fupdN_soundness_gen` is generic over this choice.
+  The lemmas without later credits still generate credits, but they cannot be used
+  in any meaningful way. The lemma `step_fupdN_soundness_gen` is generic over this choice.
 
 **Changes in `program_logic`:**
 

docs/heap_lang.md

@@ -104,6 +104,11 @@ Further tactics:
 - `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically
   applying `wp_bind` as needed.  See the [ProofMode docs](./proof_mode.md) for an
   explanation of `pm_trm`.
+- `wp_smart_apply pm_trm`: like `wp_apply`, but also performs pure reduction
+  steps to reveal a redex that matches `pm_trm`. Precisely, if applying the
+  lemma fails, `wp_smart_apply` will perform a step of pure reduction (via
+  `wp_pure`), and repeat. (This means that `wp_smart_apply` is not the same
+  as `wp_pures; wp_apply`.)
 
 There is no tactic for `Fork`, just do `wp_apply wp_fork`.
 

iris/base_logic/lib/fancy_updates.v

@@ -112,40 +112,44 @@ Proof.
     by iFrame.
 Qed.
 
-Lemma fupd_plain_soundness_no_lc `{!invGpreS Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
-  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
+(** Note: the [_no_lc] soundness lemmas also allow generating later credits, but
+  these cannot be used for anything. They are merely provided to enable making
+  the adequacy proof generic in whether later credits are used. *)
+Lemma fupd_plain_soundness_no_lc `{!invGpreS Σ} E1 E2 (P: iProp Σ) `{!Plain P} m :
+  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, £ m ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hw) "[Hw HE]".
   (* We don't actually want any credits, but we need the [lcGS]. *)
-  iMod (later_credits.le_upd.lc_alloc 0) as (Hc) "[_ _]".
+  iMod (later_credits.le_upd.lc_alloc m) as (Hc) "[_ Hc]".
   set (Hi := InvG _ Hw Hc false).
-  iAssert (|={⊤,E2}=> P)%I as "H".
-  { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd. by constructor. }
+  iAssert (|={⊤,E2}=> P)%I with "[Hc]" as "H" .
+  { iMod (fupd_mask_subseteq E1) as "_"; first done. iApply Hfupd; last done. by constructor. }
   rewrite uPred_fupd_unseal /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
 
-Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} φ n :
-  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
+Lemma step_fupdN_soundness_no_lc `{!invGpreS Σ} φ n m :
+  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤,∅}=> |={∅}▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter.
   apply (soundness (M:=iResUR Σ) _  (S n)); simpl.
-  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _)=> Hinv hc.
+  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ m)=> Hinv hc. iIntros "Hc".
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
-  iApply fupd_plainly_mask_empty. iMod "H".
-  iMod (step_fupdN_plain with "H") as "H". iModIntro.
+  iApply fupd_plainly_mask_empty. iSpecialize ("H" with "Hc").
+  iMod (step_fupdN_plain with "H") as "H". iMod "H". iModIntro.
   rewrite -later_plainly -laterN_plainly -later_laterN laterN_later.
   iNext. iMod "H" as %Hφ. auto.
 Qed.
 
-Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} φ n :
-  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
+Lemma step_fupdN_soundness_no_lc' `{!invGpreS Σ} φ n m :
+  (∀ `{Hinv: !invGS Σ} `{!HasNoLc Σ}, £ m ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
-  iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n)=>Hinv Hc. destruct n as [|n].
+  iIntros (Hiter). eapply (step_fupdN_soundness_no_lc _ n m)=>Hinv Hc.
+  iIntros "Hcred". destruct n as [|n].
   { by iApply fupd_mask_intro_discard; [|iApply (Hiter Hinv)]. }
-   simpl in Hiter |- *. iMod Hiter as "H". iIntros "!>!>!>".
+   simpl in Hiter |- *. iMod (Hiter with "Hcred") as "H". iIntros "!>!>!>".
   iMod "H". clear. iInduction n as [|n] "IH"; [by iApply fupd_mask_intro_discard|].
   simpl. iMod "H". iIntros "!>!>!>". iMod "H". by iApply "IH".
 Qed.
@@ -228,7 +232,7 @@ Qed.
 Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (φ : Prop)
     (use_credits : bool) (n m : nat) :
   (∀ `{Hinv : invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
-    (if use_credits then £ m else True) ={⊤,∅}=∗ |={∅}▷=>^n ⌜φ⌝) →
+    £ m ={⊤,∅}=∗ |={∅}▷=>^n ⌜φ⌝) →
   φ.
 Proof.
   destruct use_credits.

iris/program_logic/total_adequacy.v

@@ -134,7 +134,7 @@ Theorem twp_total Σ Λ `{!invGpreS Σ} s e σ Φ n :
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp. apply (soundness (M:=iResUR Σ) _  1); simpl.
-  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _)=> Hinv HNC.
+  apply (fupd_plain_soundness_no_lc ⊤ ⊤ _ 0)=> Hinv HNC. iIntros "_".
   iMod (Hwp) as (stateI num_laters_per_step fork_post stateI_mono) "[Hσ H]".
   set (iG := IrisG _ _ Hinv stateI fork_post num_laters_per_step stateI_mono).
   iApply (@twptp_total _ _ iG _ _ n with "Hσ").

tests/heap_lang.v

 From iris.base_logic.lib Require Import gen_inv_heap invariants.
 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.heap_lang Require Import lang adequacy proofmode notation.
+From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
 From iris.heap_lang Require Import lang.
 From iris.prelude Require Import options.
@@ -453,3 +453,10 @@ End error_tests.
 (* Test a closed proof *)
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
 Proof. eapply (heap_adequacy heapΣ)=> ??. iIntros "_". by iApply heap_e_spec. Qed.
+
+Lemma heap_e_totally_adequate σ : sn erased_step ([heap_e], σ).
+Proof.
+  eapply (heap_total heapΣ NotStuck _ _ (const True))=> ??. iIntros "_".
+  rewrite /heap_e /=.
+  wp_alloc l. wp_load. wp_store. wp_load. auto.
+Qed.