WebAssembly Specification Release 1.1 (Draft 2021-12-18) - page 7

igt

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

• Return

1

if

𝑖

1

is greater than

𝑖

2

,

0

otherwise.

igt

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

bool

(

𝑖

1

> 𝑖

2

)

igt

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

• Let

𝑗

1

be the

signed interpretation

of

𝑖

1

.

• Let

𝑗

2

be the

signed interpretation

of

𝑖

2

.

• Return

1

if

𝑗

1

is greater than

𝑗

2

,

0

otherwise.

igt

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

=

bool

(

signed

𝑁

(

𝑖

1

)

>

signed

𝑁

(

𝑖

2

))

ile

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

• Return

1

if

𝑖

1

is less than or equal to

𝑖

2

,

0

otherwise.

ile

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

bool

(

𝑖

1

≤

𝑖

2

)

ile

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

• Let

𝑗

1

be the

signed interpretation

of

𝑖

1

.

• Let

𝑗

2

be the

signed interpretation

of

𝑖

2

.

• Return

1

if

𝑗

1

is less than or equal to

𝑗

2

,

0

otherwise.

ile

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

=

bool

(

signed

𝑁

(

𝑖

1

)

≤

signed

𝑁

(

𝑖

2

))

ige

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

• Return

1

if

𝑖

1

is greater than or equal to

𝑖

2

,

0

otherwise.

ige

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

bool

(

𝑖

1

≥

𝑖

2

)

ige

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

• Let

𝑗

1

be the

signed interpretation

of

𝑖

1

.

• Let

𝑗

2

be the

signed interpretation

of

𝑖

2

.

• Return

1

if

𝑗

1

is greater than or equal to

𝑗

2

,

0

otherwise.

ige

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

=

bool

(

signed

𝑁

(

𝑖

1

)

≥

signed

𝑁

(

𝑖

2

))

4.3. Numerics

71

iextend

𝑀

_

s

𝑁

(

𝑖

)

• Return

extend

s

𝑀,𝑁

(

𝑖

)

.

iextend

𝑀

_

s

𝑁

(

𝑖

)

=

extend

s

𝑀,𝑁

(

𝑖

)

ibitselect

𝑁

(

𝑖

1

, 𝑖

2

, 𝑖

3

)

• Let

𝑗

1

be the bitwise conjunction of

𝑖

1

and

𝑖

3

.

• Let

𝑗

′

3

be the bitwise negation of

𝑖

3

.

• Let

𝑗

2

be the bitwise conjunction of

𝑖

2

and

𝑗

′

3

.

• Return the bitwise disjunction of

𝑗

1

and

𝑗

2

.

ibitselect

𝑁

(

𝑖

1

, 𝑖

2

, 𝑖

3

)

=

ior

𝑁

(

iand

𝑁

(

𝑖

1

, 𝑖

3

)

,

iand

𝑁

(

𝑖

2

,

inot

𝑁

(

𝑖

3

)))

iabs

𝑁

(

𝑖

)

• Let

𝑗

be the

signed interpretation

of

𝑖

.

• If

𝑗

greater than or equal to

0

, then return

𝑖

.

• Else return the negation of

j

, modulo

2

𝑁

.

iabs

𝑁

(

𝑖

)

=

𝑖

(

if

signed

𝑁

(

𝑖

)

≥

0)

iabs

𝑁

(

𝑖

)

=

−

signed

𝑁

(

𝑖

) mod 2

𝑁

(

otherwise

)

ineg

𝑁

(

𝑖

)

• Return the result of negating

𝑖

, modulo

2

𝑁

.

ineg

𝑁

(

𝑖

)

=

(2

𝑁

−

𝑖

) mod 2

𝑁

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

• Return

𝑖

1

if

ilt

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

is

1

, return

𝑖

2

otherwise.

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

𝑖

1

(

if

ilt

_

u

𝑁

(

𝑖

1

, 𝑖

2

) = 1)

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

𝑖

2

(

otherwise

)

imin

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

• Return

𝑖

1

if

ilt

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

is

1

, return

𝑖

2

otherwise.

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

𝑖

1

(

if

ilt

_

s

𝑁

(

𝑖

1

, 𝑖

2

) = 1)

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

𝑖

2

(

otherwise

)

72

Chapter 4. Execution

imax

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

• Return

𝑖

1

if

igt

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

is

1

, return

𝑖

2

otherwise.

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

𝑖

1

(

if

igt

_

u

𝑁

(

𝑖

1

, 𝑖

2

) = 1)

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

𝑖

2

(

otherwise

)

imax

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

• Return

𝑖

1

if

igt

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

is

1

, return

𝑖

2

otherwise.

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

𝑖

1

(

if

igt

_

s

𝑁

(

𝑖

1

, 𝑖

2

) = 1)

imin

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

𝑖

2

(

otherwise

)

iaddsat

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

• Let

𝑖

be the result of adding

𝑖

1

and

𝑖

2

.

• Return

sat

u

𝑁

(

𝑖

)

.

iaddsat

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

sat

u

𝑁

(

𝑖

1

+

𝑖

2

)

iaddsat

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

• Let

𝑗

1

be the signed interpretation of

𝑖

1

• Let

𝑗

2

be the signed interpretation of

𝑖

2

• Let

𝑗

be the result of adding

𝑗

1

and

𝑗

2

.

• Return

sat

s

𝑁

(

𝑗

)

.

iaddsat

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

=

sat

s

𝑁

(

signed

𝑁

(

𝑖

1

) +

signed

𝑁

(

𝑖

2

))

isubsat

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

• Let

𝑖

be the result of subtracting

𝑖

2

from

𝑖

1

.

• Return

