Commit f55d64b5 authored by Jonas Kastberg's avatar Jonas Kastberg

Bumped Coq 8.10

parent 023322d5
-Q theories actris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
theories/utils/auth_excl.v
theories/utils/llist.v
theories/utils/compare.v
......
(** This file contains an instantiation of the
Dependent Separation Protocols and an integration with the channel encodings.
For starters this means fixing the types of messages to the
value type of the language [val] and the logic to the iris logic [iProp Σ].
value type of the language [val] and the logic to the Iris logic [iProp Σ].
In doing so we define way of constructing instances of the instantiated type
In doing so we define ways of constructing instances of the instantiated type
via two constructors:
- [iProto_end] which is identical to [proto_end]
- [iProto_message] which takes an action and a continuation to construct
......@@ -17,8 +17,8 @@ iProto_message with an appropriate continuation.
Said continuation ultimately establishes the following:
- Existential quantification of variables [x .. y].
- The equivalence [v = w], where [w] is the value that is eventually sent.
- Ownership of the predicate P
- The equivalence [v = w], where [w] is the value that is eventually exchanged.
- Ownership of the predicate [P]
- A continuation as [prot]
Futhermore type-specific variants of dual and append are provided:
......@@ -29,9 +29,9 @@ An encoding of branching behaviour is additionally included, defined
in terms of sending and receiving boolean flags:
- [prot1 {Q1}<+>{Q2} prot2] and
- [prot1 {Q1}<&>{Q2} prot2] which defines ownership of Q1 or Q2, and continues as
Q1 or Q2, based on the sent or received flag.
Q1 or Q2, based on the exchanged flag.
The logical connective of protocol ownership are then defined:
The logical connective of protocol ownership is then defined:
- [c ↣ prot] which describes that channel endpoint [c] adheres
to protocol [prot], achieved through Iris invariants and ghost state along
with the logical connectives of the channel encodings [is_chan] and [chan_own].
......@@ -88,7 +88,7 @@ Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
Definition iProto_message := iProto_message_aux.(unseal).
Definition iProto_message_eq : @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
Arguments iProto_message {_ _} _ _%proto.
Instance: Params (@iProto_message) 3.
Instance: Params (@iProto_message) 3 := {}.
Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
(iProto_message
......@@ -167,11 +167,11 @@ Notation "'END'" := iProto_end : proto_scope.
Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
proto_map action_dual cid cid p.
Arguments iProto_dual {_} _%proto.
Instance: Params (@iProto_dual) 1.
Instance: Params (@iProto_dual) 1 := {}.
Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ :=
if d then iProto_dual p else p.
Arguments iProto_dual_if {_} _ _%proto.
Instance: Params (@iProto_dual_if) 2.
Instance: Params (@iProto_dual_if) 2 := {}.
(** Branching *)
Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
......@@ -179,7 +179,7 @@ Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
(<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
Typeclasses Opaque iProto_branch.
Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
Instance: Params (@iProto_branch) 2.
Instance: Params (@iProto_branch) 2 := {}.
Infix "<{ P1 }+{ P2 }>" := (iProto_branch Send P1 P2) (at level 85) : proto_scope.
Infix "<{ P1 }&{ P2 }>" := (iProto_branch Receive P1 P2) (at level 85) : proto_scope.
Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
......@@ -192,7 +192,7 @@ Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
(** Append *)
Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2.
Arguments iProto_app {_} _%proto _%proto.
Instance: Params (@iProto_app) 1.
Instance: Params (@iProto_app) 1 := {}.
Infix "<++>" := iProto_app (at level 60) : proto_scope.
(** Auxiliary definitions and invariants *)
......
......@@ -4,7 +4,7 @@ and map and the necessary typeclass instances.
They are designed with inspiration from Session Types, mimicking
their constructors !T.st, ?T.st and END, respectively representing
sending and receiving messages of type T or termination.
sending and receiving messages of type T and termination.
The main difference is that the protocols are defined over predicates,
in place of types.
......@@ -22,20 +22,19 @@ The remainder (V → (▶ [proto] → PROP) → PROP)) is a continuation that
depends on the communicated value V and the dependent tail (▶ proto → PROP)
from protocols guarded under laters to the propositions of the logic.
The constructors of the protocol are then:
The constructors of the protocol are:
- [proto_end] which constructs the left-side of the sum.
- [proto_msg] which takes an action and a continuation and constructs the
right-hand side of the sum accodingly.
The type is defined as a solution to a recursive domain
equation, as it is self-referential under the guard of .
equation, as it is self-referential under the guard of [▶ ].
The available functions on [proto] are:
- [proto_map] which can be used to map the actions, the propositions of
- [proto_map] which can be used to map the actions and the propositions of
a given protocol.
- [proto_app] which appends two protocols [p1] and [p2], by substituting
all terminations in [p1] with [p2].
*)
all terminations in [p1] with [p2].*)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
......@@ -149,7 +148,7 @@ Definition proto_app_flipped {V} `{!Cofe PROPn, !Cofe PROP}
fixpoint (proto_app_flipped_aux p2).
Definition proto_app {V} `{!Cofe PROPn, !Cofe PROP}
(p1 p2 : proto V PROPn PROP) : proto V PROPn PROP := proto_app_flipped p2 p1.
Instance: Params (@proto_app) 5.
Instance: Params (@proto_app) 5 := {}.
Lemma proto_app_flipped_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP):
proto_app_flipped p2 p1 proto_app_flipped_aux p2 (proto_app_flipped p2) p1.
......
......@@ -10,7 +10,7 @@ From iris.algebra Require Import gmultiset.
Definition map_reduce {A B C} `{EqDecision K}
(map : A list (K * B)) (red : K list B list C) : list A list C :=
mbind (curry red) group mbind map.
Instance: Params (@map_reduce) 7.
Instance: Params (@map_reduce) 7 := {}.
(** Distributed version *)
Definition par_map_reduce_map : val :=
......
......@@ -24,7 +24,7 @@ Proof. solve_inG. Qed.
Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
Excl' a.
Instance: Params (@to_auth_excl) 1.
Instance: Params (@to_auth_excl) 1 := {}.
Section auth_excl_ofe.
Context {A : ofeT}.
......
......@@ -27,12 +27,12 @@ Definition server `{contributionG Σ A} (γ : gname) (n : nat) (x : A) : iProp
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.
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.
Instance: Params (@client) 5 := {}.
Section contribution.
Context `{contributionG Σ A}.
......
......@@ -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.
Instance: Params (@group_insert) 5 := {}.
Instance: Params (@group) 3 := {}.
Local Infix "≡ₚₚ" :=
(PermutationA (prod_relation (=) ())) (at level 70, no associativity) : stdpp_scope.
......
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