The source-level allocation record and checked read-byte operations from the pinned rustc_middle::mir::interpret::allocation module. The byte backend is represented by Array UInt8; host allocation is an explicit callback at the fallible constructor boundary.

inductive Miri.Memory.Mutability : Type

• Not : Mutability
• Mut : Mutability

@[instance_reducible]

instance Miri.Memory.instDecidableEqMutability : DecidableEq Mutability

Equations

• Miri.Memory.instDecidableEqMutability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprMutability : Repr Mutability

Equations

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

def Miri.Memory.instReprMutability.repr : Mutability → Nat → Std.Format

Equations

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

inductive Miri.Memory.AllocInit : Type

• Uninit : AllocInit
• Zero : AllocInit

@[instance_reducible]

instance Miri.Memory.instDecidableEqAllocInit : DecidableEq AllocInit

Equations

• Miri.Memory.instDecidableEqAllocInit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Memory.instReprAllocInit.repr : AllocInit → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprAllocInit : Repr AllocInit

Equations

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

structure Miri.Memory.BadBytesAccess : Type

• access : AllocRange
• bad : AllocRange

def Miri.Memory.instDecidableEqBadBytesAccess.decEq (x✝ x✝¹ : BadBytesAccess) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqBadBytesAccess.decEq { access := a, bad := a_1 } { access := b, bad := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqBadBytesAccess : DecidableEq BadBytesAccess

Equations

• Miri.Memory.instDecidableEqBadBytesAccess = Miri.Memory.instDecidableEqBadBytesAccess.decEq

@[instance_reducible]

instance Miri.Memory.instReprBadBytesAccess : Repr BadBytesAccess

Equations

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

def Miri.Memory.instReprBadBytesAccess.repr : BadBytesAccess → Nat → Std.Format

Equations

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

inductive Miri.Memory.AllocError : Type

• readPointerAsInt (info : Option BadBytesAccess) : AllocError
• readPartialPointer (offset : ABI.Size) : AllocError
• invalidUninitBytes (info : Option BadBytesAccess) : AllocError
• memory (reason : MemoryError) : AllocError
• provenance (reason : ProvenanceMapError) : AllocError
• alignment (reason : ABI.AlignError) : AllocError
• storageLengthOverflow (length : Nat) : AllocError
• storageLengthMismatch (requested : ABI.Size) (actual : Nat) : AllocError
• storageBackendNotZeroed (index : Nat) (value : UInt8) : AllocError
• outOfBounds (range : AllocRange) (allocationSize : ABI.Size) : AllocError
• invalidSliceEndpoints (start finish available : Nat) : AllocError
• nonEmptyProvenanceWithoutEntry : AllocError
• readOnlyAllocation : AllocError
• pointerSizeMismatch (scalarSize pointerSize : ABI.Size) : AllocError
• scalar (reason : ScalarError) : AllocError
• scalarBytesTooWide (size : ABI.Size) : AllocError
• pointerBitsDoNotFitOffset (bits : ABI.U128) : AllocError
• scalarPointerNotTargetSized (scalarSize targetSize : ABI.Size) : AllocError
• copyRangesOverlap : AllocError
• repeatedCopyRequiresNonoverlapping : AllocError
• singleByteZeroCountCopy : AllocError
• allocationHasByteFragmentProvenance : AllocError
• nativeWriteRangeOutOfBounds (range : AllocRange) (allocationSize : ABI.Size) : AllocError
• hostMemoryExhausted : AllocError

def Miri.Memory.instDecidableEqAllocError.decEq (x✝ x✝¹ : AllocError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Memory.instDecidableEqAllocError : DecidableEq AllocError

Equations

• Miri.Memory.instDecidableEqAllocError = Miri.Memory.instDecidableEqAllocError.decEq

@[instance_reducible]

instance Miri.Memory.instReprAllocError : Repr AllocError

Equations

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

def Miri.Memory.instReprAllocError.repr : AllocError → Nat → Std.Format

Equations

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

inductive Miri.Memory.AllocationAdjustError (CallbackError : Type) : Type

• allocation {CallbackError : Type} (reason : AllocError) : AllocationAdjustError CallbackError
• byteConversion {CallbackError : Type} (reason : CallbackError) : AllocationAdjustError CallbackError
• pointerAdjustment {CallbackError : Type} (reason : CallbackError) : AllocationAdjustError CallbackError

@[instance_reducible]

instance Miri.Memory.instDecidableEqAllocationAdjustError {CallbackError✝ : Type} [DecidableEq CallbackError✝] : DecidableEq (AllocationAdjustError CallbackError✝)

Equations

• Miri.Memory.instDecidableEqAllocationAdjustError = Miri.Memory.instDecidableEqAllocationAdjustError.decEq

def Miri.Memory.instDecidableEqAllocationAdjustError.decEq {CallbackError✝ : Type} [DecidableEq CallbackError✝] (x✝ x✝¹ : AllocationAdjustError CallbackError✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqAllocationAdjustError.decEq (Miri.Memory.AllocationAdjustError.allocation reason) (Miri.Memory.AllocationAdjustError.byteConversion reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAllocationAdjustError.decEq (Miri.Memory.AllocationAdjustError.allocation reason) (Miri.Memory.AllocationAdjustError.pointerAdjustment reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAllocationAdjustError.decEq (Miri.Memory.AllocationAdjustError.byteConversion reason) (Miri.Memory.AllocationAdjustError.allocation reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAllocationAdjustError.decEq (Miri.Memory.AllocationAdjustError.byteConversion reason) (Miri.Memory.AllocationAdjustError.pointerAdjustment reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAllocationAdjustError.decEq (Miri.Memory.AllocationAdjustError.pointerAdjustment reason) (Miri.Memory.AllocationAdjustError.allocation reason_1) = isFalse ⋯
• Miri.Memory.instDecidableEqAllocationAdjustError.decEq (Miri.Memory.AllocationAdjustError.pointerAdjustment reason) (Miri.Memory.AllocationAdjustError.byteConversion reason_1) = isFalse ⋯

def Miri.Memory.instReprAllocationAdjustError.repr {CallbackError✝ : Type} [Repr CallbackError✝] : AllocationAdjustError CallbackError✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprAllocationAdjustError {CallbackError✝ : Type} [Repr CallbackError✝] : Repr (AllocationAdjustError CallbackError✝)

Equations

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

@[instance_reducible]

instance Miri.Memory.instToStringProvenanceMapError : ToString ProvenanceMapError

Equations

• Miri.Memory.instToStringProvenanceMapError = { toString := Miri.Memory.provenanceErrorText✝ }

@[instance_reducible]

instance Miri.Memory.instToStringAllocError : ToString AllocError

Equations

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

structure Miri.Memory.Allocation (Prov : Type := CtfeProvenance) (Extra : Type := Unit) : Type

• rawBytes : Array UInt8
• size : Miri.ABI.Size
• provenance : Miri.Memory.ProvenanceMap Prov
• initMask : Miri.Memory.InitMask
• align : ABI.Align
• mutability : Mutability
• extra : Extra
• nativeBuffer : Option NativeBufferOwnership

def Miri.Memory.Allocation.fromBytes {Prov : Type} (bytes : Array UInt8) (align : ABI.Align) (mutability : Mutability) : Except AllocError (Allocation Prov)

Equations

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

def Miri.Memory.Allocation.fromBytesByteAlignedImmutable {Prov : Type} (bytes : Array UInt8) : Except AllocError (Allocation Prov)

Equations

• Miri.Memory.Allocation.fromBytesByteAlignedImmutable bytes = Miri.Memory.Allocation.fromBytes bytes Miri.ABI.Align.ONE Miri.Memory.Mutability.Not

def Miri.Memory.Allocation.tryNew {Prov : Type} (size : ABI.Size) (align : ABI.Align) (init : AllocInit) (zeroedStorage : ABI.Size → ABI.Align → Option (Array UInt8)) : Except AllocError (Allocation Prov)

zeroedStorage is the explicit host AllocBytes::zeroed boundary. A none result preserves the source's MemoryExhausted failure. The backend's zeroed-storage contract is checked before an allocation value is returned.

Equations

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

def Miri.Memory.Allocation.withExtra {Prov Extra : Type} (allocation : Allocation Prov) (extra : Extra) : Allocation Prov Extra

Equations

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

def Miri.Memory.Allocation.mapExtra {Prov Extra Extra' : Type} (allocation : Allocation Prov Extra) (f : Extra → Extra') : Allocation Prov Extra'

Map only allocation metadata. Byte storage, size, provenance, init mask, alignment, and mutability are copied unchanged, matching the source fieldwise metadata update boundary used by tree-retagging.

Equations

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

def Miri.Memory.Allocation.setExtra {Prov Extra : Type} (allocation : Allocation Prov Extra) (extra : Extra) : Allocation Prov Extra

Replace only allocation metadata while retaining all allocation storage and semantic state.

Equations

• allocation.setExtra extra = allocation.mapExtra fun (x : Extra) => extra

def Miri.Memory.Allocation.attachNativeBuffer {Prov Extra : Type} (allocation : Allocation Prov Extra) (owner : NativeBufferOwnership) : Except String (Allocation Prov Extra)

Attach once at actual backing creation; metadata transformations preserve this owner. Cloning bytes must allocate a fresh backing before attaching it.

Equations

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

def Miri.Memory.Allocation.withoutNativeBuffer {Prov Extra : Type} (allocation : Allocation Prov Extra) : Allocation Prov Extra

Equations

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

def Miri.Memory.Allocation.len {Prov Extra : Type} (allocation : Allocation Prov Extra) : Nat

Equations

• allocation.len = (Miri.Memory.Allocation.rawBytes✝ allocation).size

def Miri.Memory.Allocation.byteSize {Prov Extra : Type} (allocation : Allocation Prov Extra) : ABI.Size

Equations

• allocation.byteSize = Miri.Memory.Allocation.size✝ allocation

def Miri.Memory.Allocation.provenanceMap {Prov Extra : Type} (allocation : Allocation Prov Extra) : ProvenanceMap Prov

Equations

• allocation.provenanceMap = Miri.Memory.Allocation.provenance✝ allocation

def Miri.Memory.Allocation.initializationMask {Prov Extra : Type} (allocation : Allocation Prov Extra) : InitMask

Equations

• allocation.initializationMask = Miri.Memory.Allocation.initMask✝ allocation

def Miri.Memory.Allocation.adjustFromTcx {Prov : Type} [PointerProvenance Prov] {CallbackError HookState : Type} (source : Allocation) (layout : ABI.TargetDataLayout) (allocateBytes : Array UInt8 → ABI.Align → HookState → EStateM.Result CallbackError HookState (Array UInt8)) (adjustPointer : Pointer CtfeProvenance → HookState → EStateM.Result CallbackError HookState (Pointer Prov)) : EStateM (AllocationAdjustError CallbackError) HookState (Allocation Prov)

Source Allocation::adjust_from_tcx, used when importing interned global and thread-local allocations into a machine with a different byte backend or provenance representation. The two callbacks preserve the source's allocation and pointer-conversion failure boundaries. The source ptrs() assertion is reported explicitly when byte-fragment provenance is present.

Equations

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

def Miri.Memory.Allocation.getBytesUnchecked {Prov Extra : Type} (allocation : Allocation Prov Extra) (range : AllocRange) : Except AllocError (Array UInt8)

Raw bytes with the source method's caller-side bounds precondition made explicit rather than relying on a host array indexing panic.

Equations

• allocation.getBytesUnchecked range = Miri.Memory.Allocation.checkedSlice✝ allocation range

def Miri.Memory.Allocation.inspectWithUninitAndPtrOutsideInterpreter {Prov Extra : Type} (allocation : Allocation Prov Extra) (start finish : Nat) : Except AllocError (Array UInt8)

Inspect raw bytes outside interpreter execution, including uninitialized bytes and provenance. The source slice panics for invalid endpoints; Lean reports that invalid domain explicitly.

Equations

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

def Miri.Memory.Allocation.refreshNativeBytes {Prov Extra : Type} (allocation : Allocation Prov Extra) (bytes : Array UInt8) : Except AllocError (Allocation Prov Extra)

Adopt a snapshot of this allocation's actual native backing storage after an external host operation. The host must report the very same allocation; this is not an interpreter write: initialization, provenance, permissions and extras remain unchanged until source process_native_write/trace processing.

Equations

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

def Miri.Memory.Allocation.getBytesStripProvenance {Prov Extra : Type} [PointerProvenance Prov] (allocation : Allocation Prov Extra) (layout : ABI.TargetDataLayout) (range : AllocRange) : Except AllocError (Array UInt8)

Matches Allocation::get_bytes_strip_provenance: check initialization first, then reject overlapping non-address provenance when required, then return bytes. layout supplies the target pointer width used by the map.

Equations

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

Scalar memory access. The source assumes caller-side bounds and alignment; these Lean methods keep invalid ranges as explicit errors instead of array panics.

def Miri.Memory.Allocation.readScalar {Prov Extra : Type} [DecidableEq Prov] [PointerProvenance Prov] (allocation : Allocation Prov Extra) (layout : ABI.TargetDataLayout) (range : AllocRange) (readProvenance : Bool) : Except AllocError (Scalar Prov)

Equations

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

def Miri.Memory.Allocation.writeScalar {Prov Extra : Type} (layout : ABI.TargetDataLayout) (range : AllocRange) (value : Scalar Prov) : EStateM AllocError (Allocation Prov Extra) Unit

The full source Allocation::write_scalar state transition. It checks mutability, decodes the scalar, marks initialization, clears overwritten provenance against the old bytes, writes target-endian bits, then inserts a pointer provenance entry when the value is a pointer.

Equations

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

def Miri.Memory.Allocation.writePointer {Prov Extra : Type} (layout : ABI.TargetDataLayout) (range : AllocRange) (pointer : Pointer Prov) : EStateM AllocError (Allocation Prov Extra) Unit

Pointer-valued convenience wrapper around the source scalar write path.

Equations

• Miri.Memory.Allocation.writePointer layout range pointer = Miri.Memory.Allocation.writeScalar layout range (Miri.Memory.Scalar.fromPointer layout pointer)

def Miri.Memory.Allocation.writeBytes {Prov Extra : Type} (start : ABI.Size) (bytes : Array UInt8) (pointerSize : ABI.Size) : EStateM AllocError (Allocation Prov Extra) Unit

Write a finite byte stream into this allocation. The array length is the exact iterator length used by write_bytes_ptr; the range is derived from that length, and bounds remain an explicit caller-side check.

Equations

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

def Miri.Memory.Allocation.writeRepeatedByte {Prov Extra : Type} (start : ABI.Size) (byte : UInt8) (count : UInt64) (pointerSize : ABI.Size) : EStateM AllocError (Allocation Prov Extra) Unit

Write a repeated byte without materializing an input array. This is the finite-array counterpart of rustc write_bytes_ptr with std::iter::repeat_n: perform the same checked range, mutability, initialization, and provenance transitions as writeBytes, then fill the already allocated storage in place.

Equations

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

def Miri.Memory.Allocation.writeUninit {Prov Extra : Type} (range : AllocRange) (pointerSize : ABI.Size) : EStateM AllocError (Allocation Prov Extra) Unit

Source Allocation::write_uninit: clear initialization first, then clear overlapping provenance, while leaving the arbitrary byte representation alone.

Equations

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

def Miri.Memory.Allocation.clearProvenance {Prov Extra : Type} (range : AllocRange) (pointerSize : ABI.Size) : EStateM AllocError (Allocation Prov Extra) Unit

Source Allocation::clear_provenance: preserve bytes and initialization, but remove or fragment all pointer provenance intersecting the checked range.

Equations

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

def Miri.Memory.Allocation.processNativeWrite {Prov Extra : Type} [PointerProvenance Prov] (layout : ABI.TargetDataLayout) (range? : Option AllocRange) : EStateM AllocError (Allocation Prov Extra) Unit

Source Allocation::process_native_write: mark the selected range initialized, then replace provenance in it with wildcard byte fragments. This is intentionally available only to provenance types with a wildcard. Range and mutability failures are explicit; a missing wildcard remains an error after the source-ordered initialization transition.

Equations

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

def Miri.Memory.Allocation.provenanceMergeBytes {Prov Extra : Type} [DecidableEq Prov] (layout : ABI.TargetDataLayout) : EStateM AllocError (Allocation Prov Extra) Bool

Source Allocation::provenance_merge_bytes: attempt to coalesce complete byte-fragment pointers. A false result may retain successful earlier coalescings, exactly as the source map iteration does.

Equations

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

def Miri.Memory.Allocation.copyRepeatedly {Prov Extra : Type} (source : Allocation Prov Extra) (sourceRange : AllocRange) (destStart : ABI.Size) (repeatCount : UInt64) (pointerSize : ABI.Size) (sameAllocation nonoverlapping : Bool) : EStateM AllocError (Allocation Prov Extra) Unit

Source allocation-level half of mem_copy_repeatedly. Pointer resolution, access checks, and machine hooks are supplied by the caller. The source's initialization and provenance snapshots are prepared before destination overwrite clears its old metadata.

Equations

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

def Miri.Memory.Allocation.copy {Prov Extra : Type} (source : Allocation Prov Extra) (sourceRange : AllocRange) (destStart pointerSize : ABI.Size) (sameAllocation nonoverlapping : Bool) : EStateM AllocError (Allocation Prov Extra) Unit

The source mem_copy operation is a one-copy specialization.

Equations

• source.copy sourceRange destStart pointerSize sameAllocation nonoverlapping = source.copyRepeatedly sourceRange destStart 1 pointerSize sameAllocation nonoverlapping

def Miri.Memory.Allocation.withMutability {Prov Extra : Type} (self : Allocation Prov Extra) (mutability : Mutability) : Allocation Prov Extra

Source allocation mutability is a public field. This update preserves all byte, initialization, provenance and allocation-extra state.

Equations

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

def Miri.Memory.Allocation.fromCompilerImage (bytes : Array UInt8) (align : ABI.Align) (mutability : Mutability) (mask : InitMask) (provenance : ProvenanceMap CtfeProvenance) (pointerSize : ABI.Size) : Except AllocError Allocation

Validated serialization boundary for an interned compiler allocation. Unlike writes, importing its image does not initialize bytes, clear provenance, or change the byte representation of pointers.

Equations

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

theorem Miri.Memory.Allocation.writeScalar_mapExtra {P E E' : Type} (layout : ABI.TargetDataLayout) (range : AllocRange) (value : Scalar P) (allocation : Allocation P E) (f : E → E') : writeScalar layout range value (allocation.mapExtra f) = match writeScalar layout range value allocation with | EStateM.Result.ok value state => EStateM.Result.ok value (state.mapExtra f) | EStateM.Result.error error state => EStateM.Result.error error (state.mapExtra f)

theorem Miri.Memory.Allocation.writeUninit_mapExtra {P E E' : Type} (range : AllocRange) (pointerSize : ABI.Size) (allocation : Allocation P E) (f : E → E') : writeUninit range pointerSize (allocation.mapExtra f) = match writeUninit range pointerSize allocation with | EStateM.Result.ok value state => EStateM.Result.ok value (state.mapExtra f) | EStateM.Result.error error state => EStateM.Result.error error (state.mapExtra f)

theorem Miri.Memory.Allocation.tryNew_uninit_image {P : Type} (size : ABI.Size) (align : ABI.Align) (pointerSize : ABI.Size) (allocation : Allocation P) (positive : pointerSize.bytes ≠ 0) (created : (tryNew size align AllocInit.Uninit fun (n : ABI.Size) (x : ABI.Align) => some (Array.replicate n.bytes.toNat 0)) = Except.ok allocation) : allocation.len = size.bytes.toNat ∧ ∃ (initialized : Allocation P), fromBytes (Array.replicate size.bytes.toNat 0) align Mutability.Mut = Except.ok initialized ∧ writeUninit (allocRange ABI.Size.ZERO size) pointerSize initialized = EStateM.Result.ok () (if size.bytes = 0 then { rawBytes := Miri.Memory.Allocation.rawBytes✝ Unit allocation, size := Miri.Memory.Allocation.size✝ Unit allocation, provenance := Miri.Memory.Allocation.provenance✝ Unit allocation, initMask := InitMask.new size true, align := allocation.align Unit, mutability := allocation.mutability Unit, extra := allocation.extra Unit, nativeBuffer := allocation.nativeBuffer Unit } else allocation)

theorem Miri.Memory.Allocation.tryNew_replicate {P : Type} (size : ABI.Size) (align : ABI.Align) (alignmentBytes : UInt64) (bytes : align.bytes = Except.ok alignmentBytes) (normalized : ABI.Align.fromBytes alignmentBytes = Except.ok align) : ∃ (allocation : Allocation P), (tryNew size align AllocInit.Uninit fun (n : ABI.Size) (x : ABI.Align) => some (Array.replicate n.bytes.toNat 0)) = Except.ok allocation ∧ allocation.byteSize = size ∧ allocation.len = size.bytes.toNat ∧ allocation.nativeBuffer Unit = none ∧ allocation.mutability Unit = Mutability.Mut

theorem Miri.Memory.Allocation.tryNew_replicate_full {P : Type} (size : ABI.Size) (align : ABI.Align) (alignmentBytes : UInt64) (bytes : align.bytes = Except.ok alignmentBytes) (normalized : ABI.Align.fromBytes alignmentBytes = Except.ok align) : ∃ (allocation : Allocation P), (tryNew size align AllocInit.Uninit fun (n : ABI.Size) (x : ABI.Align) => some (Array.replicate n.bytes.toNat 0)) = Except.ok allocation ∧ allocation.byteSize = size ∧ allocation.len = size.bytes.toNat ∧ allocation.nativeBuffer Unit = none ∧ allocation.mutability Unit = Mutability.Mut ∧ allocation.align Unit = align

theorem Miri.Memory.Allocation.writeScalar_fresh_zero {P E : Type} (layout : ABI.TargetDataLayout) (allocation : Allocation P E) (value : Scalar P) (converted : ScalarBitsOrPointer P) (storage : allocation.len = allocation.byteSize.bytes.toNat) (mutable : allocation.mutability = Mutability.Mut) (maskLength : allocation.initializationMask.len = allocation.byteSize) (maskValid : InitMask.WriteProof.WellFormed allocation.initializationMask) (empty : allocation.provenanceMap = ProvenanceMap.new) (nonzero : value.size.bytes ≠ 0) (width : value.size.bytes.toNat ≤ 16) (bound : value.size.bytes.toNat ≤ allocation.byteSize.bytes.toNat) (target : layout.pointerWidth = ABI.PointerWidth.w64) (pointerWidth : match converted with | ScalarBitsOrPointer.bits value => True | ScalarBitsOrPointer.pointer value_1 => value.size = ABI.Size.fromBits layout.pointerWidth.bits) (conversion : value.toBitsOrPtrInternal value.size = Except.ok converted) : ∃ (updated : Allocation P E), writeScalar layout (allocRange ABI.Size.ZERO value.size) value allocation = EStateM.Result.ok () updated ∧ updated.byteSize = allocation.byteSize ∧ updated.len = allocation.len ∧ updated.mutability = allocation.mutability ∧ updated.align = allocation.align ∧ updated.extra = allocation.extra ∧ updated.nativeBuffer = allocation.nativeBuffer ∧ updated.initializationMask.len = allocation.initializationMask.len ∧ InitMask.WriteProof.WellFormed updated.initializationMask ∧ (updated.provenanceMap = ProvenanceMap.new ∨ value.size = Miri.Memory.pointerSize✝ layout ∧ ∃ (provenance : P), updated.provenanceMap = Miri.Memory.Allocation.zeroPointer✝ provenance)

Successful physical first component write in fresh uninitialized storage. All non-byte metadata is retained; only an optional zero-offset pointer entry can be present for the subsequent disjoint component.

theorem Miri.Memory.Allocation.writeScalar_separated {P E : Type} (layout : ABI.TargetDataLayout) (allocation : Allocation P E) (offset : ABI.Size) (value : Scalar P) (converted : ScalarBitsOrPointer P) (storage : allocation.len = allocation.byteSize.bytes.toNat) (mutable : allocation.mutability = Mutability.Mut) (maskLength : allocation.initializationMask.len = allocation.byteSize) (maskValid : InitMask.WriteProof.WellFormed allocation.initializationMask) (separated : allocation.provenanceMap = ProvenanceMap.new ∨ ∃ (provenance : P), allocation.provenanceMap = Miri.Memory.Allocation.zeroPointer✝ provenance ∧ (Miri.Memory.pointerSize✝ layout).bytes.toNat ≤ offset.bytes.toNat) (nonzero : value.size.bytes ≠ 0) (width : value.size.bytes.toNat ≤ 16) (bound : offset.bytes.toNat + value.size.bytes.toNat ≤ allocation.byteSize.bytes.toNat) (target : layout.pointerWidth = ABI.PointerWidth.w64) (pointerWidth : match converted with | ScalarBitsOrPointer.bits value => True | ScalarBitsOrPointer.pointer value_1 => value.size = ABI.Size.fromBits layout.pointerWidth.bits) (conversion : value.toBitsOrPtrInternal value.size = Except.ok converted) : ∃ (updated : Allocation P E), writeScalar layout (allocRange offset value.size) value allocation = EStateM.Result.ok () updated ∧ updated.byteSize = allocation.byteSize ∧ updated.len = allocation.len ∧ updated.mutability = allocation.mutability ∧ updated.align = allocation.align ∧ updated.extra = allocation.extra ∧ updated.nativeBuffer = allocation.nativeBuffer ∧ updated.initializationMask.len = allocation.initializationMask.len ∧ InitMask.WriteProof.WellFormed updated.initializationMask

The second component writes a disjoint window of fresh storage. It keeps an earlier pointer entry intact and derives every provenance operation.

theorem Miri.Memory.Allocation.tryNew_uninit_shape {P : Type} (size : ABI.Size) (align : ABI.Align) (allocation : Allocation P) (created : (tryNew size align AllocInit.Uninit fun (n : ABI.Size) (x : ABI.Align) => some (Array.replicate n.bytes.toNat 0)) = Except.ok allocation) : allocation.provenanceMap = ProvenanceMap.new ∧ allocation.initializationMask = InitMask.new size false