Merge branch 'lc-heaplang' into 'master'

Basic later credits implementation for HeapLang

See merge request iris/iris!823

CHANGELOG.md

@@ -73,9 +73,8 @@ lemma.
 
 * Make the `inG` instances for `libG` fields local, so they are only used inside
   the library that defines the `libG`.
-* Prepare for supporting later credits, by adding a resource `£ n` describing
-  ownership of `n` credits that can be eliminated at fancy updates.
-  Note that HeapLang has not yet been equipped with support for later credits.
+* Add infrastructure for supporting later credits, by adding a resource `£ n`
+  describing ownership of `n` credits that can be eliminated at fancy updates.
   + To retain backwards compatibility with the interaction laws of fancy updates
     with the plainly modality (`BiFUpdPlainly`), which are incompatible with
     later credits, the logic has a new parameter of type `has_lc`, which is
@@ -129,14 +128,18 @@ lemma.
   number of steps taken so far. This number is tied to ghost state in the state
   interpretation, which is exposed, updated, and used with new lemmas
   `wp_lb_init`, `wp_lb_update`, and `wp_step_fupdN_lb`. (by Jonas Kastberg Hinrichsen)
-* In line with the support for later credits (see `base_logic`), `heapGS_gen`
-  now takes an additional `has_lc` parameter, and `heapGS` is a short-hand for
-  `heapGS_gen HasLc`. The adequacy statements for HeapLang have been changed
-  accordingly:
+* Make pattern argument of `wp_pure` tactic optional (defaults to wildcard
+  pattern, matching all redexes).
+* In line with the support for later credits (see `base_logic`), the tactic
+  `wp_pure` now takes an optional parameter `credit:"H"` which generates a
+  hypothesis `H` for a single later credit `£ 1` that can be eliminated using
+  `lc_fupd_elim_later`.
+  The typeclass `heapGS_gen` now takes an additional `has_lc` parameter, and
+  `heapGS` is a short-hand for `heapGS_gen HasLc`. The adequacy statements for
+  HeapLang have been changed accordingly:
   + `heap_adequacy` provides `heapGS`, thus enabling the use of later credits.
     This precludes usage of the laws in `BiFUpdPlainly` in the HeapLang instance of Iris.
   + `heap_total` provides `heapGS_gen HasNoLc`.
-  Currently, the primitive laws for HeapLang do not yet provide later credits.
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

docs/heap_lang.md

@@ -55,9 +55,12 @@ that the current goal is of the shape `WP e @ E {{ Q }}`.
 
 Tactics to take one or more pure program steps:
 
-- `wp_pure`: Perform one pure reduction step.  Pure steps are defined by the
-  `PureExec` typeclass and include beta reduction, projections, constructors, as
-  well as unary and binary arithmetic operators.
+- `wp_pure pat credit:"H"`: Perform one pure reduction step. `pat` optionally
+  defines the pattern that the redex has to match; it defaults to `_` (any
+  redex). The `credit:` argument is optional, too; when present, a later credit
+  will be generated in a fresh hypothesis named `"H"`.
+  Pure steps are defined by the `PureExec` typeclass and include beta reduction,
+  projections, constructors, as well as unary and binary arithmetic operators.
 - `wp_pures`: Perform as many pure reduction steps as possible. This
   tactic will **not** reduce lambdas/recs that are hidden behind a definition.
   If the computation reaches a value, the `WP` will be entirely removed and the

iris_heap_lang/proofmode.v

@@ -53,6 +53,26 @@ Proof.
   rewrite -total_lifting.twp_pure_step //.
 Qed.
 