sat

u

𝑁

(

𝑖

)

.

isubsat

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

sat

u

𝑁

(

𝑖

1

−

𝑖

2

)

isubsat

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

• Let

𝑗

1

be the signed interpretation of

𝑖

1

• Let

𝑗

2

be the signed interpretation of

𝑖

2

• Let

𝑗

be the result of subtracting

𝑗

2

from

𝑗

1

.

• Return

sat

s

𝑁

(

𝑗

)

.

isubsat

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

=

sat

s

𝑁

(

signed

𝑁

(

𝑖

1

)

−

signed

𝑁

(

𝑖

2

))

4.3. Numerics

73

iavgr

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

• Let

𝑗

be the result of adding

𝑖

1

,

𝑖

2

, and

1

.

• Return the result of dividing

𝑗

by

2

, truncated toward zero.

iavgr

_

u

𝑁

(

𝑖

1

, 𝑖

2

)

=

trunc

((

𝑖

1

+

𝑖

2

+ 1)

/

2)

iq15mulrsat

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

• Return the result of

sat

s

𝑁

(

ishr

_

s

𝑁

(

𝑖

1

·

𝑖

2

+ 2

14

,

15))

.

iq15mulrsat

_

s

𝑁

(

𝑖

1

, 𝑖

2

)

=

sat

s

𝑁

(

ishr

_

s

𝑁

(

𝑖

1

·

𝑖

2

+ 2

14

,

15))

4.3.3 Floating-Point Operations

Floating-point arithmetic follows the

IEEE 754-2019

24

standard, with the following qualifications:

• All operators use round-to-nearest ties-to-even, except where otherwise specified. Non-default directed

rounding attributes are not supported.

• Following the recommendation that operators propagate

NaN

payloads from their operands is permitted but

not required.

• All operators use “non-stop” mode, and floating-point exceptions are not otherwise observable. In particular,

neither alternate floating-point exception handling attributes nor operators on status flags are supported.

There is no observable difference between quiet and signalling NaNs.

Note:

Some of these limitations may be lifted in future versions of WebAssembly.

Rounding

Rounding always is round-to-nearest ties-to-even, in correspondence with

IEEE 754-2019

25

(Section 4.3.1).

An

exact

floating-point number is a rational number that is exactly representable as a

floating-point number

of

given bit width

𝑁

.

A

limit

number for a given floating-point bit width

𝑁

is a positive or negative number whose magnitude is the

smallest power of

2

that is not exactly representable as a floating-point number of width

𝑁

(that magnitude is

2

128

for

𝑁

= 32

and

2

1024

for

𝑁

= 64

).

A

candidate

number is either an exact floating-point number or a positive or negative limit number for the given

bit width

𝑁

.

A

candidate pair

is a pair

𝑧

1

, 𝑧

2

of candidate numbers, such that no candidate number exists that lies between the

two.
A real number

𝑟

is converted to a floating-point value of bit width

𝑁

as follows:

• If

𝑟

is

0

, then return

+0

.

• Else if

𝑟

is an exact floating-point number, then return

𝑟

.

• Else if

𝑟

greater than or equal to the positive limit, then return

+

∞

.

• Else if

𝑟

is less than or equal to the negative limit, then return

−∞

.

• Else if

𝑧

1

and

𝑧

2

are a candidate pair such that

𝑧

1

< 𝑟 < 𝑧

2

, then:

24

https://ieeexplore.ieee.org/document/8766229

25

https://ieeexplore.ieee.org/document/8766229

74

Chapter 4. Execution

–

If

|

𝑟

−

𝑧

1

|

<

|

𝑟

−

𝑧

2

|

, then let

𝑧

be

𝑧

1

.

–

Else if

|

𝑟

−

𝑧

1

|

>

|

𝑟

−

𝑧

2

|

, then let

𝑧

be

𝑧

2

.

–

Else if

|

𝑟

−

𝑧

1

|

=

|

𝑟

−

𝑧

2

|

and the

significand

of

𝑧

1

is even, then let

𝑧

be

𝑧

1

.

–

Else, let

𝑧

be

𝑧

2

.

• If

𝑧

is

0

, then:

–

If

𝑟 <

0

, then return

−

0

.

–

Else, return

+0

.

• Else if

𝑧

is a limit number, then:

–

If

𝑟 <

0

, then return

−∞

.

–

Else, return

+

∞

.

• Else, return

𝑧

.

float

𝑁

(0)

=

+0

float

𝑁

(

𝑟

)

=

𝑟

(

if

𝑟

∈

exact

𝑁

)

float

𝑁

(

𝑟

)

=

+

∞

(

if

𝑟

≥

+limit

𝑁

)

float

𝑁

(

𝑟

)

=

−∞

(

if

𝑟

≤ −

limit

𝑁

)

float

𝑁

(

𝑟

)

=

closest

𝑁

(

𝑟, 𝑧

1

, 𝑧

2

)

(

if

𝑧

1

< 𝑟 < 𝑧

2

∧

(

𝑧

1

, 𝑧

2

)

∈

candidatepair

𝑁

)

closest

𝑁

(

𝑟, 𝑧

1

, 𝑧

2

)

=

rectify

𝑁

(

𝑟, 𝑧

1

)

(

if

|

𝑟

−

𝑧

1

|

<

|

𝑟

−

𝑧

2

|

)

closest

𝑁

(

𝑟, 𝑧

1

, 𝑧

2

)

=

rectify

𝑁

(

𝑟, 𝑧

2

)

(

if

|

𝑟

−

𝑧

1

|

>

|

𝑟

−

𝑧

2

|

)

closest

𝑁

(

𝑟, 𝑧

1

, 𝑧

2

)

