Backend-selection policy

A policy says how much one-time setup may be amortized, how allocations and memory are charged, and which resource ceilings are absolute. The built-in latency, balanced, and throughput profiles are format-independent starting points rather than claims about a particular machine.

PolicyFor makes the choice static at the format carrier. Users can select another profile with a scoped instance, while the encoded value type and arithmetic semantics remain unchanged. This also keeps execution and #float_info on the same plan.

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

Workload and memory policy used by the deterministic selector.

• expectedCalls : Nat

  Expected calls over which one-time setup is amortized.

• allocationPenalty : Nat

  Relative cost charged for one allocation on every call.

• memoryBlockBytes : Nat

  Number of bytes represented by one memory-cost block.

• temporaryBlockPenalty : Nat

  Relative warm-call cost charged for one temporary-memory block.

• residentBlockPenalty : Nat

  Relative cold cost charged for one persistent-memory block.

• maxTemporaryBytes : Nat

  Hard peak-temporary-memory limit for every optional candidate.

• maxResidentBytes : Nat

  Hard resident-memory limit for every optional candidate.

def FloatLib.Floats.ExecFloat.Backend.instDecidableEqPolicy.decEq (x✝ x✝¹ : Policy) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instDecidableEqPolicy : DecidableEq Policy

def FloatLib.Floats.ExecFloat.Backend.instReprPolicy.repr : Policy → Nat → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Backend.instReprPolicy : Repr Policy

def FloatLib.Floats.ExecFloat.Backend.Policy.latency : Policy

First-call-oriented policy.

This profile is appropriate when an operation may be used only a handful of times and a large one-time setup cost would dominate. Resource ceilings remain identical to Policy.default.

def FloatLib.Floats.ExecFloat.Backend.Policy.default : Policy

Default balanced policy.

The one-megabyte resident-memory ceiling admits all unary and binary byte-result tables through eight encoded bits and ternary tables through six bits, while rejecting an eight-bit FMA table (sixteen megabytes). The cost model may still reject an admissible table when its construction cannot amortize over the expected workload. Families and applications may publish a different static policy when their workload warrants it.

def FloatLib.Floats.ExecFloat.Backend.Policy.throughput : Policy

Sustained-throughput policy.

The five-million-call horizon admits a larger one-time setup cost when the selected kernel has a materially faster steady state. The resident-memory ceiling admits every exhaustive table over a byte-sized carrier; the cost model still rejects a large table when its setup cannot amortize at this horizon. Wider carriers remain governed by the same fixed resource bound.

def FloatLib.Floats.ExecFloat.Backend.Policy.profileName (policy : Policy) : String

Stable user-facing name for a built-in policy, or custom for an application policy.

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

A statically recognizable planning profile.

The built-in constructors expose fixed policies for specialization. custom carries an application-defined policy, which may be fixed or computed at runtime. Execution and inspection recover the complete policy from the same profile.

• latency : PolicyProfile
• balanced : PolicyProfile
• throughput : PolicyProfile
• custom (policy : Policy) : PolicyProfile

@[always_inline]

def FloatLib.Floats.ExecFloat.Backend.PolicyProfile.policy : PolicyProfile → Policy

Recover the complete cost policy represented by a static profile.

class FloatLib.Floats.ExecFloat.Backend.PolicyFor (F : Type u) : Type

Static planning policy associated with a format carrier.

This class changes backend choice, not numerical semantics or the ExecFloat value type. Concrete format families may depend on it when constructing operation capabilities. A local or scoped instance can therefore request a latency or throughput plan without wrapping values or changing user arithmetic.

• profile : PolicyProfile

  Static or application-defined profile used to choose kernels for F.

@[always_inline]

def FloatLib.Floats.ExecFloat.Backend.PolicyFor.policy {F : Type u} (planning : PolicyFor F) : Policy

The complete cost policy carried by a format's static planning profile.

@[instance_reducible]

def FloatLib.Floats.ExecFloat.Backend.PolicyFor.custom {F : Type u} (policy : Policy) : PolicyFor F

Construct a planning instance for an application-defined cost policy.

@[instance_reducible, instance 100]

instance FloatLib.Floats.ExecFloat.Backend.defaultPolicyFor (F : Type u) : PolicyFor F

Balanced planning is the format-independent default.

@[instance_reducible]

def FloatLib.Floats.ExecFloat.Backend.PlanningLatency.policy (F : Type u) : PolicyFor F

Select first-call-oriented plans for every capability that consumes PolicyFor.

Opening this scope changes execution planning, not the numerical type or its semantics.

@[instance_reducible]

def FloatLib.Floats.ExecFloat.Backend.PlanningThroughput.policy (F : Type u) : PolicyFor F

Select sustained-throughput plans for every capability that consumes PolicyFor.

The scope is carrier- and format-independent: descriptor families, direct standard formats, and user-defined formats all use the same policy mechanism.