phanerozoic/Coq-Iris huggingface dataset:
(* iris_heap_lang/proph_erasure.v *)
Lemma fill_to_resolve e v1 v2 K e' :
  to_val e' = None →
  Resolve e v1 v2 = fill K e' →
  K = [] ∨ ∃ K' Ki, K = K' ++ [ResolveLCtx Ki v1 v2].
Proof.
  intros Hnv Hrs; simpl in *.
  assert (∀ v K, fill K e' ≠ v) as Hcontr.
  { intros w K' Hw.
    assert (to_val (of_val w) = to_val (fill K' e')) as He'
        by (by rewrite Hw).
    rewrite fill_not_val in He'; by eauto. }
  destruct K as [|Ki K _] using rev_ind; first by left.
  rewrite fill_app in Hrs.
  destruct Ki; simplify_eq/=; eauto;
    try exfalso; eapply Hcontr; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma projs_pure_steps (v0 v1 v2 : val) :
  rtc pure_step (Fst (Fst (v0, v1, v2))) v0.
Proof.
  etrans; first apply (rtc_pure_step_ctx (fill [PairLCtx _; FstCtx; FstCtx])).
  { apply rtc_once.
    apply pure_base_step_pure_step.
    split; first repeat econstructor.
    intros ????? Hhstep; inversion Hhstep; simplify_eq/=; eauto. }
  simpl.
  etrans; first apply (rtc_pure_step_ctx (fill [FstCtx; FstCtx])).
  { apply rtc_once.
    apply pure_base_step_pure_step.
    split; first repeat econstructor.
    intros ????? Hhstep; inversion Hhstep; simplify_eq/=; eauto. }
  simpl.
  etrans; first apply (rtc_pure_step_ctx (fill [FstCtx])).
  { apply rtc_once.
    apply pure_base_step_pure_step.
    split; first repeat econstructor.
    intros ????? Hhstep; inversion Hhstep; simplify_eq/=; eauto. }
  simpl.
  apply rtc_once.
  apply pure_base_step_pure_step.
  split; first repeat econstructor.
  intros ????? Hhstep; inversion Hhstep; simplify_eq/=; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma Resolve_3_vals_base_stuck v0 v1 v2 σ κ e σ' efs :
  ¬ base_step (Resolve v0 v1 v2) σ κ e σ' efs.
Proof.
  intros Hhstep.
  inversion Hhstep; simplify_eq/=.
  apply (eq_None_not_Some (to_val (Val v0))); last eauto.
  by eapply val_base_stuck.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma Resolve_3_vals_unsafe (v0 v1 v2 : val) σ :
  ¬ not_stuck (Resolve v0 v1 v2) σ.
Proof.
  assert(∀ w K e, Val w = fill K e → is_Some (to_val e)) as Hvfill.
  { intros ? K ? Heq; eapply (fill_val K); rewrite /= -Heq; eauto. }
  apply not_not_stuck.
  split; first done.
  intros ???? [K e1' e2' Hrs Hhstep]; simplify_eq/=.
  destruct K as [|Ki K _] using rev_ind.
  { simplify_eq/=.
    eapply Resolve_3_vals_base_stuck; eauto. }
  rewrite fill_app in Hrs.
  destruct Ki; simplify_eq/=.
  - rename select ectx_item into Ki.
    pose proof (fill_item_val Ki (fill K e1')) as Hnv.
    apply fill_val in Hnv as [? Hnv]; last by rewrite -Hrs; eauto.
    by erewrite val_base_stuck in Hnv.
  - edestruct Hvfill as [? Heq]; eauto.
    by erewrite val_base_stuck in Heq.
  - edestruct Hvfill as [? Heq]; eauto.
    by erewrite val_base_stuck in Heq.
Qed.
(* iris_heap_lang/proph_erasure.v *)
(* [(e1, σ1)] takes a [prim_step] to [(e2', σ2')] forking threads [efs']
 such that [σ2] is the erasure of [σ2'] and [efs] is the erasure of
 [efs']. Furthermore, [e2] takes [pure_steps] to match up with [e2].  It is
 crucial for us that [e2] takes [pure_step]s because we need to know
 that [e2] does not get stuck and that the steps are deterministic.

 Essentially, the main part of the erasure proof's argument is that if
 the erased program takes steps, then the original program also takes
 matching steps. This however, does not entirely hold. In cases where
 the erasure of [Resovle] takes a step, the original program
 immediately produces the value while the erased program has to still
 perform projections [Fst] to get the result (see the [Resolve] case
 of [erase_expr]). For this purpose, we prove that in those cases (and
 also in general) the erased program also takes a number of (possibly
 zero) steps so that the original and the erased programs are matched
 up again. *)
Definition prim_step_matched_by_erased_steps e1 σ1 e2 σ2 efs
:=
  ∃ e2' σ2' κ' efs' e2'',
    prim_step e1 σ1 κ' e2' σ2' efs' ∧ rtc pure_step e2 e2'' ∧
    erase_expr e2' = e2'' ∧ erase_state σ2' = σ2 ∧ erase_tp efs' = efs.
(* iris_heap_lang/proph_erasure.v *)
Lemma prim_step_matched_by_erased_steps_ectx K e1 σ1 e2 σ2 efs :
  prim_step_matched_by_erased_steps e1 σ1 e2 σ2 efs →
  prim_step_matched_by_erased_steps (fill K e1) σ1 (fill (erase_ectx K) e2) σ2 efs.
Proof.
  intros (?&?&?&?&?&?&?&?&?&?); simplify_eq/=.
  eexists _, _, _, _, _; repeat split.
  - by apply fill_prim_step.
  - rewrite erase_ectx_expr.
    by eapply (rtc_pure_step_ctx (fill (erase_ectx K))).
Qed.
(* iris_heap_lang/proph_erasure.v *)
Definition is_Resolve (e : expr)
:=
  match e with Resolve _ _ _ => True | _ => False end.
(* iris_heap_lang/proph_erasure.v *)
Instance is_Resolve_dec e : Decision (is_Resolve e).
Proof. destruct e; solve_decision. Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma non_resolve_prim_step_matched_by_erased_steps_ectx_item
      Ki e1 e1' σ1 e2 σ2 efs :
  to_val e1' = None →
  ¬ is_Resolve e1 →
  not_stuck e1 σ1 →
  erase_expr e1 = fill_item Ki e1' →
  (∀ e1, erase_expr e1 = e1' → not_stuck e1 σ1 →
         prim_step_matched_by_erased_steps e1 σ1 e2 σ2 efs) →
  prim_step_matched_by_erased_steps e1 σ1 (fill_item Ki e2) σ2 efs.
Proof.
  intros Hnv Hnr Hsf He1 IH.
  destruct Ki; simplify_eq/=;
    repeat
      match goal with
      | H : erase_expr ?e = _ |- _ => destruct e; simplify_eq/=; try done
      | H : context [erased_new_proph] |- _ =>
        rewrite /erased_new_proph in H; simplify_eq/=
      | |- prim_step_matched_by_erased_steps ?e _ _ _ _ =>
        let tac K e :=
            lazymatch K with
            | [] => fail
            | _ => apply (prim_step_matched_by_erased_steps_ectx K);
                    apply IH; [done| by eapply (not_stuck_fill_inv (fill K))]
            end
        in
        reshape_expr e tac
      end.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma erased_prim_step_prim_step e1 σ1 κ e2 σ2 efs:
  prim_step (erase_expr e1) (erase_state σ1) κ e2 σ2 efs → not_stuck e1 σ1 →
  prim_step_matched_by_erased_steps e1 σ1 e2 σ2 efs.
Proof.
  intros Hstp He1sf.
  inversion Hstp as [K e1' e2' He1 ? Hhstp]; clear Hstp; simplify_eq/=.
  set (len := length K); assert (length K = len) as Hlen by done; clearbody len.
  revert K Hlen e1 He1 He1sf.
  induction len as [m IHm]using lt_wf_ind; intros K Hlen e1 He1 He1sf;
    simplify_eq.
  destruct K as [|Ki K _] using rev_ind; simplify_eq/=.
  { apply erased_base_step_base_step in Hhstp as (?&?&?&?&?&<-&?&<-).
    eexists _, _, _, _, _; repeat split;
      first (by apply base_prim_step); auto using rtc_refl. }
  rewrite length_app in IHm; simpl in *.
  rewrite fill_app /=; rewrite fill_app /= in He1.
  eapply prim_step_matched_by_erased_steps_ectx_item; eauto; [].
  { intros K' **; simpl in *. apply (IHm (length K')); auto with lia. }
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_CmpXchg v1 v2 σ l vl:
  heap σ !! l = Some (Some vl) →
  vals_compare_safe vl v1 →
  ∃ e2' σ2' ef', prim_step (CmpXchg #l (erase_val v1)
                             (erase_val v2)) (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hl Hv.
  destruct (bool_decide (vl = v1)) eqn:Heqvls.
  - do 3 eexists; apply base_prim_step;
      econstructor; [|by apply vals_compare_safe_erase|by eauto].
      by rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl.
  - do 3 eexists; apply base_prim_step;
        econstructor; [|by apply vals_compare_safe_erase|by eauto].
      by rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_resolve e w σ :
  (∃ e2' σ2' ef', prim_step (erase_expr e) (erase_state σ) [] e2' σ2' ef') →
  ∃ e2' σ2' ef',
    prim_step (erase_resolve (erase_expr e) #LitPoison (erase_val w))
              (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros (?&?&?&?).
  by eexists _, _, _;
    apply (fill_prim_step [PairLCtx _; PairLCtx _;FstCtx; FstCtx]).
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_un_op σ op v v':
  un_op_eval op v = Some v' →
  ∃ e2' σ2' ef', prim_step (UnOp op (erase_val v)) (erase_state σ) [] e2' σ2' ef'.
Proof.
  do 3 eexists; apply base_prim_step; econstructor.
  apply un_op_eval_erase; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_bin_op σ op v1 v2 v':
  bin_op_eval op v1 v2 = Some v' →
  ∃ e2' σ2' ef', prim_step (BinOp op (erase_val v1) (erase_val v2))
                           (erase_state σ) [] e2' σ2' ef'.
Proof.
  do 3 eexists; apply base_prim_step; econstructor.
  apply bin_op_eval_erase; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_allocN σ l n v:
  (0 < n)%Z →
  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
  ∃ e2' σ2' ef',
    prim_step (AllocN #n (erase_val v)) (erase_state σ) [] e2' σ2' ef'.
Proof.
  do 3 eexists; apply base_prim_step; econstructor; eauto.
  intros; rewrite lookup_erase_heap_None; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_free σ l v :
  heap σ !! l = Some (Some v) →
  ∃ e2' σ2' ef', prim_step (Free #l) (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hw. do 3 eexists; apply base_prim_step; econstructor.
  rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hw; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_load σ l v:
  heap σ !! l = Some (Some v) →
  ∃ e2' σ2' ef', prim_step (! #l) (erase_state σ) [] e2' σ2' ef'.
Proof.
  do 3 eexists; apply base_prim_step; econstructor.
  rewrite /erase_state /state_upd_heap /= lookup_erase_heap.
  by destruct lookup; simplify_eq.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_xchg σ l v w :
  heap σ !! l = Some (Some v) →
  ∃ e2' σ2' ef', prim_step (Xchg #l (erase_val w)) (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hl. do 3 eexists; apply base_prim_step; econstructor.
  rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_store σ l v w :
  heap σ !! l = Some (Some v) →
  ∃ e2' σ2' ef', prim_step (#l <- erase_val w) (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hw. do 3 eexists; apply base_prim_step; econstructor.
  rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hw; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma base_step_erased_prim_step_FAA σ l n n':
  heap σ !! l = Some (Some #n) →
  ∃ e2' σ2' ef', prim_step (FAA #l #n') (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hl.
  do 3 eexists; apply base_prim_step. econstructor.
  by rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl.
Qed.
(* iris_heap_lang/proph_erasure.v *)
(* [Resolve] is translated as a projection out of a triple.
Therefore, when resolve takes a head step, the erasure of [Resolve] takes a
prim step inside the triple. *)
Lemma base_step_erased_prim_step e1 σ1 κ e2 σ2 ef:
  base_step e1 σ1 κ e2 σ2 ef →
  ∃ e2' σ2' ef', prim_step (erase_expr e1) (erase_state σ1) [] e2' σ2' ef'.
Proof.
  induction 1; simplify_eq/=;
    eauto using base_step_erased_prim_step_CmpXchg,
                base_step_erased_prim_step_resolve,
                base_step_erased_prim_step_un_op,
                base_step_erased_prim_step_bin_op,
                base_step_erased_prim_step_allocN,
                base_step_erased_prim_step_free,
                base_step_erased_prim_step_load,
                base_step_erased_prim_step_store,
                base_step_erased_prim_step_xchg,
                base_step_erased_prim_step_FAA;
    by do 3 eexists; apply base_prim_step; econstructor.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma reducible_erased_reducible e σ :
  reducible e σ → reducible (erase_expr e) (erase_state σ).
Proof.
  intros (?&?&?&?&Hpstp); simpl in *.
  inversion Hpstp; simplify_eq/=.
  rewrite erase_ectx_expr.
  edestruct base_step_erased_prim_step as (?&?&?&?); first done; simpl in *.
  eexists _, _, _, _; eapply fill_prim_step; eauto.
Qed.
(* iris_heap_lang/proph_erasure.v *)
Lemma pure_step_tp_safe t1 t2 e1 σ :
  (∀ e2, e2 ∈ t2 → not_stuck e2 σ) → pure_steps_tp t1 (erase_tp t2) →
  e1 ∈ t1 → not_stuck e1 (erase_state σ).
Proof.
  intros Ht2 Hpr [i He1]%list_elem_of_lookup_1.
  eapply Forall2_lookup_l in Hpr as [e2' [He2' Hpr]]; simpl in *; eauto.
  rewrite /erase_tp list_lookup_fmap in He2'.
  destruct (t2 !! i) eqn:He2; simplify_eq/=.
  apply list_elem_of_lookup_2, Ht2 in He2.
  clear -Hpr He2.
  inversion Hpr as [|??? [? _]]; simplify_eq.
  - destruct He2 as [[? ?%of_to_val]|]; simplify_eq/=; first by left; eauto.
    by right; apply reducible_erased_reducible.
  - right; eauto using reducible_no_obs_reducible.
Qed.
(* iris_heap_lang/proph_erasure.v *)
(* This is the top-level erasure theorem: erasure preserves adequacy. *)
Theorem erasure e σ φ :
  adequate NotStuck e σ φ →
  adequate NotStuck (erase_expr e) (erase_state σ)
           (λ v σ, ∃ v' σ', erase_val v' = v ∧ erase_state σ' = σ ∧ φ v' σ').
Proof.
  simpl; intros Hade; simpl in *.
  cut (∀ t2 σ2,
          rtc erased_step ([erase_expr e], erase_state σ) (t2, σ2) →
          (∃ t2' t2'' σ2',
              rtc erased_step ([e], σ) (t2'', σ2') ∧
              t2' = erase_tp t2'' ∧ σ2 = erase_state σ2' ∧
              pure_steps_tp t2 t2')).
  { intros Hreach; split; simpl in *.
    - intros ? ? ? Hrtc; edestruct (Hreach _ _ Hrtc) as
          (t2'&t2''&σ2'&Hos&Ht2'&Hσ2&Hptp); simplify_eq/=.
      apply Forall2_cons_inv_l in Hptp as (oe&t3&Hoe%rtc_pure_step_val&_&?);
        destruct t2''; simplify_eq/=.
      apply erase_to_val in Hoe as (?&?%of_to_val&?); simplify_eq.
      pose proof (adequate_result _ _ _ _ Hade _ _ _ Hos); eauto.
    - intros ? ? ? Hs Hrtc He2; edestruct (Hreach _ _ Hrtc) as
          (t2'&t2''&σ2'&Hos&Ht2'&Hσ2&Hptp); simplify_eq/=.
      eapply pure_step_tp_safe; [|done..].
      intros e2' He2'.
      apply (adequate_not_stuck _ _ _ _ Hade _ _ _ eq_refl Hos He2'). }
  intros t2 σ2 [n Hstps]%rtc_nsteps; simpl in *; revert t2 σ2 Hstps.
  induction n as [|n IHn].
  { intros t2 σ2 Hstps; inversion Hstps; simplify_eq /=.
    repeat econstructor. }
  intros t2 σ2 Hstps.
  apply nsteps_inv_r in Hstps as [[t3 σ3] [Hstps Hρ]]; simpl in *.
  destruct (IHn _ _ Hstps) as (t2'&t2''&σ2'&Hostps&?&?&Hprstps); simplify_eq.
  edestruct @erased_step_pure_step_tp as [[? Hint]|Hext]; simplify_eq/=;
    eauto 10; [|done..].
  destruct Hext as (i&ei&t2'&efs&e'&κ&Hi1&Ht2&Hpstp);
    simplify_eq/=.
  rewrite /erase_tp list_lookup_fmap in Hi1.
  destruct (t2'' !! i) as [eio|] eqn:Heq; simplify_eq/=.
  edestruct erased_prim_step_prim_step as
    (eio' & σ3 & κ' & efs' & ee & Heiopstp & Hprstps' & ?&?&?); first done;
    last simplify_eq/=.
  { eapply adequate_not_stuck; eauto using list_elem_of_lookup_2. }
  eexists _, _, _; repeat split.
  { etrans; first done.
    apply rtc_once; eexists.
    eapply step_insert; eauto. }
  rewrite /erase_tp fmap_app.
  rewrite list_fmap_insert/=.
  apply Forall2_app; last done.
  apply Forall2_same_length_lookup; split.
  { apply Forall2_length in Hprstps; rewrite length_fmap in Hprstps.
    by rewrite !length_insert length_fmap. }
  intros j x y.
  destruct (decide (i = j)); simplify_eq.
  { rewrite !list_lookup_insert_eq ?length_fmap; eauto using lookup_lt_Some; [].
    by intros ? ?; simplify_eq. }
  rewrite !list_lookup_insert_ne // list_lookup_fmap.
  intros ? ?.
  eapply Forall2_lookup_lr; eauto.
  by rewrite /erase_tp list_lookup_fmap.
Qed.
(* iris_heap_lang/tactics.v *)
(* The tactic [inv_base_step] performs inversion on hypotheses of the shape
[base_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
operations. This tactic is slightly ad-hoc and tuned for proving our lifting
lemmas. *)
Ltac inv_base_step
:=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : base_step ?e _ _ _ _ _ |- _ =>
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and should thus better be avoided. *)
     inversion H; subst; clear H
  end.
(* iris_heap_lang/total_adequacy.v *)
Definition heap_total hlc Σ `{!heapGpreS Σ} s e σ φ m :
  (∀ `{!heapGS_gen hlc Σ},
    ⊢ inv_heap_inv -∗ £ m -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
  sn erased_step ([e], σ).
Proof.
  intros Hwp; eapply (twp_total _ _ _); iIntros (?) "".
  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
  iMod (inv_heap_init loc (option val)) as (?) ">Hi".
  iMod (proph_map_init [] σ.(used_proph_id)) as (?) "[Hp _]".
  iMod (mono_nat_own_alloc 0) as (γ) "[Hsteps _]".
  iModIntro.
  iExists
    (λ σ ns κs _, (gen_heap_interp σ.(heap) ∗
                   proph_map_interp κs σ.(used_proph_id) ∗
                   γ ↪●MN ns)%I),
    id, (λ _, True%I), _; iFrame.
  by iApply (Hwp (HeapGS _ _ _ _ _ _ _ _)).
Qed.
(* iris_heap_lang/lib/arith.v *)
(* A library defining binary [minimum] and [maximum] functions, together with
their expected specs. These operations come up often when working manipulating
array indices (checking for bounds). *)
Definition minimum : val
:=
  λ: "m" "n", if: "m" < "n" then "m" else "n".
(* iris_heap_lang/lib/arith.v *)
Definition maximum : val
:=
  λ: "m" "n", if: "m" < "n" then "n" else "m".
(* iris_heap_lang/lib/arith.v *)
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.
(* iris_heap_lang/lib/arith.v *)
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.
(* iris_heap_lang/lib/arith.v *)
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.
(* iris_heap_lang/lib/arith.v *)
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/array.v *)
(* Provides some array utilities:

* [array_free], to deallocate an entire array in one go.
* [array_copy_to], a function which copies to an array in-place.
* Using [array_copy_to] we also implement [array_clone], which allocates a fresh
array and copies to it.
* [array_init], to create and initialize an array with a given
function. Specifically, [array_init n f] creates a new array of size
[n] in which the [i]th element is initialized with [f #i] *)
Definition array_free : val
:=
  rec: "freeN" "ptr" "n" :=
    if: "n" ≤ #0 then #()
    else Free "ptr";;
         "freeN" ("ptr" +ₗ #1) ("n" - #1).
(* iris_heap_lang/lib/array.v *)
Definition array_copy_to : val
:=
  rec: "array_copy_to" "dst" "src" "n" :=
    if: "n" ≤ #0 then #()
    else "dst" <- !"src";;
         "array_copy_to" ("dst" +ₗ #1) ("src" +ₗ #1) ("n" - #1).
(* iris_heap_lang/lib/array.v *)
Definition array_clone : val
:=
  λ: "src" "n",
    let: "dst" := AllocN "n" #() in
    array_copy_to "dst" "src" "n";;
    "dst".
(* iris_heap_lang/lib/array.v *)
(* [array_init_loop src i n f] initializes elements
   [i], [i+1], ..., [n] of the array [src] to
   [f #i], [f #(i+1)], ..., [f #n] *)
Definition array_init_loop : val
:=
  rec: "loop" "src" "i" "n" "f" :=
    if: "i" = "n" then #()
    else "src" +ₗ "i" <- "f" "i";;
         "loop" "src" ("i" + #1) "n" "f".
(* iris_heap_lang/lib/array.v *)
Definition array_init : val
:=
  λ: "n" "f",
    let: "src" := AllocN "n" #() in
    array_init_loop "src" #0 "n" "f";;
    "src".
(* iris_heap_lang/lib/array.v *)
Lemma twp_array_free s E l vs (n : Z) :
    n = length vs →
    [[{ l ↦∗ vs }]] array_free #l #n @ s; E [[{ RET #(); True }]].
Proof.
    iIntros (Hlen Φ) "Hl HΦ".
    iInduction vs as [|v vs IH] forall (l n Hlen); subst n; wp_rec; wp_pures.
    { iApply "HΦ". done. }
    iDestruct (array_cons with "Hl") as "[Hv Hl]".
    wp_free. wp_pures. iApply ("IH" with "[] Hl"); eauto with lia.
  Qed.
(* iris_heap_lang/lib/array.v *)
Lemma wp_array_free s E l vs (n : Z) :
    n = length vs →
    {{{ l ↦∗ vs }}} array_free #l #n @ s; E {{{ RET #(); True }}}.
Proof.
    iIntros (? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
    iApply (twp_array_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
  Qed.
(* iris_heap_lang/lib/array.v *)
Lemma twp_array_copy_to stk E (dst src : loc) vdst vsrc dq (n : Z) :
    Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
    [[{ dst ↦∗ vdst ∗ src ↦∗{dq} vsrc }]]
      array_copy_to #dst #src #n @ stk; E
    [[{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }]].
Proof.
    iIntros (Hvdst Hvsrc Φ) "[Hdst Hsrc] HΦ".
    iInduction vdst as [|v1 vdst IH] forall (n dst src vsrc Hvdst Hvsrc);
      destruct vsrc as [|v2 vsrc]; simplify_eq/=; try lia; wp_rec; wp_pures.
    { iApply "HΦ". auto with iFrame. }
    iDestruct (array_cons with "Hdst") as "[Hv1 Hdst]".
    iDestruct (array_cons with "Hsrc") as "[Hv2 Hsrc]".
    wp_load; wp_store.
    wp_smart_apply ("IH" with "[%] [%] Hdst Hsrc") as "[Hvdst Hvsrc]"; [ lia .. | ].
    iApply "HΦ"; by iFrame.
  Qed.
(* iris_heap_lang/lib/array.v *)
Lemma wp_array_copy_to stk E (dst src : loc) vdst vsrc dq (n : Z) :
    Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
    {{{ dst ↦∗ vdst ∗ src ↦∗{dq} vsrc }}}
      array_copy_to #dst #src #n @ stk; E
    {{{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }}}.
Proof.
    iIntros (? ? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
    iApply (twp_array_copy_to with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
  Qed.
(* iris_heap_lang/lib/array.v *)
Lemma twp_array_clone stk E l dq vl n :
    Z.of_nat (length vl) = n →
    (0 < n)%Z →
    [[{ l ↦∗{dq} vl }]]
      array_clone #l #n @ stk; E
    [[{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{dq} vl }]].
Proof.
    iIntros (Hvl Hn Φ) "Hvl HΦ".
    wp_lam.
    wp_alloc dst as "Hdst"; first by auto.
    wp_smart_apply (twp_array_copy_to with "[$Hdst $Hvl]") as "[Hdst Hl]".
    - rewrite length_replicate Z2Nat.id; lia.
    - auto.
    - wp_pures.
      iApply "HΦ"; by iFrame.
  Qed.
(* iris_heap_lang/lib/array.v *)
Lemma wp_array_clone stk E l dq vl n :
    Z.of_nat (length vl) = n →
    (0 < n)%Z →
    {{{ l ↦∗{dq} vl }}}
      array_clone #l #n @ stk; E
    {{{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{dq} vl }}}.
Proof.
    iIntros (? ? Φ) "H HΦ". iApply (twp_wp_step with "HΦ").
    iApply (twp_array_clone with "H"); [auto..|]; iIntros (l') "H HΦ". by iApply "HΦ".
  Qed.
(* iris_heap_lang/lib/array.v *)
Lemma wp_array_init_loop stk E l i n k f  :
      n = Z.of_nat (i + k) →
      {{{
        (l +ₗ i) ↦∗ replicate k #() ∗
        [∗ list] j ∈ seq i k, WP f #(j : nat) @ stk; E {{ Q j }}
      }}}
        array_init_loop #l #i #n f @ stk; E
      {{{ vs, RET #();
        ⌜ length vs = k ⌝ ∗ (l +ₗ i) ↦∗ vs ∗ [∗ list] j↦v ∈ vs, Q (i + j) v
      }}}.
Proof.
      iIntros (Hn Φ) "[Hl Hf] HΦ".
      iInduction k as [|k IH] forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
      { rewrite bool_decide_eq_true_2; last (repeat f_equal; lia).
        wp_pures. iApply ("HΦ" $! []). auto. }
      rewrite bool_decide_eq_false_2; last naive_solver lia.
      iDestruct (array_cons with "Hl") as "[Hl HSl]".
      iDestruct "Hf" as "[Hf HSf]".
      wp_smart_apply (wp_wand with "Hf") as (v) "Hv". wp_store. wp_pures.
      rewrite Z.add_1_r -Nat2Z.inj_succ.
      iApply ("IH" with "[%] [HSl] HSf"); first lia.
      { by rewrite Loc.add_assoc Z.add_1_r -Nat2Z.inj_succ. }
      iIntros "!>" (vs). iDestruct 1 as (<-) "[HSl Hvs]".
      iApply ("HΦ" $! (v :: vs)). iSplit; [naive_solver|]. iSplitL "Hl HSl".
      - iFrame "Hl". by rewrite Loc.add_assoc Z.add_1_r -Nat2Z.inj_succ.
      - iEval (rewrite /= Nat.add_0_r; setoid_rewrite Nat.add_succ_r). iFrame.
    Qed.