Merge branch 'array_init' into 'master'

Add `array_init` and corresponding WP specs.

See merge request iris/iris!492

theories/heap_lang/lib/array.v

@@ -10,6 +10,9 @@ From iris Require Import options.
 * [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]
 
 *)
 
@@ -31,6 +34,21 @@ Definition array_clone : val :=
     array_copy_to "dst" "src" "n";;
     "dst".
 
+(* [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] *)
+Local 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".
+
+Definition array_init : val :=
+  λ: "n" "f",
+    let: "src" := AllocN "n" #() in
+    array_init_loop "src" #0 "n" "f";;
+    "src".
+
 Section proof.
   Context `{!heapG Σ}.
 
@@ -52,7 +70,7 @@ Section proof.
     iApply (twp_array_free with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
   Qed.
 
-  Theorem twp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
+  Lemma twp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
     Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
     [[{ dst ↦∗ vdst ∗ src ↦∗{q} vsrc }]]
       array_copy_to #dst #src #n @ stk; E
@@ -69,7 +87,7 @@ Section proof.
     iIntros "[Hvdst Hvsrc]".
     iApply "HΦ"; by iFrame.
   Qed.
-  Theorem wp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
+  Lemma wp_array_copy_to stk E (dst src : loc) vdst vsrc q (n : Z) :
     Z.of_nat (length vdst) = n → Z.of_nat (length vsrc) = n →
     {{{ dst ↦∗ vdst ∗ src ↦∗{q} vsrc }}}
       array_copy_to #dst #src #n @ stk; E
@@ -79,7 +97,7 @@ Section proof.
     iApply (twp_array_copy_to with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ".
   Qed.
 
-  Theorem twp_array_clone stk E l q vl n :
+  Lemma twp_array_clone stk E l q vl n :
     Z.of_nat (length vl) = n →
     (0 < n)%Z →
     [[{ l ↦∗{q} vl }]]
@@ -96,7 +114,7 @@ Section proof.
       wp_pures.
       iApply "HΦ"; by iFrame.
   Qed.
-  Theorem wp_array_clone stk E l q vl n :
+  Lemma wp_array_clone stk E l q vl n :
     Z.of_nat (length vl) = n →
     (0 < n)%Z →
     {{{ l ↦∗{q} vl }}}
@@ -107,4 +125,149 @@ Section proof.
     iApply (twp_array_clone with "H"); [auto..|]; iIntros (l') "H HΦ". by iApply "HΦ".
   Qed.
 
+  Section array_init.
+    Context (Q : nat → val → iProp Σ).
+    Implicit Types (f v : val) (i j : nat).
+
+    Local 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_apply (wp_wand with "Hf"); iIntros (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.
+    Local Lemma twp_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_apply (twp_wand with "Hf"); iIntros (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.
+
+    Lemma wp_array_init stk E n f :
+      (0 < n)%Z →
+      {{{
+        [∗ list] i ∈ seq 0 (Z.to_nat n), WP f #(i : nat) @ stk; E {{ Q i }}
+      }}}
+        array_init #n f @ stk; E
+      {{{ l vs, RET #l;
+        ⌜Z.of_nat (length vs) = n⌝ ∗ l ↦∗ vs ∗ [∗ list] k↦v ∈ vs, Q k v
+      }}}.
+    Proof.
+      iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
+      wp_apply (wp_array_init_loop _ _ _ 0 n (Z.to_nat n)
+        with "[Hl $Hf] [HΦ]"); first lia.
+      { by rewrite loc_add_0. }
+      iIntros "!>" (vs). iDestruct 1 as (?) "[Hl Hvs]". wp_pures.
+      iApply ("HΦ" $! _ vs). iSplit; [iPureIntro; lia|].
+      rewrite loc_add_0. iFrame.
+    Qed.
+    Lemma twp_array_init stk E n f :
+      (0 < n)%Z →
+      [[{
+        [∗ list] i ∈ seq 0 (Z.to_nat n), WP f #(i : nat) @ stk; E [{ Q i }]
+      }]]
+        array_init #n f @ stk; E
+      [[{ l vs, RET #l;
+        ⌜Z.of_nat (length vs) = n⌝ ∗ l ↦∗ vs ∗ [∗ list] k↦v ∈ vs, Q k v
+      }]].
+    Proof.
+      iIntros (Hn Φ) "Hf HΦ". wp_lam. wp_alloc l as "Hl"; first done.
+      wp_apply (twp_array_init_loop _ _ _ 0 n (Z.to_nat n)
+        with "[Hl $Hf] [HΦ]"); first lia.
+      { by rewrite loc_add_0. }
+      iIntros (vs). iDestruct 1 as (?) "[Hl Hvs]". wp_pures.
+      iApply ("HΦ" $! _ vs). iSplit; [iPureIntro; lia|].
+      rewrite loc_add_0. iFrame.
+    Qed.
+  End array_init.
+
+  Section array_init_fmap.
+    Context {A} (g : A → val) (Q : nat → A → iProp Σ).
+    Implicit Types (xs : list A) (f : val).
+
+    Local Lemma big_sepL_exists_eq vs :
+      ([∗ list] k↦v ∈ vs, ∃ x, ⌜v = g x⌝ ∗ Q k x) -∗
+      ∃ xs, ⌜ vs = g <$> xs ⌝ ∗ [∗ list] k↦x ∈ xs, Q k x.
+    Proof.
+      iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (Q); simpl.
+      { iExists []. by auto. }
+      iDestruct "Hvs" as "[Hv Hvs]"; iDestruct "Hv" as (x ->) "Hv".
+      iDestruct ("IH" with "Hvs") as (xs ->) "Hxs".
+      iExists (x :: xs). by iFrame.
+    Qed.
+
+    Lemma wp_array_init_fmap stk E n f :
+      (0 < n)%Z →
+      {{{
+        [∗ list] i ∈ seq 0 (Z.to_nat n),
+          WP f #(i : nat) @ stk; E {{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }}
+      }}}
+        array_init #n f @ stk; E
+      {{{ l xs, RET #l;
+        ⌜Z.of_nat (length xs) = n⌝ ∗ l ↦∗ (g <$> xs) ∗ [∗ list] k↦x ∈ xs, Q k x
+      }}}.
+    Proof.
+      iIntros (Hn Φ) "Hf HΦ". iApply (wp_array_init with "Hf"); first done.
+      iIntros "!>" (l vs). iDestruct 1 as (<-) "[Hl Hvs]".
+      iDestruct (big_sepL_exists_eq with "Hvs") as (xs ->) "Hxs".
+      iApply "HΦ". iFrame "Hl Hxs". by rewrite fmap_length.
+    Qed.
+    Lemma twp_array_init_fmap stk E n f :
+      (0 < n)%Z →
+      [[{
+        [∗ list] i ∈ seq 0 (Z.to_nat n),
+          WP f #(i : nat) @ stk; E [{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }]
+      }]]
+        array_init #n f @ stk; E
+      [[{ l xs, RET #l;
+        ⌜Z.of_nat (length xs) = n⌝ ∗ l ↦∗ (g <$> xs) ∗ [∗ list] k↦x ∈ xs, Q k x
+      }]].
+    Proof.
+      iIntros (Hn Φ) "Hf HΦ". iApply (twp_array_init with "Hf"); first done.
+      iIntros (l vs). iDestruct 1 as (<-) "[Hl Hvs]".
+      iDestruct (big_sepL_exists_eq with "Hvs") as (xs ->) "Hxs".
+      iApply "HΦ". iFrame "Hl Hxs". by rewrite fmap_length.
+    Qed.
+  End array_init_fmap.
 End proof.