Constraints
The typechecker gives you the result of the privacy analysis of your julia code in form of Types that usually contains variables of two kinds, namely type variables and number variables. The analysis result holds as long as you choose the values for these variables in a way that does not violate any of the constraints that also belong to the typechecking result. There is a variety of constraints, here's a list:
Equality and inequality
IsEqual
constr : constr : τ₁ and τ must be equal
The variables must be equal, i.e. describe the same type (for type variables) or have the same value (for number variables).
IsLess
and IsLessEqual
constr : constr₁ : eps < 1
constr₂ : 0 ≤ eps
The (numeric) variable eps
must be in [0,1)
.
constr : τ ⊑ Real
The type variable τ
must be a subtype of Real
.
IsSupremum
and IsInfimum
constr : constr : Type τ₁ is the supremum of types τ₂ and Integer
constr : Type τ₃ is the infimum of types τ₄ and Real
Suprema and infima w.r.t. the subtyping hierarchy. That is, τ₁
is the type that is lowest in the subtyping hierarchy such that τ₂ ⊑ τ₁
and Integer ⊑ τ₁
Const/NonConst
We support static number types, so we need constraints on whether a number type is static or not.
MakeConst
If type τ is numeric or a tuple, it can become static
All numeric types in τ
will be set to static once they are known.
MakeNonConst
All Numeric types in τ will be set non-static
All numeric types in τ
will be set to non-static once they are known.
UnifyWithConstSubtype
constr : constr : Types τ₁ and τ₂ are equal except for static-ness, where the fist is a subtype of the second
In case τ₁ = τ[s ©]
is a static number for some s
, we allow τ₁ ⊑ τ₂
. Otherwise, it is τ₁ = τ₂
.
Choices/Mulitple Dispatch (IsChoice
)
If the julia type information is not sufficient to resolve multiple dispatch, you end up with constraints instead. Behold the following example, where the function f
has two methods, but in the call to f
that happens withing g
, it is not yet clear which of the methods will be called. Annotating the argument of g
would have made it possible to resolve the constraint, so it is advisable to add annotations where possible.
julia> typecheck_from_string("module L
f(x::Matrix) = x+x
f(x::Integer) = 2*x
g(x) = f(x)
end")
---------------------------------------------------------------------------
Type:
{
| (τ₁₃ @ s₈) -> τ₁₄
}
---------------------------------------------------------------------------
Constraints:
constr : Function types
{
| (τ₁₃ @ s₈) -> τ₁₄
}
are required to exist among the following choices:
- julia signature [Matrix{<:Any}]:
{
| - Matrix<n: τ₈, c: τ₉>[s₅ × s₄]{τ₅₁}
| @ 2.0
| --------------------------
| -> Matrix<n: τ₈, c: U>[s₅ × s₄]{τ₅₁}
}
- julia signature [Integer]:
{
| (Integer @ 2.0) -> Integer
}
Arithmetic operations (IsTypeOpResult
)
Arithemtic operations like addition and multiplication have different sensitivities depending on the types of the operand. On the one hand, arithmetics on matrices behaves different from that on numbers, on the other hand we support static types which behave like constant numbers. For example, the expression s * x
is infinitely sensitive in both s
and x
, but if we assume s
to be of static type, it is 0-sensitive in s
and s
-sensitive in x
. This results in a constraint if the static-ness of the operands is unknown:
constr : Binary operation * on (τ_s @ s₄, τ_x @ s₁) with result type τ₂
Scalars s₄
and s₁
denote the sensitivities of the operands and will be set once the static-ness of τ_s
and τ_x
is determined. The possible operations are +,-,*,/,mod,==,ceil
. Refer to page 36 of the duet paper for reference on the sensitivity of these operations.
Julia Types
IsJuliaEqual
constr : Types τ₁ and τ₂ describe the same julia type
As you can read in the documentation on our types, in addition to the supported julia types we use some refinements. For example, our function types contain information about argument and return types (as well as sensitivity/privacy, of course), while the only type julia provides for functions is Function
. Other examples are static number types, container types that have information about dimension and metric. This constraint requires the julia representation of two types to be indistinguishable, while they might not be equal.
IsFunction
Type τ is a k-function
τ
must be some function type of kind k
where k
is either SensitivityK
or PrivacyK
(not a black box function, though).
Loops (IsLoopResult
)
constr : Sensitivities (s₃, s₄, s₅) are dependant on whether number of iterations in τ₁:τ₂:τ₃ is static. Loop body has sensitivity s₉
If a loop has a static number of iterations, we can give better sensitivity bounds. If the static-ness remains unknown, you end up with a constraint like this. Page 42 of the duet paper has detailed rules on how the sensitivities will be resolved in case of static/non-static number of iterations. If you know the number of iterations is static, consider annotating the relevant variables to avoid unresolved constraints of this kind.
Additive noise mechanisms (IsAdditiveNoiseResult
)
Type τ₁ is the result of an additive noise mechanism executed on τ₂
We provide additive noise mechanisms on numbers and matrices, where they result in different differential privacy. As long as the input type is not known, this constraint remains.
Black Boxes
IsBlackBox
constr : Black box function τ is applied to arguments [τ₁,...]
The only things the typechecker knows about black box functions is their name and the julia signature of the arguments. This constraint makes sure the signature matches the types of what the function was applied to.
IsBlackBoxReturn
constr : Type τ₁ is an argument of a black box, its sensitivity s₁ can be set accordingly
With some combination of input and output types of a black box, the typechecker can infer better privacy bounds. See the documentation on black boxes for details.
Container types
IsVecOrMat
Type τ must be a vector or matrix
IsVecLike
Type τ must be a vector, gradient or one-row matrix
ConversionResult
constr : Converted norm n to norm m on an r-row container, incurring conversion penalty is p
Converting between container types measured with different metrics has effect on the sensitivity of functions. See the documentation of container metrics and page 19f of the duet paper for details.