Format-independent ExecFloat automation #
execfloat_spec rewrites the six universal public operations to their capability-selected
specifications. 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 six 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.