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 the policy of its context. ConversionOutcome retains the resulting value and flags, or the reason conversion failed. RoundingModes and ModeContext give the type of a conversion's (mode := ...) option and the destination context each mode selects.

Conversion.Runtime has the entry points, and Conversion.Proof has their correctness theorems and the laws for composing outcomes.

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 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, and either can also be inexact. Composing successful outcomes with bind combines their flags with Boolean OR.

• 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.

• invalid : Bool

  The conversion signaled invalid operation. Binary destinations raise it for a signaling NaN source, as IEEE 754 §7.2 requires.

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

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instDecidableEqConversionStatus : DecidableEq ConversionStatus

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

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instReprConversionStatus : Repr ConversionStatus

@[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 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.

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

Exact is an output parameter, so a destination has one canonical mathematical input domain. Alternative execution backends must refine that semantics and keep the domain users see. Sources with a different exact domain reach it through an ExactMap.

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

correct relates run to spec and does not constrain these arithmetic hooks, so a family proves separately that its hooks keep the numerical sum and difference. The generic prepared-spec theorems compose quantization with the supplied hooks, and an arithmetic correctness result also needs those preservation lemmas, as the binary instances supply.

What spec says is up to the family. Choosing Spec.ofFunction run makes correct reflexive and gives no rounding property of its own. A family contract can expose denotation, coefficient or policy predicates while keeping full output and status equality, and the generic conversion theorems transport the clauses that the installed relation contains and no others.

• 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 canonical context used when a conversion or mixed operation names neither mode nor context.

• defaultContext : Quantizer.Context Destination

  Context selected by a conversion that names neither mode nor context.

class FloatLib.Floats.ExecFloat.RoundingModes (Destination : Type u) (Mode : outParam Type) : Type

The type of the mode option of conversions into Destination, with the direction used when a call names none.

Binary destinations use IEEERoundingMode, nearest-even by default. A destination without directed conversion falls back to RoundingModes.unit, so naming a direction for it is a type error rather than an ignored option.

• default : Mode

  The direction used when a call names no mode.

@[instance_reducible, instance 100]

instance FloatLib.Floats.ExecFloat.RoundingModes.unit {Destination : Type u} : RoundingModes Destination Unit

A destination without selectable rounding directions has the single mode ().

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.ContextFor (Destination : Type u) {Exact : Type v} [quantizer : Quantizer Destination Exact] {Mode : Type} (_mode : Mode) : Type

The context type of Destination, indexed by the mode that selects its default.

Conversions take (context : ContextFor target mode := ...). The index lets the default value find ModeContext target mode, and a caller's context of type Quantizer.Context target fits because the two types are definitionally equal.

class FloatLib.Floats.ExecFloat.ModeContext (Destination : Type u) (Exact : outParam (Type v)) [Quantizer Destination Exact] {Mode : Type} (mode : Mode) : Type

The destination context that a conversion's mode option selects when it names no context.

ModeContext.canonical gives the canonical context to every destination with a DefaultQuantizer and no rounding directions. Binary destinations install an instance for every direction. A destination without a canonical context, such as a shared-scale block, has no instance and needs a context argument.

• context : ContextFor Destination mode

  The context that rounds in direction mode.

@[instance_reducible, inline]

instance FloatLib.Floats.ExecFloat.ModeContext.canonical {Destination : Type u} {Exact : Type v} [Quantizer Destination Exact] [defaults : DefaultQuantizer Destination Exact] (mode : Unit) : ModeContext Destination Exact mode

A destination without rounding directions uses its canonical context for its one mode.