Static dispatch for public ExecFloat operations

These are the 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; 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. Proofs can use ExecFloat.Proof.add_eq_spec to replace the call with its 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. Proofs can use ExecFloat.Proof.sub_eq_spec to replace the call with its 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. Proofs can use ExecFloat.Proof.mul_eq_spec to replace the call with its 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. Proofs can use ExecFloat.Proof.div_eq_spec to replace the call with its 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.

This is the function behind value.sqrt. Proofs can use ExecFloat.Proof.sqrt_eq_spec to replace the call with its 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.

Proofs can use ExecFloat.Proof.fma_eq_spec to replace the call with its reference definition.