Miri.Interpreter.Float

Miri.Interpreter.instDecidableEqFloatBits.decEq { format := a, bits := a_1 } { format := b, bits := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

source

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqFloatBits :

DecidableEq FloatBits

Equations

Miri.Interpreter.instDecidableEqFloatBits = Miri.Interpreter.instDecidableEqFloatBits.decEq

source

@[instance_reducible]

instance Miri.Interpreter.instReprFloatBits :

Repr FloatBits

Equations

Miri.Interpreter.instReprFloatBits = { reprPrec := Miri.Interpreter.instReprFloatBits.repr }

source

def Miri.Interpreter.instReprFloatBits.repr :

FloatBits → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

inductive Miri.Interpreter.FloatClass :

Type

finite (numerator denominator : Nat) : FloatClass
infinite : FloatClass
nan (payload : Nat) : FloatClass

Instances For

source

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqFloatClass :

DecidableEq FloatClass

Equations

Miri.Interpreter.instDecidableEqFloatClass = Miri.Interpreter.instDecidableEqFloatClass.decEq

source

def Miri.Interpreter.instDecidableEqFloatClass.decEq (x✝ x✝¹ : FloatClass) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Miri.Interpreter.instDecidableEqFloatClass.decEq (Miri.Interpreter.FloatClass.finite numerator denominator) Miri.Interpreter.FloatClass.infinite = isFalse ⋯
Miri.Interpreter.instDecidableEqFloatClass.decEq (Miri.Interpreter.FloatClass.finite numerator denominator) (Miri.Interpreter.FloatClass.nan payload) = isFalse ⋯
Miri.Interpreter.instDecidableEqFloatClass.decEq Miri.Interpreter.FloatClass.infinite (Miri.Interpreter.FloatClass.finite numerator denominator) = isFalse ⋯
Miri.Interpreter.instDecidableEqFloatClass.decEq Miri.Interpreter.FloatClass.infinite Miri.Interpreter.FloatClass.infinite = isTrue ⋯
Miri.Interpreter.instDecidableEqFloatClass.decEq Miri.Interpreter.FloatClass.infinite (Miri.Interpreter.FloatClass.nan payload) = isFalse ⋯
Miri.Interpreter.instDecidableEqFloatClass.decEq (Miri.Interpreter.FloatClass.nan payload) (Miri.Interpreter.FloatClass.finite numerator denominator) = isFalse ⋯
Miri.Interpreter.instDecidableEqFloatClass.decEq (Miri.Interpreter.FloatClass.nan payload) Miri.Interpreter.FloatClass.infinite = isFalse ⋯
Miri.Interpreter.instDecidableEqFloatClass.decEq (Miri.Interpreter.FloatClass.nan a) (Miri.Interpreter.FloatClass.nan b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source

@[instance_reducible]

instance Miri.Interpreter.instReprFloatClass :

Repr FloatClass

Equations

Miri.Interpreter.instReprFloatClass = { reprPrec := Miri.Interpreter.instReprFloatClass.repr }

source

def Miri.Interpreter.instReprFloatClass.repr :

FloatClass → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure Miri.Interpreter.FloatDecoded :

Type

negative : Bool
value : FloatClass

Instances For

source

def Miri.Interpreter.instDecidableEqFloatDecoded.decEq (x✝ x✝¹ : FloatDecoded) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqFloatDecoded :

DecidableEq FloatDecoded

Equations

Miri.Interpreter.instDecidableEqFloatDecoded = Miri.Interpreter.instDecidableEqFloatDecoded.decEq

source

def Miri.Interpreter.instReprFloatDecoded.repr :

FloatDecoded → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[instance_reducible]

instance Miri.Interpreter.instReprFloatDecoded :

Repr FloatDecoded

Equations

Miri.Interpreter.instReprFloatDecoded = { reprPrec := Miri.Interpreter.instReprFloatDecoded.repr }

source

inductive Miri.Interpreter.FloatError :

Type

encodingExceedsWidth : FloatError
zeroDenominator : FloatError
formatMismatch : FloatError
invalidBinaryOperator (op : MIR.BinOp) : FloatError
invalidIntegerWidth (width : Nat) : FloatError
inconsistentRounding : FloatError
invalidNaNChoice : FloatError

Instances For

source

@[instance_reducible]

instance Miri.Interpreter.instDecidableEqFloatError :

DecidableEq FloatError

Equations

Miri.Interpreter.instDecidableEqFloatError = Miri.Interpreter.instDecidableEqFloatError.decEq

source

def Miri.Interpreter.instDecidableEqFloatError.decEq (x✝ x✝¹ : FloatError) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

def Miri.Interpreter.instReprFloatError.repr :

FloatError → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[instance_reducible]

instance Miri.Interpreter.instReprFloatError :

Repr FloatError

Equations

Miri.Interpreter.instReprFloatError = { reprPrec := Miri.Interpreter.instReprFloatError.repr }

source

def Miri.Interpreter.FloatBits.zero (f : FloatFormat) (negative : Bool := false) :

FloatBits

Equations

Miri.Interpreter.FloatBits.zero f negative = Miri.Interpreter.FloatBits.encode✝ f negative 0 0

Instances For

source

def Miri.Interpreter.FloatBits.infinity (f : FloatFormat) (negative : Bool := false) :

FloatBits

Equations

Miri.Interpreter.FloatBits.infinity f negative = Miri.Interpreter.FloatBits.encode✝ f negative (2 ^ f.exponentBits - 1) 0

Instances For

source

def Miri.Interpreter.FloatBits.preferredNaN (f : FloatFormat) :

FloatBits

Equations

Miri.Interpreter.FloatBits.preferredNaN f = Miri.Interpreter.FloatBits.encode✝ f false (2 ^ f.exponentBits - 1) (2 ^ (f.fractionBits - 1))

Instances For

source

def Miri.Interpreter.FloatBits.decode (x : FloatBits) :

Except FloatError FloatDecoded

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.negate (x : FloatBits) :

Except FloatError FloatBits

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.isNaN (x : FloatBits) :

Except FloatError Bool

Equations

x.isNaN = do let __do_lift ← x.decode pure (match __do_lift.value with | Miri.Interpreter.FloatClass.nan payload => true | x => false)

Instances For

source

def Miri.Interpreter.FloatBits.isSignaling (x : FloatBits) :

Except FloatError Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.roundRatio (f : FloatFormat) (negative : Bool) (n d : Nat) :

Except FloatError FloatBits

Round an exact nonnegative rational with a separate sign. Clamping the working exponent to MIN_EXP gives gradual subnormal underflow, including ties at signed zero. Overflow after rounding produces infinity.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.convert (x : FloatBits) (target : FloatFormat) :

Except FloatError FloatBits

Cast finite values with correct rounding. NaN payload conversion first quiets, shifts to the target precision, and forces the target quiet bit, as pinned ieee.rs::convert_r does. Miri's adjust_nan is applied separately.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.nanChoices (target : FloatFormat) (inputs : List FloatBits) (nondeterministic : Bool) :

Except FloatError (List FloatBits)

All outcomes generated by pinned Miri operator.rs::generate_nan. Sign choice is independent of candidate choice. A fixed seed is not a safety model.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.arithmetic (op : MIR.BinOp) (left right : FloatBits) :

Except FloatError FloatBits

MIR arithmetic's base result. NaN payload/sign selection is subsequently performed by nanChoices/adjust_nan; finite arithmetic never calls a host float.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.partialCompare (left right : FloatBits) :

Except FloatError (Option Ordering)

IEEE partial ordering: both signs of zero compare equal; all NaNs are unordered. Infinities are ordered without rational approximation.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.comparison (op : MIR.BinOp) (left right : FloatBits) :

Except FloatError Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Miri.Interpreter.FloatBits.fromInteger (format : FloatFormat) (value : Int) :

Except FloatError FloatBits

Equations

Miri.Interpreter.FloatBits.fromInteger format value = Miri.Interpreter.FloatBits.roundRatio format (decide (value < 0)) value.natAbs 1

Instances For

source

def Miri.Interpreter.FloatBits.toInteger (value : FloatBits) (width : Nat) (isSigned : Bool) :

Except FloatError Int

Rust as float-to-int conversion saturates and truncates toward zero; NaNs map to zero. Width and signedness are from the target compiler layout.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Miri.Interpreter.FloatBits.roundRatio_zero (format : FloatFormat) (negative : Bool) (denominator : Nat) (nonzero : denominator ≠ 0) :

roundRatio format negative 0 denominator = Except.ok (zero format negative)

Every exact zero retains its input sign under nearest-even conversion.

source

theorem Miri.Interpreter.FloatBits.nan_toInteger (value : FloatBits) (negative : Bool) (payload width : Nat) (decoded : value.decode = Except.ok { negative := negative, value := FloatClass.nan payload }) (nonzero : width ≠ 0) (bounded : width ≤ 128) (isSigned : Bool) :

value.toInteger width isSigned = Except.ok 0

Saturating integer casts of any decoded NaN are exactly zero.