Core conversion capabilities and outcomes

A source's ExactDecoder gives its exact value. An ExactMap embeds that value into the destination's exact domain, and a Quantizer rounds it under an explicit policy. ConversionOutcome retains the resulting value and flags, or the reason conversion failed.

The entry points are in Conversion.Runtime; their correctness theorems and the laws for composing outcomes are in Conversion.Proof.

inductive FloatLib.Floats.ExecFloat.InputPosition : Type

Location of an input that prevented a conversion or mixed operation.

• source : InputPosition

  The sole input of a conversion.

• left : InputPosition

  The left input of a binary or fused operation.

• right : InputPosition

  The right input of a binary or fused operation.

• addend : InputPosition

  The third input of a fused multiply-add.

• operand (index : ℕ) : InputPosition

  A zero-based input of a user-defined exact expression.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instDecidableEqInputPosition : DecidableEq InputPosition

def FloatLib.Floats.ExecFloat.instDecidableEqInputPosition.decEq (x✝ x✝¹ : InputPosition) : Decidable (x✝ = x✝¹)

def FloatLib.Floats.ExecFloat.instReprInputPosition.repr : InputPosition → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instReprInputPosition : Repr InputPosition

inductive FloatLib.Floats.ExecFloat.ConversionFailure : Type

Why an explicit conversion or mixed-format operation produced no destination value.

• infinity (position : InputPosition) (negative : Bool) : ConversionFailure

  An infinity reached an operation that requires an ordinary finite input.

• exceptional (position : InputPosition) (value : Numerics.ExceptionalValue) : ConversionFailure

  An exceptional value reached an operation that requires an ordinary finite input.

• divisionByZero : ConversionFailure

  Exact division was requested with a zero denominator.

• outOfRange : ConversionFailure

  A finite exact result is outside a destination configured to reject overflow.

• unsupportedPolicy : ConversionFailure

  The requested family-specific conversion policy is not implemented by the destination.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instDecidableEqConversionFailure : DecidableEq ConversionFailure

def FloatLib.Floats.ExecFloat.instDecidableEqConversionFailure.decEq (x✝ x✝¹ : ConversionFailure) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instReprConversionFailure : Repr ConversionFailure

def FloatLib.Floats.ExecFloat.instReprConversionFailure.repr : ConversionFailure → ℕ → Std.Format

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.ExactExpression (Exact : Type u) : Type u

An exact scalar computation that may reject a non-finite input or an undefined operation.

Successful expressions contain an unrounded value in the destination's exact domain. Applying roundOnce or roundOnceWith quantizes the result once. The Except alias supports ordinary do notation and stops at the first failure.

structure FloatLib.Floats.ExecFloat.ConversionStatus : Type

Representation-independent information about a successful quantization.

Flags describe one conversion. saturated and wrapped distinguish clamping from modular reduction; either can also be inexact. Composing successful outcomes with bind combines their flags with Boolean OR. A failed continuation returns its failure reason without accumulated flags.

• inexact : Bool

  The stored destination does not denote the exact finite input.

• overflow : Bool

  The rounded result did not fit the destination's finite range. Binary destinations set this after rounding, in the IEEE 754 sense; each quantizer documents its own rule.

• underflow : Bool

  The result was tiny. Binary destinations use the IEEE 754 rule, tiny after rounding and inexact; P3109 reports a nonzero exact input below its least positive datum.

• saturated : Bool

  The result was clamped to a finite endpoint.

• wrapped : Bool

  The result was reduced modulo a bounded storage width.

• mappedSpecial : Bool

  A source infinity or exceptional value was mapped to another value class.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instDecidableEqConversionStatus : DecidableEq ConversionStatus

def FloatLib.Floats.ExecFloat.instDecidableEqConversionStatus.decEq (x✝ x✝¹ : ConversionStatus) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instReprConversionStatus : Repr ConversionStatus

def FloatLib.Floats.ExecFloat.instReprConversionStatus.repr : ConversionStatus → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instInhabitedConversionStatus : Inhabited ConversionStatus

@[inline]

def FloatLib.Floats.ExecFloat.ConversionStatus.merge (first second : ConversionStatus) : ConversionStatus

Combine the flags raised by two successful conversion steps.

inductive FloatLib.Floats.ExecFloat.ConversionOutcome (α : Type u) : Type u

Result of an explicit conversion or destination-driven mixed operation.

• success {α : Type u} (value : α) (status : ConversionStatus := { }) : ConversionOutcome α

  A destination value together with conversion status.

