<commit_before>\documentclass{report}

\usepackage{hyperref}
\usepackage{color}
\usepackage[usenames]{xcolor}
\usepackage{tikz}
\usepackage{amsmath,amssymb}

\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{stmaryrd}
\newcommand\sem[1]{\llbracket #1\rrbracket}
\newcommand{\pkt}{\ensuremath{pkt}}
\newcommand{\env}{\ensuremath{env}}
\newcommand{\args}{\ensuremath{args}}
\newcommand{\true}{\texttt{true}}
\newcommand{\false}{\texttt{false}}
\newcommand{\ERROR}{\texttt{ERROR}}


\usepackage[letterpaper, left=25mm, right=25mm]{geometry} 

% New definitions
\algnewcommand\algorithmicswitch{\textbf{case}}
\algnewcommand\algorithmiccase{\textbf{}}
% New "environments"
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ {\bf of}}{\algorithmicend\ \algorithmicswitch}%
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1 :}{\algorithmicend\ \algorithmiccase}%
\algtext*{EndSwitch}%
\algtext*{EndCase}%

%\usepackage[T1]{fontenc}

\definecolor{lgray}{gray}{0.9}
\definecolor{lyellow}{cmyk}{0,0,0.3,0}

\usepackage{listings}

\lstnewenvironment{ccnlisting}[1]
{\vspace{3mm}
 \lstset{
    backgroundcolor=\color{lyellow},
    basicstyle=\small\ttfamily, 
%    keywordstyle=\bfseries,
    keywordstyle=\underbar,
    identifierstyle=,
    commentstyle=\slshape,
    stringstyle=,
    showstringspaces=false,
    keywords={ and
             , bool 
             , case
             , default
             , endrefine
             , filter
             , fork
             , function 
             , assume 
             , host 
             , havoc 
             , let 
             , not 
             , or 
             , pkt 
             , refine 
             , role 
             , send 
             , struct 
             , switch
             , case 
             , if 
             , then 
             , else
             , true
             , false
             , uint
             , typedef},
    sensitive=false,
    morecomment=[l]{//},
    morecomment=[s]{(*}{*)},
    numberstyle=\tiny,
    stepnumber=1,
    numbersep=1pt,
    emphstyle=\bfseries,
    belowskip=0pt,
    aboveskip=0pt,
    #1
}}{\vspace{3mm}}

\lstnewenvironment{bnflisting}[1]
{\vspace{3mm}
 \lstset{
    backgroundcolor=\color{lgray},
    basicstyle=\small\ttfamily,
    keywordstyle=\underbar,
    identifierstyle=,
    commentstyle=\slshape,
    stringstyle=,
    showstringspaces=false,
    keywords=,
    sensitive=false,
    morecomment=[l]{//},
    morecomment=[s]{/*}{*/},
    numberstyle=\tiny,
    stepnumber=1,
    numbersep=1pt,
    emphstyle=\bfseries,
    belowskip=0pt,
    aboveskip=0pt,
    #1
}}{\vspace{3mm}}


\newcommand{\src}[1]{\texttt{#1}}

\newcommand{\comment}[1]{{\textit{\textbf{#1}}}}


\title{Cocoon Language Reference}

\begin{document}

\maketitle

\tableofcontents

%The second type of magic blocks are magic blocks with 
%\emph{goals}.  These are needed because not all correctness 
%conditions can be captured using postconditions and assertions.  
%For correctness conditions specified using goals (see 
%Section~\ref{s:o:correctness}), the synthesis algorithm computes a 
%strategy for each goal; however the scheduling of strategies is 
%left to the user, i.e., the user decides when to execute each 
%strategy by assigning goals to magic blocks. \comment{TODO: I 
%still have not figured out the exact meaning of this construct.}

%\section{Constraints on the environment}

\chapter{Syntax reference}\label{s:reference}

\section{Top-level declarations}

A cocoon specification is a sequence of refinements:
\begin{bnflisting}{}
<spec> := <refinement>*
\end{bnflisting}

A refinement declaration starts with a possibly empty list of names of roles that 
are being refined.  These roles must be defined in the body of the refinement.
The body of the refinement consists of type definitions, function declarations,
role declarations, assumptions, and node declarations.
\begin{bnflisting}{}
<refinement> := "refine" [<identifier>(,<identifier>)*] 
                "{"<decl>*"}"

<decl> := <typeDef>
        | <funcDecl>
        | <roleDecl>
        | <assumption>
        | <nodeDecl>
\end{bnflisting}

\subsection*{Example}

\begin{ccnlisting}{}
(* This refinement provides a new implementation of the HostOut role.
   It can also define new roles; however it cannot re-define other 
   previously defined roles that do not appear *)
refine HostOut{ 

    (* Uninterpreted function declaration *)
    function nCoreRedundant(): uint<8>
    
    (* Interpreted function declaration *)
    function iTORPort(TORPortId port): bool = 
        iTOR(port.pod, port.tor) and port.port < nTORPorts()

    (* Assumption *)
    assume (HostPortId hport) 
           iHostPort(hport) => iTORPort(hostSwitchConnection(hport))

    (* Role refined by this refinement *)
    role HostOut[HostId hst, uint<8> port] 
    | iHostPort(HostPortId{hst, port}) = 
        let TORPortId swport = hostSwitchConnection(HostPortId{hst, port});
        send TORIn[swport.pod, swport.tor, swport.port]

    (* New role *)
    role TORIn[uint<8> pod, uint<8> tor, uint<8> port] 
    | iTORPort(TORPortId{pod, tor, port}) = 
        ...
}
\end{ccnlisting}
    


\section{Types}

Type definition introduces a new user-defined type.  This type is visible in all
subsequent refinements.

\begin{bnflisting}{}
<typeDef> := "typedef" <typeSpec> <identifier>
\end{bnflisting}

\begin{bnflisting}{}
<typeSpec> := <arrayType>
            | <uintType>
            | <boolType>
            | <userType>
            | <structType>
\end{bnflisting}

\begin{bnflisting}{}
<uintType>   := "uint" "<" <decimal> ">"
<boolType>   := "bool"
<userType>   := <identifier>
<arrayType>  := "[" <typeSpec> ";" <decimal> "]"
<structType> := "struct" "{" 
                 <field> ("," <field>)*
                "}"
<field> := <typeSpec> <identifier>
\end{bnflisting}

Note:
\begin{itemize}
    \item Every complete cocoon specification must declare \texttt{Packet} type.
        It must match packet headers supported by the target backend.
\end{itemize}

\subsection*{Example}

\begin{ccnlisting}{}
typedef struct {
    uint<48> dstAddr,
    uint<48> srcAddr
} eth_t

typedef uint<12> VLANId

typedef [bool; 3] PIP // array of 3 booleans
\end{ccnlisting}


\section{Functions}

Cocoon functions are pure.  A function can have optional definition.
An undefined function can be defined in a subsequent refinement.  A
defined function cannot be re-defined.

\begin{bnflisting}{}
<funcDecl> := "function" <identifier>"("[<arg>(,<arg>)*]")"
              ":" <typeSpec> // return type
              ["=" <expr>]   // optional function definition
\end{bnflisting}

\begin{bnflisting}{}
<arg> := <typeSpec> <identifier>
\end{bnflisting}

Assumptions have the form $\forall x_1\ldots x_n . e$, 
where $e$ is a boolean-valued expression that only depends on variables $x_i$ and
may contain calls to one or more functions.
When all functions referenced by the assumption become defined, the assumption can be
validated.

\begin{bnflisting}{}
<assumption> = "assume" 
           "("[<arg>(,<arg>)*]")" // universally-quantified vars
           <expr>                 // bolean expression
\end{bnflisting}

\subsection*{Examples}

\begin{ccnlisting}{}
(* Uninterpreted function declaration *)
function vHostLocation(VHostId vhost): HostId

(* Assumption restricting possible values of the uninterpreted function *)
assume (VHostId vhost) iVHost(vhost) => iHost(vHostLocation(vhost))

...

(* Uninterpreted function is defined in one of subsequent refinements *)
function vHostLocation(VHostId vhost): HostId = case {
        vhost == 32'd0 or vhost == 32'd2 or vhost == 32'd4: 48'd0;
        default: 48'd1;
    }
\end{ccnlisting}

\section{Expressions}


\begin{bnflisting}{}
<expr> := <term>
        | "not" <expr>
        | "(" <expr> ")"
        | <expr> "%" <expr>
        | <expr> "+" <expr>
        | <expr> "-" <expr>
        | <expr> ">>" <expr>
        | <expr> "<<" <expr>
        | <expr> "++" <expr>
        | <expr> "==" <expr>
        | <expr> "!=" <expr>
        | <expr> "<" <expr>
        | <expr> "<=" <expr>
        | <expr> ">" <expr>
        | <expr> ">=" <expr>
        | <expr> "and" <expr>
        | <expr> "or" <expr>
        | <expr> "=>" <expr>
        | <expr> "." <identifier> // struct field
        | <expr> "["<decimal> "," <decimal>"]" // bit slice
\end{bnflisting}

\begin{bnflisting}{}
<term> := <structTerm>   // struct given by listing its fields
        | <applyTerm>    // user-defined function call
        | <builtinTerm>  // builtin function call
        | <instanceTerm> // role instance (used in send statements)
        | <intTerm>      // integer constant
        | <boolTerm>     // boolean constant
        | <packetTerm>   // special packet variable
        | <varTerm>      // variable reference: role key or local var
        | <dotvarTerm>   // dot-variable reference
        | <condTerm>     // case split
\end{bnflisting}

\begin{bnflisting}{}
<structTerm>   := <identifier> "{" <expr> (,<expr>)* "}"
<applyTerm>    := <identifier> "(" [<expr> (,<expr>)*] ")"
<builtinTerm>  := <identifier> "!" "(" [<expr> (,<expr>)*] ")"
<instanceTerm> := <identifier> "[" [<expr> (,<expr>)*] "]"
<boolTerm>     := "true" | "false"
<packetTerm>   := "pkt"
<varTerm>      := <identifier>
<dotvarTerm>   := "." <identifier>
<condTerm>     := "case" "{"
                  (<expr> ":" <expr> ";")*
                  "default" ":" <expr> ";"
                  "}"
<intTerm>      := [<width>] "'d" <decimal>
                | [<width>] "'h" <hexadecimal>
                | [<width>] "'o" <octal>
                | [<width>] "'b" <binary>
<width> := <decimal>
\end{bnflisting}

\section{Roles}

\begin{bnflisting}{}
<roleDecl> := "role" <identifier> 
              "["[<arg>(,<arg>)*]"]" // role keys
              ["|" <expr>]    // constraint on role keys
              ["/" <expr>]    // constraint on input packets
              "=" <stat>      // role body
\end{bnflisting}

\subsection*{Example}

\begin{ccnlisting}{}
(* Role with two keys *)
role VSwitchIn[HostId hst, uint<16> vport] | iVSwitchPort(hst, vport) = 
    (* Local variable declaration: binding *)
    let VHPortId from_vhport = vSw2HLink(hst, vport);
    if (iNFVHost(from_vhport.vhost) and (not (pkt.eth.dstAddr == bCastMAC()))) or 
       pkt.eth.srcAddr == vHPort2Mac(from_vhport) then {
        let VNetId vnet = vSwPortVNet(hst, vport);
        if bCastMAC() == pkt.eth.dstAddr then {
            fork(HostId dhst | iHost(dhst) and hHostsVNet(dhst, vnet)) {
                if dhst == hst then {
                    pkt.vlan.vid := 12'd0;
                    fork(VHPortId vhport | iVHostPort(vhport) and 
                                           vHPortVNet(vhport) == vnet and 
                                           vHostLocation(vhport.vhost) == hst and 
                                           vH2SwLink(vhport) != vport and
                                           connection(from_vhport, vhport)) {
                        send VSwitchOut[hst, vH2SwLink(vhport)]
                    }
                } else {
                    pkt.vlan.vid := vnet;
                    send VSwitchTunOut[hst, tunPort(hst, dhst)]
                }
            }
        } else {
            let VHPortId to_vhport = nextHop(pkt.eth, from_vhport);
            if iVHostPort(to_vhport) and connection(from_vhport, to_vhport) then {
                if (vHostLocation(to_vhport.vhost) == hst) then { 
                    (* Local destination -- deliver *)
                    pkt.vlan.vid := 12'd0;
                    pkt.vlan.pcp := 3'd0;
                    send VSwitchOut[hst, vH2SwLink(to_vhport)]
                } else {
                    (* Remote destination -- encapsulate *)
                    pkt.vlan.vid := vnet;
                    pkt.vlan.pcp := label(pkt.eth, from_vhport);
                    send VSwitchTunOut[hst, 
                                       tunPort(hst, 
                                               vHostLocation(to_vhport.vhost))]

                }
            }
        }
    }
\end{ccnlisting}

\section{Statements}

\begin{bnflisting}{}
<stat> := <test> 
        | <ite>
        | <send>
        | <sendNondet>
        | <set>
        | <havoc>
        | <assume>
        | <let>           // local variable declaration
        | <fork>
        | "{" <stat> "}"
        | "(" <stat> ")"
        | <stat> ";" <stat>

<test>       := "filter" <expr>
<sendNondet> := "?" "send" <identifier> "[" <expr> "]"
<send>       := "send" <expr> // expression must return role instance
<set>        := <expr> ":=" <expr>
<ite>        := "if" <expr> "then" <stat> ["else" <stat>]
<havoc>      := "havoc" <expr>
<assume>     := "assume" <expr>
<let>        := "let" <typeSpec> <identifier> "=" <expr>
<fork>       := "fork" "(" <arg> (,<arg>)* "|" <expr> ")" <stat>
\end{bnflisting}

Note:
\begin{itemize}
    \item Only fields of the special \texttt{pkt} variable can be modified 
        with \texttt{:=} or \texttt{havoc}.
    \item Every field can be modified at most once by a role.  Packet fields
        that are not modified by the role keep their input values.        
    \item Local variables are declared and assigned at the same time using 
        \texttt{let}.  Their values never change.
\end{itemize}

\subsection*{Examples}

\begin{ccnlisting}{}
filter false (* drop all packets *)
\end{ccnlisting}

\begin{ccnlisting}{}
filter true (* no-op *)
\end{ccnlisting}

\begin{ccnlisting}{}
(* Role with two keys: as and port *)
role ASSDXIn[ASId as, ASPort port] | iASPort(as, port) = filter false

...

(* Multicast packet to all instances of role ASSDXIn, whose "as" key satisfies the
   condition prefixMatch(.as, pkt.ip4.dst), where .as refers to the as key
   of ASSDXIn, and pkt.ip4.dst is the destination IP of the packet.  *)
?send ASSDXIn[prefixMatch(.as, pkt.ip4.dst)]

(* Unicast to a single instance of ASSDXIn *)
send ASSDXIn[defdst, inboundPolicy(defdst, pkt.ip4)]
\end{ccnlisting}

\begin{ccnlisting}{}
(* Assign the mtag header of the packet *)
pkt.mtag := computeMTag(pod, tor, dstAddr)
\end{ccnlisting}

\section{Nodes}

There are two types of nodes: switches and hosts.  

\begin{bnflisting}{}
<nodeDecl> := ("switch" | "host") <identifier> "(" 
              "(" <identifier> "," <identifier> ")" // list of in/out port pairs
              ("," "(" <identifier> "," <identifier> ")")*
              ")"
\end{bnflisting}

\clearpage
\appendix

\chapter{Cocoon Core Calculus}

\section{Syntax}

\begin{figure}
\[ \begin{array}{lrcl}

\textrm{integers} & n & & \\
\textrm{identifier} & id & & \\
                    & ids & = & id \mid id, ids \\ [6pt]

\textrm{arguments}
                  & args & = & \tau~id \mid \tau~id, args \\
\textrm{port pairs} & ps & = & \texttt{($id$, $id$)} \mid \texttt{($id$, $id$)}, ps \\
\textrm{role constraints} & cs & = & \cdot \mid \texttt{|~$e$} % restrict role parameters
                                     \mid \texttt{/~$e$}       % restrict packets this role accepts
                                     \mid \texttt{|~$e$}~\texttt{/~$e$} \\ [6pt]

\textrm{case body} & cbod & = & \cdot \mid \textrm{$e_1$ : $e_2$; } cbod \\
\textrm{expression} & e & = & \texttt{not}~e \mid e_1 \otimes e_2 \mid e \texttt{.} id \mid e \texttt{[$n$, $n$]} \\
              &   &   &  \mid \texttt{$id$\{$es$\}} \mid \texttt{$id$($es$)} \mid \texttt{$id$!($es$)} \mid \texttt{$id$[$es$]} \\
              &   &   &  \mid \texttt{true} \mid \texttt{false} \mid \texttt{pkt} \mid id \mid \texttt{.$id$} \\
              &   &   &  \mid \texttt{case \{$cbod$; default : $e$ ; \}} \mid \texttt{ [$n$]~'d~n } \\
              & es & = & e \mid e, es \\
\textrm{type specs} & \tau & = & \texttt{uint <} n \texttt{>}
                                 \mid \texttt{bool}
                                 \mid id
                                 \mid \texttt{[} \tau \texttt{;} n \texttt{]}
                                 \mid \texttt{struct \{} \textit{args} \texttt{\}} \\
\textrm{statement} & a & = & \texttt{filter}~e \mid e_3 \texttt{:=} e_2  \\
                   &   &   & \mid \texttt{if $e$ then $a_1$} \mid \texttt{if $e$ then $a_1$ else $a_2$} \\
                   &   &   & \mid \texttt{havoc $e$} \mid \texttt{assume $e$} \mid \texttt{let $\tau$ $id$ = $e$} \\
                   & as & = & f \mid a, as \\
\textrm{final statement} & f & = & \texttt{send $e$} \mid \texttt{?send $id$[$e$]} \mid 
                            \texttt{fork ($args$ | $e$) $as$}\\
\textrm{declaration} & d & = & \texttt{typedef}~\tau~id \\
                     &   &   & \mid \texttt{function}~id \texttt{(} args \texttt{)} : \tau \mid \texttt{function}~id \texttt{(} args \texttt{)} : \tau = e \\
                     &   &   & \mid \texttt{role~$id$\texttt{[}$args$\texttt{]}~$cs$~ = $as$} \\
                     &   &   & \mid \texttt{assume ($args$) $e$} \\ % meaning: \forall args.e
                     &   &   & \mid \texttt{switch $id$ $ps$} \mid \texttt{host $id$ $ps$} \\
                     & ds & = & d \mid d, ds \\
\textrm{refinement} & r & = & \texttt{refine}~ids~ds \\
\textrm{spec} & spec & = & r \mid r, spec \\

\end{array} \]
\caption{Cocoon core calculus.}
\label{fig:core_calc}
\end{figure}

Things that are not implementable:
%
\begin{itemize}

\item \texttt{?send $id$ [$e$]}
\item \texttt{havoc $e$}
\item \texttt{assume $e$}

\end{itemize}

\section{Semantics}
\subsection{Expressions}
$\sem{e}(\pkt,\env, rec) :: value$

An $e$ doesn't seem to introduce any nondeterminism.

$rec$ is recipient, only useful to evaluate $.id$ inside a \texttt{?send}.
Can be \texttt{None} (maybe use an option explicitly?).

To simplify we just write $\sem{e}\pkt,\env$ when we mean $\sem{e}\pkt,\env,{\tt None}$

$\env$ contains local variables (defined with \texttt{let}), functions, function signatures and
roles. Roles kinda act as functions. Maybe we'll need to separate eventually.

\subsection{Statement}
{\sf Pkt} the set of packets \pkt, and {\sf Env} the set of environments \env
\begin{align*}
\sem{a}(\pkt,\env) & :: \mathcal{P}(\mathcal{P}({\sf Pkt}\times{\sf Env})) &
&\text{outer is nondeterminism, inner is different threads}
\\
\sem{\texttt{filter}\ e}(\pkt,\env) & =\{\{(\pkt,\env)\mid\sem{e}(\pkt,\env)=\texttt{true}\}\} &
&\text{could be $\{\emptyset\}$, cannot be $\emptyset$}
\\
\sem{\texttt{assume}\ e}(\pkt,\env) & =\{\{(\pkt,\env)\mid\sem{e}(\pkt,\env)=\texttt{true}\}\} &
& \text{if $\{(\pkt,\env)\mid\sem{e}\pkt,\env=\texttt{true}\}\neq\emptyset$}
\\
\sem{\texttt{assume}\ e}(\pkt,\env) & =\emptyset &
& \text{otherwise}
\\& & & \text{can be $\emptyset$, cannot be a set containing $\emptyset$}
\\
\sem{e_3:=e_2}(\pkt,\env) & =\{\{(\pkt[\sem{e_3}\mapsto\sem{e_2}],\env)\}\} &
&\text{singleton, TODO be more precise on $\sem{e_3}$}
\\
\sem{\texttt{if $e$ then $a_1$}}(\pkt,\env) & = \sem{a_1}(\pkt,\env) & 
&\text{ if $\sem{e}(\pkt,\env)=\true$}
\\
\sem{\texttt{if $e$ then $a_1$}}(\pkt,\env) & = \{\{(\pkt,\env)\}\} &
&\text{ if $\sem{e}(\pkt,\env)=\false$}
\\
\sem{\texttt{if $e$ then $a_1$}}(\pkt,\env) & = \ERROR &
&\text{ otherwise}
\\
\sem{\texttt{if $e$ then $a_1$ else $a_2$}}(\pkt,\env) & = \sem{a_1}(\pkt,\env) &
&\text{ if $\sem{e}(\pkt,\env)=\true$}
\\
\sem{\texttt{if $e$ then $a_1$ else $a_2$}}(\pkt,\env) & = \sem{a_2}(\pkt,\env) &
&\text{ if $\sem{e}(\pkt,\env)=\false$}
\\
\sem{\texttt{if $e$ then $a_1$ else $a_2$}}(\pkt,\env) & = \ERROR &
&\text{ otherwise}
\\
\sem{\texttt{havoc } e}(\pkt,\env) & =\{\{(\pkt[\sem{e}\mapsto v],\env)\}\mid\text{$v$ any value}\} & &
\text{Constrain $v$ of being the right type? Usually bad idea to mix typing and semantics.}\\
&&&\text{TODO be more precise on $\sem{e}$}
\\
\sem{\texttt{let}\ id=e}(\pkt,\env) & =\{\{(\pkt,\env[id\mapsto\sem{e}])\}\} &
& \text{if $id\not\in{\sf dom}(\env)$ ($\env$ is extended)}
\\
\sem{\texttt{let}\ id=e}(\pkt,\env) & =\ERROR &
& \text{otherwise}
\end{align*}

\subsection{Final statement}
\begin{align*} 
\sem{f}(\pkt,\env) & :: \mathcal{P}(\mathcal{P}({\sf Pkt}\times{\sf Env})) &
&\text{outer is nondeterminism, inner is different threads}
\\
\sem{\texttt{send }e}(\pkt,\env) & =\sem{e}(\pkt,\textsf{strip}(\env)) &
& \text{(role seen as a function)}
\\&&& \text{$env$ should be stripped of all \textrm{let}-defined variables}
\\
\texttt{?send }id[e] & \equiv
\texttt{let }args=\texttt{havoc};\\
&\quad\ \texttt{assume }e;\ \texttt{send }id[args];&
& \text{Syntactic sugar}
\\
\sem{\texttt{?send }id[e]}(\pkt,\env) & \simeq\bigcup\left(\sem{id[args]}(\pkt,\env)\mid\sem{e}(\pkt,\env[,args])=\true\right) &
& \text{kind of, except for the calls \texttt{.id}}
\\
\sem{\texttt{fork } (args\mid e)\ as} & =\rlap{$\displaystyle\bigotimes\left(\sem{as}(\pkt,\env[args\mapsto vals])\mid\sem{e}(\pkt,\env[args\mapsto vals])=\texttt{true}\right), vals\text{ any value}$}
\\
\text{where } & \rlap{$\displaystyle\bigotimes\{A_1,\ldots,A_n\}=\{a_1\cup\ldots\cup a_n\mid a_1\in A_1,\ldots,a_n\in A_n\}, a_i\in\mathcal P(\pkt,\env), A_i\in\mathcal P(\mathcal P(\pkt,\env))$}
\end{align*}

\paragraph{Remark} 
$\texttt{fork }(a_1,\ldots,a_n\mid e)\ as\equiv
\texttt{fork }(a_1\mid\true)\ (\texttt{fork } (a_2\mid\true)\ (\ldots\ (\texttt{fork }(a_n\mid e)\ as)\ldots))$

\paragraph{Remark} Sending is like calling a function, the function being the role we are sending to.

\paragraph{Remark} But does the environment set up by the let carry over? No, hence the strip.

\paragraph{Remark} Do we want the semantics to keep the trace of the nodes the packet has been through?
No.<commit_msg>cleaning up semantics<commit_after>\documentclass{report}

\usepackage{hyperref}
\usepackage{color}
\usepackage[usenames]{xcolor}
\usepackage{tikz}
\usepackage{amsmath,amssymb}

\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{stmaryrd}
\newcommand\sem[1]{\llbracket #1\rrbracket}
\newcommand{\pkt}{\ensuremath{pkt}}
\newcommand{\env}{\ensuremath{env}}
\newcommand{\args}{\ensuremath{args}}
\newcommand{\true}{\texttt{true}}
\newcommand{\false}{\texttt{false}}
\newcommand{\ERROR}{\texttt{ERROR}}


\usepackage[letterpaper, left=25mm, right=25mm]{geometry} 

% New definitions
\algnewcommand\algorithmicswitch{\textbf{case}}
\algnewcommand\algorithmiccase{\textbf{}}
% New "environments"
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ {\bf of}}{\algorithmicend\ \algorithmicswitch}%
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1 :}{\algorithmicend\ \algorithmiccase}%
\algtext*{EndSwitch}%
\algtext*{EndCase}%

%\usepackage[T1]{fontenc}

\definecolor{lgray}{gray}{0.9}
\definecolor{lyellow}{cmyk}{0,0,0.3,0}

\usepackage{listings}

\lstnewenvironment{ccnlisting}[1]
{\vspace{3mm}
 \lstset{
    backgroundcolor=\color{lyellow},
    basicstyle=\small\ttfamily, 
%    keywordstyle=\bfseries,
    keywordstyle=\underbar,
    identifierstyle=,
    commentstyle=\slshape,
    stringstyle=,
    showstringspaces=false,
    keywords={ and
             , bool 
             , case
             , default
             , endrefine
             , filter
             , fork
             , function 
             , assume 
             , host 
             , havoc 
             , let 
             , not 
             , or 
             , pkt 
             , refine 
             , role 
             , send 
             , struct 
             , switch
             , case 
             , if 
             , then 
             , else
             , true
             , false
             , uint
             , typedef},
    sensitive=false,
    morecomment=[l]{//},
    morecomment=[s]{(*}{*)},
    numberstyle=\tiny,
    stepnumber=1,
    numbersep=1pt,
    emphstyle=\bfseries,
    belowskip=0pt,
    aboveskip=0pt,
    #1
}}{\vspace{3mm}}

\lstnewenvironment{bnflisting}[1]
{\vspace{3mm}
 \lstset{
    backgroundcolor=\color{lgray},
    basicstyle=\small\ttfamily,
    keywordstyle=\underbar,
    identifierstyle=,
    commentstyle=\slshape,
    stringstyle=,
    showstringspaces=false,
    keywords=,
    sensitive=false,
    morecomment=[l]{//},
    morecomment=[s]{/*}{*/},
    numberstyle=\tiny,
    stepnumber=1,
    numbersep=1pt,
    emphstyle=\bfseries,
    belowskip=0pt,
    aboveskip=0pt,
    #1
}}{\vspace{3mm}}


\newcommand{\src}[1]{\texttt{#1}}

\newcommand{\comment}[1]{{\textit{\textbf{#1}}}}


\title{Cocoon Language Reference}

\begin{document}

\maketitle

\tableofcontents

%The second type of magic blocks are magic blocks with 
%\emph{goals}.  These are needed because not all correctness 
%conditions can be captured using postconditions and assertions.  
%For correctness conditions specified using goals (see 
%Section~\ref{s:o:correctness}), the synthesis algorithm computes a 
%strategy for each goal; however the scheduling of strategies is 
%left to the user, i.e., the user decides when to execute each 
%strategy by assigning goals to magic blocks. \comment{TODO: I 
%still have not figured out the exact meaning of this construct.}

%\section{Constraints on the environment}

\chapter{Syntax reference}\label{s:reference}

\section{Top-level declarations}

A cocoon specification is a sequence of refinements:
\begin{bnflisting}{}
<spec> := <refinement>*
\end{bnflisting}

A refinement declaration starts with a possibly empty list of names of roles that 
are being refined.  These roles must be defined in the body of the refinement.
The body of the refinement consists of type definitions, function declarations,
role declarations, assumptions, and node declarations.
\begin{bnflisting}{}
<refinement> := "refine" [<identifier>(,<identifier>)*] 
                "{"<decl>*"}"

<decl> := <typeDef>
        | <funcDecl>
        | <roleDecl>
        | <assumption>
        | <nodeDecl>
\end{bnflisting}

\subsection*{Example}

\begin{ccnlisting}{}
(* This refinement provides a new implementation of the HostOut role.
   It can also define new roles; however it cannot re-define other 
   previously defined roles that do not appear *)
refine HostOut{ 

    (* Uninterpreted function declaration *)
    function nCoreRedundant(): uint<8>
    
    (* Interpreted function declaration *)
    function iTORPort(TORPortId port): bool = 
        iTOR(port.pod, port.tor) and port.port < nTORPorts()

    (* Assumption *)
    assume (HostPortId hport) 
           iHostPort(hport) => iTORPort(hostSwitchConnection(hport))

    (* Role refined by this refinement *)
    role HostOut[HostId hst, uint<8> port] 
    | iHostPort(HostPortId{hst, port}) = 
        let TORPortId swport = hostSwitchConnection(HostPortId{hst, port});
        send TORIn[swport.pod, swport.tor, swport.port]

    (* New role *)
    role TORIn[uint<8> pod, uint<8> tor, uint<8> port] 
    | iTORPort(TORPortId{pod, tor, port}) = 
        ...
}
\end{ccnlisting}
    


\section{Types}

Type definition introduces a new user-defined type.  This type is visible in all
subsequent refinements.

\begin{bnflisting}{}
<typeDef> := "typedef" <typeSpec> <identifier>
\end{bnflisting}

\begin{bnflisting}{}
<typeSpec> := <arrayType>
            | <uintType>
            | <boolType>
            | <userType>
            | <structType>
\end{bnflisting}

\begin{bnflisting}{}
<uintType>   := "uint" "<" <decimal> ">"
<boolType>   := "bool"
<userType>   := <identifier>
<arrayType>  := "[" <typeSpec> ";" <decimal> "]"
<structType> := "struct" "{" 
                 <field> ("," <field>)*
                "}"
<field> := <typeSpec> <identifier>
\end{bnflisting}

Note:
\begin{itemize}
    \item Every complete cocoon specification must declare \texttt{Packet} type.
        It must match packet headers supported by the target backend.
\end{itemize}

\subsection*{Example}

\begin{ccnlisting}{}
typedef struct {
    uint<48> dstAddr,
    uint<48> srcAddr
} eth_t

typedef uint<12> VLANId

typedef [bool; 3] PIP // array of 3 booleans
\end{ccnlisting}


\section{Functions}

Cocoon functions are pure.  A function can have optional definition.
An undefined function can be defined in a subsequent refinement.  A
defined function cannot be re-defined.

\begin{bnflisting}{}
<funcDecl> := "function" <identifier>"("[<arg>(,<arg>)*]")"
              ":" <typeSpec> // return type
              ["=" <expr>]   // optional function definition
\end{bnflisting}

\begin{bnflisting}{}
<arg> := <typeSpec> <identifier>
\end{bnflisting}

Assumptions have the form $\forall x_1\ldots x_n . e$, 
where $e$ is a boolean-valued expression that only depends on variables $x_i$ and
may contain calls to one or more functions.
When all functions referenced by the assumption become defined, the assumption can be
validated.

\begin{bnflisting}{}
<assumption> = "assume" 
           "("[<arg>(,<arg>)*]")" // universally-quantified vars
           <expr>                 // bolean expression
\end{bnflisting}

\subsection*{Examples}

\begin{ccnlisting}{}
(* Uninterpreted function declaration *)
function vHostLocation(VHostId vhost): HostId

(* Assumption restricting possible values of the uninterpreted function *)
assume (VHostId vhost) iVHost(vhost) => iHost(vHostLocation(vhost))

...

(* Uninterpreted function is defined in one of subsequent refinements *)
function vHostLocation(VHostId vhost): HostId = case {
        vhost == 32'd0 or vhost == 32'd2 or vhost == 32'd4: 48'd0;
        default: 48'd1;
    }
\end{ccnlisting}

\section{Expressions}


\begin{bnflisting}{}
<expr> := <term>
        | "not" <expr>
        | "(" <expr> ")"
        | <expr> "%" <expr>
        | <expr> "+" <expr>
        | <expr> "-" <expr>
        | <expr> ">>" <expr>
        | <expr> "<<" <expr>
        | <expr> "++" <expr>
        | <expr> "==" <expr>
        | <expr> "!=" <expr>
        | <expr> "<" <expr>
        | <expr> "<=" <expr>
        | <expr> ">" <expr>
        | <expr> ">=" <expr>
        | <expr> "and" <expr>
        | <expr> "or" <expr>
        | <expr> "=>" <expr>
        | <expr> "." <identifier> // struct field
        | <expr> "["<decimal> "," <decimal>"]" // bit slice
\end{bnflisting}

\begin{bnflisting}{}
<term> := <structTerm>   // struct given by listing its fields
        | <applyTerm>    // user-defined function call
        | <builtinTerm>  // builtin function call
        | <instanceTerm> // role instance (used in send statements)
        | <intTerm>      // integer constant
        | <boolTerm>     // boolean constant
        | <packetTerm>   // special packet variable
        | <varTerm>      // variable reference: role key or local var
        | <dotvarTerm>   // dot-variable reference
        | <condTerm>     // case split
\end{bnflisting}

\begin{bnflisting}{}
<structTerm>   := <identifier> "{" <expr> (,<expr>)* "}"
<applyTerm>    := <identifier> "(" [<expr> (,<expr>)*] ")"
<builtinTerm>  := <identifier> "!" "(" [<expr> (,<expr>)*] ")"
<instanceTerm> := <identifier> "[" [<expr> (,<expr>)*] "]"
<boolTerm>     := "true" | "false"
<packetTerm>   := "pkt"
<varTerm>      := <identifier>
<dotvarTerm>   := "." <identifier>
<condTerm>     := "case" "{"
                  (<expr> ":" <expr> ";")*
                  "default" ":" <expr> ";"
                  "}"
<intTerm>      := [<width>] "'d" <decimal>
                | [<width>] "'h" <hexadecimal>
                | [<width>] "'o" <octal>
                | [<width>] "'b" <binary>
<width> := <decimal>
\end{bnflisting}

\section{Roles}

\begin{bnflisting}{}
<roleDecl> := "role" <identifier> 
              "["[<arg>(,<arg>)*]"]" // role keys
              ["|" <expr>]    // constraint on role keys
              ["/" <expr>]    // constraint on input packets
              "=" <stat>      // role body
\end{bnflisting}

\subsection*{Example}

\begin{ccnlisting}{}
(* Role with two keys *)
role VSwitchIn[HostId hst, uint<16> vport] | iVSwitchPort(hst, vport) = 
    (* Local variable declaration: binding *)
    let VHPortId from_vhport = vSw2HLink(hst, vport);
    if (iNFVHost(from_vhport.vhost) and (not (pkt.eth.dstAddr == bCastMAC()))) or 
       pkt.eth.srcAddr == vHPort2Mac(from_vhport) then {
        let VNetId vnet = vSwPortVNet(hst, vport);
        if bCastMAC() == pkt.eth.dstAddr then {
            fork(HostId dhst | iHost(dhst) and hHostsVNet(dhst, vnet)) {
                if dhst == hst then {
                    pkt.vlan.vid := 12'd0;
                    fork(VHPortId vhport | iVHostPort(vhport) and 
                                           vHPortVNet(vhport) == vnet and 
                                           vHostLocation(vhport.vhost) == hst and 
                                           vH2SwLink(vhport) != vport and
                                           connection(from_vhport, vhport)) {
                        send VSwitchOut[hst, vH2SwLink(vhport)]
                    }
                } else {
                    pkt.vlan.vid := vnet;
                    send VSwitchTunOut[hst, tunPort(hst, dhst)]
                }
            }
        } else {
            let VHPortId to_vhport = nextHop(pkt.eth, from_vhport);
            if iVHostPort(to_vhport) and connection(from_vhport, to_vhport) then {
                if (vHostLocation(to_vhport.vhost) == hst) then { 
                    (* Local destination -- deliver *)
                    pkt.vlan.vid := 12'd0;
                    pkt.vlan.pcp := 3'd0;
                    send VSwitchOut[hst, vH2SwLink(to_vhport)]
                } else {
                    (* Remote destination -- encapsulate *)
                    pkt.vlan.vid := vnet;
                    pkt.vlan.pcp := label(pkt.eth, from_vhport);
                    send VSwitchTunOut[hst, 
                                       tunPort(hst, 
                                               vHostLocation(to_vhport.vhost))]

                }
            }
        }
    }
\end{ccnlisting}

\section{Statements}

\begin{bnflisting}{}
<stat> := <test> 
        | <ite>
        | <send>
        | <sendNondet>
        | <set>
        | <havoc>
        | <assume>
        | <let>           // local variable declaration
        | <fork>
        | "{" <stat> "}"
        | "(" <stat> ")"
        | <stat> ";" <stat>

<test>       := "filter" <expr>
<sendNondet> := "?" "send" <identifier> "[" <expr> "]"
<send>       := "send" <expr> // expression must return role instance
<set>        := <expr> ":=" <expr>
<ite>        := "if" <expr> "then" <stat> ["else" <stat>]
<havoc>      := "havoc" <expr>
<assume>     := "assume" <expr>
<let>        := "let" <typeSpec> <identifier> "=" <expr>
<fork>       := "fork" "(" <arg> (,<arg>)* "|" <expr> ")" <stat>
\end{bnflisting}

Note:
\begin{itemize}
    \item Only fields of the special \texttt{pkt} variable can be modified 
        with \texttt{:=} or \texttt{havoc}.
    \item Every field can be modified at most once by a role.  Packet fields
        that are not modified by the role keep their input values.        
    \item Local variables are declared and assigned at the same time using 
        \texttt{let}.  Their values never change.
\end{itemize}

\subsection*{Examples}

\begin{ccnlisting}{}
filter false (* drop all packets *)
\end{ccnlisting}

\begin{ccnlisting}{}
filter true (* no-op *)
\end{ccnlisting}

\begin{ccnlisting}{}
(* Role with two keys: as and port *)
role ASSDXIn[ASId as, ASPort port] | iASPort(as, port) = filter false

...

(* Multicast packet to all instances of role ASSDXIn, whose "as" key satisfies the
   condition prefixMatch(.as, pkt.ip4.dst), where .as refers to the as key
   of ASSDXIn, and pkt.ip4.dst is the destination IP of the packet.  *)
?send ASSDXIn[prefixMatch(.as, pkt.ip4.dst)]

(* Unicast to a single instance of ASSDXIn *)
send ASSDXIn[defdst, inboundPolicy(defdst, pkt.ip4)]
\end{ccnlisting}

\begin{ccnlisting}{}
(* Assign the mtag header of the packet *)
pkt.mtag := computeMTag(pod, tor, dstAddr)
\end{ccnlisting}

\section{Nodes}

There are two types of nodes: switches and hosts.  

\begin{bnflisting}{}
<nodeDecl> := ("switch" | "host") <identifier> "(" 
              "(" <identifier> "," <identifier> ")" // list of in/out port pairs
              ("," "(" <identifier> "," <identifier> ")")*
              ")"
\end{bnflisting}

\clearpage
\appendix

\chapter{Cocoon Core Calculus}

\section{Syntax}

\begin{figure}
\[ \begin{array}{lrcl}

\textrm{integers} & n & & \\
\textrm{identifier} & id & & \\
                    & ids & = & id \mid id, ids \\ [6pt]

\textrm{arguments}
                  & args & = & \tau~id \mid \tau~id, args \\
\textrm{port pairs} & ps & = & \texttt{($id$, $id$)} \mid \texttt{($id$, $id$)}, ps \\
\textrm{role constraints} & cs & = & \cdot \mid \texttt{|~$e$} % restrict role parameters
                                     \mid \texttt{/~$e$}       % restrict packets this role accepts
                                     \mid \texttt{|~$e$}~\texttt{/~$e$} \\ [6pt]

\textrm{case body} & cbod & = & \cdot \mid \textrm{$e_1$ : $e_2$; } cbod \\
\textrm{expression} & e & = & \texttt{not}~e \mid e_1 \otimes e_2 \mid e \texttt{.} id \mid e \texttt{[$n$, $n$]} \\
              &   &   &  \mid \texttt{$id$\{$es$\}} \mid \texttt{$id$($es$)} \mid \texttt{$id$!($es$)} \mid \texttt{$id$[$es$]} \\
              &   &   &  \mid \texttt{true} \mid \texttt{false} \mid \texttt{pkt} \mid id \mid \texttt{.$id$} \\
              &   &   &  \mid \texttt{case \{$cbod$; default : $e$ ; \}} \mid \texttt{ [$n$]~'d~n } \\
              & es & = & e \mid e, es \\
\textrm{type specs} & \tau & = & \texttt{uint <} n \texttt{>}
                                 \mid \texttt{bool}
                                 \mid id
                                 \mid \texttt{[} \tau \texttt{;} n \texttt{]}
                                 \mid \texttt{struct \{} \textit{args} \texttt{\}} \\
\textrm{statement} & a & = & \texttt{filter}~e \mid e_3 \texttt{:=} e_2  \\
                   &   &   & \mid \texttt{if $e$ then $a_1$} \mid \texttt{if $e$ then $a_1$ else $a_2$} \\
                   &   &   & \mid \texttt{havoc $e$} \mid \texttt{assume $e$} \mid \texttt{let $\tau$ $id$ = $e$} \\
                   & as & = & f \mid a, as \\
\textrm{final statement} & f & = & \texttt{send $e$} \mid \texttt{?send $id$[$e$]} \mid 
                            \texttt{fork ($args$ | $e$) $as$}\\
\textrm{declaration} & d & = & \texttt{typedef}~\tau~id \\
                     &   &   & \mid \texttt{function}~id \texttt{(} args \texttt{)} : \tau \mid \texttt{function}~id \texttt{(} args \texttt{)} : \tau = e \\
                     &   &   & \mid \texttt{role~$id$\texttt{[}$args$\texttt{]}~$cs$~ = $as$} \\
                     &   &   & \mid \texttt{assume ($args$) $e$} \\ % meaning: \forall args.e
                     &   &   & \mid \texttt{switch $id$ $ps$} \mid \texttt{host $id$ $ps$} \\
                     & ds & = & d \mid d, ds \\
\textrm{refinement} & r & = & \texttt{refine}~ids~ds \\
\textrm{spec} & spec & = & r \mid r, spec \\

\end{array} \]
\caption{Cocoon core calculus.}
\label{fig:core_calc}
\end{figure}

Things that are not implementable:
%
\begin{itemize}

\item \texttt{?send $id$ [$e$]}
\item \texttt{havoc $e$}
\item \texttt{assume $e$}

\end{itemize}

\section{Semantics}
\subsection{Expressions}
$\sem{e}(\pkt,\env, rec) :: value$

An $e$ doesn't seem to introduce any nondeterminism.

$rec$ is recipient, only useful to evaluate $.id$ inside a \texttt{?send}.
Can be \texttt{None} (maybe use an option explicitly?).

To simplify we just write $\sem{e}\pkt,\env$ when we mean $\sem{e}\pkt,\env,{\tt None}$

$\env$ contains local variables (defined with \texttt{let}), functions, function signatures and
roles. Roles kinda act as functions. Maybe we'll need to separate eventually.

\subsection{Statement}
{\sf Pkt} the set of packets all \pkt, and {\sf Env} the set of environments all \env
\begin{align*}
\sem{a}(\pkt,\env) & :: \mathcal{P}(\mathcal{P}({\sf Pkt}\times{\sf Env})) &
&\text{outer is nondeterminism, inner is different threads}
\\
\sem{\texttt{filter}\ e}(\pkt,\env) & =\{\{(\pkt,\env)\mid\sem{e}(\pkt,\env)=\texttt{true}\}\} &
&\text{could be $\{\emptyset\}$, cannot be $\emptyset$}
\\
\sem{\texttt{assume}\ e}(\pkt,\env) & =\{\{(\pkt,\env)\mid\sem{e}(\pkt,\env)=\texttt{true}\}\} &
& \text{if $\{(\pkt,\env)\mid\sem{e}\pkt,\env=\texttt{true}\}\neq\emptyset$}
\\
\sem{\texttt{assume}\ e}(\pkt,\env) & =\emptyset &
& \text{otherwise}
\\& & & \text{can be $\emptyset$, cannot be a set containing $\emptyset$}
\\
\sem{e_3:=e_2}(\pkt,\env) & =\{\{(\pkt[\sem{e_3}\mapsto\sem{e_2}],\env)\}\} &
&\text{singleton, TODO be more precise on $\sem{e_3}$}
\\
\sem{\texttt{if $e$ then $a_1$}}(\pkt,\env) & = \sem{a_1}(\pkt,\env) & 
&\text{ if $\sem{e}(\pkt,\env)=\true$}
\\
\sem{\texttt{if $e$ then $a_1$}}(\pkt,\env) & = \{\{(\pkt,\env)\}\} &
&\text{ if $\sem{e}(\pkt,\env)=\false$}
\\
\sem{\texttt{if $e$ then $a_1$}}(\pkt,\env) & = \ERROR = \emptyset&
&\text{ otherwise}
\\
\sem{\texttt{if $e$ then $a_1$ else $a_2$}}(\pkt,\env) & = \sem{a_1}(\pkt,\env) &
&\text{ if $\sem{e}(\pkt,\env)=\true$}
\\
\sem{\texttt{if $e$ then $a_1$ else $a_2$}}(\pkt,\env) & = \sem{a_2}(\pkt,\env) &
&\text{ if $\sem{e}(\pkt,\env)=\false$}
\\
\sem{\texttt{if $e$ then $a_1$ else $a_2$}}(\pkt,\env) & = \ERROR=\emptyset &
&\text{ otherwise}
\\
\sem{\texttt{havoc } e}(\pkt,\env) & =\{\{(\pkt[\sem{e}\mapsto v],\env)\}\mid\text{$v$ any value}\} & &
\text{Constrain $v$ of being the right type? Usually bad idea to mix typing and semantics.}\\
&&&\text{TODO be more precise on $\sem{e}$}
\\
\sem{\texttt{let}\ id=e}(\pkt,\env) & =\{\{(\pkt,\env[id\mapsto\sem{e}])\}\} &
& \text{if $id\not\in{\sf dom}(\env)$ ($\env$ is extended)}
\\
\sem{\texttt{let}\ id=e}(\pkt,\env) & =\ERROR &
& \text{otherwise}
\\
\end{align*}

\subsection{Final statement}
\begin{align*} 
\sem{f}(\pkt,\env) & :: \mathcal{P}(\mathcal{P}({\sf Pkt}\times{\sf Env})) &
&\text{outer is nondeterminism, inner is different threads}
\\
\sem{\texttt{send }e}(\pkt,\env) & =\sem{id[es]}(\pkt,\textsf{strip}(\env))
\text{ if }\sem{e}(\pkt,\env)=id[es] &
& \text{(role seen as a function)}
\\& = \sem{\sem{e}(\pkt,\env)}(\pkt,\textsf{strip}(\env))
&& \text{$env$ should be stripped of all \textrm{let}-defined variables}
\\
\texttt{?send }id[e] & \equiv
\texttt{let }args=\texttt{havoc};\\
&\quad\ \texttt{assume }e;\ \texttt{send }id[args];&
& \text{Syntactic sugar}
\\
\sem{\texttt{?send }id[e]}(\pkt,\env) & \simeq\bigcup\left(\sem{id[args]}(\pkt,\env)\mid\sem{e}(\pkt,\env[,args])=\true\right) &
& \text{kind of, except for the calls \texttt{.id}}
\\
\sem{\texttt{fork } (args\mid e)\ as} & =\rlap{$\displaystyle\bigotimes\left(\sem{as}(\pkt,\env[args\mapsto vals])\mid\sem{e}(\pkt,\env[args\mapsto vals])=\texttt{true}\right), vals\text{ any value}$}
\\
\text{where } & \rlap{$\displaystyle\bigotimes\{A_1,\ldots,A_n\}=\{a_1\cup\ldots\cup a_n\mid a_1\in A_1,\ldots,a_n\in A_n\}, a_i\in\mathcal P({\sf Pkt}\times{\sf Env}), A_i\in\mathcal P(\mathcal P({\sf Pkt}\times{\sf Env}))$}
\\
\sem{a,as}(\pkt,\env) & = \bigcup\left((\sem{as}(\pkt',\env') \mid (\pkt',\env')\right)
\end{align*}

\paragraph{Remark} 
$\texttt{fork }(a_1,\ldots,a_n\mid e)\ as\equiv
\texttt{fork }(a_1\mid\true)\ (\texttt{fork } (a_2\mid\true)\ (\ldots\ (\texttt{fork }(a_n\mid e)\ as)\ldots))$

\paragraph{Remark} Sending is like calling a function, the function being the role we are sending to.

\paragraph{Remark} But does the environment set up by the let carry over? No, hence the strip.

\paragraph{Remark} Do we want the semantics to keep the trace of the nodes the packet has been through?
No.
{'fraction_non_alphanumeric': 0.1824445775913721, 'fraction_numerical': 0.005576807853620316, 'mean_word_length': 2.493680057966347, 'pattern_counts': {'":': 8, '<': 413, '<?xml version=': 0, '>': 417, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 38, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1360537', 'n_tokens_mistral': 15107, 'n_tokens_neox': 14557, 'n_words': 3502}