=

rectify

𝑁

(

𝑟, 𝑧

1

)

(

if

|

𝑟

−

𝑧

1

|

=

|

𝑟

−

𝑧

2

| ∧

even

𝑁

(

𝑧

1

))

closest

𝑁

(

𝑟, 𝑧

1

, 𝑧

2

)

=

rectify

𝑁

(

𝑟, 𝑧

2

)

(

if

|

𝑟

−

𝑧

1

|

=

|

𝑟

−

𝑧

2

| ∧

even

𝑁

(

𝑧

2

))

rectify

𝑁

(

𝑟,

±

limit

𝑁

)

=

±∞

rectify

𝑁

(

𝑟,

0)

=

+0

(

𝑟

≥

0)

rectify

𝑁

(

𝑟,

0)

=

−

0

(

𝑟 <

0)

rectify

𝑁

(

𝑟, 𝑧

)

=

𝑧

where:

exact

𝑁

=

f

𝑁

∩

Q

limit

𝑁

=

2

2

expon

(

𝑁

)

−

1

candidate

𝑁

=

exact

𝑁

∪ {

+limit

𝑁

,

−

limit

𝑁

}

candidatepair

𝑁

=

{

(

𝑧

1

, 𝑧

2

)

∈

candidate

2

𝑁

|

𝑧

1

< 𝑧

2

∧ ∀

𝑧

∈

candidate

𝑁

, 𝑧

≤

𝑧

1

∨

𝑧

≥

𝑧

2

}

even

𝑁

((

𝑑

+

𝑚

·

2

−

𝑀

)

·

2

𝑒

)

⇔

𝑚

mod 2 = 0

even

𝑁

(

±

limit

𝑁

)

⇔

true

NaN Propagation

When the result of a floating-point operator other than

fneg

,

fabs

, or

fcopysign

is a

NaN

, then its sign is non-

deterministic and the

payload

is computed as follows:

• If the payload of all NaN inputs to the operator is

canonical

(including the case that there are no NaN inputs),

then the payload of the output is canonical as well.

• Otherwise the payload is picked non-deterministically among all

arithmetic NaNs

; that is, its most significant

bit is

1

and all others are unspecified.

This non-deterministic result is expressed by the following auxiliary function producing a set of allowed outputs

from a set of inputs:

nans

𝑁

{

𝑧

*

}

=

{

+

nan

(

𝑛

)

,

−

nan

(

𝑛

)

|

𝑛

=

canon

𝑁

}

(

if

∀

nan

(

𝑛

)

∈

𝑧

*

, 𝑛

=

canon

𝑁

)

nans

𝑁

{

𝑧

*

}

=

{

+

nan

(

𝑛

)

,

−

nan

(

𝑛

)

|

𝑛

≥

canon

𝑁

}

(

otherwise

)

4.3. Numerics

75

fadd

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return an element of

nans

𝑁

{

𝑧

1

, 𝑧

2

}

.

• Else if both

𝑧

1

and

𝑧

2

are infinities of opposite signs, then return an element of

nans

𝑁

{}

.

• Else if both

𝑧

1

and

𝑧

2

are infinities of equal sign, then return that infinity.

• Else if one of

𝑧

1

or

𝑧

2

is an infinity, then return that infinity.

• Else if both

𝑧

1

and

𝑧

2

are zeroes of opposite sign, then return positive zero.

• Else if both

𝑧

1

and

𝑧

2

are zeroes of equal sign, then return that zero.

• Else if one of

𝑧

1

or

𝑧

2

is a zero, then return the other operand.

• Else if both

𝑧

1

and

𝑧

2

are values with the same magnitude but opposite signs, then return positive zero.

• Else return the result of adding

𝑧

1

and

𝑧

2

,

rounded

to the nearest representable value.

fadd

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

2

}

fadd

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

1

}

fadd

𝑁

(

±∞

,

∓∞

)

=

nans

𝑁

{}

fadd

𝑁

(

±∞

,

±∞

)

=

±∞

fadd

𝑁

(

𝑧

1

,

±∞

)

=

±∞

fadd

𝑁

(

±∞

, 𝑧

2

)

=

±∞

fadd

𝑁

(

±

0

,

∓

0)

=

+0

fadd

𝑁

(

±

0

,

±

0)

=

±

0

fadd

𝑁

(

𝑧

1

,

±

0)

=

𝑧

1

fadd

𝑁

(

±

0

, 𝑧

2

)

=

𝑧

2

fadd

𝑁

(

±

𝑞,

∓

𝑞

)

=

+0

fadd

𝑁

(

𝑧

1

, 𝑧

2

)

=

float

𝑁

(

𝑧

1

+

𝑧

2

)

fsub

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return an element of

nans

𝑁

{

𝑧

1

, 𝑧

2

}

.

• Else if both

𝑧

1

and

𝑧

2

are infinities of equal signs, then return an element of

nans

𝑁

{}

.

• Else if both

𝑧

1

and

𝑧

2

are infinities of opposite sign, then return

𝑧

1

.

• Else if

𝑧

1

is an infinity, then return that infinity.

• Else if

𝑧

2

is an infinity, then return that infinity negated.

• Else if both

𝑧

1

and

𝑧

2

are zeroes of equal sign, then return positive zero.

• Else if both

𝑧

1

and

𝑧

2

are zeroes of opposite sign, then return

𝑧

1

.

• Else if

𝑧

2

is a zero, then return

𝑧

1

.

• Else if

𝑧

1

is a zero, then return

𝑧

2

negated.

• Else if both

𝑧

1

and

𝑧

2

are the same value, then return positive zero.

• Else return the result of subtracting

𝑧

2

