Result#

A result holds everything ExactRef works out for one call: the exact answer rounded to the output format, certified enclosures of the exact answer, and the bounds that say which outputs a correct implementation can produce.

Every operation returns an er.Result. Results walks through it with examples; this page lists every method.

At a glance#

Attribute or method	What it gives
`r.rounded`	the exact answer, rounded once to the output format
`r.exact`	certified enclosures of the exact answer
`r.guarantee`	`"correctly_rounded"`, or `"exact"` for integer outputs
`r.tolerance()`	per element, how far a correct implementation's finite output can be from `rounded`
`r.finite_range()`	the lowest and highest finite output a correct implementation can produce
`r.may_be(kind)`	where a correct implementation may output `"+inf"`, `"-inf"` or `"nan"`
`r.covers(output)`	per element, whether a correct implementation can produce `output`
`r.normal()`	the output of normal accumulation in index order, emulated exactly
`r.backward(grad)`	the operation's backward on the same inputs
`r[name]`	a result for one of several outputs
`r.reshape(shape)`, `r.transpose(i, j)`	the same result in another layout
`r.boundaries`	the operation's required rounding steps
`r.op`	the operation's name

tolerance(), finite_range(), may_be() and covers() take the same options: compute, ulps, flush_to_zero and standard.

Full specification#

class Result#

What an operation definition returns.

rounded: the exact answer rounded once to the output format.
exact: the exact answer as certified enclosures (ExactArray).
tolerance(): how far normal accumulation's finite output can be from rounded on these inputs, a proven bound; tolerance(standard="any_order") covers every accumulation order that does not overflow.
finite_range(), may_be() and covers(): the lowest and highest finite output, the infinities and NaN an implementation may produce, and the judgment of an implementation's output.
normal(): the output of normal accumulation in index order on these inputs, computed when asked for.

For one output these are the arrays themselves; several outputs use PyTorch's names, for example result.rounded.Q, and result["Q"] is a result holding just that output. guarantee states what rounded satisfies, and boundaries lists the operation's required rounding boundaries. backward(grad) runs the operation's backward from the same inputs.

A result with one output can be passed in place of an array to any operation, backward or algorithm. The implementation under test stored that output, so each stored value is one this result's bounds allow: within its tolerance of rounded (part by part for complex values), or an infinity or NaN that may_be() allows. The later result's rounded and exact are the exact answer on rounded, rounded once; its bounds cover every value these bounds allow, taken with the same arguments: an infinite radius leaves no bound in the outputs it reaches, and a stored infinity or NaN passes on as their flags (proofs/foundations.md, Results as inputs); its normal() works on this normal(); and an algorithm's run() uses rounded.

