Pinned shims/native_lib/mod.rs boundary data. Host addresses are bounded by the configured host usize, independently of the MIR target pointer width.

inductive Miri.Interpreter.Native.FfiType : Type

• i8 : FfiType
• i16 : FfiType
• i32 : FfiType
• i64 : FfiType
• u8 : FfiType
• u16 : FfiType
• u32 : FfiType
• u64 : FfiType
• f32 : FfiType
• f64 : FfiType
• pointer : FfiType
• void : FfiType
• structureType (fields : Array FfiType) : FfiType

partial def Miri.Interpreter.Native.instReprFfiType.repr : FfiType → Nat → Std.Format

@[instance_reducible]

instance Miri.Interpreter.Native.instReprFfiType : Repr FfiType

Equations

• Miri.Interpreter.Native.instReprFfiType = { reprPrec := Miri.Interpreter.Native.instReprFfiType.repr }

structure Miri.Interpreter.Native.OwnedArg : Type

• type : FfiType
• bytes : Array UInt8

def Miri.Interpreter.Native.instReprOwnedArg.repr : OwnedArg → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.instReprOwnedArg : Repr OwnedArg

Equations

• Miri.Interpreter.Native.instReprOwnedArg = { reprPrec := Miri.Interpreter.Native.instReprOwnedArg.repr }

structure Miri.Interpreter.Native.AccessRange : Type

• addr : Nat
• size : Nat

@[instance_reducible]

instance Miri.Interpreter.Native.instDecidableEqAccessRange : DecidableEq AccessRange

Equations

• Miri.Interpreter.Native.instDecidableEqAccessRange = Miri.Interpreter.Native.instDecidableEqAccessRange.decEq

def Miri.Interpreter.Native.instDecidableEqAccessRange.decEq (x✝ x✝¹ : AccessRange) : Decidable (x✝ = x✝¹)

Equations

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

def Miri.Interpreter.Native.instReprAccessRange.repr : AccessRange → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.instReprAccessRange : Repr AccessRange

Equations

• Miri.Interpreter.Native.instReprAccessRange = { reprPrec := Miri.Interpreter.Native.instReprAccessRange.repr }

inductive Miri.Interpreter.Native.AccessEvent : Type

• read (range : AccessRange) : AccessEvent
• write (range : AccessRange) (certain : Bool) : AccessEvent

def Miri.Interpreter.Native.instDecidableEqAccessEvent.decEq (x✝ x✝¹ : AccessEvent) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Native.instDecidableEqAccessEvent.decEq (Miri.Interpreter.Native.AccessEvent.read range) (Miri.Interpreter.Native.AccessEvent.write range_1 certain) = isFalse ⋯
• Miri.Interpreter.Native.instDecidableEqAccessEvent.decEq (Miri.Interpreter.Native.AccessEvent.write range certain) (Miri.Interpreter.Native.AccessEvent.read range_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.Native.instDecidableEqAccessEvent : DecidableEq AccessEvent

Equations

• Miri.Interpreter.Native.instDecidableEqAccessEvent = Miri.Interpreter.Native.instDecidableEqAccessEvent.decEq

def Miri.Interpreter.Native.instReprAccessEvent.repr : AccessEvent → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.instReprAccessEvent : Repr AccessEvent

Equations

• Miri.Interpreter.Native.instReprAccessEvent = { reprPrec := Miri.Interpreter.Native.instReprAccessEvent.repr }

def Miri.Interpreter.Native.AccessEvent.range : AccessEvent → AccessRange

Equations

• (Miri.Interpreter.Native.AccessEvent.read a).range = a
• (Miri.Interpreter.Native.AccessEvent.write a a_1).range = a

structure Miri.Interpreter.Native.StartFfiInfo : Type

• pagePtrs : Array Nat
• stackPtr : Nat

@[instance_reducible]

instance Miri.Interpreter.Native.instReprStartFfiInfo : Repr StartFfiInfo

Equations

• Miri.Interpreter.Native.instReprStartFfiInfo = { reprPrec := Miri.Interpreter.Native.instReprStartFfiInfo.repr }

def Miri.Interpreter.Native.instReprStartFfiInfo.repr : StartFfiInfo → Nat → Std.Format

Equations

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

inductive Miri.Interpreter.Native.TraceRequest : Type

• startFfi (info : StartFfiInfo) : TraceRequest
• overrideRetcode (code : Int32) : TraceRequest

def Miri.Interpreter.Native.instReprTraceRequest.repr : TraceRequest → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.instReprTraceRequest : Repr TraceRequest

Equations

• Miri.Interpreter.Native.instReprTraceRequest = { reprPrec := Miri.Interpreter.Native.instReprTraceRequest.repr }

inductive Miri.Interpreter.Native.TypeShape : Type

• adt (isEnum isStruct reprC : Bool) (fields : Array MIR.TyId) : TypeShape
• emptyTuple : TypeShape
• other : TypeShape

def Miri.Interpreter.Native.instReprTypeShape.repr : TypeShape → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Interpreter.Native.instReprTypeShape : Repr TypeShape

Equations

• Miri.Interpreter.Native.instReprTypeShape = { reprPrec := Miri.Interpreter.Native.instReprTypeShape.repr }

structure Miri.Interpreter.Native.RawAllocation (P : Type) : Type

• address : Nat
• size : Nat
• mutable : Bool
• provenances : Array P

  Provenance range enumeration must retain source order.

@[instance_reducible]

instance Miri.Interpreter.Native.instReprRawAllocation {P✝ : Type} [Repr P✝] : Repr (RawAllocation P✝)

Equations

• Miri.Interpreter.Native.instReprRawAllocation = { reprPrec := Miri.Interpreter.Native.instReprRawAllocation.repr }

def Miri.Interpreter.Native.instReprRawAllocation.repr {P✝ : Type} [Repr P✝] : RawAllocation P✝ → Nat → Std.Format

Equations

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

structure Miri.Interpreter.Native.Library : Type

• path : String

@[instance_reducible]

instance Miri.Interpreter.Native.instReprLibrary : Repr Library

Equations

• Miri.Interpreter.Native.instReprLibrary = { reprPrec := Miri.Interpreter.Native.instReprLibrary.repr }

def Miri.Interpreter.Native.instReprLibrary.repr : Library → Nat → Std.Format

Equations

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

structure Miri.Interpreter.Native.SymbolInfo (Code : Type) : Type

• code : Code
• definingPath : String

  dladdr success and UTF8 conversion are required backend checks.

@[instance_reducible]

instance Miri.Interpreter.Native.instReprSymbolInfo {Code✝ : Type} [Repr Code✝] : Repr (SymbolInfo Code✝)

Equations

• Miri.Interpreter.Native.instReprSymbolInfo = { reprPrec := Miri.Interpreter.Native.instReprSymbolInfo.repr }

def Miri.Interpreter.Native.instReprSymbolInfo.repr {Code✝ : Type} [Repr Code✝] : SymbolInfo Code✝ → Nat → Std.Format

Equations

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