Impute Constant #8

gracetian6 · 2021-07-26T21:23:22Z

make_impute_constant is a function that "imputes" or inserts a constant input variable whenever the vector entry is null.

Changes as of July 26:

pseudocode with preconditions and post conditions
proofs with appropriate output domain, domain metric, stability guarantee

PRIORITIZE: Appropriate Output Domain Proof. Not really sure if checking type signature is enough? Unsure whether the error check in the code needs to be included in pseudo code (and is needed to justify output domain pf).

Please look at impute_constant.pdf as you review the .tex!

gracetian6 · 2021-07-26T21:24:38Z

impute_constant/impute_constant.tex

+\item \textbf{(Appropriate output domain).} 
+In the case of \texttt{make\_impute\_constant}, this corresponds to showing that for every vector $v$ of elements of type \texttt{DA}, \texttt{function}$(v)$ is a vector of elements of type \texttt{DA::NonNull}.
+
+The $\function(v)$ has type \texttt{Vec(DA)} follows from the assumption that element $v$ is in \texttt{input\_domain} and from the type signature of \texttt{function} in line~\ref{line:fn} of the pseudocode (Section~\ref{sec:pseudocode}), which takes in an element of type \texttt{Vec(DA)} and returns an element of type \texttt{Vec(DA::NonNull)}. If the Rust code compiles correctly, then the type correctness follows from the definition of the type signature enforced by Rust. Otherwise, the code raises an exception for incorrect input type. 
+
+Lastly, we ensure that return type must be \texttt{NonNull} \grace{Attribute? Property? Carrier} \texttt{DA::NonNull} because we check to make sure the \texttt{constant} being imputed in the function must be null. \grace{Not sure if this needs to be explicit in the pseudo code with the error check, or if I can just cite some trait property.} This check already exists because in the input of the \texttt{make\_impute\_constant}, \texttt{constant} is required to have type of \texttt{DA::NonNull}.


Want feedback on appropriate output domain - not sure how to make it more rigorous, and if I need to consider more than just the type signature.

Based on this message I think there should first be a definition of AllDomain along the lines of "the set of all non-null values that T may take on." You want to show that the output domain on this constructor is VectorDomain<AllDomain<T>>, or "any Vec<T> without nulls". You can first lean on the type system to get you most of the way there- the type system constrains the output set to "any Vec<T>". You can then show that the set of potential outputs is equivalent to the set described by VectorDomain<AllDomain<T>> by showing that vectors with nulls are not members of the output set.

Unmarking this as resolved, because you resolved it before I finished writing my response!

The Ord changes make this comment is partially outdated. AllDomain will not be adjusted.

impute_constant/impute_constant.tex

gracetian6 · 2021-07-29T20:01:38Z

Changes as of Thu Jul 29:

incorporated check for nullity in the pseudo code (per Mike's comments)
added lemma that shows that DA::NonNull can contain null values
updated proof for appropriate output domain to take into account the check for nullity (of the lemma above)

PRIORITIZE (see my comments on the code below):

In the pseudocode: Is the type signature correct (input and output type)? Are the input and output domain correct?
In the appropriate output domain proof: What is the reason the type signature is not sufficient? Is it because the output type is more general than the output domain? Or is it theoretically because constant can be null value even if it has the type DA::NonNull?
First lemma in proof: so, is it correct that a variable with type DA::NonNull can contain null values?

gracetian6

Below I have marked down the questions and parts I'd like reviewers to prioritize.

impute_constant/impute_constant.tex

gracetian6 · 2021-07-29T20:04:14Z

impute_constant/impute_constant.tex

+
+The $\function(v)$ has type \texttt{Vec(DA)} follows from the assumption that element $v$ is in \texttt{input\_domain} and from the type signature of \texttt{function} in line~\ref{line:fn} of the pseudocode (Section~\ref{sec:pseudocode}), which takes in an element of type \texttt{Vec(DA)} and returns an element of type \texttt{Vec(DA::NonNull)}. If the Rust code compiles correctly, then the type correctness follows from the definition of the type signature enforced by Rust. Otherwise, the code raises an exception for incorrect input type. 
+
+Lemma \ref{lemma-NonNull} tells us the type signature is not sufficient check because (1) the output type of \texttt{VectorDomain(DA::NonNull)} is more general than the output domain of \texttt{VectorDomain(DA::NonNull)}. \grace{?? The output type matches the output domain I wrote, so something's wrong.} (2) \texttt{constant} can be \texttt{null} even if it is of type \texttt{DA::NonNull}. For (2), if the constant is null, then \texttt{impute\_constant} function (line \ref{line:atomfn}) could potentially return \texttt{null} values since it replaces a \texttt{null} input with \texttt{constant}.


for appropriate output domain:

What is the reason the type signature is not sufficient? Is it because the output type is more general than the output domain? Or is it theoretically because constant can be null value even if it has the type DA::NonNull?

Hmm, Vec(DA) or "a vector of atomic domains" doesn't really make sense in this context. I think you meant Vec(DA::Carrier) in these blocks instead of Vec(DA).

And yes, in this case the output type can represent a value (float nan) that is not a member of the output domain. The purpose of the impute function is to ensure that these outputs are never null at runtime, so it replaces null with a constant. Since constant has type DA::NonNull, and DA::NonNull may itself be f64, we must check that constant is non-null. This check should make it impossible for analysts to "impute" by nonsensically replacing nulls with nulls, thus violating the output domain.

Thank you Mike. This helps clarify things a lot!

gracetian6 · 2021-07-29T20:05:13Z

impute_constant/impute_constant.tex

+\begin{lemma}[\texttt{DA::NonNull} contains \texttt{null}] \label{lemma-NonNull}
+\texttt{var} of type \texttt{DA::NonNull} can be of type \texttt{null}.
+\end{lemma}
+\begin{proof}
+Let the domain of atom variable \texttt{DA} be \texttt{InherentNullDomain<AllDomain<f64>>}. Recall that \texttt{InherentNullDomain} exists for types that can represent null inherently in the carrier type. Then the type $$\texttt{DA::NonNull == InherentNullDomain<AllDomain<f64>>::NonNull == f64}.$$ The latter holds because in the \texttt{InherentNullDomain} implementation in the rust code \url{https://github.com/opendp/opendp/blob/main/rust/opendp/src/trans/impute.rs#L48-L56}, the \texttt{type NonNull = Self::Carrier}. The \texttt{Carrier} of \texttt{VectorDomain<AllDomain<T>>} has type \texttt{T}, so in this case the \texttt{::Carrier} is type \texttt{f64}.
+
+Therefore \texttt{var} is also of type \texttt{f64}. \texttt{f64} can contain \texttt{null} values, so we are done.
+\end{proof}


is it correct that a variable with type DA::NonNull can contain null values?

DA::NonNull may be capable of representing a null value. This is the case when DA is InherentNullDomain<AllDomain<f64>>, meaning DA::NonNull is f64. If an instance of DA::NonNull is null, it is either imputed or a construction-time error is raised by 2.

Shoeboxam · 2021-07-29T22:42:10Z

If it helps with clarity, we could rename DA::NonNull to DA::Imputed or something else. I'm indifferent towards renaming as it's not clear to me personally if that's an improvement.

Shoeboxam · 2021-07-29T22:54:29Z

In the context of the overall library, this constructor slightly changes the meaning of AllDomain<T>. AllDomain<T> used to be "the set of values T may take on." It is now "the set of non-null values T may take on." This change to AllDomain simplifies the domains of all transformations/measurements after imputation, as it keeps descriptors for nullity isolated to two specific domains early in the data processing pipeline. On the other hand, this distinction is not currently captured in the member check for AllDomain.

See also opendp/opendp#203. If we adopted noisy-float, then we wouldn't be changing the AllDomain description.

gracetian6

Changes as of Aug 5 (ready to be reviewed)

stability guarantee pf references row transform
proof of pure function (satisfies row transform criteria)
row transform incorporated into pseudocode

PRIORITIZE comments specifically added by me below!

impute_constant/impute_constant.tex

gracetian6 · 2021-09-04T17:39:59Z

impute_constant/impute_constant.tex

+
+The $\function(v)$ has type \texttt{Vec[DA::Imputed]} follows from the assumption that element $v$ is in \texttt{input\_domain} and from the type signature of \texttt{function} in line~\ref{line:fn} of the pseudocode (Section~\ref{sec:pseudocode}). The type signature takes in an element of type \texttt{Vec[DA::Carrier]} and returns an element of type \texttt{Vec[DA::Imputed]}. If the Rust code compiles correctly, then the type correctness follows from the definition of the type signature enforced by Rust. Otherwise, the code will halt at compile time.
+
+The type signature is not a sufficient check, since by Lemma \ref{lemma:Imputed}, the function's output type can represent a value (e.g. \texttt{float nan}) that is not a member in the \texttt{output\_domain}. \grace{How do I clarify that the output domain \\ \texttt{VectorDomain(AllDomain(DA::Imputed))} should actually contain NO NULLS? The code seems too loose because in Lemma 1.1 we just showed that \texttt{DA::Imputed} can contain null values.} To ensure that function returns the appropriate output domain at run time, we must ensure that at run time the \texttt{function}$(v)$ is not null. To do so, we must check whether the \texttt{constant} is not null.


Would like feedback on how to clarify that the output domain VectorDomain(AllDomain(DA::Imputed)) should actually contain NO NULLS but the output type Vec[DA::Imputed] can contain a null value?

Seems contradictory since Lemma 1.1 we just showed that DA::Imputed can contain null values

gracetian6 · 2021-09-04T17:43:43Z

New changes as of Sept 4, 2021:

addressed comments about pure function (updated to proofs def doc)
stylistic changes to pseudo code, pre conditions
want feedback on appropriate output domain proof

gracetian6 and others added 12 commits July 8, 2021 10:41

Update README.md

768d4a6

Add files via upload

3cc1e56

Rename is_equal.tex to is_equal/is_equal.tex

abc2218

Delete make_impute_unif_float.png

0fe3b9a

Delete make_impute_constant.jpg

7a70304

moved folders

c7c1fd5

pdf and png

da7d1ef

7/23 style + hist proof

755986d

fixed typos 7/26

8ec984c

typos 7/26

d76d3db

impute_constant preliminary -- confused about output domain pf

3a124dd

confused about output domain pf

549defc

gracetian6 requested review from pdurbin, ecowan, Shoeboxam, andrewvyrros, SalilVadhan, cwagaman and silviacasac July 26, 2021 21:23

gracetian6 self-assigned this Jul 26, 2021

gracetian6 commented Jul 26, 2021

View reviewed changes

gracetian6 added 3 commits July 29, 2021 15:54

check constant for nullity

1667f72

check constant for nullity

9ddcc31

actually checks constant for nullity

2c26e1c

gracetian6 commented Jul 29, 2021

View reviewed changes

gracetian6 added 2 commits July 30, 2021 17:28

Delete impute_constant.tex

05d4d50

Delete impute_constant.pdf

3d37f8f

gracetian6 added 4 commits July 30, 2021 17:29

why we must check constant for nullity

e9e096b

Delete impute_constant.tex

f77198d

Delete impute_constant.pdf

0e35cc9

pure function + row transform (stability)

7b5483a

gracetian6 commented Aug 5, 2021

View reviewed changes

SalilVadhan reviewed Aug 6, 2021

View reviewed changes

impute_constant/impute_constant.tex Outdated Show resolved Hide resolved

SalilVadhan reviewed Aug 6, 2021

View reviewed changes

impute_constant/impute_constant.tex Outdated Show resolved Hide resolved

SalilVadhan reviewed Aug 6, 2021

View reviewed changes

impute_constant/impute_constant.tex Outdated Show resolved Hide resolved

SalilVadhan reviewed Aug 6, 2021

View reviewed changes

impute_constant/impute_constant.tex Outdated Show resolved Hide resolved

SalilVadhan reviewed Aug 6, 2021

View reviewed changes

impute_constant/impute_constant.tex Outdated Show resolved Hide resolved

SalilVadhan reviewed Aug 6, 2021

View reviewed changes

impute_constant/impute_constant.tex Show resolved Hide resolved

gracetian6 added 3 commits September 4, 2021 13:33

Delete impute_constant.pdf

a2d4561

Delete impute_constant.tex

6406357

impute constant changes from summer

c5e09b9

gracetian6 commented Sep 4, 2021

View reviewed changes

Shoeboxam mentioned this pull request Sep 23, 2021

Impute Constant Transformation -- Proof opendp/opendp#118

Open

Shoeboxam mentioned this pull request Aug 5, 2022

make_impute_constant proof opendp/opendp#515

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Impute Constant #8

Impute Constant #8

gracetian6 commented Jul 26, 2021

gracetian6 Jul 26, 2021

Shoeboxam Jul 29, 2021

Shoeboxam Jul 29, 2021

Shoeboxam Aug 7, 2021

gracetian6 commented Jul 29, 2021 •

edited

Loading

gracetian6 left a comment

gracetian6 Jul 29, 2021

Shoeboxam Jul 29, 2021 •

edited

Loading

gracetian6 Jul 30, 2021

gracetian6 Jul 29, 2021

Shoeboxam Jul 29, 2021 •

edited

Loading

Shoeboxam commented Jul 29, 2021 •

edited

Loading

Shoeboxam commented Jul 29, 2021 •

edited

Loading

gracetian6 left a comment

gracetian6 Sep 4, 2021

gracetian6 commented Sep 4, 2021


		The $\function(v)$ has type \texttt{Vec(DA)} follows from the assumption that element $v$ is in \texttt{input\_domain} and from the type signature of \texttt{function} in line~\ref{line:fn} of the pseudocode (Section~\ref{sec:pseudocode}), which takes in an element of type \texttt{Vec(DA)} and returns an element of type \texttt{Vec(DA::NonNull)}. If the Rust code compiles correctly, then the type correctness follows from the definition of the type signature enforced by Rust. Otherwise, the code raises an exception for incorrect input type.

		Lemma \ref{lemma-NonNull} tells us the type signature is not sufficient check because (1) the output type of \texttt{VectorDomain(DA::NonNull)} is more general than the output domain of \texttt{VectorDomain(DA::NonNull)}. \grace{?? The output type matches the output domain I wrote, so something's wrong.} (2) \texttt{constant} can be \texttt{null} even if it is of type \texttt{DA::NonNull}. For (2), if the constant is null, then \texttt{impute\_constant} function (line \ref{line:atomfn}) could potentially return \texttt{null} values since it replaces a \texttt{null} input with \texttt{constant}.


		The $\function(v)$ has type \texttt{Vec[DA::Imputed]} follows from the assumption that element $v$ is in \texttt{input\_domain} and from the type signature of \texttt{function} in line~\ref{line:fn} of the pseudocode (Section~\ref{sec:pseudocode}). The type signature takes in an element of type \texttt{Vec[DA::Carrier]} and returns an element of type \texttt{Vec[DA::Imputed]}. If the Rust code compiles correctly, then the type correctness follows from the definition of the type signature enforced by Rust. Otherwise, the code will halt at compile time.

		The type signature is not a sufficient check, since by Lemma \ref{lemma:Imputed}, the function's output type can represent a value (e.g. \texttt{float nan}) that is not a member in the \texttt{output\_domain}. \grace{How do I clarify that the output domain \\ \texttt{VectorDomain(AllDomain(DA::Imputed))} should actually contain NO NULLS? The code seems too loose because in Lemma 1.1 we just showed that \texttt{DA::Imputed} can contain null values.} To ensure that function returns the appropriate output domain at run time, we must ensure that at run time the \texttt{function}$(v)$ is not null. To do so, we must check whether the \texttt{constant} is not null.

Impute Constant #8

Are you sure you want to change the base?

Impute Constant #8

Conversation

gracetian6 commented Jul 26, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gracetian6 commented Jul 29, 2021 • edited Loading

gracetian6 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Shoeboxam Jul 29, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Shoeboxam Jul 29, 2021 • edited Loading

Choose a reason for hiding this comment

Shoeboxam commented Jul 29, 2021 • edited Loading

Shoeboxam commented Jul 29, 2021 • edited Loading

gracetian6 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gracetian6 commented Sep 4, 2021

gracetian6 commented Jul 29, 2021 •

edited

Loading

Shoeboxam Jul 29, 2021 •

edited

Loading

Shoeboxam Jul 29, 2021 •

edited

Loading

Shoeboxam commented Jul 29, 2021 •

edited

Loading

Shoeboxam commented Jul 29, 2021 •

edited

Loading