Operations build results from results through three internal methods, their interface to this class: _single (the one output's rounded), _bounds_of (its bounds for tolerance arguments) and _with_bounds (this result with other bounds).

guarantee#: What rounded satisfies: "correctly_rounded" for floating-point and complex outputs, "exact" for integer outputs.

op#: The operation's name, such as "matmul" or "matmul.backward".

tolerance(compute=None, *, ulps=None, flush_to_zero: bool = False, standard: str = 'normal')#

Worst-case |implementation output - rounded| per element.

The bound covers every implementation that loses precision only at the operation's required boundaries:

one rounding to compute at each required rounding boundary,
accumulation in compute: with standard="normal" (the default), normal accumulation, which adds in index order or in 2 or 4 SIMD-style lanes, rounds each product and then adds it, and starts a new partial sum where adding the next value would overflow; with standard="any_order", any order (any summation tree, with or without fused multiply-add) that does not overflow,
library functions within ulps units in the last place of compute, and for matrix functions a backward error measured in ulps (see each operation),
the final rounding to the output format.

An output within the normal tolerance is no worse than normal accumulation can be. Beyond it but within the any-order tolerance, it is technically correct but worse than normal accumulation can be (for example from a poor accumulation order). Beyond the any-order tolerance, no implementation that rounds only there without overflowing could produce it. Matrix functions bound a backward error instead and give the same tolerance for both standards.

compute defaults to float32 for inputs narrower than float32 and to the input format otherwise. With flush_to_zero, the implementation flushes subnormal values of the compute format to zero, as torch.set_flush_denormal(True) does: such a value may be read as zero, and a result that would be one may be produced as zero.

The result is a float64 array rounded upward, counting only finite output values the output format can represent. For complex outputs it is complex128 with one bound per part: its real part bounds |Re(output - rounded)| and its imaginary part |Im(output - rounded)|. A finite reference gets a finite tolerance wherever its finite outputs can be bounded; inf marks elements with no finite bound, and nan elements whose reference is not finite. finite_range() gives the lowest and highest finite output, may_be() the infinities and NaN an implementation may produce, and covers() judges an implementation's output. Results are kept, so repeating a call with the same arguments returns at once. Each operation's bound is proven in proofs/.

finite_range(compute=None, *, ulps=None, flush_to_zero: bool = False, standard: str = 'normal')#

The lowest and highest finite output of a correct implementation, per element, as (low, high) arrays of the output's dtype; the arguments are tolerance()'s.

They lie within tolerance() of rounded, and can be closer on one side. Where the reference is an infinity only because a finite exact value rounds past the largest finite value, they hold the finite outputs that can still occur. Where no finite output can occur, both are NaN, so low <= output <= high is false.

may_be(kind: str, compute=None, *, ulps=None, flush_to_zero: bool = False, standard: str = 'normal')#: Where a correct implementation may output kind ("+inf", "-inf" or "nan"), as a bool array; for complex outputs it has a last axis of 2 (real part, imaginary part). The other arguments are tolerance()'s. A reference that is not finite counts, and formats without infinity produce NaN where a value overflows. It can be true where no correct implementation overflows (an overflow check uses the error bound), never false where one can.

covers(output, compute=None, *, ulps=None, flush_to_zero: bool = False, standard: str = 'normal')#

Where a correct implementation can produce output, as a bool array: a finite value within finite_range(), or an infinity or NaN that may_be() allows.

output is an implementation's output (anything asarray takes) with this result's dtype and shape; for complex outputs the array has a last axis of 2 (real part, imaginary part). assert result.covers(output).all() checks an implementation. The other arguments are tolerance()'s; the standard, the compute format and flushing describe the implementations judged correct. A result with several outputs is checked one output at a time, as result[name].

normal(compute=None, *, flush_to_zero: bool = False)#

The output of normal accumulation in index order on these inputs.

Each product is rounded to compute and added in index order, each sum rounded to compute (to nearest, ties to even); where adding the next value would overflow, it starts a new partial sum, and the partial sums are then combined the same way. The result is rounded to the output format as rounded is. compute and flush_to_zero are as in tolerance(); each operation says what else its normal answer fixes. It is computed only when called, and kept.

reshape(shape) -> Result#

This one-output result with its elements in row-major order in a new shape.

Moving elements rounds nothing: rounded, exact, tolerance() and normal() are this result's, moved the same way, so the view can be passed to a later operation in place of an array. A view has no backward of its own: call backward on this result, with the gradient reshaped back.

transpose(i: int, j: int) -> Result#: This one-output result with dimensions i and j swapped, as reshape describes for views.

backward(grad, **options) -> Result#

The operation's backward for these inputs and the output gradient grad.

The same as calling the operation's standalone .backward with this result's inputs; options are its keyword options (such as dtype and rounding), with the same defaults.

Code

import exactref as er

# A 1x2 float32 matrix
A = er.asarray([[1.0, 2.0]], "float32")
# The product of A and a 2x1 float32 matrix, as a Result
r = er.matmul(A, er.asarray([[3.0], [4.0]], "float32"))
# The operation's name, and what r.rounded satisfies
print("op:", r.op)
print("guarantee:", r.guarantee)

Output

op: matmul
guarantee: correctly_rounded

Outputs#

class Outputs#: Several outputs of one operation, by name: outputs.Q or outputs["Q"].

Code

# matmul's backward on the same inputs, for the output gradient [[1.0]]
g = r.backward(er.asarray([[1.0]], "float32"))
# g has several outputs; listing g.rounded gives their names
print("outputs:", list(g.rounded))
# One output, by attribute and by name
print("grad_A by attribute:", g.rounded.grad_A.tolist())
print("grad_A by name:", g.rounded["grad_A"].tolist())

Output

outputs: ['grad_A', 'grad_B']
grad_A by attribute: [[3.0, 4.0]]
grad_A by name: [[3.0, 4.0]]

Boundary#

r.boundaries maps each required rounding step's name to a Boundary.

class Boundary#: Boundary(kind: 'str', description: 'str', applies_to: 'str | None' = None)

Code

# matmul's required rounding step for the sum of each element's products
b = r.boundaries["accumulate"]
# Its kind: "accumulate" is a sum of terms
print("kind:", b.kind)
# What the sum adds up: "dot" for products, "sum" for plain terms
print("applies to:", b.applies_to)

Output

kind: accumulate
applies to: dot