Discussions about SPARK Math implementation (integer and fixed-point operations)

[Heziode]

This topic is created to discuss the implementation of operations on integer and fixed-point types implemented in SPARK_Math.

Notably, the 1st question:

[ANN] Looking for volunteers for an Ada funding committee

I looked into it, specifically spark_math. I tried to implement the natural logarithm using the taylor series but had two problems. For fixed point: I need exponentiation but that is not implemented (would need n-th square root for that ig). For integers: exponentiation is implemented but after copying the code from fixed point I noticed that all values get floored and the result becomes bogus. After implementing the taylor series I saw in the readme that it should be implemented in CORDIC. …

As a side note:
SPARK_Math was developed because I would like to create distance library, to provide distances functions on vectors and strings, notably to help me in the development of a side project, Halmada, an Halma board game implementation in Ada (it’s only for fun, and will be open-sourced in comings weeks).

I have a good knowledge of Ada, but, I am not a mathematician, and I still learning SPARK. So any help is welcome

For implementation, I suggest CORDIC, but I am not aware of the SOTA on fixed-point operations. @dmitry-kazakov also suggests Chebyshev polynomials.

In fact, it should be more “easy” to have a non-spark library, but a proven version could be a game changer for domains that require high precision and reproducibility.

Ping @AdaOrbit