Specify the non-integral calculations in Praos

[JaredCorduan]

This involves being aware of the error.

[mgudemann]

In the formal-spec meeting on Jan. 15th I gave a presentation on some research on doing verification for programs doing numerical calculations. @kantp can share the link to the video, the slides are available too

main outcomes:

• consistent results over all languages and architectures are highest priority
• reference implementation (C/Rust?) in addition to reference document
• Definition of desired properties before decision on what approach to use finally

general fp calculation requirements:

• exponential decay modeling
• exponentiation a^b where a, b \in [0, 1], i.e., ln(x), exp(x)

main approaches for implementation

• IEEE754 floating point
• rational numbers
• fixed-point

verification tools:

• SMT solvers, bitvectors for fixed-point, QF_FP for IEEE754
• gappa: interval artihmetic prover for IEEE754 and fixed-point
• Coq/Flocq: interactive prover for IEEE754

higher level tools:

• why3: ML like language, multiple solvers, provers
• SBV: Haskell library for SMT-based verification
• CBMC: bounded SW model checker with SMT solver for IEEE754 and bitvectors

Pro/Contra rationals

• arbitrary precision approximation
• standard mathematics for error estimation etc.
• nominators can get arbitrarily large
• no standard

Pro/Contra IEEE754

• standard
• verification tools available
• subtle differences in architectures with excess precision (e.g. 80bit internal registers, at least the D language uses maximal precision as default)
• single lovelace precision not for maximal ADA amount

Pro/Contra fixed-point

• verification tools available
• precision down to single lovelace can be defined by us
• unambiguous on all architectures
• no standard, but libraries available in general