for now, only prodice a simple one-credit-per-step tactic

iris_heap_lang/primitive_laws.v

@@ -170,36 +170,8 @@ Proof.
   iIntros "_". iPureIntro. rewrite /num_laters_per_step /=. lia.
 Qed.
 
-(** This lemma allows to get [S n] credits on a pure step,
-  when a lower bound of [n] on the number of steps taken is available. *)
-Lemma wp_pure_step_credits_lb ϕ e1 e2 s E n Φ :
-  PureExec ϕ 1 e1 e2 →
-  ϕ →
-  steps_lb n -∗
-  ▷ (£ (S n) -∗ steps_lb (S n) -∗ WP e2 @ s; E {{ Φ }}) -∗
-  WP e1 @ s; E {{ Φ }}.
-Proof.
-  iIntros (Hpure Hphi) "Hlb Hwp".
-  specialize (Hpure Hphi) as [Hsafe Hdet]%nsteps_once_inv.
-  iApply wp_lift_step_fupdN.
-  { eapply (reducible_not_val _ inhabitant). by apply reducible_no_obs_reducible. }
-  iIntros (σ1 ns κ κs nt) "(Hσ & Hκ & Hsteps)".
-  iDestruct (steps_lb_valid with "Hsteps Hlb") as %?.
-  iApply fupd_mask_intro; first set_solver. iIntros "Hcl".
-  iSplitR. { iPureIntro. destruct s; eauto using reducible_no_obs_reducible. }
-  iIntros (? σ2 efs (-> & -> & -> & ->)%Hdet) "Hcred".
-  iApply step_fupdN_intro; first done. iNext. iNext.
-  iMod "Hcl" as "_".
-  iPoseProof (lc_weaken (S n) with "Hcred") as "Hcred".
-  { rewrite /num_laters_per_step /=. lia. }
-  iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
-  iPoseProof (steps_lb_get with "Hsteps") as "#HlbS".
-  iModIntro. iFrame. iSplitL; last done.
-  iDestruct (steps_lb_le _ (S n) with "HlbS") as "HlbS'"; [lia|].
-  iApply ("Hwp" with "Hcred HlbS'").
-Qed.
-
-(** This just re-exports the lifting lemma when one wants to generate a single credit during a pure step. *)
+(** This just re-exports the lifting lemma when one wants to generate a single
+credit during a pure step. *)
 Lemma wp_pure_step_credit s E e1 e2 ϕ Φ :
   PureExec ϕ 1 e1 e2 →
   ϕ →

iris_heap_lang/proofmode.v

@@ -73,48 +73,6 @@ Proof.
   rewrite right_id. apply wand_intro_r. by rewrite wand_elim_l.
 Qed.
 
