/agda-routing

An Agda library for reasoning about asynchronous iterative algorithms and network routing problems

Primary LanguageAgda

Agda-routing

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.

Section 2 - Model

B. Paths

C. Routing algebras

D. Synchronous DBF protocol

E. Asynchronous DBF protocol

Section 3 - Convergence results

A. Some useful concepts

B. Convergence

C. An existing convergence theorem

D. Types of routing algebras

E. DBF convergence results

Section 5: A safe-by-design algebra

Appendix B - Distance-vector proof

Appendix C - Path-vector proof