Correctness of direct storage-word arithmetic

Each direct operation equals the word operation it replaces, so it inherits that operation's refinement of the specification. For binary64, an accepted word-kernel result is the one-word view of the result the model dispatcher returns: the dispatcher tries the same one-word kernel first, and NativeSmallWordAdd.addFinite?_ofWord relates the kernel on models to the kernel on storage words. Two-word codes follow the same pattern through the NativePair kernels and NativePair.toWords.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.decode_word64 {format : FloatFormat} (hw : format.bitWidth ≤ 64) (value : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat.ModelCodec.decode value = Model.NativeSmallWord.ofWord ↑value.raw

The model value of a word64 code is the one-word view of its stored word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Add_eq {format : FloatFormat} (hw : format.bitWidth ≤ 64) (h64 : format.IsBinary64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : binary64Add hw left right = wordAdd left right

Addition on stored binary64 words is word addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Sub_eq {format : FloatFormat} (hw : format.bitWidth ≤ 64) (h64 : format.IsBinary64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : binary64Sub hw left right = wordSub left right

Subtraction on stored binary64 words is word subtraction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Mul_eq {format : FloatFormat} (hw : format.bitWidth ≤ 64) (h64 : format.IsBinary64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : binary64Mul hw left right = wordMul left right

Multiplication on stored binary64 words is word multiplication.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.ofWord_eq_ofUInt64 (bits : UInt64) : Model.NativeSmallWord.ofWord bits = Model.NativeBinary64.ofUInt64 bits

For binary64 the one-word view and the native binary64 view of a word agree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Div_eq {format : FloatFormat} (hw : format.bitWidth ≤ 64) (h64 : format.IsBinary64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : binary64Div hw left right = wordDiv left right

Division on stored binary64 words is word division.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Fma_eq {format : FloatFormat} (hw : format.bitWidth ≤ 64) (h64 : format.IsBinary64) (left right addend : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : binary64Fma hw left right addend = wordFma left right addend

Fused multiply-add on stored binary64 words is word fused multiply-add.

Two-word carriers

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.toNatBits_decode_pair {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (value : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : (ExecFloat.ModelCodec.decode value).toNatBits = (↑value.raw).toNat

The model value of a pair code has the code's two words as its encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.toWords_decode_pair {format : FloatFormat} (hpair : Model.NativePair.Eligible format) (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (value : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : Model.NativePair.toWords (ExecFloat.ModelCodec.decode value) = ↑value.raw

Splitting the model value of a pair code returns the code's two words.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.decode_pairCode {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (words : Numerics.FixedWord.UInt128) : ExecFloat.ModelCodec.decode (ExecFloat.ofRaw (pairCode hgt hle words)) = Model.NativePair.ofWords format words

A packed kernel result decodes to the model value the model kernel builds from its words.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairAdd_eq {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (hpair : Model.NativePair.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : pairAdd hgt hle left right = wordAdd left right

Addition on stored two-word codes is word addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairSub_eq {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (hpair : Model.NativePair.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : pairSub hgt hle left right = wordSub left right

Subtraction on stored two-word codes is word subtraction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairMul_eq {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (hpair : Model.NativePair.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : pairMul hgt hle left right = wordMul left right

Multiplication on stored two-word codes is word multiplication.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairDiv_eq {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (hpair : Model.NativePair.Eligible format) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : pairDiv hgt hle left right = wordDiv left right

Division on stored two-word codes is word division.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairSqrt_eq_spec {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (hpair : Model.NativePair.Eligible format) (value : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : pairSqrt hgt hle value = Spec.sqrt value

Square root of a stored two-word code implements the configured square-root specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairFma_eq_spec {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (hpair : Model.NativePair.Eligible format) (left right addend : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : pairFma hgt hle left right addend = Spec.fma left right addend

Fused multiply-add on stored two-word codes implements the configured FMA specification.

Plan dispatch

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.directAdd_eq {format : FloatFormat} {plan : StoragePlan format} (left right : ExecFloat (Family format (Code plan) plan)) : directAdd left right = wordAdd left right

Direct addition is word addition on every plan.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.directSub_eq {format : FloatFormat} {plan : StoragePlan format} (left right : ExecFloat (Family format (Code plan) plan)) : directSub left right = wordSub left right

Direct subtraction is word subtraction on every plan.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.directMul_eq {format : FloatFormat} {plan : StoragePlan format} (left right : ExecFloat (Family format (Code plan) plan)) : directMul left right = wordMul left right

Direct multiplication is word multiplication on every plan.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.directDiv_eq {format : FloatFormat} {plan : StoragePlan format} (left right : ExecFloat (Family format (Code plan) plan)) : directDiv left right = wordDiv left right

Direct division is word division on every plan.