from

𝑧

1

,

rounded

to the nearest representable value.

76

Chapter 4. Execution

fsub

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

2

}

fsub

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

1

}

fsub

𝑁

(

±∞

,

±∞

)

=

nans

𝑁

{}

fsub

𝑁

(

±∞

,

∓∞

)

=

±∞

fsub

𝑁

(

𝑧

1

,

±∞

)

=

∓∞

fsub

𝑁

(

±∞

, 𝑧

2

)

=

±∞

fsub

𝑁

(

±

0

,

±

0)

=

+0

fsub

𝑁

(

±

0

,

∓

0)

=

±

0

fsub

𝑁

(

𝑧

1

,

±

0)

=

𝑧

1

fsub

𝑁

(

±

0

,

±

𝑞

2

)

=

∓

𝑞

2

fsub

𝑁

(

±

𝑞,

±

𝑞

)

=

+0

fsub

𝑁

(

𝑧

1

, 𝑧

2

)

=

float

𝑁

(

𝑧

1

−

𝑧

2

)

Note:

Up to the non-determinism regarding NaNs, it always holds that

fsub

𝑁

(

𝑧

1

, 𝑧

2

) =

fadd

𝑁

(

𝑧

1

,

fneg

𝑁

(

𝑧

2

))

.

fmul

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return an element of

nans

𝑁

{

𝑧

1

, 𝑧

2

}

.

• Else if one of

𝑧

1

and

𝑧

2

is a zero and the other an infinity, then return an element of

nans

𝑁

{}

.

• Else if both

𝑧

1

and

𝑧

2

are infinities of equal sign, then return positive infinity.

• Else if both

𝑧

1

and

𝑧

2

are infinities of opposite sign, then return negative infinity.

• Else if one of

𝑧

1

or

𝑧

2

is an infinity and the other a value with equal sign, then return positive infinity.

• Else if one of

𝑧

1

or

𝑧

2

is an infinity and the other a value with opposite sign, then return negative infinity.

• Else if both

𝑧

1

and

𝑧

2

are zeroes of equal sign, then return positive zero.

• Else if both

𝑧

1

and

𝑧

2

are zeroes of opposite sign, then return negative zero.

• Else return the result of multiplying

𝑧

1

and

𝑧

2

,

rounded

to the nearest representable value.

fmul

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

2

}

fmul

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

1

}

fmul

𝑁

(

±∞

,

±

0)

=

nans

𝑁

{}

fmul

𝑁

(

±∞

,

∓

0)

=

nans

𝑁

{}

fmul

𝑁

(

±

0

,

±∞

)

=

nans

𝑁

{}

fmul

𝑁

(

±

0

,

∓∞

)

=

nans

𝑁

{}

fmul

𝑁

(

±∞

,

±∞

)

=

+

∞

fmul

𝑁

(

±∞

,

∓∞

)

=

−∞

fmul

𝑁

(

±

𝑞

1

,

±∞

)

=

+

∞

fmul

𝑁

(

±

𝑞

1

,

∓∞

)

=

−∞

fmul

𝑁

(

±∞

,

±

𝑞

2

)

=

+

∞

fmul

𝑁

(

±∞

,

∓

𝑞

2

)

=

−∞

fmul

𝑁

(

±

0

,

±

0)

=

+0

fmul

𝑁

(

±

0

,

∓

0)

=

−

0

fmul

𝑁

(

𝑧

1

, 𝑧

2

)

=

float

𝑁

(

𝑧

1

·

𝑧

2

)

4.3. Numerics

77

fdiv

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return an element of

nans

𝑁

{

𝑧

1

, 𝑧

2

}

.

• Else if both

𝑧

1

and

𝑧

2

are infinities, then return an element of

nans

𝑁

{}

.

• Else if both

𝑧

1

and

𝑧

2

are zeroes, then return an element of

nans

𝑁

{

𝑧

1

, 𝑧

2

}

.

• Else if

𝑧

1

is an infinity and

𝑧

2

a value with equal sign, then return positive infinity.

• Else if

𝑧

1

is an infinity and

𝑧

2

a value with opposite sign, then return negative infinity.

• Else if

𝑧

2

is an infinity and

𝑧

1

a value with equal sign, then return positive zero.

• Else if

𝑧

2

is an infinity and

𝑧

1

a value with opposite sign, then return negative zero.

• Else if

𝑧

1

is a zero and

𝑧

2

a value with equal sign, then return positive zero.

• Else if

𝑧

1

is a zero and

𝑧

2

a value with opposite sign, then return negative zero.

• Else if

𝑧

2

is a zero and

𝑧

1

a value with equal sign, then return positive infinity.

• Else if

𝑧

2

is a zero and

𝑧

1

a value with opposite sign, then return negative infinity.

• Else return the result of dividing

𝑧

1

by

𝑧

2

,

rounded

to the nearest representable value.

fdiv

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

2

}

fdiv

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

1

}

fdiv

𝑁

(

±∞

,

±∞

)

=

nans

𝑁

{}

fdiv

𝑁

(

±∞

,

∓∞

)

=

nans

𝑁

{}

fdiv

𝑁

(

±

0

,

±

0)

=

nans

𝑁

{}

fdiv

𝑁

(

±

0

,

∓

0)

=

nans

𝑁

{}

fdiv

𝑁

(

±∞

,

±

𝑞

2

)

=

+

∞

fdiv

𝑁

(

±∞

,

∓

𝑞

2

)

=

−∞

fdiv

𝑁

(

±

𝑞

1

,

±∞

)

=

+0

fdiv

𝑁

(

±

𝑞

1

,

∓∞

)

=

−

0

fdiv

𝑁

