Correctness of direct-carrier software FMA #
These theorems connect the binary32 and binary64 FMA adapters in NativeFPU.Runtime to the
independent configured specification. The adapters use proved fixed-word software arithmetic in
both logical and compiled execution. Host experiments live in the separately imported
NativeFPU.Unchecked module and cannot enter this proof surface transitively.
Binary32 #
theorem
FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.softwareFma32_eq_spec
{width_le : FloatFormat.binary32.bitWidth ≤ 32}
(left right addend : Binary32Value width_le)
:
The direct-carrier binary32 FMA agrees with the independent configured specification.
Binary64 #
theorem
FloatLib.Floats.Formats.BinaryInterchange.Configured.NativeFPU.softwareFma64_eq_spec
{width_le : FloatFormat.binary64.bitWidth ≤ 64}
(left right addend : Binary64Value width_le)
:
The direct-carrier binary64 FMA agrees with the independent configured specification.