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

\newcommand\numberthis{\addtocounter{equation}{1}\tag{\theequation}}

\title{\texttt{fn make\_randomized\_response\_bitvec}}
\author{\AbigailGentleAuthor}

\allowdisplaybreaks

\begin{document}

\maketitle



\contrib

Proves soundness of \rustdoc{measurements/fn}{make\_randomized\_response\_bitvec} in \asOfCommit{mod.rs}{cfd1bec5}.

\section{Introduction}
This is a randomizer in the local model of differential privacy, which is a simplification of the RAPPOR protocol~\cite{rappor}. Under local differential privacy each user is guaranteed $\varepsilon$-DP for their response. RAPPOR achieves local differentially private frequency estimation by flipping each bit of an input vector with fixed probability. Because the noise is added mechanically we can efficiently post-process a set of outputs from this randomizer with the function \rustdoc{measurements/fn}{debias\_randomized\_response\_bitvec}, which sums and normalises a vector of private outputs to account for the bias introduced. The input to this function are elements from a \rustdoc{domains/struct}{BitVectorDomain} with fixed $\texttt{max\_weight}$, setting this value is necessary in order to bound the sensitivity of the function. we detail two use cases below to explain two possible settings of $\texttt{max\_weight}$, which we will denote $m$.

Frequency estimation is the problem of generating a histogram of the empirical frequencies of categorical elements. Any categorical domain of size $k$ can be mapped to the set $[k]=\{0,1,\ldots,k-1\}$, and we can represent any element $j\in[k]$ as the $j$'th standard basis vector so that $m=1$. In cases where the domain is extremely large or even unbounded (such as a set of strings) we can hash the domain elements using a bloom filter with $m$ hash functions. In order to decode a set of outputs generated in this fashion we must perform a regression against the bloom filter representations of a set of candidate elements, neither bloom filters nor the regression tools required for this are implemented here, but details can be found in the original RAPPOR paper. We will require that $2m+1<k$, but $m$ should be much less than $k$ in order to preserve utility. As we will prove in~\ref{thm:privacy-parameter} privacy degrades linearly with $m$. 

\section{Hoare Triple}
\subsection*{Precondition}
\subsubsection*{Compiler-verified}
\begin{itemize}
	\item Variable \texttt{input\_domain} must be of type \rustdoc{domains/struct}{BitVectorDomain}, with \texttt{max\_weight}.
	\item Variable \texttt{input\_metric} must be of type \rustdoc{metrics/struct}{DiscreteDistance}.
	\item Variable \texttt{f} must be of type \texttt{f64}.
    \item Variable \texttt{constant\_time} must be of type \texttt{bool}.
\end{itemize}

\subsubsection*{Caller-verified}
None

\subsection*{Pseudocode}

\lstinputlisting[language=Python,firstline=2,escapechar=|]{./pseudocode/make_randomized_response_bitvec.py}

\subsection*{Postcondition}
\begin{theorem}
\validMeasurement{\texttt{(f, m, constant\_time)}}{\\ \texttt{make\_randomized\_response\_bitvec}}
\end{theorem}
\subsection{Privacy}

\begin{tcolorbox}
\begin{note}[Proof relies on correctness of Bernoulli sampler]
The following proof makes use of the following lemma that asserts the correctness of the Bernoulli sampler function.
    \begin{lemma}
    If system entropy is not sufficient, \texttt{sample\_bernoulli} raises an error. 
    Otherwise, \texttt{sample\_bernoulli(f/2, constant\_time)}, the Bernoulli sampler function used in \texttt{make\_randomized\_response\_bool}, 
    returns \texttt{true} with probability (\texttt{prob}) and returns  \texttt{false} with probability (1 - \texttt{f/2}).
    \end{lemma}
\end{note}
\end{tcolorbox}
\begin{theorem}[\cite{rappor}]
\label{thm:privacy-parameter}
	The program \rustdoc{measurements/fn}{make\_randomized\_response\_bitvec} satisfies $\varepsilon$-DP, where 
	\begin{equation*}
		\varepsilon = 2m\log\left(\frac{2-f}{f}\right).
	\end{equation*}
