ReactorJet/Coq-Iris huggingface dataset:
(* iris/proofmode/string_ident.v *)
From Ltac2 Require Ltac2
From Stdlib Require Import Strings.String
From Stdlib Require Import Init.Byte Ascii
From iris.prelude Require Import options

Local OpenScope list.

Ltac2 Typeexn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ].

Ltac2 coq_byte_to_int(b : constr) : int :=
    match! b with

Ltac2 coq_byte_to_char(b : constr) : char :=
    Char.of_int (coq_byte_to_int b).

Fixpoint coq_string_to_list_byte(s : string) : list byte :=
    match s with
    | EmptyString => []
    | String c s => Ascii.byte_of_ascii c :: coq_string_to_list_byte s
    end.

Ltac2 reccoq_byte_list_blit_list (pos : int) (ls : constr) (str : string) : unit :=
    match! ls with
    | nil => ()
    | ?c :: ?ls =>
      let b := coq_byte_to_char c in
      String.set str pos b; coq_byte_list_blit_list (Int.add pos 1) ls str
    end.

Ltac2 reccoq_string_length (s : constr) : int :=
    match! s with
    | EmptyString => 0
    | String _ ?s' => Int.add 1 (coq_string_length s')
    | _ => Control.throw (NotStringLiteral s)
    end.

Ltac2 compute(c : constr) : constr :=
    Std.eval_vm None c.

Ltac2 coq_string_to_string(s : constr) : string :=
    let l := coq_string_length s in
    let str := String.make l (Char.of_int 0) in
    let bytes := compute constr:(coq_string_to_list_byte $s) in
    let _ := coq_byte_list_blit_list 0 bytes str in
    str.

Ltac2 string_to_ident(s : string) : ident :=
    match Ident.of_string s with
    | Some id => id
    | None => Control.throw (InvalidIdent s)
    end.

Ltac2 coq_string_to_ident(s : constr) : ident :=
    string_to_ident (coq_string_to_string s).

Ltac string_to_ident_cps:=
    ltac2:(s1 r |- let s := Option.get (Ltac1.to_constr s1) in
                   let ident := coq_string_to_ident s in
                   Ltac1.apply r [Ltac1.of_ident ident] Ltac1.run).

Ltac2 get_bit(n : int) (i : int) : bool :=
    Int.equal (Int.land (Int.lsr n i) 1) 1.

Ltac2 get_bit_coq_bool(n : int) (i : int) : constr :=
    if get_bit n i then constr:(true) else constr:(false).

Ltac2 char_to_coq_ascii(c : char) : constr :=
    let i := Char.to_int c in
    let bs := Array.init 8 (get_bit_coq_bool i) in
    Constr.Unsafe.make (Constr.Unsafe.App constr:(Ascii) bs).

Ltac2 string_to_coq_string(s : string) : constr :=
    let len := String.length s in
    let rec to_string i :=
      if Int.equal i len then constr:(EmptyString) else
        let tail := to_string (Int.add i 1) in
        let head := char_to_coq_ascii (String.get s i) in
        constr:(String $head $tail)
    in
    to_string 0.

Ltac2 ident_to_string(id : ident) : constr :=
    string_to_coq_string (Ident.to_string id).

Ltac ident_to_string_cps:=
    ltac2:(id r |- let id := Option.get (Ltac1.to_ident id) in
                   let s := ident_to_string id in
                   Ltac1.apply r [Ltac1.of_constr s] Ltac1.run).

Ltac rename_by_stringid s :=
  StringToIdent.string_to_ident_cps s ltac:(fun x => rename id into x).

Ltac string_to_ident_cps:= StringToIdent.string_to_ident_cps.

Ltac ident_to_string_cps:= IdentToString.ident_to_string_cps.
(* iris/proofmode/tokens.v *)
From iris.proofmode Require Import base
From iris.prelude Require Import options

