Library Network

Require Import graphs.
Require Import types.
Require Import ListFacts.

Require Import List.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Finite_sets.
Require Import Sets.Powerset.

Require Import Arith.
Require Import Coq.Logic.Classical.
Require Import Logic.FunctionalExtensionality.

Section Network.

Variable U:Type.
Hypothesis dec: forall a b:U, {a=b}+{a<>b}.
Variable ORIGIN:U.
Lemma ddec: forall a b:U*U, {a=b}+{a<>b}.

Definition Flit:=U.
Definition Queue:=list U.
Definition Nodeset:=Ensemble U.

Definition Topology:=Graph U.

Definition Network := (U*U) -> nat.

Definition NetworkState := (U*U) -> Queue.

Definition NetworkState_consistent (N:Network) (NS:NetworkState):=
forall (a b:U), length (NS (a,b)) <= (N (a,b)).

Definition initialstate (N:Network) : NetworkState :=
fun (link:(U*U))=> nil.

Lemma initial_consistent: forall (N:Network),
NetworkState_consistent N (initialstate N).

Definition RoutePolicy (N:Network):=NetworkState->(U*U)->U->Prop.

Definition InjectionPolicy (N:Network):=NetworkState->(U*U)->Prop.

Definition getpacket (NS:NetworkState) (queue:U*U): U.
Defined.

Definition injectpacket (N:Network) (NS:NetworkState) (queue:U*U) (flit:U)
:NetworkState.
Defined.

Definition destroypacket (N:Network) (NS:NetworkState) (queue:U*U)
:NetworkState.
Defined.

Definition movepacket (N:Network) (NS:NetworkState) (queue:U*U) (dest:U)
:NetworkState
:=let (a,b):=queue in
injectpacket N (destroypacket N NS queue) (b,dest) (getpacket NS queue).

Definition havepacket (NS:NetworkState) (queue:U*U):bool:=
match (NS queue) with
|nil=> false
|cons _ _=> true
end.

Definition freespace (N:Network) (NS:NetworkState) (queue:U*U):nat:=
(N queue)-(length (NS queue)).

Definition genericroutepolicy (N:Network):RoutePolicy N:=
fun (NS:NetworkState) (origin:U*U) (dest:U)=>
let (a,b):=origin in
havepacket NS origin=true /\ 0<freespace N NS (b,dest).

Definition genericinjectionpolicy (N:Network):InjectionPolicy N:=
fun (NS:NetworkState) (link:U*U)=>
0<freespace N NS (link).

Definition consistentRP (N:Network) (RP:RoutePolicy N):=
forall (NS:NetworkState) (origin:U*U) (dest:U),
RP NS origin dest->genericroutepolicy N NS origin dest.

Definition consistentIP (N:Network) (IP:InjectionPolicy N):=
forall (NS:NetworkState) (link:U*U),
IP NS link->genericinjectionpolicy N NS link.

Definition consistent_polices (N:Network) (RP:RoutePolicy N) (IP:InjectionPolicy N)
:=consistentRP N RP /\ consistentIP N IP.

Definition canconsume (NS:NetworkState) (link:U*U):bool.
Defined.

Inductive reachable_step (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N)
:NetworkState->Prop:=
|reachable_consume: forall (link:U*U), canconsume NS link=true->
 reachable_step N NS RP IP (destroypacket N NS link)
|reachable_inject: forall (link:U*U) (flit:U), (IP NS link)->
 reachable_step N NS RP IP (injectpacket N NS link flit)
|reachable_move: forall (link:U*U) (dest:U), (RP NS link dest)->
 reachable_step N NS RP IP (movepacket N NS link dest).

