TorchLean API

Docs Home Installation Guide Examples Graphs Tools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.NativeCandidates

Certified fixed-format candidates for binary32 and binary64 #

Binary32 and binary64 need first-order capabilities because their public typeclass heads do not always expose the computed storage plan during instance search. Named software certificates supply these capabilities, and the selection theorems identify the certificate chosen by each ordinary software portfolio under every Policy.

The guarded NativeFPU.Unchecked functions remain an explicit application, differential-test, and benchmark API outside these certified portfolios.

Named fixed-format certificates #

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareAdd32Certified (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.Certified Spec.add

Certified fixed-word binary32 addition.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareSub32Certified (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.Certified Spec.sub

Certified fixed-word binary32 subtraction.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareMul32Certified (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.Certified Spec.mul

Certified fixed-word binary32 multiplication.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareDiv32Certified (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.Certified Spec.div

Certified fixed-word binary32 division.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareSqrt32Certified (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.Certified Spec.sqrt

Certified fixed-word binary32 square root.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareFma32Certified (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.Certified Spec.fma

Certified fixed-word binary32 fused multiply-add.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareAdd64Certified (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.Certified Spec.add

Certified fixed-word binary64 addition.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareSub64Certified (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.Certified Spec.sub

Certified fixed-word binary64 subtraction.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareMul64Certified (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.Certified Spec.mul

Certified fixed-word binary64 multiplication.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareDiv64Certified (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.Certified Spec.div

Certified fixed-word binary64 division.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareSqrt64Certified (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.Certified Spec.sqrt

Certified fixed-word binary64 square root.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.softwareFma64Certified (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.Certified Spec.fma

Certified fixed-word binary64 fused multiply-add.

Instances For

Complete software portfolios #

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary32AddCandidates (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.add)

Every certified software implementation considered for binary32 addition.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary32SubCandidates (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.sub)

Every certified software implementation considered for binary32 subtraction.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary32MulCandidates (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.mul)

Every certified software implementation considered for binary32 multiplication.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary32DivCandidates (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.div)

Every certified software implementation considered for binary32 division.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary32SqrtCandidates (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.sqrt)

Every certified software implementation considered for binary32 square root.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary32FmaCandidates (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.fma)

Every certified software implementation considered for binary32 fused multiply-add.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary64AddCandidates (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.add)

Every certified software implementation considered for binary64 addition.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary64SubCandidates (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.sub)

Every certified software implementation considered for binary64 subtraction.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary64MulCandidates (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.mul)

Every certified software implementation considered for binary64 multiplication.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary64DivCandidates (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.div)

Every certified software implementation considered for binary64 division.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary64SqrtCandidates (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.sqrt)

Every certified software implementation considered for binary64 square root.

Instances For

def FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.binary64FmaCandidates (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.CandidateSet (ExecFloat.Backend.Certified Spec.fma)

Every certified software implementation considered for binary64 fused multiply-add.

Instances For

Cost facts for fixed-format selection #

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

ExecFloat.Backend.Candidate.admissible policy (structuralEstimate plan operation Descriptor.Plan.StructuralRoute.fixedFormat) = true

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.better_structuralFixedFormat_generic {format : FloatFormat} (policy : ExecFloat.Backend.Policy) (plan : StoragePlan format) (operation : ExecFloat.Backend.Operation) (hsteady : (Descriptor.Plan.fixedFormatEstimate operation).steadyCost < (Descriptor.Plan.genericEstimate format operation).steadyCost) :

ExecFloat.Backend.Candidate.better policy (structuralEstimate plan operation Descriptor.Plan.StructuralRoute.fixedFormat) (genericEstimate plan operation) = true

Once its steady cost is lower, the fixed-format structural candidate beats the generic baseline under every policy.

Fixed-format selection for binary32 #

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary32AddCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.selectCertified policy (binary32AddCandidates width_le) = softwareAdd32Certified width_le

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary32SubCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.selectCertified policy (binary32SubCandidates width_le) = softwareSub32Certified width_le

Under every policy the binary32 subtraction portfolio selects the certified software kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary32MulCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.selectCertified policy (binary32MulCandidates width_le) = softwareMul32Certified width_le

Under every policy the binary32 multiplication portfolio selects the certified software kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary32DivCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.selectCertified policy (binary32DivCandidates width_le) = softwareDiv32Certified width_le

Under every policy the binary32 division portfolio selects the certified software kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary32SqrtCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.selectCertified policy (binary32SqrtCandidates width_le) = softwareSqrt32Certified width_le

Under every policy the binary32 square-root portfolio selects the certified software kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary32FmaCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary32.bitWidth ≤ 32) :

ExecFloat.Backend.selectCertified policy (binary32FmaCandidates width_le) = softwareFma32Certified width_le

Under every policy the binary32 fused multiply-add portfolio selects the certified software kernel.

Fixed-format selection for binary64 #

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary64AddCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.selectCertified policy (binary64AddCandidates width_le) = softwareAdd64Certified width_le

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary64SubCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.selectCertified policy (binary64SubCandidates width_le) = softwareSub64Certified width_le

Under every policy the binary64 subtraction portfolio selects the certified software kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary64MulCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.selectCertified policy (binary64MulCandidates width_le) = softwareMul64Certified width_le

Under every policy the binary64 multiplication portfolio selects the certified software kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary64DivCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.selectCertified policy (binary64DivCandidates width_le) = softwareDiv64Certified width_le

Under every policy the binary64 division portfolio selects the certified software kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary64SqrtCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.selectCertified policy (binary64SqrtCandidates width_le) = softwareSqrt64Certified width_le

Under every policy the binary64 square-root portfolio selects the certified software kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Configured.Plan.selectCertified_binary64FmaCandidates (policy : ExecFloat.Backend.Policy) (width_le : FloatFormat.binary64.bitWidth ≤ 64) :

ExecFloat.Backend.selectCertified policy (binary64FmaCandidates width_le) = softwareFma64Certified width_le

Under every policy the binary64 fused multiply-add portfolio selects the certified software kernel.