list_reverse.v 1.72 KB
Newer Older
1 2 3 4 5 6
(** Correctness of in-place list reversal *)
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export hoare.
From iris.heap_lang Require Import proofmode notation.

Section list_reverse.
7
Context `{!heapG Σ}.
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
Notation iProp := (iPropG heap_lang Σ).
Implicit Types l : loc.

Fixpoint is_list (hd : val) (xs : list val) : iProp :=
  match xs with
  | [] => hd = NONEV
  | x :: xs =>  l hd', hd = SOMEV #l  l  (x,hd')  is_list hd' xs
  end%I.

Definition rev : val :=
  rec: "rev" "hd" "acc" :=
    match: "hd" with
      NONE => "acc"
    | SOME "l" =>
       let: "tmp1" := Fst !"l" in
       let: "tmp2" := Snd !"l" in
       "l" <- ("tmp1", "acc");;
       "rev" "tmp2" "hd"
    end.
Global Opaque rev.

Lemma rev_acc_wp hd acc xs ys (Φ : val  iProp) :
30
  heap_ctx  is_list hd xs  is_list acc ys 
31 32 33 34
    ( w, is_list w (reverse xs ++ ys) - Φ w)
   WP rev hd acc {{ Φ }}.
Proof.
  iIntros "(#Hh & Hxs & Hys & HΦ)".
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  iLöb (hd acc xs ys Φ) as "IH". wp_rec. wp_let.
36 37 38 39 40 41 42 43 44 45
  destruct xs as [|x xs]; iSimplifyEq.
  - wp_match. by iApply "HΦ".
  - iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
    wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
    iApply ("IH" $! hd' (SOMEV #l) xs (x :: ys) with "Hxs [Hx Hys]"); simpl.
    { iExists l, acc; by iFrame. }
    iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
Qed.

Lemma rev_wp hd xs (Φ : val  iProp) :
46
  heap_ctx  is_list hd xs  ( w, is_list w (reverse xs) - Φ w)
47 48 49 50 51 52 53
   WP rev hd (InjL #()) {{ Φ }}.
Proof.
  iIntros "(#Hh & Hxs & HΦ)".
  iApply (rev_acc_wp hd NONEV xs []); iFrame "Hh Hxs".
  iSplit; first done. iIntros (w). rewrite right_id_L. iApply "HΦ".
Qed.
End list_reverse.