<commit_before>\documentclass[twocolumn]{sig-alternate-10pt}
%\documentclass[twocolumn]{article}
%\documentclass[10pt]{sigalternate052015}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{xcolor}
\usepackage{url}
\usepackage{times}
\usepackage{xspace}
\usepackage{listings}
\usepackage{code}
\usepackage{algorithm}
\usepackage[noend]{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{arrows,automata,positioning}
\let\proof\relax
\let\endproof\relax
\usepackage{amsthm}
\usepackage{subcaption}
\usepackage{balance}
\usepackage[ampersand]{easylist}
\usepackage{textcomp}
\usepackage{pifont}
\newcommand{\cmark}{\ding{51}}
\newcommand{\xmark}{\ding{55}}

\definecolor{princetonorange}{RGB}{255,143,0}
\definecolor{tmlblue}{RGB}{0,58,120}  % tmlblue == Toronto Maple Leafs Blue!

\newcommand{\todo}[1]{\textcolor{red}{[TODO: #1]}}
\newcommand{\ratul}[1]{\textcolor{blue}{[ratul: #1]}}
\newcommand{\ryan}[1]{\textcolor{green}{[ryan: #1]}}
\newcommand{\dpw}[1]{\textcolor{tmlblue}{[dpw: #1]}}
\newcommand{\todd}[1]{\textcolor{princetonorange}{[todd: #1]}}

\newcommand{\EG}{\emph{e.g.}}
\newcommand{\IE}{\emph{i.e.}}
\newcommand{\ETC}{\emph{etc.}}
\newcommand{\ETAL}{\emph{et al.}}

\newcommand{\sysname}{{\small \sf Methane}\xspace}
\newcommand{\sysnamesec}{{\sf Methane}\xspace}
\newcommand{\propane}{{\small \sf Propane}\xspace}

\newcommand{\para}[1]{\paragraph*{\textbf{#1}}}

\newcommand{\set}[1]{\ensuremath{\{ #1 \} }}
\newcommand{\abs}[1]{\ensuremath{ \lvert #1 \rvert }}

\newcommand{\CD}[1]{\texttt{\small #1}}  % code font
\newcommand{\KW}[1]{\texttt{\small\bfseries{#1}}}

\newcommand{\True}{\CD{true}}
\newcommand{\Define}{\KW{define}}
\newcommand{\Prefer}{\texttt{>>}}
\newcommand{\Path}{\texttt{=>}}
\newcommand{\Link}{\texttt{->}}
\newcommand{\Agg}{\KW{agg}}
\newcommand{\Any}{\KW{any}}
\newcommand{\None}{\KW{drop}}
\newcommand{\In}{\KW{in}}
\newcommand{\Out}{\KW{out}}
\newcommand{\AND}{\texttt{\&}}
\newcommand{\OR}{\texttt{|}}
\newcommand{\NOT}{\texttt{!}}
\newcommand{\Intersect}{\ensuremath{\cap}}
\newcommand{\Union}{\ensuremath{\cup}}

\newcommand{\Exit}{\KW{exit}}
\newcommand{\End}{\KW{end}}
\newcommand{\Start}{\KW{start}}
\newcommand{\Enter}{\KW{enter}}
\newcommand{\Eventually}{\KW{eventually}}
\newcommand{\Already}{\KW{already}}
\newcommand{\Internal}{\KW{internal}}
\newcommand{\Never}{\KW{never}}
\newcommand{\Always}{\KW{always}}
\newcommand{\Through}{\KW{through}}
\newcommand{\LinkKW}{\KW{link}}
\newcommand{\PathKW}{\KW{path}}
\newcommand{\Novalley}{\KW{novalley}}

\renewcommand{\path}[2]{ #1 \mapsto \ensuremath{#2} }

%% grammar
\newcommand{\BNFALT}{\;\;|\;\;}
\newcommand{\hdr}[2]{\flushleft \chdr{\hspace{5mm}#1}{#2}}
\newcommand{\chdr}[2]{\textbf{#1} {#2} \\ \centering}%

\newtheorem{thm}{Theorem}[section]
\newtheorem{defn}{Definition}
\newtheorem{lem}[thm]{Lemma}

\begin{document}

\special{papersize=8.5in,11in}
\setlength{\pdfpageheight}{\paperheight}
\setlength{\pdfpagewidth}{\paperwidth}

\appendix

\onecolumn
\section{Preliminaries}

\subsection{Methane}

The full \sysname syntax as well as expansions from constraints into regular expressions are shown in Figure~\ref{fig:syntax}. The language includes constraints of the form $\CD{\Agg(pfx, \ensuremath{r_1 \rightarrow r_2})}$ that say that aggregation for summary prefix $\CD{pfx}$ will occur from any single location matching $\CD{\ensuremath{r_1}}$ to any location matching $\CD{\ensuremath{r_2}}$.


\begin{figure*}[h!]\small
  \begin{minipage}[t]{.45\linewidth}
  \hdr{Syntax}{}
  \vspace*{-1\baselineskip}
  %
  \[ \begin{array}{rclr}
    \hline%

     pol     &::=& p_1, \dots, p_n & \textit{policies} \\
     p       &::=& t \hspace{.3em} \Path \hspace{.3em} r_1 \Prefer \dots \Prefer r_m \BNFALT cc & \textit{constraints} \\
     pfx     &::=& d.d.d.d/[d..d] & \textit{prefix} \\
     t       &::=& \$x & \textit{template variable} \\
         &\BNFALT& pfx & \textit{prefix test} \\
     r       &::=& l & \textit{location} \\
         &\BNFALT& \emptyset & \textit{empty set} \\
         &\BNFALT& \In & \textit{internal loc} \\
         &\BNFALT& \Out & \textit{external loc} \\
         &\BNFALT& r_1 \cup r_2 & \textit{union} \\
         &\BNFALT& r_1 \cap r_2 & \textit{intersection} \\
         &\BNFALT& r_1 \cdot r_2 & \textit{concatenation} \\
         &\BNFALT& \NOT r & \textit{path negation} \\
         &\BNFALT& r^* & \textit{iteration} \\
     cc     &::=& agg(pfx, r_1 \rightarrow r_2)  & \textit{control constraints} \\
  \end{array} \]%

  \end{minipage}
  %
  ~~
  \vrule
  ~~
  %
  \begin{minipage}[t]{.5\linewidth}\small
  \hdr{Expansions}{}
  \vspace*{-1\baselineskip}
  %
  \[\begin{array}{rcl}
    \hline
    \Any               & = & \Sigma^* \\
    \None              & = & \emptyset \\
    \Internal          & = & \In^+ \\
    \Always(X)         & = & X^* \\
    \Never(X)          & = & (!X)^* \\
    \Through(X)        & = & \Sigma^* \cdot X \cdot \Sigma^* \\
    \End(X)            & = & \Sigma^* \cdot X \\
    \Start(X)          & = & X \cdot \Sigma^* \\
    \Enter(X)          & = & \Sigma^* \cdot \Out \cdot (X \cap \In) \cdot \Sigma^* ~ \cup \\
                       &   & \Sigma^* \cdot (X \cap \Out) \cdot \In \cdot \Sigma^* \\
    \Exit(X)           & = & \Sigma^* \cdot \In \cdot (X \cap \Out) \cdot \Sigma^* ~ \cup \\
                       &   & \Sigma^* \cdot (X \cap \In) \cdot \Out \cdot \Sigma^* \\
    \LinkKW(X,Y)       & = & \Sigma^* \cdot X \cdot Y \cdot \Sigma^* \\
    \PathKW(\vec{X})   & = & \Sigma^* \cdot X_1 \dots X_n \cdot \Sigma^* \\
    \Novalley(\vec{X}) & = & \NOT\PathKW(X_2,X_1,X_2) ~ \cap \dots \cap \\
                       &   & \NOT\PathKW(X_n,X_{n-1},X_n) \\
  \end{array} \]%

  \end{minipage}%

  \hrulefill%
  \vspace{1em}

  \caption{Methane syntax and expansions.}
  \label{fig:syntax}
  %\vspace{-1em}
\end{figure*}%



\subsection{BGP Configuration}

We define syntax for an abstraction of BGP configurations -- called ABGP -- in Figure~\ref{fig:abgp-syntax}. An ABGP policy consists of a map from topology locations $l$ to router configurations $rc$. Each router configuration $rc$ is a sequence of prefix (templates) $t$ and their corresponding prefix configuration $pc$. A prefix configuration $pc$ is a sequence of match actions $ma$. Each match action $ma$ consists of a preference value $n$, followed by a set of peers $ns$ and community value (\IE, state of the product graph) $n$, and the exports the route to a new set of neighbors $ns$ and updates the community value $n$.

\vspace{2em}
\begin{figure}[h!]\small

  \hrulefill%
  \vspace{1em}

  \begin{minipage}[t]{.5\linewidth}
  \vspace*{-1\baselineskip}
  %
  \[ \begin{array}{rclr}
     abgp &::=& l_1 \rightarrow {rc}_1, ~\dots,~ l_k \rightarrow {rc}_k & \textit{abgp policy} \\
     rc   &::=& t_1 \rightarrow {pc}_1, ~\dots,~ t_k \rightarrow {pc}_k & \textit{router config} \\
     pc   &::=& ma_1, \dots, ma_k & \textit{prefix config} \\
     ma   &::=& n_1 : ({ns}_1, n_2) \rightarrow ({ns}_2, n_3) & \textit{match action} \\
     ns   &::=& \{ l_1, ~\dots,~ l_k \} & \textit{peers} \\
  \end{array} \]%

  \end{minipage}
  %
  ~~
  \vrule
  ~~
  %
  \begin{minipage}[t]{.5\linewidth}
  \vspace*{-1\baselineskip}
  %
  \[ \begin{array}{l}
     \textbf{compile}_\textbf{ABGP}(PG,ord) = \{ \\
     ~~~~~ \{ l \rightarrow rc ~\vert \\
     ~~~~~~~~~ l \in internal(V) \\
     ~~~~~~~~~ m = (l,q_m) \in PG, \\
     ~~~~~~~~~ in = \{ b_i ~\vert~ n_i = (b_i,q_n) \in \text{adjIn}(PG,m) \} \\
     ~~~~~~~~~ out = \{ c ~\vert~ (c,\dots) \in \text{adjOut}(PG,m) \} \\
     ~~~~~~~~~ rc = ord(m) : (in,q_n) \rightarrow (out,q_m) \\

     ~~~~~ \}
  \end{array} \]%

  \end{minipage}

  \vspace{1em}
  \hrulefill%
  \vspace{1em}

  \caption{Simplified BGP syntax.}
  \label{fig:abgp-syntax}
\end{figure}%

We assume a particular router $l$ appears at most once in any abgp specification.
An abgp configuration is a partial function from router to prefix configuration.
We write $abgp(l)$ to apply such a config to a router location $l$.
%
We often build configs using set-builder notation.  For instance,
$\{l \rightarrow rc ~\vert~ l \in V \wedge p(l,rc)\}$ denotes the abgp policy

\[ \begin{array}{c}
  l_1 \rightarrow rc_{11},... \\
  ...           \\
  l_k \rightarrow rc_{1k},... \\
\end{array} \]


where $l_1, ..., l_k$ are the nodes in the topology
and each $rc_{ij}$ satisfies $p(l_i,rc_{ij})$. Similarly for $rc$.

Figure~\ref{fig:abgp-syntax} also defines the translation of the product graph $PG = (G', s, P)$ to the ABGP representation. It looks at each incoming neighbor with the same community state $q_n$ and matches any of those neighbor with the preference provided by the ordering $ord$ obtained from the search for local preferences. It then exports this advertisement to each adjacent peer along an outgoing edge and adds the community value for the current state $q_m$.


\subsection{Concretization}

Here we define what it means to concretize an abstract \sysname policy. 
Concretization takes as input, a policy and a map $m$ from template prefix to a set of concrete prefixes.

\[ \begin{array}{rcl}
  con(\emptyset,m)                        & = & \emptyset \\
  con(l,m)                                & = & \Sigma ~ \{ l_i \in f^{-1}(l) \} \\
  con(r_1 \cup r_2,m)                     & = & con(r_1,m) \cup con(r_2,m) \\
  con(r_1 \cap r_2,m)                     & = & con(r_1,m) \cap con(r_2,m) \\
  con(!r,m)                               & = & !con(r,m) \\
  con(r^*,m)                              & = & con(r,m)^* \\
  con(pfx \Rightarrow r_1, \dots, r_n,m)  & = & pfx \Rightarrow con(r_1,m), \dots, con(r_n,m) \\
  con(\$x \Rightarrow r_1, \dots, r_n,m)  & = & \{ pfx \Rightarrow con(r_1,m), \dots, con(r_n,m) ~\vert~ {pfx} \in m(x) \} \\
\end{array} \]

For each regular expression $r$, we replace each abstract location with the sum over its corresponding concrete locations under the inverse homomorphism $f^{-1}$. For each template variable, we replace it with a single entry for each of its corresponding concrete values under the supplied mapping $m$.
We can also define concretization over the ABGP policy as:

\[ \begin{array}{rcl}
     con(l_1 \rightarrow {rc}_1, ~\dots,~ l_k \rightarrow {rc}_k,m) 
        & = & 
        \{ x \rightarrow con(rc_i,m)  ~\vert~ x \in f^{-1}(l_i) \}
        \\
     con(t_1 \rightarrow {pc}_1, ~\dots,~ t_k \rightarrow {pc}_k,m) 
        & = &  
        \{ pfx \rightarrow con(pc_i,m) ~\vert~ pfx \in m(t_i) \}
        \\
     con(ma_1, \dots, ma_k,m) 
        & = &
        con(ma_1,m), \dots, con(ma_k,m)
        \\
     con(n_1 : ({ns}_1, n_2) \rightarrow ({ns}_2, n_3),m) 
        & = & 
        n_1 : (con({ns}_1,m), n_2) \rightarrow (con({ns}_2,m),n_3)
        \\
     con(\{ l_1, ~\dots,~ l_k \}, m) 
        & = &  
        \bigcup ~ \{ f^{-1}(l_i) \}
        \\
\end{array} \]

\subsection{Notation}

Throughout the remainder of the appendix, we use the following convention for metavariables:

\[ \begin{array}{ll}
  \text{Product Graph nodes} & n,m,o \\
  \text{Topology locations} & a,b,c \\
  \text{Automata states} & q_i \\
  \text{Topologies} & G, G^A \\
  \text{Product Graph} & PG, PG^A \\
  \text{Automata} & M_i, M_i^A \\
\end{array} \]

We use capital letters for abstract topology/product graph nodes and we use lower case letters for concrete topology nodes. By default, product graph nodes with different subscripts refer to nodes that share the same topology location (\IE, $n_1 \approx n_2$). A superscript $G^A$ refers to the abstract version (in this case of the topology), while the non-superscripted value refers to the concrete version.


\section{Substitution Theorem}

The goal of this section is to prove that the concretization and compilation functions commute. That is -- we can perform compilation directly over the abstraction and only substitute for the concrete values afterwards.


\end{document}<commit_msg>start adding substitution theorem to the appendix<commit_after>\documentclass[twocolumn]{sig-alternate-10pt}
%\documentclass[twocolumn]{article}
%\documentclass[10pt]{sigalternate052015}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{xcolor}
\usepackage{url}
\usepackage{times}
\usepackage{xspace}
\usepackage{listings}
\usepackage{code}
\usepackage{algorithm}
\usepackage[noend]{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{arrows,automata,positioning}
\let\proof\relax
\let\endproof\relax
\usepackage{amsthm}
\usepackage{subcaption}
\usepackage{balance}
\usepackage[ampersand]{easylist}
\usepackage{textcomp}
\usepackage{pifont}
\newcommand{\cmark}{\ding{51}}
\newcommand{\xmark}{\ding{55}}

\definecolor{princetonorange}{RGB}{255,143,0}
\definecolor{tmlblue}{RGB}{0,58,120}  % tmlblue == Toronto Maple Leafs Blue!

\newcommand{\todo}[1]{\textcolor{red}{[TODO: #1]}}
\newcommand{\ratul}[1]{\textcolor{blue}{[ratul: #1]}}
\newcommand{\ryan}[1]{\textcolor{green}{[ryan: #1]}}
\newcommand{\dpw}[1]{\textcolor{tmlblue}{[dpw: #1]}}
\newcommand{\todd}[1]{\textcolor{princetonorange}{[todd: #1]}}

\newcommand{\EG}{\emph{e.g.}}
\newcommand{\IE}{\emph{i.e.}}
\newcommand{\ETC}{\emph{etc.}}
\newcommand{\ETAL}{\emph{et al.}}

\newcommand{\sysname}{{\small \sf Methane}\xspace}
\newcommand{\sysnamesec}{{\sf Methane}\xspace}
\newcommand{\propane}{{\small \sf Propane}\xspace}

\newcommand{\para}[1]{\paragraph*{\textbf{#1}}}

\newcommand{\set}[1]{\ensuremath{\{ #1 \} }}
\newcommand{\abs}[1]{\ensuremath{ \lvert #1 \rvert }}

\newcommand{\CD}[1]{\texttt{\small #1}}  % code font
\newcommand{\KW}[1]{\texttt{\small\bfseries{#1}}}

\newcommand{\True}{\CD{true}}
\newcommand{\Define}{\KW{define}}
\newcommand{\Prefer}{\texttt{>>}}
\newcommand{\Path}{\texttt{=>}}
\newcommand{\Link}{\texttt{->}}
\newcommand{\Agg}{\KW{agg}}
\newcommand{\Any}{\KW{any}}
\newcommand{\None}{\KW{drop}}
\newcommand{\In}{\KW{in}}
\newcommand{\Out}{\KW{out}}
\newcommand{\AND}{\texttt{\&}}
\newcommand{\OR}{\texttt{|}}
\newcommand{\NOT}{\texttt{!}}
\newcommand{\Intersect}{\ensuremath{\cap}}
\newcommand{\Union}{\ensuremath{\cup}}

\newcommand{\Exit}{\KW{exit}}
\newcommand{\End}{\KW{end}}
\newcommand{\Start}{\KW{start}}
\newcommand{\Enter}{\KW{enter}}
\newcommand{\Eventually}{\KW{eventually}}
\newcommand{\Already}{\KW{already}}
\newcommand{\Internal}{\KW{internal}}
\newcommand{\Never}{\KW{never}}
\newcommand{\Always}{\KW{always}}
\newcommand{\Through}{\KW{through}}
\newcommand{\LinkKW}{\KW{link}}
\newcommand{\PathKW}{\KW{path}}
\newcommand{\Novalley}{\KW{novalley}}

\renewcommand{\path}[2]{ #1 \mapsto \ensuremath{#2} }

%% grammar
\newcommand{\BNFALT}{\;\;|\;\;}
\newcommand{\hdr}[2]{\flushleft \chdr{\hspace{5mm}#1}{#2}}
\newcommand{\chdr}[2]{\textbf{#1} {#2} \\ \centering}%

\newtheorem{thm}{Theorem}[section]
\newtheorem{defn}{Definition}
\newtheorem{lem}[thm]{Lemma}

\begin{document}

\special{papersize=8.5in,11in}
\setlength{\pdfpageheight}{\paperheight}
\setlength{\pdfpagewidth}{\paperwidth}

\appendix

\onecolumn
\section{Definitions}

\subsection{Methane}

The full \sysname syntax as well as expansions from constraints into regular expressions are shown in Figure~\ref{fig:syntax}. The language includes constraints of the form $\CD{\Agg(pfx, \ensuremath{r_1 \rightarrow r_2})}$ that say that aggregation for summary prefix $\CD{pfx}$ will occur from any single location matching $\CD{\ensuremath{r_1}}$ to any location matching $\CD{\ensuremath{r_2}}$.


\begin{figure*}[h!]\small
  \begin{minipage}[t]{.45\linewidth}
  \hdr{Syntax}{}
  \vspace*{-1\baselineskip}
  %
  \[ \begin{array}{rclr}
    \hline%

     pol     &::=& p_1, \dots, p_n & \textit{policies} \\
     p       &::=& t \hspace{.3em} \Path \hspace{.3em} r_1 \Prefer \dots \Prefer r_m \BNFALT cc & \textit{constraints} \\
     pfx     &::=& d.d.d.d/[d..d] & \textit{prefix} \\
     t       &::=& \$x & \textit{template variable} \\
         &\BNFALT& pfx & \textit{prefix test} \\
     r       &::=& l & \textit{location} \\
         &\BNFALT& \emptyset & \textit{empty set} \\
         &\BNFALT& \In & \textit{internal loc} \\
         &\BNFALT& \Out & \textit{external loc} \\
         &\BNFALT& r_1 \cup r_2 & \textit{union} \\
         &\BNFALT& r_1 \cap r_2 & \textit{intersection} \\
         &\BNFALT& r_1 \cdot r_2 & \textit{concatenation} \\
         &\BNFALT& \NOT r & \textit{path negation} \\
         &\BNFALT& r^* & \textit{iteration} \\
     cc     &::=& agg(pfx, r_1 \rightarrow r_2)  & \textit{control constraints} \\
  \end{array} \]%

  \end{minipage}
  %
  ~~
  \vrule
  ~~
  %
  \begin{minipage}[t]{.5\linewidth}\small
  \hdr{Expansions}{}
  \vspace*{-1\baselineskip}
  %
  \[\begin{array}{rcl}
    \hline
    \Any               & = & \Sigma^* \\
    \None              & = & \emptyset \\
    \Internal          & = & \In^+ \\
    \Always(X)         & = & X^* \\
    \Never(X)          & = & (!X)^* \\
    \Through(X)        & = & \Sigma^* \cdot X \cdot \Sigma^* \\
    \End(X)            & = & \Sigma^* \cdot X \\
    \Start(X)          & = & X \cdot \Sigma^* \\
    \Enter(X)          & = & \Sigma^* \cdot \Out \cdot (X \cap \In) \cdot \Sigma^* ~ \cup \\
                       &   & \Sigma^* \cdot (X \cap \Out) \cdot \In \cdot \Sigma^* \\
    \Exit(X)           & = & \Sigma^* \cdot \In \cdot (X \cap \Out) \cdot \Sigma^* ~ \cup \\
                       &   & \Sigma^* \cdot (X \cap \In) \cdot \Out \cdot \Sigma^* \\
    \LinkKW(X,Y)       & = & \Sigma^* \cdot X \cdot Y \cdot \Sigma^* \\
    \PathKW(\vec{X})   & = & \Sigma^* \cdot X_1 \dots X_n \cdot \Sigma^* \\
    \Novalley(\vec{X}) & = & \NOT\PathKW(X_2,X_1,X_2) ~ \cap \dots \cap \\
                       &   & \NOT\PathKW(X_n,X_{n-1},X_n) \\
  \end{array} \]%

  \end{minipage}%

  \hrulefill%
  \vspace{1em}

  \caption{Methane syntax and expansions.}
  \label{fig:syntax}
  %\vspace{-1em}
\end{figure*}%



\subsection{BGP Configuration}

We define syntax for an abstraction of BGP configurations -- called ABGP -- in Figure~\ref{fig:abgp-syntax}. An ABGP policy consists of a map from topology locations $l$ to router configurations $rc$. Each router configuration $rc$ is a sequence of prefix (templates) $t$ and their corresponding prefix configuration $pc$. A prefix configuration $pc$ is a sequence of match actions $ma$. Each match action $ma$ consists of a preference value $n$, followed by a set of peers $ns$ and community value (\IE, state of the product graph) $n$, and the exports the route to a new set of neighbors $ns$ and updates the community value $n$.

\vspace{2em}
\begin{figure}[h!]\small

  \hrulefill%
  \vspace{1em}

  \begin{minipage}[t]{.5\linewidth}
  \vspace*{-1\baselineskip}
  %
  \[ \begin{array}{rclr}
     abgp &::=& l_1 \rightarrow {rc}_1, ~\dots,~ l_k \rightarrow {rc}_k & \textit{abgp policy} \\
     rc   &::=& t_1 \rightarrow {pc}_1, ~\dots,~ t_k \rightarrow {pc}_k & \textit{router config} \\
     pc   &::=& ma_1, \dots, ma_k & \textit{prefix config} \\
     ma   &::=& n_1 : ({ns}_1, n_2) \rightarrow ({ns}_2, n_3) & \textit{match action} \\
     ns   &::=& \{ l_1, ~\dots,~ l_k \} & \textit{peers} \\
  \end{array} \]%

  \end{minipage}
  %
  ~~
  \vrule
  ~~
  %
  \begin{minipage}[t]{.5\linewidth}
  \vspace*{-1\baselineskip}
  %
  \[ \begin{array}{l}
     \textbf{compile}_\textbf{ABGP}(PG,ord) = \{ \\
     ~~~~~ \{ l \rightarrow rc ~\vert \\
     ~~~~~~~~~ l \in internal(V) \\
     ~~~~~~~~~ m = (l,q_m) \in PG, \\
     ~~~~~~~~~ in = \{ b_i ~\vert~ n_i = (b_i,q_n) \in \text{adjIn}(PG,m) \} \\
     ~~~~~~~~~ out = \{ c ~\vert~ (c,\dots) \in \text{adjOut}(PG,m) \} \\
     ~~~~~~~~~ rc = ord(m) : (in,q_n) \rightarrow (out,q_m) \\

     ~~~~~ \}
  \end{array} \]%

  \end{minipage}

  \vspace{1em}
  \hrulefill%
  \vspace{1em}

  \caption{Simplified BGP syntax.}
  \label{fig:abgp-syntax}
\end{figure}%

We assume a particular router $l$ appears at most once in any abgp specification.
An abgp configuration is a partial function from router to prefix configuration.
We write $abgp(l)$ to apply such a config to a router location $l$.
%
We often build configs using set-builder notation.  For instance,
$\{l \rightarrow rc ~\vert~ l \in V \wedge p(l,rc)\}$ denotes the abgp policy

\[ \begin{array}{c}
  l_1 \rightarrow rc_{11},... \\
  ...           \\
  l_k \rightarrow rc_{1k},... \\
\end{array} \]


where $l_1, ..., l_k$ are the nodes in the topology
and each $rc_{ij}$ satisfies $p(l_i,rc_{ij})$. Similarly for $rc$.

Figure~\ref{fig:abgp-syntax} also defines the translation of the product graph $PG = (G', s, P)$ to the ABGP representation. It looks at each incoming neighbor with the same community state $q_n$ and matches any of those neighbor with the preference provided by the ordering $ord$ obtained from the search for local preferences. It then exports this advertisement to each adjacent peer along an outgoing edge and adds the community value for the current state $q_m$.


\subsection{Concretization}

Here we define what it means to concretize an abstract \sysname policy. 
Concretization takes as input, a policy and a map $m$ from template prefix to a set of concrete prefixes.

\[ \begin{array}{rcl}
  con(\emptyset,m)                        & = & \emptyset \\
  con(l,m)                                & = & \Sigma ~ \{ l_i \in f^{-1}(l) \} \\
  con(r_1 \cup r_2,m)                     & = & con(r_1,m) \cup con(r_2,m) \\
  con(r_1 \cap r_2,m)                     & = & con(r_1,m) \cap con(r_2,m) \\
  con(!r,m)                               & = & !con(r,m) \\
  con(r^*,m)                              & = & con(r,m)^* \\
  con(pfx \Rightarrow r_1, \dots, r_n,m)  & = & pfx \Rightarrow con(r_1,m), \dots, con(r_n,m) \\
  con(\$x \Rightarrow r_1, \dots, r_n,m)  & = & \{ pfx \Rightarrow con(r_1,m), \dots, con(r_n,m) ~\vert~ {pfx} \in m(x) \} \\
\end{array} \]

For each regular expression $r$, we replace each abstract location with the sum over its corresponding concrete locations under the inverse homomorphism $f^{-1}$. For each template variable, we replace it with a single entry for each of its corresponding concrete values under the supplied mapping $m$.
We can also define concretization over the ABGP policy as:

\[ \begin{array}{rcl}
     con(l_1 \rightarrow {rc}_1, ~\dots,~ l_k \rightarrow {rc}_k,m) 
        & = & 
        \{ x \rightarrow con(rc_i,m)  ~\vert~ x \in f^{-1}(l_i) \}
        \\
     con(t_1 \rightarrow {pc}_1, ~\dots,~ t_k \rightarrow {pc}_k,m) 
        & = &  
        \{ pfx \rightarrow con(pc_i,m) ~\vert~ pfx \in m(t_i) \}
        \\
     con(ma_1, \dots, ma_k,m) 
        & = &
        con(ma_1,m), \dots, con(ma_k,m)
        \\
     con(n_1 : ({ns}_1, n_2) \rightarrow ({ns}_2, n_3),m) 
        & = & 
        n_1 : (con({ns}_1,m), n_2) \rightarrow (con({ns}_2,m),n_3)
        \\
     con(\{ l_1, ~\dots,~ l_k \}, m) 
        & = &  
        \bigcup ~ \{ f^{-1}(l_i) \}
        \\
\end{array} \]

\subsection{Abstraction}

A network topology is a graph $G$ = ($V, E$), where $V$ is a set of vertices and $E \colon V \times V$ a set of directed edges. A role-based abstraction is a graph homomorphism from $G$ to an abstract graph $G^A$ = ($V^A$,$E^A$). A graph homorphism $f : G \rightarrow G^A$ is a function that maps each node in the concrete graph to a node in the abstract graph such that, whenever $(u,v) \in E$, then $(f(u),f(v)) \in E^A$. We write $f^{-1}(v)$ to denote the set of concrete nodes mapping to the abstract node $v$. Given a path as a sequence of locations $p = l_1, \dots, l_k$ we define $f(p) = f(l_1), \dots, f(l_k)$.


\subsection{Notation}

Throughout the remainder of the appendix, we use the following convention for metavariables:

\[ \begin{array}{ll}
  \text{Product Graph nodes} & n,m,o \\
  \text{Topology locations} & a,b,c \\
  \text{Automata states} & q_i \\
  \text{Topologies} & G, G^A \\
  \text{Product Graph} & PG, PG^A \\
  \text{Automata} & M_i, M_i^A \\
\end{array} \]

We use capital letters for abstract topology/product graph nodes and we use lower case letters for concrete topology nodes. By default, product graph nodes with different subscripts refer to nodes that share the same topology location (\IE, $n_1 \approx n_2$). A superscript $G^A$ refers to the abstract version (in this case of the topology), while the non-superscripted value refers to the concrete version.


\section{Substitution Theorem}

The goal of this section is to prove that the concretization and compilation functions commute. That is -- we can perform compilation directly over the abstraction and only substitute for the concrete values afterwards.

\subsection{Automata}

\newcommand{\Lang}{\ensuremath{\mathcal{L}}}



\begin{lem}
  For any map $m$ and regular expression $r$ over abstract locations, path $p \in \Lang(con(r,m)) \iff f(p) \in \Lang(r)$.
\end{lem}
\begin{proof}
By induction on the structure of $r$

\emph{Case $\emptyset$:}
  \[ \begin{array}{lll}
    p \in \Lang(con(\emptyset)) &\iff& f(p) \in \Lang(\emptyset) \\
    p \in \emptyset &\iff& f(p) \in \emptyset \\
  \end{array} \]

\emph{Case $l$:}
  \[ \begin{array}{lll}
    p \in \Lang(con(l)) &\iff& f(p) \in \Lang(l) \\
    p \in \Lang(\Sigma ~ f^{-1}(l)) &\iff& f(p) \in \Lang(l) \\
    p \in \bigcup f^{-1}(l) &\iff& f(p) \in \Lang(l) \\
    p \in f^{-1}(l) &\iff& f(p) \in \{ l \} \\
    p \in f^{-1}(l) &\iff& f(p) = l \\
    \text{by homomorphism} & & \\
  \end{array} \]

\emph{Case $r_1 \cup r_2$:}
  \[ \begin{array}{lll}
    p \in \Lang(con(r_1 \cup r_1)) &\iff& f(p) \in \Lang(r_1 \cup r_2) \\
    p \in \Lang(con(r_1) \cup con(r_1)) &\iff& f(p) \in \Lang(r_1 \cup r_2) \\
    p \in \Lang(con(r_1)) \cup \Lang(con(r_1)) &\iff& f(p) \in \Lang(r_1 \cup r_2) \\
    p \in \Lang(con(r_1)) \vee p \in \Lang(con(r_1)) 
       &\iff& 
       f(p) \in \Lang(r_1) \vee f(p) \in \Lang(r_2) \\
    \text{by cases + IH} & & \\
  \end{array} \]

\emph{Case $r_1 \cap r_2$:} 
  \[ \begin{array}{c}
    \text{symmetric to } \cup \text{ case}
  \end{array} \]

\emph{Case $!r$:}
  \[ \begin{array}{lll}
    p \in \Lang(con(!r)) &\iff& f(p) \in \Lang(!r) \\
    p \in \Lang(!con(r)) &\iff& f(p) \in \Lang(!r) \\
    p \in \Sigma^* - \Lang(con(r)) &\iff& f(p) \in \Sigma^* - \Lang(r) \\
    \text{by IH} & & \\
  \end{array} \]

\emph{Case $r^*$:}
  \[ \begin{array}{lll}
    p \in \Lang(con(r^*)) &\iff& f(p) \in \Lang(r^*) \\
    \ryan{TODO} & & \\
  \end{array} \]

\end{proof}



\begin{defn}
If $r$ complies to state machine $M^A$, then we compile the policy $con(r)$ in the following way:

  \[ \begin{array}{ll}
    1. & \sigma^A(q,f(l)) = q' \iff \sigma(q,l) = q' \\
    2. & q \in F^A \iff q \in F \\
  \end{array} \]

That is, we construct a new automata over the same states and final states, but with a different transition function $\sigma$. This ensures that there is a bisimulation between the two state machines.

\end{defn}


\begin{lem}
  $M^A$ matches $f(p)$ $\iff$ $M$ matches $p$.
\end{lem}

\begin{proof}
  Suppose $M^A$ matches $f(p) = A_1, \dots, A_k$, then there exists a trace through $M^A$ of the form:

  $$q_0, q_1, \dots, q_{k+1}$$

  where $\sigma^A(q_i, A_i) = q_{i+1}$ and $q_{k+1} \in F^A$. We must show that $M$ matches $p = a_1, \dots, a_k$. 

  From the construction of the automaton, we know that $\sigma(q_i, a_i) = q_{i+1}$ and $q_{k+1} \in F \iff q_{k+1} \in F^A$. Therefore, the trace $q_0, q_1, \dots, q_{k+1}$ is accepted by $M$. 
  %
  The same proof is symmetric for the other direction.
\end{proof}


\begin{thm}
  $M$ matches $p$ $\iff$ $p \in \Lang(con(r))$
  \begin{proof}
    \[ \begin{array}{lllr}
      M ~\text{matches}~ p &\iff& M^A ~\text{matches}~ f(p) & \textit{previous lemma} \\
                         &\iff& f(p) \in \Lang(r) & \textit{automaton construction} \\
                         &\iff& p \in \Lang(con(r)) & \textit{first lemma} \\
    \end{array} \]

  \end{proof}
\end{thm}


\subsection{Product Graph}

\begin{defn}
  Because compilation guarantees that the automata states are the same under the concretization function, we can lift the graph homomorphism $f$ to a new homomorphism $f_{pg}$ over the product graph in the following way:
  \[ \begin{array}{rcl}
    f_{pg}( s ) & = & s^A  \\
    f_{pg}( (l,q_1,\ldots,q_n) ) & = & (f(l),q_1,\ldots,q_n) \\
  \end{array} \]
\end{defn}


\begin{lem}
  If, for product graph $PG = (G,s,P)$ with $G=(V,E)$, if we have the following:

  \[ \begin{array}{ll}
    1. & (a,b) ~\text{is an edge in the concrete topology} \\
    2. & \tilde{m} = a \\
    3. & f_{pg}(m) = M \\
    4. & (M,N) ~ \text{is an edge in the product graph}~ PG^A \\
    5. & \tilde{N} = f(b) \\
  \end{array} \]

  then there exists a node $n$ in the concrete product graph $PG$ where:

  \[ \begin{array}{ll}
    1. & \tilde{n} = b \\
    2. & f_{pg}(n) = N \\
    3. & (m,n) ~ \text{is an edge in the product graph}~ PG \\
    4. & P(n) = P(N) \\
  \end{array} \]

  \begin{proof}

    suppose that $m = (a, q_1, \dots, q_k)$. Then we know that $M = (f(a), q_1, \dots, q_k)$. Also suppose there is some $b$ such that $N = (f(b), s_1, \dots, s_k)$ since $f^{-1}(N) \neq \emptyset$. This means that, since $(a,b)$ is an edge in the concrete topology, so $(f(a),f(b))$ is an edge in the abstract topology. Also we know that $\tilde{N} = f(b)$.

    Let us take the node $n = (b, s_1, \dots, s_k)$. 

    \begin{easylist}
      & Clearly $\tilde{n} = b$
      & Clearly $f_{pg}(n) = (f(b), s_1, \dots, s_k) = N$
      & For each regular expression $\sigma^A(q_i, f(b)) = s_i$. This means that for each regular expression, $\sigma(q_i, b) = s_i$. It follows that $(m,n)$ is an edge in the product graph by definition.
      & Since the final states are the same for each state $q_i$ of each product graph state, it follows that $P(n) = P^A(f(n)) = P^A(N)$.
    \end{easylist}

  \end{proof}
\end{lem}


\begin{thm}
  $m \leq m'$ in the concrete product graph iff $f_{pg}(m) \leq f_{pg}(m')$ in the abstract product graph under the lifted graph homomorphism $f_{pg}$.

  \begin{proof}
    $(\leftarrow)$

    Suppose we have a simulation relation from the subgraphs rooted at nodes $M$ and $M'$ with $M' \geq_{rank} M$ in the abstract product graph. Assume that $\tilde{M} = f(a)$ and $\tilde{N} = f(b)$. For each neighbor $N'$, if we can make a move from $M'$:

    $$M' \overset{\tilde{N'}}{\rightarrow} N'$$

    then we also make a similar move for $M$ for some $N$ where $N \approx N'$ and $N' \geq_{rank} N$:

    $$M \overset{\tilde{N}}{\rightarrow} N$$

    We must show that the same relation holds for $m$ and $m'$. 

    Now assume $m'$ has a neighbor $n'$ where $\tilde{m} = a$ and $\tilde{n} = b$. Then clearly $(a,b)$ is a valid topology edge since it is a transition in the product graph. We now apply the previous lemma with the following facts:

    \[ \begin{array}{ll}
      1. & (a,b) ~\text{is a topology edge} \\
      2. & \tilde{m} = a \\
      3. & f_{pg}(m) = M \\
      4. & (M,N) ~\text{is an edge in}~ PG^A \\
      5. & \tilde{N} = f(b) \\
    \end{array} \]

    This lets us conclude that there exists a node $n'$ such that:

    \[ \begin{array}{ll}
      1. & \tilde{n} = b \\
      2. & f_{pg}(n) = N \\
      3. & (m,n) ~\text{is an edge in}~ PG \\
      4. & P(n) = P(N) \\
    \end{array} \] 

    Thus if we have $m' \overset{b}{\rightarrow} n'$, then we also have $m \overset{b}{\rightarrow} n$. The previous lemma can also be used to show that $P(n') = P(N')$ in a symmetric fashion, so we are guaranteed that $n' \geq_{rank} n$ from the fact that $N' \geq_{rank} N$.

  \end{proof}

  \begin{proof}
    $(\rightarrow)$

    This is the simpler case. We assume we have $m' \overset{b}{\rightarrow} n'$ implies $m \overset{b}{\rightarrow} n$.
    Simply take $N = f_{pg}(n)$ and $N' = f_{pg}(n')$. If we know that $M' \overset{b}{\rightarrow} N'$ then we already know that $M \overset{b}{\rightarrow} N$ from the homomorphism. All that's required is to show that $N' \geq_{rank} N$. This follows trivially from the fact that $P(n) = P(N)$ and $P(n') = P(N')$.
  \end{proof}


\end{thm}



\end{document}
{'fraction_non_alphanumeric': 0.19558805070917534, 'fraction_numerical': 0.011422116229446467, 'mean_word_length': 2.849377944196159, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1185039', 'n_tokens_mistral': 11934, 'n_tokens_neox': 11523, 'n_words': 3149}