Uniform operation-specific capability API

The public Add, Sub, Mul, Div, Sqrt, and Fma namespaces derive their interfaces from the single indexed Capability contract. Each namespace exposes the same planning and certification surface while retaining the operation's natural arity.

@[inline]

def FloatLib.Floats.ExecFloat.Add.spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.add] : OperationSignature F Backend.Operation.add

Clear reference operation for this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Add.candidates {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.add] : Backend.CandidateSet (Backend.Certified spec)

Certified kernels offered by this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Add.policy {F : Type u} [planning : Backend.PolicyFor F] : Backend.Policy

Workload and resource policy shared by planning and execution.

@[inline]

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

Certified implementation selected from the candidates supplied by the format.

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

The stored selected certificate equals the planner's result.

@[inline]

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

Static estimate attached to the selected implementation.

@[inline]

def FloatLib.Floats.ExecFloat.Add.run {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.add] : ExecFloat F → ExecFloat F → ExecFloat F

Execute the selected binary kernel.

theorem FloatLib.Floats.ExecFloat.Add.run_eq_spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.add] (left✝ right✝ : ExecFloat F) : run left✝ right✝ = spec left✝ right✝

The selected binary kernel agrees with its reference operation.

@[inline]

def FloatLib.Floats.ExecFloat.Sub.spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.sub] : OperationSignature F Backend.Operation.sub

Clear reference operation for this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Sub.candidates {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.sub] : Backend.CandidateSet (Backend.Certified spec)

Certified kernels offered by this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Sub.policy {F : Type u} [planning : Backend.PolicyFor F] : Backend.Policy

Workload and resource policy shared by planning and execution.

@[inline]

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

Certified implementation selected from the candidates supplied by the format.

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

The stored selected certificate equals the planner's result.

@[inline]

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

Static estimate attached to the selected implementation.

@[inline]

def FloatLib.Floats.ExecFloat.Sub.run {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.sub] : ExecFloat F → ExecFloat F → ExecFloat F

Execute the selected binary kernel.

theorem FloatLib.Floats.ExecFloat.Sub.run_eq_spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.sub] (left✝ right✝ : ExecFloat F) : run left✝ right✝ = spec left✝ right✝

The selected binary kernel agrees with its reference operation.

@[inline]

def FloatLib.Floats.ExecFloat.Mul.spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.mul] : OperationSignature F Backend.Operation.mul

Clear reference operation for this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Mul.candidates {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.mul] : Backend.CandidateSet (Backend.Certified spec)

Certified kernels offered by this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Mul.policy {F : Type u} [planning : Backend.PolicyFor F] : Backend.Policy

Workload and resource policy shared by planning and execution.

@[inline]

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

Certified implementation selected from the candidates supplied by the format.

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

The stored selected certificate equals the planner's result.

@[inline]

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

Static estimate attached to the selected implementation.

@[inline]

def FloatLib.Floats.ExecFloat.Mul.run {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.mul] : ExecFloat F → ExecFloat F → ExecFloat F

Execute the selected binary kernel.

theorem FloatLib.Floats.ExecFloat.Mul.run_eq_spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.mul] (left✝ right✝ : ExecFloat F) : run left✝ right✝ = spec left✝ right✝

The selected binary kernel agrees with its reference operation.

@[inline]

def FloatLib.Floats.ExecFloat.Div.spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.div] : OperationSignature F Backend.Operation.div

Clear reference operation for this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Div.candidates {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.div] : Backend.CandidateSet (Backend.Certified spec)

Certified kernels offered by this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Div.policy {F : Type u} [planning : Backend.PolicyFor F] : Backend.Policy

Workload and resource policy shared by planning and execution.

@[inline]

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

Certified implementation selected from the candidates supplied by the format.

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

The stored selected certificate equals the planner's result.

@[inline]

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

Static estimate attached to the selected implementation.

@[inline]

def FloatLib.Floats.ExecFloat.Div.run {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.div] : ExecFloat F → ExecFloat F → ExecFloat F

Execute the selected binary kernel.

theorem FloatLib.Floats.ExecFloat.Div.run_eq_spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.div] (left✝ right✝ : ExecFloat F) : run left✝ right✝ = spec left✝ right✝

The selected binary kernel agrees with its reference operation.

@[inline]

def FloatLib.Floats.ExecFloat.Sqrt.spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.sqrt] : OperationSignature F Backend.Operation.sqrt

Clear reference operation for this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Sqrt.candidates {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.sqrt] : Backend.CandidateSet (Backend.Certified spec)

Certified kernels offered by this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Sqrt.policy {F : Type u} [planning : Backend.PolicyFor F] : Backend.Policy

Workload and resource policy shared by planning and execution.

@[inline]

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

Certified implementation selected from the candidates supplied by the format.

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

The stored selected certificate equals the planner's result.

@[inline]

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

Static estimate attached to the selected implementation.

@[inline]

def FloatLib.Floats.ExecFloat.Sqrt.run {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.sqrt] : ExecFloat F → ExecFloat F

Execute the selected unary kernel.

theorem FloatLib.Floats.ExecFloat.Sqrt.run_eq_spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.sqrt] (value✝ : ExecFloat F) : run value✝ = spec value✝

The selected unary kernel agrees with its reference operation.

@[inline]

def FloatLib.Floats.ExecFloat.Fma.spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.fma] : OperationSignature F Backend.Operation.fma

Clear reference operation for this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Fma.candidates {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.fma] : Backend.CandidateSet (Backend.Certified spec)

Certified kernels offered by this capability.

@[inline]

def FloatLib.Floats.ExecFloat.Fma.policy {F : Type u} [planning : Backend.PolicyFor F] : Backend.Policy

Workload and resource policy shared by planning and execution.

@[inline]

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

Certified implementation selected from the candidates supplied by the format.

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

The stored selected certificate equals the planner's result.

@[inline]

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

Static estimate attached to the selected implementation.

@[inline]

def FloatLib.Floats.ExecFloat.Fma.run {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.fma] : ExecFloat F → ExecFloat F → ExecFloat F → ExecFloat F

Execute the selected ternary kernel.

theorem FloatLib.Floats.ExecFloat.Fma.run_eq_spec {F : Type u} [Numerics.EncodedFormat F] [planning : Backend.PolicyFor F] [Capability F Backend.Operation.fma] (left✝ right✝ addend✝ : ExecFloat F) : run left✝ right✝ addend✝ = spec left✝ right✝ addend✝

The selected ternary kernel agrees with its reference operation.