Commit 1b9fc4de authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

WIP List sort example

parent 4ce5eb98
...@@ -3,10 +3,18 @@ From iris.heap_lang Require Import assert. ...@@ -3,10 +3,18 @@ From iris.heap_lang Require Import assert.
From osiris Require Export encodable. From osiris Require Export encodable.
(** Immutable ML-style functional lists *) (** Immutable ML-style functional lists *)
Fixpoint is_list_enc `{EncDec T} (hd : val) (xs : list T) : Prop := Instance pair_encodable `{Encodable A, Encodable B} : Encodable (A * B) :=
λ p, (encode p.1, encode p.2)%V.
Instance option_encodable `{Encodable A} : Encodable (option A) := λ mx,
match mx with Some x => SOMEV (encode x) | None => NONEV end%V.
Instance list_encodable `{Encodable A} : Encodable (list A) :=
fix go xs :=
let _ : Encodable _ := @go in
match xs with match xs with
| [] => hd = NONEV | [] => encode None
| x :: xs => hd', hd = SOMEV (encode x, hd') is_list_enc hd' xs | x :: xs => encode (Some (x,xs))
end. end.
Definition lnil : val := λ: <>, NONEV. Definition lnil : val := λ: <>, NONEV.
...@@ -67,135 +75,109 @@ Section lists. ...@@ -67,135 +75,109 @@ Section lists.
Context `{heapG Σ}. Context `{heapG Σ}.
Implicit Types i : nat. Implicit Types i : nat.
Context `{EncDec T}. Context `{EncDec T}.
Implicit Types v : val. Implicit Types x : T.
Implicit Types xs : list T.
Lemma lnil_spec : Lemma lnil_spec :
{{{ True }}} {{{ True }}} lnil #() {{{ RET encode []; True }}}.
lnil #()
{{{ hd, RET hd; is_list_enc hd [] }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed. Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
Lemma lcons_spec hd xs x : Lemma lcons_spec x xs :
{{{ is_list_enc hd xs }}} {{{ True }}} lcons (encode x) (encode xs) {{{ RET (encode (x :: xs)); True }}}.
lcons (encode x) hd Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
{{{ hd', RET hd'; is_list_enc hd' (x :: xs) }}}.
Proof.
iIntros (Φ ?) "HΦ". wp_lam. wp_pures.
iApply "HΦ". simpl; eauto 10.
Qed.
Lemma lhead_spec hd x xs: Lemma lhead_spec x xs:
{{{ is_list_enc hd (x :: xs) }}} {{{ True }}} lhead (encode (x::xs)) {{{ RET encode x; True }}}.
lhead hd Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
{{{ RET encode x; True }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma ltail_spec hd xs x : Lemma ltail_spec x xs :
{{{ is_list_enc hd (x :: xs) }}} {{{ True }}} ltail (encode (x::xs)) {{{ RET encode xs; True }}}.
ltail hd Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
{{{ hd', RET hd'; is_list_enc hd' xs }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma llookup_spec i hd xs x : Lemma llookup_spec i xs x:
xs !! i = Some x xs !! i = Some x
{{{ is_list_enc hd xs }}} {{{ True }}}
llookup #i hd llookup #i (encode xs)
{{{ RET encode x; True }}}. {{{ RET encode x; True }}}.
Proof. Proof.
iIntros (Hi Φ Hl) "HΦ". iIntros (Hi Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd i Hi Hl); iInduction xs as [|x' xs] "IH" forall (i Hi Hl);
destruct i as [|i]=> //; simplify_eq/=. destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). } { wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
wp_lam. wp_pures. wp_lam. wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let. wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH". wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed. Qed.
Lemma linsert_spec i hd xs x : Lemma linsert_spec i xs x :
is_Some (xs !! i) is_Some (xs !! i)
{{{ is_list_enc hd xs }}} {{{ True }}}
linsert #i (encode x) hd linsert #i (encode x) (encode xs)
{{{ hd', RET hd'; is_list_enc hd' (<[i:=x]> xs) }}}. {{{ RET encode (<[i:=x]>xs); True }}}.
Proof. Proof.
iIntros ([w Hi] Φ Hl) "HΦ". iIntros ([w Hi] Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd i Hi Hl Φ); iInduction xs as [|x' xs] "IH" forall (i Hi Hl Φ);
destruct i as [|i]=> //; simplify_eq/=. destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?). { wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (?).
wp_let. by iApply (lcons_spec with "[//]"). } wp_let. by iApply (lcons_spec with "[//]"). }
wp_lam; wp_pures. wp_lam; wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let. wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let. wp_apply ("IH" with "[//] [//]"). iIntros (?). wp_let.
wp_apply (lhead_spec with "[//]"); iIntros "_". wp_apply (lhead_spec with "[//]"); iIntros "_".
by wp_apply (lcons_spec with "[//]"). by wp_apply (lcons_spec with "[//]").
Qed. Qed.
Lemma llist_member_spec hd xs x : (* Lemma llist_member_spec `{EqDecision T} `{Inj T} (xs : list T) (x : T) : *)
{{{ is_list_enc hd xs }}} (* {{{ True }}} *)
llist_member (encode x) hd (* llist_member (encode x) (encode xs) *)
{{{ RET #(bool_decide (x xs)); True }}}. (* {{{ RET #(bool_decide (x ∈ xs)); True }}}. *)
Proof. (* Proof. *)
iIntros (Φ Hl) "HΦ". (* iIntros (Φ Hl) "HΦ". *)
iInduction xs as [|x' xs] "IH" forall (hd Hl); simplify_eq/=. (* iInduction xs as [|x' xs] "IH" forall (Hl); simplify_eq/=. *)
{ wp_lam; wp_pures. by iApply "HΦ". } (* { wp_lam; wp_pures. by iApply "HΦ". } *)
destruct Hl as (hd'&->&?). wp_lam; wp_pures. (* wp_lam; wp_pures. *)
destruct (bool_decide_reflect (encode x' = encode x)) as [Heq|?]; wp_if. (* destruct (bool_decide_reflect (encode x' = encode x)) as [Heq|?]; wp_if. *)
{ rewrite -Heq. inversion Heq. rewrite (bool_decide_true (_ _ :: _)); last by left. by iApply "HΦ". } (* { rewrite -Heq. inversion Heq. rewrite (bool_decide_true (_ ∈ _ :: _)). by iApply "HΦ". left. by left. by iApply "HΦ". } *)
wp_proj. wp_let. iApply ("IH" with "[//]"). (* wp_proj. wp_let. iApply ("IH" with "[//]"). *)
destruct (bool_decide_reflect (x xs)). (* destruct (bool_decide_reflect (x ∈ xs)). *)
- by rewrite bool_decide_true; last by right. (* - by rewrite bool_decide_true; last by right. *)
- by rewrite bool_decide_false ?elem_of_cons; last naive_solver. (* - by rewrite bool_decide_false ?elem_of_cons; last naive_solver. *)
Qed. (* Qed. *)
Lemma lreplicate_spec i x : Lemma lreplicate_spec i x :
{{{ True }}} {{{ True }}}
lreplicate #i (encode x) lreplicate #i (encode x)
{{{ hd, RET hd; is_list_enc hd (replicate i x) }}}. {{{ RET encode (replicate i x); True }}}.
Proof. Proof.
iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl. iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
{ wp_lam; wp_pures. { wp_lam; wp_pures.
iApply (lnil_spec with "[//]"). iApply "HΦ". } iApply (lnil_spec with "[//]"). iApply "HΦ". }
wp_lam; wp_pures. wp_lam; wp_pures.
rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]"). wp_apply "IH"; iIntros (Hl). wp_let. by iApply (lcons_spec with "[//]").
Qed. Qed.
Lemma llength_spec hd xs : Lemma llength_spec xs :
{{{ is_list_enc hd xs }}} llength hd {{{ RET #(length xs); True }}}. {{{ True }}} llength (encode xs) {{{ RET #(length xs); True }}}.
Proof. Proof.
iIntros (Φ Hl) "HΦ". iIntros (Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd Hl Φ); simplify_eq/=. iInduction xs as [|x' xs] "IH" forall (Hl Φ); simplify_eq/=.
{ wp_lam. wp_match. by iApply "HΦ". } { wp_lam. wp_match. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam. wp_match. wp_proj. wp_lam. wp_match. wp_proj.
wp_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op. wp_apply ("IH" with "[//]"); iIntros "_ /=". wp_op.
rewrite (Nat2Z.inj_add 1). by iApply "HΦ". rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed. Qed.
Lemma lsnoc_spec hd xs x : Lemma lsnoc_spec xs x :
{{{ is_list_enc hd xs }}} {{{ True }}} lsnoc (encode xs) (encode x) {{{ RET (encode (xs++[x])); True }}}.
lsnoc hd (encode x)
{{{ hd', RET hd'; is_list_enc hd' (xs++[x]) }}}.
Proof. Proof.
iIntros (Φ Hvs) "HΦ". iIntros (Φ Hvs) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd Hvs Φ). iInduction xs as [|x' xs] "IH" forall (Hvs Φ).
- simplify_eq/=. { wp_rec. wp_pures. wp_lam. wp_pures. by iApply "HΦ". }
wp_rec. wp_rec.
wp_pures. wp_apply "IH"=> //.
wp_lam. iIntros (_). by wp_apply lcons_spec=> //.
wp_pures.
iApply "HΦ". simpl. eauto 10.
- destruct Hvs as [vs' [-> Hvs']].
wp_rec.
wp_pures.
wp_bind (lsnoc vs' (encode x)).
iApply "IH".
eauto.
iNext.
iIntros (hd' Hhd').
wp_pures.
iApply lcons_spec.
eauto.
iApply "HΦ".
Qed. Qed.
End lists. End lists.
\ No newline at end of file
...@@ -17,23 +17,23 @@ Section ListSortExample. ...@@ -17,23 +17,23 @@ Section ListSortExample.
Definition sorted (xs : list Z) : Prop := Definition sorted (xs : list Z) : Prop :=
ordered () xs. ordered () xs.
Definition sorted_hd (hd : val) (xs : list Z) : Prop := (* Definition sorted_val (xs : val) : Prop := *)
is_list_enc hd xs sorted xs. (* sorted (encode xs). *)
Definition sorted_of (xs ys : list Z) : Prop := Definition sorted_of (xs ys : list Z) : Prop :=
sorted xs permutation xs ys. sorted xs permutation xs ys.
Definition sorted_of_hd (hd : val) (xs ys : list Z) : Prop := (* Definition sorted_of_hd (hd : val) (xs ys : list Z) : Prop := *)
is_list_enc hd xs sorted_of xs ys. (* is_list_enc hd xs ∧ sorted_of xs ys. *)
Definition is_list_enc_ref (l : val) (xs : list Z) : iProp Σ := Definition is_list_enc_ref (l : val) (xs : list Z) : iProp Σ :=
( l':loc, hd : val, l = #l' l' hd is_list_enc hd xs)%I. ( l':loc, l = #l' l' encode xs)%I.
Definition sorted_ref (hd : val) (xs : list Z) : iProp Σ := Definition sorted_ref (lxs : val) (xs : list Z) : iProp Σ :=
(is_list_enc_ref hd xs sorted xs)%I. (is_list_enc_ref lxs xs sorted xs)%I.
Definition sorted_of_ref (hd : val) (xs ys : list Z) : iProp Σ := Definition sorted_of_ref (lxs : val) (xs ys : list Z) : iProp Σ :=
(is_list_enc_ref hd xs sorted_of xs ys)%I. (is_list_enc_ref lxs xs sorted_of xs ys)%I.
Definition lsplit : val := Definition lsplit : val :=
λ: "xs", λ: "xs",
...@@ -42,31 +42,28 @@ Section ListSortExample. ...@@ -42,31 +42,28 @@ Section ListSortExample.
let: "zs" := ltail !"xs" in let: "zs" := ltail !"xs" in
(ref "ys",ref "zs"). (ref "ys",ref "zs").
Lemma lsplit_spec (hdx : val) (xs : list Z) : Lemma lsplit_spec (lxs : val) (x : Z ) (xs : list Z) :
{{{ is_list_enc_ref hdx xs ( x xs', xs = x::xs')}}} {{{ is_list_enc_ref lxs (x::xs) }}}
lsplit hdx lsplit lxs
{{{ hdy hdz ys zs, RET (hdy,hdz); {{{ lys lzs ys zs, RET (lys,lzs);
is_list_enc_ref hdx xs is_list_enc_ref hdy ys is_list_enc_ref hdz zs xs = ys++zs }}}. is_list_enc_ref lxs (x::xs) is_list_enc_ref lys ys is_list_enc_ref lzs zs (x::xs) = ys++zs }}}.
Proof. Proof.
iIntros (Φ) "[Hhd Heq] HΦ". iIntros (Φ) "Hhd HΦ".
iDestruct "Heq" as %(x & xs' & ->). iDestruct "Hhd" as (l ->) "Hlxs".
iDestruct "Hhd" as (l hd ->) "[Hlxs Hhd]".
iDestruct "Hhd" as %Hhd.
wp_lam. wp_lam.
wp_load. wp_load.
wp_apply (lhead_spec (T := Z) hd)=> //. wp_apply (lhead_spec (T := Z))=> //.
iIntros "_". iIntros "_".
wp_pures. wp_pures.
wp_apply (lcons_spec (T := Z) _ [])=> //. wp_apply (lcons_spec (T := Z) _ [])=> //.
iIntros (ys Hys). iIntros (_).
wp_load. wp_load.
wp_apply (ltail_spec (T := Z))=> //. wp_apply (ltail_spec (T := Z))=> //.
iIntros (zs Hzs). iIntros (_).
wp_alloc lzs as "Hlzs". wp_alloc lzs as "Hlzs".
wp_alloc lys as "Hlys". wp_alloc lys as "Hlys".
wp_pures. wp_pures.
iApply "HΦ". iApply "HΦ".
iFrame.
rewrite /is_list_enc_ref. rewrite /is_list_enc_ref.
iSplitL "Hlxs". eauto 10 with iFrame. iSplitL "Hlxs". eauto 10 with iFrame.
iSplitL "Hlys". eauto 10 with iFrame. iSplitL "Hlys". eauto 10 with iFrame.
...@@ -74,8 +71,8 @@ Section ListSortExample. ...@@ -74,8 +71,8 @@ Section ListSortExample.
eauto. eauto.
Qed. Qed.
Definition compare_vals : val := Definition compare_vals : val :=
λ: "x" "y", "x" "y". λ: "x" "y", "x" "y".
Lemma compare_vals_spec (x y : Z) : Lemma compare_vals_spec (x y : Z) :
{{{ True%I }}} {{{ True%I }}}
...@@ -88,6 +85,24 @@ Section ListSortExample. ...@@ -88,6 +85,24 @@ Section ListSortExample.
by iApply "HΦ". by iApply "HΦ".
Qed. Qed.
Definition my_lemma (xs ys zs : list Z) y z :
ordered Z.le xs ->
ordered Z.le (y::ys) ->
ordered Z.le (z::zs) ->
permutation xs (ys++(z::zs)) ->
y z ->
ordered Z.le (y::xs).
Proof. Admitted.
Definition my_lemma2 (xs ys zs : list Z) y z :
ordered Z.le xs ->
ordered Z.le (y::ys) ->
ordered Z.le (z::zs) ->
permutation xs ((y::ys)++zs) ->
z y ->
ordered Z.le (z::xs).
Proof. Admitted.
Definition lmerge : val := Definition lmerge : val :=
rec: "go" "hys" "hzs" := rec: "go" "hys" "hzs" :=
if: llength "hys" = #0 if: llength "hys" = #0
...@@ -100,15 +115,16 @@ Section ListSortExample. ...@@ -100,15 +115,16 @@ Section ListSortExample.
then lcons "y" ("go" (ltail "hys") "hzs") then lcons "y" ("go" (ltail "hys") "hzs")
else lcons "z" ("go" "hys" (ltail "hzs")). else lcons "z" ("go" "hys" (ltail "hzs")).
Lemma lmerge_spec hdy hdz (ys zs : list Z) : (* Change to just functional version of merge sort *)
{{{ sorted_hd hdy ys sorted_hd hdz zs }}} Lemma lmerge_spec (ys zs : list Z) :
lmerge hdy hdz {{{ sorted ys sorted zs }}}
{{{ hxs xs, RET hxs; sorted_of_hd hxs xs (ys++zs) }}}. lmerge (encode ys) (encode zs)
{{{ xs, RET (encode xs); sorted_of xs (ys++zs) }}}.
Proof. Proof.
revert hdy hdz ys zs. revert ys zs.
iLöb as "IH". iLöb as "IH".
iIntros (hdy hdz ys zs). iIntros (ys zs).
iIntros (Φ [[Hhdy Hhdy_sorted] [Hhdz Hhdz_sorted]]) "HΦ". iIntros (Φ [ys_sorted zs_sorted]) "HΦ".
wp_lam. wp_lam.
wp_pures. wp_pures.
wp_apply (llength_spec (T:=Z))=> //. wp_apply (llength_spec (T:=Z))=> //.
...@@ -116,74 +132,80 @@ Section ListSortExample. ...@@ -116,74 +132,80 @@ Section ListSortExample.
destruct ys as [|y ys]. destruct ys as [|y ys].
{ {
simpl. wp_pures. simpl. wp_pures.
iApply ("HΦ" $!hdz zs) => //. simpl. iApply ("HΦ" $!zs) => //. simpl.
iSplit=> //. iSplit=> //.
iPureIntro. rewrite /sorted_of. split=> //. apply permutation_refl. iPureIntro. apply permutation_refl.
} }
wp_pures. wp_pures.
wp_bind (llength _).
wp_apply (llength_spec (T:=Z))=> //. wp_apply (llength_spec (T:=Z))=> //.
iIntros "_". iIntros "_".
destruct zs as [|z zs]. destruct zs as [|z zs].
{ {
simpl. wp_pures. simpl. wp_pures.
iApply ("HΦ" $!hdy (y::ys)) => //. repeat rewrite app_nil_r. simpl. iApply ("HΦ" $!(y::ys)) => //. repeat rewrite app_nil_r. simpl.
iSplit=> //. iSplit=> //.
iPureIntro. rewrite /sorted_of. split=> //. apply permutation_refl. iPureIntro. apply permutation_refl.
} }
wp_pures.
wp_apply (lhead_spec (T:=Z))=> //. wp_apply (lhead_spec (T:=Z))=> //.
iIntros "_". iIntros "_".
wp_apply (lhead_spec (T:=Z))=> //. wp_apply (lhead_spec (T:=Z))=> //.
iIntros "_". iIntros "_".
wp_pures.
wp_apply (compare_vals_spec)=> //. wp_apply (compare_vals_spec)=> //.
iIntros "_". iIntros "_".
wp_pures. wp_pures.
destruct (bool_decide (y z)). destruct (bool_decide (y z)).
- wp_pures. - wp_pures.
wp_apply (ltail_spec (T:=Z))=> //. wp_apply (ltail_spec (T:=Z))=> //.
iIntros (hdy' Hhdy'). iIntros (_).
wp_apply ("IH")=> //. rewrite /sorted_hd. iSplit; iSplit=>//. iPureIntro. eapply ordered_cons=> //. wp_apply ("IH")=> //. rewrite /sorted.
iIntros (hxs xs [Hhxs [Hhxs_sorted Hhxs_of]]). iSplit=>//. iPureIntro. eapply ordered_cons=> //.
iIntros (xs [Hhxs_sorted Hhxs_of]).
wp_apply (lcons_spec (T:=Z))=> //. wp_apply (lcons_spec (T:=Z))=> //.
iIntros (hd Hhd). iIntros (_).
iApply ("HΦ"). iApply ("HΦ" $!(y::xs)).
iPureIntro. iPureIntro.
admit. simpl.
assert (y z). admit.
split=> //.
+ eapply my_lemma=> //.
+ by apply permutation_cons.
- wp_pures. - wp_pures.
wp_apply (ltail_spec (T:=Z))=> //. wp_apply (ltail_spec (T:=Z))=> //.
iIntros (hdz' Hhdz'). iIntros (_).
wp_apply ("IH")=> //. rewrite /sorted_hd. iSplit; iSplit=>//. iPureIntro. eapply ordered_cons=> //. wp_apply ("IH")=> //. rewrite /sorted. iSplit=>//. iPureIntro. eapply ordered_cons=> //.
iIntros (hxs xs [Hhxs [Hhxs_sorted Hhxs_of]]). iIntros (xs [Hhxs_sorted Hhxs_of]).
wp_apply (lcons_spec (T:=Z))=> //. wp_apply (lcons_spec (T:=Z))=> //.
iIntros (hd Hhd). iIntros (_).
iApply ("HΦ"). iApply ("HΦ").
iPureIntro. iPureIntro.
admit. simpl.
assert (z y). admit.
split=> //.
+ eapply (my_lemma2 xs ys zs)=> //.
+ apply permutation_sym. admit.
Admitted. Admitted.
Definition lmerge_ref : val := Definition lmerge_ref : val :=
λ: "lxs" "hys" "hzs", λ: "lxs" "hys" "hzs",
"lxs" <- lmerge "hys" "hzs". "lxs" <- lmerge "hys" "hzs".
Lemma lmerge_ref_spec (ldx hdy hdz : val) xs ys zs ys' zs' : Lemma lmerge_ref_spec ldx xs ys zs ys' zs' :
{{{ sorted_of_hd hdy ys' ys {{{ sorted_of ys' ys
sorted_of_hd hdz zs' zs sorted_of zs' zs
xs = ys++zs xs = ys++zs
is_list_enc_ref ldx xs }}} is_list_enc_ref ldx xs }}}