diff options
Diffstat (limited to 'chapters/core/soundness-proof')
4 files changed, 613 insertions, 4 deletions
diff --git a/chapters/core/soundness-proof/01-mathematical-definitions.tex b/chapters/core/soundness-proof/01-mathematical-definitions.tex index 3d8c031..19059ad 100644 --- a/chapters/core/soundness-proof/01-mathematical-definitions.tex +++ b/chapters/core/soundness-proof/01-mathematical-definitions.tex @@ -1,4 +1,36 @@ \subsection{Mathematical Definitions} \label{sec:mathematical-definitions} -% This subsection contains the mathematical definitions used in the proof +We define the semantic function $\llbracket \cdot \rrbracket$. This function maps the state of an IN +to its equivalent mathematical interpretation. Wires and attributes in IN are mapped respectively to +free variables and real numbers in the mathematical interpretation. + +The agents are defined as: +\begin{itemize} + \item $\llbracket \mathit{Linear}(x, q, r) \sim \mathit{out} \rrbracket \iff \mathit{out} = q \cdot x + r $\\ + where $x, \mathit{out}$ are wires and $q, r \in \mathbb{R}$ are attributes. + \item $\llbracket \mathit{Concrete}(k) \sim \mathit{out} \rrbracket \iff \mathit{out} = k$\\ + where $\mathit{out}$ is a wire and $k \in \mathbb{R}$ is an attribute. + \item $\llbracket \mathit{Add}(\mathit{out}, b) \sim a \rrbracket \iff \mathit{out} = a + b$\\ + where $a, b, \mathit{out}$ are wires. + \item $\llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \iff \mathit{out} = q \cdot x + (r + b)$\\ + where $x, b, \mathit{out}$ are wires and $q, r \in \mathbb{R}$ are attributes. + \item $\llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \iff \mathit{out} = k + b$\\ + where $b, \mathit{out}$ are wires and $k \in \mathbb{R}$ is an attribute. + \item $\llbracket \mathit{Mul}(\mathit{out}, b) \sim a \rrbracket \iff \mathit{out} = a \cdot b$\\ + where $a, b, \mathit{out}$ are wires. + \item $\llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \iff \mathit{out} = q \cdot b \cdot x + r \cdot b$\\ + where $x, b, \mathit{out}$ are wires and $q, r \in \mathbb{R}$ are attributes. + \item $\llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \iff \mathit{out} = k \cdot b$\\ + where $b, \mathit{out}$ are wires and $k \in \mathbb{R}$ is an attribute. + \item $\llbracket \mathit{ReLU}(\mathit{out}) \sim x \rrbracket \iff \mathit{out} = \max(0, x)$\\ + where $x, \mathit{out}$ are wires. + \item $\llbracket \mathit{Materialize}(\mathit{out}) \sim x \rrbracket \iff \mathit{out} = x$\\ + where $x, \mathit{out}$ are wires. + \item $\llbracket \mathit{TermAdd}(a, b) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = a + b$\\ + where $a, b, \mathit{out}$ are wires. + \item $\llbracket \mathit{TermMul}(a, b) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = a \cdot b$\\ + where $a, b, \mathit{out}$ are wires. + \item $\llbracket \mathit{TermReLU}(x) \sim \mathit{out} \rrbracket \iff \mathit{out} = \max(0, x)$\\ + where $x, \mathit{out}$ are wires. +\end{itemize} diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex index f112aa5..6764ea2 100644 --- a/chapters/core/soundness-proof/02-soundness-of-translation.tex +++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex @@ -1,4 +1,54 @@ \subsection{Soundness of Translation} \label{sec:soundness-of-translation} -% This subsection gives the proof for ONNX-to-Inpla translation soundness +We need to prove that for each ONNX operator a semantically equivalent IN is produced. + +\paragraph{ReLU} +The ONNX ReLU operator for an input tensor X and output tensor Y is defined as: +$$ +Y = \max(0, X) +$$ +The translation layer produces, for each neuron, the interaction: +$$ +\mathit{ReLU}(y_i) \sim x_i +$$ +Applying the semantic function: +$$ +\llbracket \mathit{ReLU}(y_i) \sim x_i \rrbracket \Rightarrow y_i = \max(0, x_i) +$$ +Which is identical to the ONNX definition. + +\paragraph{Gemm} +The ONNX Gemm (General Matrix Multiplication) operator for input tensors A, B, C, input $\alpha$ +and $\beta$ and output tensor Y is defined as: +$$ +Y = \alpha \cdot A \cdot B + \beta \cdot C +$$ +The translation layer produces, for each neuron, the interactions: +$$ +\mathit{Mul}(v_i, \mathit{Concrete}(\alpha \cdot b_{j, i})) \sim a_i +$$ +And for each layer: +$$ +\mathit{Add}(\dots(\mathit{Add}(y_j, v_1),\dots), v_n) \sim \mathit{Concrete}(\beta \cdot c_j) +$$ +Applying the semantic function: +$$ +\begin{aligned} + \llbracket \mathit{Mul}(v_i, \mathit{Concrete}(\alpha \cdot b_{j, i})) \sim a_i \rrbracket \Rightarrow v_i = \alpha \cdot a_i \cdot b_{j, i}\\ + \llbracket \mathit{Add}(\dots(\mathit{Add}(y_j, v_1),\dots), v_n) \sim \mathit{Concrete}(\beta \cdot c_j) \rrbracket \Rightarrow y_j = \sum_{i=1}^n v_i + \beta \cdot c_j +\end{aligned} +$$ +By substituting $v_i$, the result matches the ONNX definition. + +\paragraph{Identity} +The ONNX Identity does not modify the numerical values of the tensors. As this operator results in a +direct wire connection: +$$ +y_i \sim x_i +$$ +The semantic: +$$ +\llbracket y_i \sim x_i \rrbracket \Rightarrow y_i = x_i +$$ +trivially preserve the identity mapping. diff --git a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex index 9aa84ac..2336135 100644 --- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex +++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex @@ -1,4 +1,507 @@ \subsection{Soundness of Interaction Rules} \label{sec:soundness-of-interaction-rules} -% This subsections gives the proof for each interaction rule +\paragraph{Linear and Add} +For the \textit{Linear} and \textit{Add} agents we have the interaction rule: +$$ +\mathit{Linear}(x, q, r) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\ + & \llbracket \mathit{Add}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w + b \\ + & \Rightarrow \mathit{out} = (q \cdot x + r) + b + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \\ + & \Rightarrow \mathit{out} = q \cdot x + (r + b) + \end{aligned} +\end{aligned} +$$ +Since $(q \cdot x + r) + b = q \cdot x + (r + b)$, the rule is sound. + +\paragraph{Linear and Mul} +For the \textit{Linear} and \textit{Mul} agents we have the interaction rule: +$$ +\mathit{Linear}(x, q, r) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\ + & \llbracket \mathit{Mul}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w \cdot b \\ + & \Rightarrow \mathit{out} = (q \cdot x + r) \cdot b + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \rrbracket \\ + & \Rightarrow \mathit{out} = q \cdot b \cdot x + r \cdot b + \end{aligned} +\end{aligned} +$$ +Since $(q \cdot x + r) \cdot b = q \cdot b \cdot x + r \cdot b$, the rule is sound. + +\paragraph{Concrete and Add} +For the \textit{Concrete} and \textit{Add} agents we have the interaction rule: +$$ +\mathit{Concrete}(k) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow +\begin{cases} + \mathit{out} \sim b & \text{if } k = 0 \\ + \mathit{AddCheckConcrete}(\mathit{out}, k) \sim b & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{Add}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w + b \\ + & \Rightarrow \mathit{out} = k + b + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim b \rrbracket \Rightarrow \mathit{out} = b & \text{if } k = 0 \\ + \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \Rightarrow \mathit{out} = k + b & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 + b = b & \text{if } k = 0 \\ + k + b = k + b & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Concrete and Mul} +For the \textit{Concrete} and \textit{Mul} agents we have the interaction rule: +$$ +\mathit{Concrete}(k) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow +\begin{cases} + \mathit{out} \sim \mathit{Concrete}(0); b \sim \mathit{Eraser} & \text{if } k = 0 \\ + \mathit{out} \sim b & \text{if } k = 1 \\ + \mathit{MulCheckConcrete}(\mathit{out}, k) \sim b & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{Mul}(\mathit{out}, b) \sim w \rrbracket \Rightarrow \mathit{out} = w \cdot b \\ + & \Rightarrow \mathit{out} = k \cdot b + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(0); b \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } k = 0 \\ + \llbracket \mathit{out} \sim b \rrbracket \Rightarrow \mathit{out} = b & \text{if } k = 1 \\ + \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim b \rrbracket \Rightarrow \mathit{out} = k \cdot b & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 \cdot b = 0 & \text{if } k = 0 \\ + 1 \cdot b = b & \text{if } k = 1 \\ + k \cdot b = k \cdot b & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Linear and AddCheckLinear} +For the \textit{Linear} and \textit{AddCheckLinear} agents we have the interaction rule: +$$ +\begin{aligned} + & \mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} & \text{if } q,r,s,t = 0 \\ + \mathit{out} \sim \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} & \text{if } s,t = 0 \\ + \mathit{out} \sim \mathit{Linear}(y, s, t); x \sim \mathit{Eraser} & \text{if } q,r = 0 \\ + \begin{aligned} + & \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\ + & \mathit{Linear}(y, s, t) \sim \mathit{Materialize}(\mathit{out}_y); \\ + & \mathit{out} \sim \mathit{Linear}(\mathit{TermAdd}(\mathit{out}_x, \mathit{out}_y), 1, 0) + \end{aligned} + & \text{otherwise} + \end{cases} +\end{aligned} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\ + & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\ + & \Rightarrow \mathit{out} = q \cdot x + (r + s \cdot y + t) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r,s,t = 0 \\ + \llbracket \mathit{out} \sim \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{if } s,t = 0 \\ + \llbracket \mathit{out} \sim \mathit{Linear}(y, s, t); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = s \cdot y + t & \text{if } q,r = 0 \\ + \begin{aligned} + & \llbracket \mathit{Linear}(x, q, r) \sim w_1 \rrbracket \Rightarrow w_1 = q \cdot x + r \\ + & \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w_1 \rrbracket \Rightarrow \mathit{out}_x = w_1 \\ + & \llbracket \mathit{Linear}(y, s, t) \sim w_2 \rrbracket \Rightarrow w_2 = s \cdot y + t \\ + & \llbracket \mathit{Materialize}(\mathit{out}_y) \sim w_2 \rrbracket \Rightarrow \mathit{out}_y = w_2 \\ + & \llbracket \mathit{Linear}(\mathit{TermAdd}(\mathit{out}_x, \mathit{out}_y), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot (\mathit{out}_x + \mathit{out}_y) + 0 + \end{aligned}\\ + \Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 \cdot x + (0 + 0 \cdot y + 0) = 0 & \text{if } q,r,s,t = 0 \\ + q \cdot x + (r + 0 \cdot y + 0) = q \cdot x + r & \text{if } s,t = 0 \\ + 0 \cdot x + (0 + s \cdot y + t) = s \cdot y + t & \text{if } q,r = 0 \\ + q \cdot x + (r + s \cdot y + t) = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Linear and MulCheckLinear} +For the \textit{Linear} and \textit{MulCheckLinear} agents we have the interaction rule: +$$ +\begin{aligned} + & \mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} & \text{if } q,r = 0 \lor s,t = 0 \\ + \begin{aligned} + & \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); \\ + & \mathit{Linear}(y, s, t) \sim \mathit{Materialize}(\mathit{out}_y); \\ + & \mathit{out} \sim \mathit{Linear}(\mathit{TermMul}(\mathit{out}_x, \mathit{out}_y), 1, 0) + \end{aligned} + & \text{otherwise} + \end{cases} +\end{aligned} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\ + & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\ + & \Rightarrow \mathit{out} = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r = 0 \lor s,t = 0 \\ + \begin{aligned} + & \llbracket \mathit{Linear}(x, q, r) \sim w_1 \rrbracket \Rightarrow w_1 = q \cdot x + r \\ + & \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w_1 \rrbracket \Rightarrow \mathit{out}_x = w_1 \\ + & \llbracket \mathit{Linear}(y, s, t) \sim w_2 \rrbracket \Rightarrow w_2 = s \cdot y + t \\ + & \llbracket \mathit{Materialize}(\mathit{out}_y) \sim w_2 \rrbracket \Rightarrow \mathit{out}_y = w_2 \\ + & \llbracket \mathit{Linear}(\mathit{TermMul}(\mathit{out}_x, \mathit{out}_y), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot \mathit{out}_x \cdot \mathit{out}_y + 0 + \end{aligned}\\ + \Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 \cdot (s \cdot y + t) \cdot x + 0 \cdot (s \cdot y + t) = 0 \lor q \cdot (0 \cdot y + 0) \cdot x + r \cdot (0 \cdot y + 0) = 0 & \text{if } q,r = 0 \lor s,t = 0 \\ + 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Concrete and AddCheckLinear} +For the \textit{Concrete} and \textit{AddCheckLinear} agents we have the interaction rule: +$$ +\mathit{Concrete}(j) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q, r + j) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\ + & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\ + & \Rightarrow \mathit{out} = q \cdot x + (r + j) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(x, q, r + j) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = q \cdot x + (r + j) + \end{aligned} +\end{aligned} +$$ +Since $q \cdot x + (r + j) = q \cdot x + (r + j)$, the rule is sound. + +\paragraph{Concrete and MulCheckLinear} +For the \textit{Concrete} and \textit{MulCheckLinear} agents we have the interaction rule: +$$ +\mathit{Concrete}(j) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\ + & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\ + & \Rightarrow \mathit{out} = q \cdot j \cdot x + r \cdot j + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = (q \cdot j) \cdot x + (r \cdot j) + \end{aligned} +\end{aligned} +$$ +Since $q \cdot j \cdot x + r \cdot j = (q \cdot j) \cdot x + (r \cdot j)$, the rule is sound. + +\paragraph{Linear and AddCheckConcrete} +For the \textit{Linear} and \textit{AddCheckConcrete} agents we have the interaction rule: +$$ +\mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s, t + k) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\ + & \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k + w \\ + & \Rightarrow \mathit{out} = k + (s \cdot y + t) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(y, s, t + k) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = s \cdot y + (t + k) + \end{aligned} +\end{aligned} +$$ +Since $k + (s \cdot y + t) = s \cdot y + (t + k)$, the rule is sound. + +\paragraph{Linear and MulCheckConcrete} +For the \textit{Linear} and \textit{MulCheckConcrete} agents we have the interaction rule: +$$ +\mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(y, s, t) \sim w \rrbracket \Rightarrow s \cdot y + t = w \\ + & \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k \cdot w \\ + & \Rightarrow \mathit{out} = k \cdot (s \cdot y + t) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = (s \cdot k) \cdot y + (t \cdot k) + \end{aligned} +\end{aligned} +$$ +Since $k \cdot (s \cdot y + t) = (s \cdot k) \cdot y + (t \cdot k)$, the rule is sound. + +\paragraph{Concrete and AddCheckConcrete} +For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule: +$$ +\mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow +\begin{cases} + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\ + \mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\ + & \llbracket \mathit{AddCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k + w \\ + & \Rightarrow \mathit{out} = k + j + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } j = 0 \\ + \llbracket \mathit{out} \sim \mathit{Concrete}(k + j) \rrbracket \Rightarrow \mathit{out} = k + j & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + k + 0 = k & \text{if } j = 0 \\ + k + j = k + j & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Concrete and MulCheckConcrete} +For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule: +$$ +\mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow +\begin{cases} + \mathit{out} \sim \mathit{Concrete}(0) & \text{if } j = 0 \\ + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 1 \\ + \mathit{out} \sim \mathit{Concrete}(k \cdot j) & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(j) \sim w \rrbracket \Rightarrow j = w \\ + & \llbracket \mathit{MulCheckConcrete}(\mathit{out}, k) \sim w \rrbracket \Rightarrow \mathit{out} = k \cdot w \\ + & \Rightarrow \mathit{out} = k \cdot j + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(0) \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } j = 0 \\ + \llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } j = 1 \\ + \llbracket \mathit{out} \sim \mathit{Concrete}(k \cdot j) \rrbracket \Rightarrow \mathit{out} = k \cdot j & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + k \cdot 0 = 0 & \text{if } j = 0 \\ + k \cdot 1 = k & \text{if } j = 1 \\ + k \cdot j = k \cdot j & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Linear and ReLU} +For the \textit{Linear} and \textit{ReLU} agents we have the interaction rule: +$$ +\begin{aligned} + & \mathit{Linear}(x, q, r) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow + \mathit{Linear}(x, q, r) \sim \mathit{Materialize}(\mathit{out}_x); + \mathit{out} \sim \mathit{Linear}(\mathit{TermReLU}(\mathit{out}_x), 1, 0) +\end{aligned} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(q, x, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\ + & \llbracket \mathit{ReLU}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = \max(0, w) \\ + & \Rightarrow \mathit{out} = \max(0, q \cdot x + r) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow w = q \cdot x + r \\ + & \llbracket \mathit{Materialize}(\mathit{out}_x) \sim w \rrbracket \Rightarrow \mathit{out}_x = w \\ + & \llbracket \mathit{Linear}(\mathit{TermReLU}(\mathit{out}_x), 1, 0) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = 1 \cdot \max(0, \mathit{out}_x) + 0 \\ + & \Rightarrow \mathit{out} = 1 \cdot \max(0, q \cdot x + r) + 0 + \end{aligned} +\end{aligned} +$$ +Since $\max(0, q \cdot x + r) = 1 \cdot \max(0, q \cdot x + r) + 0$ the rule is sound. + +\paragraph{Concrete and ReLU} +For the \textit{Concrete} and \textit{ReLU} agents we have the interaction rule: +$$ +\mathit{Concrete}(k) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow +\begin{cases} + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } k > 0 \\ + \mathit{out} \sim \mathit{Concrete}(0) & \text{otherwise} +\end{cases} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{ReLU}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = \max(0, w) \\ + & \Rightarrow \mathit{out} = \max(0, k) + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(k) \rrbracket \Rightarrow \mathit{out} = k & \text{if } k > 0 \\ + \llbracket \mathit{out} \sim \mathit{Concrete}(0) \rrbracket \Rightarrow \mathit{out} = 0 & \text{otherwise} + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + \max(0, k) = k & \text{if } k > 0 \\ + \max(0, k) = 0 & \text{otherwise} +\end{cases} +$$ +the rule is sound. + +\paragraph{Linear and Materialize} +For the \textit{Linear} and \textit{Materialize} agents we have the interaction rule: +$$ +\begin{aligned} + & \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(r); x \sim \mathit{Eraser} & \text{if } q = 0 \\ + \mathit{out} \sim x & \text{if } q = 1, r = 0 \\ + \mathit{out} \sim \mathit{TermAdd}(x, \mathit{Concrete}(r)) & \text{if } q = 1 \\ + \mathit{out} \sim \mathit{TermMul}(\mathit{Concrete}(q), x) & \text{if } r = 0 \\ + \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{Concrete}(q), x), \mathit{Concrete}(r)) & \text{otherwise} + \end{cases} +\end{aligned} +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Linear}(x, q, r) \sim w \rrbracket \Rightarrow q \cdot x + r = w \\ + & \llbracket \mathit{Materialize}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = w \\ + & \Rightarrow \mathit{out} = q \cdot x + r + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } + \begin{cases} + \llbracket \mathit{out} \sim \mathit{Concrete}(r); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = r & \text{if } q = 0 \\ + \llbracket \mathit{out} \sim x \rrbracket \Rightarrow \mathit{out} = x & \text{if } q = 1, r = 0 \\ + \llbracket \mathit{out} \sim \mathit{TermAdd}(x, \mathit{Concrete}(r)) \rrbracket \Rightarrow \mathit{out} = x + r & \text{if } q = 1 \\ + \llbracket \mathit{out} \sim \mathit{TermMul}(\mathit{Concrete}(q), x) \rrbracket \Rightarrow \mathit{out} = q \cdot x & \text{if } r = 0 \\ + \llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{Concrete}(q), x), \mathit{Concrete}(r)) \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{otherwise} \\ + \end{cases} + \end{aligned} +\end{aligned} +$$ +Since: +$$ +\begin{cases} + 0 \cdot x + r = r & \text{if } q = 0 \\ + 1 \cdot x + 0 = x & \text{if } q = 1, r = 0 \\ + 1 \cdot x + r = x + r & \text{if } q = 1 \\ + q \cdot x + 0 = q \cdot x & \text{if } r = 0 \\ + q \cdot x + r = q \cdot x + r & \text{otherwise} \\ +\end{cases} +$$ +the rule is sound. + +\paragraph{Concrete and Materialize} +For the \textit{Concrete} and \textit{Materialize} agents we have the interaction rule: +$$ +\mathit{Concrete}(k) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \mathit{Concrete}(k) \sim \mathit{out} \\ +$$ +We need to show that the LHS and RHS are semantically equivalent: +$$ +\begin{aligned} + & \begin{aligned} + \text{LHS: } & \llbracket \mathit{Concrete}(k) \sim w \rrbracket \Rightarrow k = w \\ + & \llbracket \mathit{Materialize}(\mathit{out}) \sim w \rrbracket \Rightarrow \mathit{out} = w \\ + & \Rightarrow \mathit{out} = k + \end{aligned} \\ + & \begin{aligned} + \text{RHS: } & \llbracket \mathit{Concrete}(k) \sim \mathit{out} \rrbracket \\ + & \Rightarrow \mathit{out} = k + \end{aligned} +\end{aligned} +$$ +Since $k = k$, the rule is sound. diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex index b2d6116..b0a7906 100644 --- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex +++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex @@ -1,4 +1,28 @@ \subsection{Soundness of Reduction} \label{sec:soundness-of-reduction} -% This subsection gives the proof that each reduction step doesn't alter the semantic +Let $\text{IN}_0$ be the IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be +the IN after $n$ reduction steps. Then we need to prove: +$$ +\forall n \in \mathbb{N} \quad \llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket +$$ + +\paragraph{Base case: $n = 0$} By \textbf{\Cref{sec:soundness-of-translation}}, the initial +$\text{IN}_0$ is constructed such that its semantics $\llbracket \text{IN}_0 \rrbracket$ exactly +match the mathematical definition of the ONNX operators in $\text{NN}$. + +\paragraph{Induction step: $n \to n + 1$} Assume $\llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket$. +If $\text{IN}_n$ is in normal form, the proof is complete. Otherwise, there exists an active pair +$A \bowtie B$ that reduces $\text{IN}_n$ to $\text{IN}_{n+1}$. By \textbf{\Cref{sec:soundness-of-interaction-rules}}, +the mathematical definition is preserved after any reduction step, it follows that: +$$ +\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{IN}_{n} \rrbracket +$$ +By the inductive hypothesis: +$$ +\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{NN} \rrbracket +$$ + +By the principle of mathematical induction, $\text{IN}_n$ remains semantically equivalent to the +original $\text{NN}$ at every step of the reduction process. Additionally, since IN are confluent, +the reduced mathematical expression is unique regardless of order in which rules are applied. |