Inductive token:=
  | TName : string → token
  | TNat : nat → token
  | TAnon : token
  | TFrame : token
  | TBar : token
  | TBracketL : token
  | TBracketR : token
  | TAmp : token
  | TParenL : token
  | TParenR : token
  | TBraceL : token
  | TBraceR : token
  | TPure : option string → token
  | TIntuitionistic : token
  | TModal : token
  | TPureIntro : token
  | TIntuitionisticIntro : token
  | TModalIntro : token
  | TSimpl : token
  | TDone : token
  | TForall : token
  | TAll : token
  | TMinus : token
  | TSep : token
  | TArrow : direction → token.

Inductive state:=
  | SName : string → state
  | SNat : nat → state
  | SPure : string -> state
  | SNone : state.

Definition cons_state(kn : state) (k : list token) : list token :=
  match kn with
  | SNone => k
  | SName s => TName (String.rev s) :: k
  | SPure s => TPure (if String.eqb s "" then None else Some (String.rev s)) :: k
  | SNat n => TNat n :: k
  end.

Fixpoint tokenize_go(s : string) (k : list token) (kn : state) : list token :=
  match s with
  | "" => reverse (cons_state kn k)
  | String "?" s => tokenize_go s (TAnon :: cons_state kn k) SNone
  | String "$" s => tokenize_go s (TFrame :: cons_state kn k) SNone
  | String "[" s => tokenize_go s (TBracketL :: cons_state kn k) SNone
  | String "]" s => tokenize_go s (TBracketR :: cons_state kn k) SNone
  | String "|" s => tokenize_go s (TBar :: cons_state kn k) SNone
  | String "(" s => tokenize_go s (TParenL :: cons_state kn k) SNone
  | String ")" s => tokenize_go s (TParenR :: cons_state kn k) SNone
  | String "&" s => tokenize_go s (TAmp :: cons_state kn k) SNone
  | String "{" s => tokenize_go s (TBraceL :: cons_state kn k) SNone
  | String "}" s => tokenize_go s (TBraceR :: cons_state kn k) SNone
  | String "%" s => tokenize_go s (cons_state kn k) (SPure "")
  | String "#" s => tokenize_go s (TIntuitionistic :: cons_state kn k) SNone
  | String ">" s => tokenize_go s (TModal :: cons_state kn k) SNone
  | String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_state kn k) SNone
  | String "!" (String "#" s) => tokenize_go s (TIntuitionisticIntro :: cons_state kn k) SNone
  | String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_state kn k) SNone
  | String "/" (String "/" (String "=" s)) =>
     tokenize_go s (TSimpl :: TDone :: cons_state kn k) SNone
  | String "/" (String "/" s) => tokenize_go s (TDone :: cons_state kn k) SNone
  | String "/" (String "=" s) => tokenize_g
...

Definition tokenize(s : string) : list token := tokenize_go s [] SNone.
(* iris/algebra/lib/excl_auth.v *)
From iris.algebra Require Export auth excl updates
From iris.algebra Require Import local_updates
From iris.prelude Require Import options

Definition excl_authR{SI : sidx} (A : ofe) : cmra :=
  authR (optionUR (exclR A)).

Definition excl_authUR{SI : sidx} (A : ofe) : ucmra :=
  authUR (optionUR (exclR A)).

Definition excl_auth_auth{SI : sidx} {A : ofe} (a : A) : excl_authR A :=
  ● (Some (Excl a)).

Definition excl_auth_frag{SI : sidx} {A : ofe} (a : A) : excl_authR A :=
  ◯ (Some (Excl a)).

Global TypeclassesOpaque excl_auth_auth excl_auth_frag.

Global Instance: Params (@excl_auth_auth) 2 := {}.

Global Instance: Params (@excl_auth_frag) 3 := {}.

Global Instanceexcl_auth_auth_ne : NonExpansive (@excl_auth_auth SI A).
  Proof. solve_proper. Qed.

Global Instanceexcl_auth_auth_proper :
    Proper ((≡) ==> (≡)) (@excl_auth_auth SI A).
  Proof. solve_proper. Qed.

Global Instanceexcl_auth_frag_ne : NonExpansive (@excl_auth_frag SI A).
  Proof. solve_proper. Qed.