(

±

0

,

±

𝑞

2

)

=

+0

fdiv

𝑁

(

±

0

,

∓

𝑞

2

)

=

−

0

fdiv

𝑁

(

±

𝑞

1

,

±

0)

=

+

∞

fdiv

𝑁

(

±

𝑞

1

,

∓

0)

=

−∞

fdiv

𝑁

(

𝑧

1

, 𝑧

2

)

=

float

𝑁

(

𝑧

1

/𝑧

2

)

fmin

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return an element of

nans

𝑁

{

𝑧

1

, 𝑧

2

}

.

• Else if one of

𝑧

1

or

𝑧

2

is a negative infinity, then return negative infinity.

• Else if one of

𝑧

1

or

𝑧

2

is a positive infinity, then return the other value.

• Else if both

𝑧

1

and

𝑧

2

are zeroes of opposite signs, then return negative zero.

• Else return the smaller value of

𝑧

1

and

𝑧

2

.

fmin

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

2

}

fmin

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

1

}

fmin

𝑁

(+

∞

, 𝑧

2

)

=

𝑧

2

fmin

𝑁

(

−∞

, 𝑧

2

)

=

−∞

fmin

𝑁

(

𝑧

1

,

+

∞

)

=

𝑧

1

fmin

𝑁

(

𝑧

1

,

−∞

)

=

−∞

fmin

𝑁

(

±

0

,

∓

0)

=

−

0

fmin

𝑁

(

𝑧

1

, 𝑧

2

)

=

𝑧

1

(

if

𝑧

1

≤

𝑧

2

)

fmin

𝑁

(

𝑧

1

, 𝑧

2

)

=

𝑧

2

(

if

𝑧

2

≤

𝑧

1

)

78

Chapter 4. Execution

fmax

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return an element of

nans

𝑁

{

𝑧

1

, 𝑧

2

}

.

• Else if one of

𝑧

1

or

𝑧

2

is a positive infinity, then return positive infinity.

• Else if one of

𝑧

1

or

𝑧

2

is a negative infinity, then return the other value.

• Else if both

𝑧

1

and

𝑧

2

are zeroes of opposite signs, then return positive zero.

• Else return the larger value of

𝑧

1

and

𝑧

2

.

fmax

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

2

}

fmax

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

, 𝑧

1

}

fmax

𝑁

(+

∞

, 𝑧

2

)

=

+

∞

fmax

𝑁

(

−∞

, 𝑧

2

)

=

𝑧

2

fmax

𝑁

(

𝑧

1

,

+

∞

)

=

+

∞

fmax

𝑁

(

𝑧

1

,

−∞

)

=

𝑧

1

fmax

𝑁

(

±

0

,

∓

0)

=

+0

fmax

𝑁

(

𝑧

1

, 𝑧

2

)

=

𝑧

1

(

if

𝑧

1

≥

𝑧

2

)

fmax

𝑁

(

𝑧

1

, 𝑧

2

)

=

𝑧

2

(

if

𝑧

2

≥

𝑧

1

)

fcopysign

𝑁

(

𝑧

1

, 𝑧

2

)

• If

𝑧

1

and

𝑧

2

have the same sign, then return

𝑧

1

.

• Else return

𝑧

1

with negated sign.

fcopysign

𝑁

(

±

𝑝

1

,

±

𝑝

2

)

=

±

𝑝

1

fcopysign

𝑁

(

±

𝑝

1

,

∓

𝑝

2

)

=

∓

𝑝

1

fabs

𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return

𝑧

with positive sign.

• Else if

𝑧

is an infinity, then return positive infinity.

• Else if

𝑧

is a zero, then return positive zero.

• Else if

𝑧

is a positive value, then

𝑧

.

• Else return

𝑧

negated.

fabs

𝑁

(

±

nan

(

𝑛

))

=

+

nan

(

𝑛

)

fabs

𝑁

(

±∞

)

=

+

∞

fabs

𝑁

(

±

0)

=

+0

fabs

𝑁

(

±

𝑞

)

=

+

𝑞

fneg

𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return

𝑧

with negated sign.

• Else if

𝑧

is an infinity, then return that infinity negated.

• Else if

𝑧

is a zero, then return that zero negated.

• Else return

𝑧

negated.

fneg

𝑁

(

±

nan

(

𝑛

))

=

∓

nan

(

𝑛

)

fneg

𝑁

(

±∞

)

=

∓∞

fneg

𝑁

(

±

0)

=

∓

0

fneg

𝑁

(

±

𝑞

)

=

∓

𝑞

4.3. Numerics

79

fsqrt

𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return an element of

nans

𝑁

{

𝑧

}

.

• Else if

𝑧

is negative infinity, then return an element of

nans

𝑁

{}

.

• Else if

𝑧

is positive infinity, then return positive infinity.

• Else if

𝑧

is a zero, then return that zero.

• Else if

𝑧

has a negative sign, then return an element of

nans

𝑁

{}

.

• Else return the square root of

𝑧

.

fsqrt

𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

}

fsqrt

𝑁

(

−∞

)

=

nans

𝑁

{}

fsqrt

𝑁

(+

∞

)

=

+

∞

fsqrt

𝑁

(

±

0)

=

±

0

fsqrt

𝑁

(

−

𝑞

)

=

nans

𝑁

{}

fsqrt

𝑁

(+

𝑞

)

=

float

𝑁

(︀

√

𝑞

)︀

fceil

𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return an element of

nans

𝑁

{

𝑧

}

.

• Else if

𝑧

is an infinity, then return

𝑧

.

• Else if

𝑧

is a zero, then return

𝑧

.

• Else if

𝑧

is smaller than

0

but greater than

−

