Nonlinear arithmetic

[SSoelvsten]

To prove GapSparseVector correct Wang et al. [Wan+19] removed the nonlinearity introduced in the absolute value due to the T-Laplace. Their approach was to replace the |d| with its numerical upper bound of 2. This upper bound is true due to the precondition that

∀i < |q| : −1 ≤ ˆq[i] ≤ 1 .

In general, one could automate major parts of this step. If there is a bound on a star typed variable x such that

l ≤ ˆx ≤ u ,

then one may provide a variant of the Lap function that instead adds the bound |l|+|u| to v_epsilon rather than |d|. If l and u are provided by the programmer, then one may want to prove

Φ =⇒ l ≤ d ≤ u

as an assert statement in the transformed program.