Global Instanceexcl_auth_frag_proper :
    Proper ((≡) ==> (≡)) (@excl_auth_frag SI A).
  Proof. solve_proper. Qed.

Global Instanceexcl_auth_auth_discrete a : Discrete a → Discrete (●E a).
  Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.

Global Instanceexcl_auth_frag_discrete a : Discrete a → Discrete (◯E a).
  Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.

Lemma excl_auth_validNn a : ✓{n} (●E a ⋅ ◯E a).
  Proof. by rewrite auth_both_validN. Qed.

Lemma excl_auth_valida : ✓ (●E a ⋅ ◯E a).
  Proof. intros. by apply auth_both_valid_2. Qed.

Lemma excl_auth_agreeNn a b : ✓{n} (●E a ⋅ ◯E b) → a ≡{n}≡ b.
  Proof.
    rewrite auth_both_validN /= => -[Hincl Hvalid].
    move: Hincl=> /Some_includedN_exclusive /(_ I) ?. by apply (inj Excl).
  Qed.

Lemma excl_auth_agreea b : ✓ (●E a ⋅ ◯E b) → a ≡ b.
  Proof.
    intros. apply equiv_dist=> n. by apply excl_auth_agreeN, cmra_valid_validN.
  Qed.

Lemma excl_auth_agree_L`{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
  Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.

Lemma excl_auth_auth_op_validNn a b : ✓{n} (●E a ⋅ ●E b) ↔ False.
  Proof. apply auth_auth_op_validN. Qed.

Lemma excl_auth_auth_op_valida b : ✓ (●E a ⋅ ●E b) ↔ False.
  Proof. apply auth_auth_op_valid. Qed.

Lemma excl_auth_frag_op_validNn a b : ✓{n} (◯E a ⋅ ◯E b) ↔ False.
  Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.

Lemma excl_auth_frag_op_valida b : ✓ (◯E a ⋅ ◯E b) ↔ False.
  Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.

Lemma excl_auth_updatea b a' : ●E a ⋅ ◯E b ~~> ●E a' ⋅ ◯E a'.
  Proof.
    intros. by apply auth_update, option_local_update, exclusive_local_update.
  Qed.

Definition excl_authURF{SI : sidx} (F : oFunctor) : urFunctor :=
  authURF (optionURF (exclRF F)).

Global Instanceexcl_authURF_contractive {SI : sidx} F :
  oFunctorContractive F → urFunctorContractive (excl_authURF F).
Proof. apply _. Qed.

Definition excl_authRF{SI : sidx} (F : oFunctor) : rFunctor :=
  authRF (optionURF (exclRF F)).

Global Instanceexcl_authRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (excl_authRF F).
Proof. apply _. Qed.
(* iris/base_logic/lib/fancy_updates_from_vs.v *)
From stdpp Require Export coPset
From iris.proofmode Require Import proofmode
From iris.base_logic Require Export base_logic
From iris.prelude Require Import options

Definition fupd(E1 E2 : coPset) (P : uPred M) : uPred M :=
  ∃ R, R ∗ vs E1 E2 R P.

Global Instancefupd_ne E1 E2 : NonExpansive (@fupd E1 E2).
Proof. solve_proper. Qed.

Lemma fupd_introE P : P ⊢ |={E,E}=> P.
Proof. iIntros "HP". iExists P. iFrame "HP". iApply vs_impl; auto. Qed.

Lemma fupd_monoE1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
Proof.
  iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]".
  iExists R; iFrame "HR". iApply (vs_trans with "[$Hvs]").
  iApply vs_impl. iIntros "!> HP". by iApply HPQ.
Qed.

Lemma fupd_transE1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P.
Proof.
  iDestruct 1 as (R) "[HR Hvs]". iExists R. iFrame "HR".
  iApply (vs_trans with "[$Hvs]"). clear R.
  iApply vs_exists; iIntros (R). iApply vs_persistent_intro_r; iIntros "Hvs".
  iApply (vs_trans with "[$Hvs]"). iApply vs_impl; auto.
Qed.

Lemma fupd_mask_frame_rE1 E2 Ef P :
  E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P.
Proof.
  iIntros (HE); iDestruct 1 as (R) "[HR Hvs]". iExists R; iFrame "HR".
  by iApply vs_mask_frame_r.
Qed.

Lemma fupd_frame_rE1 E2 P Q : (|={E1,E2}=> P) ∗ Q ⊢ |={E1,E2}=> P ∗ Q.
Proof.
  iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]".
  iExists (R ∗ Q)%I. iFrame "HR HQ". by iApply vs_frame_r.
Qed.
(* iris/base_logic/lib/token.v *)
From iris.algebra Require Import excl
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Export own
From iris.prelude Require Import options

Class tokenGΣ := TokenG {
  #[local] token_inG :: inG Σ (exclR unitO);
}.

Global HintMode tokenG - : typeclass_instances.

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

Global InstancesubG_tokenΣ Σ : subG tokenΣ Σ → tokenG Σ.
Proof. solve_inG. Qed.

Local Definitiontoken_def `{!tokenG Σ} (γ : gname) : iProp Σ :=
  own γ (Excl ()).

