Executable arithmetic capabilities

A capability bundles an operation's specification, its certified implementations, and their cost estimates. The selector starts from a mandatory baseline and uses the estimates to consider alternatives within the resource limits. The named operations in ExecFloat.Core.Operations use this indexed contract.

Capability.run_eq_spec is an equality of Lean definitions. The binary software kernels use proved refinements and @[csimp] replacements, so their compiled correctness also depends on the compiler. The binary32/binary64 NativeFPU.Unchecked host functions are not capabilities, because they have no packed-word equality theorem of the kind Backend.Certified requires.

@[reducible, inline]

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

Function type of each arithmetic operation over one encoded format.

Indexing by Backend.Operation keeps addition, subtraction, multiplication, division, square root, and FMA distinct capabilities even when two of them share a 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 keeps the instances of different operations apart without six structurally identical planner records.

• spec : OperationSignature F operation

  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 store a winner.

  The first projection runs the planner and later projections reuse the selected certificate. Static built-in formats skip even this projection by supplying implementation.

• implementation : Backend.Certified spec

  Certified implementation whose run public arithmetic computes.

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

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

  The stored certificate is the planner's winner over candidates under the policy in scope.

  A static package that stores the winner for code generation must prove that the planner selects that same certificate. Inspection tools such as #float_info report implementation. The equation holds in Lean's logic and says nothing about the generated machine code.

• execute : OperationSignature F operation

  First-order executable entry point that public arithmetic runs.

  The default projects the selected certificate. A static format may name the proved kernel itself, which lets Lean erase the certificate and typeclass dictionaries from monomorphic calls without changing the selection metadata or the correctness boundary.

• execute_eq_implementation : execute = implementation.run

  The entry point execute 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 kernel. Code named here must not acquire an unproved compiler replacement, because the equation is about the logical kernel and says nothing about 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 candidate set and a first-order dispatcher equal to spec.

The candidates stay authoritative for inspection and certification. A separate execute lets a format run the selected behavior without keeping 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 from one certified kernel and an entry point equal to its run.

Formats whose planner has one implementation use this package. The singleton still takes part in inspection and selection proofs, and execute stays 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 singleton capability whose entry point is the certificate's stored kernel certified.run.

Statically selected backends use it, so operation-specific planners do not repeat the same certificate projection and rfl proof.

@[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 add a trust boundary, which that family documents.

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

run agrees with the capability's reference semantics.

class FloatLib.Floats.ExecFloat.Capability.HasSpec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] {operation : Backend.Operation} (cap : Capability F operation) (spec : outParam (OperationSignature F operation)) : Prop

HasSpec cap spec states that the capability cap has the reference operation spec.

Instance search proves it whenever cap.spec unfolds to spec, as it does for every capability instance that names its reference operation. A theorem about a function that runs the selected capability takes HasSpec as an instance argument to learn which reference the kernel computes, and run_eq_spec then rewrites the kernel to that reference.

• spec_eq : Capability.spec = spec

  The capability's reference operation is spec.

instance FloatLib.Floats.ExecFloat.Capability.instHasSpecSpec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] {operation : Backend.Operation} (cap : Capability F operation) : cap.HasSpec spec

Every capability has its own reference operation.