Merge branch 'add-array-copy' into 'master'

Add array_copy to heap_lang

Closes #293

See merge request iris/iris!379

CHANGELOG.md

@@ -71,7 +71,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 **Changes in heap_lang:**
 
 * Added a fraction to the heap_lang `array` assertion.
-
+* Added array_copy library for copying and cloning arrays.
 
 ## Iris 3.2.0 (released 2019-08-29)
 

_CoqProject

@@ -124,6 +124,7 @@ theories/heap_lang/lib/atomic_heap.v
 theories/heap_lang/lib/increment.v
 theories/heap_lang/lib/diverge.v
 theories/heap_lang/lib/arith.v
+theories/heap_lang/lib/array_copy.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v

theories/heap_lang/array.v

@@ -60,6 +60,11 @@ Proof.
   by setoid_rewrite Z.add_1_l.
 Qed.
 
+Global Instance array_cons_frame l q v vs R Q :
+  Frame false R (l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vs) Q →
+  Frame false R (l ↦∗{q} (v :: vs)) Q.
+Proof. by rewrite /Frame array_cons. Qed.
+
 Lemma update_array l q vs off v :
   vs !! off = Some v →
   l ↦∗{q} vs -∗ ((l +ₗ off) ↦{q} v ∗ ∀ v', (l +ₗ off) ↦{q} v' -∗ l ↦∗{q} <[off:=v']>vs).

theories/heap_lang/lib/array_copy.v

+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang array.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(** Implement [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. *)
+
+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).
+
+Definition array_clone: val :=
+  λ: "src" "n",
+    let: "dst" := AllocN "n" #() in
+    array_copy_to "dst" "src" "n";;
+    "dst".
+
+Section proof.
+  Context `{!heapG Σ}.
+
+  Theorem 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
+    [[{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{q} 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Φ". iFrame. }
+    iDestruct (array_cons with "Hdst") as "[Hv1 Hdst]".
+    iDestruct (array_cons with "Hsrc") as "[Hv2 Hsrc]".
+    wp_load; wp_store.
+    wp_apply ("IH" with "[%] [%] Hdst Hsrc"); [ lia .. | ].
+    iIntros "[Hvdst Hvsrc]".
+    iApply "HΦ"; by iFrame.
+  Qed.
+  Theorem 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
+    {{{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{q} 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.
+
+  Theorem twp_array_clone stk E l q vl n :
+    Z.of_nat (length vl) = n →
+    0 < n →
+    [[{ l ↦∗{q} vl }]]
+      array_clone #l #n @ stk; E
+    [[{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} vl }]].
+  Proof.
+    iIntros (Hvl Hn Φ) "Hvl HΦ".
+    wp_lam.
+    wp_alloc dst as "Hdst"; first by auto.
+    wp_apply (twp_array_copy_to with "[$Hdst $Hvl]").
+    - rewrite replicate_length Z2Nat.id; lia.
+    - auto.
+    - iIntros "[Hdst Hl]".
+      wp_pures.
+      iApply "HΦ"; by iFrame.
+  Qed.
+  Theorem wp_array_clone stk E l q vl n :
+    Z.of_nat (length vl) = n →
+    0 < n →
+    {{{ l ↦∗{q} vl }}}
+      array_clone #l #n @ stk; E
+    {{{ l', RET #l'; l' ↦∗ vl ∗ l ↦∗{q} 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.
+
+End proof.