Clamp

[silviacasac]

First pull request for the Clamp transformation, which corresponds to this GitHub permalink.

It has undergone a first correction by Prof. Vadhan on June 22 and a first correction by Mike on July 1 and 7. All these corrections have been implemented. The pseudocode has not been changed to include Andy's comment on July 1 on adding the domains and metrics as declarative statements in the preconditions. (Edit: the updated version now includes said preconditions)

Files:

• clamp.tex -- the LaTeX document with the proof.
• clamp.pdf -- the PDF generated from the TeX document.
• clamp_rust.png -- the screenshot of the corresponding Rust code.

Update: July 12, 2021

• Resolved comments by Phil and Mike above.
• Added the preconditions (and taken them out from the pseudocode) as discussed last week. We also decided to separate the preconditions into "user-specified types" and the 4 "input metric, output metric, input metric, output metric" that all transformations will have. We also decided to add a postcondition to deal with the fallible case.
• Changed floats to non-null floats after Mike's comment on total ordering not working for possibly null floats.
• Changed the statement of Theorem 1 to make it as general as possible (i.e., "under input_metric" instead of "under symmetric distance" so that the Theorem statement can be re-used in the proofs. Changed "appropriately quantified" to specifying the types of din, dout; which is what it meant.
• Changed some of the "rustiness" expressions that were left in the proof after the preconditions explained "in words" change (e.g., delete VectorDomain(IntervalDomain(L, U)).
• Deleted the section "Conditions as specified in the pseudocode" because it is repetitive with the new preconditions. There is also no equation form for the stability relation and I refer directly to the pseudocode lines.
• Added table of contents

Further questions on the new version:

• Type sign L and U as it is now (def MakeClamp(L: T, U: T) or add that L and U have type T in the preconditions?
• Move the if L>U: raise Exception to the preconditions? a) But this would not be a compile time error. b) Mike said that the Rust construction for IntervalDomain is enforced to check that L<=U, so do I need to check this condition in the pseudocode and raise an exception if IntervalDomain(L, U) is in the preconditions?
• We were discussing to maybe define symmetric distance for vectors (as opposed to multisets) so that we can drop having to write MultiSet(v) every time in the proofs.

Update: July 14, 2021

• Domains and metrics are still listed as preconditions (pending a double-check with @andrewvyrros), but they are likely to be put back into the code, as discussed with @SalilVadhan on July 13. Main issue: the declaration of certain domains requires variables that are only defined in the pseudocode.
• Added another part to the theorem statement (which should, from now on, appear in all of the proofs): "2. Domain-metric compatibility". As discussed on July 13, it is necessary to ensure that the input domain is part of the list of domains included in the definition of said metric. This usually follows directly from our list of definitions, but some later proofs might need to include some checking in the code.
• With Mike we decided not to do inf_cast on d_in given that d_in and d_out have the same type (namely u32).

Update: September 6, 2021

• All the revisions suggested in this pull request have been implemented.
• The major change constitutes the simplification of the stability guarantee proof by means of defining a row transform and proving their general stability lemma, which is now included in the "List of definitions used in the proofs". For now, we are only using the row transform as a proof strategy and is not in the code, and hence there is no discussion about pure functions in this documents. We wanted to separate the lemmas that relate to row transform as a proof strategy as opposed to the actual transformation that would be called in the code.

[raprasad]

Looks good!

[pdurbin]

Good stuff. The math is beyond be but I left a few comments.

[SalilVadhan]

add a cross-reference to the pseudocode_defs file so that the reviewer knows where to find the def of the trait TotalOrd.

[silviacasac]

We have been meaning to add cross-references between the tex files, but it didn't quite work (tex-wise) -- we have to look again into it. But in any case, are you then saying that we should cross-reference every single term that appears defined in pseudocode_defs and proof_defs? So what I mean is that it is not just TotalOrd, but also many other terms in the document

[SalilVadhan]

is this an old version of the code? still has PartialOrd in it.

[SalilVadhan]

Also it looks like it doesn't enforce that M is SymmetricDistance.

[silviacasac]

No, TotalOrd is still not implemented in the OpenDP code. Mike said it is in the to do list, but it has not yet been changed, which is why PartialOrd still appears in the pseudocode. Still, I do the proof with TotalOrd because Mike said it will for sure be updated in the near future.

[SalilVadhan]

Got it, thanks

[Shoeboxam]

I haven't made the change to Ord a priority because it hasn't been clear to me if this is what we want for the library. I wrote a bit more about this in an issue here: opendp/opendp#203

I'd be happy to make the changes once it's clear that we want to adopt noisy-float newtypes to strengthen this trait bound.

[silviacasac]

(Discussed on the architecture meeting on August 3rd)

[SalilVadhan]

Until the code has been fixed, the proof document should say explicitly that the proof is being given assuming Ord even though the Rust code only requires PartialOrd, so the Rust code is not quite correct yet. In general, any gaps like this should be highlighted clearly at the beginning of the document under a section titled something like "Remaining Gaps between Proof and Code".

[silviacasac]

It is a good idea to have such a section -- but TotalOrd is fixed now, so I deleted it

[SalilVadhan]

where can I find definitions of max, min, list, map? Are these built-in Rust functions?

[silviacasac]

Max and min are defined in the pseudocode definitions file (see Definitions 4.17 and 4.18). Map and list are built-in functions, but I can add them to the pseudocode definitions file. In the case of clamp, the Rust code does not directly use a list, but talking to Mike we settled on that the best Python-Rust blend term for this line would be to use a list, instead of the Rust .collect() function that appears in the code.

[SalilVadhan]

I do think it would be good to add map and state in the pseudocode defs file that it is representing the Rust function collect. Actually doesn't map by definition return a list? So what is the list(.) function doing?

[SalilVadhan]

nvm, I see my questions are answered below- but the fact that Grace and I had the same question reinforces that it would be good to add defs of map and list into the pseudocode_defns file

[silviacasac]

Yes, they are added now

[SalilVadhan]

I think the following will give a simpler proof. Whenever we have a function from Vector Domains to Vector Domains of the form function(data)=list(map(f,data)), then h_{function(v)}(z) = sum_{y in f^{-1}(z)) h_v(y). And then apply triangle inequality and that the sets f^{-1}(z) form a partition of the domain of f. This will avoid a need to do a case analysis, and we can use the same proof for all of transformations of this form. In fact, this can be a general lemma in the proof_defns file that we cite, or a proof for "make_rowtransform" (which I believe that Mike may have written, but which will require a precondition on the function f).

[SalilVadhan]

the requirement is that f should be a "pure" function, i.e. a function in the standard mathematical sense, not a piece of code that has side effects or can access some global state.

[gracetian6]

I am typing up proof of stability relations for row by row transformations. Would it make more sense for this to be in the list of definitions in proofs or a separate transformation proof for make_row_by_row?

[silviacasac]

Decided on August 4: clamp will not include this simplified row by row proof until the Rust code for clamp actually calls the make_row_by_row transformation inside of it. But see e.g., is_equal for a use case of the make_row_by_row transformation.

[SalilVadhan]

Also it looks like it doesn't enforce that M is SymmetricDistance.

[SalilVadhan]

Got it, thanks

[gracetian6]

very well organized; it really helps that you broke down each case to consider with firstly, secondly, etc.

[gracetian6]

Why do we use list()? By definition of map, it should apply to clamp function elementwise to the entire input vector. https://en.wikipedia.org/wiki/Map_(higher-order_function)#:~:text=In%20many%20programming%20languages%2C%20map,when%20considered%20in%20functional%20form.

[gracetian6]

Nvm, Silvia explained that the reaosn is because

Mike: “2. returning a map has a slightly different meaning. list(map(...)) or [clamp(L, U, v) for v in arg] is more accurate. In rust, the .collect exhausts the iterator into a vector. So the analogue here is list or the list comprehension (not a generator comprehension). It would be cool if we chained iterators, but that makes other things more complicated (edited)”

[silviacasac]

Right so we want to return a vector (for appropriate output domain) hence we use the Python list, not a map

[Shoeboxam]

Why the special naming "Relation" instead of "stability_relation"? The code makes sense. Are you guys planning on switching type hints to the type hint syntax? I prefer the typing syntax for hints as it looks less like a function invocation. It's a pretty minor pick, basically Vec(T) -> Vec[T]. Also, are we keeping Vec from rust or using python's list in the pseudocode? The iterator collection uses list, but the type is a Vec. I would change one or the other to be consistent.

[silviacasac]

Regarding the special naming of "Relation": I mainly did this to save space in Section 2. Proof when proving the stability relation, so that only "Relation" appears in the text instaed of "stability_relation". And also so that the theorem statement for the stability/privacy guarantee looks the same for measurements, where we would have privacy_relation = Relation. But if you think this is not enough to change it I can add stability_relation back, no problem.

[silviacasac]

About the type hint syntax, are you saying that the correct function type signing for clamp is def function(data: Vec(T)) -> Vec[T]? How so? So initially we had Vec(T) -> Vec(T) but you said that this was not correct, and so we introduced the rule "Parentheses, (), are used to create an instance of a domain. Square brackets, [], are used to describe the type of a domain. For example, AllDomain(i8) is the domain of all values of type i8. However, the type of AllDomain(i8) -- the domain itself, not the elements of the domain -- is AllDomain[i8]; note the square brackets. This typing style is inspired by the notation used in Python; see \url{https://docs.python.org/3/library/typing.html}." (this is now included in the pseudocode definitions).

[silviacasac]

Regarding Vec vs list: so I thought we wanted the pseudocode to look as Python as possible, which is why I wrote it in list format. But then it seemed not correct to change the input and output domains, because the VectorDomain formulation is important and appears everywhere, and also for showing correct output domain. When you say you would change either or the other are you proposing to either: 1. Change line 148 to return Vec(map(clamp, data)) and keep the domains as they are, or 2. To keep line 148 as it is and change the domains to something different? Approach 2 seems worse I think, because that is inventing new domains that don't exist in the Rust library. And could we not just say that list has type Vec in the list of definitions to resolve this? But perhaps approach 1 is better then, although less Python

[Shoeboxam]

1. I think the part throwing me is that camel-case code in python usually represents classes. I have a soft preference towards relation or stability_relation.

2. No, the arrow in my statement was meant to communicate "replace Vec(T) with Vec[T]". The current syntax in the pseudocode is def function(data: Vec(T)) -> Vec(T):. The revised syntax would be def function(data: Vec[T]) -> Vec[T]:. The type hints should use the type syntax, because you're not making instances of a Vec within the signature.

3. You're right, there's no win here. I think we leave Vec/list inconsistent unless someone else has strong feelings.

[silviacasac]

1. That makes sense, I had not considered the implications of having it capitzalied. I will change all of them to relation then.
2. Ah okay, I thought the TeX had already been changed to Vec(T), but it is fixed now.
3. Okay!

[Shoeboxam]

Will switching to IntDistance cause headaches elsewhere? I'm thinking no, but sometimes making things more flexible complicates things. IntDistance is just a type alias, the user can't change it, but having it behind an alias makes it easy to change across the library. The naming could be adjusted, as always. It might make sense to add an explicit list of types IntDistance can be- basically all primitive int types.

[silviacasac]

Oh right you had changed the associated type of symmetric distance to IntDistance, right? But then set IntDistance = u32 -- so you say to add an explicit list of types IntDistance can be, but isn't it only used for u32 in symmetric distance no? And are you saying that I should change the above to def Relation(d_in: IntDistance, d_out: IntDistance)? Or perhaps not yet because it does not appear in the clamp Rust code?

[silviacasac]

Okay I think you are saying to write def Relation(d_in: IntDistance, d_out: IntDistance) instead, but then should IntDistance = u32 be specified anywhere in the clamp pseudocode or do we add the explicit list of types for IntDistance in the definitions for the pseudocode document?

[Shoeboxam]

It would be nice to pull this u32 constant out in favor of an alias, but it does seem to cause headaches--

1. The name is much longer
2. We use all sorts of traits/methods on IntDistance that aren't qualified in the trait bounds because it's a type alias, not a generic. I wouldn't want to have to pull these details down into proofs everywhere.

I vote we don't bother making changes at this point. If we did, I would advocate:

1. a better alias name
2. the alias definition only makes a definitive statement that it is defined to be u32
3. include a weaker statement that any type from a list of int types should be isomorphic, but not give explicit guarantees.

Maybe a better approach is to just add the statement in (3) to the definition of SymmetricDistance, and leave the proofs as-is.

[silviacasac]

Okay, for now I will leave u32 then.

[silviacasac]

Remaining things to double-check (all minor):

• Vec vs list
• IntDistance vs u32
• Vec(T) vs Vec[T]

Will require future edits if make_row_by_row is added to the clamp Rust code in the library.

Edit: the remaining things have been double-checked.

[SalilVadhan]

comment on the Rust code (should probably be a comment on manipulation.rs): 1-stability and Lipschitz constant of 1 are the same thing (so "as well as" should be "i.e.")

[SalilVadhan]

why include this code if the proof is only going to be for make_clamp_vec?

[silviacasac]

I took it out

[SalilVadhan]

minor nit "dout is the associated type" -> "dout is of the associated type" (actually "dout has the associated type" reads more nicely)

[SalilVadhan]

shouldn't we say "MakeClamp raises a exception (at compile time or run time) or returns a valid transformation."? (And then we can/should put the def of what constitutes a valid transformation in either the pseudocode_defns or proof_defns file (not sure which).)

[SalilVadhan]

I think the fact that IntervalDomain raises an exception when L>U should be stated at the beginning of the proof, before item 1. Otherwise much of what follows doesn't make sense (e.g. case analysis above for clamp).

[SalilVadhan]

I think it's worth doing that here in this proof even prior to make_row_by_row. It is much simpler and shorter than what's above.