Executable division backends

The width-generic divider and fixed-width dispatcher live here. Their correctness theorems are kept in Div.Proof.

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

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; exceptional operands retain 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 enters the single exact width-generic baseline here. The dispatcher is specialized on the descriptor, as described in Dispatch.Add.Runtime.