-Local Lemma wp_pure_step_credits_lb' `{!heapGS_gen hlc Σ} ϕ e1 e2 s E n Φ :
-  PureExec ϕ 1 e1 e2 →
-  ϕ →
-  ▷ (steps_lb n ∗ (£ (S n) -∗ steps_lb (S n) -∗ WP e2 @ s; E {{ Φ }})) -∗
-  WP e1 @ s; E {{ Φ }}.
-Proof.
-  iIntros (??) "[>Ha Hb]". by iApply (wp_pure_step_credits_lb with "Ha Hb").
-Qed.
-Lemma tac_wp_pure_credits_lb `{!heapGS_gen hlc Σ} Δ Δ' s E i j K e1 e2 ϕ n b Φ :
-  PureExec ϕ 1 e1 e2 →
-  ϕ →
-  MaybeIntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (b, steps_lb n)%I →
-  (match envs_simple_replace i b (Esnoc Enil i (steps_lb (S n))) Δ' with
-  | Some Δ'' =>
-     match envs_app false (Esnoc Enil j (£ (S n))) Δ'' with
-     | Some Δ''' => envs_entails Δ''' (WP fill K e2 @ s; E {{ Φ }})
-     | None => False
-     end
-  | None => False
-  end) →
-  envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
-Proof.
-  rewrite envs_entails_unseal=> ??? Hlb HΔ.
-  pose proof @pure_exec_fill.
-  rewrite -(wp_pure_step_credits_lb' _ _ _ _ _ n); last done.
-  rewrite into_laterN_env_sound /=.
-  destruct (envs_simple_replace _ _ _) as [Δ'''|] eqn:HΔ'''; [ | contradiction ].
-  destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ].
-  rewrite envs_simple_replace_sound; [ | done..]. simpl.
-  rewrite intuitionistically_if_elim.
-  destruct b.
-  all: rewrite right_id !later_sep.
-  all: apply sep_mono; first done.
-  all: apply later_mono, wand_intro_r, wand_intro_r.
-  all: rewrite -sep_assoc sep_comm -sep_assoc.
-  1: fold (bi_intuitionistically (steps_lb (S n))).
-  1: rewrite -(intuitionistically_intro (steps_lb (S n)) (steps_lb (S n))); last done.
-  all: rewrite wand_elim_r.
-  all: rewrite envs_app_sound // /= right_id wand_elim_r //.
-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.
@@ -196,7 +154,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
-Tactic Notation "wp_pure" open_constr(efoc) "as" constr(H) :=
+Tactic Notation "wp_pure" open_constr(efoc) "credit:" constr(H) :=
   iStartProof;
   let Htmp := iFresh in
   let finish _ :=
@@ -221,38 +179,8 @@ Tactic Notation "wp_pure" open_constr(efoc) "as" constr(H) :=
     fail "wp_pure: credit generation is not supported for a TWP"
   | _ => fail "wp_pure: not a 'wp'"
   end.
-Tactic Notation "wp_pure" "as" constr(H) :=
-  wp_pure _ as H.
-
-Tactic Notation "wp_pure" open_constr(efoc) "with" constr(Hlb) "as" 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
-  let find_lb _ := iAssumptionCore || fail 2 "wp_pure: cannot find " Hlb " : steps_lb _" 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_credits_lb _ _ _ _ Hlb Htmp K e');
-      [iSolveTC                       (* PureExec *)
-      |try solve_vals_compare_safe    (* The pure condition for PureExec --
-         handles trivial goals, including [vals_compare_safe] *)
-      |iSolveTC                       (* IntoLaters *)
-      |find_lb ()                     (* The [steps_lb _] hypothesis *)
-      |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" "with" constr(Hlb) "as" constr(H) :=
-  wp_pure _ with Hlb as H.
+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

@@ -193,39 +193,6 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
      : string
 The command has indeed failed with message:
 Tactic failure: wp_pure:  "Hcred"  is not fresh.
-"test_wp_pure_credits_lb_succeed_spatial"
-     : string
-1 goal
-  
-  Σ : gFunctors
-  heapGS0 : heapGS Σ
-  n : nat
-  ============================
-  "Hlb" : steps_lb (S n)
-  "Hcred" : £ (S n)
-  --------------------------------------∗
-  |={⊤}=> True
-"test_wp_pure_credits_lb_succeed_intuit"
-     : string
-1 goal
-  
-  Σ : gFunctors
-  heapGS0 : heapGS Σ
-  n : nat
-  ============================
-  "Hlb" : steps_lb (S n)
-  --------------------------------------□
-  "Hcred" : £ (S n)
-  --------------------------------------∗
-  |={⊤}=> True
-"test_wp_pure_credits_lb_fail1"
-     : string
-The command has indeed failed with message:
-Tactic failure: wp_pure: cannot find  "Hl"  : steps_lb _.
-"test_wp_pure_credits_lb_fail2"
-     : string
-The command has indeed failed with message:
-Tactic failure: wp_pure:  "Hlb"  is not fresh.
 1 goal
   
   Σ : gFunctors

tests/heap_lang.v

@@ -341,7 +341,7 @@ Section tests.
   Lemma test_wp_pure_credit_succeed :
     ⊢ WP #42 + #420 {{ v, True }}.
   Proof.
-    wp_pure as "Hcred". Show. done.
+    wp_pure credit: "Hcred". Show. done.
   Qed.
 
   Check "test_wp_pure_credit_fail".
@@ -349,40 +349,9 @@ Section tests.
     ⊢ True -∗ WP #42 + #420 {{ v, True }}.
   Proof.
     iIntros "Hcred".
-    Fail wp_pure as "Hcred".
+    Fail wp_pure credit: "Hcred".
   Abort.
 
-  Check "test_wp_pure_credits_lb_succeed_spatial".
-  Lemma test_wp_pure_credits_lb_succeed_spatial n :
-    ⊢ steps_lb n -∗ WP #42 + #420 {{ v, True }}.
-  Proof.
-    iIntros "Hlb".
-    wp_pure with "Hlb" as "Hcred". Show. done.
-  Qed.
-
-  Check "test_wp_pure_credits_lb_succeed_intuit".
-  Lemma test_wp_pure_credits_lb_succeed_intuit n :
-    ⊢ steps_lb n -∗ WP #42 + #420 {{ v, True }}.
-  Proof.
-    iIntros "#Hlb".
-    wp_pure with "Hlb" as "Hcred". Show. done.
-  Qed.
-
-  Check "test_wp_pure_credits_lb_fail1".
-  Lemma test_wp_pure_credits_lb_fail1 n :
-    ⊢ steps_lb n -∗ WP #42 + #420 {{ v, True }}.
-  Proof.
-    iIntros "Hlb".
-    Fail wp_pure with "Hl" as "Hcred".
-  Abort.
-
-  Check "test_wp_pure_credits_lb_fail2".
-  Lemma test_wp_pure_credits_lb_fail2 n :
-    ⊢ steps_lb n -∗ WP #42 + #420 {{ v, True }}.
-  Proof.
-    iIntros "Hlb".
-    Fail wp_pure with "Hlb" as "Hlb".
-  Abort.
 End tests.
 
 Section mapsto_tests.