core

13 files changed, 884 insertions, 37 deletions

diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex
index 8b912db..fc4017a 100644
--- a/chapters/01-introduction.tex
+++ b/chapters/01-introduction.tex
@@ -18,20 +18,19 @@ either hold or are violated. The kind of properties that can be verified are two
 	\item \textbf{Multi-Network}: we check if multiple neural networks satisfy a given relation.
 \end{itemize}
 An example of a Multi-Network property is equivalence between different neural networks; this
-verification is crucial if we want to replace a neural network with a smaller, equivalent one.
-Techniques based on specialized \textit{Satisfiability Modulo Theories} (SMT) solvers may be used in
-the verification algorithm, however, as networks grow in depth and width, the number of non-linear
-components, most notably the \textit{Rectified Linear Unit}\footnote{Defined as $f(x)=\max(0, x)$, where $x$ is
-the input to the neuron.} (ReLU) activation function, creates an exponential search space for the
-solver. Because of this issue, running a solver against a raw, unoptimized network is often
-computationally prohibitive.
+verification is crucial when replacing a neural network with a smaller, equivalent one. Techniques
+based on specialized \textit{Satisfiability Modulo Theories} (SMT) solvers may be used in the verification
+algorithm, however, as networks grow in depth and width, the number of non-linear components, most
+notably the \textit{Rectified Linear Unit}\footnote{Defined as $f(x)=\max(0, x)$, where $x$ is the input to the
+neuron.} (ReLU) activation function, creates an exponential search space for the solver. Because of
+this issue, running a solver against a raw, unoptimized network is often computationally prohibitive.
 
 Furthermore, we lack a formal intermediate representation. Since we are
 not able to directly feed a neural network to a SMT solver, a sound and deterministic model of
 representation is needed to bridge this gap.
 
 % Solution
-To address the computational bottleneck, we can perform symbolic simplification on the neural
+To address the computational bottleneck, symbolic simplification is performed on the neural
 network as a pre-processing step to reduce the burden on the SMT solver. Considering that we can
 easily map the layers and neurons of neural networks to graph nodes and that the input of a SMT
 solver is a mathematical formula that can be represented by an \textit{Abstract Syntax Tree} (AST), we can
diff --git a/chapters/03-core.tex b/chapters/03-core.tex
index d8913d3..f9a4cab 100644
--- a/chapters/03-core.tex
+++ b/chapters/03-core.tex
@@ -1,7 +1,9 @@
 \chapter{VEIN: VErification via Interaction Nets}
 \label{ch:core}
 
-% This chapter contains the core of the thesis, where the work is presented in details.
+This chapter contains details on framework implementation (\textbf{\Cref{sec:implementation}}), the
+proof of soundness of the pipeline (\textbf{\Cref{sec:soundness-proof}}) and a collection of data
+gathered from benchmarks (\textbf{\Cref{sec:benchmarks}})
 
 \input{chapters/core/01-implementation}
 
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.
diff --git a/main.tex b/main.tex
index e1c1a06..21356f3 100644
--- a/main.tex
+++ b/main.tex
@@ -6,15 +6,19 @@
 \usepackage{amsmath, amssymb, amsthm}
 \usepackage{cite}
 \usepackage[colorlinks=true, linkcolor=black, citecolor=black, urlcolor=black]{hyperref}
+\usepackage[linesnumbered,ruled,vlined]{algorithm2e}
 \usepackage[nameinlink]{cleveref}
 \usepackage{xspace}
 \usepackage[colorinlistoftodos]{todonotes}
 % \usepackage[scaled=.83]{beramono} 
 \usepackage{lineno}
 \usepackage{tikz-inet}
+\usepackage{stmaryrd}
 
 \usetikzlibrary{calc}
 \linenumbers
+\crefname{algocf}{alg.}{algs.}
+\Crefname{algocf}{Algorithm}{Algorithms}
 
 \input{macros}