Coq Library
Tools

A Framework for Certified Self-Stabilization
• Feb 2016 - updated April 2018

#### Global imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.

#### Local imports

Open Scope signature_scope.
Set Implicit Arguments.

# Distributed Algorithm:

In this section we provide the main definitions of
• Channels
• Network
• Algorithm
Usage: prove a specification of a distributed algorithm
forall Channels,
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).
Section Distributed_Algorithm.

## 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'
The type Channel is endowed with a decidable equivalence relation (equiv, notation '==') to express equality between channels.
Specifies the interface between an algorithm and a given network.
Class Channels :=
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.
The type Node is endowed with a decidable equivalence relation (equiv, notation '==') to express equality between nodes.
Network is defined w.r.t given channels.
Class Network {Chans: Channels} :=
mkNet {

Node: Type;
Node_setoid :> Setoid Node;
Node_dec:> Decider (equiv (A := Node));

• 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'.
is_channel n1 c12 n2 := peer n1 c12 == Some n2;

peer and link cover the same edges of the network
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.
all_nodes: list Node;
all_nodes_prop: forall n, InA equiv n all_nodes;
}.

Global Instance is_channel_compat {Chans: Channels} {Net: Network}:
Proper fequiv is_channel.

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'.

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.

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.

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.

## Symmetric Network: Bidirectionnal channels

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);

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': 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.

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.

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'.

Note on compatibility: Let consider the above function f: Node -> A
The assumption 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.
We say in this case that f is compatible (implicitely: f is compatible with respect to the (partial) equivalence relations on its parameter(s) and result).
The explanation applies to hardly every function in PADEC (eg. peer, reverse and peers above).

## Class Algorithm:

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: run s sn
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 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.

Class Algorithm {Chans: Channels} :=
{

Type State: state of a node
State: Type;
State_setoid:> Setoid State;
State_dec:> Decider (equiv (A := State));

run: see above

## Stable Variable

Some part of the state of the node cannot be changed by the algorithm, we call them stable or read-only variables. The class (Stable_Variable GetVar) expresses the fact that the part of the state (usually a projection) computed using GetVar is constant, i.e. cannot be changed using run;
The type of the result of GetVar should be endowed with a partial equivalence relation that represents equality (stability). We also require GetVar to be compatible.
Class Stable_Variable {Chans: Channels}
(Algo: Algorithm) (VarType: Type) (GetVar: State -> VarType) :=
{

VarType: type of the projection
projection is compatible
GetVar projection is preserved by run
GetVar_stable: forall s sn, GetVar (run s sn) =~= GetVar s
}.

## Networks

The signature of the run function assumes that the state of the node contains some information about the neighborhood and in particular some outgoing channels, to be able to use the second parameters that contains the neighbor states.
In the following, we provide tools to check that the elements stored in the state of a node about the topology actually represents the network.
See SubNetwork_assumption, Network_assumption and Symmetric_Network_assumption. Similar definition will be given for particular topologies (ring, tree...).
We comment Network_assumption (others are similar): given a network, we check that the function tested_peers exactly contains the peers represented in the network. The idea is that, from a node and its state in the algorithm, if their exists a projection that represents the peers of the node then we can instantiate tested_peers using the result of the projection and check the assumption.

### 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).

### Network: same set of peers

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.

### Symmetric Networks:

• same set of peers
• for element in peers, same reverse channel
(i.e. for every outgoing channel, we check that they have the 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}.

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

Definition build_links (Net: Network) (n: Node): list Channel :=
peers n.

triviality :)
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 }.
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).

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

{Net: Symmetric_Network}:
Proper (equiv ==> equivlistA equiv) (build_symlinks Net).

forall Net n, lpeers_reverse_assume (build_symlinks Net n).

forall (Net: Symmetric_Network),
Symmetric_Network_assumption
Net (fun n => llpeers (build_symlinks Net n))
(fun n => llreverse (build_symlinks Net n)).