• failure {α : Type u} (reason : ConversionFailure) : ConversionOutcome α

  A conversion rejected by its explicit policy or by finite-only mixed arithmetic.

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

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instDecidableEqConversionOutcome {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (ConversionOutcome α✝)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instReprConversionOutcome {α✝ : Type u_1} [Repr α✝] : Repr (ConversionOutcome α✝)

def FloatLib.Floats.ExecFloat.instReprConversionOutcome.repr {α✝ : Type u_1} [Repr α✝] : ConversionOutcome α✝ → ℕ → Std.Format

@[inline]

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

Transform a successful value while preserving status and failure information.

@[inline]

def FloatLib.Floats.ExecFloat.ConversionOutcome.bind {α : Type u} {β : Type v} (outcome : ConversionOutcome α) (next : α → ConversionOutcome β) : ConversionOutcome β

Continue from a successful value, accumulating status from both successful steps.

A failure short-circuits unchanged. Because ConversionOutcome.failure does not carry status, flags from an earlier success are unavailable when a later step fails.

@[inline]

def FloatLib.Floats.ExecFloat.ConversionOutcome.value? {α : Type u} : ConversionOutcome α → Option α

Extract a successful destination value.

@[inline]

def FloatLib.Floats.ExecFloat.ConversionOutcome.status? {α : Type u} : ConversionOutcome α → Option ConversionStatus

Extract status from a successful conversion.

@[inline]

def FloatLib.Floats.ExecFloat.ConversionOutcome.failure? {α : Type u} : ConversionOutcome α → Option ConversionFailure

Extract the reason for a failed conversion.

class FloatLib.Floats.ExecFloat.ExactDecoder (Source : Type u) (Exact : outParam (Type v)) : Type (max u v)

Executable exact interpretation of a source value.

Exact is an output parameter so the source type selects its canonical executable exact domain. For example, configured binary sources select SignedRat to retain signed zero, posit sources select Rat, and a shared-scale block may select Vector Rat lanes.

• decode : Source → Numerics.NumericalValue Exact

  Decode every source value, retaining infinity and exceptional observations.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactDecoder.natural : ExactDecoder ℕ ℕ

Natural numbers enter explicit conversion as exact finite natural values.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactDecoder.integer : ExactDecoder ℤ ℤ

Integers enter explicit conversion as exact finite integer values.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactDecoder.rational : ExactDecoder ℚ ℚ

Rationals enter explicit conversion without an intermediate floating-point approximation.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.ExactDecoder.dyadic : ExactDecoder Numerics.Dyadic Numerics.Dyadic

Dyadic values enter explicit conversion with their exact significand and binary exponent.

class FloatLib.Floats.ExecFloat.Quantizer (Destination : Type u) (Exact : outParam (Type v)) : Type (max (max 1 u) v)

Context-indexed quantization capability for one destination value type.

The specification is relational so stochastic, state-indexed, and otherwise nondeterministic mathematics remain expressible even when run chooses one executable result.

Exact is an output parameter: a destination has one canonical mathematical input domain. Alternative execution backends must refine that same semantics rather than changing the domain seen by users. Sources with a different exact domain reach it through an explicit ExactMap.

Mixed addition and subtraction also consult this context before quantization. The default operations are those of Exact; a signed-zero domain can refine the sign of an exact cancellation without changing its numerical value. Multiplication and division use the exact domain directly.

Preservation of the numerical sum and difference is a separate family-specific proof obligation. correct relates run to spec; it does not constrain these arithmetic hooks. The generic prepared-spec theorems compose quantization with the supplied hooks. An arithmetic correctness result also needs their numerical preservation lemmas, as supplied by the binary instances.

The relation's content is a separate obligation: choosing Spec.ofFunction run makes correct reflexive and supplies no independent rounding property. A family contract can expose denotation, coefficient, or policy predicates while retaining complete output and status equality. The generic conversion theorems transport precisely the clauses that the installed relation contains.

• Context : Type

  Family-specific context, such as rounding policy, entropy, overflow rule, or block exponent.

• run : Context Destination → Numerics.NumericalValue Exact → ConversionOutcome Destination

  Executable quantizer.

• spec : Numerics.Quantization.Spec (Context Destination) (Numerics.NumericalValue Exact) (ConversionOutcome Destination)

  Mathematical relation implemented by run.

• correct : spec.Implements run

  The executable quantizer always chooses a result permitted by spec.

• addExact [Add Exact] : Context Destination → Exact → Exact → Exact

  Exact addition under the destination context, including any direction-dependent zero sign.

  A family overriding this operation must retain the numerical sum in its exact domain.

• subExact [Sub Exact] : Context Destination → Exact → Exact → Exact

  Exact subtraction under the destination context, including any direction-dependent zero sign.

  A family overriding this operation must retain the numerical difference in its exact domain.

class FloatLib.Floats.ExecFloat.DefaultQuantizer (Destination : Type u) (Exact : outParam (Type v)) [Quantizer Destination Exact] : Type

The default context used when a conversion omits an explicit policy.

• defaultContext : Quantizer.Context Destination

  Context selected by the context-free cast and mixed-operation helpers.