Local Definitiontoken_aux : seal (@token_def). Proof. by eexists. Qed.

Definition token:= token_aux.(unseal).

Local Definitiontoken_unseal :
  @token = @token_def := token_aux.(seal_eq).

Global Argumentstoken {Σ _} γ.

Local Ltacunseal := rewrite ?token_unseal /token_def.

Global Instancetoken_timeless γ : Timeless (token γ).
  Proof. unseal. apply _. Qed.

Lemma token_alloc_strong(P : gname → Prop) :
    pred_infinite P →
    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ token γ.
  Proof. unseal. intros. iApply own_alloc_strong; done. Qed.

Lemma token_alloc:
    ⊢ |==> ∃ γ, token γ.
  Proof. unseal. iApply own_alloc. done. Qed.

Lemma token_exclusiveγ :
    token γ -∗ token γ -∗ False.
  Proof.
    unseal. iIntros "Htok1 Htok2".
    iCombine "Htok1 Htok2" gives %[].
  Qed.

Global Instancetoken_combine_gives γ :
    CombineSepGives (token γ) (token γ) ⌜False⌝.
  Proof.
    rewrite /CombineSepGives. iIntros "[H1 H2]".
    iDestruct (token_exclusive with "H1 H2") as %[].
  Qed.
(* iris/bi/lib/core.v *)
From iris.bi Require Export bi plainly
From iris.proofmode Require Import proofmode
From iris.prelude Require Import options

Definition coreP`{!Sbi PROP} (P : PROP) : PROP :=

Global Instance: Params (@coreP) 1 := {}.

Global TypeclassesOpaque coreP.

Lemma coreP_introP : P -∗ coreP P.
  Proof.
    rewrite /coreP. iIntros "HP" (Q) "_ HPQ".

Global InstancecoreP_persistent
      `{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP} P :
    Persistent (coreP P).
  Proof.
    rewrite /coreP /Persistent. iIntros "HC" (Q).
    iApply persistently_wand_affinely_plainly. iIntros "#HQ".
    iApply persistently_wand_affinely_plainly. iIntros "#HPQ".
    iApply "HQ". iApply "HC"; auto.
  Qed.

Global InstancecoreP_affine P : Affine P → Affine (coreP P).
  Proof. intros ?. rewrite /coreP /Affine. iIntros "HC". iApply "HC"; eauto. Qed.

Global InstancecoreP_ne : NonExpansive (coreP (PROP:=PROP)).
  Proof. solve_proper. Qed.

Global InstancecoreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (coreP (PROP:=PROP)).
  Proof. solve_proper. Qed.

Global InstancecoreP_mono : Proper ((⊢) ==> (⊢)) (coreP (PROP:=PROP)).
  Proof. solve_proper. Qed.

Global InstancecoreP_flip_mono :
    Proper (flip (⊢) ==> flip (⊢)) (coreP (PROP:=PROP)).
  Proof. solve_proper. Qed.

