\documentclass{article}
\input{../../lib.sty}

\title{\texttt{fn make\_clamp}}
\author{S\'ilvia Casacuberta}
\date{}

\begin{document}

\maketitle

\contrib
Proves soundness of \texttt{fn make\_clamp} in \asOfCommit{mod.rs}{0db9c6036}.

\subsection*{Vetting History}
\begin{itemize}
    \item \vettingPR{512}
\end{itemize}

\section{Hoare Triple}
\subsection*{Precondition}
To ensure the correctness of the output, we require the following preconditions:

\begin{itemize}
    \item Type \texttt{TA} must have trait \texttt{ProductOrd}.
    \item Type \texttt{M} must have trait \texttt{DatasetMetric}.
\end{itemize}

\subsection*{Pseudocode}
\lstinputlisting[language=Python,firstline=2,escapechar=|]{./pseudocode/make_clamp.py}

\subsubsection*{Postconditions}
\validTransformation{\texttt{(input\_domain, input\_metric, bounds)}}{\texttt{make\_clamp}}

\section{Proof}

\begin{lemma}
    The invocation of \rustdoc{transformations/manipulation/fn}{make\_row\_by\_row\_fallible} (line \ref{line:row-by-row}) satisfies its preconditions.
\end{lemma}

\begin{proof}
    \label{lemma:row-by-row-precondition}
    The preconditions of \texttt{make\_clamp} and pseudocode definition (line \ref{line:def}) ensure that the type preconditions of \texttt{make\_row\_by\_row\_fallible} are satisfied. 
    The remaining preconditions of \texttt{make\_row\_by\_row\_fallible} are:
    \begin{itemize}
        \item \texttt{row\_function} has no side-effects.
        \item If the input to \texttt{row\_function} is a member of \texttt{input\_domain}'s row domain, then the output is a member of \texttt{output\_row\_domain}.
    \end{itemize}

    The first precondition is satisfied by the definition of \texttt{clamper} (line \ref{line:clamper}) in the pseudocode.

    For the second precondition, assume the input is a member of \texttt{input\_domain}'s row domain. 
    Therefore, by \ref{line:assert-non-null}, the input is non-null.
    In addition, since \texttt{Bounds.new\_closed} did not raise an exception, then by the definition of \texttt{Bounds.new\_closed}, the bounds are non-null.
    Thus, by the definition of \rustdoc{traits/trait}{ProductOrd}, the preconditions of \texttt{total\_clamp} are satisfied, so the output is within the bounds.
    Therefore, the output is a member of \texttt{output\_row\_domain}.
\end{proof}

We now prove the postcondition of \texttt{make\_clamp}.
\begin{proof}
By \ref{lemma:row-by-row-precondition}, the preconditions of \rustdoc{transformations/manipulation/fn}{make\_row\_by\_row\_fallible} are satisfied.
Thus, by the definition of \\\texttt{make\_row\_by\_row\_fallible}, the output is a valid transformation.
\end{proof}

\end{document}