1

, then return negative zero.

• Else return the smallest integral value that is not smaller than

𝑧

.

fceil

𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

}

fceil

𝑁

(

±∞

)

=

±∞

fceil

𝑁

(

±

0)

=

±

0

fceil

𝑁

(

−

𝑞

)

=

−

0

(

if

−

1

<

−

𝑞 <

0)

fceil

𝑁

(

±

𝑞

)

=

float

𝑁

(

𝑖

)

(

if

±

𝑞

≤

𝑖 <

±

𝑞

+ 1)

ffloor

𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return an element of

nans

𝑁

{

𝑧

}

.

• Else if

𝑧

is an infinity, then return

𝑧

.

• Else if

𝑧

is a zero, then return

𝑧

.

• Else if

𝑧

is greater than

0

but smaller than

1

, then return positive zero.

• Else return the largest integral value that is not larger than

𝑧

.

ffloor

𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

}

ffloor

𝑁

(

±∞

)

=

±∞

ffloor

𝑁

(

±

0)

=

±

0

ffloor

𝑁

(+

𝑞

)

=

+0

(

if

0

<

+

𝑞 <

1)

ffloor

𝑁

(

±

𝑞

)

=

float

𝑁

(

𝑖

)

(

if

±

𝑞

−

1

< 𝑖

≤ ±

𝑞

)

80

Chapter 4. Execution

ftrunc

𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return an element of

nans

𝑁

{

𝑧

}

.

• Else if

𝑧

is an infinity, then return

𝑧

.

• Else if

𝑧

is a zero, then return

𝑧

.

• Else if

𝑧

is greater than

0

but smaller than

1

, then return positive zero.

• Else if

𝑧

is smaller than

0

but greater than

−

1

, then return negative zero.

• Else return the integral value with the same sign as

𝑧

and the largest magnitude that is not larger than the

magnitude of

𝑧

.

ftrunc

𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

}

ftrunc

𝑁

(

±∞

)

=

±∞

ftrunc

𝑁

(

±

0)

=

±

0

ftrunc

𝑁

(+

𝑞

)

=

+0

(

if

0

<

+

𝑞 <

1)

ftrunc

𝑁

(

−

𝑞

)

=

−

0

(

if

−

1

<

−

𝑞 <

0)

ftrunc

𝑁

(

±

𝑞

)

=

float

𝑁

(

±

𝑖

)

(

if

+

𝑞

−

1

< 𝑖

≤

+

𝑞

)

fnearest

𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return an element of

nans

𝑁

{

𝑧

}

.

• Else if

𝑧

is an infinity, then return

𝑧

.

• Else if

𝑧

is a zero, then return

𝑧

.

• Else if

𝑧

is greater than

0

but smaller than or equal to

0

.

5

, then return positive zero.

• Else if

𝑧

is smaller than

0

but greater than or equal to

−

0

.

5

, then return negative zero.

• Else return the integral value that is nearest to

𝑧

; if two values are equally near, return the even one.

fnearest

𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{±

nan

(

𝑛

)

}

fnearest

𝑁

(

±∞

)

=

±∞

fnearest

𝑁

(

±

0)

=

±

0

fnearest

𝑁

(+

𝑞

)

=

+0

(

if

0

<

+

𝑞

≤

0

.

5)

fnearest

𝑁

(

−

𝑞

)

=

−

0

(

if

−

0

.

5

≤ −

𝑞 <

0)

fnearest

𝑁

(

±

𝑞

)

=

float

𝑁

(

±

𝑖

)

(

if

|

𝑖

−

𝑞

|

<

0

.

5)

fnearest

𝑁

(

±

𝑞

)

=

float

𝑁

(

±

𝑖

)

(

if

|

𝑖

−

𝑞

|

= 0

.

5

∧

𝑖

even

)

feq

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return

0

.

• Else if both

𝑧

1

and

𝑧

2

are zeroes, then return

1

.

• Else if both

𝑧

1

and

𝑧

2

are the same value, then return

1

.

• Else return

0

.

feq

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

0

feq

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

0

feq

𝑁

(

±

0

,

∓

0)

=

1

feq

𝑁

(

𝑧

1

, 𝑧

2

)

=

bool

(

𝑧

1

=

𝑧

2

)

4.3. Numerics

81

fne

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return

1

.

• Else if both

𝑧

1

and

𝑧

2

are zeroes, then return

0

.

• Else if both

𝑧

1

and

𝑧

2

are the same value, then return

0

.

• Else return

1

.

fne

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

1

fne

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

1

fne

𝑁

(

±

0

,

∓

0)

=

0

fne

𝑁

(

𝑧

1

, 𝑧

2

)

=

bool

(

𝑧

1

̸

=

𝑧

2

)

flt

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return

0

.

• Else if

𝑧

1

and

𝑧

2

are the same value, then return

0

.

• Else if

𝑧

1

is positive infinity, then return

0

.

• Else if

𝑧

1

is negative infinity, then return

1

.

• Else if

𝑧

2

is positive infinity, then return

1

.

• Else if

𝑧

2

is negative infinity, then return

0

.

• Else if both

𝑧

1

and

𝑧

2

are zeroes, then return

0

.

• Else if

𝑧

1

is smaller than

𝑧

2

, then return

1

.

• Else return

0

.

flt

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

0

flt

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

0

flt

𝑁

(

𝑧, 𝑧

)

=

0

flt

𝑁

(+

∞

, 𝑧

2

)

=

0

flt

𝑁

(

−∞

, 𝑧

2

)

=

1

flt

𝑁

(

𝑧

1

,

+

∞

)

=

1

flt

𝑁

(

𝑧

1

,

−∞

)

