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

\title{\texttt{CompositionMeasure for MaxDivergence}}
\author{Michael Shoemate}
\date{}

\begin{document}

\maketitle

\contrib
Proves soundness of the implementation of \rustdoc{combinators/sequential_composition/trait}{CompositionMeasure} 
for \texttt{MaxDivergence} in \asOfCommit{mod.rs}{f5bb719}.

\section{Hoare Triple}
\subsection*{Precondition}
\subsubsection*{Compiler-Verified}
Types matching pseudocode.


\subsubsection*{Caller-Verified}
None

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

\subsection*{Postcondition}
\begin{theorem}
  \texttt{composability} returns \texttt{Ok(out)} if the composition of a vector of privacy parameters \texttt{d\_mids} 
  is bounded above by \texttt{self.compose(d\_mids)} under \texttt{adaptivity} adaptivity and \texttt{out}-composability.
  Otherwise returns an error.
\end{theorem}

\begin{proof}
  By the postcondition of \rustdoc{traits/trait}{InfAdd} we have that $\sum_i \texttt{d\_mids}_i \le \texttt{compose(d\_mids)}$.

  \begin{center}
    \begin{tabular}{ r | l l }
      Adaptivity & Sequential & Concurrent \\ 
      \hline
      Non-Adaptive & Theorem~1\cite{dwork2006calibrating} & Theorem~1.8\cite{vadhan2021concurrent} \\  
      Adaptive & Theorem~1\cite{dwork2006calibrating} & Theorem~1.8\cite{vadhan2021concurrent} \\
      Fully-Adaptive & None & None
    \end{tabular}

    This table is reflected in the implementation of \texttt{composability} on line~\ref{line:composability}.
  \end{center}
  
\end{proof}

\bibliographystyle{alpha}
\bibliography{ref}

\end{document}