ReactorJet/Coq-Iris huggingface dataset:
(* iris_heap_lang/lib/lazy_coin.v *)
From iris.base_logic Require Export invariants
From iris.program_logic Require Export weakestpre
From iris.heap_lang Require Export lang proofmode notation
From iris.heap_lang.lib Require Export nondet_bool
From iris.prelude Require Import options

Definition new_coin: val := λ: <>, (ref NONE, NewProph).

Definition read_coin: val :=
  λ: "cp",
  let: "c" := Fst "cp" in
  let: "p" := Snd "cp" in
  match: !"c" with
    NONE => let: "r" := nondet_bool #() in
           "c" <- SOME "r";; resolve_proph: "p" to: "r";; "r"
  | SOME "b" => "b"
  end.

Definition val_to_bool(v : val) : bool := bool_decide (v = #true).

Definition prophecy_to_bool(vs : list (val * val)) : bool :=
    default false (val_to_bool ∘ snd <$> head vs).

Lemma prophecy_to_bool_of_bool(b : bool) v vs :
    prophecy_to_bool ((v, #b) :: vs) = b.
  Proof. by destruct b. Qed.

Definition coin(cp : val) (b : bool) : iProp Σ :=
    ∃ (c : loc) (p : proph_id) (vs : list (val * val)),
       ⌜cp = (#c, #p)%V⌝ ∗ proph p vs ∗
       (c ↦ SOMEV #b ∨ (c ↦ NONEV ∗ ⌜b = prophecy_to_bool vs⌝)).

Lemma new_coin_spec: {{{ True }}} new_coin #() {{{ c b, RET c; coin c b }}}.
  Proof.
    iIntros (Φ) "_ HΦ".
    wp_lam.
    wp_apply wp_new_proph; first done.
    iIntros (vs p) "Hp".
    wp_alloc c as "Hc".
    wp_pair.
    iApply ("HΦ" $! (#c, #p)%V ).
    rewrite /coin; eauto 10 with iFrame.
  Qed.

Lemma read_coin_speccp b :
    {{{ coin cp b }}} read_coin cp {{{ RET #b; coin cp b }}}.
  Proof.
    iIntros (Φ) "Hc HΦ".
    iDestruct "Hc" as (c p vs ->) "[Hp [Hc | [Hc ->]]]".
    - wp_lam. wp_load. wp_match.
      iApply "HΦ".
      rewrite /coin; eauto 10 with iFrame.
    - wp_lam. wp_load. wp_match.
      wp_apply nondet_bool_spec; first done.
      iIntros (r) "_".
      wp_let.
      wp_store.
      wp_apply (wp_resolve_proph with "[Hp]"); first done.
      iIntros (ws) "[-> Hws]".
      rewrite !prophecy_to_bool_of_bool.
      wp_seq.
      iApply "HΦ".
      rewrite /coin; eauto 10 with iFrame.
  Qed.
(* iris_heap_lang/lib/lock.v *)
From iris.base_logic.lib Require Export invariants
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

Class lock:= Lock {

Global Argumentsnewlock : simpl never.

Global Argumentsacquire : simpl never.

Global Argumentsrelease : simpl never.

Global Argumentsis_lock : simpl never.

Global Argumentslocked : simpl never.
Existing Class lockG.

Global HintMode lockG + + : typeclass_instances.

Global HintExtern 0 (lockG _) => progress simpl : typeclass_instances.

Global Instanceis_lock_contractive `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk :
  Contractive (is_lock γ lk).
Proof.
  apply (contractive_internal_eq (PROP:=iPropI Σ)).
  iIntros (P Q) "#HPQ". iApply prop_ext. iIntros "!>".
  iSplit; iIntros "H"; iApply (is_lock_iff with "H");
    iNext; iRewrite "HPQ"; auto.
Qed.

Global Instanceis_lock_proper `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk :
  Proper ((≡) ==> (≡)) (is_lock γ lk) := ne_proper _.

Lemma newlock_spec(R : iProp Σ) :
    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
  Proof.
    iIntros (Φ) "HR HΦ".
    iApply wp_fupd.
    wp_apply newlock_spec_delay_init; first done.
    iIntros (lk γ) "Hlk". iApply "HΦ".
    by iMod ("Hlk" $! R ⊤ with "HR").
  Qed.
(* iris_heap_lang/lib/logatom_lock.v *)
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Import ghost_var
From iris.program_logic Require Export atomic
From iris.heap_lang Require Import proofmode notation atomic_heap lock
From iris.prelude Require Import options

Inductive state:= Free | Locked.

Class alockGΣ := LockG { #[local] lock_tokG :: ghost_varG Σ state }.

Definition alockΣ: gFunctors := #[ghost_varΣ state].

Global InstancesubG_alockΣ {Σ} : subG alockΣ Σ → alockG Σ.
Proof. solve_inG. Qed.

Record tada_lock_name:= TadaLockName {
    tada_lock_name_state : gname;
    tada_lock_name_lock : lock_name;
  }.

Definition tada_lock_state(γ : tada_lock_name) (s : state) : iProp Σ :=
    ghost_var γ.(tada_lock_name_state) (3/4) s ∗
    if s is Locked then
      locked γ.(tada_lock_name_lock) ∗ ghost_var γ.(tada_lock_name_state) (1/4) Locked
    else True.

Definition tada_is_lock(γ : tada_lock_name) (lk : val) : iProp Σ :=
    is_lock γ.(tada_lock_name_lock) lk
      (ghost_var γ.(tada_lock_name_state) (1/4) Free).

Global Instancetada_is_lock_persistent γ lk : Persistent (tada_is_lock γ lk).
  Proof. apply _. Qed.

Global Instancetada_lock_state_timeless γ s : Timeless (tada_lock_state γ s).
  Proof. destruct s; apply _. Qed.

Lemma tada_lock_state_exclusiveγ s1 s2 :
    tada_lock_state γ s1 -∗ tada_lock_state γ s2 -∗ False.
  Proof.
    iIntros "[Hvar1 _] [Hvar2 _]".
    iCombine "Hvar1 Hvar2" gives %[Hval _].
    exfalso. done.
  Qed.

Lemma newlock_tada_spec:
    {{{ True }}}
      newlock #()
    {{{ lk γ, RET lk; tada_is_lock γ lk ∗ tada_lock_state γ Free }}}.
  Proof.
    iIntros (Φ) "_ HΦ".
    iMod (ghost_var_alloc Free) as (γvar) "Hvar".
    replace 1%Qp with (3/4 + 1/4)%Qp; last first.
    { rewrite Qp.three_quarter_quarter //. }
    iDestruct "Hvar" as "[Hvar1 Hvar2]".
    wp_apply (newlock_spec with "Hvar2") as (lk γlock) "Hlock".
    iApply ("HΦ" $! lk (TadaLockName _ _)).
    iFrame.
  Qed.

Lemma acquire_tada_specγ lk :
    tada_is_lock γ lk -∗
    <<{ ∀∀ s, tada_lock_state γ s }>>
      acquire lk @ ∅
    <<{ ⌜ s = Free ⌝ ∗ tada_lock_state γ Locked | RET #() }>>.
  Proof.
    iIntros "#Hislock %Φ AU". iApply wp_fupd.
    wp_apply (acquire_spec with "Hislock") as "[Hlocked Hvar1]".
    iMod "AU" as (s) "[[Hvar2 _] [_ Hclose]]".
    iCombine "Hvar1 Hvar2" gives %[_ <-].
    iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
    { rewrite Qp.quarter_three_quarter //. }
    iMod ("Hclose" with "[$Hvar2 $Hlocked $Hvar1]"); done.
  Qed.

Lemma release_tada_specγ lk :
    tada_is_lock γ lk -∗
    <<{ tada_lock_state γ Locked }>>
      release lk @ ∅
    <<{ tada_lock_state γ Free | RET #() }>>.
  Proof.
    iIntros "#Hislock %Φ AU". iApply fupd_wp.
    iMod "AU" as "[[Hvar1 [Hlocked Hvar2]] [_ Hclose]]".
    iMod (ghost_var_update_2 Free with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
    { rewrite Qp.three_quarter_quarter //. }
    iMod ("Hclose" with "[$Hvar1]"). iModIntro.
    wp_apply (release_spec with "[$Hislock $Hlocked $Hvar2]").
    auto.
  Qed.

Global TypeclassesOpaque tada_is_lock tada_lock_state.
(* iris_heap_lang/lib/nondet_bool.v *)
From iris.base_logic Require Export invariants
From iris.program_logic Require Export weakestpre
From iris.heap_lang Require Export lang proofmode notation
From iris.prelude Require Import options

Definition nondet_bool: val :=
  λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l".

Lemma nondet_bool_spec: {{{ True }}} nondet_bool #() {{{ (b : bool), RET #b; True }}}.
  Proof.
    iIntros (Φ) "_ HΦ".
    wp_lam. wp_alloc l as "Hl". wp_let.
    pose proof (nroot .@ "rnd") as rndN.
    iMod (inv_alloc rndN _ (∃ (b : bool), l ↦ #b)%I with "[Hl]") as "#Hinv";
      first by eauto.
    wp_apply wp_fork.
    - iInv rndN as (?) "?". wp_store; eauto.
    - wp_seq. iInv rndN as (?) "?". wp_load.
      iSplitR "HΦ"; first by eauto.
      by iApply "HΦ".
  Qed.
(* iris_heap_lang/lib/par.v *)
From iris.heap_lang Require Import proofmode notation
From iris.heap_lang Require Export spawn
From iris.prelude Require Import options

Definition parN: namespace := nroot .@ "par".

Definition par: val :=
  λ: "e1" "e2",
    let: "handle" := spawn "e1" in
    let: "v2" := "e2" #() in
    let: "v1" := join "handle" in
    ("v1", "v2").

Local SetDefault Proof Using "Type*".
Context `{!heapGS_gen hlc Σ, !spawnG Σ}.

Lemma par_spec(Ψ1 Ψ2 : val → iProp Σ) (f1 f2 : val) (Φ : val → iProp Σ) :
  WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗
  (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
  WP par f1 f2 {{ Φ }}.
Proof.
  iIntros "Hf1 Hf2 HΦ". wp_lam. wp_let.
  wp_apply (spawn_spec parN with "Hf1") as (l) "Hl".
  wp_let. wp_bind (f2 _).
  wp_apply (wp_wand with "Hf2") as (v) "H2". wp_let.
  wp_apply (join_spec with "[$Hl]") as (w) "H1".
  iSpecialize ("HΦ" with "[$H1 $H2]"). by wp_pures.
Qed.

Lemma wp_par(Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
  WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
  (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
  WP (e1 ||| e2)%V {{ Φ }}.
Proof.
  iIntros "H1 H2 H".
  wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
Qed.
(* iris_heap_lang/lib/rw_lock.v *)
From iris.base_logic.lib Require Export invariants
From iris.bi.lib Require Export fractional
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

Class rwlock:= RwLock {

Global Argumentsnewlock : simpl never.

Global Argumentsacquire_reader : simpl never.

Global Argumentsrelease_reader : simpl never.

Global Argumentsacquire_writer : simpl never.

Global Argumentsrelease_writer : simpl never.

Global Argumentsis_rw_lock : simpl never.

Global Argumentsreader_locked : simpl never.

Global Argumentswriter_locked : simpl never.
Existing Class rwlockG.

Global HintMode rwlockG + + : typeclass_instances.

Global HintExtern 0 (rwlockG _) => progress simpl : typeclass_instances.

Global Instanceis_rw_lock_contractive `{!heapGS_gen hlc Σ, !rwlock, !rwlockG Σ} γ lk n :
  Proper (pointwise_relation _ (dist_later n) ==> dist n) (is_rw_lock γ lk).
Proof.
  assert (Contractive (is_rw_lock γ lk : (Qp -d> iPropO Σ) → _)) as Hcontr.
  { apply (contractive_internal_eq (PROP:=iPropI Σ)); iIntros (Φ1 Φ2) "#HΦ".
    rewrite discrete_fun_equivI.
    iApply prop_ext_2; iIntros "!>"; iSplit; iIntros "H";
      iApply (is_rw_lock_iff with "H");
      iIntros "!> !>" (q); iRewrite ("HΦ" $! q); auto. }
  intros Φ1 Φ2 HΦ. apply Hcontr. dist_later_intro. apply HΦ.
Qed.

Global Instanceis_rw_lock_proper `{!heapGS_gen hlc Σ, !rwlock, !rwlockG Σ} γ lk :
  Proper (pointwise_relation _ (≡) ==> (≡)) (is_rw_lock γ lk).
Proof.
  intros Φ1 Φ2 HΦ. apply equiv_dist=> n. apply is_rw_lock_contractive=> q.
  dist_later_intro. apply equiv_dist, HΦ.
Qed.
(* iris_heap_lang/lib/spawn.v *)
From iris.algebra Require Import excl
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Export invariants
From iris.program_logic Require Export weakestpre
From iris.heap_lang Require Export lang
From iris.heap_lang Require Import proofmode notation
From iris.prelude Require Import options

Definition spawn: val :=
  λ: "f",
    let: "c" := ref NONE in
    Fork ("c" <- SOME ("f" #())) ;; "c".

Definition join: val :=
  rec: "join" "c" :=
    match: !"c" with
      SOME "x" => "x"
    | NONE => "join" "c"
    end.

Class spawnGΣ := SpawnG { #[local] spawn_tokG :: inG Σ (exclR unitO) }.

Definition spawnΣ: gFunctors := #[GFunctor (exclR unitO)].

Global InstancesubG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
Proof. solve_inG. Qed.

Definition spawn_inv(γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
  ∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌝ ∨
                  ∃ w, ⌜lv = SOMEV w⌝ ∗ (Ψ w ∨ own γ (Excl ()))).

Definition join_handle(l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
  ∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ).

Global Instancespawn_inv_ne n γ l :
  Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
Proof. solve_proper. Qed.

Global Instancejoin_handle_ne n l :
  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle l).
Proof. solve_proper. Qed.

Lemma spawn_spec(Ψ : val → iProp Σ) (f : val) :
  {{{ WP f #() {{ Ψ }} }}} spawn f {{{ l, RET #l; join_handle l Ψ }}}.
Proof.
  iIntros (Φ) "Hf HΦ". rewrite /spawn /=. wp_lam.
  wp_alloc l as "Hl".
  iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
  iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
  { iNext. iExists NONEV. iFrame; eauto. }
  wp_smart_apply (wp_fork with "[Hf]").
  - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
    wp_inj. iInv N as (v') "[Hl _]".
    wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
  - wp_pures. iApply "HΦ". rewrite /join_handle. eauto.
Qed.

Lemma join_spec(Ψ : val → iProp Σ) l :
  {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
Proof.
  iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
  iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]".
  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
  - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
    wp_smart_apply ("IH" with "Hγ [HΦ]"). auto.
  - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
    + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
      wp_pures. by iApply "HΦ".
    + iCombine "Hγ Hγ'" gives %[].
Qed.

Global TypeclassesOpaque join_handle.
(* iris_unstable/bi/algebra.v *)
From iris.algebra Require Import cmra
From iris.unstable.algebra Require Import list
From iris.bi Require Import algebra
From iris.prelude Require Import options

Lemma list_validIl : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
    Proof. sbi_unfold=> n. apply list_lookup_validN. Qed.