diff options
Diffstat (limited to 'chapters/core')
| -rw-r--r-- | chapters/core/01-implementation.tex | 4 | ||||
| -rw-r--r-- | chapters/core/02-soundness-proof.tex | 5 | ||||
| -rw-r--r-- | chapters/core/implementation/01-inpla.tex | 53 | ||||
| -rw-r--r-- | chapters/core/implementation/02-interaction-rules.tex | 43 | ||||
| -rw-r--r-- | chapters/core/implementation/03-translation.tex | 142 | ||||
| -rw-r--r-- | chapters/core/implementation/04-python-module.tex | 34 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/01-mathematical-definitions.tex | 34 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/02-soundness-of-translation.tex | 52 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex | 505 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/04-soundness-of-reduction.tex | 26 |
10 files changed, 870 insertions, 28 deletions
diff --git a/chapters/core/01-implementation.tex b/chapters/core/01-implementation.tex index fcb1345..3e8fa20 100644 --- a/chapters/core/01-implementation.tex +++ b/chapters/core/01-implementation.tex @@ -1,7 +1,9 @@ \section{Implementation} \label{sec:implementation} -% This sections contain the implementation sections +This sections contains details on the implementation of the reduction engine (\textbf{\Cref{sec:inpla}}), +the interaction rules designed (\textbf{\Cref{sec:interaction-rules}}), the algorithm used in the +ONNX-to-IN translation (\textbf{\Cref{sec:translation}}) and the Python module (\textbf{\Cref{sec:python-module}}). \input{chapters/core/implementation/01-inpla} diff --git a/chapters/core/02-soundness-proof.tex b/chapters/core/02-soundness-proof.tex index c353946..6b014da 100644 --- a/chapters/core/02-soundness-proof.tex +++ b/chapters/core/02-soundness-proof.tex @@ -1,7 +1,10 @@ \section{Soundness Proof} \label{sec:soundness-proof} -% This section contains the proof that my tool is sound +This section contains proof of soundness of the VEIN framework, which is organized in mathematical +definitions (\textbf{\Cref{sec:mathematical-definitions}}), proof of the translation layer (\textbf{\Cref{sec:soundness-of-translation}}), +proof of the interaction rules (\textbf{\Cref{sec:soundness-of-interaction-rules}}) and the final +induction proof (\textbf{\Cref{sec:soundness-of-reduction}}). \input{chapters/core/soundness-proof/01-mathematical-definitions} diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex index b534705..5b2eab9 100644 --- a/chapters/core/implementation/01-inpla.tex +++ b/chapters/core/implementation/01-inpla.tex @@ -1,4 +1,55 @@ \subsection{Inpla fork} \label{sec:inpla} -% This subsection talks about my Inpla fork +The VEIN reduction engine utilizes a modified version of INPLA\footnote{\textbf{\href{https://github.com/inpla/inpla/blob/main/Gentle_introduction_Inpla.md}{INPLA documentation.}}}, +a multi-threaded parallel interpreter of IN. Performance and ease of use motivated the choice of +INPLA. Additionally, it supports attribute values, which is a special extension that allows agents +to hold numerical values at their ports. + +Several modifications adapt INPLA to the pipeline of the framework: +\begin{itemize} + \item \textbf{Floating-Point arithmetic}: attributes were limited to integer values. To correctly + represent the computation performed by neural networks, the fork replaces the internal numerical + representation by floating-point types. + \item \textbf{Pipeline integration}: INPLA was designed for interactive use through the command line, so + various debugging and informational messages are printed along the actual output. To integrate + INPLA in our automated framework, the fork introduces a suppression flag to prevent unnecessary + printing from disrupting its execution. +\end{itemize} + +\paragraph{INPLA syntax} +INPLA evaluates nets, they consist of connections between terms. Terms are built on names and agents: +\begin{verbatim} +<term> ::= <name> | <agent> +<name> ::= <nameID> +<agent> ::= <agentID> + | <agentID> ['(' <term> ',' ... ',' <term> ')'] +\end{verbatim} +\begin{itemize} + \item \textbf{Name}: it works as a buffer between terms. + \item \textbf{Agent}: it works as a constructor and de-constructor (defined functions). +\end{itemize} +A connection is a relation between two terms and the symbol \texttt{\~} expresses this relation. +Interaction rules rewrite connections between agents: +\begin{verbatim} +<interaction-rule> ::= <rule-agent> '><' <rule-agent> '=>' <connections> ';' +<rule-agent> ::= <agentID> + | <agentID> '(' <name> ',' ... ',' <name> ')' +\end{verbatim} + +\paragraph{Example} +Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successive function). For +instance, 0, 1, 2, 3 are expressed as \texttt{Z}, \texttt{S(Z)}, \texttt{S(S(Z))}, \texttt{S(S(S(Z)))}. Here, let's think about an +increment operation "inc" such that: +\begin{verbatim} +inc(n) = S(n). +\end{verbatim} +This is written as the following rules: +\begin{verbatim} +inc(r) >< Z => r ~ S(Z); +inc(r) >< S(x) => r ~ S(S(x)); +\end{verbatim} +Then, the result of \texttt{inc(r) \~{} S(S(Z))} is: +\begin{verbatim} +r ~ S(S(S(Z))); +\end{verbatim} diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex index 84dc27b..b657ee9 100644 --- a/chapters/core/implementation/02-interaction-rules.tex +++ b/chapters/core/implementation/02-interaction-rules.tex @@ -1,9 +1,7 @@ \subsection{Interaction Rules} \label{sec:interaction-rules} -This subsection contains the definition of the agents and the interaction rules that implement the symbolic simplification. - -The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into three groups: +The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into four groups: \begin{itemize} \item \textbf{Carriers}: Agents that contain float attributes. @@ -30,12 +28,12 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into t \item \textbf{Materialize}: Converts a Linear agent into an explicit representation for the SMT solver. \end{itemize} \item - \textbf{Inerts}: Agents that will compose the normal form. + \textbf{Inerts}: Agents that compose the normal form. \begin{itemize} - \item \textbf{TermAdd}: This agent that will be parsed as addition for the SMT solver. - \item \textbf{TermMul}: This agent that will be parsed as multiplication for the SMT solver. - \item \textbf{TermReLU}: This agent that will be parsed as rectified linear unit for the SMT solver. - \item \textbf{Symbolic}: This agent that will be parsed as specific variable for the SMT solver. + \item \textbf{TermAdd}: This agent is parsed as addition for the SMT solver. + \item \textbf{TermMul}: This agent is parsed as multiplication for the SMT solver. + \item \textbf{TermReLU}: This agent is parsed as rectified linear unit for the SMT solver. + \item \textbf{Symbolic}: This agent is parsed as specific variable for the SMT solver. \end{itemize} \end{itemize} @@ -172,11 +170,12 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into t \label{fig:agents} \end{figure} +\paragraph{Linear with Add/Mul} The \textit{Linear} carrier agent interacts directly with the \textit{Add} and \textit{Mul} operators agents as illustrated in \textbf{\Cref{fig:rule-linear-add}} and \textbf{\Cref{fig:rule-linear-mul}}. Because interactions are local, the binary -operators need to check one operator at the time. For this reason \textit{Add} and \textit{Mul} gets replaced by +operators need to check one operand a time. For this reason \textit{Add} and \textit{Mul} agents are replaced by \textit{AddCheckLinear} and \textit{MulCheckLinear} intermediate agents that carry the attributes $q$ and $r$ and their -principal port is faced toward the other operand. +principal port faces the other operand. % Linear >< Add \begin{figure}[ht] @@ -222,12 +221,13 @@ principal port is faced toward the other operand. \label{fig:rule-linear-mul} \end{figure} +\paragraph{Concrete with Add/Mul} The same logic is applied to the \textit{Concrete} carrier agent, but here analyzing the attribute $k$ enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}} we can see that when summing a \textit{Concrete} with $k=0$ we do not need to check the other operand and we simply wire it to the output. This rewiring is also implemented when multiplying a \textit{Concrete} with $k=1$, as shown in \textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$ the other operand is deleted -before is even invoked. +before it is even invoked. % Concrete >< Add \begin{figure}[ht] @@ -325,11 +325,13 @@ before is even invoked. \label{fig:rule-concrete-mul} \end{figure} +\paragraph{Linear with AddCheckLinear/MulCheckLinear} If both operands are \textit{Linear} agents they need to be materialized before being wrapped in another \textit{Linear} to allow further simplification. This is done because multiplying two linear packets gives a non-linear result. -While adding two linear packets gives a linear result, it depends on two free variables and the \textit{Linear} agent -only supports one. A solution to this could be storing a dictionay of variables instead of a single one. +While adding two linear packets gives a linear result, it depends on two free variables and the +\textit{Linear} agent only supports keeping track of one; consequently, the addition of two linear packets +results in their materialization. This is illustrated in \textbf{\Cref{fig:rule-linear-addchecklinear}} and \textbf{\Cref{fig:rule-linear-mulchecklinear}} where the result of the materialization is passed to a TermAdd or TermMul, for Add and Mul respectively, and then to a \textit{Linear} with attributes @@ -475,10 +477,11 @@ $q=1,r=0$. \label{fig:rule-linear-mulchecklinear} \end{figure} -Instead if the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent different rules are applied. -In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) we add the attribute of the \textit{Concrete} -agent to the attribute that represents the constant of the \textit{Linear} agent. -For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) we multiply the attribute of +\paragraph{Concrete with AddCheckLinear/MulCheckLinear} +If, instead, the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent different rules +are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) the system adds the +attribute of the \textit{Concrete} agent to the attribute that represents the constant of the \textit{Linear} agent. +For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) the system multiplies the attribute of the \textit{Concrete} agent to both the attributes of the \textit{Linear} % Concrete >< AddCheckLinear @@ -521,6 +524,7 @@ the \textit{Concrete} agent to both the attributes of the \textit{Linear} \label{fig:rule-concrete-mulchecklinear} \end{figure} +\paragraph{Linear with AddCheckConcrete/MulCheckConcrete} In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \textbf{\Cref{fig:rule-linear-mulcheckconcrete}} we follow the exact same logic except the first operand is a \textit{Concrete} and the second is a \textit{Linear}. @@ -564,6 +568,7 @@ we follow the exact same logic except the first operand is a \textit{Concrete} a \label{fig:rule-linear-mulcheckconcrete} \end{figure} +\paragraph{Concrete with AddCheckConcrete/MulCheckConcrete} Finally if both operands are \textit{Concrete} agents they are either merged into a single \textit{Concrete} or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckconcrete}} and \textbf{\Cref{fig:rule-concrete-mulcheckconcrete}} following a similar logic to the previous rules. @@ -653,6 +658,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \label{fig:rule-concrete-mulcheckconcrete} \end{figure} +\paragraph{Linear/Concrete with ReLU} When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is no enough information to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}}, the agent is just materialized, passed to a \textit{TermReLU} and then wrapped in a \textit{Linear}. @@ -722,7 +728,8 @@ if $k>0$ or with attribute equal $0$ otherwise. \label{fig:rule-concrete-relu} \end{figure} -When a \textit{Linear} is materialized it will explicitly build an AST using \textit{TermAdd} and \textit{TermMul} +\paragraph{Linear/Concrete with Materialize} +When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd} and \textit{TermMul} to recreate $q*x+r$ as shown in \textbf{\Cref{fig:rule-linear-materialize}}. When a \textit{Concrete} needs to be materialized nothing needs to be done and it is directly wired to output \textbf{\Cref{fig:rule-concrete-materialize}}. diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex index 4f2064c..638ff17 100644 --- a/chapters/core/implementation/03-translation.tex +++ b/chapters/core/implementation/03-translation.tex @@ -1,4 +1,142 @@ -\subsection{ONNX Translation} +\subsection{ONNX-to-IN Translation} \label{sec:translation} -% This subsection talks about the function used to translate ONNX to Inpla syntax +An ONNX neural network is organized as a \textit{Directed Acyclic Graph} (DAG), where nodes represent +a specific mathematical operation. While in a standard DAG, a node can be connected to many nodes to +share its value or result, in an IN, an agent has a fixed number of ports, with each port supporting +at most one connection. This limitation is solved by utilizing the \textit{Dup} agent to create the +necessary copies of a value required by the next operations. Since nodes do not know how successor +nodes will utilize their outputs, the translation layer traverses the DAG in reverse order +to be able to instantiate the correct number of \textit{Dup} agents. The main algorithm, illustrated +in \textbf{\Cref{alg:onnx-to-in}}, maintains an \textit{interactions} dictionary data-structure, that maps each tensor +name to a list of ports, to keep track of the graph traversal. + +To maximize the concurrency of the INPLA engine, the translation layer avoids generating linear +chains of agents, opting instead for balanced binary trees for signal distribution (single input to +multiple output) and signal reduction (multiple input to single output). As \textbf{\Cref{alg:balanced-fan-in}} +and \textbf{\Cref{alg:balanced-fan-out}} illustrate, the depth of agent chains (especially \textit{Dup} chains) +is limited to $O(\log N)$. The two algorithms are very similar, the difference is in how they wire the +agents together: in the \textit{Fan-In} the principal port of the agents are facing the leaves, while in the +\textit{Fan-Out} they are facing the root. + +\begin{algorithm}[ht] + \caption{Backwards ONNX-to-IN Translation} + \label{alg:onnx-to-in} + \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} + \Input{ONNX Graph $G$} + \Output{Inpla script $S$} + + $interactions \leftarrow \emptyset$ \tcp*{Map: Tensor Name $\rightarrow$ List of ports} + $S \leftarrow \emptyset$ + + \ForEach{neuron $y$ in $G.output$}{ + $interactions[G.output][y] \leftarrow [\text{Materialize}(result_y)]$ + } + + \ForEach{node $N$ in \textbf{reverse}($G.nodes$)}{ + \Switch{$N.type$}{ + \Case{ReLU}{ + \ForEach{neuron $i$ in $N.output$}{ + $sink \leftarrow \text{BalancedFanOut}(interactions[N.output][i], \text{Dup}, S)$ + + $v \leftarrow \text{generate\_wire}()$ + + $interactions[N.input][i].\text{append}(\text{ReLU}(v))$ + + $S.\text{append}(v \sim sink)$ + } + } + \Case{Gemm}{ + \ForEach{neuron $j$ in $N.output$}{ + $sink \leftarrow \text{BalancedFanOut}(interactions[N.output][j], \text{Dup}, S)$ + + $neuron\_terms \leftarrow \emptyset$ + + \ForEach{neuron $i$ in $N.input$}{ + $v \leftarrow \text{generate\_wire}()$ + + $interactions[N.input][i].\text{append}(\text{Mul}(v, \text{Concrete}(N.alpha * N.weight[j, i])))$ + + $neuron\_terms.\text{append}(v)$ + } + + $neuron\_terms.\text{append}(\text{Concrete}(N.beta * N.bias[j]))$ + + $root \leftarrow \text{BalancedFanIn}(neuron\_terms, \text{Add}, S)$ + + $S.\text{append}(root \sim sink)$ + } + } + \Case{Identity}{ + $interactions[N.input] \leftarrow interactions[N.output]$ + } + } + } + + \ForEach{neuron $x$ in $G.input$}{ + $sink \leftarrow \text{BalancedFanOut}(interactions[G.input][x], \text{Dup}, S)$ + + $S.\text{append}(sink \sim \text{Linear}(\text{Symbolic}(x), 1.0, 0.0))$ + } + + \Return{S} +\end{algorithm} + +\begin{algorithm}[ht] + \caption{Balanced Fan-In} + \label{alg:balanced-fan-in} + \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} + \Input{A list of input signal wires $T$, Agent type $A$, Script $S$} + \Output{A single wire connected to the output of the balanced tree} + + \If{$T = \emptyset$}{\Return{\text{Eraser}}} + \If{$|T| = 1$}{\Return{$T[0]$}} + + \While{$|T| > 1$}{ + $T' \leftarrow \emptyset$ + + \For{$i \leftarrow 0$ \KwTo $|T|-1$ \textbf{by} 2}{ + \eIf{$i+1 < |T|$}{ + $w_{out} \leftarrow \text{generate\_wire}()$ + + $S.\text{append}(T[i] \sim A(w_{out}, T[i+1]))$ + + $T'.\text{append}(w_{out})$ + }{ + $T'.\text{append}(T[i])$ + } + } + $T \leftarrow T'$ + } + \Return{$T[0]$} +\end{algorithm} + + +\begin{algorithm}[ht] + \caption{Balanced Fan-Out} + \label{alg:balanced-fan-out} + \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} + \Input{A list of output signal wires $T$, Agent type $A$, Script $S$} + \Output{A single wire connected to the input of the balanced tree} + + \If{$T = \emptyset$}{\Return{\text{Eraser}}} + \If{$|T| = 1$}{\Return{$T[0]$}} + + \While{$|T| > 1$}{ + $T' \leftarrow \emptyset$ + + \For{$i \leftarrow 0$ \KwTo $|T|-1$ \textbf{by} 2}{ + \eIf{$i+1 < |T|$}{ + $w_{out} \leftarrow \text{generate\_wire}()$ + + $S.\text{append}(w_{out} \sim A(T[i], T[i+1]))$ + + $T'.\text{append}(w_{out})$ + }{ + $T'.\text{append}(T[i])$ + } + } + $T \leftarrow T'$ + } + \Return{$T[0]$} +\end{algorithm} diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex index 7f144db..a40df41 100644 --- a/chapters/core/implementation/04-python-module.tex +++ b/chapters/core/implementation/04-python-module.tex @@ -1,4 +1,36 @@ \subsection{Python Module} \label{sec:python-module} -% This subsection talks how the tool is contained in a neat python module and various optimizations +The core functionality of the VEIN system is implemented via the \texttt{vein.Solver}, an extension of +the \texttt{z3.Solver} class offered in the Z3 python +package\footnote{\href{https://pypi.org/project/z3-solver}{\textbf{PyPi package}}}. This design choice +ensures flexibility and ease of use for researchers already familiar with using the Z3 Python API. + +The methods offered by \texttt{vein.Solver} are: +\begin{itemize} + \item \texttt{load\_onnx}: loads a neural network in ONNX file format. + \item \texttt{load\_smtlib}: loads a file containing the specification. + \item \texttt{check}: orchestrates the translation and reduction pipeline before invoking the + solver to check the specification against one or many neural networks. +\end{itemize} + +The framework uses a \textit{lazy evaluation} strategy: when loading a neural network, it is placed +into a pending queue and it is reduced to normal form only after the \texttt{check} method is +called. + +The specification follows the SMT-LIB\footnote{\href{https://smt-lib.org}{\textbf{SMT-LIB Website}}} +format. It should contain the input and output symbolic variables declaration, optional range +constraints on the input variables and the properties to be verified. For Multi-Network (relational) +verification, the system ensures that multiple networks share the same input symbolic variables. +This approach allows Z3 to compare their outputs directly given the same inputs. + +The execution pipeline is implemented within the \texttt{check} method: +\begin{itemize} + \item \texttt{inpla\_export}: invokes the translation layer to generate an IN. + \item \texttt{inpla\_run}: executes INPLA as a subprocess. + \item \texttt{z3\_evaluate}: parses the normal form, represented by an AST, and constructs the + Z3 expression. +\end{itemize} +This method utilizes a memoization technique to increase performance: if a specific pair of (neural +network, range constraints) has been previously reduced to a normal form, the system retrieves the +cached Z3 expression, instead of running the pipeline redundantly. diff --git a/chapters/core/soundness-proof/01-mathematical-definitions.tex b/chapters/core/soundness-proof/01-mathematical-definitions.tex index 3d8c031..19059ad 100644 --- a/chapters/core/soundness-proof/01-mathematical-definitions.tex +++ b/chapters/core/soundness-proof/01-mathematical-definitions.tex @@ -1,4 +1,36 @@ \subsection{Mathematical Definitions} \label{sec:mathematical-definitions} -% This subsection contains the mathematical definitions used in the proof +We define the semantic function $\llbracket \cdot \rrbracket$. This function maps the state of an IN +to its equivalent mathematical interpretation. Wires and attributes in IN are mapped respectively to +free variables and real numbers in the mathematical interpretation. + +The agents are defined as: +\begin{itemize} + \item $\llbracket \mathit{Linear}(x, q, r) \sim \mathit{out} \rrbracket \iff \mathit{out} = q \cdot x + r $\\ + where $x, \mathit{out}$ are wires and $q, r \in \mathbb{R}$ are attributes. + \item $\llbracket \mathit{Concrete}(k) \sim \mathit{out} \rrbracket \iff \mathit{out} = k$\\ + where $\mathit{out}$ is a wire and $k \in \mathbb{R}$ is an attribute. + \item $\llbracket \mathit{Add}(\mathit{out}, b) \sim a \rrbracket \iff \mathit{out} = a + b$\\ + where $a, b, \mathit{out}$ are wires. + \item $\llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \iff \mathit{out} = q \cdot x + (r + b)$\\ + where $x, b, \mathit{out}$ are wires and $q, r \in \mathbb{R}$ are attributes. + \item $\llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \iff \mathit{out} = k + b$\\ + where $b, \mathit{out}$ are wires and $k \in \mathbb{R}$ is an attribute. + \item $\llbracket \mathit{Mul}(\mathit{out}, b) \sim a \rrbracket \iff \mathit{out} = a \cdot b$\\ + where $a, b, \mathit{out}$ are wires. + \item $\llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \iff \mathit{out} = q \cdot b \cdot x + r \cdot b$\\ + where $x, b, \mathit{out}$ are wires and $q, r \in \mathbb{R}$ are attributes. + \item $\llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \iff \mathit{out} = k \cdot b$\\ + where $b, \mathit{out}$ are wires and $k \in \mathbb{R}$ is an attribute. + \item $\llbracket \mathit{ReLU}(\mathit{out}) \sim x \rrbracket \iff \mathit{out} = \max(0, x)$\\ + where $x, \mathit{out}$ are wires. + \item $\llbracket \mathit{Materialize}(\mathit{out}) \sim x \rrbracket \iff \mathit{out} = x$\\ + where $x, \mathit{out}$ are wires. + \item $\llbracket \mathit{TermAdd}(a, b) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = a + b$\\ + where $a, b, \mathit{out}$ are wires. + \item $\llbracket \mathit{TermMul}(a, b) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = a \cdot b$\\ + where $a, b, \mathit{out}$ are wires. + \item $\llbracket \mathit{TermReLU}(x) \sim \mathit{out} \rrbracket \iff \mathit{out} = \max(0, x)$\\ + where $x, \mathit{out}$ are wires. +\end{itemize} diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex index f112aa5..6764ea2 100644 --- a/chapters/core/soundness-proof/02-soundness-of-translation.tex +++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex @@ -1,4 +1,54 @@ \subsection{Soundness of Translation} \label{sec:soundness-of-translation} -% This subsection gives the proof for ONNX-to-Inpla translation soundness +We need to prove that for each ONNX operator a semantically equivalent IN is produced. + +\paragraph{ReLU} +The ONNX ReLU operator for an input tensor X and output tensor Y is defined as: +$$ +Y = \max(0, X) +$$ +The translation layer produces, for each neuron, the interaction: +$$ +\mathit{ReLU}(y_i) \sim x_i +$$ +Applying the semantic function: +$$ +\llbracket \mathit{ReLU}(y_i) \sim x_i \rrbracket \Rightarrow y_i = \max(0, x_i) +$$ +Which is identical to the ONNX definition. + +\paragraph{Gemm} +The ONNX Gemm (General Matrix Multiplication) operator for input tensors A, B, C, input $\alpha$ +and $\beta$ and output tensor Y is defined as: +$$ +Y = \alpha \cdot A \cdot B + \beta \cdot C +$$ +The translation layer produces, for each neuron, the interactions: +$$ +\mathit{Mul}(v_i, \mathit{Concrete}(\alpha \cdot b_{j, i})) \sim a_i +$$ +And for each layer: +$$ +\mathit{Add}(\dots(\mathit{Add}(y_j, v_1),\dots), v_n) \sim \mathit{Concrete}(\beta \cdot c_j) +$$ +Applying the semantic function: +$$ +\begin{aligned} + \llbracket \mathit{Mul}(v_i, \mathit{Concrete}(\alpha \cdot b_{j, i})) \sim a_i \rrbracket \Rightarrow v_i = \alpha \cdot a_i \cdot b_{j, i}\\ + \llbracket \mathit{Add}(\dots(\mathit{Add}(y_j, v_1),\dots), v_n) \sim \mathit{Concrete}(\beta \cdot c_j) \rrbracket \Rightarrow y_j = \sum_{i=1}^n v_i + \beta \cdot c_j +\end{aligned} +$$ +By substituting $v_i$, the result matches the ONNX definition. + +\paragraph{Identity} +The ONNX Identity does not modify the numerical values of the tensors. As this operator results in a +direct wire connection: +$$ +y_i \sim x_i +$$ +The semantic: +$$ +\llbracket y_i \sim x_i \rrbracket \Rightarrow y_i = x_i +$$ +trivially preserve the identity mapping. diff --git a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex index 9aa84ac..2336135 100644 --- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex +++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex @@ -1,4 +1,507 @@ \subsection{Soundness of Interaction Rules} \label{sec:soundness-of-interaction-rules} -% This subsections gives the proof for each interaction rule +\paragraph{Linear and Add} +For the \textit{Linear} and \textit{Add} agents we have the interaction rule: +$$ +\mathit{Linear}(x, q, r) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\ + & \llbracket \mathit{Add}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w + b \\ + & \Rightarrow \mathit{out} = (q \cdot x + r) + b + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \\ + & \Rightarrow \mathit{out} = q \cdot x + (r + b) + \end{aligned} +\end{aligned} +$$ +Since $(q \cdot x + r) + b = q \cdot x + (r + b)$, the rule is sound. + +\paragraph{Linear and Mul} +For the \textit{Linear} and \textit{Mul} agents we have the interaction rule: +$$ +\mathit{Linear}(x, q, r) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\ + & \llbracket \mathit{Mul}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w \cdot b \\ + & \Rightarrow \mathit{out} = (q \cdot x + r) \cdot b + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \\ + & \Rightarrow \mathit{out} = q \cdot b \cdot x + r \cdot b + \end{aligned} +\end{aligned} +$$ +Since $(q \cdot x + r) \cdot b = q \cdot b \cdot x + r \cdot b$, the rule is sound. + +\paragraph{Concrete and Add} +For the \textit{Concrete} and \textit{Add} agents we have the interaction rule: +$$ +\mathit{Concrete}(k) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow +\begin{cases} + \mathit{out} \sim b & \text{if } k = 0 \\ + \mathit{AddCheckConcrete}(\mathit{out}, k) \sim b & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{Add}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w + b \\ + & \Rightarrow \mathit{out} = k + b + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim b \rrbracket \Rightarrow \mathit{out} = b & \text{if } k = 0 \\ + \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \Rightarrow \mathit{out} = k + b & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 + b = b & \text{if } k = 0 \\ + k + b = k + b & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Concrete and Mul} +For the \textit{Concrete} and \textit{Mul} agents we have the interaction rule: +$$ +\mathit{Concrete}(k) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow +\begin{cases} + \mathit{out} \sim \mathit{Concrete}(0); b \sim \mathit{Eraser} & \text{if } k = 0 \\ + \mathit{out} \sim b & \text{if } k = 1 \\ + \mathit{MulCheckConcrete}(\mathit{out}, k) \sim b & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{Mul}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w \cdot b \\ + & \Rightarrow \mathit{out} = k \cdot b + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(0); b \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } k = 0 \\ + \llbracket \mathit{out} \sim b \rrbracket \Rightarrow \mathit{out} = b & \text{if } k = 1 \\ + \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \Rightarrow \mathit{out} = k \cdot b & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 \cdot b = 0 & \text{if } k = 0 \\ + 1 \cdot b = b & \text{if } k = 1 \\ + k \cdot b = k \cdot b & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Linear and AddCheckLinear} +For the \textit{Linear} and \textit{AddCheckLinear} agents we have the interaction rule: +$$ +\begin{aligned} + & \mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} & \text{if } q,r,s,t = 0 \\ + \mathit{out} \sim \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} & \text{if } s,t = 0 \\ + \mathit{out} \sim \mathit{Linear}(y, s, t); x \sim \mathit{Eraser} & \text{if } q,r = 0 \\ + \begin{aligned} + & \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\ + & \mathit{Linear}(y, s, t) \sim \mathit{Materialize}(\mathit{out}_y); \\ + & \mathit{out} \sim \mathit{Linear}(\mathit{TermAdd}(\mathit{out}_x, \mathit{out}_y), 1, 0) + \end{aligned} + & \text{otherwise} + \end{cases} +\end{aligned} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\ + & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\ + & \Rightarrow \mathit{out} = q \cdot x + (r + s \cdot y + t) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r,s,t = 0 \\ + \llbracket \mathit{out} \sim \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{if } s,t = 0 \\ + \llbracket \mathit{out} \sim \mathit{Linear}(y, s, t); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = s \cdot y + t & \text{if } q,r = 0 \\ + \begin{aligned} + & \llbracket \mathit{Linear}(x, q, r) \sim w_1 \rrbracket \Rightarrow w_1 = q \cdot x + r \\ + & \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w_1 \rrbracket \Rightarrow \mathit{out}_x = w_1 \\ + & \llbracket \mathit{Linear}(y, s, t) \sim w_2 \rrbracket \Rightarrow w_2 = s \cdot y + t \\ + & \llbracket \mathit{Materialize}(\mathit{out}_y) \sim w_2 \rrbracket \Rightarrow \mathit{out}_y = w_2 \\ + & \llbracket \mathit{Linear}(\mathit{TermAdd}(\mathit{out}_x, \mathit{out}_y), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot (\mathit{out}_x + \mathit{out}_y) + 0 + \end{aligned}\\ + \Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 \cdot x + (0 + 0 \cdot y + 0) = 0 & \text{if } q,r,s,t = 0 \\ + q \cdot x + (r + 0 \cdot y + 0) = q \cdot x + r & \text{if } s,t = 0 \\ + 0 \cdot x + (0 + s \cdot y + t) = s \cdot y + t & \text{if } q,r = 0 \\ + q \cdot x + (r + s \cdot y + t) = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Linear and MulCheckLinear} +For the \textit{Linear} and \textit{MulCheckLinear} agents we have the interaction rule: +$$ +\begin{aligned} + & \mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} & \text{if } q,r = 0 \lor s,t = 0 \\ + \begin{aligned} + & \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\ + & \mathit{Linear}(y, s, t) \sim \mathit{Materialize}(\mathit{out}_y); \\ + & \mathit{out} \sim \mathit{Linear}(\mathit{TermMul}(\mathit{out}_x, \mathit{out}_y), 1, 0) + \end{aligned} + & \text{otherwise} + \end{cases} +\end{aligned} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\ + & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\ + & \Rightarrow \mathit{out} = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r = 0 \lor s,t = 0 \\ + \begin{aligned} + & \llbracket \mathit{Linear}(x, q, r) \sim w_1 \rrbracket \Rightarrow w_1 = q \cdot x + r \\ + & \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w_1 \rrbracket \Rightarrow \mathit{out}_x = w_1 \\ + & \llbracket \mathit{Linear}(y, s, t) \sim w_2 \rrbracket \Rightarrow w_2 = s \cdot y + t \\ + & \llbracket \mathit{Materialize}(\mathit{out}_y) \sim w_2 \rrbracket \Rightarrow \mathit{out}_y = w_2 \\ + & \llbracket \mathit{Linear}(\mathit{TermMul}(\mathit{out}_x, \mathit{out}_y), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot \mathit{out}_x \cdot \mathit{out}_y + 0 + \end{aligned}\\ + \Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 \cdot (s \cdot y + t) \cdot x + 0 \cdot (s \cdot y + t) = 0 \lor q \cdot (0 \cdot y + 0) \cdot x + r \cdot (0 \cdot y + 0) = 0 & \text{if } q,r = 0 \lor s,t = 0 \\ + 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Concrete and AddCheckLinear} +For the \textit{Concrete} and \textit{AddCheckLinear} agents we have the interaction rule: +$$ +\mathit{Concrete}(j) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q, r + j) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\ + & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\ + & \Rightarrow \mathit{out} = q \cdot x + (r + j) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(x, q, r + j) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = q \cdot x + (r + j) + \end{aligned} +\end{aligned} +$$ +Since $q \cdot x + (r + j) = q \cdot x + (r + j)$, the rule is sound. + +\paragraph{Concrete and MulCheckLinear} +For the \textit{Concrete} and \textit{MulCheckLinear} agents we have the interaction rule: +$$ +\mathit{Concrete}(j) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\ + & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\ + & \Rightarrow \mathit{out} = q \cdot j \cdot x + r \cdot j + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = (q \cdot j) \cdot x + (r \cdot j) + \end{aligned} +\end{aligned} +$$ +Since $q \cdot j \cdot x + r \cdot j = (q \cdot j) \cdot x + (r \cdot j)$, the rule is sound. + +\paragraph{Linear and AddCheckConcrete} +For the \textit{Linear} and \textit{AddCheckConcrete} agents we have the interaction rule: +$$ +\mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s, t + k) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\ + & \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k + w \\ + & \Rightarrow \mathit{out} = k + (s \cdot y + t) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(y, s, t + k) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = s \cdot y + (t + k) + \end{aligned} +\end{aligned} +$$ +Since $k + (s \cdot y + t) = s \cdot y + (t + k)$, the rule is sound. + +\paragraph{Linear and MulCheckConcrete} +For the \textit{Linear} and \textit{MulCheckConcrete} agents we have the interaction rule: +$$ +\mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\ + & \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k \cdot w \\ + & \Rightarrow \mathit{out} = k \cdot (s \cdot y + t) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = (s \cdot k) \cdot y + (t \cdot k) + \end{aligned} +\end{aligned} +$$ +Since $k \cdot (s \cdot y + t) = (s \cdot k) \cdot y + (t \cdot k)$, the rule is sound. + +\paragraph{Concrete and AddCheckConcrete} +For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule: +$$ +\mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow +\begin{cases} + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\ + \mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\ + & \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k + w \\ + & \Rightarrow \mathit{out} = k + j + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } j = 0 \\ + \llbracket \mathit{out} \sim \mathit{Concrete}(k + j) \rrbracket \Rightarrow \mathit{out} = k + j & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + k + 0 = k & \text{if } j = 0 \\ + k + j = k + j & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Concrete and MulCheckConcrete} +For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule: +$$ +\mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow +\begin{cases} + \mathit{out} \sim \mathit{Concrete}(0) & \text{if } j = 0 \\ + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 1 \\ + \mathit{out} \sim \mathit{Concrete}(k \cdot j) & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\ + & \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k \cdot w \\ + & \Rightarrow \mathit{out} = k \cdot j + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(0) \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } j = 0 \\ + \llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } j = 1 \\ + \llbracket \mathit{out} \sim \mathit{Concrete}(k \cdot j) \rrbracket \Rightarrow \mathit{out} = k \cdot j & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + k \cdot 0 = 0 & \text{if } j = 0 \\ + k \cdot 1 = k & \text{if } j = 1 \\ + k \cdot j = k \cdot j & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Linear and ReLU} +For the \textit{Linear} and \textit{ReLU} agents we have the interaction rule: +$$ +\begin{aligned} + & \mathit{Linear}(x, q, r) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow + \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); + \mathit{out} \sim \mathit{Linear}(\mathit{TermReLU}(\mathit{out}_x), 1, 0) +\end{aligned} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(q, x, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\ + & \llbracket \mathit{ReLU}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = \max(0, w) \\ + & \Rightarrow \mathit{out} = \max(0, q \cdot x + r) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow w = q \cdot x + r \\ + & \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w \rrbracket \Rightarrow \mathit{out}_x = w \\ + & \llbracket \mathit{Linear}(\mathit{TermReLU}(\mathit{out}_x), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot \max(0, \mathit{out}_x) + 0 \\ + & \Rightarrow \mathit{out} = 1 \cdot \max(0, q \cdot x + r) + 0 + \end{aligned} +\end{aligned} +$$ +Since $\max(0, q \cdot x + r) = 1 \cdot \max(0, q \cdot x + r) + 0$ the rule is sound. + +\paragraph{Concrete and ReLU} +For the \textit{Concrete} and \textit{ReLU} agents we have the interaction rule: +$$ +\mathit{Concrete}(k) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow +\begin{cases} + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } k > 0 \\ + \mathit{out} \sim \mathit{Concrete}(0) & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{ReLU}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = \max(0, w) \\ + & \Rightarrow \mathit{out} = \max(0, k) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } k > 0 \\ + \llbracket \mathit{out} \sim \mathit{Concrete}(0) \rrbracket \Rightarrow \mathit{out} = 0 & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + \max(0, k) = k & \text{if } k > 0 \\ + \max(0, k) = 0 & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Linear and Materialize} +For the \textit{Linear} and \textit{Materialize} agents we have the interaction rule: +$$ +\begin{aligned} + & \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(r); x \sim \mathit{Eraser} & \text{if } q = 0 \\ + \mathit{out} \sim x & \text{if } q = 1, r = 0 \\ + \mathit{out} \sim \mathit{TermAdd}(x, \mathit{Concrete}(r)) & \text{if } q = 1 \\ + \mathit{out} \sim \mathit{TermMul}(\mathit{Concrete}(q), x) & \text{if } r = 0 \\ + \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{Concrete}(q), x), \mathit{Concrete}(r)) & \text{otherwise} + \end{cases} +\end{aligned} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\ + & \llbracket \mathit{Materialize}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = w \\ + & \Rightarrow \mathit{out} = q \cdot x + r + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(r); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = r & \text{if } q = 0 \\ + \llbracket \mathit{out} \sim x \rrbracket \Rightarrow \mathit{out} = x & \text{if } q = 1, r = 0 \\ + \llbracket \mathit{out} \sim \mathit{TermAdd}(x, \mathit{Concrete}(r)) \rrbracket \Rightarrow \mathit{out} = x + r & \text{if } q = 1 \\ + \llbracket \mathit{out} \sim \mathit{TermMul}(\mathit{Concrete}(q), x) \rrbracket \Rightarrow \mathit{out} = q \cdot x & \text{if } r = 0 \\ + \llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{Concrete}(q), x), \mathit{Concrete}(r)) \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{otherwise} \\ + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 \cdot x + r = r & \text{if } q = 0 \\ + 1 \cdot x + 0 = x & \text{if } q = 1, r = 0 \\ + 1 \cdot x + r = x + r & \text{if } q = 1 \\ + q \cdot x + 0 = q \cdot x & \text{if } r = 0 \\ + q \cdot x + r = q \cdot x + r & \text{otherwise} \\ +\end{cases} +$$ +the rule is sound. + +\paragraph{Concrete and Materialize} +For the \textit{Concrete} and \textit{Materialize} agents we have the interaction rule: +$$ +\mathit{Concrete}(k) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \mathit{Concrete}(k) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{Materialize}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = w \\ + & \Rightarrow \mathit{out} = k + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Concrete}(k) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = k + \end{aligned} +\end{aligned} +$$ +Since $k = k$, the rule is sound. diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex index b2d6116..b0a7906 100644 --- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex +++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex @@ -1,4 +1,28 @@ \subsection{Soundness of Reduction} \label{sec:soundness-of-reduction} -% This subsection gives the proof that each reduction step doesn't alter the semantic +Let $\text{IN}_0$ be the IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be +the IN after $n$ reduction steps. Then we need to prove: +$$ +\forall n \in \mathbb{N} \quad \llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket +$$ + +\paragraph{Base case: $n = 0$} By \textbf{\Cref{sec:soundness-of-translation}}, the initial +$\text{IN}_0$ is constructed such that its semantics $\llbracket \text{IN}_0 \rrbracket$ exactly +match the mathematical definition of the ONNX operators in $\text{NN}$. + +\paragraph{Induction step: $n \to n + 1$} Assume $\llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket$. +If $\text{IN}_n$ is in normal form, the proof is complete. Otherwise, there exists an active pair +$A \bowtie B$ that reduces $\text{IN}_n$ to $\text{IN}_{n+1}$. By \textbf{\Cref{sec:soundness-of-interaction-rules}}, +the mathematical definition is preserved after any reduction step, it follows that: +$$ +\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{IN}_{n} \rrbracket +$$ +By the inductive hypothesis: +$$ +\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{NN} \rrbracket +$$ + +By the principle of mathematical induction, $\text{IN}_n$ remains semantically equivalent to the +original $\text{NN}$ at every step of the reduction process. Additionally, since IN are confluent, +the reduced mathematical expression is unique regardless of order in which rules are applied. |