Pinned step.rs write_aggregate and write_repeat. The same MIR operands and canonical layouts flow through RvalueHooks; stateful obligations retain effects on failure. No field write is treated as initialization of aggregate padding.

structure Miri.Interpreter.AggregateHooks (Prov S C V : Type) : Type

• target : ABI.TargetDataLayout
• placeLayout : V → LocalLayout
• evalOperand : C → MIR.Operand → Option LocalLayout → RvalueM S (OpTy Prov)
• evalOperandAt : C → OperandPath → MIR.Operand → Option LocalLayout → RvalueM S (OpTy Prov)
• readPointer : C → OpTy Prov → RvalueM S (Memory.Pointer (Option Prov))
• readScalar : C → OpTy Prov → RvalueM S (Memory.Scalar Prov)
• projectDowncast : C → V → MIR.VariantIndex → RvalueM S V
• projectField : C → V → MIR.FieldIndex → RvalueM S V
• copyOp : C → OpTy Prov → V → RvalueM S Unit
• copyOpNoValidate : C → OpTy Prov → V → Bool → RvalueM S Unit
• writeDiscriminant : C → MIR.VariantIndex → V → RvalueM S Unit
• enforceValidity : C → LocalLayout → RvalueM S Bool
• validate : C → V → RvalueM S Unit

  Includes recursive validity policy and reset_provenance_and_padding=true.

• forceAllocation : C → V → RvalueM S V
• length : C → V → RvalueM S UInt64
• getPlaceAllocMut : C → V → RvalueM S Unit
• projectIndex : C → V → UInt64 → RvalueM S V
• placePointer : V → Except StepError (Memory.Pointer (Option Prov))
• wrappingOffset : Memory.Pointer (Option Prov) → ABI.Size → Except StepError (Memory.Pointer (Option Prov))
• memCopyRepeatedly : C → Memory.Pointer (Option Prov) → Memory.Pointer (Option Prov) → ABI.Size → UInt64 → Bool → RvalueM S Unit

  No alignment requirement: first-element copy already checked it. Must retain nonoverlapping checks, memory hooks and partial mutations.

def Miri.Interpreter.writeAggregate {P S C V : Type} (h : AggregateHooks P S C V) (choice : C) (kind : MIR.AggregateKind) (operands : Array MIR.Operand) (dest : V) : RvalueM S Unit

Equations

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

def Miri.Interpreter.writeRepeat {P S C V : Type} (h : AggregateHooks P S C V) (choice : C) (operand : MIR.Operand) (dest : V) : RvalueM S Unit

The repeat count is the destination array length. Even zero-length repeats first evaluate the operand and force allocation, then validate mutable access. Positive lengths copy once and replicate the resulting bytes; the source can alias the destination, so evaluating/copying every element would be incorrect.

Equations

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

def Miri.Interpreter.RvalueHooks.withAggregate {P S C V : Type} (base : RvalueHooks P S C V) (aggregate : AggregateHooks P S C V) : RvalueHooks P S C V

Install the aggregate/repeat source ports into the existing rvalue dispatch.

Equations

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

def Miri.Interpreter.aggregateWrappingOffset {Prov : Type} (target : Memory.PointerArithmetic) (pointer : Memory.Pointer (Option Prov)) (size : ABI.Size) : Except StepError (Memory.Pointer (Option Prov))

Actual pointer wrapping arithmetic, retaining provenance and target width.

Equations

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

def Miri.Interpreter.aggregateMemoryCopyRepeatedly {Kind Prov Extra HookState ProvExtra S : Type} [DecidableEq Kind] (pointerSize : ABI.Size) (hooks : Memory.MemoryCopyHooks Prov Extra Kind HookState ProvExtra) (getMemory : S → Memory.MemoryState Prov Extra Kind) (getHooks : S → HookState) (putMemoryHooks : S → Memory.MemoryState Prov Extra Kind → HookState → S) (mapError : Memory.MemoryLifecycleError → StepError) (source dest : Memory.Pointer (Option Prov)) (size : ABI.Size) (count : UInt64) (nonoverlapping : Bool) : RvalueM S Unit

Concrete repeated-copy adapter to existing allocation/memory semantics. The supplied state embedding must preserve unrelated execution state.

Equations

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