Format-independent ExecFloat automation #
execfloat_spec rewrites the six universal public operations to their capability-selected
specifications, both as explicit calls such as ExecFloat.add x y and as notation such as
x + y. It knows nothing about IEEE fields, radix arithmetic, exceptional encodings, or a
particular backend family. Format packages may register additional semantic rules with
numerics, but those plugins remain below this layer.
The equations are ordinary kernel-checked theorems from the capability dictionaries. The automation introduces no axiom and does not unfold an executable backend.
Rewrite universal ExecFloat arithmetic in the goal and local hypotheses to the exact
specifications. Use grind directly when a public-to-specification equality is itself the goal.