Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Wrong semantics for fmul_add inafp/IEEE_Float...

view this post on Zulip Email Gateway (Oct 30 2021 at 17:44):

From: Fabian Immler via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Peter,

It is possible that this formalisation is not faithful to the IEEE standard.
The commit message of the changeset that is to blame reminded me that I just “ported float_mul_add and float_round … from HOL Kananaskis-12”.
I.e., I did not validate these definitions thoroughly.

The corresponding code in HOL Kananaskis-12 (pretty much unchanged in current Kananaskis-14) reads as follows and probably shows the same behaviour:
https://github.com/HOL-Theorem-Prover/HOL/blob/kananaskis-12/src/floating-point/binary_ieeeScript.sml#L488 <https://github.com/HOL-Theorem-Prover/HOL/blob/kananaskis-12/src/floating-point/binary_ieeeScript.sml#L488>

float_round_with_flags mode
(if (r1 = 0) /\ (r2 = 0) /\ (signP = z.Sign) then
signP = 1w
else mode = roundTowardNegative) (r1 + r2)`

Best wishes,
Fabian

Last updated: Jan 04 2025 at 20:18 UTC