ssomayyajula

/-
 - Definition of insertion sort.
 - Copyright Siva Somayyajula, 2017
 -/

namespace list

universe u
variable {α : Type u}

ssomayyajula

{- Heyting arithmetic and Fast Integer Square Root.
   Author: Siva Somayyajula -}

induction : (P : Nat -> Type)
         -> P Z
         -> ((x : Nat) -> P x -> P (S x))
         -> (n : Nat)
         -> P n
induction P pz ps n = case n of
  Z    => pz

ssomayyajula

Prereqs: General understanding of NetKAT syntax & semantics + software-defined networking (SDN)

Background: VNOs and the NetKAT pipeline

NetKAT is a network programming language designed by Prof. Nate Foster et al. based on Kleene algebra with tests, a system where regular expressions allow network paths to be described and boolean predicates to perform packet testing and processing.

Generally speaking, networks consist of programmable switches that route traffic (discrete packets of information) between nodes (hosts and other switches). Although we could program the physical network directly, it is useful to add a layer of abstraction, a virtual network (VN), so we can program/reason about the network without dealing with intermediate switches and nodes. Thus, we work with an abstraction called a Virtual Network Object (VNO) that describes a virtual network and sits on top of the physical topology as well as the physical ingress/egress predicates (which determine where packets enter and exit the phy