Miri.Input.Model.Types

Miri.Input.instDecidableEqObligation.decEq { path := a, message := a_1 } { path := b, message := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

source

structure Miri.Input.SourcePosition :

Type

Exact source coordinate payload emitted by the pinned rustc span exporter. file and context retain the compiler's diagnostic spellings; no consumer should parse them to recover instruction semantics.

line : Nat
column : Nat

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourcePosition :

Repr SourcePosition

Equations

Miri.Input.instReprSourcePosition = { reprPrec := Miri.Input.instReprSourcePosition.repr }

source

def Miri.Input.instReprSourcePosition.repr :

SourcePosition → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqSourcePosition.decEq (x✝ x✝¹ : SourcePosition) :

Decidable (x✝ = x✝¹)

Equations

Miri.Input.instDecidableEqSourcePosition.decEq { line := a, column := a_1 } { line := b, column := 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.Input.instDecidableEqSourcePosition :

DecidableEq SourcePosition

Equations

Miri.Input.instDecidableEqSourcePosition = Miri.Input.instDecidableEqSourcePosition.decEq

source

structure Miri.Input.SourceSpanData :

Type

originalPayload : String
lo : Nat
hi : Nat
start : SourcePosition
end : SourcePosition
context : String
file : String

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceSpanData :

Repr SourceSpanData

Equations

Miri.Input.instReprSourceSpanData = { reprPrec := Miri.Input.instReprSourceSpanData.repr }

source

def Miri.Input.instReprSourceSpanData.repr :

SourceSpanData → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqSourceSpanData.decEq (x✝ x✝¹ : SourceSpanData) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceSpanData :

DecidableEq SourceSpanData

Equations

Miri.Input.instDecidableEqSourceSpanData = Miri.Input.instDecidableEqSourceSpanData.decEq

source

structure Miri.Input.SourceInfo :

Type

span : SourceSpanData
scope : Nat

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceInfo :

Repr SourceInfo

Equations

Miri.Input.instReprSourceInfo = { reprPrec := Miri.Input.instReprSourceInfo.repr }

source

def Miri.Input.instReprSourceInfo.repr :

SourceInfo → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceInfo :

DecidableEq SourceInfo

Equations

Miri.Input.instDecidableEqSourceInfo = Miri.Input.instDecidableEqSourceInfo.decEq

source

def Miri.Input.instDecidableEqSourceInfo.decEq (x✝ x✝¹ : SourceInfo) :

Decidable (x✝ = x✝¹)

Equations

Miri.Input.instDecidableEqSourceInfo.decEq { span := a, scope := a_1 } { span := b, scope := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

source

structure Miri.Input.Producer :

Type

miriCommit : String
rustcCommit : String
rustcVersion : String
targetTriple : String

Instances For

source

def Miri.Input.instReprProducer.repr :

Producer → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprProducer :

Repr Producer

Equations

Miri.Input.instReprProducer = { reprPrec := Miri.Input.instReprProducer.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqProducer :

DecidableEq Producer

Equations

Miri.Input.instDecidableEqProducer = Miri.Input.instDecidableEqProducer.decEq

source

def Miri.Input.instDecidableEqProducer.decEq (x✝ x✝¹ : Producer) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

structure Miri.Input.TaggedNode :

Type

status : PayloadStatus
tag : String
payload : Lean.Json

Instances For

source

def Miri.Input.instBEqTaggedNode.beq :

TaggedNode → TaggedNode → Bool

Equations

Miri.Input.instBEqTaggedNode.beq { status := a, tag := a_1, payload := a_2 } { status := b, tag := b_1, payload := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
Miri.Input.instBEqTaggedNode.beq x✝¹ x✝ = false

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqTaggedNode :

BEq TaggedNode

Equations

Miri.Input.instBEqTaggedNode = { beq := Miri.Input.instBEqTaggedNode.beq }

source

structure Miri.Input.FieldShape :

Type

kind : FieldShapeKind
fieldCount : Nat
offsetBytes : Option Nat
strideBytes : Option Nat
offsetsBytes : Array Nat
memoryOrder : Array Nat
payload : Lean.Json

Instances For

source

structure Miri.Input.PrimitiveLayout :

Type

kind : PrimitiveKind
sizeBytes : Nat
integerKind : Option IntegerTypeTag
signed : Option Bool
floatKind : Option FloatTypeTag
addressSpace : Option Nat
payload : Lean.Json

Instances For

source

structure Miri.Input.ScalarLayout :

Type

kind : ScalarShapeKind
primitive : PrimitiveLayout
validRange : Option (Nat × Nat)
payload : Lean.Json

Instances For

source

structure Miri.Input.BackendRepr :

Type

kind : BackendReprKind
sized : Option Bool
scalar : Option ScalarLayout
first : Option ScalarLayout
second : Option ScalarLayout
secondOffsetBytes : Option Nat
element : Option ScalarLayout
laneCount : Option Nat
vectorCount : Option Nat
payload : Lean.Json

Instances For

source

structure Miri.Input.LayoutVariant :

Type

variantIndex : Nat
sizeBytes : Nat
backendRepr : BackendRepr
fieldOffsetsBytes : Array Nat
uninhabited : Bool
payload : Lean.Json

Instances For

source

inductive Miri.Input.TagEncodingKind :

Type

direct : TagEncodingKind
niche : TagEncodingKind
unknown (value : String) : TagEncodingKind

Instances For

source

def Miri.Input.instReprTagEncodingKind.repr :

TagEncodingKind → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprTagEncodingKind :

Repr TagEncodingKind

Equations

Miri.Input.instReprTagEncodingKind = { reprPrec := Miri.Input.instReprTagEncodingKind.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqTagEncodingKind :

DecidableEq TagEncodingKind

Equations

Miri.Input.instDecidableEqTagEncodingKind = Miri.Input.instDecidableEqTagEncodingKind.decEq

source

def Miri.Input.instDecidableEqTagEncodingKind.decEq (x✝ x✝¹ : TagEncodingKind) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

structure Miri.Input.TagEncoding :

Type

status : PayloadStatus
kind : TagEncodingKind
untaggedVariant : Option Nat
nicheVariants : Option (Nat × Nat)
nicheStart : Option Nat
payload : Lean.Json

Instances For

source

structure Miri.Input.VariantsLayout :

Type

kind : LayoutVariantsKind
variantIndex : Option Nat
tag : Option ScalarLayout
tagEncoding : Option TagEncoding
tagFieldIndex : Option Nat
variants : Array LayoutVariant
payload : Lean.Json

Instances For

source

structure Miri.Input.Layout :

Type

status : PayloadStatus
kind : LayoutKind
sizeBytes : Option Nat
abiAlignBytes : Option Nat
unadjustedAbiAlignBytes : Option Nat
fieldOffsetsBytes : Array Nat
fields : Option FieldShape
variantsLayout : Option VariantsLayout
backendRepresentation : Option BackendRepr
variantsKind : Option LayoutVariantsKind
backendReprKind : Option BackendReprKind
variants : Option TaggedNode
backendRepr : Option TaggedNode
payload : Lean.Json

Instances For

source

structure Miri.Input.ExternAbi :

Type

kind : TaggedNode
unwind : Option Bool
sourceSpelling : Option String
payload : Lean.Json

Instances For

source

inductive Miri.Input.ArmCallKind :

Type

aapcs : ArmCallKind
cmseNonSecureCall : ArmCallKind
cmseNonSecureEntry : ArmCallKind
unknown (value : String) : ArmCallKind

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprArmCallKind :

Repr ArmCallKind

Equations

Miri.Input.instReprArmCallKind = { reprPrec := Miri.Input.instReprArmCallKind.repr }

source

def Miri.Input.instReprArmCallKind.repr :

ArmCallKind → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqArmCallKind.decEq (x✝ x✝¹ : ArmCallKind) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqArmCallKind :

DecidableEq ArmCallKind

Equations

Miri.Input.instDecidableEqArmCallKind = Miri.Input.instDecidableEqArmCallKind.decEq

source

inductive Miri.Input.InterruptCallKind :

Type

avr : InterruptCallKind
avrNonBlocking : InterruptCallKind
msp430 : InterruptCallKind
riscvMachine : InterruptCallKind
riscvSupervisor : InterruptCallKind
x86 : InterruptCallKind
unknown (value : String) : InterruptCallKind

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprInterruptCallKind :

Repr InterruptCallKind

Equations

Miri.Input.instReprInterruptCallKind = { reprPrec := Miri.Input.instReprInterruptCallKind.repr }

source

def Miri.Input.instReprInterruptCallKind.repr :

InterruptCallKind → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqInterruptCallKind :

DecidableEq InterruptCallKind

Equations

Miri.Input.instDecidableEqInterruptCallKind = Miri.Input.instDecidableEqInterruptCallKind.decEq

source

def Miri.Input.instDecidableEqInterruptCallKind.decEq (x✝ x✝¹ : InterruptCallKind) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

inductive Miri.Input.X86CallKind :

Type

fastcall : X86CallKind
stdcall : X86CallKind
sysv64 : X86CallKind
thiscall : X86CallKind
vectorcall : X86CallKind
win64 : X86CallKind
unknown (value : String) : X86CallKind

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprX86CallKind :

Repr X86CallKind

Equations

Miri.Input.instReprX86CallKind = { reprPrec := Miri.Input.instReprX86CallKind.repr }

source

def Miri.Input.instReprX86CallKind.repr :

X86CallKind → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqX86CallKind.decEq (x✝ x✝¹ : X86CallKind) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqX86CallKind :

DecidableEq X86CallKind

Equations

Miri.Input.instDecidableEqX86CallKind = Miri.Input.instDecidableEqX86CallKind.decEq

source

inductive Miri.Input.CanonicalAbiKind :

Type

c : CanonicalAbiKind
rust : CanonicalAbiKind
rustCold : CanonicalAbiKind
rustPreserveNone : CanonicalAbiKind
rustTail : CanonicalAbiKind
custom : CanonicalAbiKind
swift : CanonicalAbiKind
arm : CanonicalAbiKind
gpuKernel : CanonicalAbiKind
interrupt : CanonicalAbiKind
x86 : CanonicalAbiKind
unknown (value : String) : CanonicalAbiKind

Instances For

source

def Miri.Input.instReprCanonicalAbiKind.repr :

CanonicalAbiKind → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprCanonicalAbiKind :

Repr CanonicalAbiKind

Equations

Miri.Input.instReprCanonicalAbiKind = { reprPrec := Miri.Input.instReprCanonicalAbiKind.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqCanonicalAbiKind :

DecidableEq CanonicalAbiKind

Equations

Miri.Input.instDecidableEqCanonicalAbiKind = Miri.Input.instDecidableEqCanonicalAbiKind.decEq

source

def Miri.Input.instDecidableEqCanonicalAbiKind.decEq (x✝ x✝¹ : CanonicalAbiKind) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

structure Miri.Input.CanonicalAbi :

Type

status : PayloadStatus
kind : CanonicalAbiKind
armCall : Option ArmCallKind
interruptKind : Option InterruptCallKind
x86Call : Option X86CallKind
payload : Lean.Json

Instances For

source

inductive Miri.Input.TypedEnumTag :

Type

safety : TypedEnumTag
borrowKind : TypedEnumTag
fakeBorrowKind : TypedEnumTag
mutBorrowKind : TypedEnumTag
mutability : TypedEnumTag
castKind : TypedEnumTag
pointerCoercion : TypedEnumTag
coercionSource : TypedEnumTag
unwindReason : TypedEnumTag
aggregateKind : TypedEnumTag
unwindAction : TypedEnumTag
mirPhase : TypedEnumTag
mirPhaseStage : TypedEnumTag
withRetag : TypedEnumTag
runtimeCheck : TypedEnumTag
fakeReadCause : TypedEnumTag
callSource : TypedEnumTag
backwardDropReason : TypedEnumTag
regionKind : TypedEnumTag
boundRegionKind : TypedEnumTag
boundVarIndexKind : TypedEnumTag
lateParamRegionKind : TypedEnumTag
integerType : TypedEnumTag
floatType : TypedEnumTag
adtKind : TypedEnumTag
variance : TypedEnumTag
coverageKind : TypedEnumTag
coveragePointKind : TypedEnumTag
fakeBorrowRetagMode : TypedEnumTag
other (value : String) : TypedEnumTag

Instances For

source

def Miri.Input.instReprTypedEnumTag.repr :

TypedEnumTag → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprTypedEnumTag :

Repr TypedEnumTag

Equations

Miri.Input.instReprTypedEnumTag = { reprPrec := Miri.Input.instReprTypedEnumTag.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqTypedEnumTag :

DecidableEq TypedEnumTag

Equations

Miri.Input.instDecidableEqTypedEnumTag = Miri.Input.instDecidableEqTypedEnumTag.decEq

source

def Miri.Input.instDecidableEqTypedEnumTag.decEq (x✝ x✝¹ : TypedEnumTag) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instHashableTypedEnumTag :

Hashable TypedEnumTag

Equations

Miri.Input.instHashableTypedEnumTag = { hash := Miri.Input.instHashableTypedEnumTag.hash }

source

def Miri.Input.instHashableTypedEnumTag.hash :

TypedEnumTag → UInt64

Equations

Instances For

source

inductive Miri.Input.UserTypeProjectionKind :

Type

deref : UserTypeProjectionKind
field (index : Nat) : UserTypeProjectionKind
index : UserTypeProjectionKind
constantIndex (offset minLength : Nat) (fromEnd : Bool) : UserTypeProjectionKind
subslice (startIndex endIndex : Nat) (fromEnd : Bool) : UserTypeProjectionKind
downcast (name : Option String) (variantIndex : Nat) : UserTypeProjectionKind
opaqueCast : UserTypeProjectionKind
unwrapUnsafeBinder : UserTypeProjectionKind
phantomDeref : UserTypeProjectionKind
unknown (tag : String) : UserTypeProjectionKind

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprUserTypeProjectionKind :

Repr UserTypeProjectionKind

Equations

Miri.Input.instReprUserTypeProjectionKind = { reprPrec := Miri.Input.instReprUserTypeProjectionKind.repr }

source

def Miri.Input.instReprUserTypeProjectionKind.repr :

UserTypeProjectionKind → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqUserTypeProjectionKind.decEq (x✝ x✝¹ : UserTypeProjectionKind) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqUserTypeProjectionKind :

DecidableEq UserTypeProjectionKind

Equations

Miri.Input.instDecidableEqUserTypeProjectionKind = Miri.Input.instDecidableEqUserTypeProjectionKind.decEq

source

structure Miri.Input.UserTypeProjection :

Type

status : PayloadStatus
baseIndex : Option Nat
projections : Option (Array UserTypeProjectionKind)
payload : Lean.Json

Instances For

source

def Miri.Input.instBEqUserTypeProjection.beq :

UserTypeProjection → UserTypeProjection → Bool

Equations

One or more equations did not get rendered due to their size.
Miri.Input.instBEqUserTypeProjection.beq x✝¹ x✝ = false

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqUserTypeProjection :

BEq UserTypeProjection

Equations

Miri.Input.instBEqUserTypeProjection = { beq := Miri.Input.instBEqUserTypeProjection.beq }

source

structure Miri.Input.FunctionSignature :

Type

inputs : Array TypeId
output : TypeId
safety : TaggedNode
abi : ExternAbi
cVariadic : Bool

Instances For

source

inductive Miri.Input.CompilerPattern :

Type

Source compiler pattern AST; range endpoints retain original const payloads until lowered through the shared TypeConst interner.

range (start finish : Lean.Json) : CompilerPattern
or (patterns : Array CompilerPattern) : CompilerPattern
notNull : CompilerPattern

Instances For

source

structure Miri.Input.CompilerBooleanEvidence :

Type

Exact rustc query evidence; unsupported is never interpreted as false.

status : PayloadStatus
value : Option Bool
reason : Option String
payload : Lean.Json

Instances For

source

structure Miri.Input.CompilerTypeEvidence :

Type

status : PayloadStatus
value : Option TypeId
Supported null is an actual None result (e.g. builtin_deref).
reason : Option String
payload : Lean.Json

Instances For

source

structure Miri.Input.TypeCompilerFacts :

Type

typingEnvironment : String
inputTypeId : TypeId
booleanQueries : Array (String × CompilerBooleanEvidence)
typeQueries : Array (String × CompilerTypeEvidence)
adtPayload : Option Lean.Json
captureNames : Option (Array (Option String))
captureNamesStatus : Option PayloadStatus
payload : Lean.Json

Instances For

source

structure Miri.Input.TypeNode :

Type

pattern : Option CompilerPattern
compilerFacts : Option TypeCompilerFacts
id : TypeId
display : String
shapeStatus : PayloadStatus
shapeKind : TypeShapeKind
shapeMetadata : TypeShapeMetadata
signature : Option FunctionSignature
layout : Layout
payload : Lean.Json

Instances For

source

structure Miri.Input.InitRange :

Type

initialized : Bool
startBytes : Nat
endBytesExclusive : Nat

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprInitRange :

Repr InitRange

Equations

Miri.Input.instReprInitRange = { reprPrec := Miri.Input.instReprInitRange.repr }

source

def Miri.Input.instReprInitRange.repr :

InitRange → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqInitRange.decEq (x✝ x✝¹ : InitRange) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqInitRange :

DecidableEq InitRange

Equations

Miri.Input.instDecidableEqInitRange = Miri.Input.instDecidableEqInitRange.decEq

source

structure Miri.Input.Relocation :

Type

storageOffsetBytes : Nat
target : AllocationId
targetOffsetEncodedBytes : String
immutable : Bool
sharedRef : Bool
ctfeProvenance : Memory.CtfeProvenance

Instances For

source

def Miri.Input.instReprRelocation.repr :

Relocation → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprRelocation :

Repr Relocation

Equations

Miri.Input.instReprRelocation = { reprPrec := Miri.Input.instReprRelocation.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqRelocation :

DecidableEq Relocation

Equations

Miri.Input.instDecidableEqRelocation = Miri.Input.instDecidableEqRelocation.decEq

source

def Miri.Input.instDecidableEqRelocation.decEq (x✝ x✝¹ : Relocation) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

inductive Miri.Input.MemoryMutability :

Type

mutable : MemoryMutability
immutable : MemoryMutability
unknown (value : String) : MemoryMutability

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprMemoryMutability :

Repr MemoryMutability

Equations

Miri.Input.instReprMemoryMutability = { reprPrec := Miri.Input.instReprMemoryMutability.repr }

source

def Miri.Input.instReprMemoryMutability.repr :

MemoryMutability → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqMemoryMutability.decEq (x✝ x✝¹ : MemoryMutability) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqMemoryMutability :

DecidableEq MemoryMutability

Equations

Miri.Input.instDecidableEqMemoryMutability = Miri.Input.instDecidableEqMemoryMutability.decEq

source

structure Miri.Input.AllocationMemory :

Type

sizeBytes : Nat
alignBytes : Nat
mutability : MemoryMutability
bytesHex : String
initializationRanges : Array InitRange
relocations : Array Relocation

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprAllocationMemory :

Repr AllocationMemory

Equations

Miri.Input.instReprAllocationMemory = { reprPrec := Miri.Input.instReprAllocationMemory.repr }

source

def Miri.Input.instReprAllocationMemory.repr :

AllocationMemory → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqAllocationMemory.decEq (x✝ x✝¹ : AllocationMemory) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqAllocationMemory :

DecidableEq AllocationMemory

Equations

Miri.Input.instDecidableEqAllocationMemory = Miri.Input.instDecidableEqAllocationMemory.decEq

source

structure Miri.Input.AbiAttributes :

Type

noAlias : Bool
noFree : Bool
noUndef : Bool
nonNull : Bool
readOnly : Bool
writable : Bool
inRegister : Bool
regularBits : Nat
pointeeSizeBytes : Nat
pointeeAlignBytes : Option Nat
argExtension : TaggedNode
captures : TaggedNode

Instances For

source

inductive Miri.Input.AbiRegisterKind :

Type

integer : AbiRegisterKind
float : AbiRegisterKind
ppcF128 : AbiRegisterKind
vector : AbiRegisterKind
unknown (value : String) : AbiRegisterKind

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprAbiRegisterKind :

Repr AbiRegisterKind

Equations

Miri.Input.instReprAbiRegisterKind = { reprPrec := Miri.Input.instReprAbiRegisterKind.repr }

source

def Miri.Input.instReprAbiRegisterKind.repr :

AbiRegisterKind → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqAbiRegisterKind.decEq (x✝ x✝¹ : AbiRegisterKind) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqAbiRegisterKind :

DecidableEq AbiRegisterKind

Equations

Miri.Input.instDecidableEqAbiRegisterKind = Miri.Input.instDecidableEqAbiRegisterKind.decEq

source

structure Miri.Input.AbiRegister :

Type

kind : AbiRegisterKind
sizeBits : Nat
hintElement : Option TaggedNode
payload : Lean.Json

Instances For

source

structure Miri.Input.AbiCastTarget :

Type

prefixRegisters : Array AbiRegister
restOffsetBytes : Option Nat
restRegister : AbiRegister
restTotalBytes : Nat
restIsConsecutive : Bool
attributes : AbiAttributes
payload : Lean.Json

Instances For

source

structure Miri.Input.AbiPassMode :

Type

kind : PassModeKind
attributes : Array AbiAttributes
castTarget : Option AbiCastTarget
padI32Count : Option Nat
addressSpace : Option Nat
indirectMode : Option TaggedNode
payload : Lean.Json

Instances For

source

structure Miri.Input.AbiArgument :

Type

typeId : TypeId
layout : Option Layout
Physical compiler TyAndLayout for this FnAbi argument. The logical type remains typeId; Rust can adjust the ABI layout independently (notably the forced-thin virtual-call receiver). Legacy exports leave this unavailable.
mode : AbiPassMode
payload : Lean.Json

Instances For

source

structure Miri.Input.FunctionAbi :

Type

arguments : Array AbiArgument
returnValue : AbiArgument
callingConvention : CanonicalAbi
canUnwind : Bool
cVariadic : Bool
fixedCount : Nat
payload : Lean.Json

Instances For

source

inductive Miri.Input.TypedValue :

Type

scalar (value : Lean.Json) : TypedValue
diagnostic (value : Lean.Json) : TypedValue
array (values : Array TypedValue) : TypedValue
object (fields : Array (String × TypedValue)) : TypedValue
typeRef (id : TypeId) : TypedValue
allocationRef (id : AllocationId) : TypedValue
instanceRef (id : InstanceId) : TypedValue
localRef (id : LocalId) : TypedValue
blockRef (id : BlockId) : TypedValue
sourceSpan (value : SourceSpanData) : TypedValue
sourceInfo (value : SourceInfo) : TypedValue
statement (variant : StatementVariant) (status : PayloadStatus) (fields : Array (String × TypedValue)) : TypedValue
terminator (variant : TerminatorVariant) (status : PayloadStatus) (fields : Array (String × TypedValue)) : TypedValue
rvalue (variant : RvalueVariant) (status : PayloadStatus) (fields : Array (String × TypedValue)) : TypedValue
binOperator (operator : MIR.BinOp) (status : PayloadStatus) : TypedValue
unknownBinOperator (tag : String) (status : PayloadStatus) : TypedValue
unOperator (operator : MIR.UnOp) (status : PayloadStatus) : TypedValue
unknownUnOperator (tag : String) (status : PayloadStatus) : TypedValue
enumTag (category : TypedEnumTag) (tag : TaggedNode) (children : Array (String × TypedValue)) : TypedValue
userTypeProjection (value : UserTypeProjection) : TypedValue
operand (variant : OperandVariant) (status : PayloadStatus) (fields : Array (String × TypedValue)) : TypedValue
projection (variant : ProjectionVariant) (fields : Array (String × TypedValue)) : TypedValue

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqTypedValue :

BEq TypedValue

Equations

Miri.Input.instBEqTypedValue = { beq := Miri.Input.instBEqTypedValue.beq }

source

partial def Miri.Input.instBEqTypedValue.beq :

TypedValue → TypedValue → Bool

source

structure Miri.Input.DefinitionId :

Type

crateIndex : Nat
index : Nat

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprDefinitionId :

Repr DefinitionId

Equations

Miri.Input.instReprDefinitionId = { reprPrec := Miri.Input.instReprDefinitionId.repr }

source

def Miri.Input.instReprDefinitionId.repr :

DefinitionId → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqDefinitionId :

DecidableEq DefinitionId

Equations

Miri.Input.instDecidableEqDefinitionId = Miri.Input.instDecidableEqDefinitionId.decEq

source

def Miri.Input.instDecidableEqDefinitionId.decEq (x✝ x✝¹ : DefinitionId) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

inductive Miri.Input.VtableEntryKind :

Type

dropInPlaceNull : VtableEntryKind
dropInPlace : VtableEntryKind
sizeBytes : VtableEntryKind
alignBytes : VtableEntryKind
vacant : VtableEntryKind
method : VtableEntryKind
supertraitVtablePointer : VtableEntryKind
unknown (value : String) : VtableEntryKind

Instances For

source

def Miri.Input.instReprVtableEntryKind.repr :

VtableEntryKind → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprVtableEntryKind :

Repr VtableEntryKind

Equations

Miri.Input.instReprVtableEntryKind = { reprPrec := Miri.Input.instReprVtableEntryKind.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqVtableEntryKind :

DecidableEq VtableEntryKind

Equations

Miri.Input.instDecidableEqVtableEntryKind = Miri.Input.instDecidableEqVtableEntryKind.decEq

source

def Miri.Input.instDecidableEqVtableEntryKind.decEq (x✝ x✝¹ : VtableEntryKind) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

inductive Miri.Input.VtablePredicateKind :

Type

trait : VtablePredicateKind
autoTrait : VtablePredicateKind
projection : VtablePredicateKind
unknown (value : String) : VtablePredicateKind

Instances For

source

def Miri.Input.instReprVtablePredicateKind.repr :

VtablePredicateKind → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprVtablePredicateKind :

Repr VtablePredicateKind

Equations

Miri.Input.instReprVtablePredicateKind = { reprPrec := Miri.Input.instReprVtablePredicateKind.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqVtablePredicateKind :

DecidableEq VtablePredicateKind

Equations

Miri.Input.instDecidableEqVtablePredicateKind = Miri.Input.instDecidableEqVtablePredicateKind.decEq

source

def Miri.Input.instDecidableEqVtablePredicateKind.decEq (x✝ x✝¹ : VtablePredicateKind) :

Decidable (x✝ = x✝¹)

Equations

Instances For

source

structure Miri.Input.FunctionAllocation :

Type

instanceId : InstanceId
definitionId : DefinitionId
definitionPath : String
genericArgs : TypedValue
payload : Lean.Json

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqFunctionAllocation :

BEq FunctionAllocation

Equations

Miri.Input.instBEqFunctionAllocation = { beq := Miri.Input.instBEqFunctionAllocation.beq }

source

def Miri.Input.instBEqFunctionAllocation.beq :

FunctionAllocation → FunctionAllocation → Bool

Equations

One or more equations did not get rendered due to their size.
Miri.Input.instBEqFunctionAllocation.beq x✝¹ x✝ = false

Instances For

source

structure Miri.Input.StaticGlobalInfo :

Type

Exact compiler GlobalAlloc::Static metadata queries, independent of initializer evaluation and runtime allocation adjustment.

status : PayloadStatus
sizeBytes : Nat
alignBytes : Nat
mutability : MemoryMutability
isStatic : Bool
foreignItem : Bool
threadLocal : Bool
payload : Lean.Json

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqStaticGlobalInfo :

BEq StaticGlobalInfo

Equations

Miri.Input.instBEqStaticGlobalInfo = { beq := Miri.Input.instBEqStaticGlobalInfo.beq }

source

def Miri.Input.instBEqStaticGlobalInfo.beq :

StaticGlobalInfo → StaticGlobalInfo → Bool

Equations

One or more equations did not get rendered due to their size.
Miri.Input.instBEqStaticGlobalInfo.beq x✝¹ x✝ = false

Instances For

source

structure Miri.Input.StaticAllocation :

Type

globalInfo : Option StaticGlobalInfo
definitionId : DefinitionId
definitionPath : String
threadLocal : Bool
initializer : Option AllocationMemory
payload : Lean.Json

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqStaticAllocation :

BEq StaticAllocation

Equations

Miri.Input.instBEqStaticAllocation = { beq := Miri.Input.instBEqStaticAllocation.beq }

source

def Miri.Input.instBEqStaticAllocation.beq :

StaticAllocation → StaticAllocation → Bool

Equations

One or more equations did not get rendered due to their size.
Miri.Input.instBEqStaticAllocation.beq x✝¹ x✝ = false

Instances For

source

structure Miri.Input.VtablePredicate :

Type

kind : VtablePredicateKind
status : PayloadStatus
definitionId : Option DefinitionId
definitionPath : Option String
genericArgs : Option TypedValue
payload : Lean.Json

Instances For

source

def Miri.Input.instBEqVtablePredicate.beq :

VtablePredicate → VtablePredicate → Bool

Equations

One or more equations did not get rendered due to their size.
Miri.Input.instBEqVtablePredicate.beq x✝¹ x✝ = false

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqVtablePredicate :

BEq VtablePredicate

Equations

Miri.Input.instBEqVtablePredicate = { beq := Miri.Input.instBEqVtablePredicate.beq }

source

structure Miri.Input.VtableEntry :

Type

kind : VtableEntryKind
status : PayloadStatus
instanceId : Option InstanceId
definitionId : Option DefinitionId
definitionPath : Option String
allocationId : Option AllocationId
traitDefinitionId : Option DefinitionId
traitDefinitionPath : Option String
genericArgs : Option TypedValue
payload : Lean.Json

Instances For

source

def Miri.Input.instBEqVtableEntry.beq :

VtableEntry → VtableEntry → Bool

Equations

One or more equations did not get rendered due to their size.
Miri.Input.instBEqVtableEntry.beq x✝¹ x✝ = false

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqVtableEntry :

BEq VtableEntry

Equations

Miri.Input.instBEqVtableEntry = { beq := Miri.Input.instBEqVtableEntry.beq }

source

structure Miri.Input.VtableAllocation :

Type

typeId : TypeId
sizeBytes : Option Nat
alignBytes : Option Nat
layoutStatus : PayloadStatus
predicates : Array VtablePredicate
entries : Array VtableEntry
payload : Lean.Json

Instances For

source

def Miri.Input.instBEqVtableAllocation.beq :

VtableAllocation → VtableAllocation → Bool

Equations

One or more equations did not get rendered due to their size.
Miri.Input.instBEqVtableAllocation.beq x✝¹ x✝ = false

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqVtableAllocation :

BEq VtableAllocation

Equations

Miri.Input.instBEqVtableAllocation = { beq := Miri.Input.instBEqVtableAllocation.beq }

source

inductive Miri.Input.AllocationData :

Type

memory (value : AllocationMemory) : AllocationData
function (value : FunctionAllocation) : AllocationData
static (value : StaticAllocation) : AllocationData
vtable (value : VtableAllocation) : AllocationData
typeId (value : TypeId) : AllocationData

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqAllocationData :

BEq AllocationData

Equations

Miri.Input.instBEqAllocationData = { beq := Miri.Input.instBEqAllocationData.beq }

source

structure Miri.Input.AllocationNode :

Type

id : AllocationId
sourceAllocId : Option UInt64
Exact rustc AllocId.0.get() witness supplied by the pinned exporter. This is absent in legacy exports and is never inferred from id.
status : PayloadStatus
kind : AllocationKind
memory : Option AllocationMemory
data : Option AllocationData
payload : Lean.Json

Instances For

source

def Miri.Input.instBEqAllocationNode.beq :

AllocationNode → AllocationNode → Bool

Equations

One or more equations did not get rendered due to their size.
Miri.Input.instBEqAllocationNode.beq x✝¹ x✝ = false

Instances For

source

@[instance_reducible]

instance Miri.Input.instBEqAllocationNode :

BEq AllocationNode

Equations

Miri.Input.instBEqAllocationNode = { beq := Miri.Input.instBEqAllocationNode.beq }

source

inductive Miri.Input.SourceAllocIdKind :

Type

The optional prepared post-export rustc allocator snapshot. Raw rustc IDs remain separate from exporter graph IDs and from the runtime's dense IDs.

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceAllocIdKind :

Repr SourceAllocIdKind

Equations

Miri.Input.instReprSourceAllocIdKind = { reprPrec := Miri.Input.instReprSourceAllocIdKind.repr }

source

def Miri.Input.instReprSourceAllocIdKind.repr :

SourceAllocIdKind → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceAllocIdKind :

DecidableEq SourceAllocIdKind

Equations

Miri.Input.instDecidableEqSourceAllocIdKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

inductive Miri.Input.SourceAllocIdStatus :

Type

Instances For

source

def Miri.Input.instReprSourceAllocIdStatus.repr :

SourceAllocIdStatus → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceAllocIdStatus :

Repr SourceAllocIdStatus

Equations

Miri.Input.instReprSourceAllocIdStatus = { reprPrec := Miri.Input.instReprSourceAllocIdStatus.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceAllocIdStatus :

DecidableEq SourceAllocIdStatus

Equations

Miri.Input.instDecidableEqSourceAllocIdStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

structure Miri.Input.SourceAllocIdPoolRow :

Type

sourceAllocId : UInt64
kind : SourceAllocIdKind
status : SourceAllocIdStatus
allocationId : Option AllocationId
opaqueAllocationId : Option AllocationId
memoryMutability : Option MemoryMutability
memoryAlignBytes : Option Nat
memoryAllBytesInitialized : Option Bool
memoryHasProvenance : Option Bool
byteImageHex : Option String

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceAllocIdPoolRow :

Repr SourceAllocIdPoolRow

Equations

Miri.Input.instReprSourceAllocIdPoolRow = { reprPrec := Miri.Input.instReprSourceAllocIdPoolRow.repr }

source

def Miri.Input.instReprSourceAllocIdPoolRow.repr :

SourceAllocIdPoolRow → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceAllocIdPoolRow :

DecidableEq SourceAllocIdPoolRow

Equations

Miri.Input.instDecidableEqSourceAllocIdPoolRow = Miri.Input.instDecidableEqSourceAllocIdPoolRow.decEq

source

def Miri.Input.instDecidableEqSourceAllocIdPoolRow.decEq (x✝ x✝¹ : SourceAllocIdPoolRow) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

inductive Miri.Input.SourceAllocIdDedupKind :

Type

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceAllocIdDedupKind :

Repr SourceAllocIdDedupKind

Equations

Miri.Input.instReprSourceAllocIdDedupKind = { reprPrec := Miri.Input.instReprSourceAllocIdDedupKind.repr }

source

def Miri.Input.instReprSourceAllocIdDedupKind.repr :

SourceAllocIdDedupKind → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceAllocIdDedupKind :

DecidableEq SourceAllocIdDedupKind

Equations

Miri.Input.instDecidableEqSourceAllocIdDedupKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

inductive Miri.Input.SourceAllocIdProbeOutcome :

Type

preexistingHit : SourceAllocIdProbeOutcome
missReservedByProbe : SourceAllocIdProbeOutcome

Instances For

source

def Miri.Input.instReprSourceAllocIdProbeOutcome.repr :

SourceAllocIdProbeOutcome → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceAllocIdProbeOutcome :

Repr SourceAllocIdProbeOutcome

Equations

Miri.Input.instReprSourceAllocIdProbeOutcome = { reprPrec := Miri.Input.instReprSourceAllocIdProbeOutcome.repr }

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceAllocIdProbeOutcome :

DecidableEq SourceAllocIdProbeOutcome

Equations

Miri.Input.instDecidableEqSourceAllocIdProbeOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

structure Miri.Input.SourceAllocIdSaltResult :

Type

salt : Nat
allocationId : AllocationId
sourceAllocId : UInt64
outcome : SourceAllocIdProbeOutcome

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceAllocIdSaltResult :

Repr SourceAllocIdSaltResult

Equations

Miri.Input.instReprSourceAllocIdSaltResult = { reprPrec := Miri.Input.instReprSourceAllocIdSaltResult.repr }

source

def Miri.Input.instReprSourceAllocIdSaltResult.repr :

SourceAllocIdSaltResult → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqSourceAllocIdSaltResult.decEq (x✝ x✝¹ : SourceAllocIdSaltResult) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceAllocIdSaltResult :

DecidableEq SourceAllocIdSaltResult

Equations

Miri.Input.instDecidableEqSourceAllocIdSaltResult = Miri.Input.instDecidableEqSourceAllocIdSaltResult.decEq

source

structure Miri.Input.SourceAllocIdDedupRow :

Type

keyKind : SourceAllocIdDedupKind
keyAllocationId : AllocationId
byteImageHex : Option String
salts : Array SourceAllocIdSaltResult

Instances For

source

def Miri.Input.instReprSourceAllocIdDedupRow.repr :

SourceAllocIdDedupRow → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprSourceAllocIdDedupRow :

Repr SourceAllocIdDedupRow

Equations

Miri.Input.instReprSourceAllocIdDedupRow = { reprPrec := Miri.Input.instReprSourceAllocIdDedupRow.repr }

source

def Miri.Input.instDecidableEqSourceAllocIdDedupRow.decEq (x✝ x✝¹ : SourceAllocIdDedupRow) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqSourceAllocIdDedupRow :

DecidableEq SourceAllocIdDedupRow

Equations

Miri.Input.instDecidableEqSourceAllocIdDedupRow = Miri.Input.instDecidableEqSourceAllocIdDedupRow.decEq

source

structure Miri.Input.CompilerAllocIdWorld :

Type

lastReservedSourceAllocId : UInt64
nextSourceAllocId : UInt64
finalSentinelSourceAllocId : UInt64
rawPool : Array SourceAllocIdPoolRow
dedupCatalog : Array SourceAllocIdDedupRow
completeKeyFamilies : Array SourceAllocIdDedupKind
unsupportedKeyFamilies : Array SourceAllocIdDedupKind

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprCompilerAllocIdWorld :

Repr CompilerAllocIdWorld

Equations

Miri.Input.instReprCompilerAllocIdWorld = { reprPrec := Miri.Input.instReprCompilerAllocIdWorld.repr }

source

def Miri.Input.instReprCompilerAllocIdWorld.repr :

CompilerAllocIdWorld → Nat → Std.Format

Equations

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

Instances For

source

def Miri.Input.instDecidableEqCompilerAllocIdWorld.decEq (x✝ x✝¹ : CompilerAllocIdWorld) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqCompilerAllocIdWorld :

DecidableEq CompilerAllocIdWorld

Equations

Miri.Input.instDecidableEqCompilerAllocIdWorld = Miri.Input.instDecidableEqCompilerAllocIdWorld.decEq

source

structure Miri.Input.MirNode :

Type

value : TypedValue
sourceInfo : SourceInfo

Instances For

source

structure Miri.Input.BasicBlock :

Type

id : BlockId
statements : Array MirNode
terminator : MirNode
cleanup : Bool
payload : Lean.Json

Instances For

source

structure Miri.Input.LocalDecl :

Type

id : LocalId
typeId : TypeId
sourceInfo : SourceInfo
payload : Lean.Json

Instances For

source

structure Miri.Input.BodyCore :

Type

sourcePath : String
Exact location of this body in the source document. Lowering checks this path against the retained raw document before using source-scoped metadata.
defPath : String
definitionId : Option DefinitionId
phase : TypedValue
injectionPhase : Option TypedValue
argumentCount : Nat
spreadArgument : Option LocalId
locals : Array LocalDecl
blocks : Array BasicBlock
sourceScopes : Option (Array Lean.Json)
payload : Lean.Json

Instances For

source

structure Miri.Input.PromotedBody :

Type

index : Nat
status : PayloadStatus
body : Option BodyCore
payload : Lean.Json

Instances For

source

structure Miri.Input.Bodyextends Miri.Input.BodyCore :

Type

Instances For

source

structure Miri.Input.InstanceNode :

Type

id : InstanceId
status : PayloadStatus
kind : InstanceKind
defPath : Option String
definitionId : Option DefinitionId
bodyInstantiation : Option TaggedNode
bodyTemplateIsPolymorphic : Option Bool
instanceArgsAreMonomorphic : Option Bool
body : Option Body
promotedBodies : Array PromotedBody
payload : Lean.Json

Instances For

source

structure Miri.Input.ScopeRoot :

Type

defPath : String
definitionId : DefinitionId

Instances For

source

@[instance_reducible]

instance Miri.Input.instReprScopeRoot :

Repr ScopeRoot

Equations

Miri.Input.instReprScopeRoot = { reprPrec := Miri.Input.instReprScopeRoot.repr }

source

def Miri.Input.instReprScopeRoot.repr :

ScopeRoot → Nat → Std.Format

Equations

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

Instances For

source

@[instance_reducible]

instance Miri.Input.instDecidableEqScopeRoot :

DecidableEq ScopeRoot

Equations

Miri.Input.instDecidableEqScopeRoot = Miri.Input.instDecidableEqScopeRoot.decEq

source

def Miri.Input.instDecidableEqScopeRoot.decEq (x✝ x✝¹ : ScopeRoot) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

structure Miri.Input.SelectedScope :

Type

kind : String
statusText : String
status : PayloadStatus
semantics : String
roots : Array ScopeRoot
unresolvedObligations : Array String
unresolvedEvidence : Array Obligation
payload : Lean.Json

Instances For

source

structure Miri.Input.TargetDataLayoutEvidence :

Type

Compiler-query target layout evidence, retained independently of a runtime layout validator. Missing evidence is not inferred from the target triple.

status : PayloadStatus
payload : Lean.Json

Instances For

source

structure Miri.Input.CompilerPredicateEvidence :

Type

Exact compiler existential-predicate identity, stable comparison rank and late-bound-region-erasing normalization result under an explicit environment.

id : Nat
typingEnvironment : String
stableKey : Nat
autoTrait : Bool
normalizationStatus : PayloadStatus
normalizedId : Option Nat
original : Lean.Json
payload : Lean.Json

Instances For