The integer-or-pointer scalar core from mir/interpret/value.rs. Floating point wrappers are intentionally absent until the pinned apfloat conversion semantics are available; no host-float approximation is used.

inductive Miri.Memory.ScalarError : Type

• scalarInt (reason : ScalarIntError) : ScalarError
• pointerSizeMismatch (expected actual : ABI.Size) : ScalarError
• pointerOffsetDoesNotFit (offset targetSize : ABI.Size) : ScalarError
• integerConversionOverflow (bits : ABI.U128) : ScalarError
• provenanceHasNoAllocationId : ScalarError
• readPointerAsInt : ScalarError
• zeroSizedBits : ScalarError

@[instance_reducible]

instance Miri.Memory.instDecidableEqScalarError : DecidableEq ScalarError

Equations

• Miri.Memory.instDecidableEqScalarError = Miri.Memory.instDecidableEqScalarError.decEq

def Miri.Memory.instDecidableEqScalarError.decEq (x✝ x✝¹ : ScalarError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.scalarInt a) (Miri.Memory.ScalarError.scalarInt b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.scalarInt reason) (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.scalarInt reason) (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.scalarInt reason) (Miri.Memory.ScalarError.integerConversionOverflow bits) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.scalarInt reason) Miri.Memory.ScalarError.provenanceHasNoAllocationId = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.scalarInt reason) Miri.Memory.ScalarError.readPointerAsInt = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.scalarInt reason) Miri.Memory.ScalarError.zeroSizedBits = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) (Miri.Memory.ScalarError.scalarInt reason) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) (Miri.Memory.ScalarError.integerConversionOverflow bits) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) Miri.Memory.ScalarError.provenanceHasNoAllocationId = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) Miri.Memory.ScalarError.readPointerAsInt = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) Miri.Memory.ScalarError.zeroSizedBits = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) (Miri.Memory.ScalarError.scalarInt reason) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) (Miri.Memory.ScalarError.integerConversionOverflow bits) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) Miri.Memory.ScalarError.provenanceHasNoAllocationId = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) Miri.Memory.ScalarError.readPointerAsInt = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) Miri.Memory.ScalarError.zeroSizedBits = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.integerConversionOverflow bits) (Miri.Memory.ScalarError.scalarInt reason) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.integerConversionOverflow bits) (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.integerConversionOverflow bits) (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.integerConversionOverflow bits) Miri.Memory.ScalarError.provenanceHasNoAllocationId = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.integerConversionOverflow bits) Miri.Memory.ScalarError.readPointerAsInt = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq (Miri.Memory.ScalarError.integerConversionOverflow bits) Miri.Memory.ScalarError.zeroSizedBits = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.provenanceHasNoAllocationId (Miri.Memory.ScalarError.scalarInt reason) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.provenanceHasNoAllocationId (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.provenanceHasNoAllocationId (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.provenanceHasNoAllocationId (Miri.Memory.ScalarError.integerConversionOverflow bits) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.provenanceHasNoAllocationId Miri.Memory.ScalarError.provenanceHasNoAllocationId = isTrue ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.readPointerAsInt (Miri.Memory.ScalarError.scalarInt reason) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.readPointerAsInt (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.readPointerAsInt (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.readPointerAsInt (Miri.Memory.ScalarError.integerConversionOverflow bits) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.readPointerAsInt Miri.Memory.ScalarError.readPointerAsInt = isTrue ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.readPointerAsInt Miri.Memory.ScalarError.zeroSizedBits = isFalse Miri.Memory.instDecidableEqScalarError.decEq._proof_46
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.zeroSizedBits (Miri.Memory.ScalarError.scalarInt reason) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.zeroSizedBits (Miri.Memory.ScalarError.pointerSizeMismatch expected actual) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.zeroSizedBits (Miri.Memory.ScalarError.pointerOffsetDoesNotFit offset targetSize) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.zeroSizedBits (Miri.Memory.ScalarError.integerConversionOverflow bits) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.zeroSizedBits Miri.Memory.ScalarError.readPointerAsInt = isFalse Miri.Memory.instDecidableEqScalarError.decEq._proof_52
• Miri.Memory.instDecidableEqScalarError.decEq Miri.Memory.ScalarError.zeroSizedBits Miri.Memory.ScalarError.zeroSizedBits = isTrue ⋯

@[instance_reducible]

instance Miri.Memory.instReprScalarError : Repr ScalarError

Equations

• Miri.Memory.instReprScalarError = { reprPrec := Miri.Memory.instReprScalarError.repr }

def Miri.Memory.instReprScalarError.repr : ScalarError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instToStringScalarError : ToString ScalarError

Equations

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

inductive Miri.Memory.ScalarPayload (Prov : Type) : Type

• integer {Prov : Type} (value : ScalarInt) : ScalarPayload Prov
• pointer {Prov : Type} (value : Pointer Prov) : ScalarPayload Prov

def Miri.Memory.instDecidableEqScalarPayload.decEq {Prov✝ : Type} [DecidableEq Prov✝] (x✝ x✝¹ : ScalarPayload Prov✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqScalarPayload.decEq (Miri.Memory.ScalarPayload.integer a) (Miri.Memory.ScalarPayload.integer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqScalarPayload.decEq (Miri.Memory.ScalarPayload.integer value) (Miri.Memory.ScalarPayload.pointer value_1) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarPayload.decEq (Miri.Memory.ScalarPayload.pointer value) (Miri.Memory.ScalarPayload.integer value_1) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarPayload.decEq (Miri.Memory.ScalarPayload.pointer a) (Miri.Memory.ScalarPayload.pointer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqScalarPayload {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (ScalarPayload Prov✝)

Equations

• Miri.Memory.instDecidableEqScalarPayload = Miri.Memory.instDecidableEqScalarPayload.decEq

@[instance_reducible]

instance Miri.Memory.instReprScalarPayload {Prov✝ : Type} [Repr Prov✝] : Repr (ScalarPayload Prov✝)

Equations

• Miri.Memory.instReprScalarPayload = { reprPrec := Miri.Memory.instReprScalarPayload.repr }

def Miri.Memory.instReprScalarPayload.repr {Prov✝ : Type} [Repr Prov✝] : ScalarPayload Prov✝ → Nat → Std.Format

Equations

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

inductive Miri.Memory.ScalarBitsOrPointer (Prov : Type) : Type

• bits {Prov : Type} (value : ABI.U128) : ScalarBitsOrPointer Prov
• pointer {Prov : Type} (value : Pointer Prov) : ScalarBitsOrPointer Prov

def Miri.Memory.instDecidableEqScalarBitsOrPointer.decEq {Prov✝ : Type} [DecidableEq Prov✝] (x✝ x✝¹ : ScalarBitsOrPointer Prov✝) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqScalarBitsOrPointer.decEq (Miri.Memory.ScalarBitsOrPointer.bits a) (Miri.Memory.ScalarBitsOrPointer.bits b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqScalarBitsOrPointer.decEq (Miri.Memory.ScalarBitsOrPointer.bits value) (Miri.Memory.ScalarBitsOrPointer.pointer value_1) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarBitsOrPointer.decEq (Miri.Memory.ScalarBitsOrPointer.pointer value) (Miri.Memory.ScalarBitsOrPointer.bits value_1) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarBitsOrPointer.decEq (Miri.Memory.ScalarBitsOrPointer.pointer a) (Miri.Memory.ScalarBitsOrPointer.pointer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqScalarBitsOrPointer {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (ScalarBitsOrPointer Prov✝)

Equations

• Miri.Memory.instDecidableEqScalarBitsOrPointer = Miri.Memory.instDecidableEqScalarBitsOrPointer.decEq

def Miri.Memory.instReprScalarBitsOrPointer.repr {Prov✝ : Type} [Repr Prov✝] : ScalarBitsOrPointer Prov✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprScalarBitsOrPointer {Prov✝ : Type} [Repr Prov✝] : Repr (ScalarBitsOrPointer Prov✝)

Equations

• Miri.Memory.instReprScalarBitsOrPointer = { reprPrec := Miri.Memory.instReprScalarBitsOrPointer.repr }

inductive Miri.Memory.ScalarIntCastResult : Type

• integer (value : ScalarInt) : ScalarIntCastResult
• erasedPointer (value : Pointer AllocId) (size : ABI.Size) : ScalarIntCastResult

@[instance_reducible]

instance Miri.Memory.instDecidableEqScalarIntCastResult : DecidableEq ScalarIntCastResult

Equations

• Miri.Memory.instDecidableEqScalarIntCastResult = Miri.Memory.instDecidableEqScalarIntCastResult.decEq

def Miri.Memory.instDecidableEqScalarIntCastResult.decEq (x✝ x✝¹ : ScalarIntCastResult) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqScalarIntCastResult.decEq (Miri.Memory.ScalarIntCastResult.integer a) (Miri.Memory.ScalarIntCastResult.integer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqScalarIntCastResult.decEq (Miri.Memory.ScalarIntCastResult.integer value) (Miri.Memory.ScalarIntCastResult.erasedPointer value_1 size) = isFalse ⋯
• Miri.Memory.instDecidableEqScalarIntCastResult.decEq (Miri.Memory.ScalarIntCastResult.erasedPointer value size) (Miri.Memory.ScalarIntCastResult.integer value_1) = isFalse ⋯

def Miri.Memory.instReprScalarIntCastResult.repr : ScalarIntCastResult → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprScalarIntCastResult : Repr ScalarIntCastResult

Equations

• Miri.Memory.instReprScalarIntCastResult = { reprPrec := Miri.Memory.instReprScalarIntCastResult.repr }

structure Miri.Memory.Scalar (Prov : Type := CtfeProvenance) : Type

• payload : Miri.Memory.ScalarPayload Prov
• scalarSize : Miri.ABI.Size

@[instance_reducible]

instance Miri.Memory.instDecidableEqScalar {Prov✝ : Type} [DecidableEq Prov✝] : DecidableEq (Scalar Prov✝)

Equations

• Miri.Memory.instDecidableEqScalar = Miri.Memory.instDecidableEqScalar.decEq

def Miri.Memory.instDecidableEqScalar.decEq {Prov✝ : Type} [DecidableEq Prov✝] (x✝ x✝¹ : Scalar Prov✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprScalar {Prov✝ : Type} [Repr Prov✝] : Repr (Scalar Prov✝)

Equations

• Miri.Memory.instReprScalar = { reprPrec := Miri.Memory.instReprScalar.repr }

def Miri.Memory.instReprScalar.repr {Prov✝ : Type} [Repr Prov✝] : Scalar Prov✝ → Nat → Std.Format

Equations

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

def Miri.Memory.Scalar.size {Prov : Type} (self : Scalar Prov) : ABI.Size

Equations

• self.size = Miri.Memory.Scalar.scalarSize✝ self

def Miri.Memory.Scalar.fromScalarInt {Prov : Type} (value : ScalarInt) : Scalar Prov

Equations

• Miri.Memory.Scalar.fromScalarInt value = { payload := Miri.Memory.ScalarPayload.integer value, scalarSize := value.size }

def Miri.Memory.Scalar.fromPointer {Prov : Type} (layout : ABI.TargetDataLayout) (value : Pointer Prov) : Scalar Prov

Equations

• Miri.Memory.Scalar.fromPointer layout value = { payload := Miri.Memory.ScalarPayload.pointer value, scalarSize := Miri.Memory.Scalar.targetPointerSize✝ layout }

def Miri.Memory.Scalar.fromMaybePointer {Prov : Type} (layout : ABI.TargetDataLayout) (value : Pointer (Option Prov)) : Except ScalarError (Scalar Prov)

Equations

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

def Miri.Memory.Scalar.nullPointer {Prov : Type} (layout : ABI.TargetDataLayout) : Except ScalarError (Scalar Prov)

Equations

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

def Miri.Memory.Scalar.fromBool {Prov : Type} (value : Bool) : Scalar Prov

Equations

• Miri.Memory.Scalar.fromBool value = Miri.Memory.Scalar.fromScalarInt (Miri.Memory.ScalarInt.ofBool value)

def Miri.Memory.Scalar.fromChar {Prov : Type} (value : Char) : Scalar Prov

Equations

• Miri.Memory.Scalar.fromChar value = Miri.Memory.Scalar.fromScalarInt (Miri.Memory.ScalarInt.ofChar value)

def Miri.Memory.Scalar.fromUInt {Prov : Type} (value : ABI.U128) (size : ABI.Size) : Except ScalarError (Scalar Prov)

Equations

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

def Miri.Memory.Scalar.fromInt {Prov : Type} (value : Int) (size : ABI.Size) : Except ScalarError (Scalar Prov)

Equations

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

def Miri.Memory.Scalar.isPointer {Prov : Type} (self : Scalar Prov) : Bool

Equations

• self.isPointer = match Miri.Memory.Scalar.payload✝ self with | Miri.Memory.ScalarPayload.integer value => false | Miri.Memory.ScalarPayload.pointer value => true

def Miri.Memory.Scalar.toBitsOrPtrInternal {Prov : Type} (self : Scalar Prov) (expectedSize : ABI.Size) : Except ScalarError (ScalarBitsOrPointer Prov)

Equations

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

def Miri.Memory.Scalar.tryToScalarInt {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError ScalarIntCastResult

Equations

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

def Miri.Memory.Scalar.clearProvenance {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError (Scalar Prov)

Equations

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

def Miri.Memory.Scalar.toScalarInt {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError ScalarInt

Equations

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

def Miri.Memory.Scalar.assertScalarInt {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError ScalarInt

Equations

• self.assertScalarInt = self.toScalarInt

def Miri.Memory.Scalar.toBits {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) (targetSize : ABI.Size) : Except ScalarError ABI.U128

Equations

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

def Miri.Memory.Scalar.toUInt {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) (size : ABI.Size) : Except ScalarError ABI.U128

Equations

• self.toUInt size = self.toBits size

def Miri.Memory.Scalar.toUInt8 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError UInt8

Equations

• self.toUInt8 = do let __do_lift ← self.toUInt (Miri.ABI.Size.ofBytes 1) pure (UInt8.ofNat (BitVec.toNat __do_lift))

def Miri.Memory.Scalar.toUInt16 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError UInt16

Equations

• self.toUInt16 = do let __do_lift ← self.toUInt (Miri.ABI.Size.ofBytes 2) pure (UInt16.ofNat (BitVec.toNat __do_lift))

def Miri.Memory.Scalar.toUInt32 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError UInt32

Equations

• self.toUInt32 = do let __do_lift ← self.toUInt (Miri.ABI.Size.ofBytes 4) pure (UInt32.ofNat (BitVec.toNat __do_lift))

def Miri.Memory.Scalar.toUInt64 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError UInt64

Equations

• self.toUInt64 = do let __do_lift ← self.toUInt (Miri.ABI.Size.ofBytes 8) pure (UInt64.ofNat (BitVec.toNat __do_lift))

def Miri.Memory.Scalar.toUInt128 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError ABI.U128

Equations

• self.toUInt128 = self.toUInt (Miri.ABI.Size.ofBytes 16)

def Miri.Memory.Scalar.toInt {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) (size : ABI.Size) : Except ScalarError Int

Equations

• self.toInt size = do let bits ← self.toBits size Except.mapError (Miri.Memory.ScalarError.scalarInt ∘ Miri.Memory.ScalarIntError.sizeError) (size.signExtend bits)

def Miri.Memory.Scalar.toInt8 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError Int8

Equations

• self.toInt8 = do let __do_lift ← self.toInt (Miri.ABI.Size.ofBytes 1) pure (Int8.ofInt __do_lift)

def Miri.Memory.Scalar.toInt16 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError Int16

Equations

• self.toInt16 = do let __do_lift ← self.toInt (Miri.ABI.Size.ofBytes 2) pure (Int16.ofInt __do_lift)

def Miri.Memory.Scalar.toInt32 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError Int32

Equations

• self.toInt32 = do let __do_lift ← self.toInt (Miri.ABI.Size.ofBytes 4) pure (Int32.ofInt __do_lift)

def Miri.Memory.Scalar.toInt64 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError Int64

Equations

• self.toInt64 = do let __do_lift ← self.toInt (Miri.ABI.Size.ofBytes 8) pure (Int64.ofInt __do_lift)

def Miri.Memory.Scalar.toInt128 {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError Int

Equations

• self.toInt128 = self.toInt (Miri.ABI.Size.ofBytes 16)

def Miri.Memory.Scalar.toTargetUsize {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) (targetSize : ABI.Size) : Except ScalarError UInt64

Equations

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

def Miri.Memory.Scalar.toTargetIsize {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) (targetSize : ABI.Size) : Except ScalarError Int64

Equations

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

def Miri.Memory.Scalar.toBool {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError Bool

Equations

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

def Miri.Memory.Scalar.toChar {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) : Except ScalarError Char

Equations

• self.toChar = do let scalarInt ← self.toScalarInt Except.mapError Miri.Memory.Scalar.wrapIntError✝ scalarInt.toChar

def Miri.Memory.Scalar.toPointer {Prov : Type} [PointerProvenance Prov] (self : Scalar Prov) (layout : ABI.TargetDataLayout) : Except ScalarError (Pointer (Option Prov))

Equations

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

theorem Miri.Memory.Scalar.fromScalarInt_size {Prov : Type} (value : ScalarInt) : (fromScalarInt value).size = value.size

theorem Miri.Memory.Scalar.fromPointer_size {Prov : Type} (layout : ABI.TargetDataLayout) (pointer : Pointer Prov) : (fromPointer layout pointer).size = Miri.Memory.Scalar.targetPointerSize✝ layout