phanerozoic/Coq-Iris huggingface dataset:
(* iris_heap_lang/class_instances.v *)
(* The instance below is a more general version of [Skip] *)
Instance beta_atomic s f x v1 v2 : Atomic s (App (RecV f x (Val v1)) (Val v2)).
Proof. destruct f, x; solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance unop_atomic s op v : Atomic s (UnOp op (Val v)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance binop_atomic s op v1 v2 : Atomic s (BinOp op (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance if_true_atomic s v1 e2 :
    Atomic s (If (Val $ LitV $ LitBool true) (Val v1) e2).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance if_false_atomic s e1 v2 :
    Atomic s (If (Val $ LitV $ LitBool false) e1 (Val v2)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance fst_atomic s v : Atomic s (Fst (Val v)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance snd_atomic s v : Atomic s (Snd (Val v)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance free_atomic s v : Atomic s (Free (Val v)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance xchg_atomic s v1 v2 : Atomic s (Xchg (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance cmpxchg_atomic s v0 v1 v2 : Atomic s (CmpXchg (Val v0) (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
(* iris_heap_lang/class_instances.v *)
Instance resolve_atomic s e v1 v2 :
    Atomic s e → Atomic s (Resolve e (Val v1) (Val v2)).
Proof.
    rename e into e1. intros H σ1 e2 κ σ2 efs [Ks e1' e2' Hfill -> step].
    simpl in *. induction Ks as [|K Ks _] using rev_ind; simpl in Hfill.
    - subst. inversion_clear step. by eapply (H σ1 (Val _) _ σ2 efs), base_prim_step.
    - rewrite fill_app. rewrite fill_app in Hfill.
      assert (∀ v, Val v = fill Ks e1' → False) as fill_absurd.
      { intros v Hv. assert (to_val (fill Ks e1') = Some v) as Htv by by rewrite -Hv.
        apply to_val_fill_some in Htv. destruct Htv as [-> ->]. inversion step. }
      destruct K; (inversion Hfill; clear Hfill; subst; try
        match goal with | H : Val ?v = fill Ks e1' |- _ => by apply fill_absurd in H end).
      refine (_ (H σ1 (fill (Ks ++ [_]) e2') _ σ2 efs _)).
      + destruct s; intro Hs; simpl in *.
        * destruct Hs as [v Hs]. apply to_val_fill_some in Hs. by destruct Hs, Ks.
        * apply irreducible_resolve. by rewrite fill_app in Hs.
      + econstructor; try done. simpl. by rewrite fill_app.
  Qed.
(* iris_heap_lang/class_instances.v *)
(* The behavior of the various [wp_] tactics with regard to lambda differs in
the following way:

- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.

To realize this behavior, we define the class [AsRecV v f x erec], which takes a
value [v] as its input, and turns it into a [RecV f x erec] via the instance
[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
not if [v] contains a lambda/rec that is hidden behind a definition.

To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
Class AsRecV (v : val) (f x : binder) (erec : expr)
:=
  as_recv : v = RecV f x erec.
(* iris_heap_lang/class_instances.v *)
Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e
:= eq_refl.
(* iris_heap_lang/class_instances.v *)
Ltac solve_exec_safe
:= intros; subst; do 3 eexists; econstructor; eauto.
(* iris_heap_lang/class_instances.v *)
Ltac solve_exec_puredet
:= simpl; intros; by inv_base_step.
(* iris_heap_lang/class_instances.v *)
Ltac solve_pure_exec
:=
    subst; intros ?; apply nsteps_once, pure_base_step_pure_step;
      constructor; [solve_exec_safe | solve_exec_puredet].
(* iris_heap_lang/class_instances.v *)
Instance pure_recc f x (erec : expr) :
    PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_pairc (v1 v2 : val) :
    PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_injlc (v : val) :
    PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_injrc (v : val) :
    PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
    PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_unop op v v' :
    PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_binop op v1 v2 v' :
    PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v') | 10.
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
(* Lower-cost instance for [EqOp]. *)
Instance pure_eqop v1 v2 :
    PureExec (vals_compare_safe v1 v2) 1
      (BinOp EqOp (Val v1) (Val v2))
      (Val $ LitV $ LitBool $ bool_decide (v1 = v2)) | 1.
Proof.
    intros Hcompare.
    cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
    { intros. revert Hcompare. solve_pure_exec. }
    rewrite /bin_op_eval /= decide_True //.
  Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_if_true e1 e2 :
    PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_if_false e1 e2 :
    PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_fst v1 v2 :
    PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_snd v1 v2 :
    PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_case_inl v e1 e2 :
    PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/class_instances.v *)
Instance pure_case_inr v e1 e2 :
    PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
Proof. solve_pure_exec. Qed.
(* iris_heap_lang/derived_laws.v *)
(* The [array] connective is a version of [pointsto] that works
with lists of values. *)
Definition array `{!heapGS_gen hlc Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ
:=
  [∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v.
(* iris_heap_lang/derived_laws.v *)
Notation "l ↦∗ dq vs"
:= (array l dq vs)
  (at level 20, dq custom dfrac  at level 1, format "l  ↦∗ dq  vs") : bi_scope.
(* iris_heap_lang/derived_laws.v *)
Instance array_timeless l q vs : Timeless (array l q vs)
:= _.
(* iris_heap_lang/derived_laws.v *)
Instance array_fractional l vs : Fractional (λ q, l ↦∗{#q} vs)%I
:= _.
(* iris_heap_lang/derived_laws.v *)
Instance array_as_fractional l q vs :
  AsFractional (l ↦∗{#q} vs) (λ q, l ↦∗{#q} vs)%I q.
Proof. split; done || apply _. Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma array_nil l dq : l ↦∗{dq} [] ⊣⊢ emp.
Proof. by rewrite /array. Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma array_singleton l dq v : l ↦∗{dq} [v] ⊣⊢ l ↦{dq} v.
Proof. by rewrite /array /= right_id Loc.add_0. Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma array_app l dq vs ws :
  l ↦∗{dq} (vs ++ ws) ⊣⊢ l ↦∗{dq} vs ∗ (l +ₗ length vs) ↦∗{dq} ws.
Proof.
  rewrite /array big_sepL_app.
  setoid_rewrite Nat2Z.inj_add.
  by setoid_rewrite Loc.add_assoc.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma array_cons l dq v vs : l ↦∗{dq} (v :: vs) ⊣⊢ l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs.
Proof.
  rewrite /array big_sepL_cons Loc.add_0.
  setoid_rewrite Loc.add_assoc.
  setoid_rewrite Nat2Z.inj_succ.
  by setoid_rewrite Z.add_1_l.
Qed.
(* iris_heap_lang/derived_laws.v *)
Instance array_cons_frame l dq v vs R Q :
  Frame false R (l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs) Q →
  Frame false R (l ↦∗{dq} (v :: vs)) Q | 2.
Proof. by rewrite /Frame array_cons. Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma update_array l dq vs off v :
  vs !! off = Some v →
  ⊢ l ↦∗{dq} vs -∗ ((l +ₗ off) ↦{dq} v ∗ ∀ v', (l +ₗ off) ↦{dq} v' -∗ l ↦∗{dq} <[off:=v']>vs).
Proof.
  iIntros (Hlookup) "Hl".
  rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
  iDestruct (array_app with "Hl") as "[Hl1 Hl]".
  iDestruct (array_cons with "Hl") as "[Hl2 Hl3]".
  assert (off < length vs) as H by (apply lookup_lt_is_Some; by eexists).
  rewrite length_take min_l; last by lia. iFrame "Hl2".
  iIntros (w) "Hl2".
  clear Hlookup. assert (<[off:=w]> vs !! off = Some w) as Hlookup.
  { apply list_lookup_insert_eq. lia. }
  rewrite -[in (l ↦∗{_} <[off:=w]> vs)%I](take_drop_middle (<[off:=w]> vs) off w Hlookup).
  iApply array_app. rewrite take_insert_ge; last by lia. iFrame.
  iApply array_cons. rewrite length_take min_l; last by lia. iFrame.
  rewrite drop_insert_lt; last by lia. done.
Qed.
(* iris_heap_lang/derived_laws.v *)
(* * Rules for allocation *)
Lemma pointsto_seq_array l dq v n :
  ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{dq} v) -∗
  l ↦∗{dq} replicate n v.
Proof.
  rewrite /array. iInduction n as [|n' IH] forall (l); simpl.
  { done. }
  iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
  setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
  setoid_rewrite <-Loc.add_assoc. iApply "IH". done.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_allocN s E v n :
  (0 < n)%Z →
  [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
Proof.
  iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN_seq; [done..|].
  iIntros (l) "Hlm". iApply "HΦ".
  iDestruct (big_sepL_sep with "Hlm") as "[Hl $]".
  by iApply pointsto_seq_array.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_allocN s E v n :
  (0 < n)%Z →
  {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
Proof.
  iIntros (? Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
  iApply twp_allocN; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_allocN_vec s E v n :
  (0 < n)%Z →
  [[{ True }]]
    AllocN #n v @ s ; E
  [[{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
Proof.
  iIntros (Hzs Φ) "_ HΦ". iApply twp_allocN; [ lia | done | .. ].
  iIntros (l) "[Hl Hm]". iApply "HΦ". rewrite vec_to_list_replicate. iFrame.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_allocN_vec s E v n :
  (0 < n)%Z →
  {{{ True }}}
    AllocN #n v @ s ; E
  {{{ l, RET #l; l ↦∗ vreplicate (Z.to_nat n) v ∗
         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
Proof.
  iIntros (? Φ) "_ HΦ". iApply (twp_wp_step with "HΦ").
  iApply twp_allocN_vec; [auto..|]; iIntros (l) "H HΦ". by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
(* * Rules for accessing array elements *)
Lemma twp_load_offset s E l dq off vs v :
  vs !! off = Some v →
  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ off) @ s; E [[{ RET v; l ↦∗{dq} vs }]].
Proof.
  iIntros (Hlookup Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (twp_load with "Hl1"). iIntros "Hl1". iApply "HΦ".
  iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
  iApply "Hl2". iApply "Hl1".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_load_offset s E l dq off vs v :
  vs !! off = Some v →
  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ off) @ s; E {{{ RET v; l ↦∗{dq} vs }}}.
Proof.
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_load_offset with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
  [[{ l ↦∗{dq} vs }]] ! #(l +ₗ off) @ s; E [[{ RET vs !!! off; l ↦∗{dq} vs }]].
Proof. apply twp_load_offset. by apply vlookup_lookup. Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
  {{{ ▷ l ↦∗{dq} vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗{dq} vs }}}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_store_offset s E l off vs v :
  is_Some (vs !! off) →
  [[{ l ↦∗ vs }]] #(l +ₗ off) <- v @ s; E [[{ RET #(); l ↦∗ <[off:=v]> vs }]].
Proof.
  iIntros ([w Hlookup] Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (twp_store with "Hl1"). iIntros "Hl1".
  iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_store_offset s E l off vs v :
  is_Some (vs !! off) →
  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
Proof.
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_store_offset with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
  [[{ l ↦∗ vs }]] #(l +ₗ off) <- v @ s; E [[{ RET #(); l ↦∗ <[off:=v]> vs }]].
Proof.
  setoid_rewrite vec_to_list_insert. apply twp_store_offset.
  eexists. by apply vlookup_lookup.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_store_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
  {{{ ▷ l ↦∗ vs }}} #(l +ₗ off) <- v @ s; E {{{ RET #(); l ↦∗ <[off:=v]> vs }}}.
Proof.
  iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_store_offset_vec with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_xchg_offset s E l off vs v v' :
  vs !! off = Some v →
  [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v' @ s; E [[{ RET v; l ↦∗ <[off:=v']> vs }]].
Proof.
  iIntros (Hlookup Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (twp_xchg with "Hl1"). iIntros "Hl1".
  iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_xchg_offset s E l off vs v v' :
  vs !! off = Some v →
  {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v' @ s; E {{{ RET v; l ↦∗ <[off:=v']> vs }}}.
Proof.
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_xchg_offset with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
  [[{ l ↦∗ vs }]] Xchg #(l +ₗ off) v @ s; E [[{ RET (vs !!! off); l ↦∗ <[off:=v]> vs }]].
Proof.
  setoid_rewrite vec_to_list_insert. apply twp_xchg_offset.
  by apply vlookup_lookup.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
   {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v @ s; E {{{ RET (vs !!! off); l ↦∗ <[off:=v]> vs }}}.
Proof.
  iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_xchg_offset_vec with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
  vs !! off = Some v' →
  v' = v1 →
  vals_compare_safe v' v1 →
  [[{ l ↦∗ vs }]]
    CmpXchg #(l +ₗ off) v1 v2 @ s; E
  [[{ RET (v', #true); l ↦∗ <[off:=v2]> vs }]].
Proof.
  iIntros (Hlookup ?? Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (twp_cmpxchg_suc with "Hl1"); [done..|].
  iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_cmpxchg_suc_offset s E l off vs v' v1 v2 :
  vs !! off = Some v' →
  v' = v1 →
  vals_compare_safe v' v1 →
  {{{ ▷ l ↦∗ vs }}}
    CmpXchg #(l +ₗ off) v1 v2 @ s; E
  {{{ RET (v', #true); l ↦∗ <[off:=v2]> vs }}}.
Proof.
  iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_suc_offset with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off = v1 →
  vals_compare_safe (vs !!! off) v1 →
  [[{ l ↦∗ vs }]]
    CmpXchg #(l +ₗ off) v1 v2 @ s; E
  [[{ RET (vs !!! off, #true); l ↦∗ <[off:=v2]> vs }]].
Proof.
  intros. setoid_rewrite vec_to_list_insert.
  apply twp_cmpxchg_suc_offset; [|done..].
  by apply vlookup_lookup.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off = v1 →
  vals_compare_safe (vs !!! off) v1 →
  {{{ ▷ l ↦∗ vs }}}
    CmpXchg #(l +ₗ off) v1 v2 @ s; E
  {{{ RET (vs !!! off, #true); l ↦∗ <[off:=v2]> vs }}}.
Proof.
  iIntros (?? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_suc_offset_vec with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
  vs !! off = Some v0 →
  v0 ≠ v1 →
  vals_compare_safe v0 v1 →
  [[{ l ↦∗{dq} vs }]]
    CmpXchg #(l +ₗ off) v1 v2 @ s; E
  [[{ RET (v0, #false); l ↦∗{dq} vs }]].
Proof.
  iIntros (Hlookup HNEq Hcmp Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (twp_cmpxchg_fail with "Hl1"); first done.
  { destruct Hcmp; by [ left | right ]. }
  iIntros "Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2".
  rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
  vs !! off = Some v0 →
  v0 ≠ v1 →
  vals_compare_safe v0 v1 →
  {{{ ▷ l ↦∗{dq} vs }}}
    CmpXchg #(l +ₗ off) v1 v2 @ s; E
  {{{ RET (v0, #false); l ↦∗{dq} vs }}}.
Proof.
  iIntros (??? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_cmpxchg_fail_offset with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off ≠ v1 →
  vals_compare_safe (vs !!! off) v1 →
  [[{ l ↦∗{dq} vs }]]
    CmpXchg #(l +ₗ off) v1 v2 @ s; E
  [[{ RET (vs !!! off, #false); l ↦∗{dq} vs }]].
Proof.
  intros. apply twp_cmpxchg_fail_offset; [|done..].
  by apply vlookup_lookup.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_cmpxchg_fail_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) v1 v2 :
  vs !!! off ≠ v1 →
  vals_compare_safe (vs !!! off) v1 →
  {{{ ▷ l ↦∗{dq} vs }}}
    CmpXchg #(l +ₗ off) v1 v2 @ s; E
  {{{ RET (vs !!! off, #false); l ↦∗{dq} vs }}}.
Proof.
  intros. eapply wp_cmpxchg_fail_offset; [|done..].
  by apply vlookup_lookup.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_faa_offset s E l off vs (i1 i2 : Z) :
  vs !! off = Some #i1 →
  [[{ l ↦∗ vs }]] FAA #(l +ₗ off) #i2 @ s; E
  [[{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }]].
Proof.
  iIntros (Hlookup Φ) "Hl HΦ".
  iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
  iApply (twp_faa with "Hl1").
  iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_faa_offset s E l off vs (i1 i2 : Z) :
  vs !! off = Some #i1 →
  {{{ ▷ l ↦∗ vs }}} FAA #(l +ₗ off) #i2 @ s; E
  {{{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }}}.
Proof.
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_faa_offset with "H"); [by eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma twp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
  vs !!! off = #i1 →
  [[{ l ↦∗ vs }]] FAA #(l +ₗ off) #i2 @ s; E
  [[{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }]].
Proof.
  intros. setoid_rewrite vec_to_list_insert. apply twp_faa_offset.
  by apply vlookup_lookup.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_faa_offset_vec s E l sz (off : fin sz) (vs : vec val sz) (i1 i2 : Z) :
  vs !!! off = #i1 →
  {{{ ▷ l ↦∗ vs }}} FAA #(l +ₗ off) #i2 @ s; E
  {{{ RET LitV (LitInt i1); l ↦∗ <[off:=#(i1 + i2)]> vs }}}.
Proof.
  iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
  iApply (twp_faa_offset_vec with "H"); [by eauto..|]; iIntros "H HΦ".
  by iApply "HΦ".
Qed.
(* iris_heap_lang/derived_laws.v *)
(* Lemmas for some particular expression inside the [Resolve]. *)
Lemma wp_resolve_proph s E (p : proph_id) (pvs : list (val * val)) v :
  {{{ proph p pvs }}}
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v) @ s; E
  {{{ pvs', RET (LitV LitUnit); ⌜pvs = (LitV LitUnit, v)::pvs'⌝ ∗ proph p pvs' }}}.
Proof.
  iIntros (Φ) "Hp HΦ". iApply (wp_resolve with "Hp"); first done.
  iApply lifting.wp_pure_step_later; first done.
  iIntros "!> _". iApply wp_value. iIntros (vs') "HEq Hp". iApply "HΦ". iFrame.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_resolve_cmpxchg_suc s E l (p : proph_id) (pvs : list (val * val)) v1 v2 v :
  vals_compare_safe v1 v1 →
  {{{ proph p pvs ∗ ▷ l ↦ v1 }}}
    Resolve (CmpXchg #l v1 v2) #p v @ s; E
  {{{ RET (v1, #true) ; ∃ pvs', ⌜pvs = ((v1, #true)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦ v2 }}}.
Proof.
  iIntros (Hcmp Φ) "[Hp Hl] HΦ".
  iApply (wp_resolve with "Hp"); first done.
  assert (val_is_unboxed v1) as Hv1; first by destruct Hcmp.
  iApply (wp_cmpxchg_suc with "Hl"); [done..|]. iIntros "!> Hl".
  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.
(* iris_heap_lang/derived_laws.v *)
Lemma wp_resolve_cmpxchg_fail s E l (p : proph_id) (pvs : list (val * val)) dq v' v1 v2 v :
  v' ≠ v1 → vals_compare_safe v' v1 →
  {{{ proph p pvs ∗ ▷ l ↦{dq} v' }}}
    Resolve (CmpXchg #l v1 v2) #p v @ s; E
  {{{ RET (v', #false) ; ∃ pvs', ⌜pvs = ((v', #false)%V, v)::pvs'⌝ ∗ proph p pvs' ∗ l ↦{dq} v' }}}.
Proof.
  iIntros (NEq Hcmp Φ) "[Hp Hl] HΦ".
  iApply (wp_resolve with "Hp"); first done.
  iApply (wp_cmpxchg_fail with "Hl"); [done..|]. iIntros "!> Hl".
  iIntros (pvs' ->) "Hp". iApply "HΦ". eauto with iFrame.
Qed.
(* iris_heap_lang/lang.v *)
(* Expressions and vals. *)
Definition proph_id
:= positive.
(* iris_heap_lang/lang.v *)
(* We have a notion of "poison" as a variant of unit that may not be compared
with anything. This is useful for erasure proofs: if we erased things to unit,
[<erased> == unit] would evaluate to true after erasure, changing program
behavior. So we erase to the poison value instead, making sure that no legal
comparisons could be affected. *)
Inductive base_lit : Set
:=
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitPoison
  | LitLoc (l : loc) | LitProphecy (p: proph_id).
(* iris_heap_lang/lang.v *)
Inductive un_op : Set
:=
  | NegOp | MinusUnOp.
(* iris_heap_lang/lang.v *)
Inductive bin_op : Set
:=
  (** We use "quot" and "rem" instead of "div" and "mod" to
      better match the behavior of 'real' languages:
      e.g., in Rust, -30/-4 == 7. ("div" would return 8.) *)
  | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
  | AndOp | OrOp | XorOp (* Bitwise *)
  | ShiftLOp | ShiftROp (* Shifts *)
  | LeOp | LtOp | EqOp (* Relations *)
  | OffsetOp.