phanerozoic/Coq-Iris huggingface dataset:
(* tests/heapprop.v *)
Lemma heapProp_proofmode_test {A} (P Q R : heapProp) (Φ Ψ : A → heapProp) :
  P ∗ Q -∗
  □ R -∗
  □ (R -∗ ∃ x, Φ x) -∗
  ∃ x, Φ x ∗ Φ x ∗ P ∗ Q.
Proof.
  iIntros "[HP HQ] #HR #HRΦ".
  iDestruct ("HRΦ" with "HR") as (x) "#HΦ".
  iExists x. iFrame. by iSplitL.
Qed.
(* tests/heapprop_affine.v *)
Record heapProp
:= HeapProp {
  heapProp_holds :> gmap loc val → Prop;
  heapProp_closed σ1 σ2 : heapProp_holds σ1 → σ1 ⊆ σ2 → heapProp_holds σ2;
}.
(* tests/heapprop_affine.v *)
Definition heapProp_emp : heapProp
:= heapProp_pure True.
(* tests/heapprop_affine.v *)
Definition heapProp_impl_def (P Q : heapProp) : heapProp :=
  {| heapProp_holds σ := ∀ σ', σ ⊆ σ' → P σ' → Q σ' |}.
Next Obligation. intros P Q σ1 σ2 HPQ ? σ' ?; simpl in *. apply HPQ. by etrans. Qed.
(* tests/heapprop_affine.v *)
Definition heapProp_sep_def (P Q : heapProp) : heapProp :=
  {| heapProp_holds σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 ##ₘ σ2 ∧ P σ1 ∧ Q σ2 |}.
Next Obligation.
  intros P Q σ1 σ2 (σ11 & σ12 & -> & ? & ? & ?) ?.
  assert (σ11 ⊆ σ2) by (by etrans; [apply map_union_subseteq_l|]).
  exists σ11, (σ2 ∖ σ11). split_and!; [| |done|].
  - by rewrite map_difference_union.
  - by apply map_disjoint_difference_r1.
  - eapply heapProp_closed; [done|].
    apply map_union_reflecting_l with σ11; [done|..].
    + by apply map_disjoint_difference_r1.
    + by rewrite map_difference_union.
Qed.
(* tests/heapprop_affine.v *)
Definition heapProp_wand_def (P Q : heapProp) : heapProp :=
  {| heapProp_holds σ := ∀ σ', σ ##ₘ σ' → P σ' → Q (σ ∪ σ') |}.
