From 16263efa70f3b88840eae9234f6ac8e12b72f7ed Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Wed, 27 Jul 2022 09:09:15 +0200
Subject: [PATCH] bump Iris, and comment a few printing commands

---
 _CoqProject                                   |   1 +
 semantics.opam                                |   4 +-
 theories/program_logics/concurrency.v         |  16 +-
 theories/program_logics/fupd.v                |   4 +-
 theories/program_logics/hoare.v               |  52 ++--
 theories/program_logics/ipm.v                 |  46 +--
 theories/program_logics/later_loeb.v          | 269 +++++++++++++-----
 theories/program_logics/logrel/ghost_state.v  |  80 +++---
 .../program_logics/program_logic/adequacy.v   |   3 +-
 theories/program_logics/reloc/src_rules.v     |  16 +-
 theories/program_logics/resource_algebras.v   |  38 +--
 11 files changed, 333 insertions(+), 196 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index e67a908..ac2d6e3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -119,6 +119,7 @@ theories/program_logics/reloc/fundamental.v
 theories/program_logics/reloc/adequacy.v
 theories/program_logics/reloc/contextual_refinement.v
 
+
 # concurrency
 theories/program_logics/concurrency.v
 theories/program_logics/concurrent_logrel/syntactic.v
diff --git a/semantics.opam b/semantics.opam
index d095cc2..3a389dc 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -7,8 +7,8 @@ synopsis: "Best course this side of the milky way"
 
 depends: [
   "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
-  "coq-iris" { (= "dev.2022-07-08.0.a513639d") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2022-07-08.0.a513639d") | (= "dev") }
+  "coq-iris" { (= "dev.2022-07-26.0.23bdf6bd") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-07-26.0.23bdf6bd") | (= "dev") }
   "coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") }
   "coq-autosubst" { = "1.7" }
 ]
diff --git a/theories/program_logics/concurrency.v b/theories/program_logics/concurrency.v
index d013506..92b4319 100644
--- a/theories/program_logics/concurrency.v
+++ b/theories/program_logics/concurrency.v
@@ -13,17 +13,17 @@ From iris.prelude Require Import options.
   You can ignore the κs (it relates to another feature, prophecy variables, that we are not going to get into in this course).
   (it corresponds to the notion of "base steps" →_b  in the lecture notes)
  *)
-Check prim_step.
+(*Check prim_step.*)
 (** [step] lifts this reduction to thread pools. *)
-Check step.
+(*Check step.*)
 
-Check ForkS.
+(*Check ForkS.*)
 (** In Iris's HeapLang, CAS is encoded in terms of another primitive: CmpXchg, namely, "compare and exchange".
   The difference to CAS is that it returns not only a Boolean flag (indicating success or failure), but rather
   a pair that also contains the old/current value.
 *)
