Commit 44cb36aa authored by Léon Gondelman's avatar Léon Gondelman

in-place linked-list reversal

parent ccec1584
......@@ -11,4 +11,5 @@ theories/c_translation/translation.v
theories/c_translation/derived.v
theories/tests/test1.v
theories/tests/fact.v
theories/tests/gcd.v
\ No newline at end of file
theories/tests/gcd.v
theories/tests/lists.v
\ No newline at end of file
......@@ -58,6 +58,20 @@ Section Derived.
iApply ("HΦ" with "[$Hl] [$Hr]").
Qed.
Definition a_move: val := λ: "x" "y",
a_store (a_ret "x") (a_load (a_ret "y")).
Lemma a_move_spec (s t :loc) (v w: val) R Φ :
s U v t U w ( t U w - s L w - Φ w) -
awp (a_move #s #t) R Φ.
Proof.
iIntros "(Hs & Ht & H)". do 2 awp_lam.
iApply a_store_ret. awp_load_ret t. iIntros "Ht".
iExists v. iFrame. iSpecialize ("H" with "Ht"). done.
Qed.
End Derived.
Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
Definition a_list_nil : val := λ:<>, a_ret NONEV.
Definition a_list_data : val := λ: "x",
a_bind (λ: "s",
match: "s" with
NONE => assert: #false
| SOME "l" => (a_bind (λ: "p", a_ret (Fst "p")) (a_load (a_ret "l")))
end) "x".
Definition a_list_next : val := λ: "x",
a_bind (λ: "s",
match: "s" with
NONE => assert: #false
| SOME "l" => (a_bind (λ: "p", a_ret (Snd "p")) (a_load (a_ret "l")))
end) "x".
Section list_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
match xs with
| [] => hd = NONEV
| x :: xs => (l:loc) hd', hd = SOMEV #l l U (x,hd') is_list hd' xs
end%I.
Lemma a_list_nil_spec R Φ:
(Φ NONEV) - awp (a_list_nil #()) R Φ.
Proof. iIntros "H"; awp_lam; by awp_ret_value. Qed.
Lemma a_list_next_spec (e: expr) R Φ :
awp e R (λ v,
(l:loc) hd x xs, v = SOMEV #l l U (x, hd) is_list hd xs
(l U (x, hd) - is_list hd xs - Φ hd)) -
awp (a_list_next e) R Φ.
Proof.
iIntros "H". rewrite/ a_list_next.
awp_apply (a_wp_awp R with "H").
- iIntros (v) "H". awp_lam. iApply awp_bind. iApply (awp_wand with "H").
iIntros (v0) "H". iDestruct "H" as (i hd x xs) "[-> [Hi [Hlst HΦ]]]".
awp_let. awp_match. iApply awp_bind.
awp_load_ret i. iIntros "Hi". iSpecialize ("HΦ" with "Hi Hlst").
awp_let. iApply awp_ret. wp_proj. iFrame.
Qed.
End list_spec.
Section InPlaceReversal.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
(*TODO: generalize the function below to set an arbitrary node in the list *)
Definition a_list_set_next : val := λ: "x" "y",
a_bind (λ: "xs",
match: "xs" with
NONE => assert: #false
| SOME "l" =>
a_bind (λ:"p",
a_bind ( λ: "r",
a_store (a_ret "l") (a_ret (Fst "p", "r")))
(a_load (a_ret "y")))
(a_load (a_ret "l"))
end)
(a_load (a_ret "x")).
Definition in_place_reverse : val := λ: "hd",
a_bind (λ: "i", a_bind (λ: "j",
a_while
(λ:<>, a_un_op NegOp (a_bin_op EqOp (a_load (a_ret "i")) (a_ret NONEV)))
(λ:<>, a_bind (λ: "k",
a_list_set_next "i" "j" ;;;;
a_move "j" "i" ;;;;
a_move "i" "k")
(a_alloc (a_list_next (a_load (a_ret "i"))))) ;;;;
(a_load (a_ret "j"))
) (a_alloc (a_ret NONEV))) (a_alloc (a_ret "hd")).
Lemma a_list_set_next_spec (i j hd : loc) (x v w: val) R Φ :
i U (SOMEV #hd) hd U (x, v) j U w
(i U (SOMEV #hd) - hd L (x, w) - j U w - Φ (x, w)%V) -
awp (a_list_set_next #i #j) R Φ.
Proof.
iIntros "(Hi & Hhd & Hj & HΦ)". rewrite/ a_list_set_next. do 2 awp_lam.
iApply awp_bind. awp_load_ret i. iIntros "Hi". awp_let. awp_match.
iApply awp_bind. awp_load_ret hd. iIntros "Hd". awp_let.
iApply awp_bind. awp_load_ret j. iIntros "Hj". awp_let.
iApply (a_store_spec _ _ (λ v, v = hd)%I (λ z, z = (x, w)%V )%I).
- awp_ret_value.
- awp_proj; awp_ret_value.
- iIntros (? ?) "-> ->". iExists (x, v)%V; iFrame. iIntros "Hd".
iApply ("HΦ" with "[$Hi] [$Hd] [$Hj]").
Qed.
Lemma in_place_reverse_spec (hd:val) xs R:
is_list hd xs -
awp (in_place_reverse hd) R (λ v, is_list v (reverse xs)).
Proof.
iIntros "Hlst". awp_lam.
iApply awp_bind; awp_alloc_ret i "Hi".
iApply awp_bind; awp_alloc_ret j "Hj".
iApply a_sequence_spec.
iApply (a_while_inv_spec ( ls rs rhd hd, i U hd is_list hd ls
j U rhd is_list rhd rs (reverse rs)++ls=xs)%I with "[Hlst Hj Hi]").
- iExists xs, [], (InjLV #()), hd; eauto with iFrame.
- iModIntro; iIntros "H". clear hd.
iDestruct "H" as (ls rs rhd hd) "(Hi & Hls & Hj & Hrs & %)".
iApply a_un_op_spec.
iApply (a_bin_op_spec _ _
(λ x, x = hd i U hd)%I (λ x, x = NONEV)%I with "[Hi] [] [-]").
{ awp_load_ret i. } { awp_ret_value. }
iIntros (? ?) "[-> Hi ] ->".
destruct ls.
+ rewrite{1}/ is_list. iDestruct "Hls" as "->".
iExists #true; iSplit; first done. iExists #false; iSplit; first done.
iLeft; iSplit; first done. do 2 iModIntro. awp_seq. awp_load_ret j.
iIntros "_". simplify_eq /=. by rewrite app_nil_r reverse_involutive.
+ iDestruct "Hls" as (l lnxt) "(-> & Hl & Hls)". fold is_list.
iExists #false; iSplit; first done; iExists #true; iSplit; first done.
iRight. iSplit; first done. iApply awp_bind.
iApply a_alloc_spec. iApply a_list_next_spec.
awp_load_ret i. iIntros "Hi". iExists l, lnxt, v, ls.
iSplit; first done. iFrame. iIntros "Hl Hls".
iIntros (k) "Hk". awp_let. iApply a_sequence_spec.
iApply (a_list_set_next_spec with "[$Hi $Hl $Hj Hls Hrs Hk]").
iIntros "Hi Hl Hj". iModIntro. awp_seq. iApply a_sequence_spec.
iApply (a_move_spec with "[$Hj $Hi Hls Hrs Hk Hl]").
iIntros "Hi Hj". iModIntro. awp_seq.
iApply (a_move_spec with "[$Hi $Hk Hls Hrs Hj Hl]").
iIntros "Hk Hi". iModIntro. iExists ls, (v :: rs), (InjRV #l), lnxt.
iFrame. iSplit.
* iExists l, rhd; iSplit; first done; iFrame.
* iPureIntro. simplify_eq. by rewrite cons_middle assoc -reverse_cons.
Qed.
End InPlaceReversal.
\ No newline at end of file
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