The model's approximations: the correctly rounded reciprocal and square
root (and the reciprocal of the rounded square root) -- NOT the MUFU
unit's results, which are within a few units in the last place of them;
the trigonometric, exponential, logarithmic and tanh approximations are
not modelled (the default NaN). A statement at the model that uses them
is a statement about this choice; the checked paths state theirs for
every choice.
247def modelF32Approximate =
248 (lambda unrestricted operation : Nat . (lambda unrestricted value : Nat .
249 (specSelect (specEqual operation f32ApproximateReciprocal)
250 (modelF32Divide 1065353216 value)
251 (specSelect (specEqual operation f32ApproximateSquareRoot)
252 (modelF32SquareRoot value)
253 (specSelect (specEqual operation f32ApproximateReciprocalSquareRoot)
254 (modelF32Divide 1065353216 (modelF32SquareRoot value))
255 modelDefaultNaN)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.