# Notes on Decimal Multiplication Following conventions from [Decimal Arithmetic](https://hackmd.io/@sxtproofs/Hy3RzZtWo). We will focus on fix point multiplication in this document. For clarity, we denote the decimal we are concerned with by $a_d$ and the integer version as $a$ (assuming known fixed point). ## Example Let $a_d = 5.1$ for fixed point 1. So, $a = 51$. So, $a*a = 2601$. This means that in our usual Hadamard argument, we can prove concretely that $C_{a*a} = C_{2601}$. Unfortunately, under fixed point arithmetic this is incorrect. Rather, **the correct answer should be 2600.** Call this $2601_r$. > Jay: The correct answer should actually be 260 if we are using 1 significant digit. In this situation, we should compute 2601/10 rather than the rounded version of 2601. > Alternatively, it could be 2601 if we want the result to have 2 significant digits. > > Marvin: The issue is that for proving, we need to have precise arithmetic to some extent. So, if we have $s$ decimal points, then the product will end up with $2s$ entries in the integer representation. This can be handled in the usual proving method. However, we have to then round the first $s$ entries as these aren't valid for significant digit arithmetic. > > However, I'm not sure there's a good way to prove the result without requiring the Prover to compute both the precise arithmetic (without rounding) and the rounded version. > > > Jay: `(2601/10)*10` is the same as rounding `2601`. > > > The way to prove the result of `a/b` is for the prover to compute both $q$ and $r$ where $a=qb+r$. Then, the prover needs to produce a range proof that $r\in[0,b)$ and that $q\geq 0$. $q$ is the correct result. $qb$ would be the rounded version of $a$. > > > This is effectively the same thing that you are doing with the rounding below, but with rounding down instead of rounding to the nearest. As long as we can do integer division, we get rounding and decimals for free. > > > > Marvin: I see what you mean. I think, the ultimate deciding factors on which method is best would be: 1) if rounding down is acceptable for applications or if we need to round to nearest, 2) which is better run-time wise. > > > > > Jay: 1) Either method can be tweaked to fit the rounding we desire. `((x+4)/10)*10` would be the way to round to the nearest `10`. > > > > > 2) They both are effectively a wrapper around a range proof. > > > > > 3) We actually want to do division. The answer we want is `260` and not `2600`. (Unless we want the result to retain all sig figs, in which case the resulting column has sigfigs of 2, and the result should be `2601`, in which case neither rounding or division is required.) > > > > > > Marvin: Seems reasonable to me. However, we can do a range proof to check $t = a*a - (a*a)_r$. This means to check that $t \in [-5,4].$ ## In General For fixed point $s$. We would check that $a*b - (a*b)_r \in [-5*10^s,5*10^s)$; this is equivalent to the example when $s = 1$. ## Not Associative We note that rounding is not associative. So, great care in implementing a given SQL-query will be necessary to make sure that issues do not arise. > Jay: Take a look at the example. DataFusion's execution is not associative either. `(a*a)*b` is not the same as `a*(a*b)`. This is something that anyone using decimals is aware of. This is a limitation of decimals themselves and every other SQL engine, and not a limitation of our protocol. > > Nat: I'm not worried about expressions. I agree that as long as we're explicit about expression definitions there will be only one "right answer". The reason I bring up associativity is because we use ring theory for soundness arguments. I'm worried about anything that needs a grand product argument. The difference between us and DataFusion is that DataFusion never has to construct e.g. a polynomial with roots `(a*a)*b` or `a*(a*b)`. I'm becoming more convinced we can get away with this, but that may require more care and more overhead. For example, we can have `decimal` and `decimal_blob` types, where `decimal` has arithmetic operations but only `decimal_blob` can be used in a grand product.