Automate lifting of functions from concrete types to RandomVariables and abstract domains

[zenna]

There should be a simple and as automated as possible means to lift a function to handle random variables (and abstract domains).

There are a few cases to consider:

Lifting Primitive Julia Functions

Suppose I want to add a function in Base, e.g. round. round is defined on (among many other things) the floating points round(x::Float64). The corresponding method for RandomVariable should be something like

round(X::RandomVariableSymbolic) = RandomVariableSymbolic(Float64,:(ω ⇾ round(ω)))

So we can imagine a lift function or @lift macro, which takes as input a function, and maybe even the types we wish to update, and creates one for RandomVariables

e.g.

@lift round Float64
lift(round,Float64)
@lift div (Int64,Int64)

In this case, round will eventually be passed an Interval and so it must be overloaded to handle these. There is no simple and automated way to do this as it depends on the semantics of the function and abstract domain. In the case of round we can simply round the bounds

round(x::Interval) = Interval(round(x.l), round(x.u))

Rounding the bounds works for continuous and monotonic functions, so we may want some convenience function to do this.

If round is written in terms of other Julia primitives (i.e. it's not a ccall), then it matters not that it is in Base, and we should consider as part of the complex functions case.

Complex Functions

Here the function is complex and written in terms of Julia primitives (which we have already lifted), e.g.

x = uniform(0,1)
y = sqr(x)

If sqr is written without types sqr(x) = x * x, then it will work as is, constructing a RandomVariable with body of the function expanded.

ω -> (*)(quantile(Uniform(0.0,1.0),ω[1]),quantile(Uniform(0.0,1.0),ω[1]))

This will work as intended, but raises two issues:

1. Do we want to substitute the contents of every function into the RandomVariable?
2. What if sqr is defined only as sqr(x::Float64) = x * x

For 1, see issue (ADD REF) 2 depends on our answer to 1, but supposing we keep it as is (answer yes), then the only way seems to be to access the AST of sqr. This can be done with code_typed, etc, but it will likely be difficult. For now the best solution will be to a) leave types off functions b) use union types, e.g.

AbstractFloat = Union(Float64, RandomVariable{Float64}, Interval)