Typed MIR and cast adapters. Canonical compiler type/format/layout queries remain mandatory; every generated NaN choice is checked against the pinned Miri candidate relation, rather than trusting a random seed or host float.

structure Miri.Interpreter.FloatOpsHooks (P S C : Type) : Type

• integerKindOf : C → MIR.TyId → RvalueM S MIR.IntegerKind
• formatOf : C → MIR.TyId → RvalueM S FloatFormat
• boolLayout : C → RvalueM S (ABI.TyAndLayout MIR.TyId)
• floatNondeterministic : Bool
• chooseNaN : C → List FloatBits → RvalueM S Nat

def Miri.Interpreter.FloatOps.readBits {P S C : Type} [Memory.PointerProvenance P] (h : FloatOpsHooks P S C) (choice : C) (value : RvalueImmTy P) : RvalueM S FloatBits

Equations

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

def Miri.Interpreter.FloatOps.adjustNaN {P S C : Type} (h : FloatOpsHooks P S C) (choice : C) (value : FloatBits) (inputs : List FloatBits) : RvalueM S FloatBits

Equations

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

def Miri.Interpreter.FloatOps.binary {P S C : Type} [Memory.PointerProvenance P] (h : FloatOpsHooks P S C) (choice : C) (op : MIR.BinOp) (left right : RvalueImmTy P) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.FloatOps.unary {P S C : Type} [Memory.PointerProvenance P] (h : FloatOpsHooks P S C) (choice : C) (op : MIR.UnOp) (value : RvalueImmTy P) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.FloatOps.castFloatToFloat {P S C : Type} [Memory.PointerProvenance P] (h : FloatOpsHooks P S C) (choice : C) (value : RvalueImmTy P) (target : ABI.TyAndLayout MIR.TyId) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.FloatOps.castFloatToInt {P S C : Type} [Memory.PointerProvenance P] (h : FloatOpsHooks P S C) (choice : C) (value : RvalueImmTy P) (target : ABI.TyAndLayout MIR.TyId) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.FloatOps.castIntToFloat {P S C : Type} [Memory.PointerProvenance P] (h : FloatOpsHooks P S C) (choice : C) (value : RvalueImmTy P) (target : ABI.TyAndLayout MIR.TyId) : RvalueM S (RvalueImmTy P)

Equations

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