Binary-interchange rules for numerical automation

This format-family plugin registers the descriptor model's semantic equations and concrete decoder definitions with the representation-independent numerics tactic. The binary_interchange_spec tactic rewrites descriptor-model arithmetic to its exact specifications. Universal capability arithmetic is handled separately by FloatLib.Floats.ExecFloat.Automation, so the family-independent layer does not depend on this binary layout.

def attrFloatFormat : Lean.ParserDescr

Register a static FloatFormat definition for concrete Model proof reduction.

The format remains ordinary compile-time data; this attribute only lets numerics unfold its name when checking a closed encoded value.

def FloatLib.Floats.Formats.BinaryInterchange.Model.binaryInterchangeSpec : Lean.ParserDescr

Rewrite binary-interchange descriptor arithmetic in the goal and local hypotheses to its exact specifications. Use grind directly when a public-to-specification equality is itself the goal.