Commit a96494d6 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Finalized List sort example, and introduced list encodings

parent 1b9fc4de
-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
......@@ -18,3 +15,4 @@ theories/examples/proofs.v
theories/examples/proofs_enc.v
theories/examples/branching_examples.v
theories/examples/branching_proofs.v
theories/examples/list_sort.v
......@@ -70,7 +70,7 @@ Section channel.
Context `{!heapG Σ, !chanG Σ} (N : namespace).
Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
( l':loc, hd : val, l = #l' l' hd is_list hd xs)%I.
( l':loc, l = #l' l' encode xs)%I.
Record chan_name := Chan_name {
chan_lock_name : gname;
......@@ -119,8 +119,8 @@ Section channel.
Proof.
iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (ls Hls). wp_alloc l as "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (rs Hrs). wp_alloc r as "Hr".
wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl [])))
as (lsγ) "[Hls Hls']"; first done.
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl [])))
......@@ -164,8 +164,9 @@ Section channel.
wp_apply get_side_spec; wp_pures.
iDestruct (chan_inv_alt s with "Hinv") as
(vs ws) "(Href & Hvs & Href' & Hws)".
iDestruct "Href" as (ll lhd Hslr) "(Hll & Hlvs)"; rewrite Hslr.
wp_load. wp_apply (lsnoc_spec with "Hlvs"). iIntros (lhd' Hlvs).
iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
wp_load.
wp_apply (lsnoc_spec (T:=val))=> //; iIntros (_).
wp_bind (_ <- _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
......@@ -174,7 +175,7 @@ Section channel.
iModIntro.
wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
iApply (chan_inv_alt s).
rewrite /is_list_ref. eauto 10 with iFrame.
rewrite /is_list_ref. eauto 20 with iFrame.
Qed.
Lemma try_recv_spec Φ E γ c s :
......@@ -193,22 +194,20 @@ Section channel.
wp_apply dual_side_spec. wp_apply get_side_spec; wp_pures.
iDestruct (chan_inv_alt (dual_side s) with "Hinv") as
(vs ws) "(Href & Hvs & Href' & Hws)".
iDestruct "Href" as (ll lhd Hslr) "(Hll & Hlvs)"; rewrite Hslr.
iDestruct "Href" as (ll Hslr) "Hll"; rewrite Hslr.
wp_bind (! _)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
wp_load.
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
destruct vs as [|v vs]; simpl.
- iDestruct "Hlvs" as %->.
iDestruct "HΦ" as "[HΦ _]".
- iDestruct "HΦ" as "[HΦ _]".
iMod ("HΦ" with "[//] Hchan") as "HΦ".
iModIntro.
wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
{ iApply (chan_inv_alt (dual_side s)).
rewrite /is_list_ref. eauto 10 with iFrame. }
iIntros (_). wp_pures. by iApply "HΦ".
- iDestruct "Hlvs" as %(hd' & -> & Hhd').
iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
- iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
iDestruct "HΦ" as "[_ HΦ]".
iMod ("HΦ" with "[//] Hchan") as "HΦ".
iModIntro. wp_store.
......
......@@ -64,3 +64,14 @@ Proof.
- intros.
apply decenc. eauto.
Qed.
Lemma enc_inj {A : Type} `{ED : EncDec A}
x y : encode x = encode y -> x = y.
Proof.
intros Heq.
assert (decode (encode x) = decode (encode y)).
{ by f_equiv. }
erewrite encdec in H=> //.
erewrite encdec in H=> //.
by inversion H.
Qed.
\ No newline at end of file
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 (hd : val) (xs : list val) : 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
| [] => hd = NONEV
| x :: xs => hd', hd = SOMEV (x,hd') is_list hd' xs
| [] => encode None
| x :: xs => encode (Some (x,xs))
end.
Definition lnil : val := λ: <>, NONEV.
......@@ -65,134 +74,110 @@ Definition lsnoc : val :=
Section lists.
Context `{heapG Σ}.
Implicit Types i : nat.
Implicit Types v : val.
Context `{EncDec T}.
Implicit Types x : T.
Implicit Types xs : list T.
Lemma lnil_spec :
{{{ True }}}
lnil #()
{{{ hd, RET hd; is_list hd [] }}}.
{{{ True }}} lnil #() {{{ RET encode []; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
Lemma lcons_spec hd vs v :
{{{ is_list hd vs }}}
lcons v hd
{{{ hd', RET hd'; is_list hd' (v :: vs) }}}.
Proof.
iIntros (Φ ?) "HΦ". wp_lam. wp_pures.
iApply "HΦ". simpl; eauto.
Qed.
Lemma lcons_spec x xs :
{{{ True }}} lcons (encode x) (encode xs) {{{ RET (encode (x :: xs)); True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma lhead_spec x xs:
{{{ True }}} lhead (encode (x::xs)) {{{ RET encode x; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma lhead_spec hd vs v :
{{{ is_list hd (v :: vs) }}}
lhead hd
{{{ RET v; True }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma ltail_spec hd vs v :
{{{ is_list hd (v :: vs) }}}
ltail hd
{{{ hd', RET hd'; is_list hd' vs }}}.
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma llookup_spec i hd vs v :
vs !! i = Some v
{{{ is_list hd vs }}}
llookup #i hd
{{{ RET v; True }}}.
Lemma ltail_spec x xs :
{{{ True }}} ltail (encode (x::xs)) {{{ RET encode xs; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma llookup_spec i xs x:
xs !! i = Some x
{{{ True }}}
llookup #i (encode xs)
{{{ RET encode x; True }}}.
Proof.
iIntros (Hi Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl);
iInduction xs as [|x' xs] "IH" forall (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_apply (ltail_spec with "[//]"); iIntros (?). 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 vs v :
is_Some (vs !! i)
{{{ is_list hd vs }}}
linsert #i v hd
{{{ hd', RET hd'; is_list hd' (<[i:=v]> vs) }}}.
Lemma linsert_spec i xs x :
is_Some (xs !! i)
{{{ True }}}
linsert #i (encode x) (encode xs)
{{{ RET encode (<[i:=x]>xs); True }}}.
Proof.
iIntros ([w Hi] Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl Φ);
iInduction xs as [|x' xs] "IH" forall (i Hi Hl Φ);
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_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_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
wp_apply ("IH" with "[//] [//]"). iIntros (?). wp_let.
wp_apply (lhead_spec with "[//]"); iIntros "_".
by wp_apply (lcons_spec with "[//]").
Qed.
Lemma llist_member_spec hd vs v :
{{{ is_list hd vs }}}
llist_member v hd
{{{ RET #(bool_decide (v vs)); True }}}.
Lemma llist_member_spec `{EqDecision T} (xs : list T) (x : T) :
{{{ True }}}
llist_member (encode x) (encode xs)
{{{ RET #(bool_decide (x xs)); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
iInduction xs as [|x' xs] "IH" forall (Hl); simplify_eq/=.
{ wp_lam; wp_pures. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam; wp_pures.
destruct (bool_decide_reflect (v' = v)) as [->|?]; wp_if.
{ rewrite (bool_decide_true (_ _ :: _)); last by left. by iApply "HΦ". }
wp_lam; wp_pures.
destruct (bool_decide_reflect (encode x' = encode x)) as [Heq|?]; wp_if.
{ apply enc_inj in Heq. rewrite Heq. rewrite (bool_decide_true (_ _ :: _)). by iApply "HΦ". by left. }
wp_proj. wp_let. iApply ("IH" with "[//]").
destruct (bool_decide_reflect (v vs)).
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 v :
Lemma lreplicate_spec i x :
{{{ True }}}
lreplicate #i v
{{{ hd, RET hd; is_list hd (replicate i v) }}}.
lreplicate #i (encode x)
{{{ RET encode (replicate i x); True }}}.
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 "[//]").
wp_apply "IH"; iIntros (Hl). wp_let. by iApply (lcons_spec with "[//]").
Qed.
Lemma llength_spec hd vs :
{{{ is_list hd vs }}} llength hd {{{ RET #(length vs); True }}}.
Lemma llength_spec xs :
{{{ True }}} llength (encode xs) {{{ RET #(length xs); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hl Φ); simplify_eq/=.
iInduction xs as [|x' xs] "IH" forall (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.
wp_lam. wp_match. wp_proj.
wp_apply ("IH" with "[//]"); iIntros "_ /=". wp_op.
rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed.
Lemma lsnoc_spec hd vs v :
{{{ is_list hd vs }}}
lsnoc hd v
{{{ hd', RET hd'; is_list hd' (vs++[v]) }}}.
Lemma lsnoc_spec xs x :
{{{ True }}} lsnoc (encode xs) (encode x) {{{ RET (encode (xs++[x])); True }}}.
Proof.
iIntros (Φ Hvs) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hvs Φ).
- simplify_eq/=.
wp_rec.
wp_pures.
wp_lam.
wp_pures.
iApply "HΦ". simpl. eauto.
- destruct Hvs as [vs' [-> Hvs']].
wp_rec.
wp_pures.
wp_bind (lsnoc vs' v).
iApply "IH".
eauto.
iNext.
iIntros (hd' Hhd').
wp_pures.
iApply lcons_spec.
eauto.
iApply "HΦ".
iInduction xs as [|x' xs] "IH" forall (Hvs Φ).
{ wp_rec. wp_pures. wp_lam. wp_pures. by iApply "HΦ". }
wp_rec.
wp_apply "IH"=> //.
iIntros (_). by wp_apply lcons_spec=> //.
Qed.
End lists.
\ No newline at end of file
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 *)
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
| [] => encode None
| x :: xs => encode (Some (x,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 x : T.
Implicit Types xs : list T.
Lemma lnil_spec :
{{{ True }}} lnil #() {{{ RET encode []; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
Lemma lcons_spec x xs :
{{{ True }}} lcons (encode x) (encode xs) {{{ RET (encode (x :: xs)); True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma lhead_spec x xs:
{{{ True }}} lhead (encode (x::xs)) {{{ RET encode x; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma ltail_spec x xs :
{{{ True }}} ltail (encode (x::xs)) {{{ RET encode xs; True }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
Lemma llookup_spec i xs x:
xs !! i = Some x
{{{ True }}}
llookup #i (encode xs)
{{{ RET encode x; True }}}.
Proof.
iIntros (Hi Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (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 (?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.
Lemma linsert_spec i xs x :
is_Some (xs !! i)
{{{ True }}}
linsert #i (encode x) (encode xs)
{{{ RET encode (<[i:=x]>xs); True }}}.
Proof.
iIntros ([w Hi] Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (i Hi Hl Φ);
destruct i as [|i]=> //; simplify_eq/=.
{ wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (?).
wp_let. by iApply (lcons_spec with "[//]"). }
wp_lam; wp_pures.
wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
wp_apply ("IH" with "[//] [//]"). iIntros (?). wp_let.
wp_apply (lhead_spec with "[//]"); iIntros "_".
by wp_apply (lcons_spec with "[//]").
Qed.
(* Lemma llist_member_spec `{EqDecision T} `{Inj T} (xs : list T) (x : T) : *)
(* {{{ True }}} *)
(* llist_member (encode x) (encode xs) *)
(* {{{ RET #(bool_decide (x ∈ xs)); True }}}. *)
(* Proof. *)
(* iIntros (Φ Hl) "HΦ". *)
(* iInduction xs as [|x' xs] "IH" forall (Hl); simplify_eq/=. *)
(* { wp_lam; wp_pures. by iApply "HΦ". } *)
(* wp_lam; wp_pures. *)
(* destruct (bool_decide_reflect (encode x' = encode x)) as [Heq|?]; wp_if. *)
(* { rewrite -Heq. inversion Heq. rewrite (bool_decide_true (_ ∈ _ :: _)). by iApply "HΦ". left. 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)
{{{ RET encode (replicate i x); True }}}.
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 (Hl). wp_let. by iApply (lcons_spec with "[//]").
Qed.
Lemma llength_spec xs :
{{{ True }}} llength (encode xs) {{{ RET #(length xs); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction xs as [|x' xs] "IH" forall (Hl Φ); simplify_eq/=.
{ wp_lam. wp_match. by iApply "HΦ". }
wp_lam. wp_match. wp_proj.
wp_apply ("IH" with "[//]"); iIntros "_ /=". wp_op.
rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed.
Lemma lsnoc_spec xs x :
{{{ True }}} lsnoc (encode xs) (encode x) {{{ RET (encode (xs++[x])); True }}}.
Proof.
iIntros (Φ Hvs) "HΦ".
iInduction xs as [|x' xs] "IH" forall (Hvs Φ).
{ wp_rec. wp_pures. wp_lam. wp_pures. by iApply "HΦ". }
wp_rec.
wp_apply "IH"=> //.
iIntros (_). by wp_apply lcons_spec=> //.
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 channel stype_enc.
From iris.base_logic Require Import invariants.
From stdpp Require Import sorting.
Require Import Coq.Lists.List.
Require Import Omega.
Section ListSortExample.
Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
Definition lsplit : val :=
λ: "xs",
let: "hd" := lhead "xs" in
let: "ys" := lcons "hd" NONEV in
let: "zs" := ltail "xs" in
("ys", "zs").
Lemma lsplit_spec (x : Z) (xs : list Z) :
{{{ True }}}
lsplit (encode (x::xs))
{{{ RET (encode [x],encode xs); True }}}.
Proof.
iIntros (Φ _) "HΦ".
wp_lam. wp_apply (lhead_spec (T := Z))=> //.
iIntros (_).
wp_apply (lcons_spec (T := Z) _ [])=> //.
iIntros (_).
wp_apply (ltail_spec (T := Z))=> //.
iIntros (_).
wp_pures.
by iApply "HΦ".
Qed.
Definition lsplit_ref : val :=
λ: "xs", let: "ys_zs" := lsplit !"xs" in
(ref (Fst "ys_zs"), ref (Snd ("ys_zs"))).
Lemma lsplit_ref_spec lxs (x : Z) (xs : list Z) :
{{{ lxs encode (x::xs) }}}
lsplit_ref #lxs
{{{ lys lzs ys zs, RET (#lys,#lzs);
(x::xs) = ys++zs