Requirements: Agda 2.6.1 and Standard Library 1.6
This library reasons about asynchronous iterative algorithms and network routing
problems. It is organised in the same manner as the Agda standard library and
contains extensions of several of the Agda standard library modules. The core
contributions of this library can be found in the RoutingLib.Iteration
and
RoutingLib.Routing
directories.
This is the frozen version of the library accompanying the paper
Formally Verified Convergence of Policy-Rich DBF Routing Protocols
by Matthew L. Daggitt and Timothy G Griffin.
The latest version of the library can be found on the
master branch in this repository.
Below is a guide that helps users match up the contents of the paper with the associated formalisation in Agda.
-
Definition 1: Routing algebra
- The raw algebraic structure is in RoutingLib.Routing.Algebra.Core
- The axioms are in RoutingLib.Routing.Algebra
-
Definition 2: Path algebra - RoutingLib.Routing.Algebra
-
Some examples of basic routing algebras can be found in:
-
Adjacency matrices - RoutingLib.Routing.Basics.Network
-
Routing tables/states - RoutingLib.Routing.Basics.State
-
Synchronous iteration - RoutingLib.Routing.VectorBased.Synchronous
-
Definition 3: Synchronous state function - RoutingLib.Routing.VectorBased.Synchronous
-
Definition 4: Schedules - RoutingLib.Iteration.Asynchronous.Dynamic.Schedule
-
Definition 5: Participation topology - RoutingLib.Routing.Basics.Network.Participants
-
Definition 6: Asynchronous state function - RoutingLib.Iteration.Asynchronous.Dynamic
-
Definition 7: Preference order over paths - RoutingLib.Routing.Algebra.Core
-
Definition 8: Assignments - RoutingLib.Routing.Basics.Assignment
-
Definition 9: Preference order over assignments - RoutingLib.Routing.Basics.Assignment
-
Definition 10: Extension relation - RoutingLib.Routing.Basics.Assignment
-
Definition 11: Threatens relation - RoutingLib.Routing.Basics.Assignment
-
Definition 12: Accordant states - RoutingLib.Iteration.Asynchronous.Dynamic
-
Pseudocycles - RoutingLib.Iteration.Asynchronous.Dynamic.Schedule.Pseudoperiod
-
Definition 13: Convergent - RoutingLib.Iteration.Asynchronous.Dynamic
-
Definition 14: AMCO - RoutingLib.Iteration.Asynchronous.Dynamic.Convergence.Conditions
-
Theorem 1: AMCO implies convergent - RoutingLib.Iteration.Asynchronous.Dynamic.Convergence
-
Definition 15: Distributive routing algebra - RoutingLib.Routing.Algebra
-
Definition 16: Increasing routing algebra - RoutingLib.Routing.Algebra
-
Definition 17: Strictly increasing routing algebra - RoutingLib.Routing.Algebra
-
Definition 18: Free network topology - RoutingLib.Routing.Basics.Networks.Cycles
-
Lemma 1: Strictly increasing implies network topology always free - RoutingLib.Routing.Basics.Networks.Cycles
-
Lemma 2: Increasing path algebras are always strictly increasing - RoutingLib.Routing.Algebra.Properties.PathAlgebra
-
Theorem 2: Finite DV protocols convergent over free network topologies - RoutingLib.Routing.VectorBased.Convergence.Results
-
Theorem 3: Strictly increasing, finite DV protocols always convergent - RoutingLib.Routing.VectorBased.Convergence.Results
-
Theorem 4: PV protocols convergent over free network topologies - RoutingLib.Routing.VectorBased.Convergence.Results
-
Theorem 5: Strictly increasing PV protocols always convergent - RoutingLib.Routing.VectorBased.Convergence.Results
-
Local preferences - RoutingLib.Routing.Protocols.BGPLite.LocalPref
-
Communities - RoutingLib.Routing.Protocols.BGPLite.Communities
-
Path weights - RoutingLib.Routing.Protocols.BGPLite.PathWeights
-
Trivial route - RoutingLib.Routing.Protocols.BGPLite.Core
-
Invalid route - RoutingLib.Routing.Protocols.BGPLite.Core
-
Condition language - RoutingLib.Routing.Protocols.BGPLite.Policies
-
Condition evaluation - RoutingLib.Routing.Protocols.BGPLite.Policies
-
Policy language - RoutingLib.Routing.Protocols.BGPLite.Policies
-
Policy evaluation - RoutingLib.Routing.Protocols.BGPLite.Policies
-
Extension - RoutingLib.Routing.Protocols.BGPLite.Core
-
Extension application - RoutingLib.Routing.Protocols.BGPLite.Core
-
Path function - RoutingLib.Routing.Protocols.BGPLite.Simulation
-
Proof of convergence - RoutingLib.Routing.Protocols.BGPLite.Core
-
Dislogment order
-
Definition - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step1_FreeImpliesERO
-
Properties - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step1_FreeImpliesERO
-
Height function
-
Properties - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step2_EROImpliesHF
-
Distance function over path-weights
-
Distance function over routing tables - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
-
Distance function over routing states - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
-
Lemma 3: Routers always use the trivial route to themselves - RoutingLib.Routing.VectorBased.Synchronous.DistanceVector.Properties
-
Lemma 4: Distance strictly decreases after an iteration - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step3_HFImpliesDF_DistanceVector
-
Lemma 5: Synchronous iteration is strictly contracting
- Strictly contracting on orbits - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
- Strictly contracting on fixed points - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
- The synchronous iteration is an AMCO - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
-
Definition 19: Weight of a path - RoutingLib.Routing.Algebra
-
Definition 20: Consistent path weights - RoutingLib.Routing.Algebra.Construct.Consistent
-
Lemma 6: Choice preserves consistency - RoutingLib.Routing.Algebra.Construct.Consistent
-
Lemma 7: Extension preserves consistency - RoutingLib.Routing.Algebra.Construct.Consistent
-
Lemma 8: Synchronous iteration preserves consistency - RoutingLib.Routing.VectorBased.Synchronous.PathVector.Properties
-
Lemma 9: The set of consistent path weights is finite - RoutingLib.Routing.Algebra.Construct.Consistent
-
Inconsistent height of path-weights: RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step3_HFImpliesDF_PathVector
-
Distance function over inconsistent path-weights: RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step3_HFImpliesDF_PathVector
-
Distance function over consistent path-weights: RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step3_HFImpliesDF_PathVector
-
Distance function over path-weights: RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step3_HFImpliesDF_PathVector
-
Distance function over routing tables - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
-
Distance function over routing states - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
-
Lemma 11: Inconsistent routes cannot remain constant - RoutingLib.Routing.VectorBased.Synchronous.PathVector.Properties
-
Lemma 12: Distance strictly decreases after consecutative iteration - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step3_HFImpliesDF_PathVector
-
Lemma 13: Synchronous iteration is strictly contracting on orbits - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
-
Lemma 14: Synchronous iteration is strictly contracting on fixed points - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO
-
The synchronous iteration is an AMCO - RoutingLib.Routing.VectorBased.Asynchronous.Convergence.Step4_DFImpliesAMCO