structure Miri.Memory.NativeBufferOwnership : Type

Owned source MiriAllocBytes backing. Pointer zero is excluded by the native lifecycle constructor; mode selects the allocator used at destruction. This is storage identity, not a Rust provenance or an AllocId.

• pointer : Nat
• isolated : Bool
• layoutSize : Nat
• layoutAlign : Nat

def Miri.Memory.instDecidableEqNativeBufferOwnership.decEq (x✝ x✝¹ : NativeBufferOwnership) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqNativeBufferOwnership : DecidableEq NativeBufferOwnership

Equations

• Miri.Memory.instDecidableEqNativeBufferOwnership = Miri.Memory.instDecidableEqNativeBufferOwnership.decEq

def Miri.Memory.instReprNativeBufferOwnership.repr : NativeBufferOwnership → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprNativeBufferOwnership : Repr NativeBufferOwnership

Equations

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

structure Miri.Memory.PreparedGlobalBytes : Type

Source native prepared_alloc_bytes entry, allocated once when a global address is first assigned, then transferred into its materialized Allocation.

• owner : NativeBufferOwnership
• size : ABI.Size
• align : ABI.Align

def Miri.Memory.instReprPreparedGlobalBytes.repr : PreparedGlobalBytes → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprPreparedGlobalBytes : Repr PreparedGlobalBytes

Equations

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