Lemma coreP_wandP Q : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q.
  Proof.
    rewrite /coreP. iIntros "#HPQ HP" (R) "#HR #HQR". iApply ("HP" with "HR").
    iIntros "!> !> HP". iApply "HQR". by iApply "HPQ".
  Qed.

Lemma coreP_elimP : Persistent P → coreP P -∗ P.
  Proof. rewrite /coreP. iIntros (?) "HCP". iApply "HCP"; auto. Qed.

Lemma coreP_entails`{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP} P Q :
    (<affine> coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
  Proof.
    split.
    - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP {HP}".
      iIntros "!>". by iApply HP.
    - iIntros (->) "HcQ". by iDestruct (coreP_elim with "HcQ") as "#HQ".
  Qed.

Lemma coreP_entails'`{!BiPersistentlyForall PROP, !BiPersistentlyImplSiPure PROP}
      P Q `{!Affine P} :
    (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
  Proof.
    rewrite -(affine_affinely (coreP P)) coreP_entails. split.
    - rewrite -{2}(affine_affinely P). by intros ->.
    - intros ->. apply affinely_elim.
  Qed.
(* iris_deprecated/base_logic/viewshifts.v *)
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Export invariants
From iris.prelude Require Import options

Definition vs`{!invGS Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
  □ (P -∗ |={E1,E2}=> Q).

Global Argumentsvs {_ _} _ _ _%_I _%_I.

Global Instance: Params (@vs) 4 := {}.

Global Instancevs_ne E1 E2 : NonExpansive2 (vs E1 E2).
Proof. solve_proper. Qed.

Global Instancevs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (vs E1 E2).
Proof. apply ne_proper_2, _. Qed.

Lemma vs_monoE1 E2 P P' Q Q' :
  (P ⊢ P') → (Q' ⊢ Q) → (P' ={E1,E2}=> Q') ⊢ P ={E1,E2}=> Q.
Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.

Global Instancevs_mono' E1 E2 : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (vs E1 E2).
Proof. solve_proper. Qed.

Lemma vs_false_elimE1 E2 P : ⊢ False ={E1,E2}=> P.
Proof. iIntros "!> []". Qed.

Lemma vs_timelessE P : Timeless P → ⊢ ▷ P ={E}=> P.
Proof. by iIntros (?) "!> > ?". Qed.

Lemma vs_transE1 E2 E3 P Q R :
  (P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R.
Proof.
  iIntros "#[HvsP HvsQ] !> HP".
  iMod ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
Qed.

Lemma vs_reflexiveE P : ⊢ P ={E}=> P.
Proof. by iIntros "!> HP". Qed.

Lemma vs_implE P Q : □ (P → Q) ⊢ P ={E}=> Q.
Proof. iIntros "#HPQ !> HP". by iApply "HPQ". Qed.

Lemma vs_frame_lE1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ R ∗ P ={E1,E2}=> R ∗ Q.
Proof. iIntros "#Hvs !> [$ HP]". by iApply "Hvs". Qed.

Lemma vs_frame_rE1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q ∗ R.
Proof. iIntros "#Hvs !> [HP $]". by iApply "Hvs". Qed.

Lemma vs_mask_frame_rE1 E2 Ef P Q :
  E1 ## Ef → (P ={E1,E2}=> Q) ⊢ P ={E1 ∪ Ef,E2 ∪ Ef}=> Q.
Proof.
  iIntros (?) "#Hvs !> HP". iApply fupd_mask_frame_r; auto. by iApply "Hvs".
Qed.

Lemma vs_invN E P Q R :
  ↑N ⊆ E → inv N R ∗ (▷ R ∗ P ={E∖↑N}=> ▷ R ∗ Q) ⊢ P ={E}=> Q.
Proof.
  iIntros (?) "#[? Hvs] !> HP". iInv N as "HR" "Hclose".
  iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
  by iApply "Hclose".
Qed.

Lemma vs_inv_accN E P :
  ↑N ⊆ E →
  ⊢ inv N P ={E,E∖↑N}=> ▷ P ∗ ∃ R, R ∗ (R ∗ ▷ P ={E∖↑N,E}=> True).
Proof.

Lemma vs_allocN P : ⊢ ▷ P ={↑N}=> inv N P.
Proof. iIntros "!> HP". by iApply inv_alloc. Qed.

Lemma wand_fupd_altE1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
Proof.
  rewrite bi.wand_alt. do 2 f_equiv. setoid_rewrite bi.affine_affinely; last apply _.
  by rewrite bi.persistently_impl_wand.
Qed.
(* iris_heap_lang/lib/arith.v *)
From iris.proofmode Require Import proofmode
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 minimum: val :=
  λ: "m" "n", if: "m" < "n" then "m" else "n".

Definition maximum: val :=
  λ: "m" "n", if: "m" < "n" then "n" else "m".

Lemma minimum_spec`{!heapGS Σ} s E (Φ : val → iProp Σ) (m n : Z) :
  ▷ Φ #(m `min` n) -∗
  WP minimum #m #n @ s;E {{ Φ }}.
Proof.
  iIntros "HΦ". wp_lam. wp_pures. case_bool_decide; wp_pures.
  - rewrite Z.min_l; [ done | by lia ].
  - rewrite Z.min_r; [ done | by lia ].
Qed.

Lemma minimum_spec_nat`{!heapGS Σ} s E (Φ : val → iProp Σ) (m n : nat) :
  ▷ Φ #(m `min` n)%nat -∗
  WP minimum #m #n @ s;E {{ Φ }}.
Proof. iIntros "HΦ". iApply minimum_spec. by rewrite Nat2Z.inj_min. Qed.

Lemma maximum_spec`{!heapGS Σ} s E (Φ : val → iProp Σ) (m n : Z) :
  ▷ Φ #(m `max` n) -∗
  WP maximum #m #n @ s;E {{ Φ }}.
Proof.
  iIntros "HΦ". wp_lam. wp_pures. case_bool_decide; wp_pures.
  - rewrite Z.max_r; [ done | by lia ].
  - rewrite Z.max_l; [ done | by lia ].
Qed.

Lemma maximum_spec_nat`{!heapGS Σ} s E (Φ : val → iProp Σ) (m n : nat) :
  ▷ Φ #(m `max` n)%nat -∗
  WP maximum #m #n @ s;E {{ Φ }}.
Proof. iIntros "HΦ". iApply maximum_spec. by rewrite Nat2Z.inj_max. Qed.
(* iris_heap_lang/lib/assert.v *)
From iris.proofmode Require Import proofmode
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 assert: val :=
  λ: "v", if: "v" #() then #() else #0 #0.

Lemma twp_assert`{!heapGS_gen hlc Σ} E (Φ : val → iProp Σ) e :
  WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗
  WP (assert: e)%V @ E [{ Φ }].
Proof.
  iIntros "HΦ". wp_lam.
  wp_smart_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.

Lemma wp_assert`{!heapGS_gen hlc Σ} E (Φ : val → iProp Σ) e :
  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
  WP (assert: e)%V @ E {{ Φ }}.
Proof.
  iIntros "HΦ". wp_lam.
  wp_smart_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
(* iris_heap_lang/lib/clairvoyant_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 (nondet_bool #()), NewProph).

Definition read_coin: val := λ: "cp", !(Fst "cp").

Definition toss_coin: val :=
  λ: "cp",
  let: "c" := Fst "cp" in
  let: "p" := Snd "cp" in
  let: "r" := nondet_bool #() in
  "c" <- "r";; resolve_proph: "p" to: "r";; #().

Definition prophecy_to_list_bool(vs : list (val * val)) : list bool :=
    (λ v, bool_decide (v = #true)) ∘ snd <$> vs.

Definition coin(cp : val) (bs : list bool) : iProp Σ :=
    ∃ (c : loc) (p : proph_id) (vs : list (val * val)),
       ⌜cp = (#c, #p)%V⌝ ∗
       ⌜bs ≠ []⌝ ∗ ⌜tail bs = prophecy_to_list_bool vs⌝ ∗
       proph p vs ∗
       from_option (λ b : bool, c ↦ #b) (∃ b : bool, c ↦ #b) (head bs).

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

Lemma read_coin_speccp bs :
    {{{ coin cp bs }}}
      read_coin cp
    {{{b bs', RET #b; ⌜bs = b :: bs'⌝ ∗ coin cp bs }}}.
  Proof.
    iIntros (Φ) "Hc HΦ".
    iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
    destruct bs as [|b bs]; simplify_eq/=.
    wp_lam. wp_load.
    iApply "HΦ"; iSplitR; first done.
    rewrite /coin; eauto 10 with iFrame.
  Qed.

Lemma toss_coin_speccp bs :
    {{{ coin cp bs }}}
      toss_coin cp
    {{{b bs', RET #(); ⌜bs = b :: bs'⌝ ∗ coin cp bs' }}}.
  Proof.
    iIntros (Φ) "Hc HΦ".
    iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
    destruct bs as [|b bs]; simplify_eq/=.
    wp_lam. do 2 (wp_proj; wp_let).
    wp_apply nondet_bool_spec as (r) "_"; first done.
    wp_store.
    wp_apply (wp_resolve_proph with "[Hp]") as (ws) "[-> Hp]"; first done.
    wp_seq.
    iApply "HΦ"; iSplitR; first done.
    destruct r; rewrite /coin; eauto 10 with iFrame.
  Qed.
(* iris_heap_lang/lib/diverge.v *)
From iris.proofmode Require Import proofmode
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 diverge: val :=
  rec: "diverge" "v" := "diverge" "v".

Lemma wp_diverge`{!heapGS Σ} s E (Φ : val → iProp Σ) (v : val) :
  ⊢ WP diverge v @ s;E {{ Φ }}.
Proof.
  iLöb as "IH". wp_lam. iApply "IH".
Qed.
(* iris_heap_lang/lib/increment.v *)
From iris.bi.lib Require Import fractional
From iris.proofmode Require Import proofmode
From iris.base_logic.lib Require Export invariants
From iris.program_logic Require Export atomic
From iris.heap_lang Require Import proofmode notation atomic_heap par
From iris.prelude Require Import options

Definition incr_phy: val :=
    rec: "incr" "l" :=
       let: "oldv" := !"l" in
       if: CAS "l" "oldv" ("oldv" + #1)
         then "oldv"
         else "incr" "l".

Lemma incr_phy_spec(l: loc) :
    ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr_phy #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>.
  Proof.
    iIntros (Φ) "AU". iLöb as "IH". wp_lam.

Definition incr: val :=
    rec: "incr" "l" :=
       let: "oldv" := !"l" in
       if: CAS "l" "oldv" ("oldv" + #1)
         then "oldv"
         else "incr" "l".
  Context `{!heapGS Σ, !atomic_heapGS Σ}.

Lemma incr_spec_direct(l: loc) :
    ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>.
  Proof.
    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
    awp_apply load_spec.

Lemma incr_spec(l: loc) :
    ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>.
  Proof.
    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
    awp_apply load_spec.

Definition weak_incr: val :=
    rec: "weak_incr" "l" :=
       let: "oldv" := !"l" in
       "l" <- ("oldv" + #1);;
       "oldv" .

Lemma weak_incr_spec(l: loc) (v : Z) :
    l ↦{#1/2} #v -∗
    <<{ ∀∀ (v' : Z), l ↦{#1/2} #v' }>>
      weak_incr #l @ ∅
    <<{ ⌜v = v'⌝ ∗ l ↦ #(v + 1)
      | RET #v }>>.
  Proof.
    iIntros "Hl" (Φ) "AU". wp_lam.
    wp_apply (atomic_wp_seq $! (load_spec _) with "Hl") as "Hl".
    wp_pures. awp_apply store_spec.

Local ExistingInstance primitive_atomic_heap.

Definition incr_client: val :=
    λ: "x",
       let: "l" := ref "x" in
       incr "l" ||| incr "l".

Lemma incr_client_safe(x: Z):
    ⊢ WP incr_client #x {{ _, True }}.
  Proof using Type*.
    wp_lam. wp_alloc l as "Hl".
    iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.