=

0

flt

𝑁

(

±

0

,

∓

0)

=

0

flt

𝑁

(

𝑧

1

, 𝑧

2

)

=

bool

(

𝑧

1

< 𝑧

2

)

fgt

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return

0

.

• Else if

𝑧

1

and

𝑧

2

are the same value, then return

0

.

• Else if

𝑧

1

is positive infinity, then return

1

.

• Else if

𝑧

1

is negative infinity, then return

0

.

• Else if

𝑧

2

is positive infinity, then return

0

.

• Else if

𝑧

2

is negative infinity, then return

1

.

• Else if both

𝑧

1

and

𝑧

2

are zeroes, then return

0

.

• Else if

𝑧

1

is larger than

𝑧

2

, then return

1

.

• Else return

0

.

82

Chapter 4. Execution

fgt

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

0

fgt

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

0

fgt

𝑁

(

𝑧, 𝑧

)

=

0

fgt

𝑁

(+

∞

, 𝑧

2

)

=

1

fgt

𝑁

(

−∞

, 𝑧

2

)

=

0

fgt

𝑁

(

𝑧

1

,

+

∞

)

=

0

fgt

𝑁

(

𝑧

1

,

−∞

)

=

1

fgt

𝑁

(

±

0

,

∓

0)

=

0

fgt

𝑁

(

𝑧

1

, 𝑧

2

)

=

bool

(

𝑧

1

> 𝑧

2

)

fle

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return

0

.

• Else if

𝑧

1

and

𝑧

2

are the same value, then return

1

.

• Else if

𝑧

1

is positive infinity, then return

0

.

• Else if

𝑧

1

is negative infinity, then return

1

.

• Else if

𝑧

2

is positive infinity, then return

1

.

• Else if

𝑧

2

is negative infinity, then return

0

.

• Else if both

𝑧

1

and

𝑧

2

are zeroes, then return

1

.

• Else if

𝑧

1

is smaller than or equal to

𝑧

2

, then return

1

.

• Else return

0

.

fle

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

0

fle

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

0

fle

𝑁

(

𝑧, 𝑧

)

=

1

fle

𝑁

(+

∞

, 𝑧

2

)

=

0

fle

𝑁

(

−∞

, 𝑧

2

)

=

1

fle

𝑁

(

𝑧

1

,

+

∞

)

=

1

fle

𝑁

(

𝑧

1

,

−∞

)

=

0

fle

𝑁

(

±

0

,

∓

0)

=

1

fle

𝑁

(

𝑧

1

, 𝑧

2

)

=

bool

(

𝑧

1

≤

𝑧

2

)

fge

𝑁

(

𝑧

1

, 𝑧

2

)

• If either

𝑧

1

or

𝑧

2

is a NaN, then return

0

.

• Else if

𝑧

1

and

𝑧

2

are the same value, then return

1

.

• Else if

𝑧

1

is positive infinity, then return

1

.

• Else if

𝑧

1

is negative infinity, then return

0

.

• Else if

𝑧

2

is positive infinity, then return

0

.

• Else if

𝑧

2

is negative infinity, then return

1

.

• Else if both

𝑧

1

and

𝑧

2

are zeroes, then return

1

.

• Else if

𝑧

1

is smaller than or equal to

𝑧

2

, then return

1

.

• Else return

0

.

4.3. Numerics

83

fge

𝑁

(

±

nan

(

𝑛

)

, 𝑧

2

)

=

0

fge

𝑁

(

𝑧

1

,

±

nan

(

𝑛

))

=

0

fge

𝑁

(

𝑧, 𝑧

)

=

1

fge

𝑁

(+

∞

, 𝑧

2

)

=

1

fge

𝑁

(

−∞

, 𝑧

2

)

=

0

fge

𝑁

(

𝑧

1

,

+

∞

)

=

0

fge

𝑁

(

𝑧

1

,

−∞

)

=

1

fge

𝑁

(

±

0

,

∓

0)

=

1

fge

𝑁

(

𝑧

1

, 𝑧

2

)

=

bool

(

𝑧

1

≥

𝑧

2

)

fpmin

𝑁

(

𝑧

1

, 𝑧

2

)

• If

𝑧

2

is less than

𝑧

1

then return

𝑧

2

.

• Else return

𝑧

1

.

fpmin

𝑁

(

𝑧

1

, 𝑧

2

)

=

𝑧

2

(

if

flt

𝑁

(

𝑧

2

, 𝑧

1

) = 1)

fpmin

𝑁

(

𝑧

1

, 𝑧

2

)

=

𝑧

1

(

otherwise

)

fpmax

𝑁

(

𝑧

1

, 𝑧

2

)

• If

𝑧

1

is less than

𝑧

2

then return

𝑧

2

.

• Else return

𝑧

1

.

fpmax

𝑁

(

𝑧

1

, 𝑧

2

)

=

𝑧

2

(

if

flt

𝑁

(

𝑧

1

, 𝑧

2

) = 1)

fpmax

𝑁

(

𝑧

1

, 𝑧

2

)

=

𝑧

1

(

otherwise

)

4.3.4 Conversions

extend

u

𝑀,𝑁

(

𝑖

)

• Return

𝑖

.

extend

u

𝑀,𝑁

(

𝑖

)

=

𝑖

Note:

In the abstract syntax, unsigned extension just reinterprets the same value.

extend

s

𝑀,𝑁

(

𝑖

)

• Let

𝑗

be the

signed interpretation

of

𝑖

of size

𝑀

.

• Return the two’s complement of

𝑗

relative to size

𝑁

.

extend

s

𝑀,𝑁

(

𝑖

)

=

signed

−

1

𝑁

