From d3e761a2286d04a3c0005b199653df2f6501f070 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Fri, 19 Jun 2026 12:39:13 +0200 Subject: refined core --- chapters/core/01-implementation.tex | 2 +- chapters/core/03-benchmarks.tex | 84 +- chapters/core/implementation/01-inpla.tex | 22 +- .../core/implementation/02-interaction-rules.tex | 107 +- chapters/core/implementation/03-translation.tex | 32 +- .../01-mathematical-definitions.tex | 12 +- .../02-soundness-of-translation.tex | 18 +- .../03-soundness-of-interaction-rules.tex | 1290 +++++++++++++------- .../soundness-proof/04-soundness-of-reduction.tex | 133 +- 9 files changed, 1117 insertions(+), 583 deletions(-) (limited to 'chapters/core') diff --git a/chapters/core/01-implementation.tex b/chapters/core/01-implementation.tex index 3e8fa20..32154ef 100644 --- a/chapters/core/01-implementation.tex +++ b/chapters/core/01-implementation.tex @@ -1,7 +1,7 @@ \section{Implementation} \label{sec:implementation} -This sections contains details on the implementation of the reduction engine (\textbf{\Cref{sec:inpla}}), +This section 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}}). diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex index 40c1986..132b56d 100644 --- a/chapters/core/03-benchmarks.tex +++ b/chapters/core/03-benchmarks.tex @@ -1,4 +1,86 @@ \section{Benchmarks} \label{sec:benchmarks} -% This section contains the varius benchmarks +This section contains the benchmark data, illustrated in \textbf{\Cref{tab:benchmarks}}. + +VEIN was tested on a laptop Zenbook UX3402ZA with: +\begin{itemize} + \item \textbf{CPU}: 12th Gen Intel Core i5-1240P + \item \textbf{RAM}: 8GiB + \item \textbf{SWAP}: 16GiB on NVMe +\end{itemize} +using Hyperfine\footnote{\href{https://github.com/sharkdp/hyperfine}{\textbf{Hyperfine Github repository}}.} +benchmarking tool. Hyperfine runs the test ten times, then reports the mean and standard deviation of +execution time. + +\paragraph{Iris} +Dataset of iris flowers presented by Fisher et al.~\cite{fisher1936iris}. It consists of three +species of flower (\textit{Iris setosa}, \textit{Iris virginica} and \textit{Iris versicolor}) with fifty samples each. Each +sample has four features: width and length of sepals and petals. +\paragraph{Pendulum} +A neural safety certificate for stabilizing a pendulum to its upright position under a bound on its +angle $\theta$, with state $x=[\theta,\dot\theta]\in\mathbb{R}^2$ and nonlinear dynamics. +\paragraph{Double Integrator} +A neural safety certificate for stabilizing a second-order linear system to the origin under a bound +on its position $p$, with state $x=[p,\dot p]\in\mathbb{R}^2$. +\paragraph{MNIST} +Widely known dataset of handwritten digits presented by LeCun et al.~\cite{lecun2010mnist}. It +consists of 60'000 training images and 10'000 testing images. + +Pendulum and Double Integrator are taken from \textit{cersyve}, a benchmark presented by Kaulen et +al.~\cite{kaulen20256thinternationalverificationneural}. We check equivalence between a pre-trained +and a fine-tuned network for each task. + +In the Iris and MNIST dataset, we tested equivalence between a NN and its ad-hoc transformation, +such as pruning always positive or negative ReLUs, as presented by Kumar et al.~\cite{kumar2019equivalentapproximatetransformationsdeep}, +or changing the architecture from wide to deep and viceversa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}. + +For two NN $F: \mathbb{R}^n \to \mathbb{R}^m$ and $F': \mathbb{R}^n \to \mathbb{R}^m$, Eleftheriadis et al.~\cite{eleftheriadis2022equivalence} +define three kinds of equivalence: +\begin{itemize} + \item \textbf{Strict equivalence}: $\forall x \in \mathbb{R}^n \quad F(x) = F'(x)$. + \item \textbf{Epsilon equivalence}: $\forall x \in \mathbb{R}^n \quad ||F(x) - F'(x)|| < \epsilon$ for some $\epsilon > 0$. + \item \textbf{Argmax equivalence}: $\forall x \in \mathbb{R}^n \quad \mathtt{argmax}(F(x))=\mathtt{argmax}(F'(x))$ where \texttt{argmax} + is the function that returns the index of the maximum value of a vector. +\end{itemize} + +\begin{table}[H] + \centering + \begin{tabular}[t]{ccccc} + \hline + Benchmark & Equivalence & Direct [s] & VEIN [s] & Status \\ + \hline + Iris (Stably Active) & Strict & 0.0 & 0.0 & X \\ + Iris (Stably Active) & Epsilon & 0.0 & 0.0 & X \\ + Iris (Stably Active) & Argmax & 0.0 & 0.0 & X \\ + Iris (Stably Inactive) & Strict & 0.0 & 0.0 & X \\ + Iris (Stably Inactive) & Epsilon & 0.0 & 0.0 & X \\ + Iris (Stably Inactive) & Argmax & 0.0 & 0.0 & X \\ + Iris (To Wide) & Strict & 0.0 & 0.0 & X \\ + Iris (To Wide) & Epsilon & 0.0 & 0.0 & X \\ + Iris (To Wide) & Argmax & 0.0 & 0.0 & X \\ + Iris (To Deep) & Strict & 0.0 & 0.0 & X \\ + Iris (To Deep) & Epsilon & 0.0 & 0.0 & X \\ + Iris (To Deep) & Argmax & 0.0 & 0.0 & X \\ + Pendulum & Strict & 0.0 & 88.427 ± 0.670 & SAT \\ + Pendulum & Epsilon & 0.0 & 0.0 & X \\ + Pendulum & Argmax & 0.0 & 0.0 & X \\ + Double Integrator & Strict & 0.0 & 0.0 & X \\ + Double Integrator & Epsilon & 0.0 & 0.0 & X \\ + Double Integrator & Argmax & 0.0 & 0.0 & X \\ + MNIST (Stably Active) & Strict & 0.0 & 0.0 & X \\ + MNIST (Stably Active) & Epsilon & 0.0 & 0.0 & X \\ + MNIST (Stably Active) & Argmax & 0.0 & 0.0 & X \\ + MNIST (Stably Inactive) & Strict & 0.0 & 0.0 & X \\ + MNIST (Stably Inactive) & Epsilon & 0.0 & 0.0 & X \\ + MNIST (Stably Inactive) & Argmax & 0.0 & 0.0 & X \\ + MNIST (To Wide) & Strict & 0.0 & 0.0 & X \\ + MNIST (To Wide) & Epsilon & 0.0 & 0.0 & X \\ + MNIST (To Wide) & Argmax & 0.0 & 0.0 & X \\ + MNIST (To Deep) & Strict & 0.0 & 0.0 & X \\ + MNIST (To Deep) & Epsilon & 0.0 & 0.0 & X \\ + MNIST (To Deep) & Argmax & 0.0 & 0.0 & X \\ + \end{tabular} + \caption{Benchmark table.} + \label{tab:benchmarks} +\end{table} diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex index 5b2eab9..eeebf47 100644 --- a/chapters/core/implementation/01-inpla.tex +++ b/chapters/core/implementation/01-inpla.tex @@ -1,7 +1,7 @@ -\subsection{Inpla fork} +\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 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. @@ -18,38 +18,48 @@ Several modifications adapt INPLA to the pipeline of the framework: \end{itemize} \paragraph{INPLA syntax} -INPLA evaluates nets, they consist of connections between terms. Terms are built on names and agents: +INPLA evaluates nets which consist of connections between terms. Terms are built on names and agents: +\begin{small} \begin{verbatim} ::= | ::= ::= - | ['(' ',' ... ',' ')'] + | ['(' ',' ... ',' ')'] \end{verbatim} +\end{small} \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{small} \begin{verbatim} ::= '><' '=>' ';' ::= - | '(' ',' ... ',' ')' + | '(' ',' ... ',' ')' \end{verbatim} +\end{small} \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: +increment operation ``inc'' such that: +\begin{small} \begin{verbatim} inc(n) = S(n). \end{verbatim} +\end{small} This is written as the following rules: +\begin{small} \begin{verbatim} inc(r) >< Z => r ~ S(Z); inc(r) >< S(x) => r ~ S(S(x)); \end{verbatim} +\end{small} Then, the result of \texttt{inc(r) \~{} S(S(Z))} is: +\begin{small} \begin{verbatim} r ~ S(S(S(Z))); \end{verbatim} +\end{small} diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex index b657ee9..49a8a70 100644 --- a/chapters/core/implementation/02-interaction-rules.tex +++ b/chapters/core/implementation/02-interaction-rules.tex @@ -10,13 +10,17 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \item \textbf{Concrete}: Represents a constant value $k$. \end{itemize} \item - \textbf{Operators}: Agents that perform some kind of operation on the carrier agents. + \textbf{Computational Operators}: Agents that perform some kind of operation on the carrier agents. \begin{itemize} \item \textbf{Add}: Binary operator for addition. \item \textbf{Mul}: Binary operator for multiplication. \item \textbf{ReLU}: Unary operator for rectified linear unit. + \end{itemize} + \item + \textbf{Structural Operators}: Agents that perform some kind of operation on net structure. + \begin{itemize} \item \textbf{Eraser}: Built-in INPLA unary operator to delete other agents. - \item \textbf{Duplicator}: Built-in INPLA unary operator to duplicate other agents. + \item \textbf{Dup}: Built-in INPLA unary operator to duplicate other agents. \end{itemize} \item \textbf{Intermediates}: Agents needed to perform each step of the operators. @@ -28,32 +32,37 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \item \textbf{Materialize}: Converts a Linear agent into an explicit representation for the SMT solver. \end{itemize} \item - \textbf{Inerts}: Agents that compose the normal form. + \textbf{Terminals}: Agents that compose the normal form. \begin{itemize} \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. + \item \textbf{TermSymbolic}: This agent is parsed as a specific variable for the SMT solver. + \item \textbf{TermConcrete}: This agent is parsed as a real value for the SMT solver. \end{itemize} \end{itemize} -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ - \begin{tabular}{cccc} + \begin{tabular}{ccccc} % Linear + & \begin{tikzpicture} \agentLinear{L}{q}{r} \inetwirefree(L.pal) \inetwirefree(L.pax) \node[below] at (L.above pal) {$\mathit{out}$}; \node[above] at (L.above pax) {$\mathit{x}$}; \end{tikzpicture} & + & % Concrete \begin{tikzpicture} \agentConcrete{C}{k} \inetwirefree(C.pal) \node[below] at (C.above pal) {$\mathit{out}$}; - \end{tikzpicture} & + \end{tikzpicture} & \\ + & (a) $\mathit{Linear}$ & & (b) $\mathit{Concrete}$ & \\[0.5cm] + % Add \begin{tikzpicture} \agentAdd{A} @@ -69,9 +78,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \node[below] at (M.above pal) {$\mathit{a}$}; \node[above] at (M.above pax 1) {$\mathit{out}$}; \node[above] at (M.above pax 2) {$\mathit{b}$}; - \end{tikzpicture} \\ - (a) $\mathit{Linear}$ & (b) $\mathit{Concrete}$ & (c) $\mathit{Add}$ & (d) $\mathit{Mul}$ \\[0.5cm] - + \end{tikzpicture} & % ReLU \begin{tikzpicture} \agentReLU{R} @@ -79,13 +86,6 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \node[below] at (R.above pal) {$\mathit{x}$}; \node[above] at (R.above pax) {$\mathit{out}$}; \end{tikzpicture} & - % Materialize - \begin{tikzpicture} - \agentMaterialize{MAT} - \inetwirefree(MAT.pal) \inetwirefree(MAT.pax) - \node[below] at (MAT.above pal) {$\mathit{x}$}; - \node[above] at (MAT.above pax) {$\mathit{out}$}; - \end{tikzpicture} & % Eraser \begin{tikzpicture} \agentEraser{E} @@ -100,7 +100,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \node[above] at (D.above pax 1) {$\mathit{d_{1}}$}; \node[above] at (D.above pax 2) {$\mathit{d_{2}}$}; \end{tikzpicture} \\ - (e) $\mathit{ReLU}$ & (f) $\mathit{Materialize}$ & (g) $\mathit{Eraser}$ & (h) $\mathit{Duplicator}$ \\[0.5cm] + (c) $\mathit{Add}$ & (d) $\mathit{Mul}$ & (e) $\mathit{ReLU}$ & (f) $\mathit{Eraser}$ & (g) $\mathit{Duplicator}$ \\[0.5cm] % AddCheckLinear \begin{tikzpicture} @@ -131,8 +131,15 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \inetwirefree(MC.pal) \inetwirefree(MC.pax) \node[below] at (MC.above pal) {$\mathit{b}$}; \node[above] at (MC.above pax) {$\mathit{out}$}; + \end{tikzpicture} & + % Materialize + \begin{tikzpicture} + \agentMaterialize{MAT} + \inetwirefree(MAT.pal) \inetwirefree(MAT.pax) + \node[below] at (MAT.above pal) {$\mathit{x}$}; + \node[above] at (MAT.above pax) {$\mathit{out}$}; \end{tikzpicture} \\ - (i) $\mathit{AddCheckLinear}$ & (j) $\mathit{MulCheckLinear}$ & (k) $\mathit{AddCheckConcrete}$ & (l) $\mathit{MulCheckConcrete}$ \\[0.5cm] + (h) $\mathit{AddCheckLinear}$ & (i) $\mathit{MulCheckLinear}$ & (j) $\mathit{AddCheckConcrete}$ & (k) $\mathit{MulCheckConcrete}$ & (l) $\mathit{Materialize}$ \\[0.5cm] % TermAdd \begin{tikzpicture} @@ -157,13 +164,19 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \node[below] at (TR.above pal) {$\mathit{out}$}; \node[above] at (TR.above pax) {$\mathit{x}$}; \end{tikzpicture} & - % Symbolic + % TermSymbolic \begin{tikzpicture} - \agentSymbolic{S}{id} + \agentTermSymbolic{S}{id} \inetwirefree(S.pal) \node[below] at (S.above pal) {$\mathit{out}$}; + \end{tikzpicture} & + % TermConcrete + \begin{tikzpicture} + \agentTermConcrete{C}{k} + \inetwirefree(C.pal) + \node[below] at (C.above pal) {$\mathit{out}$}; \end{tikzpicture} \\ - (m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{Symbolic}$ \\[0.5cm] + (m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{TermSymbolic}$ & (q) $\mathit{TermConcrete}$ \\[0.5cm] \end{tabular} } \caption{Agents used in VEIN.} @@ -178,7 +191,7 @@ operators need to check one operand a time. For this reason \textit{Add} and \te principal port faces the other operand. % Linear >< Add -\begin{figure}[ht] +\begin{figure}[H] \centering \interactionrule{ \agentLinear{L}{q}{r}[90] @@ -200,7 +213,7 @@ principal port faces the other operand. \end{figure} % Linear >< Mul -\begin{figure}[ht] +\begin{figure}[H] \centering \interactionrule{ \agentLinear{L}{q}{r}[90] @@ -230,7 +243,7 @@ This rewiring is also implemented when multiplying a \textit{Concrete} with $k=1 before it is even invoked. % Concrete >< Add -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \begin{tabular}{c} @@ -270,7 +283,7 @@ before it is even invoked. \end{figure} % Concrete >< Mul -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \begin{tabular}{c} @@ -338,7 +351,7 @@ to a TermAdd or TermMul, for Add and Mul respectively, and then to a \textit{Lin $q=1,r=0$. % Linear >< AddCheckLinear -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \begin{tabular}{c} @@ -426,7 +439,7 @@ $q=1,r=0$. \end{figure} % Linear >< MulCheckLinear -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \begin{tabular}{c} @@ -485,7 +498,7 @@ For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) the system the \textit{Concrete} agent to both the attributes of the \textit{Linear} % Concrete >< AddCheckLinear -\begin{figure}[ht] +\begin{figure}[H] \centering \interactionrule{ \agentConcrete{C}{j}[90] @@ -505,7 +518,7 @@ the \textit{Concrete} agent to both the attributes of the \textit{Linear} \end{figure} % Concrete >< MulCheckLinear -\begin{figure}[ht] +\begin{figure}[H] \centering \interactionrule{ \agentConcrete{C}{j}[90] @@ -529,7 +542,7 @@ In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \text we follow the exact same logic except the first operand is a \textit{Concrete} and the second is a \textit{Linear}. % Linear >< AddCheckConcrete -\begin{figure}[ht] +\begin{figure}[H] \centering \interactionrule{ \agentLinear{L}{s}{t}[90] @@ -549,7 +562,7 @@ we follow the exact same logic except the first operand is a \textit{Concrete} a \end{figure} % Linear >< MulCheckConcrete -\begin{figure}[ht] +\begin{figure}[H] \centering \interactionrule{ \agentLinear{L}{s}{t}[90] @@ -574,7 +587,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \textbf{\Cref{fig:rule-concrete-mulcheckconcrete}} following a similar logic to the previous rules. % Concrete >< AddCheckConcrete -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \begin{tabular}{c} @@ -610,7 +623,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \end{figure} % Concrete >< MulCheckConcrete -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \begin{tabular}{c} @@ -659,7 +672,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \end{figure} \paragraph{Linear/Concrete with ReLU} -When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is no +When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is not 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}. In \textbf{\Cref{fig:rule-concrete-relu}} is illustrated that when the \textit{Concrete} carrier agent @@ -667,7 +680,7 @@ meets the \textit{ReLU} agent, a \textit{Concrete} is wired to the output either if $k>0$ or with attribute equal $0$ otherwise. % Linear >< ReLU -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \interactionrule{ @@ -693,7 +706,7 @@ if $k>0$ or with attribute equal $0$ otherwise. \end{figure} % Concrete >< ReLU -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \begin{tabular}{c} @@ -729,13 +742,13 @@ if $k>0$ or with attribute equal $0$ otherwise. \end{figure} \paragraph{Linear/Concrete with Materialize} -When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd} and \textit{TermMul} +When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd}, \textit{TermMul} and \textit{TermConcrete} 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 +When a \textit{Concrete} needs to be materialized it is converted into \textit{TermConcrete} as illustrated in \textbf{\Cref{fig:rule-concrete-materialize}}. % Linear >< Materialize -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \begin{tabular}{c} @@ -750,8 +763,8 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i }{ \agentTermAdd{TA}[90] \agentTermMul[left=of TA.pax 1]{TM}[90] - \agentConcrete[left=of TA.pax 2, below=of TM]{C1}{r}[90] - \agentConcrete[left=of TM.pax 1]{C2}{q}[90] + \agentTermConcrete[left=of TA.pax 2, below=of TM]{C1}{r}[90] + \agentTermConcrete[left=of TM.pax 1]{C2}{q}[90] \inetwire(TA.pax 1)(TM.pal) \inetwire(TA.pax 2)(C1.pal) \inetwire(TM.pax 1)(C2.pal) \inetwirefree(TA.pal) \inetwirefree(TM.pax 2) \node [left] at (TM.above pax 2) {$\mathit{x}$}; @@ -767,7 +780,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \node [left] at (L.above pax) {$\mathit{x}$}; \node [right] at (MAT.above pax) {$\mathit{out}$}; }{ - \agentConcrete{C}{r}[90] + \agentTermConcrete{C}{r}[90] \agentEraser[below=of C]{E}[90] \inetwirefree(C.pal) \inetwirefree(E.pal) \node [right] at (C.above pal) {$\mathit{out}$}; @@ -798,7 +811,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \node [right] at (MAT.above pax) {$\mathit{out}$}; }{ \agentTermAdd{TA}[90] - \agentConcrete[left=of TA.right pax]{C}{r}[90] + \agentTermConcrete[left=of TA.right pax]{C}{r}[90] \inetwire(C.pal)(TA.pax 2) \inetwirefree(TA.pax 1) \inetwirefree(TA.pal) \node [left] at (TA.above pax 1) {$\mathit{x}$}; @@ -815,7 +828,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \node [right] at (MAT.above pax) {$\mathit{out}$}; }{ \agentTermMul{TM}[90] - \agentConcrete[left=of TM.left pax]{C}{q}[90] + \agentTermConcrete[left=of TM.left pax]{C}{q}[90] \inetwire(C.pal)(TM.pax 1) \inetwirefree(TM.pax 2) \inetwirefree(TM.pal) \node [left] at (TM.above pax 2) {$\mathit{x}$}; @@ -828,7 +841,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \end{figure} % Concrete >< Materialize -\begin{figure}[ht] +\begin{figure}[H] \centering \resizebox{\textwidth}{!}{ \interactionrule{ @@ -838,7 +851,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \inetwirefree(MAT.pax) \node [right] at (MAT.above pax) {$\mathit{out}$}; }{ - \agentConcrete{C}{k}[90] + \agentTermConcrete{C}{k}[90] \inetwirefree(C.pal) \node [right] at (C.above pal) {$\mathit{out}$}; } diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex index 638ff17..0a2eec0 100644 --- a/chapters/core/implementation/03-translation.tex +++ b/chapters/core/implementation/03-translation.tex @@ -11,15 +11,7 @@ to be able to instantiate the correct number of \textit{Dup} agents. The main al 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] +\begin{algorithm}[H] \caption{Backwards ONNX-to-IN Translation} \label{alg:onnx-to-in} \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} @@ -67,22 +59,31 @@ agents together: in the \textit{Fan-In} the principal port of the agents are fac $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))$ + $S.\text{append}(sink \sim \text{Linear}(\text{TermSymbolic}(x), 1.0, 0.0))$ + } + + \ForEach{$y$ in $\text{len}(interactions[G.output])$}{ + $S.\text{append}(result_y)$ } \Return{S} \end{algorithm} -\begin{algorithm}[ht] +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}[H] \caption{Balanced Fan-In} \label{alg:balanced-fan-in} \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} @@ -111,8 +112,7 @@ agents together: in the \textit{Fan-In} the principal port of the agents are fac \Return{$T[0]$} \end{algorithm} - -\begin{algorithm}[ht] +\begin{algorithm}[H] \caption{Balanced Fan-Out} \label{alg:balanced-fan-out} \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} diff --git a/chapters/core/soundness-proof/01-mathematical-definitions.tex b/chapters/core/soundness-proof/01-mathematical-definitions.tex index 19059ad..4bcb9df 100644 --- a/chapters/core/soundness-proof/01-mathematical-definitions.tex +++ b/chapters/core/soundness-proof/01-mathematical-definitions.tex @@ -27,10 +27,18 @@ The agents are defined as: 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$\\ + \item $\llbracket \mathit{TermAdd}(a, b) \sim \mathit{out} \rrbracket \iff \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$\\ + \item $\llbracket \mathit{TermMul}(a, b) \sim \mathit{out} \rrbracket \iff \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. + \item $\llbracket \mathit{TermSymbolic}(id) \sim \mathit{out} \rrbracket \iff \mathit{out} = x_{id}$\\ + where $\mathit{out}$ is a wire and $id$ is a variable identifier. + \item $\llbracket \mathit{TermConcrete}(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{Dup}(x, y) \sim z \rrbracket \iff z = x = y$\\ + where $x, y, z$ are wires. + \item $\llbracket \mathit{Eraser} \sim x \rrbracket \iff x \in \mathbb{R}$\\ + where $x$ is a wire. \textit{Eraser} effectively removes any constraints. \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 6764ea2..800e085 100644 --- a/chapters/core/soundness-proof/02-soundness-of-translation.tex +++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex @@ -3,7 +3,7 @@ We need to prove that for each ONNX operator a semantically equivalent IN is produced. -\paragraph{ReLU} +\begin{lemma} The ONNX ReLU operator for an input tensor X and output tensor Y is defined as: $$ Y = \max(0, X) @@ -17,8 +17,9 @@ $$ \llbracket \mathit{ReLU}(y_i) \sim x_i \rrbracket \Rightarrow y_i = \max(0, x_i) $$ Which is identical to the ONNX definition. +\end{lemma} -\paragraph{Gemm} +\begin{lemma} The ONNX Gemm (General Matrix Multiplication) operator for input tensors A, B, C, input $\alpha$ and $\beta$ and output tensor Y is defined as: $$ @@ -40,15 +41,4 @@ $$ \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. +\end{lemma} 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 2336135..be0870d 100644 --- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex +++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex @@ -1,507 +1,849 @@ \subsection{Soundness of Interaction Rules} \label{sec:soundness-of-interaction-rules} -\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. +\begin{lemma} + 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. +\end{lemma} -\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} +\begin{lemma} + 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} -\end{aligned} -$$ -Since: -$$ -\begin{cases} - 0 + b = b & \text{if } k = 0 \\ - k + b = k + b & \text{otherwise} -\end{cases} -$$ -the rule is sound. + $$ + Since $(q \cdot x + r) \cdot b = q \cdot b \cdot x + r \cdot b$, the rule is sound. +\end{lemma} -\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} +\begin{lemma} + 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} -\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. + $$ + Since: + $$ + \begin{cases} + 0 + b = b & \text{if } k = 0 \\ + k + b = k + b & \text{otherwise} + \end{cases} + $$ + the rule is sound. +\end{lemma} -\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) +\begin{lemma} + 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} - & \text{otherwise} + \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} -\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 \\ + $$ + the rule is sound. +\end{lemma} + +\begin{lemma} + 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} - & \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} + & \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} -\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) + $$ + 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} - & \text{otherwise} + \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} -\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 \\ + $$ + the rule is sound. +\end{lemma} + +\begin{lemma} + 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} - & \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} + & \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} -\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. + $$ + 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. +\end{lemma} -\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. +\begin{lemma} + 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. +\end{lemma} -\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. +\begin{lemma} + 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. +\end{lemma} -\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. +\begin{lemma} + 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. +\end{lemma} -\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} +\begin{lemma} + 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} -\end{aligned} -$$ -Since: -$$ -\begin{cases} - k + 0 = k & \text{if } j = 0 \\ - k + j = k + j & \text{otherwise} -\end{cases} -$$ -the rule is sound. + $$ + Since $k \cdot (s \cdot y + t) = (s \cdot k) \cdot y + (t \cdot k)$, the rule is sound. +\end{lemma} -\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} +\begin{lemma} + 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} -\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. + $$ + Since: + $$ + \begin{cases} + k + 0 = k & \text{if } j = 0 \\ + k + j = k + j & \text{otherwise} + \end{cases} + $$ + the rule is sound. +\end{lemma} -\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. +\begin{lemma} + 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. +\end{lemma} -\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} +\begin{lemma} + 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}(x, q, 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} -\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. + $$ + Since $\max(0, q \cdot x + r) = 1 \cdot \max(0, q \cdot x + r) + 0$ the rule is sound. +\end{lemma} -\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} +\begin{lemma} + 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} -\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} \\ + $$ + the rule is sound. +\end{lemma} + +\begin{lemma} + 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{TermConcrete}(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{TermConcrete}(r)) & \text{if } q = 1 \\ + \mathit{out} \sim \mathit{TermMul}(\mathit{TermConcrete}(q), x) & \text{if } r = 0 \\ + \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(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. + $$ + 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{TermConcrete}(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{TermConcrete}(r)) \rrbracket \Rightarrow \mathit{out} = x + r & \text{if } q = 1 \\ + \llbracket \mathit{out} \sim \mathit{TermMul}(\mathit{TermConcrete}(q), x) \rrbracket \Rightarrow \mathit{out} = q \cdot x & \text{if } r = 0 \\ + \llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(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. +\end{lemma} -\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. +\begin{lemma} + For the \textit{Concrete} and \textit{Materialize} agents we have the interaction rule: + $$ + \mathit{Concrete}(k) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \mathit{TermConcrete}(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{TermConcrete}(k) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = k + \end{aligned} + \end{aligned} + $$ + Since $k = k$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{Linear} and \textit{Dup} agents we have the interaction rule: + $$ + \mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{Linear}(z_1, q, r) \sim x; \mathit{Linear}(z_2, q, r) \sim y; \mathit{Dup}(z_1, z_2) \sim z \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(z, q, r) \sim w \rrbracket \Rightarrow z\cdot q + r = w \\ + & \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\ + & \Rightarrow z \cdot q + r = x = y + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(z_1, q, r) \sim x \rrbracket \Rightarrow z_1 \cdot q + r = x \\ + & \llbracket \mathit{Linear}(z_2, q, r) \sim y \rrbracket \Rightarrow z_2 \cdot q + r = y \\ + & \llbracket \mathit{Dup}(z_1, z_2) \sim z \rrbracket \Rightarrow z = z_1 = z_2 \\ + & \Rightarrow z \cdot q + r = x \land z \cdot q + r = y + \end{aligned} + \end{aligned} + $$ + Since $z \cdot q + r = x = y \iff z \cdot q + r = x \land z \cdot q + r = y$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{Linear} and \textit{Eraser} agents we have the interaction rule: + $$ + \mathit{Linear}(x, q, r) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\ + $$ + 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 x\cdot q + r = w \\ + & \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\ + & \Rightarrow x \cdot q + r \in \mathbb{R} + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Eraser} \sim x \rrbracket \\ + & \Rightarrow x \in \mathbb{R} + \end{aligned} + \end{aligned} + $$ + Since $x \cdot q + r \in \mathbb{R} \iff x \in \mathbb{R}$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{Concrete} and \textit{Dup} agents we have the interaction rule: + $$ + \mathit{Concrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{Concrete}(k) \sim x; \mathit{Concrete}(k) \sim y \\ + $$ + 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{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\ + & \Rightarrow k = x = y + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Concrete}(k) \sim x \rrbracket \Rightarrow k = x \\ + & \llbracket \mathit{Concrete}(k) \sim y \rrbracket \Rightarrow k = y \\ + & \Rightarrow k = x \land k = y + \end{aligned} + \end{aligned} + $$ + Since $k = x = y \iff k = x \land k = y$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{Concrete} and \textit{Eraser} agents we have the interaction rule: + $$ + \mathit{Concrete}(k) \bowtie \mathit{Eraser} \Rightarrow \\ + $$ + 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{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\ + & \Rightarrow k \in \mathbb{R} + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \end{aligned} + \end{aligned} + $$ + Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermAdd} and \textit{Dup} agents we have the interaction rule: + $$ + \begin{aligned} + \mathit{TermAdd}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow & \mathit{TermAdd}(a_1, b_1) \sim x; \mathit{TermAdd}(a_2, b_2) \sim y; \\ + & \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b\\ + \end{aligned} + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermAdd}(a, b) \sim w \rrbracket \Rightarrow a + b = w \\ + & \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\ + & \Rightarrow a + b = x = y + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{TermAdd}(a_1, b_1) \sim x \rrbracket \Rightarrow a_1 + b_1 = x \\ + & \llbracket \mathit{TermAdd}(a_2, b_2) \sim y \rrbracket \Rightarrow a_2 + b_2 = y \\ + & \llbracket \mathit{Dup}(a_1, a_2) \sim a \rrbracket \Rightarrow a = a_1 = a_2 \\ + & \llbracket \mathit{Dup}(b_1, b_2) \sim b \rrbracket \Rightarrow b = b_1 = b_2 \\ + & \Rightarrow a + b = x \land a + b = y + \end{aligned} + \end{aligned} + $$ + Since $a + b = x = y \iff a + b = x \land a + b = y$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermAdd} and \textit{Eraser} agents we have the interaction rule: + $$ + \mathit{TermAdd}(a, b) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim a; \mathit{Eraser} \sim b \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermAdd}(a, b) \sim w \rrbracket \Rightarrow a + b = w \\ + & \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\ + & \Rightarrow a + b \in \mathbb{R} + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Eraser} \sim a \rrbracket \Rightarrow a \in \mathbb{R} \\ + & \llbracket \mathit{Eraser} \sim b \rrbracket \Rightarrow b \in \mathbb{R} \\ + & \Rightarrow a \in \mathbb{R} \land b \in \mathbb{R} + \end{aligned} + \end{aligned} + $$ + Since $a + b \in \mathbb{R} \iff a \in \mathbb{R} \land b \in \mathbb{R}$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermMul} and \textit{Dup} agents we have the interaction rule: + $$ + \begin{aligned} + \mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow & \mathit{TermMul}(a_1, b_1) \sim x; \mathit{TermMul}(a_2, b_2) \sim y; \\ + & \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b\\ + \end{aligned} + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermMul}(a, b) \sim w \rrbracket \Rightarrow a \cdot b = w \\ + & \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\ + & \Rightarrow a \cdot b = x = y + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{TermMul}(a_1, b_1) \sim x \rrbracket \Rightarrow a_1 \cdot b_1 = x \\ + & \llbracket \mathit{TermMul}(a_2, b_2) \sim y \rrbracket \Rightarrow a_2 \cdot b_2 = y \\ + & \llbracket \mathit{Dup}(a_1, a_2) \sim a \rrbracket \Rightarrow a = a_1 = a_2 \\ + & \llbracket \mathit{Dup}(b_1, b_2) \sim b \rrbracket \Rightarrow b = b_1 = b_2 \\ + & \Rightarrow a \cdot b = x \land a \cdot b = y + \end{aligned} + \end{aligned} + $$ + Since $a \cdot b = x = y \iff a \cdot b = x \land a \cdot b = y$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermMul} and \textit{Eraser} agents we have the interaction rule: + $$ + \mathit{TermMul}(a, b) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim a; \mathit{Eraser} \sim b \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermMul}(a, b) \sim w \rrbracket \Rightarrow a \cdot b = w \\ + & \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\ + & \Rightarrow a \cdot b \in \mathbb{R} + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Eraser} \sim a \rrbracket \Rightarrow a \in \mathbb{R} \\ + & \llbracket \mathit{Eraser} \sim b \rrbracket \Rightarrow b \in \mathbb{R} \\ + & \Rightarrow a \in \mathbb{R} \land b \in \mathbb{R} + \end{aligned} + \end{aligned} + $$ + Since $a \cdot b \in \mathbb{R} \iff a \in \mathbb{R} \land b \in \mathbb{R}$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule: + $$ + \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermReLU}(z_1) \sim x; \mathit{TermReLU}(z_2) \sim y; \mathit{Dup}(z_1, z_2) \sim z \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermReLU}(z) \sim w \rrbracket \Rightarrow \max(0, z) = w \\ + & \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\ + & \Rightarrow \max(0, z) = x = y + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{TermReLU}(z_1) \sim x \rrbracket \Rightarrow \max(0, z_1) = x \\ + & \llbracket \mathit{TermReLU}(z_2) \sim y \rrbracket \Rightarrow \max(0, z_2) = y \\ + & \llbracket \mathit{Dup}(z_1, z_2) \sim z \rrbracket \Rightarrow z = z_1 = z_2 \\ + & \Rightarrow \max(0, z) = x \land \max(0, z) = y + \end{aligned} + \end{aligned} + $$ + Since $\max(0, z) = x = y \iff \max(0, z) = x \land \max(0, z) = y$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermReLU} and \textit{Eraser} agents we have the interaction rule: + $$ + \mathit{TermReLU}(x) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermReLU}(x) \sim w \rrbracket \Rightarrow \max(0, x) = w \\ + & \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\ + & \Rightarrow \max(0, x) \in \mathbb{R} + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Eraser} \sim x \rrbracket \\ + & \Rightarrow x \in \mathbb{R} + \end{aligned} + \end{aligned} + $$ + Since $\max(0, x) \in \mathbb{R} \iff x \in \mathbb{R}$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule: + $$ + \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermConcrete}(k) \sim x; \mathit{TermConcrete}(k) \sim y \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermConcrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\ + & \Rightarrow k = x = y + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{TermConcrete}(k) \sim x \rrbracket \Rightarrow k = x \\ + & \llbracket \mathit{TermConcrete}(k) \sim y \rrbracket \Rightarrow k = y \\ + & \Rightarrow k = x \land k = y + \end{aligned} + \end{aligned} + $$ + Since $k = x = y \iff k = x \land k = y$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermConcrete} and \textit{Eraser} agents we have the interaction rule: + $$ + \mathit{TermConcrete}(k) \bowtie \mathit{Eraser} \Rightarrow \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermConcrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\ + & \Rightarrow k \in \mathbb{R} + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \end{aligned} + \end{aligned} + $$ + Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule: + $$ + \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermSymbolic}(id) \sim x; \mathit{TermSymbolic}(id) \sim y \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermSymbolic}(id) \sim w \rrbracket \Rightarrow x_{id} = w \\ + & \llbracket \mathit{Dup}(x, y) \sim w \rrbracket \Rightarrow w = x = y \\ + & \Rightarrow x_{id} = x = y + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{TermSymbolic}(id) \sim x \rrbracket \Rightarrow x_{id} = x \\ + & \llbracket \mathit{TermSymbolic}(id) \sim y \rrbracket \Rightarrow x_{id} = y \\ + & \Rightarrow x_{id} = x \land x_{id} = y + \end{aligned} + \end{aligned} + $$ + Since $x_{id} = x = y \iff x_{id} = x \land x_{id} = y$, the rule is sound. +\end{lemma} + +\begin{lemma} + For the \textit{TermSymbolic} and \textit{Eraser} agents we have the interaction rule: + $$ + \mathit{TermSymbolic}(id) \bowtie \mathit{Eraser} \Rightarrow \\ + $$ + We need to show that the LHS and RHS are semantically equivalent: + $$ + \begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{TermSymbolic}(id) \sim w \rrbracket \Rightarrow x_{id} = w \\ + & \llbracket \mathit{Eraser} \sim w \rrbracket \Rightarrow w \in \mathbb{R} \\ + & \Rightarrow x_{id} \in \mathbb{R} + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \end{aligned} + \end{aligned} + $$ + Since $x_{id} \in \mathbb{R}$ is not violated by RHS, the rule is sound. +\end{lemma} diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex index b0a7906..d0cec53 100644 --- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex +++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex @@ -1,28 +1,117 @@ \subsection{Soundness of Reduction} \label{sec:soundness-of-reduction} -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 -$$ +\begin{lemma} + A valid IN satisfies the following properties: + \begin{itemize} + \item \textbf{DAG}: the net forms a DAG where the roots are the free wires representing the network + outputs. + \item \textbf{Orientation}: carrier agents always have their principal ports oriented toward the outputs, + while operator and intermediate agents always have their principal ports oriented toward the + inputs. No interaction rule introduces carriers facing the input nor operators or + intermediates facing the output. + \item \textbf{Restricted Interaction}: the net is constructed such that active pairs only occur between a + carrier agent and an operator/intermediate agent. Because of \textbf{Orientation}, neither + carrier nor operator agents interact with agents of the same type. Terminal agents do not + interact with computational operators because they are wrapped in a \textit{Linear} agent. + \end{itemize} +\end{lemma} -\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}$. +\begin{theorem} + Let $\text{IN}_0$ be the valid IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be + the IN after $n$ reduction steps, then: + \begin{equation} + \forall n \in \mathbb{N} \quad \llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket + \end{equation} +\end{theorem} -\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 -$$ +\begin{proof} + We will proceed by induction on the number $n$ of reduction steps: + \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}$, it follows that: + \begin{equation} + \llbracket \text{IN}_{0} \rrbracket = \llbracket \text{NN} \rrbracket + \end{equation} -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. + \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: + \begin{equation} + \llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{IN}_{n} \rrbracket + \end{equation} + By the inductive hypothesis: + \begin{equation} + \llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{NN} \rrbracket + \end{equation} + By the principle of mathematical induction, $\text{IN}_n$ remains semantically equivalent to the + original $\text{NN}$ at every step of the reduction process. +\end{proof} + +\begin{theorem} + For any valid $\text{IN}_0$ translated from a neural network $\text{NN}$, the reduction process + $\text{IN}_0 \to \text{IN}_1 \to \dots \to \text{IN}_n$ reaches a unique normal form, an IN with no active pair, in a + finite number of steps $n$. +\end{theorem} + +\begin{proof} + We define a potential function $\Phi$. We need to show that: + \begin{equation} + \Phi(\text{IN}_n) > \Phi(\text{IN}_{n+1}) \quad \forall n \in \mathbb{N} + \end{equation} + The potential function is defined as: + \begin{equation} + \Phi(\text{IN}_n) = \sum_{a \in \text{Agents}(\text{IN}_n)} \begin{cases} + 4 + 3^{D-d(a)} & \text{ if }a\text{ is of type computational operator} \\ + 3 + 3^{D-d(a)} & \text{ if }a\text{ is of type intermediate} \\ + 1 + 3^{D-d(a)} & \text{ if }a\text{ is a Materialize agent} \\ + 3^{D-d(a)} & \text{ if }a\text{ is of type structural operator} \\ + 0 & \text{ if }a\text{ is a Carrier, Terminal} + \end{cases} + \end{equation} + where $d(a)$ is the distance of the agent $a$ from the nearest output wire and $D$ the maximum depth + of $\text{IN}_0$, + We observe that every reduction step $n \to n+1$ strictly reduces $\Phi$: + \begin{itemize} + \item \textbf{Carrier with Computational Operator}: If a carrier $c$ interacts with an operator agent $o$, it + either gets pruned into a new carrier agent closer to the root: + \begin{equation} + \Phi(\text{IN}_n) = 4 + 3^{D-d(c)} > 0 = \Phi(\text{IN}_{n+1}) + \end{equation} + or absorbed into an intermediate agent: + \begin{equation} + \Phi(\text{IN}_n) = 4 + 3^{D-d(c)} > 3 + 3^{D-d(c)} = \Phi(\text{IN}_{n+1}) + \end{equation} + \item \textbf{Carrier with Intermediate}: If a carrier $c$ interacts with an intermediate agent $i$, it + either gets pruned into a new carrier agent closer to the root: + \begin{equation} + \Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1}) + \end{equation} + or temporary Linear agents are wired with Materialize agents, which are then forced to + interact to produce terminal agents, then wrapped into a new Linear agent: + \begin{equation} + \Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 1 + 3^{D-d(i)-2} + 1 + 3^{D-d(i)-2} = 2 + 2 \cdot 3^{D-d(i)-2} = \Phi(\text{IN}_{n+1}) + \end{equation} + If the carrier $c$ interacts with a Materialize agent $i$: + \begin{equation} + \Phi(\text{IN}_n) = 1 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1}) + \end{equation} + \item \textbf{Carrier with Structural Operator}: If a carrier $c$ is duplicated with the \textit{Dup} or \textit{Eraser} + agent $a$, it traverses the agent structure: + \begin{equation} + \Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1}) + \end{equation} + if the Dup or Eraser agent interacts with a TermAdd or TermMul, two new agents are created at + each auxillary port: + \begin{equation} + \Phi(\text{IN}_n) = 3^{D-d(a)} > 2 * 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1}) + \end{equation} + \end{itemize} + Since $\Phi$ is a non-negative strictly decreasing function, the reduction + process must terminate in a finite number of steps $n$. + + Additionally, since each active pair has exactly one applicable rule the reduction is + deterministic. Strong confluence follows immediately, meaning that the normal form is unique + regardless of order in which rules are applied. +\end{proof} -- cgit v1.2.3