+Lemma tac_wp_pure_credit `{!heapGS_gen hlc Σ} Δ Δ' s E j K e1 e2 ϕ Φ :
+  PureExec ϕ 1 e1 e2 →
+  ϕ →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  match envs_app false (Esnoc Enil j (£ 1)) Δ' with
+  | Some Δ'' =>
+     envs_entails Δ'' (WP fill K e2 @ s; E {{ Φ }})
+  | None => False
+  end →
+  envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
+Proof.
+  rewrite envs_entails_unseal=> ??? HΔ.
+  pose proof @pure_exec_fill.
+  rewrite -lifting.wp_pure_step_later; last done.
+  rewrite into_laterN_env_sound /=. apply later_mono.
+  destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
+  rewrite envs_app_sound //; simpl.
+  rewrite right_id. apply wand_intro_r. by rewrite wand_elim_l.
+Qed.
+
 Lemma tac_wp_value_nofupd `{!heapGS_gen hlc Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_unseal=> ->. by apply wp_value. Qed.
@@ -133,6 +153,36 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
   | _ => fail "wp_pure: not a 'wp'"
   end.
+Tactic Notation "wp_pure" :=
+  wp_pure _.
+
+Tactic Notation "wp_pure" open_constr(efoc) "credit:" constr(H) :=
+  iStartProof;
+  let Htmp := iFresh in
+  let finish _ :=
+    pm_reduce;
+    (iDestructHyp Htmp as H || fail 2 "wp_pure:" H "is not fresh");
+    wp_finish
+    in
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    let e := eval simpl in e in
+    reshape_expr e ltac:(fun K e' =>
+      unify e' efoc;
+      eapply (tac_wp_pure_credit _ _ _ _ Htmp K e');
+      [iSolveTC                       (* PureExec *)
+      |try solve_vals_compare_safe    (* The pure condition for PureExec --
+         handles trivial goals, including [vals_compare_safe] *)
+      |iSolveTC                       (* IntoLaters *)
+      |finish ()                      (* new goal *)
+      ])
+    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    fail "wp_pure: credit generation is not supported for a TWP"
+  | _ => fail "wp_pure: not a 'wp'"
+  end.
+Tactic Notation "wp_pure" "credit:" constr(H) :=
+  wp_pure _ credit: H.
 
 (* TODO: do this in one go, without [repeat]. *)
 Ltac wp_pures :=

tests/heap_lang.ref

@@ -179,6 +179,21 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
              (@iris_invGS HasLc heap_lang Σ (@heapGS_irisGS HasLc Σ heapGS0))))
        (@top coPset coPset_top) (@top coPset coPset_top)
        (@bi_pure (uPredI (iResUR Σ)) True))
+"test_wp_pure_credit_succeed"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  P : iProp Σ
+  ============================
+  "Hcred" : £ 1
+  --------------------------------------∗
+  |={⊤}=> ▷ P ={∅}=∗ P
+"test_wp_pure_credit_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_pure: "Hcred" is not fresh.
 1 goal
   
   Σ : gFunctors

tests/heap_lang.v

@@ -16,7 +16,7 @@ Section tests.
     ⌜(10 = 4 + 6)%nat⌝ -∗
     WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, ⌜v = #1⌝ }}.
   Proof.
-    iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
+    iIntros "?". wp_alloc l. repeat wp_pure || wp_load || wp_store.
     match goal with
     | |- context [ (10 = 4 + 6)%nat ] => done
     end.
@@ -44,8 +44,8 @@ Section tests.
   Lemma heap_e2_spec E : ⊢ WP heap_e2 @ E [{ v, ⌜v = #2⌝ }].
   Proof.
     iIntros "". rewrite /heap_e2.
-    wp_alloc l as "Hl". Show. wp_alloc l'.
-    wp_pures. wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
+    wp_alloc l as "Hl". Show. wp_alloc l'. do 2 wp_pure.
+    wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
     wp_store. wp_load. done.
   Qed.
 
@@ -336,6 +336,23 @@ Section tests.
     Show.
     Unset Printing All.
   Abort.
+
+  Check "test_wp_pure_credit_succeed".
+  Lemma test_wp_pure_credit_succeed P :
+    ⊢ WP #42 + #420 {{ v, ▷ P ={∅}=∗ P }}.
+  Proof.
+    wp_pure credit:"Hcred". Show.
+    iIntros "!> HP". iMod (lc_fupd_elim_later with "Hcred HP"). auto.
+  Qed.
+
+  Check "test_wp_pure_credit_fail".
+  Lemma test_wp_pure_credit_fail :
+    ⊢ True -∗ WP #42 + #420 {{ v, True }}.
+  Proof.
+    iIntros "Hcred".
+    Fail wp_pure credit:"Hcred".
+  Abort.
+
 End tests.
 
 Section mapsto_tests.