First-order dispatch for binary32 and binary64 #
Binary32 and binary64 use first-order operation instances that name their fixed-format
specializations. The public type constructor lives in Configured.Type, while the generic
table, word, limb, and baseline instances live in Configured.Plan.Instances.
Each instance names the fixed-format certificate it executes.
Plan.selectCertified_binary32AddCandidates and its siblings prove that the planner selects this
certificate under every Policy. The kernel that runs is therefore the proved kernel
#float_info reports, whichever PolicyFor instance is in scope.
The explicit guarded host operations remain in Configured.NativeFPU.Unchecked, but no compiler
substitution or certified candidate places them behind these capabilities.
Configured IEEE binary32 and binary64 operations name their first-order software kernels directly.
These instances are attached to the public parameterized families rather than to a storage-plan
constructor. Lean's typeclass index preserves Binary.Family 8 23 and Binary.Family 11 52,
while it does not always unfold their computed forKnownWidth plans during instance search.
All six operations execute the proved fixed-format word kernels. Guarded host-primitive
experiments are separate functions and are not candidates until an exact equality proof exists.