1: \begin{definition}[Concrete Correctness Loss Function]

2:   \label{def:conc-loss}

3:   For an atomic output predicate $P$, the concrete correctness loss

4:   function, $dist_g(y, P)$, quantifies the {\em distance} from an

5:   output vector $y \in \mathbb R^e$ to $P$:

6:   \[

7:     dist_g(y, P) = \min_{q \models P} g(y, q)

8:   \]

9:   where $g: \mathbb R^d \times \mathbb R^d \mapsto \mathbb Z^{\geq 0}$ 

10:   is a differentiable distance function over the inputs.

11:   % \footnote{Other distance functions could also be used as

12:   % long as Theorem~\ref{thm:concrete-loss-soundness} can be proved.}

13:   Similarly, $dist_g(y, \Phi_{\safe})$, the ``\emph{distance}'' from

14:   an output vector $y \in \mathbb R^e$ to general output predicate

15:   $\Phi_{\safe}$, can be computed efficiently by induction as long as

16:   $g(\cdot,\cdot)$ can be computed efficiently:

17:   \begin{itemize}

18:   \item $dist_g(y, P)$ and $dist_g(y, \neg P)$ can be computed using basic

19:     arithmetic;

20:   \item $dist_g(y, P_1 \land P_2)$ = $\max(dist_g(y, P_1), dist_g(y, P_2))$;

21:   \item $dist_g(y, P_1 \lor P_2)$ = $\min(dist_g(y, P_1), dist_g(y, P_2))$.

22:   \end{itemize}

23: \end{definition}

24: