Commit cfbfc0ad authored by Tej Chajed's avatar Tej Chajed Committed by Ralf Jung

Add array copying functions to heap_lang

Add array_copy_to (copy in-place to destination array) and array_clone
(copy to a freshly allocated array). The heap_lang spec and proof for
array_copy_to are inspired by
https://gitlab.mpi-sws.org/iris/lambda-rust/blob/3b4ae69fa3be1344245245bf05e5e80e790e064d/theories/lang/lib/memcpy.v.

Fixes #293.
parent 0072d1d8
......@@ -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)
......
......@@ -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
......
......@@ -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).
......
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment