Supported arithmetic

Rounding directions

Some of the classes of operators presented in the following sections are templated by a rounding direction. This is the direction chosen when converting a real number that cannot be exactly represented in the destination format.

There are eleven directions:

zr

toward zero

aw

away from zero

dn

toward minus infinity (down)

up

toward plus infinity

od

to odd mantissas

ne

to nearest, tie breaking to even mantissas

no

to nearest, tie breaking to odd mantissas

nz

to nearest, tie breaking toward zero

na

to nearest, tie breaking away from zero

nd

to nearest, tie breaking toward minus infinity

nu

to nearest, tie breaking toward plus infinity

The rounding directions mandated by the IEEE-754 standard are ne (default mode, rounding to nearest), zr, dn, up, and na (introduced for decimal arithmetic).

Floating-point operators

This class of operators covers all the formats whose number sets are \(F(p,d) = \{m \cdot 2^e; |m| < 2^p, e \ge d\}\). In particular, IEEE-754 floating-point formats (with subnormal numbers) are part of this class, if we set apart overflow issues. Both parameters p and d select a particular format. The last parameter selects the rounding direction.

float< precision, minimum_exponent, rounding_direction >(...)

Formats with no minimal exponent (and thus no underflow) are also available:

float< precision, rounding_direction >(...)

Having to remember the precision and minimum exponent parameters may be a bit tedious, so an alternate syntax is provided: instead of these two parameters, a name can be given to the float class.

float< name, rounding_direction >(...)

There are four predefined formats:

ieee_32

IEEE-754 single precision

ieee_64

IEEE-754 double precision

ieee_128

IEEE-754 quadruple precision

x86_80

extended precision on x86-like processors

Fixed-point operators

This class of operators covers all the formats whose number sets are \(F(e) = \{m \cdot 2^e\}\). The first parameter selects the weight of the least significant bit. The second parameter selects the rounding direction.

fixed< lsb_weight, rounding_direction >(...)

Rounding to integer is a special case of fixed point rounding of weight 0. A syntactic shortcut is provided.

int< rounding_direction >(...)

Miscellaneous operators

The following operators are underspecified and therefore not suitable for formal proofs.

Functions with relative error

This set of functions is defined with related theorems on relative error. They can be used to express properties that cannot be directly expressed through unary rounding operators.

{add|sub|mul}_rel< precision [, minimum_exponent] >(..., ...)

If the minimum exponent is not provided, the bound on the relative error is assumed to be valid on the entire domain. Otherwise the interval \([-2^e,2^e]\) is excluded from the domain.

Talking about the expression add_rel<20,-60>(a,b) is like talking about a fresh expression c such that not |a + b| <= 1b-60 -> |c -/ (a + b)| <= 1b-20.

Rounding operators with homogen properties

To be written.