Direct calls to selected kernels

Word and pair storage can call a structural kernel without projecting a certificate closure. The guard below uses the same eligibility and cost comparison as the complete portfolio. Its selection proofs unfold that portfolio and show that the direct call is the selected candidate's own function, not another algorithm with the same numerical specification.

The generic winner also has a direct entry point for carriers without a table or limb candidate. This exposes constant format parameters to the compiler at arbitrary precision.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.firstOrderDispatch {format : FloatFormat} : StoragePlan format → Bool

Storage plans whose structural candidate can be called without a carrier-specific table or limb closure. This is a storage eligibility test, not a selection decision.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.structuralSelected {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (operation : ExecFloat.Backend.Operation) : Bool

Whether the structural candidate wins its comparison with the generic kernel.

@[noinline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.firstOrderSelected {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (operation : ExecFloat.Backend.Operation) : Bool

Whether a direct structural call executes the winner of the complete configured portfolio.

It is kept out of the arithmetic body: the compiler caches closed format/plan/policy applications, and the selected structural branch stays open to specialization.

@[noinline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.firstOrderGenericSelected {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (operation : ExecFloat.Backend.Operation) : Bool

Whether the generic kernel wins a portfolio with no carrier-specific direct candidates.

@[always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.structuralSqrt {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (value : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

The square-root function stored in the descriptor's structural candidate.

@[always_inline]

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.structuralFma {format : FloatFormat} {plan : StoragePlan format} {code : Type} [ExecFloat.ModelCodec plan (Model format) code] (left right third : ExecFloat (Family format code plan)) : ExecFloat (Family format code plan)

The fused-multiply-add function stored in the descriptor's structural candidate.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_add_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.add = true) : (ExecFloat.Backend.selectCertified policy (automaticAddCandidates format plan)).run = Backend.wordAdd

A direct add call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_sub_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.sub = true) : (ExecFloat.Backend.selectCertified policy (automaticSubCandidates format plan)).run = Backend.wordSub

A direct sub call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_mul_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.mul = true) : (ExecFloat.Backend.selectCertified policy (automaticMulCandidates format plan)).run = Backend.wordMul

A direct mul call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_div_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.div = true) : (ExecFloat.Backend.selectCertified policy (automaticDivCandidates format plan)).run = Backend.wordDiv

A direct div call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_sqrt_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.sqrt = true) : (ExecFloat.Backend.selectCertified policy (automaticSqrtCandidates format plan)).run = structuralSqrt

A direct sqrt call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_fma_run_of_firstOrder {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderSelected policy plan ExecFloat.Backend.Operation.fma = true) : (ExecFloat.Backend.selectCertified policy (automaticFmaCandidates format plan)).run = structuralFma

A direct fma call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_add_run_of_firstOrderGeneric {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderGenericSelected policy plan ExecFloat.Backend.Operation.add = true) : (ExecFloat.Backend.selectCertified policy (automaticAddCandidates format plan)).run = Backend.genericAdd

The direct generic add call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_sub_run_of_firstOrderGeneric {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderGenericSelected policy plan ExecFloat.Backend.Operation.sub = true) : (ExecFloat.Backend.selectCertified policy (automaticSubCandidates format plan)).run = Backend.genericSub

The direct generic sub call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_mul_run_of_firstOrderGeneric {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderGenericSelected policy plan ExecFloat.Backend.Operation.mul = true) : (ExecFloat.Backend.selectCertified policy (automaticMulCandidates format plan)).run = Backend.genericMul

The direct generic mul call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_div_run_of_firstOrderGeneric {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderGenericSelected policy plan ExecFloat.Backend.Operation.div = true) : (ExecFloat.Backend.selectCertified policy (automaticDivCandidates format plan)).run = Backend.genericDiv

The direct generic div call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_sqrt_run_of_firstOrderGeneric {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderGenericSelected policy plan ExecFloat.Backend.Operation.sqrt = true) : (ExecFloat.Backend.selectCertified policy (automaticSqrtCandidates format plan)).run = Backend.genericSqrt

The direct generic sqrt call names the selected candidate's function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.select_fma_run_of_firstOrderGeneric {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (h : firstOrderGenericSelected policy plan ExecFloat.Backend.Operation.fma = true) : (ExecFloat.Backend.selectCertified policy (automaticFmaCandidates format plan)).run = Backend.genericFma

The direct generic fma call names the selected candidate's function.