Runtime kernels for configured binary formats

Configured binary arithmetic lifts the descriptor-model operations through the carrier selected by StoragePlan. The definitions are the total executable baseline for every precision and encoding policy. Correctness proofs live in Configured.Core.Proof.

The carrier conversion is deliberately explicit. The execution planner can charge for it and prefer a direct byte, word, fixed-limb, or family-defined kernel when one is available.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Spec.add {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Reference addition for a configured carrier.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Spec.sub {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Reference subtraction for a configured carrier.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Spec.mul {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Reference multiplication for a configured carrier.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Spec.div {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Reference division for a configured carrier.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Spec.sqrt {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Reference square root for a configured carrier.

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Spec.fma {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right third : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Reference fused multiply-add for a configured carrier.

Total generic kernels

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericAdd {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Width-generic proved addition.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericSub {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Width-generic proved subtraction.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericMul {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Width-generic proved multiplication.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericDiv {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Width-generic proved division.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericSqrt {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Width-generic proved square root.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.genericFma {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right third : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Width-generic proved fused multiply-add.

Proved word and fixed-limb arithmetic

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordAdd {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Parameterized word/fixed-format addition, adapted through the selected carrier.

The operation planner only advertises this candidate when the descriptor satisfies the kernel's structural eligibility predicate.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordSub {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Parameterized word/fixed-format subtraction.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordMul {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Parameterized word or fixed-limb multiplication.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordDiv {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Parameterized word or fixed-limb division.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordSqrt {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Parameterized word square root.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.wordFma {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right third : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Parameterized word fused multiply-add.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.fixedLimbSqrt {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Square-root dispatcher, including structurally eligible fixed-limb kernels.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Backend.fixedLimbFma {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right third : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

Fused multiply-add dispatcher, including structurally eligible fixed-limb kernels.