From 11f14a4763533dbc24b0e98d115071036025d4f6 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Mon, 22 Jun 2026 00:43:45 +0200 Subject: refinement --- chapters/core/implementation/01-inpla.tex | 8 ++++---- chapters/core/implementation/02-interaction-rules.tex | 6 +++--- chapters/core/implementation/03-translation.tex | 7 ++++--- chapters/core/implementation/04-python-module.tex | 6 +++--- 4 files changed, 14 insertions(+), 13 deletions(-) (limited to 'chapters/core/implementation') diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex index eeebf47..57d3195 100644 --- a/chapters/core/implementation/01-inpla.tex +++ b/chapters/core/implementation/01-inpla.tex @@ -1,7 +1,7 @@ \subsection{INPLA fork} \label{sec:inpla} -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.}}}, +The \textbf{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. @@ -24,7 +24,7 @@ INPLA evaluates nets which consist of connections between terms. Terms are built ::= | ::= ::= - | ['(' ',' ... ',' ')'] + | ['(' ',' ... ',' ')'] \end{verbatim} \end{small} \begin{itemize} @@ -37,12 +37,12 @@ Interaction rules rewrite connections between agents: \begin{verbatim} ::= '><' '=>' ';' ::= - | '(' ',' ... ',' ')' + | '(' ',' ... ',' ')' \end{verbatim} \end{small} \paragraph{Example} -Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successive function). For +Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successor 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{small} diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex index 49a8a70..8b02c3c 100644 --- a/chapters/core/implementation/02-interaction-rules.tex +++ b/chapters/core/implementation/02-interaction-rules.tex @@ -1,7 +1,7 @@ \subsection{Interaction Rules} \label{sec:interaction-rules} -The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into four groups: +The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into five groups: \begin{itemize} \item \textbf{Carriers}: Agents that contain float attributes. @@ -179,7 +179,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f (m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{TermSymbolic}$ & (q) $\mathit{TermConcrete}$ \\[0.5cm] \end{tabular} } - \caption{Agents used in VEIN.} + \caption{Agents used in \textbf{VEIN}.} \label{fig:agents} \end{figure} @@ -495,7 +495,7 @@ If, instead, the first operand is a \textit{Linear} agents and the second is a \ 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} +the \textit{Concrete} agent to both the attributes of the \textit{Linear}. % Concrete >< AddCheckLinear \begin{figure}[H] diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex index 0a2eec0..b86e060 100644 --- a/chapters/core/implementation/03-translation.tex +++ b/chapters/core/implementation/03-translation.tex @@ -9,7 +9,8 @@ necessary copies of a value required by the next operations. Since nodes do not 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. +name to a list of ports, to keep track of the graph traversal. The ONNX operators supported are Gemm +(General matrix multiplication) and ReLU. \begin{algorithm}[H] \caption{Backwards ONNX-to-IN Translation} @@ -79,9 +80,9 @@ To maximize the concurrency of the INPLA engine, the translation layer avoids ge 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 +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. +\textit{Fan-Out} they face the root. \begin{algorithm}[H] \caption{Balanced Fan-In} diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex index a40df41..6023c2e 100644 --- a/chapters/core/implementation/04-python-module.tex +++ b/chapters/core/implementation/04-python-module.tex @@ -1,8 +1,8 @@ \subsection{Python Module} \label{sec:python-module} -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 +The core functionality of the \textbf{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. @@ -19,7 +19,7 @@ into a pending queue and it is reduced to normal form only after the \texttt{che 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 +format. It should contain the input and output symbolic variables declarations, 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. -- cgit v1.2.3