Direct storage-word arithmetic for configured binary formats

On the word64 plan the code is the encoding itself. Binary64 addition and subtraction run the one-word kernel on the stored UInt64 values and rebuild the proof model only when the kernel declines. A binary64 model value with the sign bit set is a natural number of at least 2 ^ 63, which the runtime allocates, so negative operands would otherwise pay for several allocations per operation.

On the pair plan the code is the two storage words of the encoding. Formats with the two-word layout of NativePair add, subtract, multiply, divide, fuse multiply-adds, and take square roots through the two-word kernels on those words. Above 64 bits every model value is an allocated natural number, and splitting and joining it costs far more than the arithmetic. Direct.Proof shows each direct operation equals the word operation it replaces.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.word64Code {format : FloatFormat} (hw : format.bitWidth ≤ 64) (bits : UInt64) : Code (StoragePlan.word64 hw)

Pack a kernel's storage word as a word64 code, masked below the radix.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.binary64Add {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

The model fallback of binary64Add, kept out of line so the word path stays small, and specialized on the format so declined inputs run the descriptor-specialized dispatcher.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Add {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Addition on stored binary64 words, rebuilding the model only when the word kernel declines.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.binary64Sub {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Out-of-line model fallback of binary64Sub, as for binary64Add.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Sub {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Subtraction on stored binary64 words, with the right operand's sign toggled in the kernel.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.binary64Mul {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Out-of-line model fallback of binary64Mul, as for binary64Add.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Mul {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Multiplication on stored binary64 words through the two-word normal-product kernel.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.binary64Div {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Out-of-line model fallback of binary64Div, as for binary64Add.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Div {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Division on stored binary64 words through the normal-result divider.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.binary64Fma {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right addend : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Out-of-line model fallback of binary64Fma, as for binary64Add.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.binary64Fma {format : FloatFormat} (hw : format.bitWidth ≤ 64) (left right addend : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))) : ExecFloat (Family format (Code (StoragePlan.word64 hw)) (StoragePlan.word64 hw))

Fused multiply-add on stored binary64 words through the normal-result kernel.

Two-word carriers

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairHighMask (format : FloatFormat) : UInt64

Mask of the encoded bits in the high word of a pair code: 2 ^ (bitWidth - 64) - 1.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairHighMask_toNat (format : FloatFormat) (hle : format.bitWidth ≤ 128) : (pairHighMask format).toNat = 2 ^ (format.bitWidth - 64) - 1

The high-word mask is exact for every width up to 128 bits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairWords_lt {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (words : Numerics.FixedWord.UInt128) : { hi := words.hi &&& pairHighMask format, lo := words.lo }.toNat < 2 ^ format.bitWidth

A high word masked by pairHighMask and any low word form an encoding below the radix.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairCode {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (words : Numerics.FixedWord.UInt128) : Code (StoragePlan.pair hgt hle)

Pack a kernel's two storage words as a pair code, masked below the radix.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.pairAdd {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Out-of-line model fallback of pairAdd, as for binary64Add.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairAdd {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Addition on stored two-word codes through the two-word finite addition kernel.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.pairSub {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Out-of-line model fallback of pairSub, as for binary64Add.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairSub {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Subtraction on stored two-word codes, with the right operand's sign toggled in the kernel.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.pairMul {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Out-of-line model fallback of pairMul, as for binary64Add.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairMul {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Multiplication on stored two-word codes through the two-word normal-product kernel.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.pairDiv {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Out-of-line model fallback of pairDiv, as for binary64Add.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairDiv {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Division on stored two-word codes through the certified two-word normal divider.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.pairSqrt {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (value : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Out-of-line fixed-limb fallback of pairSqrt, as for binary64Add.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairSqrt {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (value : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Square root of a stored two-word code through the two-word normal root kernel.

@[noinline, specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.Internal.Fallback.pairFma {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right addend : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Out-of-line fixed-limb fallback of pairFma, as for binary64Add.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.pairFma {format : FloatFormat} (hgt : 64 < format.bitWidth) (hle : format.bitWidth ≤ 128) (left right addend : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))) : ExecFloat (Family format (Code (StoragePlan.pair hgt hle)) (StoragePlan.pair hgt hle))

Fused multiply-add on stored two-word codes through the two-word finite FMA kernel.

Plan dispatch

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.directAdd {format : FloatFormat} {plan : StoragePlan format} : ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan)

Word addition for the configured code, with direct binary64 and two-word kernels.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.directSub {format : FloatFormat} {plan : StoragePlan format} : ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan)

Word subtraction for the configured code, with direct binary64 and two-word kernels.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.directMul {format : FloatFormat} {plan : StoragePlan format} : ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan)

Word multiplication for the configured code, using the two-word kernel when the layout allows.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.directDiv {format : FloatFormat} {plan : StoragePlan format} : ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan) → ExecFloat (Family format (Code plan) plan)

Word division for the configured code, using the two-word kernel when the layout allows.