Next Obligation.
  intros P Q σ1 σ2 HPQ ? σ' ??; simpl in *.
  apply heapProp_closed with (σ1 ∪ σ'); [by eauto using map_disjoint_weaken_l|].
  by apply map_union_mono_r.
Qed.
(* tests/heapprop_affine.v *)
Definition heapProp_unseal
:=
  (heapProp_pure_unseal, heapProp_and_unseal,
   heapProp_or_unseal, heapProp_impl_unseal, heapProp_forall_unseal,
   heapProp_exist_unseal, heapProp_sep_unseal, heapProp_wand_unseal,
   heapProp_persistently_unseal).
(* tests/heapprop_affine.v *)
Lemma heapProp_bi_persistently_mixin :
    BiPersistentlyMixin
      heapProp_entails heapProp_emp heapProp_and
      (@heapProp_exist) heapProp_sep heapProp_persistently.
Proof.
    eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
    - (* The "existential property" [(emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x]. For an
      affine BI the proof relies on there being a smallest resource/the unit
      (here the empty heap [∅]). *)
      unfold heapProp_emp. unseal. intros A Φ [H].
      destruct (H ∅) as [x ?]; [done|]. exists x. split=> σ _.
      eapply heapProp_closed; [done|]. by apply map_empty_subseteq.
    - by rewrite heapProp_persistently_unseal.
  Qed.
(* tests/heapprop_affine.v *)
Instance heapProp_affine : BiAffine heapPropI.
Proof. exact: bi.True_intro. Qed.
(* tests/heapprop_affine.v *)
Lemma heapProp_proofmode_test {A} (P Q Q' R : heapProp) (Φ Ψ : A → heapProp) :
  P ∗ Q ∗ Q' -∗ (* [Q'] is not used, to demonstrate affinity *)
  □ R -∗
  □ (R -∗ ∃ x, Φ x) -∗
  ∃ x, Φ x ∗ Φ x ∗ P ∗ Q.
Proof.
  iIntros "(HP & HQ & HQ') #HR #HRΦ".
  iDestruct ("HRΦ" with "HR") as (x) "#HΦ".
  iExists x. iFrame. by iSplitL.
Qed.
(* tests/heap_lang.v *)
Definition simpl_test :
    ⌜(10 = 4 + 6)%nat⌝ -∗
    WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, ⌜v = #1⌝ }}.
Proof.
    iIntros "?". wp_alloc l. repeat wp_pure || wp_load || wp_store.
    match goal with
    | |- context [ (10 = 4 + 6)%nat ] => done
    end.
  Qed.
(* tests/heap_lang.v *)
Definition val_scope_test_1
:= SOMEV (#(), #()).
(* tests/heap_lang.v *)
Definition heap_e : expr
:=
    let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
(* tests/heap_lang.v *)
Lemma heap_e_spec E : ⊢ WP heap_e @ E {{ v, ⌜v = #2⌝ }}.
Proof.
    iIntros "". rewrite /heap_e. Show.
    wp_alloc l as "?". wp_pures. wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
    wp_store. by wp_load.
  Qed.
(* tests/heap_lang.v *)
Definition heap_e2 : expr
:=
    let: "x" := ref #1 in
    let: "y" := ref #1 in
    "x" <- !"x" + #1 ;; !"x".
(* tests/heap_lang.v *)
Lemma heap_e2_spec E : ⊢ WP heap_e2 @ E [{ v, ⌜v = #2⌝ }].
Proof.
    iIntros "". rewrite /heap_e2.
    wp_alloc l as "Hl". Show. wp_alloc l'. do 2 wp_pure.
    wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
    wp_store. wp_load. done.
  Qed.
(* tests/heap_lang.v *)
Definition heap_e3 : expr
:=
    let: "x" := #true in
    let: "f" := λ: "z", "z" + #1 in
    if: "x" then "f" #0 else "f" #1.
(* tests/heap_lang.v *)
Lemma heap_e3_spec E : ⊢ WP heap_e3 @ E [{ v, ⌜v = #1⌝ }].
Proof.
    iIntros "". rewrite /heap_e3.
    by repeat (wp_pure _).
  Qed.
(* tests/heap_lang.v *)
Definition heap_e4 : expr
:=
    let: "x" := (let: "y" := ref (ref #1) in ref "y") in
    ! ! !"x".
(* tests/heap_lang.v *)
Lemma heap_e4_spec : ⊢ WP heap_e4 [{ v, ⌜ v = #1 ⌝ }].
Proof.
    rewrite /heap_e4. wp_alloc l. wp_alloc l'.
    wp_alloc l''. by repeat wp_load.
  Qed.
(* tests/heap_lang.v *)
Definition heap_e5 : expr
:=
    let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
(* tests/heap_lang.v *)
Lemma heap_e5_spec E : ⊢ WP heap_e5 @ E [{ v, ⌜v = #13⌝ }].
Proof.
    rewrite /heap_e5. wp_alloc l. wp_alloc l'.
    wp_load. wp_faa. do 2 wp_load. by wp_pures.
  Qed.
(* tests/heap_lang.v *)
Definition heap_e6 : val
:= λ: "v", "v" = "v".
(* tests/heap_lang.v *)
Lemma heap_e6_spec (v : val) :
    val_is_unboxed v → ⊢ WP heap_e6 v {{ w, ⌜ w = #true ⌝ }}.
Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
(* tests/heap_lang.v *)
Definition heap_e7 : val
:= λ: "v", CmpXchg "v" #0 #1.
(* tests/heap_lang.v *)
Lemma heap_e7_spec_total l : l ↦ #0 -∗ WP heap_e7 #l [{_,  l ↦ #1 }].
Proof. iIntros. wp_lam. wp_cmpxchg_suc. auto. Qed.
(* tests/heap_lang.v *)
Lemma heap_e7_spec l : ▷^2 l ↦ #0 -∗ WP heap_e7 #l {{_,  l ↦ #1 }}.
Proof. iIntros. wp_lam. Show. wp_cmpxchg_suc. Show. auto. Qed.
(* tests/heap_lang.v *)
Definition FindPred : val
:=
    rec: "pred" "x" "y" :=
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
(* tests/heap_lang.v *)
Definition Pred : val
:=
    λ: "x",
      if: "x" ≤ #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
(* tests/heap_lang.v *)
Lemma FindPred_spec n1 n2 E Φ :
    (n1 < n2)%Z →
    Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E [{ Φ }].
Proof.
    iIntros (Hn) "HΦ".
    iInduction (Z.gt_wf n2 n1) as [n1' _ IH] forall (Hn).
    wp_rec. wp_pures. case_bool_decide; wp_if.
    - iApply ("IH" with "[%] [%] HΦ"); lia.
    - by assert (n1' = n2 - 1)%Z as -> by lia.
  Qed.
(* tests/heap_lang.v *)
Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }].
Proof.
    iIntros "HΦ". wp_lam.
    wp_op. case_bool_decide.
    - wp_smart_apply FindPred_spec; first lia. wp_pures.
      by replace (n - 1)%Z with (- (-n + 2 - 1))%Z by lia.
    - wp_smart_apply FindPred_spec; eauto with lia.
  Qed.
(* tests/heap_lang.v *)
Lemma Pred_user E :
    ⊢ WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }].
Proof. iIntros "". wp_apply Pred_spec. by wp_smart_apply Pred_spec. Qed.
(* tests/heap_lang.v *)
Definition Id : val
:=
    rec: "go" "x" :=
      if: "x" = #0 then #() else "go" ("x" - #1).
(* tests/heap_lang.v *)
(* These tests specially test the handling of the [vals_compare_safe]
  side-condition of the [=] operator. *)
Lemma Id_wp (n : nat) : ⊢ WP Id #n {{ v, ⌜ v = #() ⌝ }}.
Proof.
    iInduction n as [|n IH]; wp_rec; wp_pures; first done.
    by replace (S n - 1)%Z with (n:Z) by lia.
  Qed.
(* tests/heap_lang.v *)
Lemma Id_twp (n : nat) : ⊢ WP Id #n [{ v, ⌜ v = #() ⌝ }].
Proof.
    iInduction n as [|n IH]; wp_rec; wp_pures; first done.
    by replace (S n - 1)%Z with (n:Z) by lia.
  Qed.
(* tests/heap_lang.v *)
Definition compare_pointers : val
:= λ: <>,
    let: "x" := ref #0 in
    let: "y" := ref #0 in
    ("x", "y", "x" ≤ "y").
(* tests/heap_lang.v *)
Lemma wp_compare_pointers E :
    ⊢ WP compare_pointers #() @ E [{ v, ∃ l1 l2 : loc,
        ⌜v = (#l1, #l2,
              #(bool_decide (loc_car l1 ≤ loc_car l2)))%V⌝ }].
Proof.
    rewrite /compare_pointers. wp_pures.
    wp_alloc l1 as "H1".
    wp_alloc l2 as "H2".
    wp_pures. by eauto.
  Qed.
(* tests/heap_lang.v *)
(* Make sure [wp_bind] works even when it changes nothing. *)
Lemma wp_bind_nop (e : expr) :
    ⊢ WP e + #0 {{ _, True }}.
Proof. wp_bind (e + #0)%E. Abort.
(* tests/heap_lang.v *)
Lemma wp_bind_nop (e : expr) :
    ⊢ WP e + #0 [{ _, True }].
Proof. wp_bind (e + #0)%E. Abort.
(* tests/heap_lang.v *)
Lemma wp_load_fail :
    ⊢ WP Fork #() {{ _, True }}.
Proof. Fail wp_load. Abort.
(* tests/heap_lang.v *)
Lemma twp_load_fail :
    ⊢ WP Fork #() [{ _, True }].
Proof. Fail wp_load. Abort.
(* tests/heap_lang.v *)
Lemma wp_load_fail_no_ptsto (l : loc) :
    ⊢ WP ! #l {{ _, True }}.
Proof. Fail wp_load. Abort.
(* tests/heap_lang.v *)
Lemma wp_store_fail :
    ⊢ WP Fork #() {{ _, True }}.
Proof. Fail wp_store. Abort.
(* tests/heap_lang.v *)
Lemma twp_store_fail :
    ⊢ WP Fork #() [{ _, True }].
Proof. Fail wp_store. Abort.
(* tests/heap_lang.v *)
Lemma wp_store_fail_no_ptsto (l : loc) :
    ⊢ WP #l <- #0 {{ _, True }}.
Proof. Fail wp_store. Abort.
(* tests/heap_lang.v *)
Lemma wp_bind_fail : ⊢ WP of_val #() {{ v, True }}.
Proof. Fail wp_bind (!_)%E. Abort.
(* tests/heap_lang.v *)
Lemma twp_bind_fail : ⊢ WP of_val #() [{ v, True }].
Proof. Fail wp_bind (!_)%E. Abort.
(* tests/heap_lang.v *)
Lemma wp_apply_evar e P :
    P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
(* tests/heap_lang.v *)
Lemma wp_pures_val (b : bool) :
    ⊢ WP of_val #b {{ _, True }}.
Proof. wp_pures. done. Qed.
(* tests/heap_lang.v *)
Lemma twp_pures_val (b : bool) :
    ⊢ WP of_val #b [{ _, True }].
Proof. wp_pures. done. Qed.
(* tests/heap_lang.v *)
Lemma wp_cmpxchg l v :
    val_is_unboxed v →
    l ↦ v -∗ WP CmpXchg #l v v {{ _, True }}.
Proof.
    iIntros (?) "?". wp_cmpxchg as ? | ?; done.
  Qed.
(* tests/heap_lang.v *)
Lemma twp_cmpxchg l v :
    val_is_unboxed v →
    l ↦ v -∗ WP CmpXchg #l v v [{ _, True }].
Proof.
    iIntros (?) "?". wp_cmpxchg as ? | ?; done.
  Qed.
(* tests/heap_lang.v *)
Lemma wp_xchg l (v₁ v₂ : val) :
    {{{ l ↦ v₁ }}}
      Xchg #l v₂
    {{{ RET v₁; l ↦ v₂ }}}.
Proof.
    iIntros (Φ) "Hl HΦ".
    wp_xchg.
    iApply "HΦ" => //.
  Qed.
(* tests/heap_lang.v *)
Lemma twp_xchg l (v₁ v₂ : val) :
     l ↦ v₁ -∗
       WP  Xchg #l v₂ [{ v₁, l ↦ v₂ }].
Proof.
    iIntros "Hl".
    wp_xchg => //.
  Qed.
(* tests/heap_lang.v *)
Lemma wp_xchg_inv N l (v : val) :
    {{{ inv N (∃ v, l ↦ v) }}}
      Xchg #l v
    {{{ v', RET v'; True }}}.
Proof.
    iIntros (Φ) "Hl HΦ".
    iInv "Hl" as (v') "Hl" "Hclose".
    wp_xchg.
    iApply "HΦ".
    iApply "Hclose".
    iExists _ => //.
  Qed.
(* tests/heap_lang.v *)
Lemma wp_alloc_split :
    ⊢ WP Alloc #0 {{ _, True }}.
Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
(* tests/heap_lang.v *)
Lemma wp_alloc_drop :
    ⊢ WP Alloc #0 {{ _, True }}.
Proof. wp_alloc l as "_". Show. done. Qed.
(* tests/heap_lang.v *)
Lemma wp_nonclosed_value :
    ⊢ WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}.
Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
(* tests/heap_lang.v *)
Lemma wp_alloc_array n :
    (0 < n)%Z →
    ⊢ {{{ True }}}
        AllocN #n #0
      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0 }}}.
Proof.
    iIntros (? Φ) "!> _ HΦ".
    wp_alloc l as "?"; first done.
    by iApply "HΦ".
  Qed.
(* tests/heap_lang.v *)
Lemma twp_alloc_array n :
    (0 < n)%Z →
    ⊢ [[{ True }]]
        AllocN #n #0
      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0 }]].
Proof.
    iIntros (? Φ) "!> _ HΦ".
    wp_alloc l as "?"; first done. Show.
    by iApply "HΦ".
  Qed.
(* tests/heap_lang.v *)
Lemma wp_load_array l :
    {{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l +ₗ #1) {{{ RET #1; True }}}.
Proof.
    iIntros (Φ) "Hl HΦ". wp_op.
    wp_apply (wp_load_offset _ _ _ _ 1 with "Hl"); first done.
    iIntros "Hl". by iApply "HΦ".
  Qed.
(* tests/heap_lang.v *)
Lemma test_array_fraction_destruct l vs :
    l ↦∗ vs -∗ l ↦∗{#1/2} vs ∗ l ↦∗{#1/2} vs.
Proof.
    iIntros "[Hl1 Hl2]". Show.
    by iFrame.
  Qed.
(* tests/heap_lang.v *)
Lemma test_array_fraction_combine l vs :
    l ↦∗{#1/2} vs -∗ l↦∗{#1/2} vs -∗ l ↦∗ vs.
Proof.
    iIntros "Hl1 Hl2".
    iSplitL "Hl1"; by iFrame.
  Qed.
(* tests/heap_lang.v *)
Lemma test_array_app l vs1 vs2 :
    l ↦∗ (vs1 ++ vs2) -∗ l ↦∗ (vs1 ++ vs2).
Proof.
    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
    iApply array_app. iSplitL "H1"; done.
  Qed.
(* tests/heap_lang.v *)
Lemma test_array_app_split l vs1 vs2 :
    l ↦∗ (vs1 ++ vs2) -∗ l ↦∗{#1/2} (vs1 ++ vs2).
Proof.
    iIntros "[$ _]". (* splits the fraction, not the app *)
  Qed.
(* tests/heap_lang.v *)
Lemma test_wp_free l v :
    {{{ l ↦ v }}} Free #l {{{ RET #(); True }}}.
Proof.
    iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
  Qed.
(* tests/heap_lang.v *)
Lemma test_twp_free l v :
    [[{ l ↦ v }]] Free #l [[{ RET #(); True }]].
Proof.
    iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
  Qed.
(* tests/heap_lang.v *)
Lemma test_wp_finish_fupd (v : val) :
    ⊢ WP of_val v {{ v, |={⊤}=> True }}.
Proof.
    wp_pures. Show. (* No second fupd was added. *)
  Abort.
(* tests/heap_lang.v *)
Lemma test_twp_finish_fupd (v : val) :
    ⊢ WP of_val v [{ v, |={⊤}=> True }].
Proof.
    wp_pures. Show. (* No second fupd was added. *)
  Abort.
(* tests/heap_lang.v *)
Lemma test_heaplang_not_unfolded :
    ⊢@{iPropI Σ} |={⊤}=> True.
Proof.
    cbn.
    Set Printing All.
    Show.
    Unset Printing All.
  Abort.
(* tests/heap_lang.v *)
Lemma test_wp_pure_credit_succeed P :
    ⊢ WP #42 + #420 {{ v, ▷ P ={∅}=∗ P }}.
Proof.
    wp_pure credit:"Hcred". Show.
    iIntros "!> HP". iNext credit: "Hcred". auto.
  Qed.
(* tests/heap_lang.v *)
Lemma test_wp_pure_credit_bump P :
    ⊢ £ 1 -∗ WP #42 + #420 {{ v, ▷ P ={∅}=∗ P }}.
Proof.
    iIntros "Hcred".
    wp_pure credit:"Hcred". Show.
    iIntros "!> HP". iNext credit: "Hcred".
    Show. (* Check that the order of hypotheses is preserved *) auto.
  Qed.
(* tests/heap_lang.v *)
Lemma test_wp_pure_credit_bump_2 P :
    ⊢ £ 1 -∗ WP #42 + #420 {{ v, ▷ ▷ P ={∅}=∗ P }}.
Proof.
    iIntros "Hcred".
    wp_pure credit:"Hcred". Show.
    iIntros "!> HP". iNext 2 credit: "Hcred". auto.
  Qed.
(* tests/heap_lang.v *)
Lemma test_wp_pure_credit_fail :
    ⊢ True -∗ WP #42 + #420 {{ v, True }}.
Proof.
    iIntros "Hcred".
    Fail wp_pure credit: "Hcred".
  Abort.
(* tests/heap_lang.v *)
(* HeapLang's allocator does not re-use freed locations.
     This test shows how one can reason about this in the logic,
     using the [meta_token]. *)
Definition address_uniqueness : expr
:=
   (let: "l1" := Alloc #1 in
    Free "l1";;
    let: "l2" := Alloc #2 in
    Free "l2";;
    if: "l1" ≠ "l2" then #0 else #0 #0)%E.
(* tests/heap_lang.v *)
Lemma test_wp_meta_token_address_reuse :
    ⊢ WP address_uniqueness {{ v, True }}.
Proof.
    unfold address_uniqueness.
    wp_apply (wp_alloc with "[//]") as (l1) "[Hl1 Hmeta1]". wp_pures.
    wp_free. wp_pures.
    wp_apply (wp_alloc with "[//]") as (l2) "[Hl2 Hmeta2]". wp_pures.
    wp_free. wp_pures.
    iPoseProof (meta_token_ne with "Hmeta1 Hmeta2") as "%Hne"; first done.
    rewrite bool_decide_false; last by congruence.
    wp_pures. done.
  Qed.
(* tests/heap_lang.v *)
(* Loading from a persistent points-to predicate in the _persistent_ context. *)
Lemma persistent_pointsto_load_persistent l v :
    {{{ l ↦□ v }}} ! #l {{{ RET v; True }}}.
Proof. iIntros (Φ) "#Hl HΦ". Show. wp_load. by iApply "HΦ". Qed.
(* tests/heap_lang.v *)
(* Loading from a persistent points-to predicate in the _spatial_ context. *)
Lemma persistent_pointsto_load_spatial l v :
    {{{ l ↦□ v }}} ! #l {{{ RET v; True }}}.
Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.
(* tests/heap_lang.v *)
Lemma persistent_pointsto_twp_load_persistent l v :
    [[{ l ↦□ v }]] ! #l [[{ RET v; True }]].
Proof. iIntros (Φ) "#Hl HΦ". wp_load. by iApply "HΦ". Qed.
(* tests/heap_lang.v *)
Lemma persistent_pointsto_twp_load_spatial l v :
    [[{ l ↦□ v }]] ! #l [[{ RET v; True }]].
Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.
(* tests/heap_lang.v *)
Lemma persistent_pointsto_load l (n : nat) :
    {{{ l ↦ #n }}} Store #l (! #l + #5) ;; ! #l {{{ RET #(n + 5); l ↦□ #(n + 5) }}}.
Proof.
    iIntros (Φ) "Hl HΦ".
    wp_load. wp_store.
    iMod (pointsto_persist with "Hl") as "#Hl".
    wp_load. by iApply "HΦ".
  Qed.
(* tests/heap_lang.v *)
(* Loading from the general pointsto for any [dfrac]. *)
Lemma general_pointsto dq l v :
    [[{ l ↦{dq} v }]] ! #l [[{ RET v; True }]].
Proof.
    iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
  Qed.
(* tests/heap_lang.v *)
(* Failing [CmpXchg] from a persistent points-to predicate in the _persistent_
  context. *)
Lemma persistent_pointsto_cmpxchg_persistent l :
    {{{ l ↦□ #1 }}} CmpXchg #l #0 #1 {{{ v, RET v; True }}}.
Proof. iIntros (Φ) "#Hl HΦ". wp_cmpxchg_fail. by iApply "HΦ". Qed.
(* tests/heap_lang.v *)
(* Failing [CmpXchg] from a persistent points-to predicate in the _spatial_
  context. *)
Lemma persistent_pointsto_cmpxchg_spatial l :
    {{{ l ↦□ #1 }}} CmpXchg #l #0 #1 {{{ v, RET v; True }}}.
Proof. iIntros (Φ) "Hl HΦ". wp_cmpxchg_fail. by iApply "HΦ". Qed.
(* tests/heap_lang.v *)
(* Make sure that we can split a pointsto containing an evar. *)
Lemma pointsto_evar_iSplit l v :
    l ↦{#1 / 2} v -∗  ∃ q, l ↦{#1 / 2 + q} v.
Proof. iIntros "H". iExists _. iSplitL; first by iAssumption. Abort.
(* tests/heap_lang.v *)
Lemma pointsto_frame_1 l v q1 q2 :
    l ↦{#q1} v -∗ l ↦{#q2} v -∗ l ↦{#q1 + q2} v.
Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
(* tests/heap_lang.v *)
Lemma pointsto_frame_2 l v q :
    l ↦{#q/2} v -∗ l ↦{#q/2} v -∗ l ↦{#q} v.
Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
(* tests/heap_lang.v *)
Lemma pointsto_combine_2 l v1 q1 v2 q2 :
    l ↦{#q1} v1 -∗ l ↦{#q2} v2 -∗
    l ↦{#(q1 + q2)} v1 ∗ ⌜q1 + q2 ≤ 1⌝%Qp ∗ ⌜v1 = v2⌝.
Proof. iIntros "H1 H2". by iCombine "H1 H2" as "$" gives %[? ->]. Qed.
(* tests/heap_lang.v *)
Lemma pointsto_combine_3 l v1 q1 v2 q2 v3 q3 :
    l ↦{#q1} v1 -∗ l ↦{#q2} v2 -∗ l ↦{#q3} v3 -∗
    l ↦{#(q1 + (q2 + q3))} v1 ∗ ⌜q1 + (q2 + q3) ≤ 1⌝%Qp ∗ ⌜v1 = v2⌝ ∗ ⌜v2 = v3⌝.
Proof.
    iIntros "H1 H2 H3".
    by iCombine "H1 H2 H3" as "$" gives %[[_ ->] [? ->]].
  Qed.
(* tests/heap_lang.v *)
Lemma pointsto_combine_4 l v1 q1 v2 q2 v3 q3 v4 q4 :
    l ↦{#q1} v1 -∗ l ↦{#q2} v2 -∗ l ↦{#q3} v3 -∗ l ↦{#q4} v4 -∗
    l ↦{#(q1 + (q2 + (q3 + q4)))} v1 ∗ ⌜q1 + (q2 + (q3 + q4)) ≤ 1⌝%Qp ∗
      ⌜v1 = v2⌝ ∗ ⌜v2 = v3⌝ ∗ ⌜v3 = v4⌝.
Proof.
    iIntros "H1 H2 H3 H4".
    iCombine "H1 H2 H3 H4" as "$" gives %H. Show.
    by destruct H as [[[_ ->] [_ ->]] [? ->]].
  Qed.
(* tests/heap_lang.v *)
(* Make sure these parse and type-check. *)
Lemma inv_pointsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5.
Abort.
(* tests/heap_lang.v *)
Lemma inv_pointsto_test (l : loc) : ⊢ l ↦_(λ _, True) □.
Abort.
(* tests/heap_lang.v *)
(* Make sure [setoid_rewrite] works. *)
Lemma inv_pointsto_setoid_rewrite (l : loc) (I : val → Prop) :
    (∀ v, I v ↔ I #true) →
    ⊢ l ↦_(λ v, I v) □.
Proof.
    iIntros (Heq). setoid_rewrite Heq. Show.
  Abort.
(* tests/heap_lang.v *)
Lemma wp_iMod_fupd_atomic E1 E2 P :
    (|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
Proof.
    iIntros "H". iMod "H". Show.
  Abort.
(* tests/heap_lang.v *)
Lemma wp_iInv_atomic N E P :
    ↑ N ⊆ E →
    inv N P -∗ WP #() #() @ E {{ _, True }}.
Proof.
    iIntros (?) "H". iInv "H" as "H" "Hclose". Show.
  Abort.
(* tests/heap_lang.v *)
Lemma wp_iInv_atomic_acc N E P :
    ↑ N ⊆ E →
    inv N P -∗ WP #() #() @ E {{ _, True }}.
Proof.
    (* Test if a side-condition for [Atomic] is generated *)
    iIntros (?) "H". iInv "H" as "H". Show.
  Abort.
(* tests/heap_lang.v *)
Lemma not_cmpxchg :
    ⊢ WP #() #() {{ _, True }}.
Proof.
    Fail wp_cmpxchg_suc.
  Abort.
(* tests/heap_lang.v *)
Lemma wp_apply_not_wp : True.
Proof. Fail wp_apply Pred_spec. Fail wp_smart_apply Pred_spec. Abort.
(* tests/heap_lang.v *)
(* Test a closed proof *)
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
Proof. eapply (heap_adequacy heapΣ). iIntros (?) "_". by iApply heap_e_spec. Qed.
(* tests/heap_lang.v *)
Lemma heap_e_totally_adequate σ : sn erased_step ([heap_e], σ).
Proof.
  eapply (heap_total HasLc heapΣ NotStuck _ _ (const True) 0).
  iIntros (?) "_ _". rewrite /heap_e /=.
  wp_alloc l. wp_load. wp_store. wp_load. auto.
Qed.
(* tests/heap_lang_interpreter.v *)
Example test_1 :
  exec 1000 ((λ: "x", "x" + #1) #2) = inl #3.
Proof. reflexivity. Qed.
(* tests/heap_lang_printing.v *)
Lemma ref_print :
    True -∗ WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
Proof.
    iIntros "_". Show.
  Abort.
(* tests/heap_lang_printing.v *)
(* These terms aren't even closed, but that's not what this is about.  The
  length of the variable names etc. has been carefully chosen to trigger
  particular behavior of the Coq pretty printer. *)
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
    True -∗ WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
Proof.
    iIntros "_". Show.
    wp_bind (fun1 #()). Show.
  Abort.
(* tests/heap_lang_printing.v *)
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) long_post :
    True -∗ WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v"
    {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
Proof.
    iIntros "_". Show.
    wp_bind (fun1 #()). Show.
  Abort.
(* tests/heap_lang_printing.v *)
Lemma wp_print_long_expr (l1 : loc) (fun2 fun3 : expr) long_post N E_long :
    ↑N ⊆ E_long →
    inv N True -∗ WP let: "val1" := ! #l1 in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v"
    @ E_long
    {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
Proof.
    iIntros (?) "Hinv". Show.
    wp_bind (! #l1)%E. Show.
    iInv "Hinv" as "_". Show.
  Abort.
(* tests/heap_lang_printing.v *)
Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
Proof. Show. Abort.
(* tests/heap_lang_printing.v *)
Lemma texan_triple_long_expr_mask (fun1 fun2 fun3 : expr) E_mask_is_long_too :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    @ E_mask_is_long_too
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
Proof. Show. Abort.
(* tests/heap_lang_printing.v *)
Lemma texan_triple_long_expr_mask_post (fun1 fun2 fun3 : expr) long_post E_mask_is_long_too :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    @ E_mask_is_long_too
    {{{ (x y : val) (z : Z), RET (x, y, #z); long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}}.
Proof. Show. Abort.
(* tests/heap_lang_printing2.v *)
Lemma vs_print (P Q : iProp Σ) :
    P ={⊤}=∗ Q.
Proof. Show. Abort.
(* tests/heap_lang_printing2.v *)
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
    True -∗ WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
Proof.
    iIntros "_". Show.
  Abort.
(* tests/heap_lang_proph.v *)
Lemma test_resolve1 E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
    l ↦ #n -∗
    proph p vs -∗
    WP Resolve (CmpXchg #l #n (#n + #1)) #p v @ E
      {{ v, ⌜v = (#n, #true)%V⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}.
Proof.
    iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
    wp_cmpxchg_suc. iIntros "!>" (ws ->) "Hp". eauto with iFrame.
  Qed.