Backend-selection metadata

Candidate metadata records the operation, storage shape, algorithm family, warm and cold costs, allocations, and memory use. It is deliberately format-independent so binary, posit, and future families can report plans through one interface.

Estimates do not establish numerical correctness or eligibility. The family supplies eligible candidates with refinement proofs; selection and inspection use this metadata to compare their estimated costs.

inductive FloatLib.Floats.ExecFloat.Backend.Operation : Type

Universal operation whose implementation is being selected.

• add : Operation
• sub : Operation
• mul : Operation
• div : Operation
• sqrt : Operation
• fma : Operation

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqOperation : DecidableEq Operation

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprOperation : Repr Operation

def FloatLib.Floats.ExecFloat.Backend.instReprOperation.repr : Operation → Nat → Std.Format

def FloatLib.Floats.ExecFloat.Backend.Operation.all : List Operation

Every universal operation, in stable user-facing display order.

def FloatLib.Floats.ExecFloat.Backend.Operation.label : Operation → String

Stable user-facing name of an operation.

def FloatLib.Floats.ExecFloat.Backend.Operation.longLabel : Operation → String

Stable expanded name for prose and inspectable implementation names.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.Operation.arity : Operation → Nat

Number of encoded operands consumed by an operation.

inductive FloatLib.Floats.ExecFloat.Backend.StorageClass : Type

Persistent runtime-storage class.

This is descriptive metadata. The authoritative carrier remains FormatCode F, so custom families may use storage not covered by these common classes and report .custom.

• byte : StorageClass
• word16 : StorageClass
• word32 : StorageClass
• word64 : StorageClass
• fixedLimbs (count : Nat) : StorageClass
• wideLimbs : StorageClass
• custom : StorageClass

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqStorageClass : DecidableEq StorageClass

def FloatLib.Floats.ExecFloat.Backend.instDecidableEqStorageClass.decEq (x✝ x✝¹ : StorageClass) : Decidable (x✝ = x✝¹)

def FloatLib.Floats.ExecFloat.Backend.instReprStorageClass.repr : StorageClass → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprStorageClass : Repr StorageClass

@[inline]

def FloatLib.Floats.ExecFloat.Backend.StorageClass.forBitWidth (bits : Nat) : StorageClass

Smallest common storage class that can contain bits encoded bits.

def FloatLib.Floats.ExecFloat.Backend.StorageClass.display : StorageClass → String

Human-readable storage name used by inspection tools.

inductive FloatLib.Floats.ExecFloat.Backend.KernelClass : Type

Algorithm family selected for one executable operation.

• exhaustiveTable : KernelClass

  Exhaustive lookup table over encoded operands.

• fixedFormat : KernelClass

  Monomorphic kernel specialized to one exact format.

• nativeWord : KernelClass

  Parameterized kernel operating within one machine word.

• fixedLimbs : KernelClass

  Kernel over a compile-time fixed number of machine-word limbs.

• wideLimbs : KernelClass

  Kernel over a runtime-sized limb buffer.

• generic : KernelClass

  Width-generic exact executable baseline.

• custom (label : String) (tieRank : Nat) : KernelClass

  Family-defined algorithm class.

  The label is shown by inspection tools. tieRank is used only after equal total scores; custom ranks start at seven, above every built-in class.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqKernelClass : DecidableEq KernelClass

def FloatLib.Floats.ExecFloat.Backend.instDecidableEqKernelClass.decEq (x✝ x✝¹ : KernelClass) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprKernelClass : Repr KernelClass

def FloatLib.Floats.ExecFloat.Backend.instReprKernelClass.repr : KernelClass → Nat → Std.Format

@[inline]

def FloatLib.Floats.ExecFloat.Backend.KernelClass.rank : KernelClass → Nat

Stable tie-breaking rank.

The score decides normal comparisons. This rank only makes equal-score selection deterministic and favors the more specialized representation.

def FloatLib.Floats.ExecFloat.Backend.KernelClass.display : KernelClass → String

User-facing name of a kernel class.

structure FloatLib.Floats.ExecFloat.Backend.Candidate : Type

Static engineering estimate for one certified candidate.

All work units are relative and family-calibrated. steadyCost, marshallingCost, allocations, and temporaryBytes estimate one warm call. Marshalling covers carrier-to-working-representation conversion and repacking of the result; keeping it separate prevents a fast arithmetic kernel behind expensive Nat or proof-model conversion from appearing artificially cheap.

setupCost and setupAllocations estimate one-time initialization such as lazy table generation. residentBytes and temporaryBytes also participate in hard memory limits.

• name : String

  Stable family-defined name shown by inspection and benchmark tools.

• kind : KernelClass

  Algorithm family used for deterministic tie-breaking and user-facing reports.

• storage : StorageClass

  Persistent carrier consumed by this kernel without changing the public value type.

• steadyCost : Nat

  Relative arithmetic work performed by one warm call, excluding representation conversion.

• marshallingCost : Nat

  Total per-call cost of decoding operands and repacking the result.

• setupCost : Nat

  Relative one-time work needed to initialize the candidate.

• setupAllocations : Nat

  Estimated number of heap allocations during one-time initialization.

• residentBytes : Nat

  Estimated persistent bytes retained after initialization.

• temporaryBytes : Nat

  Estimated peak temporary workspace for one call, in bytes.

• allocations : Nat

  Estimated number of heap allocations during one warm call.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqCandidate : DecidableEq Candidate

def FloatLib.Floats.ExecFloat.Backend.instDecidableEqCandidate.decEq (x✝ x✝¹ : Candidate) : Decidable (x✝ = x✝¹)

def FloatLib.Floats.ExecFloat.Backend.instReprCandidate.repr : Candidate → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprCandidate : Repr Candidate

structure FloatLib.Floats.ExecFloat.Backend.CandidateSet (α : Type u) : Type u

A nonempty collection represented by optional alternatives and a mandatory exact baseline.

The same container carries either inspectable cost estimates or proof-carrying implementations. Keeping the element type abstract prevents the planner and executable dispatcher from growing parallel record types whose only difference is their payload.

• alternatives : List α

  Optional implementations compared with the mandatory baseline.

• baseline : α

  Mandatory payload used as the initial incumbent, making selection total.

def FloatLib.Floats.ExecFloat.Backend.instDecidableEqCandidateSet.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : CandidateSet α✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqCandidateSet {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (CandidateSet α✝)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprCandidateSet {α✝ : Type u_1} [Repr α✝] : Repr (CandidateSet α✝)

def FloatLib.Floats.ExecFloat.Backend.instReprCandidateSet.repr {α✝ : Type u_1} [Repr α✝] : CandidateSet α✝ → Nat → Std.Format

def FloatLib.Floats.ExecFloat.Backend.CandidateSet.singleton {α : Type u} (baseline : α) : CandidateSet α

A candidate set containing only its mandatory baseline.

def FloatLib.Floats.ExecFloat.Backend.CandidateSet.map {α : Type u} {β : Type v} (f : α → β) (candidates : CandidateSet α) : CandidateSet β

Transform every payload without changing candidate order or the distinguished baseline.

def FloatLib.Floats.ExecFloat.Backend.CandidateSet.toList {α : Type u} (candidates : CandidateSet α) : List α

Optional candidates in planner order, followed by the mandatory exact baseline.