(

signed

𝑀

(

𝑖

))

84

Chapter 4. Execution

wrap

𝑀,𝑁

(

𝑖

)

• Return

𝑖

modulo

2

𝑁

.

wrap

𝑀,𝑁

(

𝑖

)

=

𝑖

mod 2

𝑁

trunc

u

𝑀,𝑁

(

𝑧

)

• If

𝑧

is a NaN, then the result is undefined.

• Else if

𝑧

is an infinity, then the result is undefined.

• Else if

𝑧

is a number and

trunc

(

𝑧

)

is a value within range of the target type, then return that value.

• Else the result is undefined.

trunc

u

𝑀,𝑁

(

±

nan

(

𝑛

))

=

{}

trunc

u

𝑀,𝑁

(

±∞

)

=

{}

trunc

u

𝑀,𝑁

(

±

𝑞

)

=

trunc

(

±

𝑞

)

(

if

−

1

<

trunc

(

±

𝑞

)

<

2

𝑁

)

trunc

u

𝑀,𝑁

(

±

𝑞

)

=

{}

(

otherwise

)

Note:

This operator is

partial

. It is not defined for NaNs, infinities, or values for which the result is out of range.

trunc

s

𝑀,𝑁

(

𝑧

)

• If

𝑧

is a NaN, then the result is undefined.

• Else if

𝑧

is an infinity, then the result is undefined.

• If

𝑧

is a number and

trunc

(

𝑧

)

is a value within range of the target type, then return that value.

• Else the result is undefined.

trunc

s

𝑀,𝑁

(

±

nan

(

𝑛

))

=

{}

trunc

s

𝑀,𝑁

(

±∞

)

=

{}

trunc

s

𝑀,𝑁

(

±

𝑞

)

=

trunc

(

±

𝑞

)

(

if

−

2

𝑁

−

1

−

1

<

trunc

(

±

𝑞

)

<

2

𝑁

−

1

)

trunc

s

𝑀,𝑁

(

±

𝑞

)

=

{}

(

otherwise

)

Note:

This operator is

partial

. It is not defined for NaNs, infinities, or values for which the result is out of range.

trunc

_

sat

_

u

𝑀,𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return

0

.

• Else if

𝑧

is negative infinity, then return

0

.

• Else if

𝑧

is positive infinity, then return

2

𝑁

−

1

.

• Else, return

sat

u

𝑁

(

trunc

(

𝑧

))

.

trunc

_

sat

_

u

𝑀,𝑁

(

±

nan

(

𝑛

))

=

0

trunc

_

sat

_

u

𝑀,𝑁

(

−∞

)

=

0

trunc

_

sat

_

u

𝑀,𝑁

(+

∞

)

=

2

𝑁

−

1

trunc

_

sat

_

u

𝑀,𝑁

(

𝑧

)

=

sat

u

𝑁

(

trunc

(

𝑧

))

4.3. Numerics

85

trunc

_

sat

_

s

𝑀,𝑁

(

𝑧

)

• If

𝑧

is a NaN, then return

0

.

• Else if

𝑧

is negative infinity, then return

−

2

𝑁

−

1

.

• Else if

𝑧

is positive infinity, then return

2

𝑁

−

1

−

1

.

• Else, return

sat

s

𝑁

(

trunc

(

𝑧

))

.

trunc

_

sat

_

s

𝑀,𝑁

(

±

nan

(

𝑛

))

=

0

trunc

_

sat

_

s

𝑀,𝑁

(

−∞

)

=

−

2

𝑁

−

1

trunc

_

sat

_

s

𝑀,𝑁

(+

∞

)

=

2

𝑁

−

1

−

1

trunc

_

sat

_

s

𝑀,𝑁

(

𝑧

)

=

sat

s

𝑁

(

trunc

(

𝑧

))

promote

𝑀,𝑁

(

𝑧

)

• If

𝑧

is a

canonical NaN

, then return an element of

nans

𝑁

{}

(i.e., a canonical NaN of size

𝑁

).

• Else if

𝑧

is a NaN, then return an element of

nans

𝑁

{±

nan

(1)

}

(i.e., any

arithmetic NaN

of size

𝑁

).

• Else, return

𝑧

.

promote

𝑀,𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{}

(

if

𝑛

=

canon

𝑁

)

promote

𝑀,𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{

+

nan

(1)

}

(

otherwise

)

promote

𝑀,𝑁

(

𝑧

)

=

𝑧

demote

𝑀,𝑁

(

𝑧

)

• If

𝑧

is a

canonical NaN

, then return an element of

nans

𝑁

{}

(i.e., a canonical NaN of size

𝑁

).

• Else if

𝑧

is a NaN, then return an element of

nans

𝑁

{±

nan

(1)

}

(i.e., any NaN of size

𝑁

).

• Else if

𝑧

is an infinity, then return that infinity.

• Else if

𝑧

is a zero, then return that zero.

• Else, return

float

𝑁

(

𝑧

)

.

demote

𝑀,𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{}

(

if

𝑛

=

canon

𝑁

)

demote

𝑀,𝑁

(

±

nan

(

𝑛

))

=

nans

𝑁

{

+

nan

(1)

}

(

otherwise

)

demote

𝑀,𝑁

(

±∞

)

=

±∞

demote

𝑀,𝑁

(

±

0)

=

±

0

demote

𝑀,𝑁

(

±

𝑞

)

=

float

𝑁

(

±

𝑞

)

convert

u

𝑀,𝑁

(

𝑖

)

• Return

float

𝑁

(

𝑖

)

.

convert

u

𝑀,𝑁

(

𝑖

)

=

float

𝑁

(

𝑖

)

86

Chapter 4. Execution