Commit 9e81320c authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Major restructuring of project

parent b4843a6b
-Q theories osiris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/list.v
theories/auth_excl.v
theories/typing.v
theories/channel.v
theories/logrel.v
theories/examples.v
theories/encodable.v
theories/typing/involutive.v
theories/typing/side.v
theories/typing/stype.v
theories/encodings/list.v
theories/encodings/auth_excl.v
theories/encodings/channel.v
theories/encodings/stype.v
theories/encodings/stype_enc.v
theories/examples/examples.v
theories/examples/proofs.v
theories/examples/encoding_proofs.v
\ No newline at end of file
......@@ -64,4 +64,4 @@ Section auth_excl.
eapply exclusive_local_update. done. }
by rewrite own_op.
Qed.
End auth_excl.
End auth_excl.
\ No newline at end of file
......@@ -5,9 +5,8 @@ From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl auth list.
From iris.base_logic.lib Require Import auth.
From iris.heap_lang.lib Require Import spin_lock.
From osiris Require Import list.
From osiris Require Import auth_excl.
From osiris Require Import typing.
From osiris.typing Require Export side.
From osiris.encodings Require Import list auth_excl.
Set Default Proof Using "Type".
Import uPred.
......
......@@ -67,30 +67,42 @@ Context `{heapG Σ}.
Implicit Types i : nat.
Implicit Types v : val.
Lemma lnil_spec : {{{ True }}} lnil #() {{{ hd, RET hd; is_list hd [] }}}.
Lemma lnil_spec :
{{{ True }}}
lnil #()
{{{ hd, RET hd; is_list hd [] }}}.
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) }}}.
{{{ 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 lhead_spec hd vs v :
{{{ is_list hd (v :: vs) }}} lhead hd {{{ RET v; True }}}.
{{{ 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 }}}.
{{{ 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 }}}.
{{{ is_list hd vs }}}
llookup #i hd
{{{ RET v; True }}}.
Proof.
iIntros (Hi Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl); destruct i as [|i]=> //; simplify_eq/=.
iInduction vs as [|v' vs] "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.
......@@ -99,10 +111,13 @@ 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) }}}.
{{{ is_list hd vs }}}
linsert #i v hd
{{{ hd', RET hd'; is_list hd' (<[i:=v]> vs) }}}.
Proof.
iIntros ([w Hi] Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl Φ); destruct i as [|i]=> //; simplify_eq/=.
iInduction vs as [|v' vs] "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.
......@@ -114,7 +129,9 @@ Proof.
Qed.
Lemma llist_member_spec hd vs v :
{{{ is_list hd vs }}} llist_member v hd {{{ RET #(bool_decide (v vs)); True }}}.
{{{ is_list hd vs }}}
llist_member v hd
{{{ RET #(bool_decide (v vs)); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
......@@ -122,13 +139,16 @@ Proof.
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_proj. wp_let. iApply ("IH" with "[//]"). destruct (bool_decide_reflect (v vs)).
wp_proj. wp_let. iApply ("IH" with "[//]").
destruct (bool_decide_reflect (v vs)).
- 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 :
{{{ True }}} lreplicate #i v {{{ hd, RET hd; is_list hd (replicate i v) }}}.
{{{ True }}}
lreplicate #i v
{{{ hd, RET hd; is_list hd (replicate i v) }}}.
Proof.
iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
{ wp_lam; wp_pures.
......@@ -150,7 +170,9 @@ Proof.
Qed.
Lemma lsnoc_spec hd vs v :
{{{ is_list hd vs }}} lsnoc hd v {{{ hd', RET hd'; is_list hd' (vs++[v]) }}}.
{{{ is_list hd vs }}}
lsnoc hd v
{{{ hd', RET hd'; is_list hd' (vs++[v]) }}}.
Proof.
iIntros (Φ Hvs) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hvs Φ).
......@@ -171,6 +193,6 @@ Proof.
wp_pures.
iApply lcons_spec.
eauto.
iApply "HΦ".
iApply "HΦ".
Qed.
End lists.
\ No newline at end of file
......@@ -3,9 +3,11 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From osiris Require Import typing auth_excl channel.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
From osiris.typing Require Export stype.
From osiris.encodings Require Import auth_excl.
From osiris.encodings Require Export channel.
Class logrelG A Σ := {
logrelG_channelG :> chanG Σ;
......@@ -138,7 +140,8 @@ Section logrel.
((r = [] st_eval l stl str)
(l = [] st_eval r str stl)))%I.
Definition is_st (γ : st_name) (st : stype val (iProp Σ)) (c : val) : iProp Σ :=
Definition is_st (γ : st_name) (st : stype val (iProp Σ))
(c : val) : iProp Σ :=
(is_chan N (st_c_name γ) c inv N (inv_st γ c))%I.
Definition interp_st (γ : st_name) (st : stype val (iProp Σ))
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From osiris Require Import typing channel logrel.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
From osiris.encodings Require Export stype.
Class Encodable A := encode : A -> val.
Instance val_encodable : Encodable val := id.
......@@ -138,8 +138,8 @@ Section Encodings.
Lemma new_chan_st_enc_spec st :
{{{ True }}}
new_chan #()
{{{ c γ, RET c; c @ Left : (stype'_to_stype st) {γ}
c @ Right : (stype'_to_stype (dual_stype' st)) {γ} }}}.
{{{ c γ, RET c; c @ Left : (stype'_to_stype st) {γ}
c @ Right : (stype'_to_stype (dual_stype' st)) {γ} }}}.
Proof.
iIntros (Φ _) "HΦ".
iApply (new_chan_st_spec). eauto.
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From osiris Require Import typing channel logrel.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
From osiris Require Import encodable.
From osiris Require Import examples.
From osiris.encodings Require Import stype_enc.
From osiris.examples Require Import examples.
Section Encodings_Examples.
Section ExampleProofsEncodings.
Context `{!heapG Σ} {N : namespace}.
Context `{!logrelG val Σ}.
......@@ -116,4 +115,4 @@ Section Encodings_Examples.
by iApply "HΦ".
Qed.
End Encodings_Examples.
\ No newline at end of file
End ExampleProofsEncodings.
\ 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 Require Import typing channel logrel.
From osiris.typing Require Import side stype.
From osiris.encodings Require Import channel stype.
From iris.base_logic Require Import invariants.
Section Examples.
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From osiris Require Import typing channel logrel.
From iris.base_logic Require Import invariants.
From osiris Require Import examples.
From osiris.typing Require Import side stype.
From osiris.encodings Require Import stype.
From osiris.examples Require Import examples.
Section ExampleProofs.
Context `{!heapG Σ} (N : namespace).
......
From iris.heap_lang Require Import proofmode notation.
Class Involutive {A} (R : relation A) (f : A A) :=
involutive x : R (f (f x)) x.
\ No newline at end of file
From iris.heap_lang Require Import proofmode notation.
From osiris.typing Require Export involutive.
Inductive side := Left | Right.
Instance side_inhabited : Inhabited side := populate Left.
Definition dual_side (s : side) : side :=
match s with Left => Right | Right => Left end.
Instance dual_side_involutive : Involutive (=) dual_side.
Proof. by intros []. Qed.
\ No newline at end of file
......@@ -4,18 +4,9 @@ From stdpp Require Export list.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import updates local_updates.
From iris.heap_lang Require Import proofmode notation.
From osiris.typing Require Import involutive.
Set Default Proof Using "Type".
Class Involutive {A} (R : relation A) (f : A A) :=
involutive x : R (f (f x)) x.
Inductive side := Left | Right.
Instance side_inhabited : Inhabited side := populate Left.
Definition dual_side (s : side) : side :=
match s with Left => Right | Right => Left end.
Instance dual_side_involutive : Involutive (=) dual_side.
Proof. by intros []. Qed.
Inductive action := Send | Receive.
Instance action_inhabited : Inhabited action := populate Send.
Definition dual_action (a : action) : action :=
......
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