feat: lazy coin example

Iris/Iris/HeapLang/Lib/LazyCoin.lean

@@ -0,0 +1,107 @@
+module
+
+public import Iris.HeapLang
+public import Iris.BI
+public import Iris.HeapLang.Lib.NondetBool
+
+namespace Iris.HeapLang
+
+-- type Coin := Ref (Option Bool) × ProphId
+def newCoin := hl_val%
+  λ _, (ref(none()), newProph())
+
+-- readCoin(cp : Coin) : Bool
+def readCoin := hl_val%
+  λ cp,
+    let c := fst(cp);
+    let p := snd(cp);
+    match !c with
+    | none() => -- The prophecy hasn't been resolved yet
+      let r := &nondetBool #();
+      c ← some(r);
+      resolveProph(p, r);
+      r
+    | some(v) => -- The prophecy has been resolved already
+      v
+
+variable {hlc GF} [HeapLangGS hlc GF]
+
+section Proofs
+
+open HeapLang
+
+def prophecyToBool (vs : List (Val × Val)) : Bool :=
+  if let some (_, v) := vs.head? then
+    v = hl_val(#true)
+  else false
+
+@[simp, grind =]
+theorem prophecyToBool_of_bool (vs : List (Val × Val)) (v : Val) (b : Bool) :
+    prophecyToBool ((v, hl_val(#b)) :: vs) = b := by
+  cases b <;> rfl
+
+/-- `cp` is a pair of `c` and `p`, where if p is a prophecy with resolutions `vs`
+    such that if `c` is non-null, it points to the first resolution value of  `vs` -/
+def coin (cp : Val) (b : Bool) : IProp GF := iprop%
+  ∃ (c : Loc) (p : ProphId) (vs : List (Val × Val)),
+  ⌜ cp = hl_val((#c, #p)) ⌝ ∗ proph p vs ∗
+  (c ↦ hl_val(some(#b)) ∨ (c ↦ hl_val(none()) ∗ ⌜ b = prophecyToBool vs ⌝))
+
+theorem newCoin.spec : ⊢@{IProp GF}
+    {{ True }} hl(&newCoin #()) {{ c b, RET c; coin c b }} := by
+  iintro %Φ - K
+  unfold newCoin
+  wp_pures
+  wp_bind newProph()
+  ihave ∗aux := wp_new_proph
+  iapply wp_strong_mono (Std.IsPreorder.le_refl _) CoPset.subseteq_refl $$ aux
+  iintro %v ⟨%p, %pvs, %eq, h⟩ !>; subst eq
+  wp_pures
+  wp_bind ref(_)
+  iapply wp_alloc
+  iintro %l !> Hl
+  wp_pures
+  iintro !>
+  iapply K
+  unfold coin
+  iexists l, p, pvs
+  isplitl []; itrivial
+  iframe
+  iright
+  iframe
+  ipureintro
+  rfl
+
+theorem readCoin.spec (cp : Val) (b : Bool) : ⊢@{IProp GF}
+    {{ coin cp b }} hl(&readCoin &cp) {{ RET hl_val(#b); coin cp b }} := by
+  conv => enter [1,1]; unfold coin
+  iintro %Φ ⟨%c, %p, %pvs, %cp_eq, proph, disj⟩ K
+  unfold readCoin
+  subst cp_eq
+  wp_pures
+  wp_bind !_
+  icases disj with (Hsome | ⟨Hnone, %b_eq⟩)
+  · iapply wp_load $$ Hsome
+    iintro !> Hc
+    wp_pures
+    iintro !>
+    iapply K
+    iexists c, p, pvs
+    iframe; ipureintro; rfl
+  · subst b_eq
+    iapply wp_load $$ Hnone
+    iintro !> Hc
+    wp_pures
+    wp_bind &nondetBool _; iapply nondetBool.spec $$ [//]; iintro !> %b -
+    wp_pures
+    wp_bind _ ← _; iapply wp_store $$ Hc; iintro !> Hc
+    wp_pure; wp_pure
+    wp_bind resolveProph(_, _); iapply wp_resolve_proph $$ proph
+    iintro %pvs' %pvs_eq proph
+    subst pvs_eq
+    wp_pures
+    iintro !>
+    simp only [prophecyToBool_of_bool]
+    iapply K
+    iexists c, p, pvs'
+    iframe; ipureintro; rfl

Iris/Iris/HeapLang/Lib/NondetBool.lean

@@ -0,0 +1,56 @@
+module
+
+public import Iris.ProgramLogic.WeakestPre
+public import Iris.HeapLang.ProofMode
+public import Iris.HeapLang.PrimitiveLaws
+public import Iris.Instances.Lib.Invariants
+
+namespace Iris.HeapLang
+
+public section
+
+variable [HeapLangGS hlc GF]
+
+def nondetBool := hl_val% λ _,
+    let l := ref(#true);
+    fork(
+      l ← #false
+    );
+    !l
+
+theorem nondetBool.spec : ⊢@{IProp GF}
+    {{ True }} hl(&nondetBool #()) {{ (b : Bool), RET hl_val(#b); True }} := by
+  iintro %Φ - K
+  unfold nondetBool
+  wp_pures
+  wp_bind ref(_)
+  iapply wp_alloc
+  iintro %l !> Hl
+  wp_pures
+  iapply fupd_wp
+  ihave >#inv := inv_alloc `rnd ⊤ iprop(∃ (b : Bool), l ↦ hl_val(#b)) $$ [Hl]
+  · iexists ?_; iassumption
+  iintro !>
+  wp_bind fork(_)
+  iapply wp_fork $$ [K] []
+  · inext
+    wp_pures
+    iapply wp_atomic
+    ihave >⟨⟨%b, Hl⟩, Hclose⟩ := inv_acc CoPset.subseteq_top $$ inv
+    iintro !>
+    iapply wp_load $$ Hl
+    iintro !> Hl
+    ihave aux :=  Hclose $$ [Hl]
+    · iexists ?_; iassumption
+    icases aux with >-
+    iintro !>
+    iapply K $$ [//]
+  · inext
+    iapply wp_atomic
+    ihave >⟨⟨%b, Hl⟩, Hclose⟩ := inv_acc CoPset.subseteq_top $$ inv
+    iintro !>
+    iapply wp_store $$ Hl
+    iintro !> Hl
+    iapply Hclose
+    iexists ?_
+    iassumption

Iris/Iris/HeapLang/PrimitiveLaws.lean

@@ -605,7 +605,7 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val ×
     iapply HΦ $$ %pvs'' %hpvs'_eq Hele
 
 theorem wp_resolve {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)}
-    (hatom : Language.Atomic Language.Atomicity.StronglyAtomic e) (hne : toVal e = none) :
+    (hatom : Language.Atomic Language.Atomicity.StronglyAtomic e) (hne : toVal e = none := by decide) :
     proph p pvs -∗
     WP e @ s; E {{ r, ∀ pvs', ⌜pvs = (r, w) :: pvs'⌝ -∗ proph p pvs' -∗ Φ r }} -∗
     WP hl(resolve(&e, v(#p), v(&w))) @ s; E {{ Φ }} := by
@@ -618,6 +618,34 @@ theorem wp_resolve {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)}
   iframe Hp
   iexact Hcont
 
+theorem wp_resolve_proph {p : ProphId} {w : Val} {pvs : List (Val × Val)} :
+    proph p pvs -∗
+    (∀ pvs', ⌜pvs = (hl_val(#()), w) :: pvs'⌝ -∗ proph p pvs' -∗ Φ hl_val(#())) -∗
+    WP hl(resolveProph(v(#p), v(&w))) @ s; E {{ Φ }} := by
+  iintro proph K
+  let Ki := ECtxItem.resolveL (ECtxItem.appL hl_val(#())) hl_val(#p) hl_val(&w)
+  have shape: hl(resolveProph(#p ,&w)) = fill (Expr := Exp) [Ki] hl(λ _, #()) := by
+    simp [fillItem, Ki, ECtxItem.fill]
+  rw [shape]
+  iapply wp_bind
+  iapply wp_pure_step_fupd (Hφ := ⟨⟩)
+  simp only [Nat.repeat, EctxItemLanguage.fill_cons, fillItem, ECtxItem.fill, EctxItemLanguage.fill_nil, wp_value_iff, Ki]
+  iintro !> !> !> _ !>
+  have hatom : Language.Atomic Language.Atomicity.StronglyAtomic hl((v(λ _, #())) #()) := by
+    constructor
+    intro σ _ _ _ _ h
+    apply prim_step_to_val_always_to_val (κsₐ := []) (σ₁ₐ := σ) ?next h
+    case next =>
+      apply ProgramLogic.EctxLanguage.primStep_of_baseStep
+      simp only [BaseStep.baseStep, val_to_ofVal]
+      constructor
+      rfl
+  iapply wp_resolve hatom (hne := by decide) $$ proph
+  iapply wp_rec rfl
+  simp only [Exp.subst, wp_value_iff]
+  iintro !> !>
+  iassumption
+
 end Lifting
 
 end Iris.HeapLang

Iris/Iris/Std/CoPset.lean

@@ -371,6 +371,8 @@ theorem not_in_union {p} {X1 X2 : CoPset} : ¬ p ∈ X1 ∪ X2 <-> ¬ p ∈ X1 
   · exact ⟨(Hu <| in_union.mpr <| .inl ·), (Hu <| in_union.mpr <| .inr ·)⟩
   · exact in_union.mp Hu |>.elim H1 H2
 
+@[refl] theorem subseteq_refl {X : CoPset} : X ⊆ X := λ _ => id
+
 theorem subseteq_trans {X Y Z : CoPset} (Hxy : X ⊆ Y) (Hyz : Y ⊆ Z) : X ⊆ Z :=
   fun p => (Hyz p) ∘ (Hxy p)