Static dispatch for public ExecFloat operations

Same-format arithmetic entry points of the format-independent execution layer. Capability dictionaries are resolved from the static format type. Each function is marked inline, and the checks under benchmarks/scripts/checks/ verify that specialization erases the dictionary lookup.

@[inline]

def FloatLib.Floats.ExecFloat.add {F : Type u} [Numerics.EncodedFormat F] [Backend.PolicyFor F] [Add F] (left right : ExecFloat F) : ExecFloat F

Add two values in the same format using the certified implementation selected for F.

This is the function behind left + right. In proofs, ExecFloat.Proof.add_eq_spec rewrites it to the reference definition.

@[inline]

def FloatLib.Floats.ExecFloat.sub {F : Type u} [Numerics.EncodedFormat F] [Backend.PolicyFor F] [Sub F] (left right : ExecFloat F) : ExecFloat F

Subtract two values in the same format using the certified implementation selected for F.

This is the function behind left - right. In proofs, ExecFloat.Proof.sub_eq_spec rewrites it to the reference definition.

@[inline]

def FloatLib.Floats.ExecFloat.mul {F : Type u} [Numerics.EncodedFormat F] [Backend.PolicyFor F] [Mul F] (left right : ExecFloat F) : ExecFloat F

Multiply two values in the same format using the certified implementation selected for F.

This is the function behind left * right. In proofs, ExecFloat.Proof.mul_eq_spec rewrites it to the reference definition.

@[inline]

def FloatLib.Floats.ExecFloat.div {F : Type u} [Numerics.EncodedFormat F] [Backend.PolicyFor F] [Div F] (left right : ExecFloat F) : ExecFloat F

Divide two values in the same format using the certified implementation selected for F.

This is the function behind left / right. In proofs, ExecFloat.Proof.div_eq_spec rewrites it to the reference definition.

@[inline]

def FloatLib.Floats.ExecFloat.sqrt {F : Type u} [Numerics.EncodedFormat F] [Backend.PolicyFor F] [Sqrt F] (value : ExecFloat F) : ExecFloat F

Compute square root using the certified implementation selected for F.

Write ExecFloat.sqrt value, or value.sqrt for a format without its own sqrt. On a configured binary value, value.sqrt is ExecFloat.Binary.sqrt, whose default call is this function. In proofs, ExecFloat.Proof.sqrt_eq_spec rewrites it to the reference definition.

@[inline]

def FloatLib.Floats.ExecFloat.fma {F : Type u} [Numerics.EncodedFormat F] [Backend.PolicyFor F] [Fma F] (left right addend : ExecFloat F) : ExecFloat F

Compute left * right + addend with one final rounding using the certified implementation selected for F.

In proofs, ExecFloat.Proof.fma_eq_spec rewrites it to the reference definition.