\end{theorem}
\begin{proof}
	Let $y=(y_1,\ldots,y_j,\ldots,y_k)$ be a randomised report generated by applying \rustdoc{measurements/fn}{make\_randomized\_response\_bitvec} to an input vector $x=(x_1,\ldots,x_j,\ldots,x_k)$. The output of the algorithm satisfies the following conditional probabilities,
	\begin{align}
		\mathbb{P}[y_j = 1~|~x_j=1] &= 1 - \frac{1}{2}f\\
		\mathbb{P}[y_j = 1~|~x_j=0] &=\frac{1}{2}f
	\end{align} 
	The probability of observing any given report $Y$ is $\mathbb{P}[Y=y | X=x]$. Suppose $x=(x,\ldots,x_k)$ is a single Boolean vector with at most $m$ ones. 
	Without loss of generality, as the probabilities are invariant under permutation, assume that $x^*=(x=1,\ldots,x_m=1,x_{m+1}=0,\ldots,x_k=0)$, then we have
	\begin{align*}
		\mathbb{P}[Y=y~|~X=x^*] &=%
			\prod\limits_{i=1}^m \left(\frac{1}{2}f\right)^{1-y_i}\left(1-\frac{1}{2}f\right)^{y_i}%
			\times \prod\limits_{i=m+1}^k\left(\frac{1}{2}f\right)^{y_i} \left(1-\frac{1}{2}f\right)^{1-y_i}.
	\end{align*}
	Then let $D$ be the ratio of two such conditional probabilities with neighbouring inputs $x,x'$, and let $S$ be the range of \rustdoc{measurements/fn}{make\_randomized\_response\_bitvec}.
	\begin{align}
		D &= \frac{\mathbb{P}[Y\in S~|~X=x]}{\mathbb{P}[Y\in S~|~X=x']}\\
			&= \frac{\sum_{y\in S}\mathbb{P}[Y=y~|~X=x]}{\sum_{y\in S}\mathbb{P}[Y=y~|~X=x']}\nonumber\\
			&\leq \max_{y\in S}\frac{\mathbb{P}[Y=y~|~X=x]}{\mathbb{P}[Y=y~|~X=x']}\nonumber\\
			&=\max_{y\in S}\frac{%
				\prod\limits_{j=1}^m \left(\frac{1}{2}f\right)^{1-y_j}\left(1-\frac{1}{2}f\right)^{y_j}%
				\times \prod\limits_{j=m+1}^k\left(\frac{1}{2}f\right)^{y_j} \left(1-\frac{1}{2}f\right)^{1-y_j}
			}{%
				\prod\limits_{j=1}^m \left(\frac{1}{2}f\right)^{y_j}\left(1-\frac{1}{2}f\right)^{1-y_j}%
				\times \prod\limits_{j=m+1}^{2m}\left(\frac{1}{2}f\right)^{1-y_j} \left(1-\frac{1}{2}f\right)^{y_j}\times%
				\prod\limits_{j=2m+1}^{k}\left(\frac{1}{2}f\right)^{y_j}\left(1-\frac{1}{2}f\right)^{1-y_j}
			}\nonumber\\
			&=\max_{y\in S}\frac{%
				\prod\limits_{j=1}^m \left(\frac{1}{2}f\right)^{1-y_j}\left(1-\frac{1}{2}f\right)^{y_j}%
				\times \prod\limits_{j=m+1}^{2m}\left(\frac{1}{2}f\right)^{y_j} \left(1-\frac{1}{2}f\right)^{1-y_j}%
			}{%
				\prod\limits_{j=1}^m \left(\frac{1}{2}f\right)^{y_j}\left(1-\frac{1}{2}f\right)^{1-y_j}%
				\times \prod\limits_{j=m+1}^{2m}\left(\frac{1}{2}f\right)^{1-y_j} \left(1-\frac{1}{2}f\right)^{y_j}%
			}\label{eq:privacy:cancel-k}\\
			&=\max_{y\in S}\left[%
				\prod\limits_{j=1}^m \left(\frac{1}{2}f\right)^{2(1-y_j)}\left(1-\frac{1}{2}f\right)^{2y_j}%
				\times \prod\limits_{j=m+1}^{2m}\left(\frac{1}{2}f\right)^{2y_j} \left(1-\frac{1}{2}f\right)^{2(1-y_j)}\right]\label{eq:maximise-product}%
	\end{align}
	Notice that, by Equation~\ref{eq:privacy:cancel-k}, the privacy is not dependent on $k$ and Equation~\ref{eq:maximise-product} is maximised when $y=1,\ldots,y_m=1$, and $y_{m+1},\ldots,y_{2m}=0$, giving
	\begin{align*}
		D &\leq \left(1-\frac{1}{2}f\right)^{2m}\times\left(\frac{1}{2}f\right)^{-2m}\\
			&= \left(\frac{2-f}{f}\right)^{2m}
	\end{align*}
	Therefore,
	\begin{equation}
		\varepsilon \leq 2m\log\left(\frac{2-f}{f}\right),
	\end{equation}
    which completes the proof.
\end{proof}

\subsection{Utility}

\begin{theorem}
\label{thm:unbiased-estimator}
	The program \rustdoc{measurements/fn}{debias\_randomized\_response\_bitvec} is an unbiased frequency estimator.
\end{theorem}
\begin{proof} 
By independence we can focus on the contribution of one message. Given an input $\bar{x}=(x_1,\ldots,x_j,\ldots,x_k)$, denote the output of \rustdoc{measurements/fn}{make\_randomized\_response\_bitvec} on this input as $\bar{y}$. Assume each $x_j$ was drawn from a distribution with probability $p(x_j)$, we can replace this assumption with the true frequency of $x_j$ later. Each coordinate of $\bar{y}$ is therefore given as follows,
\begin{equation*}
    y_j = \text{Bern}\left(1-\frac{1}{2}f\right)x_j + \text{Bern}\left(\frac{1}{2}f\right) (1-x_j).
\end{equation*}
And the expectation of $\bar{y}_j$ is 
\begin{align}
    \mathbb{E}\left[y_j\right] &= (1-\frac{1}{2}f)p(x_j) + \frac{1}{2}f(1-p(x_j))\nonumber\\
        &= (1-f)p(x_j) + \frac{1}{2}f\label{eq:expect-y}
\end{align}
Therefore rearranging~\ref{eq:expect-y} we can estimate $p(x_j)$ as,
\begin{equation}
    \hat{p}(x)=\frac{y_j - \frac{1}{2}f}{1-f}
\end{equation}
Given $n$ outputs, let $Y=\sum_{i=1}^n \bar{y}_i$ be the element-wise sum of the vector outputs. We can use the above to create an estimator the true counts $\hat{q}$ as,
\begin{equation*}
    \hat{q}_j = \frac{Y_j-n\frac{1}{2}f}{1-f}\numberthis\label{eq:estimator}
\end{equation*}
Which is the estimator in \rustdoc{measurements/fn}{debias\_randomized\_response\_bitvec}.
\end{proof}

\begin{theorem}
	The program \rustdoc{measurements/fn}{debias\_randomized\_response\_bitvec} is a frequency estimator with mean squared error
	\begin{equation*}
		\mathbb{E}[\|q-\hat{q}\|_2^2] = \frac{nk\left(f-\frac{f^2}{2}\right)}{2(1-f)^2}.
	\end{equation*}
\end{theorem}
\begin{proof}
    Let $q = q(X^n)=\sum\limits_{j=1}^n \bar{x}_i$ be the true (non-private) vector sum of the inputs. Our goal is to find the mean squared error of our estimate from this vector. Notice that each coordinate $Y_j$ of $Y=\sum_{i=1}^n \bar{y}_i$, is a sum of Bernoulli random variables with probability $\frac{1}{2}f$ or $(1-\frac{1}{2}f)$ meaning their sum is that of two binomials with equal variance (by the symmetry of their probabilities). Using this we get that the variance is,
\begin{equation}
    \text{Var}(Y_j) = n\frac{f}{2}\left(1-\frac{f}{2}\right), \label{eq:varianceY}
\end{equation}
and the mean squared error is,
\begin{align*}
    \mathbb{E}[\|\hat{q}-q\|_2^2] &= \mathbb{E}\left[\sum\limits_{j=1}^k(\hat{q_j}-q_j)^2\right] = \sum\limits_{j=1}^k\mathbb{E}[(\hat{q_j}-q_j)^2] \\
			&= \sum\limits_{j=1}^k\mathbb{E}[(\hat{q_j}-\mathbb{E}[\hat{q_j}])^2] \tag{By unbiasedness, Theorem~\ref{thm:unbiased-estimator}}\\
			&= \sum\limits_{j=1}^k\text{Var}(\hat{q_j}) = \sum\limits_{j=1}^k\text{Var}\left(\frac{\hat{Y_j}-n\frac{f}{2}}{1-f}\right) \tag{By Equation~\ref{eq:estimator}}\\
			&= \sum\limits_{j=1}^k\text{Var}\left(\frac{Y_j}{1-f}\right) \\
			&= \sum\limits_{j=1}^k\frac{\text{Var}(Y_i)}{(1-f)^2}\\
			&= k\left(\frac{n\frac{f}{2}\left(1-\frac{f}{2}\right)}{(1-f)^2}\right) \tag{By Equation~\ref{eq:varianceY}}\\
			& = \frac{nk\left(f-\frac{f^2}{2}\right)}{2(1-f)^2}
\end{align*}
\end{proof}

\bibliographystyle{plain}
\bibliography{references.bib}
\end{document}