-Print CAS.
-Check CmpXchgS.
+(*Print CAS.*)
+(*Check CmpXchgS.*)
 
 Global Notation "{{ P } } e {{ Φ } }" := (□(P%I -∗ WP e {{ Φ%I }}))%I
   (at level 20, P, e, Φ at level 200,
@@ -34,9 +34,9 @@ Global Notation "{{ P } } e {{ v , Q } }" := (□ (P%I -∗ WP e {{ v, Q%I }}))%
   format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
 
 (** Weakest Precondition Rules *)
-Check wp_cmpxchg_fail.
-Check wp_cmpxchg_suc.
-Check wp_fork.
+(*Check wp_cmpxchg_fail.*)
+(*Check wp_cmpxchg_suc.*)
+(*Check wp_fork.*)
 
 Definition assert (e : expr) : expr :=
   if: e then #() else #0 #0.
diff --git a/theories/program_logics/fupd.v b/theories/program_logics/fupd.v
index 870b73c..bca156e 100644
--- a/theories/program_logics/fupd.v
+++ b/theories/program_logics/fupd.v
@@ -25,7 +25,7 @@ Proof.
   iIntros "[>HP HPQ]". by iApply "HPQ".
 Qed.
 
-Check bupd_fupd.
+(*Check bupd_fupd.*)
 
 Lemma fupd_wp' (e : expr) (Φ : val → iProp Σ) s E1 E2 E3:
   (|={E1, E2}=> WP e @ s; E2; E3 {{ Φ }}) -∗ WP e @ s; E1; E3 {{ Φ }}.
@@ -47,7 +47,7 @@ Proof.
   intros. by iApply inv_acc.
 Qed.
 
-Check fupd_mask_frame_r.
+(*Check fupd_mask_frame_r.*)
 
 Lemma fupd_intro_mask E1 E2 P :
   E2 ⊆ E1 →
diff --git a/theories/program_logics/hoare.v b/theories/program_logics/hoare.v
index 48b28d9..ea272a6 100644
--- a/theories/program_logics/hoare.v
+++ b/theories/program_logics/hoare.v
@@ -13,23 +13,23 @@ Implicit Types
 (** * Hoare logic *)
 
 (** Entailment rules *)
-Check ent_equiv.
-Check ent_refl.
-Check ent_trans.
+(*Check ent_equiv.*)
+(*Check ent_refl.*)
+(*Check ent_trans.*)
 (* NOTE: True = ⌜True⌝ *)
 (* NOTE: False = ⌜False⌝ *)
-Check ent_prove_pure.
-Check ent_assume_pure.
-Check ent_and_elim_r.
-Check ent_and_elim_l.
-Check ent_and_intro.
-Check ent_or_introl.
-Check ent_or_intror.
-Check ent_or_elim.
-Check ent_all_intro.
-Check ent_all_elim.
-Check ent_exist_intro.
-Check ent_exist_elim.
+(*Check ent_prove_pure.*)
+(*Check ent_assume_pure.*)
+(*Check ent_and_elim_r.*)
+(*Check ent_and_elim_l.*)
+(*Check ent_and_intro.*)
+(*Check ent_or_introl.*)
+(*Check ent_or_intror.*)
+(*Check ent_or_elim.*)
+(*Check ent_all_intro.*)
+(*Check ent_all_elim.*)
+(*Check ent_exist_intro.*)
+(*Check ent_exist_elim.*)
 
 (** Derived entailment rules *)
 Lemma ent_weakening P Q R :
@@ -445,13 +445,13 @@ Proof.
 Admitted.
 
 (** * Separation Logic *)
-Check ent_sep_weaken.
-Check ent_sep_true.
-Check ent_sep_comm.
-Check ent_sep_split.
-Check ent_sep_assoc.
-Check ent_pointsto_sep.
-Check ent_exists_sep.
+(*Check ent_sep_weaken.*)
+(*Check ent_sep_true.*)
+(*Check ent_sep_comm.*)
+(*Check ent_sep_split.*)
+(*Check ent_sep_assoc.*)
+(*Check ent_pointsto_sep.*)
+(*Check ent_exists_sep.*)
 
 (* Note: the separating conjunction can be typed with `\sep` *)
 
@@ -510,10 +510,10 @@ Qed.
 
 
 (** New Hoare rules *)
-Check hoare_frame.
-Check hoare_new.
-Check hoare_store.
-Check hoare_load.
+(*Check hoare_frame.*)
+(*Check hoare_new.*)
+(*Check hoare_store.*)
+(*Check hoare_load.*)
 
 Lemma hoare_pure_pre_sep_l (ϕ : Prop) Q Φ e :
   (ϕ → {{ Q }} e {{ Φ }}) →
diff --git a/theories/program_logics/ipm.v b/theories/program_logics/ipm.v
index d2876a5..0c2e784 100644
--- a/theories/program_logics/ipm.v
+++ b/theories/program_logics/ipm.v
@@ -7,8 +7,8 @@ From semantics.pl.program_logic Require Import notation.
 
 (** ** Magic is in the air *)
 Import hoare.
-Check ent_wand_intro.
-Check ent_wand_elim.
+(*Check ent_wand_intro.*)
+(*Check ent_wand_elim.*)
 
 Section primitive.
 Implicit Types (P Q R: iProp).
@@ -283,13 +283,13 @@ Admitted.
 
 (** Weakest precondition rules *)
 
-Check ent_wp_value.
-Check ent_wp_wand.
-Check ent_wp_bind.
-Check ent_wp_pure_step.
-Check ent_wp_new.
-Check ent_wp_load.
-Check ent_wp_store.
+(*Check ent_wp_value.*)
+(*Check ent_wp_wand.*)
+(*Check ent_wp_bind.*)
+(*Check ent_wp_pure_step.*)
+(*Check ent_wp_new.*)
+(*Check ent_wp_load.*)
+(*Check ent_wp_store.*)
 
 Lemma ent_wp_pure_steps e e' Φ :
   rtc pure_step e e' →
@@ -426,14 +426,14 @@ Admitted.
 
 
 (** ** Persistency *)
-Check ent_pers_dup.
-Check ent_pers_elim.
-Check ent_pers_mono.
-Check ent_pers_pure.
-Check ent_pers_and_sep.
-Check ent_pers_idemp.
-Check ent_pers_all.
-Check ent_pers_exists.
+(*Check ent_pers_dup.*)
+(*Check ent_pers_elim.*)
+(*Check ent_pers_mono.*)
+(*Check ent_pers_pure.*)
+(*Check ent_pers_and_sep.*)
+(*Check ent_pers_idemp.*)
+(*Check ent_pers_all.*)
+(*Check ent_pers_exists.*)
 
 Lemma ent_pers_dup' P :
   □ P ⊢ (□ P) ∗ (□ P).
@@ -551,15 +551,17 @@ Section hoare_external.
 End hoare_external.
 
 (** ** Invariants *)
-Check ent_inv_pers.
-Check ent_inv_alloc.
+(*Check ent_inv_pers.*)
+(*Check ent_inv_alloc.*)
+
 (* The following rule is more comvenient to use *)
-Check inv_alloc.
+(*Check inv_alloc.*)
+
 (** We require a sidecondition here, namely that [F] is "timeless". All propositions we have seen up to now are in fact timeless.
   We will see propositions that do not satisfy this requirement and which need a stronger rule for invariants soon.
 *)
-Check ent_inv_open.
-Check inv_open.
+(*Check ent_inv_open.*)
+(*Check inv_open.*)
 
 
 (** MyMutBit *)
diff --git a/theories/program_logics/later_loeb.v b/theories/program_logics/later_loeb.v
index 6fbcae8..0b5568a 100644
--- a/theories/program_logics/later_loeb.v
+++ b/theories/program_logics/later_loeb.v
@@ -6,25 +6,25 @@ From semantics.pl Require Import hoare_lib.
 From semantics.pl.program_logic Require Import notation.
 From semantics.pl Require Import ipm.
 
-(** Step-indexing *)
+(** ** Step-indexing *)
 Import hoare ipm.
 Implicit Types
   (P Q R: iProp)
   (Φ Ψ : val → iProp)
 .
 
-Check ent_later_intro.
-Check ent_later_mono.
-Check ent_löb.
-Check ent_later_sep.
-Check ent_later_exists.
-Check ent_later_all.
-Check ent_later_pers.
+(*Check ent_later_intro.*)
+(*Check ent_later_mono.*)
+(*Check ent_löb.*)
+(*Check ent_later_sep.*)
+(*Check ent_later_exists.*)
+(*Check ent_later_all.*)
+(*Check ent_later_pers.*)
 
-Check ent_later_wp_pure_step.
-Check ent_later_wp_new.
-Check ent_later_wp_load.
-Check ent_later_wp_store.
+(*Check ent_later_wp_pure_step.*)
+(*Check ent_later_wp_new.*)
+(*Check ent_later_wp_load.*)
+(*Check ent_later_wp_store.*)
 
 (* Exercise: Derive the old rules from the new ones. *)
 Lemma ent_wp_pure_step_old e e' Φ :
@@ -49,19 +49,40 @@ Proof.
   (* FIXME: exercise *)
 Admitted.
 
-(* TODO: this is an exercise *)
 Lemma ent_later_and P Q :
   ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q.
 Proof.
-  (* FIXME: exercise *)
-Admitted.
+  specialize (ent_later_all (λ b : bool, if b then P else Q)). rewrite !ent_equiv.
+  intros [Ha Hb]. split.
+  - apply ent_and_intro.
+    + etrans; first etrans; [ | apply Ha | ].
+      * apply ent_later_mono. apply ent_all_intro. intros []; [apply ent_and_elim_l | apply ent_and_elim_r].
+      * etrans; first apply (ent_all_elim true). apply ent_later_mono. done.
+    + apply ent_later_mono. apply ent_and_elim_r.
+  - etrans; first etrans; [ | apply Hb | ].
+    + apply ent_all_intro. intros []; [apply ent_and_elim_l | apply ent_and_elim_r].
+    + apply ent_later_mono. apply ent_and_intro.
+      * apply (ent_all_elim true).
+      * apply (ent_all_elim false).
+Qed.
 
-(* TODO this is an exercise *)
 Lemma ent_later_or P Q :
   ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q.
 Proof.
-  (* FIXME: exercise *)
-Admitted.
+  specialize (ent_later_exists (λ b : bool, if b then P else Q)). rewrite !ent_equiv.
+  intros [Ha Hb]. split.
+  - etrans; first etrans; [ | apply Ha | ].
+    + apply ent_later_mono. apply ent_or_elim.
+      * by apply (ent_exist_intro true).
+      * by apply (ent_exist_intro false).
+    + apply ent_exist_elim. intros []; [apply ent_or_introl | apply ent_or_intror].
+  - etrans; first etrans; [ | apply Hb | ].
+    + apply ent_or_elim.
+      * by apply (ent_exist_intro true).
+      * by apply (ent_exist_intro false).
+    + apply ent_later_mono. apply ent_exist_elim.
+      intros []; [apply ent_or_introl | apply ent_or_intror].
+Qed.
 
 Lemma ent_all_pers {X} (Φ : X → iProp) :
   □ (∀ x : X, Φ x) ⊢ ∀ x : X, □ Φ x.
@@ -104,7 +125,7 @@ Proof.
 
   Restart.
   iIntros "($ & $)".
-Qed.
+Abort.
 
 Lemma ipm_later_exists_commuting (Φ : nat → iProp) :
   ▷ (∃ n : nat, Φ n) -∗ ∃ n : nat, ▷ Φ n.
@@ -112,8 +133,8 @@ Proof.
   (* automatically commutes the later around the existential *)
   (* note: in general, this relies on the type that is existentially quantified over
     to be [Inhabited]. The IPM tactics will fail if an instance for that cannot be found. *)
-  iIntros "(%n & Hn)". eauto with iFrame.
-Qed.
+  iIntros "(%n & Hn)".
+Abort.
 
 Lemma ipm_later_or_commuting P Q :
   ▷ (P ∨ Q) -∗ ▷ P ∨ ▷ Q.
@@ -123,7 +144,7 @@ Proof.
 
   Restart.
   iIntros "[ $ | $ ]".
-Qed.
+Abort.
 
 Lemma ipm_later_next_1 P Q R `{!Persistent P} :
   ▷ P -∗ ▷ R -∗ ▷ Q.
@@ -133,15 +154,20 @@ Proof.
   iNext.
 Abort.
 
-(* The recursion lemma from above, proved with the IPM and Löb induction *)
+(** The recursion lemma from above, proved with the IPM and Löb induction *)
 Lemma ent_wp_rec v Φ (Ψ : val → val → iProp) e :
   (∀ v, (Φ v ∗ (∀ u, {{ Φ u }} (rec: "f" "x" := e) u {{ Ψ u }}) ⊢ WP subst "x" v (subst "f" (rec: "f" "x" := e) e) {{ Ψ v }})) →
   (Φ v ⊢ WP (rec: "f" "x" := e) v {{ Ψ v }}).
 Proof.
-  iIntros (Hs). iLöb as "IH" forall (v). iIntros "Hv".
-  wp_pures. iApply Hs. iFrame "Hv". eauto.
+  iIntros (Hs). iLöb as "IH" forall (v).
+  iIntros "Hv".
+  wp_pures. iApply Hs. iFrame "Hv".
+  iIntros (v') "!> Hv'".
+  by iApply "IH".
 Qed.
 
+
+(** The Z combinator *)
 Section Z.
   Context (e : expr).
   Definition g : val := λ: "f", let: "f" := λ: "x", "f" "f" "x" in λ: "x", e.
@@ -151,21 +177,20 @@ Section Z.
     (∀ v, (Φ v ∗ (∀ u, {{ Φ u }} Z_com u {{ Ψ u }}) ⊢ WP subst "x" v (subst "f" Z_com e) {{ Ψ v }})) →
     (Φ v ⊢ WP Z_com v {{ Ψ v }}).
   Proof.
-   (* FIXME: exercise *)
-Admitted.
+    (* FIXME: exercise *)
+  Admitted.
 End Z.
 
-(** ** Recursive definitions *)
 Notation iPropO := (iPropO adequacy.heapΣ).
 (** To define the recursive predicate [infinite_exec] formally (by taking a fixpoint), we need to invoke some machinery.
  *)
-(* We first define the function of which we take the fixpoint (in [μ F. P], imagine that this is the function taking F and returning P).
+(** We first define the function of which we take the fixpoint (in [μ F. P], imagine that this is the function taking F and returning P).
  We use [exprO] instead of [expr], [iPropO] instead of [iProp], and [λne] and [-n>] to account for some of the details of Iris's algebraic step-indexed model which enables us to make this recursive definition.
   This will become clearer in a few weeks when we consider Iris's model.
  *)
 Definition infinite_exec_pre (inf : exprO -n> iPropO) : exprO -n> iPropO :=
   (λne e, ∃ e', ⌜pure_step e e'⌝ ∗ ▷ inf e')%I.
-(*
+(**
   Our recursive definition needs to be [Contractive], which essentially means that
   all recursive occurrences of the predicate are guarded by a ▷.
   This ensures that we can take the fixpoint.
@@ -196,7 +221,7 @@ Lemma infinite_exec_Omega :
   ⊢ infinite_exec Omega.
 Proof.
   iLöb as "IH".
-  rewrite {2} infinite_exec_unfold /infinite_exec_pre /=.
+  rewrite {2}infinite_exec_unfold /infinite_exec_pre /=.
   iExists Omega. iSplitR; last done.
   iPureIntro. apply pure_step_beta.
 Qed.
@@ -204,14 +229,16 @@ Qed.
 Lemma infinite_wp_False' e :
   infinite_exec e ⊢ WP e {{ _, False }}.
 Proof.
-  (* FIXME: exercise, don't use the IPM *)
+  (* FIXME: exercise *)
 Admitted.
 Lemma infinite_wp_False e :
   infinite_exec e ⊢ WP e {{ _, False }}.
 Proof.
-  (* FIXME: exercise, use the IPM *)
+  (* FIXME: exercise *)
 Admitted.
 
+
+
 (** Diverge using higher-order state *)
 Definition diverge_ho : expr :=
   let: "d" := ref (λ: "x", "x") in
@@ -227,7 +254,7 @@ Proof.
   wp_load. wp_pures. by iApply "IH".
 Qed.
 
-(** Exercise: Landin's knot *)
+(** Landin *)
 Definition landins_knot : val :=
   λ: "f",
     let: "x" := ref (λ: "x", #0) in
@@ -246,8 +273,8 @@ Admitted.
 Import impred_invariants.
 (* [ent_inv_pers] and [ent_inv_alloc] hold unchanged *)
 (* The opening rules that support impredicative invariants put a later ▷ around the contents [F]. *)
-Check ent_inv_open.
-Check inv_open.
+(*Check ent_inv_open.*)
+(*Check inv_open.*)
 
 Definition lazyintN := nroot .@ "lazyint".
 Definition LazyInt (f : val) (n : Z) : iProp := WP (f #()) {{ w, ⌜w = #n⌝ }}%I.
@@ -267,65 +294,161 @@ Proof.
   wp_pures. by iApply ent_wp_value.
 Qed.
 
+Definition retrieve : val :=
+  λ: "c", match: !"c" with
+  InjL "cc" =>
+    match: "cc" with
+     InjL "f" => "c" <- InjR #();; InjL "f"
+   | InjR "y" => InjR "y"
+   end
+ | InjR "cc" =>
+   (* error case, we just diverge *)
+   (rec: "rec" <> := "rec" #()) #()
+  end.
+
 Definition cache : val :=
   λ: "f",
   let: "c" := ref (InjL (InjL "f")) in
-  λ: <>, let: "res" := ref (InjLV #()) in
-         match: !"c" with
-          InjL "cc" =>
-            match: "cc" with
-             InjL "f" => "c" <- InjR #();; "res" <- InjL "f"
-           | InjR "y" => "res" <- InjR "y"
-           end
-         | InjR "cc" =>
-           (* error case, we just diverge *)
-           (rec: "rec" <> := "rec" #()) #()
-         end;;
-         match: !"res" with
+  λ: <>, let: "r" := retrieve "c" in
+         match: "r" with
            InjL "f" => let: "y" := "f" #() in "c" <- InjL (InjR "y");; "y"
          | InjR "y" => "y"
          end.
 
+Local Definition I (f: val) (n: Z) (l: loc) : iProp :=
+  (((l ↦ InjLV (InjLV f) ∗ LazyInt f n) ∨ l ↦ InjLV (InjRV #n)) ∨ l ↦ InjRV #())%I.
+
+Lemma retrieve_spec f n l N:
+  ▷ I f n l ⊢ WP retrieve #l @ ⊤∖↑N {{ r, I f n l ∗ (⌜r = InjLV f⌝ ∗ LazyInt f n ∨ ⌜r = InjRV #n⌝) }}.
+Proof.
+  iIntros "I". unfold retrieve. wp_pure _.
+  unfold I at 1. iDestruct "I" as "[[[Hl Hlzy]|Hl]|Hl]".
+  - wp_load. wp_pures. wp_store. wp_pures. iApply wp_value.
+    unfold I. eauto with iFrame.
+  - wp_load. wp_pures. iApply wp_value.
+    unfold I. eauto with iFrame.
+  - wp_load. wp_pures. iClear "Hl".
+    iLöb as "IH". wp_pure _. done.
+Qed.
+
 Lemma cache_spec f n :
   ⊢ {{ LazyInt f n }} cache f {{ g, □ LazyInt g n }}.
 Proof.
   iIntros "!> Hlazy". unfold cache.
   wp_alloc l as "Hc". wp_pures.
 
-  set (INV := (((l ↦ InjLV (InjLV f) ∗ LazyInt f n) ∨ l ↦ InjLV (InjRV #n)) ∨ l ↦ InjRV #())%I).
   set (Name := lazyintN.@ l).
-  iApply (inv_alloc Name INV with "[Hlazy Hc]").
-  { unfold INV. iLeft. iLeft. iFrame. }
+  iApply (inv_alloc Name (I f n l) with "[Hlazy Hc]").
+  { unfold I. eauto with iFrame. }
   iIntros "#HInv".
 
   iApply wp_value.
   unfold LazyInt. iModIntro.
-  wp_pures. wp_alloc res as "Hres". wp_pures.
-  wp_bind (Case _ _ _).
+  wp_pures. wp_bind (retrieve _).
   iApply (inv_open with "HInv"); first set_solver.
-  iIntros "Hinv". rewrite {2}/INV.
-  iDestruct "Hinv" as "[[(>Hl & Hlazy) | Hl] | Hl]".
-  - wp_load. wp_pures. wp_store. wp_store.
-    iApply wp_value. iSplitL "Hl".
-    { iRight. iFrame. }
-    wp_pures. wp_load. wp_pures.
-    wp_bind (f _).
-    iApply (wp_wand with "Hlazy").
+  iIntros "I". iApply (wp_wand with "[I]").
+  { by iApply retrieve_spec. }
+  iIntros (r) "[I Hr]". iFrame "I".
+  iDestruct "Hr" as "[[-> Hlzy]|->]"; wp_pures; last first.
+  - iApply wp_value. done.
+  - wp_bind (f _). iApply (wp_wand with "Hlzy").
     iIntros (v) "->". wp_pures.
+    wp_bind (#l <- _)%E.
     iApply (inv_open with "HInv"); first set_solver.
-    iIntros "Hinv".
-    iDestruct "Hinv" as "[[(>Hl & Hlazy) | >Hl] | >Hl]";
-    wp_store; iApply wp_value.
-    all: iSplitL; last done. all: iLeft; iRight; iFrame.
-  - wp_load. wp_pures. wp_store. iApply wp_value.
-    iSplitL "Hl". { iLeft. iRight. iFrame. }
-    wp_pures. wp_load. wp_pures. iApply wp_value. done.
-  - wp_load. wp_pures.
-    iClear "Hres Hl".
-    iLöb as "IH". wp_rec. iApply "IH".
+    iIntros "I"; iDestruct "I" as "[[[>Hl Hlzy]|>Hl]|>Hl]"; wp_store;
+      iApply wp_value; iSplitL; unfold I; eauto with iFrame.
+    all: wp_pures; iApply wp_value; done.
+Qed.
+
+Definition cache' : val :=
+  λ: "f",
+  let: "c" := ref (InjL "f") in
+  λ: <>, match: !"c" with
+          InjL "g" =>
+            let: "k" := "g" #() in "c" <- "k";; "k"
+          | InjR "k" =>  "k"
+          end.
+
+
+Definition E : expr :=
+  let: "z" := ref (λ: <>, #0) in
+  let: "r" := ref #true in
+  let: "z'" :=
+    λ: <>, (assert (!"r");; "r" <- #false;; !"z") #() in
+  let: "c" := cache' "z'" in
+  "z" <- "c";; "c" #().
+
+
+
+Lemma E_safe :
+  (∀ f n, {{ LazyInt f n }} cache' f {{ g, □ LazyInt g n }}) ⊢
+  {{ True }} E {{ _, True }}.
+Proof.
+  iIntros "#Hcache !> _". rewrite /E. wp_alloc z as "Hz".
+  iAssert (□ LazyInt (λ: <>, #0) 0)%I as "Hlazy".
+  { iModIntro. rewrite /LazyInt. wp_pures. by iApply wp_value. }
+  wp_pures. wp_alloc r as "Hr". wp_pures.
+  pose (λ: <>, (assert (! #r);; #r <- #false;; ! #z) #())%V as h. fold h.
+  iApply (inv_alloc nroot (∃ f, z ↦ f ∗ □ LazyInt f 0) with "[Hz]").
+  { iExists _. iFrame. done. }
+  iIntros "#I". iClear "Hlazy".
+  iAssert (LazyInt h 0) with "[Hr]" as "Hh".
+  { rewrite /LazyInt /h. wp_pure _.
+    (* the code here is a bit akward due to the
+       fact that we need to close invariants in the
+       post *)
+    wp_bind (_;; _ ;; _)%E.
+    iApply (inv_open with "I"); first set_solver.
+    iIntros "Inv". rewrite /h. wp_pures.
+    iDestruct "Inv" as "(%f & Hz & #Hf)".
+    wp_load. wp_pures. wp_store. wp_load.
+    iApply wp_value.
+    (* we close the invariant again *)
+    iSplitL "Hz"; first eauto with iFrame.
+    iApply "Hf". }
+    (* since h is a lazy int, we can cache it *)
+    wp_bind (cache' h).
+    iApply (wp_wand with "[Hh]"); first by iApply "Hcache".
+    iIntros (c) "#Hc".
+
+    wp_pures. wp_bind (_ <- _)%E.
+    iApply (inv_open with "I"); first set_solver.
+    iIntros "(%f & >Hz & Hlazy)". wp_store.
+    iApply wp_value.
+
+    iSplitL "Hz"; first by eauto with iFrame.
+    wp_pures. iApply (wp_wand with "Hc").
+    iIntros (v) "_". done.
 Qed.
 
-(** Exercise: LazyInt2 *)
+
+(** Let's see what happens if we symbolically execute E.
+   We do it inside of a weakest pre, because we can use all
+   of Iris's tactics. If you do not trust this setup and
+   believe some the proof takes a wrong turn somewhere, you
+   can always use the operatinal semantics itself to show
+   that E will reach a stuck state. *)
+Lemma E_not_safe:
+  ⊢ {{ True }} E {{ _, True }}.
+Proof.
+  iIntros "!> _". rewrite /E. wp_alloc z as "Hz".
+  wp_pures. wp_alloc r as "Hr". wp_pures.
+  pose (λ: <>, (assert (! #r);; #r <- #false;; ! #z) #())%V as h. fold h.
+  rewrite /cache'.
+  wp_pures. wp_alloc l as "Hl".
+  wp_pures. wp_store.
+  wp_pures. wp_load.
+  wp_pures. rewrite {2}/h.
+  wp_pures. wp_load. wp_pures.
+  wp_store. wp_load. wp_pures.
+  wp_load. wp_pures. rewrite {2}/h.
+  wp_pures. wp_load. wp_pures.
+  wp_bind (#0 #0)%E.
+
+  (* Whooops *)
+Abort.
+
+
 Definition lazyint_two : val :=
   λ: "f1" "f2" "i",
     let: "c" := cache "i" in
@@ -340,7 +463,7 @@ Proof.
 Admitted.
 
 
-(** Exercise: Derive the invariant opening rule for timeless propositions. *)
+(** Exercise: derive the invariant rule for timeless propositions *)
 Lemma inv_open_timeless N E F `{!Timeless F} e Φ :
   ↑N ⊆ E →
   inv N F -∗
diff --git a/theories/program_logics/logrel/ghost_state.v b/theories/program_logics/logrel/ghost_state.v
index b6ab827..79ab894 100644
--- a/theories/program_logics/logrel/ghost_state.v
+++ b/theories/program_logics/logrel/ghost_state.v
@@ -9,9 +9,9 @@ From iris.prelude Require Import options.
 Set Default Proof Using "Type*".
 
 (** Update rules *)
-Check upd_return.
-Check upd_bind.
-Check upd_wp.
+(*Check upd_return.*)
+(*Check upd_bind.*)
+(*Check upd_wp.*)
 
 (** Derived rules *)
 Section derived.
@@ -30,17 +30,15 @@ Section derived.
     (P ⊢ Q) →
     (|==> P) ⊢ |==> Q.
   Proof.
-    (* FIXME exercise *)
+    (* FIXME: exercise *)
   Admitted.
 
-
   Lemma upd_trans P :
     (|==> |==> P) ⊢ |==> P.
   Proof.
-    (* FIXME exercise *)
+    (* FIXME: exercise *)
   Admitted.
 
-
   Lemma upd_frame P Q :
     P -∗ (|==> Q) -∗ |==> (P ∗ Q).
   Proof.
@@ -49,19 +47,20 @@ Section derived.
 End derived.
 
 (** ** The mono nat ghost theory *)
-Check mono.
-Check lb.
+(*Check mono.*)
+(*Check lb.*)
 
-Check mono_nat_make_bound.
-Check mono_nat_use_bound.
-Check mono_nat_increase_val.
-Check mono_nat_new.
+(*Check mono_nat_make_bound.*)
+(*Check mono_nat_use_bound.*)
+(*Check mono_nat_increase_val.*)
+(*Check mono_nat_new.*)
 
 (* The lb resource is persistent *)
-Check mono_nat_lb_persistent.
+(*Check mono_nat_lb_persistent.*)
+
 (* Both resources are also timeless *)
-Check mono_nat_lb_timeless.
-Check mono_nat_mono_timeless.
+(*Check mono_nat_lb_timeless.*)
+(*Check mono_nat_mono_timeless.*)
 
 Section mono_derived.
 (** In addition to the known [heapGS] assumption, we now also need to assume that the ghost state for the theory of mono_nat has been registered with Iris, expressed through the [mono_natG] assumption.
@@ -89,7 +88,7 @@ Section mono_derived.
   Lemma mono_nat_new_wp e Φ n :
     (∀ γ, mono γ n -∗ WP e {{ Φ }}) -∗ WP e {{ Φ }}.
   Proof.
-    (* FIXME exercise *)
+    (* FIXME: exercise *)
   Admitted.
 End mono_derived.
 
@@ -189,20 +188,21 @@ Section logrel_symbol.
   Qed.
 End logrel_symbol.
 
+
 (** Exercise: Oneshot *)
 Section logrel_oneshot.
   Import logrel.notation syntactic logrel.
   Context `{heapGS Σ} `{oneshotG Σ nat}.
 
 
-  Check os_pending_alloc.
-  Check os_pending_shoot.
-  Check os_shot_persistent.
-  Check os_pending_shot_False.
-  Check os_pending_pending_False.
-  Check os_shot_agree.
-  Check os_shot_timeless.
-  Check os_pending_timeless.
+  (*Check os_pending_alloc.*)
+  (*Check os_pending_shoot.*)
+  (*Check os_shot_persistent.*)
+  (*Check os_pending_shot_False.*)
+  (*Check os_pending_pending_False.*)
+  (*Check os_shot_agree.*)
+  (*Check os_shot_timeless.*)
+  (*Check os_pending_timeless.*)
 
   Definition code : expr :=
     let: "x" := ref #42 in
@@ -225,10 +225,10 @@ Section logrel_ag.
   Import logrel.notation syntactic logrel.
   Context `{heapGS Σ} `{halvesG Σ Z}.
 
-  Check ghalves_alloc.
-  Check ghalves_agree.
-  Check ghalves_update.
-  Check ghalf_timeless.
+  (*Check ghalves_alloc.*)
+  (*Check ghalves_agree.*)
+  (*Check ghalves_update.*)
+  (*Check ghalf_timeless.*)
 
   Definition rec_code : expr :=
     λ: "f",
@@ -251,20 +251,24 @@ Section logrel_ag.
 End logrel_ag.
 
 (** Exercise: Red/blue *)
-
 Section logrel_redblue.
   Import logrel.notation syntactic logrel.
   Inductive colour := red | blue.
 
   Context `{heapGS Σ} `{agmapG Σ nat colour}.
 
-  Check agmap_auth_alloc_empty.
-  Check agmap_auth_insert.
-  Check agmap_auth_lookup.
-  Check agmap_elem_agree.
-  Check agmap_elem_persistent.
-  Check agmap_elem_timeless.
-  Check agmap_auth_timeless.
+  (*Check agmap_auth_alloc_empty.*)
+  (*Check agmap_auth_insert.*)
+  (*Check agmap_auth_lookup.*)
+  (*Check agmap_elem_agree.*)
+  (*Check agmap_elem_persistent.*)
+  (*Check agmap_elem_timeless.*)
+  (*Check agmap_auth_timeless.*)
+
+  Definition redT γ : semtypeO :=
+    mk_semtype (λ v, ∃ n : nat, ⌜v = #n⌝ ∗ agmap_elem γ n red)%I.
+  Definition blueT γ : semtypeO :=
+    mk_semtype (λ v, ∃ n : nat, ⌜v = #n⌝ ∗ agmap_elem γ n blue)%I.
 
   Definition mkColourGen : expr :=
     let: "c" := ref #0 in
@@ -275,6 +279,6 @@ Section logrel_redblue.
   Lemma mkColourGen_safe :
     TY 0; ∅ ⊨ mkColourGen : (∃: ∃: ((TUnit → #0) × (TUnit → #1)) × (#0 → #1 → TUnit)).
   Proof.
-    (* FIXME exercise *)
+    (* FIXME: exercise *)
   Admitted.
 End logrel_redblue.
diff --git a/theories/program_logics/program_logic/adequacy.v b/theories/program_logics/program_logic/adequacy.v
index 181524e..7a47f65 100644
--- a/theories/program_logics/program_logic/adequacy.v
+++ b/theories/program_logics/program_logic/adequacy.v
@@ -145,7 +145,8 @@ Theorem wp_strong_adequacy Σ Λ `{!invGpreS Σ} e σ1 n κs t2 σ2 φ :
   φ.
 Proof.
   intros Hwp ?.
-  apply (step_fupdN_soundness_no_lc _ n)=> Hinv Hlc.
+  apply (step_fupdN_soundness_no_lc _ n 0)=> Hinv Hlc.
+  iIntros "_".
   iMod Hwp as (s stateI Φ) "(Hσ & Hwp & Hφ)".
   rewrite /wp swp_eq /swp_def. iMod "Hwp".
   iMod (@wptp_strong_adequacy _ _ (IrisG _ _ Hinv stateI) _ [_]
diff --git a/theories/program_logics/reloc/src_rules.v b/theories/program_logics/reloc/src_rules.v
index 2ba26f1..8d4698b 100644
--- a/theories/program_logics/reloc/src_rules.v
+++ b/theories/program_logics/reloc/src_rules.v
@@ -57,14 +57,14 @@ Definition srcN := relocN .@ "src".
 Definition logN := relocN .@ "log".
 
 (** Interaction lemmas for the ghost theories *)
-Check pointstoS_agree.
-Check heapS_lookup.
-Check heapS_insert.
-Check heapS_update.
-Check heapS_delete.
-
-Check exprS_agree.
-Check exprS_update.
+(*Check pointstoS_agree.*)
+(*Check heapS_lookup.*)
+(*Check heapS_insert.*)
+(*Check heapS_update.*)
+(*Check heapS_delete.*)
+
+(*Check exprS_agree.*)
+(*Check exprS_update.*)
 
 (** Note that relocGS fixes the two ghost names for [exprS] and [heapS] *)
 
diff --git a/theories/program_logics/resource_algebras.v b/theories/program_logics/resource_algebras.v
index 796f275..ad9f4d5 100644
--- a/theories/program_logics/resource_algebras.v
+++ b/theories/program_logics/resource_algebras.v
@@ -13,21 +13,26 @@ From iris.prelude Require Import options.
 
 (* Allocation ResAlloc *)
 (* Note that we use the symbol ✓ for validity *)
-Check own_alloc.
+(*Check own_alloc.*)
+
 (* Interaction with separating conjunction, ResSep *)
-Check own_op.
+(*Check own_op.*)
+
 (* The core is persistent, ResPers *)
 (* (this is formulated slightly differently here: [CoreId a] says that [a] is its own core) *)
-Check own_core_persistent.
+(*Check own_core_persistent.*)
+
 (* Resources are valid, ResValid *)
-Check own_valid.
+(*Check own_valid.*)
+
 (* Frame-preserving updates, ResUpd *)
-Check own_update.
+(*Check own_update.*)
 
 (* [own] is monotonous wrt inclusion *)
-Check own_mono.
+(*Check own_mono.*)
+
 (* We can always own a unit *)
-Check own_unit.
+(*Check own_unit.*)
 
 (** Some notes on the setup in Coq:
   1. The `inG` assumptions you see for these lemmas above require that the given algebra has been registered with Iris, similar to the `mono_natG Σ` assumption you have already seen. We will discuss this later in more detail.
@@ -60,10 +65,10 @@ Check own_unit.
 
   In addition, it carries a proof that these operations satisfy the necessary laws [LRAMixin].
  *)
-Print lra.
+(*Print lra.*)
 
 (** The required laws: this matches what you can find in the lecture notes. *)
-Print LRAMixin.
+(*Print LRAMixin.*)
 
 (** We require a few additional operations:
   - [lra_included] defines the inclusion [≼]
@@ -71,11 +76,11 @@ Print LRAMixin.
    Here [⋅?] lifts the operation [⋅] to optional right-hand sides: [opMLRA].
   - [lra_exclusive] defines what it means for an element to be exclusive (i.e., not compose with any frame).
  *)
-Print lra_included.
-Print lra_update.
-Print lra_local_update.
-Print opMLRA.
-Print lra_exclusive.
+(*Print lra_included.*)
+(*Print lra_update.*)
+(*Print lra_local_update.*)
+(*Print opMLRA.*)
+(*Print lra_exclusive.*)
 
 (** We prove some derived lemmas *)
 
@@ -144,9 +149,10 @@ Qed.
 
 (** In addition, we need a notion of unital RAs (i.e., RAs with a unit). *)
 (** In addition to [lra]s, they need to have a unit [ε] (type \varepsilon). *)
-Print ulra.
+(*Print ulra.*)
+
 (** The unit needs to satisfy the following laws: *)
-Print ULRAMixin.
+(*Print ULRAMixin.*)
 
 (** Unit: derived laws *)
 Global Instance ulra_unit_right_id {A : ulra} : RightId (=) ε (@op A _).
-- 
GitLab