Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • tlsomers/actris
  • iris/actris
  • dfrumin/actris
3 results
Show changes
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 3753 additions and 131 deletions
theories/logrel/term_types.v → actris/logrel/term_types.v
View file @ c9249305
......@@ -43,7 +43,7 @@ Definition lty_bool {Σ} : ltty Σ := Ltty (λ w, ∃ b : bool, ⌜ w = #b ⌝)%
Definition lty_int {Σ} : ltty Σ := Ltty (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I.
Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
Definition lty_arr `{heapG Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
Definition lty_arr `{heapGS Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
∀ v, ▷ ltty_car A1 v -∗ WP w v {{ ltty_car A2 }})%I.
(* TODO: Make a non-linear version of prod, using ∧ *)
Definition lty_prod {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
......@@ -52,7 +52,7 @@ Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
(∃ w1, ⌜w = InjLV w1⌝ ∗ ▷ ltty_car A1 w1) ∨
(∃ w2, ⌜w = InjRV w2⌝ ∗ ▷ ltty_car A2 w2))%I.
Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
Definition lty_forall `{heapGS Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
Ltty (λ w, ∀ X, WP w #() {{ ltty_car (C X) }})%I.
Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
Ltty (λ w, ∃ X, ▷ ltty_car (C X) w)%I.
......@@ -60,25 +60,25 @@ Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, □ ltty_car A w)%I.
Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
Definition lty_ref_uniq `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
Definition lty_ref_uniq `{heapGS Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I.
Definition ref_shrN := nroot .@ "shr_ref".
Definition lty_ref_shr `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
Definition lty_ref_shr `{heapGS Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
∃ l : loc, ⌜w = #l⌝ ∗ inv (ref_shrN .@ l) (∃ v, l ↦ v ∗ □ ltty_car A v))%I.
Definition lty_chan `{heapG Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
Definition lty_chan `{heapGS Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
Ltty (λ w, w ↣ lsty_car P)%I.
Instance: Params (@lty_copy) 1 := {}.
Instance: Params (@lty_copy_minus) 1 := {}.
Instance: Params (@lty_arr) 2 := {}.
Instance: Params (@lty_prod) 1 := {}.
Instance: Params (@lty_sum) 1 := {}.
Instance: Params (@lty_forall) 2 := {}.
Instance: Params (@lty_sum) 1 := {}.
Instance: Params (@lty_ref_uniq) 2 := {}.
Instance: Params (@lty_ref_shr) 2 := {}.
Instance: Params (@lty_chan) 3 := {}.
Global Instance: Params (@lty_copy) 1 := {}.
Global Instance: Params (@lty_copy_minus) 1 := {}.
Global Instance: Params (@lty_arr) 2 := {}.
Global Instance: Params (@lty_prod) 1 := {}.
Global Instance: Params (@lty_sum) 1 := {}.
Global Instance: Params (@lty_forall) 2 := {}.
Global Instance: Params (@lty_sum) 1 := {}.
Global Instance: Params (@lty_ref_uniq) 2 := {}.
Global Instance: Params (@lty_ref_shr) 2 := {}.
Global Instance: Params (@lty_chan) 3 := {}.
Notation any := lty_any.
Notation "()" := lty_unit : lty_scope.
......@@ -110,14 +110,14 @@ Section term_types.
Global Instance lty_copy_minus_ne : NonExpansive (@lty_copy_minus Σ).
Proof. solve_proper. Qed.
Global Instance lty_arr_contractive `{heapG Σ} n :
Global Instance lty_arr_contractive `{heapGS Σ} n :
Proper (dist_later n ==> dist_later n ==> dist n) lty_arr.
Proof.
intros A A' ? B B' ?. apply Ltty_ne=> v. f_equiv=> w.
f_equiv; [by f_contractive|].
apply (wp_contractive _ _ _ _ _)=> v'. destruct n=> //=; by f_equiv.
apply (wp_contractive _ _ _ _ _)=> v'. dist_later_intro as n' Hn'. by f_equiv.
Qed.
Global Instance lty_arr_ne `{heapG Σ} : NonExpansive2 lty_arr.
Global Instance lty_arr_ne `{heapGS Σ} : NonExpansive2 lty_arr.
Proof. solve_proper. Qed.
Global Instance lty_prod_contractive n:
Proper (dist_later n ==> dist_later n ==> dist n) (@lty_prod Σ).
......@@ -130,14 +130,14 @@ Section term_types.
Global Instance lty_sum_ne : NonExpansive2 (@lty_sum Σ).
Proof. solve_proper. Qed.
Global Instance lty_forall_contractive `{heapG Σ} k n :
Global Instance lty_forall_contractive `{heapGS Σ} k n :
Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _ k).
Proof.
intros F F' A. apply Ltty_ne=> w. f_equiv=> B.
apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
by destruct n as [|n]; simpl.
dist_later_intro as n' Hn'. by f_equiv.
Qed.
Global Instance lty_forall_ne `{heapG Σ} k n :
Global Instance lty_forall_ne `{heapGS Σ} k n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
Proof. solve_proper. Qed.
Global Instance lty_exist_contractive k n :
......@@ -147,18 +147,18 @@ Section term_types.
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
Proof. solve_proper. Qed.
Global Instance lty_ref_uniq_contractive `{heapG Σ} : Contractive lty_ref_uniq.
Global Instance lty_ref_uniq_contractive `{heapGS Σ} : Contractive lty_ref_uniq.
Proof. solve_contractive. Qed.
Global Instance lty_ref_uniq_ne `{heapG Σ} : NonExpansive lty_ref_uniq.
Global Instance lty_ref_uniq_ne `{heapGS Σ} : NonExpansive lty_ref_uniq.
Proof. solve_proper. Qed.
Global Instance lty_ref_shr_contractive `{heapG Σ} : Contractive lty_ref_shr.
Global Instance lty_ref_shr_contractive `{heapGS Σ} : Contractive lty_ref_shr.
Proof. solve_contractive. Qed.
Global Instance lty_ref_shr_ne `{heapG Σ} : NonExpansive lty_ref_shr.
Global Instance lty_ref_shr_ne `{heapGS Σ} : NonExpansive lty_ref_shr.
Proof. solve_proper. Qed.
Global Instance lty_chan_contractive `{heapG Σ, chanG Σ} : Contractive lty_chan.
Global Instance lty_chan_contractive `{heapGS Σ, chanG Σ} : Contractive lty_chan.
Proof. solve_contractive. Qed.
Global Instance lty_chan_ne `{heapG Σ, chanG Σ} : NonExpansive lty_chan.
Global Instance lty_chan_ne `{heapGS Σ, chanG Σ} : NonExpansive lty_chan.
Proof. solve_proper. Qed.
End term_types.
theories/logrel/term_typing_judgment.v → actris/logrel/term_typing_judgment.v
View file @ c9249305
......@@ -9,14 +9,14 @@ semantically well-typed programs do not get stuck. *)
From iris.heap_lang Require Import metatheory adequacy.
From actris.logrel Require Export term_types.
From actris.logrel Require Export contexts.
From iris.proofmode Require Import tactics.
From iris.proofmode Require Import proofmode.
(** The semantic typing judgment *)
Definition ltyped `{!heapG Σ}
Definition ltyped `{!heapGS Σ}
(Γ1 Γ2 : ctx Σ) (e : expr) (A : ltty Σ) : iProp Σ :=
tc_opaque (■ ∀ vs, ctx_ltyped vs Γ1 -∗
WP subst_map vs e {{ v, ltty_car A v ∗ ctx_ltyped vs Γ2 }})%I.
Instance: Params (@ltyped) 2 := {}.
Global Instance: Params (@ltyped) 2 := {}.
Notation "Γ1 ⊨ e : A ⫤ Γ2" := (ltyped Γ1 Γ2 e A)
(at level 100, e at next level, A at level 200) : bi_scope.
......@@ -29,7 +29,7 @@ Notation "Γ ⊨ e : A" := (⊢ Γ ⊨ e : A ⫤ Γ)
(at level 100, e at next level, A at level 200) : type_scope.
Section ltyped.
Context `{!heapG Σ}.
Context `{!heapGS Σ}.
Global Instance ltyped_plain Γ1 Γ2 e A : Plain (ltyped Γ1 Γ2 e A).
Proof. rewrite /ltyped /=. apply _. Qed.
......@@ -55,9 +55,9 @@ To circumvent this, we make use of the following typing judgement for values,
that lets us type check values without requiring reduction steps.
The value typing judgement subsumes the typing judgement on expressions,
as made precise by the [ltyped_val_ltyped] lemma. *)
Definition ltyped_val `{!heapG Σ} (v : val) (A : ltty Σ) : iProp Σ :=
Definition ltyped_val `{!heapGS Σ} (v : val) (A : ltty Σ) : iProp Σ :=
tc_opaque (■ ltty_car A v)%I.
Instance: Params (@ltyped_val) 3 := {}.
Global Instance: Params (@ltyped_val) 3 := {}.
Notation "⊨ᵥ v : A" := (ltyped_val v A)
(at level 100, v at next level, A at level 200) : bi_scope.
Notation "⊨ᵥ v : A" := (⊢ ⊨ᵥ v : A)
......@@ -65,7 +65,7 @@ Notation "⊨ᵥ v : A" := (⊢ ⊨ᵥ v : A)
Arguments ltyped_val : simpl never.
Section ltyped_val.
Context `{!heapG Σ}.
Context `{!heapGS Σ}.
Global Instance ltyped_val_plain v A : Plain (ltyped_val v A).
Proof. rewrite /ltyped_val /=. apply _. Qed.
......@@ -79,7 +79,7 @@ Section ltyped_val.
End ltyped_val.
Section ltyped_rel.
Context `{!heapG Σ}.
Context `{!heapGS Σ}.
Lemma ltyped_val_ltyped Γ v A : (⊨ᵥ v : A) -∗ Γ ⊨ v : A.
Proof.
......@@ -91,8 +91,8 @@ Section ltyped_rel.
End ltyped_rel.
Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
(∀ `{heapG Σ}, ∃ A, [] ⊨ e : A ⫤ []) →
Lemma ltyped_safety `{heapGpreS Σ} e σ es σ' e' :
(∀ `{heapGS Σ}, ∃ A, [] ⊨ e : A ⫤ []) →
rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
is_Some (to_val e') ∨ reducible e' σ'.
Proof.
......
theories/logrel/term_typing_rules.v → actris/logrel/term_typing_rules.v
View file @ c9249305
......@@ -8,7 +8,7 @@ From actris.logrel Require Export subtyping_rules term_typing_judgment operators
From actris.channel Require Import proofmode.
Section term_typing_rules.
Context `{heapG Σ}.
Context `{heapGS Σ}.
Implicit Types A B : ltty Σ.
Implicit Types Γ : ctx Σ.
......@@ -79,7 +79,7 @@ Section term_typing_rules.
(Γ1 ⊨ UnOp op e : B ⫤ Γ2).
Proof.
iIntros (Hop) "#He !>". iIntros (vs) "HΓ1 /=".
wp_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA $]".
wp_smart_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA $]".
iDestruct (Hop with "HA") as (w ?) "HB". by wp_unop.
Qed.
......@@ -90,8 +90,8 @@ Section term_typing_rules.
(Γ1 ⊨ BinOp op e1 e2 : B ⫤ Γ3).
Proof.
iIntros (Hop) "#He2 #He1 !>". iIntros (vs) "HΓ1 /=".
wp_apply (wp_wand with "(He2 [HΓ1 //])"). iIntros (v2) "[HA2 HΓ2]".
wp_apply (wp_wand with "(He1 [HΓ2 //])"). iIntros (v1) "[HA1 $]".
wp_smart_apply (wp_wand with "(He2 [HΓ1 //])"). iIntros (v2) "[HA2 HΓ2]".
wp_smart_apply (wp_wand with "(He1 [HΓ2 //])"). iIntros (v1) "[HA1 $]".
iDestruct (Hop with "HA1 HA2") as (w ?) "HB". by wp_binop.
Qed.
......@@ -103,10 +103,10 @@ Section term_typing_rules.
(Γ1 ⊨ (if: e1 then e2 else e3) : A ⫤ Γ3).
Proof.
iIntros "#He1 #He2 #He3 !>" (v) "HΓ1 /=".
wp_apply (wp_wand with "(He1 [HΓ1 //])"). iIntros (b) "[Hbool HΓ2]".
wp_smart_apply (wp_wand with "(He1 [HΓ1 //])"). iIntros (b) "[Hbool HΓ2]".
rewrite /lty_bool. iDestruct "Hbool" as ([]) "->".
- wp_apply (wp_wand with "(He2 [HΓ2 //])"). iIntros (w) "[$$]".
- wp_apply (wp_wand with "(He3 [HΓ2 //])"). iIntros (w) "[$$]".
- wp_smart_apply (wp_wand with "(He2 [HΓ2 //])"). iIntros (w) "[$$]".
- wp_smart_apply (wp_wand with "(He3 [HΓ2 //])"). iIntros (w) "[$$]".
Qed.
(** Arrow properties *)
......@@ -115,8 +115,8 @@ Section term_typing_rules.
(Γ1 ⊨ e1 e2 : A2 ⫤ Γ3).
Proof.
iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf $]".
wp_smart_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
wp_smart_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf $]".
iApply ("Hf" $! v with "HA1").
Qed.
......@@ -125,8 +125,8 @@ Section term_typing_rules.
(Γ1 ⊨ e1 e2 : A2 ⫤ Γ3).
Proof.
iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
wp_smart_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
wp_smart_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
Qed.
......@@ -205,7 +205,7 @@ Section term_typing_rules.
(Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ ctx_filter_eq x Γ2 ++ ctx_filter_ne x Γ3).
Proof.
iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HA1 HΓ2]". wp_pures.
wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HA1 HΓ2]". wp_pures.
rewrite {3}(ctx_filter_eq_perm Γ2 x).
iDestruct (ctx_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
iDestruct ("He2" $! (binder_insert x v vs) with "[HA1 HΓ2neq]") as "He'".
......@@ -221,8 +221,8 @@ Section term_typing_rules.
(Γ1 ⊨ (e1 ;; e2) : B ⫤ Γ3).
Proof.
iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[_ HΓ2]". wp_pures.
wp_apply (wp_wand with "(He2 HΓ2)"); iIntros (w) "[HB HΓ3]".
wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[_ HΓ2]". wp_pures.
wp_smart_apply (wp_wand with "(He2 HΓ2)"); iIntros (w) "[HB HΓ3]".
iFrame "HB HΓ3".
Qed.
......@@ -232,8 +232,8 @@ Section term_typing_rules.
(Γ1 ⊨ (e1,e2) : A1 * A2 ⫤ Γ3).
Proof.
iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
wp_apply (wp_wand with "(H2 [HΓ //])"); iIntros (w2) "[HA2 HΓ]".
wp_apply (wp_wand with "(H1 [HΓ //])"); iIntros (w1) "[HA1 HΓ]".
wp_smart_apply (wp_wand with "(H2 [HΓ //])"); iIntros (w2) "[HA2 HΓ]".
wp_smart_apply (wp_wand with "(H1 [HΓ //])"); iIntros (w1) "[HA1 HΓ]".
wp_pures. iFrame "HΓ". iExists w1, w2. by iFrame.
Qed.
......@@ -267,7 +267,7 @@ Section term_typing_rules.
(Γ1 ⊨ InjL e : A1 + A2 ⫤ Γ2).
Proof.
iIntros "#HA" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(HA [HΓ //])").
wp_smart_apply (wp_wand with "(HA [HΓ //])").
iIntros (v) "[HA' $]". wp_pures.
iLeft. iExists v. auto.
Qed.
......@@ -277,7 +277,7 @@ Section term_typing_rules.
(Γ1 ⊨ InjR e : A1 + A2 ⫤ Γ2).
Proof.
iIntros "#HA" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(HA [HΓ //])").
wp_smart_apply (wp_wand with "(HA [HΓ //])").
iIntros (v) "[HA' $]". wp_pures.
iRight. iExists v. auto.
Qed.
......@@ -289,11 +289,11 @@ Section term_typing_rules.
(Γ1 ⊨ Case e1 e2 e3 : B ⫤ Γ3).
Proof.
iIntros "#H1 #H2 #H3" (vs) "!> HΓ1 /=".
wp_apply (wp_wand with "(H1 HΓ1)"). iIntros (s) "[[Hs|Hs] HΓ2]";
wp_smart_apply (wp_wand with "(H1 HΓ1)"). iIntros (s) "[[Hs|Hs] HΓ2]";
iDestruct "Hs" as (w ->) "HA"; wp_case.
- wp_apply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv $]".
- wp_smart_apply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv $]".
iApply (wp_wand with "(Hv HA)"). auto.
- wp_apply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv $]".
- wp_smart_apply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv $]".
iApply (wp_wand with "(Hv HA)"). auto.
Qed.
......@@ -313,7 +313,7 @@ Section term_typing_rules.
(Γ ⊨ e #() : C K ⫤ Γ2).
Proof.
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
wp_smart_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
iApply (wp_wand with "HB [HΓ]"). by iIntros (v) "$".
Qed.
......@@ -322,7 +322,7 @@ Section term_typing_rules.
(Γ1 ⊨ e : C K ⫤ Γ2) -∗ Γ1 ⊨ e : (∃ X, C X) ⫤ Γ2.
Proof.
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists K.
wp_smart_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists K.
Qed.
Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B :
......@@ -331,7 +331,7 @@ Section term_typing_rules.
(Γ1 ⊨ (let: x := e1 in e2) : B ⫤ ctx_filter_eq x Γ2 ++ ctx_filter_ne x Γ3).
Proof.
iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
wp_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HC HΓ2]".
wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HC HΓ2]".
iDestruct "HC" as (X) "HX". wp_pures.
rewrite {3}(ctx_filter_eq_perm Γ2 x).
iDestruct (ctx_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
......@@ -348,7 +348,7 @@ Section term_typing_rules.
(Γ1 ⊨ ref e : ref_uniq A ⫤ Γ2).
Proof.
iIntros "#He" (vs) "!> HΓ1 /=".
wp_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
wp_smart_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
wp_alloc l as "Hl". iExists l, v; eauto with iFrame.
Qed.
......@@ -357,7 +357,7 @@ Section term_typing_rules.
(Γ1 ⊨ Free e : () ⫤ Γ2).
Proof.
iIntros "#He" (vs) "!> HΓ1 /=".
wp_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
wp_smart_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
iDestruct "Hv" as (l w ->) "[Hl Hw]". by wp_free.
Qed.
......@@ -379,7 +379,7 @@ Section term_typing_rules.
(Γ ⊨ x <- e : () ⫤ ctx_cons x (ref_uniq B) Γ').
Proof.
iIntros (HΓx%ctx_lookup_perm) "#He"; iIntros (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
wp_smart_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
rewrite {2}HΓx /=.
iDestruct (ctx_ltyped_cons with "HΓ'") as (vl Hvs) "[HA HΓ']"; rewrite Hvs.
iDestruct "HA" as (l w ->) "[? HA]". wp_store. iModIntro. iSplit; [done|].
......@@ -405,7 +405,7 @@ Section term_typing_rules.
Γ ⊨ ! e : A ⫤ Γ'.
Proof.
iIntros "#He" (vs) "!> HΓ /=".
wp_apply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
wp_smart_apply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
iDestruct "Hv" as (l ->) "#Hv".
iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose".
wp_load.
......@@ -419,7 +419,7 @@ Section term_typing_rules.
(Γ1 ⊨ e1 <- e2 : () ⫤ Γ3).
Proof.
iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
wp_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
wp_smart_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
wp_bind (subst_map vs e1).
iApply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
iDestruct "Hw" as (l ->) "#Hw".
......@@ -434,14 +434,14 @@ Section term_typing_rules.
(Γ1 ⊨ FAA e1 e2 : lty_int ⫤ Γ3).
Proof.
iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
wp_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
wp_apply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
wp_smart_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
wp_smart_apply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
iDestruct "Hw" as (l ->) "#Hw".
iInv (ref_shrN .@ l) as (w) "[Hl >Hn]" "Hclose".
iDestruct "Hn" as %[k ->].
iDestruct "Hv" as %[n ->].
wp_faa.
iMod ("Hclose" with "[Hl]") as %_.
iMod ("Hclose" with "[Hl]") as % _.
{ iExists #(k + n). iFrame "Hl". by iExists (k + n)%Z. }
by iExists k.
Qed.
......@@ -454,7 +454,7 @@ Section term_typing_rules.
Proof.
iIntros "#He1 #He2 !>" (vs) "HΓ /=".
iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 HΓ2]".
wp_apply (wp_par with "(He1 HΓ1) (He2 HΓ2)").
wp_smart_apply (wp_par with "(He1 HΓ1) (He2 HΓ2)").
iIntros (v1 v2) "[[HA HΓ1'] [HB HΓ2']] !>". iSplitL "HA HB".
+ iExists v1, v2. by iFrame.
+ iApply ctx_ltyped_app. by iFrame.
......
theories/utils/cofe_solver_2.v → actris/utils/cofe_solver_2.v
View file @ c9249305
......@@ -9,13 +9,13 @@ Record solution_2 (F : ofe → oFunctor) := Solution2 {
ofe_iso (oFunctor_apply (F A) (solution_2_car A An)) (solution_2_car An A);
}.
Arguments solution_2_car {F}.
Existing Instance solution_2_cofe.
Global Existing Instance solution_2_cofe.
Section cofe_solver_2.
Context (F : ofe → oFunctor).
Context `{Fcontr : !∀ T, oFunctorContractive (F T)}.
Context `{Fcofe : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
Context `{Finh : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
Context `{Fcofe : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
Context `{Finh : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
Notation map := (oFunctor_map (F _)).
Definition F_2 (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : oFunctor :=
......@@ -72,15 +72,15 @@ Section cofe_solver_2.
rewrite -{2}(ofe_iso_12 T_result y). f_equiv.
rewrite -(oFunctor_map_id (F _) (ofe_iso_2 T_result y))
-!oFunctor_map_compose.
f_equiv; apply Fcontr; destruct n as [|n]; simpl; [done|].
split => x /=; rewrite ofe_iso_21 -{2}(oFunctor_map_id (F _) x)
-!oFunctor_map_compose; do 2 f_equiv; split=> z /=; auto.
f_equiv; apply Fcontr; dist_later_intro as n' Hn'; split=> x /=;
rewrite ofe_iso_21 -{2}(oFunctor_map_id (F _) x)
-!oFunctor_map_compose; do 2 f_equiv; split=> z /=; auto.
- intros y. apply equiv_dist=> n. revert An Hcn A Hc y.
induction (lt_wf n) as [n _ IH]; intros An ? A ? y.
rewrite T_iso_fun_unfold_1 T_iso_fun_unfold_2 /= ofe_iso_21.
rewrite -(oFunctor_map_id (F _) y) -!oFunctor_map_compose.
f_equiv; apply Fcontr; destruct n as [|n]; simpl; [done|].
split => x /=; rewrite -{2}(ofe_iso_12 T_result x); f_equiv;
f_equiv; apply Fcontr; dist_later_intro as n' Hn'; split=> x /=;
rewrite -{2}(ofe_iso_12 T_result x); f_equiv;
rewrite -{2}(oFunctor_map_id (F _) (ofe_iso_2 T_result x))
-!oFunctor_map_compose;
do 2 f_equiv; split=> z /=; auto.
......
theories/utils/compare.v → actris/utils/compare.v
View file @ c9249305
......@@ -5,17 +5,17 @@ on integers [Z].*)
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Definition cmp_spec `{!heapG Σ} {A} (I : A → val → iProp Σ)
Definition cmp_spec `{!heapGS Σ} {A} (I : A → val → iProp Σ)
(R : relation A) `{!RelDecision R} (cmp : val) : iProp Σ :=
(∀ x x' v v',
{{{ I x v ∗ I x' v' }}}
cmp v v'
{{{ RET #(bool_decide (R x x')); I x v ∗ I x' v' }}})%I.
Definition IZ `{!heapG Σ} (x : Z) (v : val) : iProp Σ := ⌜v = #x⌝%I.
Definition IZ `{!heapGS Σ} (x : Z) (v : val) : iProp Σ := ⌜v = #x⌝%I.
Definition cmpZ : val := λ: "x" "y", "x" ≤ "y".
Lemma cmpZ_spec `{!heapG Σ} : ⊢ cmp_spec IZ (≤)%Z cmpZ.
Lemma cmpZ_spec `{!heapGS Σ} : ⊢ cmp_spec IZ (≤)%Z cmpZ.
Proof.
rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ".
wp_lam. wp_pures. by iApply "HΦ".
......
theories/utils/contribution.v → actris/utils/contribution.v
View file @ c9249305
......@@ -16,12 +16,12 @@ later used in the protocol.
To model this ghost theory construction, we use the camera
[auth (option (csum (positive * A) (excl unit)))]. *)
From iris.base_logic Require Export base_logic lib.iprop lib.own.
From iris.proofmode Require Export tactics.
From iris.proofmode Require Export proofmode.
From iris.algebra Require Import excl auth csum gmultiset numbers.
From iris.algebra Require Export local_updates.
Class contributionG Σ (A : ucmra) `{!CmraDiscrete A} := {
contribution_inG :> inG Σ
contribution_inG :: inG Σ
(authR (optionUR (csumR (prodR positiveR A) (exclR unitO))))
}.
......@@ -29,13 +29,13 @@ Definition server `{contributionG Σ A} (γ : gname) (n : nat) (x : A) : iProp
(if decide (n = O)
then x ≡ ε ∗ own γ (● (Some (Cinr (Excl ())))) ∗ own γ (◯ (Some (Cinr (Excl ()))))
else own γ (● (Some (Cinl (Pos.of_nat n, x)))))%I.
Typeclasses Opaque server.
Instance: Params (@server) 6 := {}.
Global Typeclasses Opaque server.
Global Instance: Params (@server) 6 := {}.
Definition client `{contributionG Σ A} (γ : gname) (x : A) : iProp Σ :=
own γ (◯ (Some (Cinl (1%positive, x)))).
Typeclasses Opaque client.
Instance: Params (@client) 5 := {}.
Global Typeclasses Opaque client.
Global Instance: Params (@client) 5 := {}.
Section contribution.
Context `{contributionG Σ A}.
......@@ -63,8 +63,8 @@ Section contribution.
Lemma server_1_agree γ x y : server γ 1 x -∗ client γ y -∗ ⌜ x ≡ y ⌝.
Proof.
rewrite /server /client. case_decide=> //. iIntros "Hs Hc".
iDestruct (own_valid_2 with "Hs Hc")
as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete; first done.
iCombine "Hs Hc"
gives %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete; first done.
move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[? _].
by destruct (Pos.lt_irrefl 1).
Qed.
......@@ -87,9 +87,9 @@ Section contribution.
Proof.
rewrite /server /client. iIntros "Hs Hc". case_decide; subst.
- iDestruct "Hs" as "(_ & _ & Hc')".
by iDestruct (own_valid_2 with "Hc Hc'") as %?%auth_frag_op_valid_1.
- iDestruct (own_valid_2 with "Hs Hc")
as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
by iCombine "Hc Hc'" gives %?%auth_frag_op_valid_1.
- iCombine "Hs Hc"
gives %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
{ setoid_subst. by destruct n. }
move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[??].
by destruct n.
......
theories/utils/group.v → actris/utils/group.v
View file @ c9249305
......@@ -17,8 +17,8 @@ Fixpoint group {A} `{EqDecision K} (ixs : list (K * A)) : list (K * list A) :=
| (i,x) :: ixs => group_insert i x (group ixs)
end.
Instance: Params (@group_insert) 5 := {}.
Instance: Params (@group) 3 := {}.
Global Instance: Params (@group_insert) 5 := {}.
Global Instance: Params (@group) 3 := {}.
Local Infix "≡ₚₚ" :=
(PermutationA (prod_relation (=) (≡ₚ))) (at level 70, no associativity) : stdpp_scope.
......
theories/utils/llist.v → actris/utils/llist.v
View file @ c9249305
......@@ -5,7 +5,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.
(** *)
Fixpoint llist `{heapG Σ} {A} (I : A → val → iProp Σ)
Fixpoint llist `{heapGS Σ} {A} (I : A → val → iProp Σ)
(l : loc) (xs : list A) : iProp Σ :=
match xs with
| [] => l ↦ NONEV
......@@ -87,7 +87,7 @@ Definition lreverse : val :=
"l" <- !(lreverse_at "l'" (lnil #())).
Section lists.
Context `{heapG Σ} {A} (I : A → val → iProp Σ).
Context `{heapGS Σ} {A} (I : A → val → iProp Σ).
Implicit Types i : nat.
Implicit Types xs : list A.
Implicit Types l : loc.
......@@ -150,7 +150,7 @@ Lemma lhead_spec l x xs :
lhead #l
{{{ v, RET v; I x v ∗ (I x v -∗ llist I l (x :: xs)) }}}.
Proof.
iIntros (Φ) "Hll HΦ". wp_apply (lhead_spec_aux with "Hll").
iIntros (Φ) "Hll HΦ". wp_smart_apply (lhead_spec_aux with "Hll").
iIntros (v l') "(HIx&?&?)". iApply "HΦ". iIntros "{$HIx} HIx".
simpl; eauto with iFrame.
Qed.
......@@ -159,7 +159,7 @@ Lemma lpop_spec l x xs :
{{{ llist I l (x :: xs) }}} lpop #l {{{ v, RET v; I x v ∗ llist I l xs }}}.
Proof.
iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
wp_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
wp_smart_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
Qed.
Lemma llookup_spec l i xs x :
......@@ -171,11 +171,11 @@ Proof.
iIntros (Hi Φ) "Hll HΦ".
iInduction xs as [|x' xs] "IH" forall (l i x Hi Φ); [done|simpl; wp_rec; wp_pures].
destruct i as [|i]; simplify_eq/=; wp_pures.
- wp_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
- wp_smart_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
iApply "HΦ"; eauto with iFrame.
- iDestruct "Hll" as (v l') "(HIx' & Hl' & Hll)". wp_load; wp_pures.
rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
wp_smart_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
iApply "HΦ". iIntros "{$HIx} HIx". iExists v, l'. iFrame. by iApply "Hll".
Qed.
......@@ -186,7 +186,7 @@ Proof.
iInduction xs as [|x xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
- wp_load; wp_pures. by iApply "HΦ".
- iDestruct "Hll" as (v l') "(HIx & Hl' & Hll)". wp_load; wp_pures.
wp_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
wp_smart_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
rewrite (Nat2Z.inj_add 1). iApply "HΦ"; eauto with iFrame.
Qed.
......@@ -202,7 +202,7 @@ Proof.
+ iDestruct "Hll2" as (v2 l2') "(HIx2 & Hl2 & Hll2)". wp_load. wp_store.
iApply "HΦ". iSplitR "Hl2"; eauto 10 with iFrame.
- iDestruct "Hll1" as (v1 l') "(HIx1 & Hl1 & Hll1)". wp_load; wp_pures.
wp_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
wp_smart_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
iApply "HΦ"; eauto with iFrame.
Qed.
......@@ -212,7 +212,7 @@ Lemma lprep_spec l1 l2 xs1 xs2 :
{{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ (∃ v, l2 ↦ v) }}}.
Proof.
iIntros (Φ) "[Hll1 Hll2] HΦ". wp_lam.
wp_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
wp_smart_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
iDestruct "Hl1" as (w) "Hl1". destruct (xs1 ++ xs2) as [|x xs]; simpl; wp_pures.
- wp_load. wp_store. iApply "HΦ"; eauto with iFrame.
- iDestruct "Hll2" as (v l') "(HIx & Hl2 & Hll2)". wp_load. wp_store.
......@@ -226,7 +226,7 @@ Proof.
iInduction xs as [|x' xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
- wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
- iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)". wp_load; wp_pures.
wp_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
wp_smart_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
Qed.
Lemma lsplit_at_spec l xs (n : nat) :
......@@ -242,7 +242,7 @@ Proof.
- iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures.
+ wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
+ wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
wp_smart_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
iApply "HΦ"; eauto with iFrame.
Qed.
......@@ -252,9 +252,9 @@ Lemma lsplit_spec l xs :
{{{ k xs1 xs2, RET #k; ⌜ xs = xs1 ++ xs2 ⌝ ∗ llist I l xs1 ∗ llist I k xs2 }}}.
Proof.
iIntros (Φ) "Hl HΦ". wp_lam.
wp_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Nat2Z_inj_div _ 2).
wp_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
wp_smart_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Nat2Z.inj_div _ 2).
wp_smart_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
iApply "HΦ". iFrame. by rewrite take_drop.
Qed.
......@@ -264,13 +264,13 @@ Lemma lreverse_at_spec l xs acc ys :
{{{ l', RET #l'; llist I l' (reverse xs ++ ys) }}}.
Proof.
iIntros (Φ) "[Hl Hacc] HΦ".
iInduction xs as [|x xs] "IH" forall (l acc Φ ys).
- wp_lam. wp_load. wp_pures. iApply "HΦ". rewrite app_nil_l. iApply "Hacc".
- wp_lam. iDestruct "Hl" as (v l') "[HI [Hl Hl']]".
wp_load. wp_apply (lcons_spec with "[$Hacc $HI]").
iIntros "Hacc". wp_apply ("IH" with "Hl' Hacc").
iInduction xs as [|x xs] "IH" forall (l acc Φ ys); simpl; wp_lam.
- wp_load. wp_pures. iApply "HΦ". iApply "Hacc".
- iDestruct "Hl" as (v l') "[HI [Hl Hl']]".
wp_load. wp_smart_apply (lcons_spec with "[$Hacc $HI]").
iIntros "Hacc". wp_smart_apply ("IH" with "Hl' Hacc").
iIntros (l'') "Hl''". iApply "HΦ".
rewrite reverse_cons -app_assoc. iApply "Hl''".
rewrite reverse_cons -assoc_L. iApply "Hl''".
Qed.
Lemma lreverse_spec l xs :
......@@ -279,29 +279,25 @@ Lemma lreverse_spec l xs :
{{{ RET #(); llist I l (reverse xs) }}}.
Proof.
iIntros (Φ) "Hl HΦ". wp_lam.
destruct xs.
destruct xs as [|x xs]; simpl.
- wp_load. wp_alloc l' as "Hl'".
wp_apply (lnil_spec)=> //.
wp_smart_apply (lnil_spec with "[//]").
iIntros (lnil) "Hlnil".
iAssert (llist I l' []) with "Hl'" as "Hl'".
wp_apply (lreverse_at_spec with "[$Hl' $Hlnil]").
wp_smart_apply (lreverse_at_spec with "[$Hl' $Hlnil]").
iIntros (l'') "Hl''".
wp_load. wp_store. iApply "HΦ". rewrite app_nil_r. iApply "Hl".
wp_load. wp_store. iApply "HΦ". rewrite right_id_L. iApply "Hl".
- iDestruct "Hl" as (v lcons) "[HI [Hlcons Hrec]]".
wp_load. wp_alloc l' as "Hl'".
wp_apply (lnil_spec)=> //.
wp_smart_apply (lnil_spec with "[//]").
iIntros (lnil) "Hlnil".
wp_apply (lreverse_at_spec _ (a::xs) with "[Hl' HI Hrec Hlnil]").
{ iFrame "Hlnil". iExists v, lcons. iFrame. }
iIntros (l'') "Hl''".
assert (∃ ys, ys = reverse (a :: xs)) as [ys Hys].
{ by exists (reverse (a :: xs)). }
rewrite -Hys. destruct ys.
wp_smart_apply (lreverse_at_spec _ (x :: xs) with "[Hl' HI Hrec $Hlnil]").
{ simpl; eauto with iFrame. }
iIntros (l'') "Hl''". rewrite right_id_L. destruct (reverse _) as [|y ys].
+ wp_load. wp_store. by iApply "HΦ".
+ simpl. iDestruct "Hl''" as (v' lcons') "[HI [Hcons Hrec]]".
wp_load. wp_store.
iApply "HΦ". rewrite app_nil_r.
eauto with iFrame.
iApply "HΦ". eauto with iFrame.
Qed.
End lists.
theories/utils/switch.v → actris/utils/switch.v
View file @ c9249305
......@@ -51,10 +51,12 @@ Proof.
apply IH. lia.
Qed.
Lemma switch_lams_spec `{heapG Σ} y i n ws vs e Φ :
Lemma switch_lams_spec `{heapGS Σ} y i n ws vs e Φ :
length vs = n →
WP subst_map (map_string_seq y i vs ∪ ws) e {{ Φ }} -∗
WP subst_map ws (switch_lams y i n e) {{ w, WP fill (AppLCtx <$> vs) w {{ Φ }} }}.
WP subst_map ws (switch_lams y i n e) {{ w, WP fill (AppLCtx <$> vs) (of_val w) {{ Φ }} }}.
(* FIXME: Once we depend on Coq 8.13, make WP notation use [v closed binder]
so that we can add a type annotation at the [w] binder here. *)
Proof.
iIntros (<-) "H".
iInduction vs as [|v vs] "IH" forall (i ws); csimpl.
......@@ -67,7 +69,7 @@ Proof.
lookup_map_string_seq_None_lt; auto with lia.
Qed.
Lemma switch_body_spec `{heapG Σ} y xs i j ws (x : Z) edef ecase Φ :
Lemma switch_body_spec `{heapGS Σ} y xs i j ws (x : Z) edef ecase Φ :
fst <$> list_find (x =.) xs = Some i →
ws !! y = Some #x →
WP subst_map ws (ecase (i + j)%nat) {{ Φ }} -∗
......@@ -82,7 +84,7 @@ Proof.
iApply ("IH" $! i'). by simplify_option_eq. by rewrite Nat.add_succ_r.
Qed.
Lemma switch_fail_spec `{heapG Σ} vfs xs i (x : Z) (vf : val) Φ :
Lemma switch_fail_spec `{heapGS Σ} vfs xs i (x : Z) (vf : val) Φ :
length vfs = length xs →
fst <$> list_find (x =.) xs = Some i →
vfs !! i = Some vf →
......
opam → coq-actris.opam
View file @ c9249305
This diff is collapsed.
make-package 0 → 100755
View file @ c9249305
This diff is collapsed.
multris/channel/channel.v 0 → 100644
View file @ c9249305
This diff is collapsed.
multris/channel/proofmode.v 0 → 100644
View file @ c9249305
This diff is collapsed.
multris/channel/proto.v 0 → 100644
View file @ c9249305
This diff is collapsed.
multris/channel/proto_model.v 0 → 100644
View file @ c9249305
This diff is collapsed.
multris/examples/basics.v 0 → 100644
View file @ c9249305
This diff is collapsed.
multris/examples/leader_election.v 0 → 100644
View file @ c9249305
This diff is collapsed.
multris/examples/three_buyer.v 0 → 100644
View file @ c9249305
This diff is collapsed.
multris/examples/two_buyer.v 0 → 100644
View file @ c9249305
This diff is collapsed.