PADEC - Coq Library

# Library Padec.Model.Algorithm

From Padec Require Import SetoidUtil.

From Padec Require Import OptionUtil.

From Padec Require Import ListUtils.

Open Scope signature_scope.

Set Implicit Arguments.

From Padec Require Import OptionUtil.

From Padec Require Import ListUtils.

Open Scope signature_scope.

Set Implicit Arguments.

# Distributed Algorithm:

- Channels
- Network
- Algorithm

exists an Algorithm (the one to be proven) (uses Channels)

forall Network using Channels,

the Algorithm meets its specification

defined on Network and Channels

(provided some assumption on Network and Channels).

## Class Channels:

Channels are used to model the access of a node to its neighbors. A channel (Type Channel) c connects a node n to its neighbor n': n --c--> n'
Class Channels :=

mkChannels {

Channel: Type;

Channel_setoid:> Setoid Channel;

Channel_dec: Decider (equiv (A := Channel))

}.

mkChannels {

Channel: Type;

Channel_setoid:> Setoid Channel;

Channel_dec: Decider (equiv (A := Channel))

}.

## Class Network:

A network is described by its nodes (Type Node) and links between nodes. A link is defined through a channel from one node to another.
Class Network {Chans: Channels} :=

mkNet {

Node: Type;

Node_setoid :> Setoid Node;

Node_dec: Decider (equiv (A := Node));

mkNet {

Node: Type;

Node_setoid :> Setoid Node;

Node_dec: Decider (equiv (A := Node));

link: (link n n') is

- either None when n and n' are not neighbors
- either Some c when n --c--> n', i.e. n' is the neighbor of n through channel c.

peer: (peer n c) is

- either None when c is not a channel from n
- either Some n' when n --c--> n', i.e. n' is the neighbor of n through channel c.

is_channel: is_channel n c n' holds when n --c--> n'.

peer and link cover the same edges of the network

link_peer_spec: forall n1 n2 c12,

link n1 n2 == Some c12 <-> is_channel n1 c12 n2;

link_compat: Proper fequiv link;

peer_compat: Proper fequiv peer;

link n1 n2 == Some c12 <-> is_channel n1 c12 n2;

link_compat: Proper fequiv link;

peer_compat: Proper fequiv peer;

The number of nodes is finite: this is modeled using
a (finite) list of nodes and with the predicate:
every node is in this list.

From a node a given channel points to at most one node.
Namely, each node has a local referential given by its outgoing
channels

Lemma is_channel_unique {Chans: Channels} {Net: Network}:

forall n c m m', is_channel n c m -> is_channel n c m' ->

m == m'.

forall n c m m', is_channel n c m -> is_channel n c m' ->

m == m'.

For a given network and a given node n, (peers n) is the list
of outgoing channels from n

Definition peers {Chans: Channels} {Net: Network} (n: Node): list Channel :=

map_filter (fun nn => link n nn) all_nodes.

Global Instance peers_compat {Chans: Channels} {Net: Network}:

Proper fequiv peers.

Global Instance peers_compat_equiv {Chans: Channels} {Net: Network}:

Proper (equiv ==> equivlistA equiv) peers.

map_filter (fun nn => link n nn) all_nodes.

Global Instance peers_compat {Chans: Channels} {Net: Network}:

Proper fequiv peers.

Global Instance peers_compat_equiv {Chans: Channels} {Net: Network}:

Proper (equiv ==> equivlistA equiv) peers.

peers characterization using the function peer:
every channel in (peer n) is actually a channel from n
in the network

Lemma peers_spec_peer {Chans: Channels} {Net: Network}:

forall n1 c12, InA equiv c12 (peers n1)

<->

exists n2, is_channel n1 c12 n2.

forall n1 c12, InA equiv c12 (peers n1)

<->

exists n2, is_channel n1 c12 n2.

peers characterization using the function link

Lemma peers_spec_link {Chans: Channels} {Net: Network}:

forall n1 c12, InA equiv c12 (peers n1)

<->

exists n2, link n1 n2 == Some c12.

forall n1 c12, InA equiv c12 (peers n1)

<->

exists n2, link n1 n2 == Some c12.

Class Symmetric_Network {Chans: Channels} :=

mkSymNet {

net:> Network;

sym_net: forall n1 n2,

(exists c12, is_channel n1 c12 n2) <->

(exists c21, is_channel n2 c21 n1);

mkSymNet {

net:> Network;

sym_net: forall n1 n2,

(exists c12, is_channel n1 c12 n2) <->

(exists c21, is_channel n2 c21 n1);

reverse: if c is a channel outgoing from n, then
(reverse n c) is the channel corresponding to c in
the other direction

specification of reverse:
n1 --c12--> n2 and n1 <--c21-- n2

reverse_spec: forall n1 n2 c12 c21,

is_channel n1 c12 n2 /\ is_channel n2 c21 n1 ->

reverse n1 c12 == c21;

reverse_compat:> Proper fequiv reverse

}.

is_channel n1 c12 n2 /\ is_channel n2 c21 n1 ->

reverse n1 c12 == c21;

reverse_compat:> Proper fequiv reverse

}.

reverse_spec': same as reverse_spec, maybe easier to use

Lemma reverse_spec' {Chans: Channels} {Net: Symmetric_Network}:

forall n1 c n2, is_channel n1 c n2 ->

is_channel n2 (reverse n1 c) n1.

forall n1 c n2, is_channel n1 c n2 ->

is_channel n2 (reverse n1 c) n1.

reverse is "involutive" (using adequate parameters for nodes)

Lemma reverse_involutive {Chans: Channels} {Net: Symmetric_Network}:

forall n c m, is_channel n c m ->

reverse m (reverse n c) == c.

forall n c m, is_channel n c m ->

reverse m (reverse n c) == c.

A symmetric network (as we defined it) allows no multi-edge

Lemma no_multi_edge {Chans: Channels} {Net: Symmetric_Network}:

forall n c c' m, is_channel n c m -> is_channel n c' m

-> c == c'.

forall n c c' m, is_channel n c m -> is_channel n c' m

-> c == c'.

Note on
The assumption
We say in this case that f is
The explanation applies to hardly every function in PADEC
(eg. peer, reverse and peers above).
States are attached to nodes: an algorithm describes step by
step the way the state of a node evolves. In the locally
shared memory model, this evolution depends on the state itself
but also on the state of neighbors of the node.
The class Algorithm describes the algorithm of a node. It
contains the type State (which should be endowed with a
decidable equivalence relation to express equality), and the
function run which is actually the local algorithm of the node.
The function run has 2 parameters: the current state s of the node
(let call it n) and a function sn from Channel to (option
State). A call to run:
For sn, we have the following convention (implemented in the
semantics, see RelModel, function RUN):
For a channel c, (sn c) provides the state of the neightbor pointed by c.
Otherwise it is None.
Now, if the node can access, from its current state, some
of its outgoing channels c, it will be able to access to the
states of the pointed neighbors using sn, and so to use their
values in run.
The call to

**compatibility**: Let consider the above function`f: Node -> A`

`Proper fequiv f`

means that when taking to equivalent nodes n1 and n2,
i.e., s.t.
`n1 == n2`

(in this model, this means that n1 and n2 are equal and
represent the same node in the network),
we expect that `(f n1)`

and `(f n2)`

produce the same
result. Again "same result" is expressed using relation:
`(f n1) == (f n2)`

when A is a setoid or
`(f n1) =~= (f n2)`

when A is a partial setoid.
*compatible*(implicitely: f is compatible with respect to the (partial) equivalence relations on its parameter(s) and result).## Class Algorithm:

`run s sn `

`run s sn`

returns a new state for node n.
If this new state is actually different from s, then the node
was enabled and did compute. Otherwise the run function has no
effect and this means that either the node was disabled or that the
statement of the algorithm has no effect.
Type State: state of a node

run: see above

## Stable Variable

Class Stable_Variable {Chans: Channels}

(Algo: Algorithm) (VarType: Type) (GetVar: State -> VarType) :=

{

(Algo: Algorithm) (VarType: Type) (GetVar: State -> VarType) :=

{

VarType: type of the projection

projection is compatible

GetVar projection is preserved by run

## Networks

### Subnetwork: inclusion of the peers

Definition SubNetwork_assumption {Chans: Channels} (Net: Network)

(tested_peers: Node -> list Channel) :=

forall n c, InA equiv c (tested_peers n) -> InA equiv c (peers n).

Global Instance SubNetwork_assumption_compat

{Chans: Channels} (Net: Network):

Proper ((equiv ==> equivlistA equiv) ==> equiv)

(SubNetwork_assumption Net).

(tested_peers: Node -> list Channel) :=

forall n c, InA equiv c (tested_peers n) -> InA equiv c (peers n).

Global Instance SubNetwork_assumption_compat

{Chans: Channels} (Net: Network):

Proper ((equiv ==> equivlistA equiv) ==> equiv)

(SubNetwork_assumption Net).

Definition Network_assumption {Chans: Channels} (Net: Network)

(tested_peers: Node -> list Channel) :=

forall n, equivlistA equiv (tested_peers n) (peers n).

Global Instance Network_assumption_compat

{Chans: Channels} (Net: Network):

Proper ((equiv ==> equivlistA equiv) ==> equiv)

(Network_assumption Net).

Lemma Network_is_SubNetwork:

forall {Chans: Channels} (Net: Network)

(tested_peers: Node -> list Channel),

Network_assumption Net tested_peers ->

SubNetwork_assumption Net tested_peers.

(tested_peers: Node -> list Channel) :=

forall n, equivlistA equiv (tested_peers n) (peers n).

Global Instance Network_assumption_compat

{Chans: Channels} (Net: Network):

Proper ((equiv ==> equivlistA equiv) ==> equiv)

(Network_assumption Net).

Lemma Network_is_SubNetwork:

forall {Chans: Channels} (Net: Network)

(tested_peers: Node -> list Channel),

Network_assumption Net tested_peers ->

SubNetwork_assumption Net tested_peers.

### Symmetric Networks:

- same set of peers
- for element in peers, same reverse channel

Definition Symmetric_Network_assumption {Chans: Channels}

(Net: Symmetric_Network)

(tested_peers: Node -> list Channel)

(tested_reverse: Node -> Channel -> Channel): Prop :=

Network_assumption net tested_peers /\

forall n c, InA equiv c (peers n) ->

tested_reverse n c == reverse n c.

Global Instance Symmetric_Network_assumption_compat

{Chans: Channels} (Net: Symmetric_Network):

Proper ((equiv ==> equivlistA equiv) ==> fequiv ==> equiv)

(Symmetric_Network_assumption Net).

Lemma Symmetric_Network_assumption_compat_equiv

{Chans: Channels} (Net: Symmetric_Network):

forall t1 t2 (et: (equiv ==> equivlistA equiv) t1 t2)

r1 r2

(er: forall n c, InA equiv c (t1 n) -> r1 n c == r2 n c),

Symmetric_Network_assumption Net t1 r1 ==

Symmetric_Network_assumption Net t2 r2.

Section Net_Algorithm_mapping.

Context {Chans: Channels}.

(Net: Symmetric_Network)

(tested_peers: Node -> list Channel)

(tested_reverse: Node -> Channel -> Channel): Prop :=

Network_assumption net tested_peers /\

forall n c, InA equiv c (peers n) ->

tested_reverse n c == reverse n c.

Global Instance Symmetric_Network_assumption_compat

{Chans: Channels} (Net: Symmetric_Network):

Proper ((equiv ==> equivlistA equiv) ==> fequiv ==> equiv)

(Symmetric_Network_assumption Net).

Lemma Symmetric_Network_assumption_compat_equiv

{Chans: Channels} (Net: Symmetric_Network):

forall t1 t2 (et: (equiv ==> equivlistA equiv) t1 t2)

r1 r2

(er: forall n c, InA equiv c (t1 n) -> r1 n c == r2 n c),

Symmetric_Network_assumption Net t1 r1 ==

Symmetric_Network_assumption Net t2 r2.

Section Net_Algorithm_mapping.

Context {Chans: Channels}.

General network (without reverse)
To ensure Network_Assumption,
we assume ROState is built as follows
Record ROState := mkROState {
...
lpeers: list Channel
}.
and provide the function build_links that ensures Network_Assumption

triviality :)

Lemma build_links_ensures_Network_Assumption:

forall (Net: Network),

Network_assumption Net (fun n => build_links Net n).

forall (Net: Network),

Network_assumption Net (fun n => build_links Net n).

Symmetric network (with reverse)
To ensure Symmetric_Network_Assumption,
we assume ROState is built as follows
Record ROState := mkROState {
...
lpeers_reverse: list (Channel * Channel);
pr_assume: lpeers_reverse_assume lpeers_reverse
}.
and provide functions that build links and reverse links
each peer has a unique reverse channel

- existence is ensured by construction (list)
- uniqueness is enforced by the following assumption:

Definition lpeers_reverse_assume (lp: list (Channel * Channel)) :=

forall x1 y1 x2 y2, InA equiv (x1, y1) lp ->

InA equiv (x2, y2) lp ->

x1 == x2 -> y1 == y2.

Instance lpeers_reverse_assume_compat:

Proper (equivlistA equiv ==> equiv) lpeers_reverse_assume.

Definition llpeers (lr: list (Channel * Channel)): list Channel :=

map (fun xy => fst xy) lr.

Definition llreverse (lr: list (Channel * Channel)) (c: Channel): Channel :=

let lf := filter (fun xy => if Channel_dec (fst xy) c

then true else false) lr in

match lf with nil => c | (_,y)::_ => y end.

Instance llpeers_compat: Proper fequiv llpeers.

Instance llpeers_compat_equivlist:

Proper (equivlistA equiv ==> equivlistA equiv) llpeers.

Instance llreverse_compat: Proper fequiv llreverse.

Lemma llreverse_compat_equivlist:

forall l1 l2, lpeers_reverse_assume l1 ->

equivlistA equiv l1 l2 ->

fequiv (llreverse l1) (llreverse l2).

Definition build_symlinks (Net: Symmetric_Network) (n: Node):

list (Channel * Channel) :=

map (fun c => (c, reverse n c)) (peers n).

Instance build_symlinks_compat

{Net: Symmetric_Network}: Proper fequiv (build_symlinks Net).

Instance build_symlinks_compat_equiv

{Net: Symmetric_Network}:

Proper (equiv ==> equivlistA equiv) (build_symlinks Net).

Lemma build_symlinks_ensures_lpeers_reverse_assume:

forall Net n, lpeers_reverse_assume (build_symlinks Net n).

Lemma build_links_ensures_Symmetric_Network_Assumption:

forall (Net: Symmetric_Network),

Symmetric_Network_assumption

Net (fun n => llpeers (build_symlinks Net n))

(fun n => llreverse (build_symlinks Net n)).

Lemma build_links_ensures_Symmetric_Network_Assumption_equivlist:

forall Net (pr: Node -> list (Channel * Channel)),

(forall n, equivlistA equiv (pr n)

(build_symlinks Net n)) ->

Symmetric_Network_assumption

Net (fun n => llpeers (pr n))

(fun n => llreverse (pr n)).

End Net_Algorithm_mapping.

End Distributed_Algorithm.

Unset Implicit Arguments.

Close Scope signature_scope.

forall x1 y1 x2 y2, InA equiv (x1, y1) lp ->

InA equiv (x2, y2) lp ->

x1 == x2 -> y1 == y2.

Instance lpeers_reverse_assume_compat:

Proper (equivlistA equiv ==> equiv) lpeers_reverse_assume.

Definition llpeers (lr: list (Channel * Channel)): list Channel :=

map (fun xy => fst xy) lr.

Definition llreverse (lr: list (Channel * Channel)) (c: Channel): Channel :=

let lf := filter (fun xy => if Channel_dec (fst xy) c

then true else false) lr in

match lf with nil => c | (_,y)::_ => y end.

Instance llpeers_compat: Proper fequiv llpeers.

Instance llpeers_compat_equivlist:

Proper (equivlistA equiv ==> equivlistA equiv) llpeers.

Instance llreverse_compat: Proper fequiv llreverse.

Lemma llreverse_compat_equivlist:

forall l1 l2, lpeers_reverse_assume l1 ->

equivlistA equiv l1 l2 ->

fequiv (llreverse l1) (llreverse l2).

Definition build_symlinks (Net: Symmetric_Network) (n: Node):

list (Channel * Channel) :=

map (fun c => (c, reverse n c)) (peers n).

Instance build_symlinks_compat

{Net: Symmetric_Network}: Proper fequiv (build_symlinks Net).

Instance build_symlinks_compat_equiv

{Net: Symmetric_Network}:

Proper (equiv ==> equivlistA equiv) (build_symlinks Net).

Lemma build_symlinks_ensures_lpeers_reverse_assume:

forall Net n, lpeers_reverse_assume (build_symlinks Net n).

Lemma build_links_ensures_Symmetric_Network_Assumption:

forall (Net: Symmetric_Network),

Symmetric_Network_assumption

Net (fun n => llpeers (build_symlinks Net n))

(fun n => llreverse (build_symlinks Net n)).

Lemma build_links_ensures_Symmetric_Network_Assumption_equivlist:

forall Net (pr: Node -> list (Channel * Channel)),

(forall n, equivlistA equiv (pr n)

(build_symlinks Net n)) ->

Symmetric_Network_assumption

Net (fun n => llpeers (pr n))

(fun n => llreverse (pr n)).

End Net_Algorithm_mapping.

End Distributed_Algorithm.

Unset Implicit Arguments.

Close Scope signature_scope.