From 2b1b2c89b5925447f771c8676378330f0728bad3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Wed, 27 Jul 2022 21:31:53 +0200
Subject: [PATCH] basic heaplang implementation

---
 iris_heap_lang/primitive_laws.v | 40 +++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 91fd17a56..bfc3a73d7 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -170,6 +170,46 @@ 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. *)
+Lemma wp_pure_step_credit s E e1 e2 ϕ Φ :
+  PureExec ϕ 1 e1 e2 →
+  ϕ →
+  (£ 1 -∗ WP e2 @ s; E {{ Φ }}) -∗
+  WP e1 @ s; E {{ Φ }}.
+Proof.
+  iIntros (Hexec Hphi) "Hwp".
+  iApply wp_pure_step_later; done.
+Qed.
+
 (** Recursive functions: we do not use this lemmas as it is easier to use Löb
 induction directly, but this demonstrates that we can state the expected
 reasoning principle for recursive functions, without any visible â–·. *)
-- 
GitLab