Inductive reachable_from (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N)
:NetworkState->Prop:=
|reachable_self: reachable_from N NS RP IP NS
|reachable_stepping: forall (NS' NSn:NetworkState),
 reachable_from N NS RP IP NS' ->
 reachable_step N NS' RP IP NSn ->
 reachable_from N NS RP IP NSn.


Definition reachable (N:Network) (RP:RoutePolicy N) (IP:InjectionPolicy N)
(NS:NetworkState):Prop:=
reachable_from N (initialstate N) RP IP NS.

Lemma consume_different: forall (N:Network) (NS:NetworkState)
(link:U*U), havepacket NS link=true->
NS<>destroypacket N NS link.
SearchAbout removelast.
Qed.

Lemma inject_different: forall (N:Network) (NS:NetworkState)
(link:U*U) (flit:U),
NS<>injectpacket N NS link flit.

Lemma move_different: forall (N:Network) (NS:NetworkState)
(link:U*U) (dest:U),
(let (a,b):=link in a<>b \/ b<>dest)->
NS<>movepacket N NS link dest.

Lemma reachable_noallpreviousequal: forall (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N), reachable N RP IP NS->
NS<>initialstate N->
(forall NS':NetworkState, reachable_step N NS' RP IP NS->
reachable N RP IP NS'-> NS'=NS)->False.


Lemma reachable_nonequalprevious: forall (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N),
reachable N RP IP NS -> NS<>initialstate N ->
exists NSp:NetworkState, NSp<>NS /\
reachable_step N NSp RP IP NS /\
reachable N RP IP NSp.

Lemma reachable_previous: forall (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N),
reachable N RP IP NS -> NS<>initialstate N ->
exists NSp:NetworkState, NSp<>NS /\
( (exists link:U*U, NS=destroypacket N NSp link)\/
(exists link:U*U, exists flit:U, NS=injectpacket N NSp link flit)\/
(exists link:U*U, exists dest:U, NS=movepacket N NSp link dest)) /\
reachable_from N NSp RP IP NS /\
reachable N RP IP NSp.

Theorem consistency_from_policies: forall (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N),
NetworkState_consistent N NS->consistent_polices N RP IP->
forall NSn:NetworkState,
reachable_from N NS RP IP NSn->NetworkState_consistent N NSn.

Definition livestate (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N):Prop:=
exists NSn:NetworkState, NS<>NSn /\
reachable_from N NS RP IP NSn.

Definition deadlock (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N):Prop:=~livestate N NS RP IP.

Lemma deadlock_is_blocked: forall (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N) (link:U*U) (dest:U),
deadlock N NS RP IP ->
canconsume NS link=false /\
~IP NS link /\
(~RP NS link dest \/ let (a,b):=link in (a=b/\b=dest)).

Inductive topology (N:Network):Topology:=
|topology_intro: forall (link:U*U), 0<N link->topology N link.


Definition Tcycle (T:Topology) : list U -> Prop:=
fun P:list U, Path U T P /\ In _ T (last P ORIGIN,hd ORIGIN P).

Definition candeadlock (N:Network) (RP:RoutePolicy N) (IP:InjectionPolicy N):=
exists NS:NetworkState,
reachable N RP IP NS /\ deadlock N NS RP IP.

Definition queue_blocked (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N) (queue:U*U):=
canconsume NS queue=false /\
let (a,b):=queue in
forall dest:U, a<>b->b<>dest->~RP NS queue dest.

Lemma deadlock_implies_allblocked: forall (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N),
deadlock N NS RP IP -> forall (queue:U*U),
queue_blocked N NS RP IP queue.


Definition livelock (N:Network) (NS:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N):Prop:=
~exists NSn:NetworkState, reachable_from N NS RP IP NSn /\
exists link:U*U, canconsume NSn link=true.


Definition THamiltonianCycle (T:Topology) (C:list U):=
Tcycle T C /\
forall x:U, count_occ dec C x=1.

Lemma THamiltonianCycle_all: forall (T:Topology) (C:list U),
THamiltonianCycle T C-> forall (x:U), List.In x C.

Lemma listInddec: forall (l:list (U*U)) (x:U*U),
{List.In x l}+{~List.In x l}.

Lemma THamiltonianCycle_selflink_simple: forall (T:Topology) (C:list U),
THamiltonianCycle T C-> forall (x:U),
~List.In (x,x) (listpairs U C).

Lemma THamiltonianCycle_selflink: forall (T:Topology) (C:list U),
THamiltonianCycle T C-> forall (x:U),
List.In (x,x) (listpairscycle U C) -> C=x::nil.

Definition bubbleroutepolicy (N:Network) (HC:list U):RoutePolicy N:=
fun (NS:NetworkState) (origin:U*U) (dest:U)=>
let (a,b):=origin in
havepacket NS origin=true /\
match listInddec (listpairscycle U HC) (b,dest) with
|left _=> match listInddec (listpairscycle U HC) (a,b) with
 |left _=> 0
 |right _=>1
 end
|right _=> 0
end <freespace N NS (b,dest).

Lemma bubbleroutepolicy_consistent: forall (N:Network) (HC:list U),
consistentRP N (bubbleroutepolicy N HC).

Definition bubbleinjectionpolicy (N:Network) (HC:list U):InjectionPolicy N:=
fun (NS:NetworkState) (link:U*U)=>
match listInddec (listpairscycle U HC) link with
|left _=> 1
|right _=> 0
end <freespace N NS link.

Lemma bubbleinjectionpolicy_consistent: forall (N:Network) (HC:list U),
consistentIP N (bubbleinjectionpolicy N HC).

Lemma notinitial_haveflits: forall (N:Network) (NS:NetworkState),
NS<>initialstate N -> exists link:U*U, NS link<>nil.

Lemma single_lives: forall (N:Network) (RP:RoutePolicy N) (IP:InjectionPolicy N)
(UNIQUE:forall x y:U, x=y),
livestate N (initialstate N) RP IP->
~candeadlock N RP IP.

Definition bubblelifecondition (N:Network) (C:list U):=
THamiltonianCycle (topology N) C /\
exists link:U*U, List.In link (listpairscycle U C) /\
2<=N link.

Theorem bubblelifecondition_initialstate: forall (N:Network) (C:list U),
bubblelifecondition N C->
livestate N (initialstate N)
 (bubbleroutepolicy N C) (bubbleinjectionpolicy N C).

Lemma rotatelist_TCycle: forall (T:Topology) (C:list U),
Tcycle T C -> Tcycle T (rotatelist U C).

Lemma rotatelist_hamiltonian: forall (T:Topology) (C:list U),
THamiltonianCycle T C -> THamiltonianCycle T (rotatelist U C).

Lemma rotatelistn_hamiltonian: forall (T:Topology) (C:list U) (n:nat),
THamiltonianCycle T C -> THamiltonianCycle T (rotatelistn U C n).

Lemma Path_included: forall (A:Type) (G:Graph A) (P:list A),
Path A G P -> forall (link:A*A),
List.In link (listpairs A P) -> In _ G link.

Lemma Tcycle_included: forall (T:Topology) (P:list U),
Tcycle T P -> forall (link:U*U),
List.In link (listpairscycle U P) -> In _ T link.

Lemma Tcycle_Network_some: forall (N:Network) (P:list U),
Tcycle (topology N) P -> forall (link:U*U),
List.In link (listpairscycle U P) -> 0<N link.

Lemma findstate_changing: forall (N:Network) (NSs NSe:NetworkState)
(RP:RoutePolicy N) (IP:InjectionPolicy N)
(P:NetworkState->Prop),
reachable_from N NSs RP IP NSe-> P NSs -> ~P NSe->
exists NSa:NetworkState,
exists NSb:NetworkState,
P NSa /\ ~P NSb /\
reachable_from N NSs RP IP NSa /\
reachable_step N NSa RP IP NSb /\
reachable_from N NSb RP IP NSe.

Theorem bubble_lives: forall (N:Network) (C:list U),
bubblelifecondition N C->
~candeadlock N (bubbleroutepolicy N C) (bubbleinjectionpolicy N C).
SearchAbout THamiltonianCycle.
SearchAbout List.In.

Qed.