Executable division backends

The width-generic divider and fixed-width dispatcher live here, and their correctness theorems in Div.Proof.

The dispatcher selects native kernels by format capability. A selected kernel may decline when its operand or intermediate bounds fail, and the generic implementation then supplies the result, including the descriptor's exceptional-value policy.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.DivBackend.generic {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Width-generic compiled division.

Finite operands use the compact scale kernel, and every other case goes to Spec.divSpecial.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.DivBackend.word {fmt : FloatFormat} (x y : Model fmt) : Model fmt

Compiled implementation of div.

Binary32 and binary64 finite operands use native-word decoding. Structurally eligible pair layouts use the certified radix-2^32 normal quotient kernel. Every other one-word IEEE layout uses restoring division. Every declined or ineligible case falls back to generic. The dispatcher is specialized on the descriptor, as described in Dispatch.Add.Runtime.