Executable arithmetic capabilities

A capability supplies an operation's specification, certified implementations, and cost estimates. The selector starts with a mandatory baseline and considers alternatives within the resource limits using those estimates. This indexed contract is used by the named operations in ExecFloat.Core.Operations.

Capability.run_eq_spec proves equality of Lean definitions. The binary software kernels use proved refinements and @[csimp] replacements; their compiled correctness also depends on the compiler. The explicit binary32/binary64 NativeFPU.Unchecked host functions are deliberately not capabilities because they do not yet have the packed-word equality theorem required by Backend.Certified.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.OperationSignature (F : Type u) [Numerics.EncodedFormat F] : Backend.Operation → Type u_1

Function type of a universal arithmetic operation over one encoded format.

Indexing the operation package by Backend.Operation keeps addition, subtraction, multiplication, division, square root, and FMA as distinct capabilities even when some operations have the same Lean function type.

class FloatLib.Floats.ExecFloat.Capability (F : Type u) [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] (operation : Backend.Operation) : Type u_1

Semantics, certified kernels, and static selection for one arithmetic operation.

The operation index prevents accidental instance sharing between operations while avoiding six structurally identical planner records.

• spec : OperationSignature F operation

  Clear reference operation for F.

• candidates : Backend.CandidateSet (Backend.Certified spec)

  Certified kernels offered by this capability for the operation on F.

• selection : Thunk (Backend.Certified spec)

  Lazy, memoized automatic selection for capabilities that do not materialize a direct winner.

  The first projection evaluates the planner; subsequent projections reuse the selected certificate. Static built-in formats may bypass even this projection by supplying implementation directly.

• implementation : Backend.Certified spec

  Certified implementation executed by public arithmetic.

  The default reads the memoized automatic selection. A statically specialized package may store the planner's already-known winner directly, allowing Lean to erase both planning and closure dispatch from the generated hot path.

• implementation_is_selected : implementation = Backend.selectCertified planning.policy candidates

  The stored certificate is, in Lean's logic, the winner of the advertised candidate plan under the policy in scope.

  A static package may materialize the winner for code generation, but it must then prove that the planner selects that same certificate. Inspection tools such as #float_info report implementation; execute_eq_implementation relates the public entry point to its logical operation. These equations establish equality of behavior in Lean, not identity of generated machine code.

• execute : OperationSignature F operation

  First-order executable entry point used by public arithmetic.

  The default projects the selected certificate. Static formats may name the same proved kernel directly, which lets Lean erase the certificate and typeclass dictionaries from monomorphic calls without changing either selection metadata or the correctness boundary.

• execute_eq_implementation : execute = implementation.run

  In Lean's logic, the first-order entry point is propositionally equal to the selected certificate's run.

  When a package supplies execute := implementation.run, or names the certificate's kernel and proves this field by rfl, the compiled code of execute is that certificate's kernel. Code named here must not acquire an unproved compiler replacement: this equation identifies the logical kernel but could not establish equality with such a substitute.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Add (F : Type u) [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] : Type u_1

Addition capability for one format.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Sub (F : Type u) [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] : Type u_1

Subtraction capability for one format.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Mul (F : Type u) [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] : Type u_1

Multiplication capability for one format.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Div (F : Type u) [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] : Type u_1

Division capability for one format.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Sqrt (F : Type u) [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] : Type u_1

Square-root capability for one format.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Fma (F : Type u) [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] : Type u_1

Fused multiply-add capability for one format.

@[instance_reducible, always_inline]

def FloatLib.Floats.ExecFloat.Capability.ofCandidates {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] (operation : Backend.Operation) (spec : OperationSignature F operation) (candidates : Backend.CandidateSet (Backend.Certified spec)) (execute : OperationSignature F operation) (execute_eq_spec : execute = spec) : Capability F operation

Build a capability from a policy-selected portfolio and a first-order dispatcher.

The candidates remain authoritative for inspection and certification. Naming execute separately lets a format expose the same selected behavior without retaining a certificate projection in monomorphic generated code.

@[instance_reducible, always_inline]

def FloatLib.Floats.ExecFloat.Capability.ofDirectKernel {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] (operation : Backend.Operation) (spec : OperationSignature F operation) (certified : Backend.Certified spec) (execute : OperationSignature F operation) (execute_eq_certified : execute = certified.run) : Capability F operation

Build a singleton capability whose public entry point names its certified kernel directly.

This is the common package for formats whose planner has one genuine implementation. The singleton still participates in inspection and selection proofs, while execute remains a first-order format kernel.

@[instance_reducible, always_inline]

def FloatLib.Floats.ExecFloat.Capability.ofCertified {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] (operation : Backend.Operation) {spec : OperationSignature F operation} (certified : Backend.Certified spec) : Capability F operation

Build a direct capability from a certificate whose stored kernel is the public entry point.

This is the common case for statically selected backends. It keeps operation-specific planners from repeating the same certificate projection and reflexive equality, while preserving the first-order kernel stored in certified.run.

@[inline]

def FloatLib.Floats.ExecFloat.Capability.selected {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] {operation : Backend.Operation} [self : Capability F operation] : Backend.Certified spec

Certified implementation selected from the candidates supplied by F.

theorem FloatLib.Floats.ExecFloat.Capability.selected_eq_planner {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] {operation : Backend.Operation} [self : Capability F operation] : selected = Backend.selectCertified planning.policy candidates

The stored selected certificate equals the planner's result.

@[inline]

def FloatLib.Floats.ExecFloat.Capability.selectedCandidate {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] {operation : Backend.Operation} [Capability F operation] : Backend.Candidate

Static estimate attached to the selected implementation.

@[inline]

def FloatLib.Floats.ExecFloat.Capability.run {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] {operation : Backend.Operation} [self : Capability F operation] : OperationSignature F operation

Execute the selected logical operation.

The operation is certified in Lean; a family-specific compiled replacement may have an additional trust boundary documented by that family.

theorem FloatLib.Floats.ExecFloat.Capability.run_eq_spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] {operation : Backend.Operation} [self : Capability F operation] : run = spec

The selected executable operation agrees with its reference semantics.