Commit 4ce5eb98 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

WIP list sort example

parent 44759644
-Q theories osiris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/utils/ordering.v
theories/utils/permutation.v
theories/typing/involutive.v
theories/typing/side.v
theories/typing/stype.v
theories/encodings/encodable.v
theories/encodings/list_enc.v
theories/encodings/list.v
theories/encodings/auth_excl.v
theories/encodings/channel.v
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.
From osiris Require Export encodable.
(** Immutable ML-style functional lists *)
Fixpoint is_list_enc `{EncDec T} (hd : val) (xs : list T) : Prop :=
match xs with
| [] => hd = NONEV
| x :: xs => hd', hd = SOMEV (encode x, hd') is_list_enc hd' xs
end.
Definition lnil : val := λ: <>, NONEV.
Definition lcons : val := λ: "x" "l", SOME ("x", "l").
Definition lhead : val := λ: "l",
match: "l" with
SOME "p" => Fst "p"
| NONE => assert: #false
end.
Definition ltail : val := λ: "l",
match: "l" with
SOME "p" => Snd "p"
| NONE => assert: #false
end.
Definition llookup : val :=
rec: "go" "n" "l" :=
if: "n" = #0 then lhead "l" else
let: "l" := ltail "l" in "go" ("n" - #1) "l".
Definition linsert : val :=
rec: "go" "n" "x" "l" :=
if: "n" = #0 then let: "l" := ltail "l" in lcons "x" "l" else
let: "k" := ltail "l" in
let: "k" := "go" ("n" - #1) "x" "k" in
lcons (lhead "l") "k".
Definition lreplicate : val :=
rec: "go" "n" "x" :=
if: "n" = #0 then lnil #() else
let: "l" := "go" ("n" - #1) "x" in lcons "x" "l".
Definition llist_member : val :=
rec: "go" "x" "l" :=
match: "l" with
NONE => #false
| SOME "p" =>
if: Fst "p" = "x" then #true
else let: "l" := (Snd "p") in "go" "x" "l"
end.
Definition llength : val :=
rec: "go" "l" :=
match: "l" with
NONE => #0
| SOME "p" => #1 + "go" (Snd "p")
end.
Definition lsnoc : val :=
rec: "go" "l" "x" :=
match: "l" with
SOME "p" => (lcons (Fst "p") ("go" (Snd "p") "x"))
| NONE => lcons "x" NONE
end.
Section lists.
Context `{heapG Σ}.
Implicit Types i : nat.
Context `{EncDec T}.
Implicit Types v : val.
Lemma lnil_spec :
{{{ True }}}
lnil #()
{{{ hd, RET hd; is_list_enc hd [] }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
Lemma lcons_spec hd xs x :
{{{ is_list_enc hd xs }}}
lcons (encode x) hd
{{{ 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:
{{{ is_list_enc hd (x :: xs) }}}
lhead hd
{{{ RET encode x; True }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma ltail_spec hd xs x :
{{{ is_list_enc hd (x :: xs) }}}
ltail hd
{{{ 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 :
xs !! i = Some x
{{{ is_list_enc hd xs }}}
llookup #i hd
{{{ RET encode x; True }}}.
Proof.
iIntros (Hi Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd i Hi Hl);
destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
wp_lam. wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.
Lemma linsert_spec i hd xs x :
is_Some (xs !! i)
{{{ is_list_enc hd xs }}}
linsert #i (encode x) hd
{{{ hd', RET hd'; is_list_enc hd' (<[i:=x]> xs) }}}.
Proof.
iIntros ([w Hi] Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd i Hi Hl Φ);
destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
wp_let. by iApply (lcons_spec with "[//]"). }
wp_lam; wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
wp_apply (lhead_spec with "[//]"); iIntros "_".
by wp_apply (lcons_spec with "[//]").
Qed.
Lemma llist_member_spec hd xs x :
{{{ is_list_enc hd xs }}}
llist_member (encode x) hd
{{{ RET #(bool_decide (x xs)); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd Hl); simplify_eq/=.
{ wp_lam; wp_pures. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam; wp_pures.
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Φ". }
wp_proj. wp_let. iApply ("IH" with "[//]").
destruct (bool_decide_reflect (x xs)).
- by rewrite bool_decide_true; last by right.
- by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
Qed.
Lemma lreplicate_spec i x :
{{{ True }}}
lreplicate #i (encode x)
{{{ hd, RET hd; is_list_enc hd (replicate i x) }}}.
Proof.
iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
{ wp_lam; wp_pures.
iApply (lnil_spec with "[//]"). iApply "HΦ". }
wp_lam; wp_pures.
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 "[//]").
Qed.
Lemma llength_spec hd xs :
{{{ is_list_enc hd xs }}} llength hd {{{ RET #(length xs); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd Hl Φ); simplify_eq/=.
{ wp_lam. wp_match. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam. wp_match. wp_proj.
wp_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op.
rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed.
Lemma lsnoc_spec hd xs x :
{{{ is_list_enc hd xs }}}
lsnoc hd (encode x)
{{{ hd', RET hd'; is_list_enc hd' (xs++[x]) }}}.
Proof.
iIntros (Φ Hvs) "HΦ".
iInduction xs as [|x' xs] "IH" forall (hd Hvs Φ).
- simplify_eq/=.
wp_rec.
wp_pures.
wp_lam.
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.
End lists.
\ No newline at end of file
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From osiris.typing Require Import side stype.
From osiris.encodings Require Import list_enc channel stype_enc.
From osiris.utils Require Import ordering permutation.
From iris.base_logic Require Import invariants.
Require Import Coq.Lists.List.
Require Import Omega.
Section ListSortExample.
Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
Definition lsort : val :=
λ: "hd", "hd".
Definition sorted (xs : list Z) : Prop :=
ordered () xs.
Definition sorted_hd (hd : val) (xs : list Z) : Prop :=
is_list_enc hd xs sorted xs.
Definition sorted_of (xs ys : list Z) : Prop :=
sorted xs permutation xs ys.
Definition sorted_of_hd (hd : val) (xs ys : list Z) : Prop :=
is_list_enc hd xs sorted_of xs ys.
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.
Definition sorted_ref (hd : val) (xs : list Z) : iProp Σ :=
(is_list_enc_ref hd xs sorted xs)%I.
Definition sorted_of_ref (hd : val) (xs ys : list Z) : iProp Σ :=
(is_list_enc_ref hd xs sorted_of xs ys)%I.
Definition lsplit : val :=
λ: "xs",
let: "hd" := lhead !"xs" in
let: "ys" := lcons "hd" NONEV in
let: "zs" := ltail !"xs" in
(ref "ys",ref "zs").
Lemma lsplit_spec (hdx : val) (xs : list Z) :
{{{ is_list_enc_ref hdx xs ( x xs', xs = x::xs')}}}
lsplit hdx
{{{ hdy hdz ys zs, RET (hdy,hdz);
is_list_enc_ref hdx xs is_list_enc_ref hdy ys is_list_enc_ref hdz zs xs = ys++zs }}}.
Proof.
iIntros (Φ) "[Hhd Heq] HΦ".
iDestruct "Heq" as %(x & xs' & ->).
iDestruct "Hhd" as (l hd ->) "[Hlxs Hhd]".
iDestruct "Hhd" as %Hhd.
wp_lam.
wp_load.
wp_apply (lhead_spec (T := Z) hd)=> //.
iIntros "_".
wp_pures.
wp_apply (lcons_spec (T := Z) _ [])=> //.
iIntros (ys Hys).
wp_load.
wp_apply (ltail_spec (T := Z))=> //.
iIntros (zs Hzs).
wp_alloc lzs as "Hlzs".
wp_alloc lys as "Hlys".
wp_pures.
iApply "HΦ".
iFrame.
rewrite /is_list_enc_ref.
iSplitL "Hlxs". eauto 10 with iFrame.
iSplitL "Hlys". eauto 10 with iFrame.
iSplitL "Hlzs". eauto 10 with iFrame.
eauto.
Qed.
Definition compare_vals : val :=
λ: "x" "y", "x" "y".
Lemma compare_vals_spec (x y : Z) :
{{{ True%I }}}
compare_vals (encode x) (encode y)
{{{ RET (encode (bool_decide (x y))); True%I }}}.
Proof.
iIntros (Φ) "_ HΦ".
wp_lam.
wp_pures.
by iApply "HΦ".
Qed.
Definition lmerge : val :=
rec: "go" "hys" "hzs" :=
if: llength "hys" = #0
then "hzs"
else if: llength "hzs" = #0
then "hys"
else let: "y" := lhead "hys" in
let: "z" := lhead "hzs" in
if: (compare_vals "y" "z")
then lcons "y" ("go" (ltail "hys") "hzs")
else lcons "z" ("go" "hys" (ltail "hzs")).
Lemma lmerge_spec hdy hdz (ys zs : list Z) :
{{{ sorted_hd hdy ys sorted_hd hdz zs }}}
lmerge hdy hdz
{{{ hxs xs, RET hxs; sorted_of_hd hxs xs (ys++zs) }}}.
Proof.
revert hdy hdz ys zs.
iLöb as "IH".
iIntros (hdy hdz ys zs).
iIntros (Φ [[Hhdy Hhdy_sorted] [Hhdz Hhdz_sorted]]) "HΦ".
wp_lam.
wp_pures.
wp_apply (llength_spec (T:=Z))=> //.
iIntros "_".
destruct ys as [|y ys].
{
simpl. wp_pures.
iApply ("HΦ" $!hdz zs) => //. simpl.
iSplit=> //.
iPureIntro. rewrite /sorted_of. split=> //. apply permutation_refl.
}
wp_pures.
wp_bind (llength _).
wp_apply (llength_spec (T:=Z))=> //.
iIntros "_".
destruct zs as [|z zs].
{
simpl. wp_pures.
iApply ("HΦ" $!hdy (y::ys)) => //. repeat rewrite app_nil_r. simpl.
iSplit=> //.
iPureIntro. rewrite /sorted_of. split=> //. apply permutation_refl.
}
wp_pures.
wp_apply (lhead_spec (T:=Z))=> //.
iIntros "_".
wp_apply (lhead_spec (T:=Z))=> //.
iIntros "_".
wp_pures.
wp_apply (compare_vals_spec)=> //.
iIntros "_".
wp_pures.
destruct (bool_decide (y z)).
- wp_pures.
wp_apply (ltail_spec (T:=Z))=> //.
iIntros (hdy' Hhdy').
wp_apply ("IH")=> //. rewrite /sorted_hd. iSplit; iSplit=>//. iPureIntro. eapply ordered_cons=> //.
iIntros (hxs xs [Hhxs [Hhxs_sorted Hhxs_of]]).
wp_apply (lcons_spec (T:=Z))=> //.
iIntros (hd Hhd).
iApply ("HΦ").
iPureIntro.
admit.
- wp_pures.
wp_apply (ltail_spec (T:=Z))=> //.
iIntros (hdz' Hhdz').
wp_apply ("IH")=> //. rewrite /sorted_hd. iSplit; iSplit=>//. iPureIntro. eapply ordered_cons=> //.
iIntros (hxs xs [Hhxs [Hhxs_sorted Hhxs_of]]).
wp_apply (lcons_spec (T:=Z))=> //.
iIntros (hd Hhd).
iApply ("HΦ").
iPureIntro.
admit.
Admitted.
Definition lmerge_ref : val :=
λ: "lxs" "hys" "hzs",
"lxs" <- lmerge "hys" "hzs".
Lemma lmerge_ref_spec (ldx hdy hdz : val) xs ys zs ys' zs' :
{{{ sorted_of_hd hdy ys' ys
sorted_of_hd hdz zs' zs
xs = ys++zs
is_list_enc_ref ldx xs }}}
lmerge_ref ldx hdy hdz
{{{ xs', RET #(); sorted_of_ref ldx xs' xs }}}.
Proof.
iIntros (Φ) "HPre HΦ".
iDestruct "HPre" as ([Hhdy [Hys_sorted Hys_perm]]
[Hhdz [Hzs_sorted Hzs_perm]] Heq)
"Hldx".
iDestruct "Hldx" as (l hd ->) "[Hl Hldx]".
wp_lam.
wp_apply (lmerge_spec hdy hdz ys' zs')=> //.
iIntros (hxs xs') "Hhxs".
iDestruct "Hhxs" as %(Hhxs & Hhys & HHzs).
wp_store.
iApply ("HΦ" $!xs').
rewrite /sorted_of_ref /sorted_of /is_list_enc_ref.
iSplit.
- eauto 10 with iFrame.
- rewrite Heq. iPureIntro.
split=> //.
eapply permutation_trans=> //.
apply permutation_app3=> //.
Qed.
Definition list_sort_service : val :=
rec: "go" "c" :=
let: "xs" := recv "c" #Right in
if: llength (!"xs") #1
then send "c" #Right "xs"
else let: "ys_zs" := lsplit "xs" in
let: "ys" := Fst "ys_zs" in
let: "zs" := Snd "ys_zs" in
let: "cy" := new_chan #() in Fork("go" "cy");;
let: "cz" := new_chan #() in Fork("go" "cz");;
send "cy" #Left "ys";;
send "cz" #Left "zs";;
let: "ys" := recv "cy" #Left in
let: "zs" := recv "cz" #Left in
lmerge_ref "xs" !"ys" !"zs";;
send "c" #Right "xs".
Lemma list_sort_service_spec γ c xs :
{{{ c @ Right : (<?> hd @ is_list_enc_ref hd xs,
<!> hd' @
hd = hd' ( ys : list Z, sorted_of_ref hd' ys xs),
TEnd) {N,γ} }}}
list_sort_service c
{{{ RET #(); c @ Right : TEnd {N,γ} }}}.
Proof.
revert γ c xs.
iLöb as "IH".
iIntros (γ c xs Φ) "Hstr HΦ".
wp_lam.
wp_apply (recv_st_spec N val with "Hstr").
iIntros (v) "Hstr".
iDestruct "Hstr" as "[Hstr HP]".
wp_pures.
iDestruct "HP" as (l hd' ->) "[Hl Hhd']".
wp_load.
iDestruct ("Hhd'") as %Hhd'.
destruct xs.
+ rewrite /is_list_ref.
wp_apply (llength_spec (T:=Z))=> //.
iIntros "_".
wp_pures.
wp_apply (send_st_spec N val with "[Hl Hstr]")=> //. iFrame.
iSplit=> //.
rewrite /(sorted_of_ref #l). rewrite /(is_list_enc_ref #l).
iExists _.
iSplit; first by eauto 10 with iFrame.
iPureIntro.
split; constructor.
iIntros "Hstr".
by iApply "HΦ".
+ destruct xs.
* rewrite /is_list_ref.
wp_apply (llength_spec (T:=Z))=> //.
iIntros "_".
wp_pures.
wp_apply (send_st_spec N val with "[Hl Hstr]")=> //. iFrame.
iSplit=> //.
rewrite /(sorted_of_ref #l). rewrite /(is_list_enc_ref #l).
iExists _.
iSplit; first by eauto 10 with iFrame.
iPureIntro.
split; [ constructor | apply permutation_cons; constructor ].
iIntros "Hstr".
by iApply "HΦ".
* wp_apply (llength_spec (T:=Z))=> //.
iIntros "_".
wp_pures.
assert (bool_decide (S (S (length xs)) 1) = false).
{ apply bool_decide_false. lia. }
rewrite H0.
wp_pures.
wp_apply (lsplit_spec with "[Hl]").
rewrite /(is_list_enc_ref (encode #l)). eauto 10 with iFrame.
iIntros (hdy hdz ys zs) "(Hhdx & Hhdy & Hhdz & Heq)".
wp_pures.
iDestruct "Hhdy" as (ly hdy' ->) "[Hhdy Hhdys]".
iDestruct "Hhdys" as %Hhdys.
iDestruct "Hhdz" as (lz hdz' ->) "[Hhdz Hhdzs]".
iDestruct "Hhdzs" as %Hhdzs.
iDestruct "Heq" as %->.
wp_apply (new_chan_st_spec N
(<!> hd @ is_list_enc_ref hd ys,
<?> hd' @ (hd = hd' ys',
sorted_of_ref hd' ys' ys)%I, TEnd))=>//;
iIntros (cy γy) "[Hstly Hstry]".
wp_apply (wp_fork with "[Hstry]").
{ iApply ("IH" with "Hstry"). iNext. iNext. iIntros "Hstry". done. }
wp_apply (new_chan_st_spec N
(<!> hd @ is_list_enc_ref hd zs,
<?> hd' @ (hd = hd' zs',
sorted_of_ref hd' zs' zs)%I, TEnd))=>//;
iIntros (cz γz) "[Hstlz Hstrz]".
wp_apply (wp_fork with "[Hstrz]").
{ iApply ("IH" with "Hstrz"). iNext. iNext. iIntros "Hstrz". done. }
wp_apply (send_st_spec N val with "[Hhdy Hstly]"). iFrame.
{ rewrite /is_list_enc_ref.
iExists _, _. iSplit=> //. iFrame.
eauto 10 with iFrame. }
iIntros "Hstly".
wp_apply (send_st_spec N val with "[Hhdz Hstlz]"). iFrame.
{ rewrite /is_list_enc_ref.
iExists _, _. iSplit=> //. iFrame.
eauto 10 with iFrame. }
iIntros "Hstlz".
wp_apply (recv_st_spec N val with "Hstly").
iIntros (hdy) "[Hstly Hys']".
iDestruct "Hys'" as (<-) "Hys'_sorted".
iDestruct "Hys'_sorted" as (ys') "[Hys' Hys'_sorted]".
iDestruct "Hys'_sorted" as %Hys'_sorted.
iDestruct "Hys'" as (ly' Hy' ->) "[Hlys' Hys']".
iDestruct "Hys'" as %Hys'.
wp_apply (recv_st_spec N val with "Hstlz").
iIntros (hdz) "[Hstlz Hzs']".
iDestruct "Hzs'" as (<-) "Hzs'_sorted".
iDestruct "Hzs'_sorted" as (zs') "[Hzs' Hzs'_sorted]".
iDestruct "Hzs'_sorted" as %Hzs'_sorted.
iDestruct "Hzs'" as (lz' Hz' ->) "[Hlzs' Hzs']".
iDestruct "Hzs'" as %Hzs'.
wp_load.
wp_load.
wp_apply (lmerge_ref_spec with "[Hhdx]")=> //.
iFrame. rewrite /sorted_hd. eauto 10 with iFrame.
iIntros (xs') "Hxs'_sorted".
wp_apply (send_st_spec N val with "[Hstr Hxs'_sorted]"). iFrame.
eauto 10 with iFrame.
iIntros "Hstr".
by iApply "HΦ".
Qed.
Definition list_sort : val :=
λ: "xs",
let: "c" := new_chan #() in
Fork(list_sort_service "c");;
send "c" #Left "xs";;