Certified execution candidates for arbitrary binary descriptors

Every binary FloatFormat has a proof-carrying candidate plan for addition, subtraction, multiplication, division, square root, and fused multiply-add. The public ExecFloat dispatcher makes the only selection:

• every format of at most eight encoded bits can use a lazily generated exhaustive table;
• each operation exposes at most one structural route, classified as fixed-format, native-word, or fixed-limb in exactly the same order as its executable dispatcher;
• every descriptor retains a proved width-generic baseline.

Every candidate is selected from descriptor data through the same structural predicates used by runtime dispatch. Layout-specific kernels remain specialized, but no plan depends on descriptor identity or a catalogued format name. A new IEEE, finite-only, FNUZ, or otherwise custom descriptor receives table and structural candidates when eligible, together with the generic baseline.

Cost estimates live in Descriptor.Plan.Estimates; this module is responsible for candidate availability and proof-carrying construction.

Generic certified constructors

theorem FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.toNatBits_lt_256_of_bitWidth_le {format : FloatFormat} (hwidth : format.bitWidth ≤ 8) (value : Model format) : value.toNatBits < 256

Descriptor-generic exhaustive tables

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.binaryTableCertified {format : FloatFormat} (operation : ExecFloat.Backend.Operation) (modelSpec modelRun : Model format → Model format → Model format) (modelRun_eq_spec : ∀ (left right : Model format), modelRun left right = modelSpec left right) (hwidth : format.bitWidth ≤ 8) : ExecFloat.Backend.Certified (ExecFloat.ModelCodec.liftBinary modelSpec)

Build a certified exhaustive binary table for a descriptor of at most eight bits.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.unaryTableCertified {format : FloatFormat} (operation : ExecFloat.Backend.Operation) (modelSpec modelRun : Model format → Model format) (modelRun_eq_spec : ∀ (value : Model format), modelRun value = modelSpec value) (hwidth : format.bitWidth ≤ 8) : ExecFloat.Backend.Certified (ExecFloat.ModelCodec.liftUnary modelSpec)

Build a certified exhaustive unary table for a descriptor of at most eight bits.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.ternaryTableCertified {format : FloatFormat} (operation : ExecFloat.Backend.Operation) (modelSpec modelRun : Model format → Model format → Model format → Model format) (modelRun_eq_spec : ∀ (left right addend : Model format), modelRun left right addend = modelSpec left right addend) (hwidth : format.bitWidth ≤ 8) : ExecFloat.Backend.Certified (ExecFloat.ModelCodec.liftTernary modelSpec)

Build a certified exhaustive ternary table for a descriptor of at most eight bits.

Candidate availability

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.tableBinary? {format : FloatFormat} (operation : ExecFloat.Backend.Operation) (modelSpec modelRun : Model format → Model format → Model format) (modelRun_eq_spec : ∀ (left right : Model format), modelRun left right = modelSpec left right) : Option (ExecFloat.Backend.Certified (ExecFloat.ModelCodec.liftBinary modelSpec))

Offer an exhaustive binary table exactly when the encoded width fits in one byte.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.tableUnary? {format : FloatFormat} (operation : ExecFloat.Backend.Operation) (modelSpec modelRun : Model format → Model format) (modelRun_eq_spec : ∀ (value : Model format), modelRun value = modelSpec value) : Option (ExecFloat.Backend.Certified (ExecFloat.ModelCodec.liftUnary modelSpec))

Offer an exhaustive unary table exactly when the encoded width fits in one byte.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.tableTernary? {format : FloatFormat} (operation : ExecFloat.Backend.Operation) (modelSpec modelRun : Model format → Model format → Model format → Model format) (modelRun_eq_spec : ∀ (left right addend : Model format), modelRun left right addend = modelSpec left right addend) : Option (ExecFloat.Backend.Certified (ExecFloat.ModelCodec.liftTernary modelSpec))

Offer an exhaustive ternary table exactly when the encoded width fits in one byte.

Complete per-operation plans

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.addCandidates (format : FloatFormat) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.add)

Certified addition candidates derived from descriptor structure.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.subCandidates (format : FloatFormat) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.sub)

Certified subtraction candidates derived from descriptor structure.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.mulCandidates (format : FloatFormat) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.mul)

Certified multiplication candidates derived from descriptor structure.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.divCandidates (format : FloatFormat) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.div)

Certified division candidates derived from descriptor structure.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.sqrtCandidates (format : FloatFormat) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.sqrt)

Certified square-root candidates derived from descriptor structure.

def FloatLib.Floats.Formats.BinaryInterchange.Descriptor.Plan.fmaCandidates (format : FloatFormat) : ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.fma)

Certified fused-multiply-add candidates derived from descriptor structure.