Canonical SIMD/architecture/x86 execution dictionaries. Compiler vector and integer type construction remains typed metadata; projection, typed memory, transmute and pointer conversion execute the existing source operations.

@[reducible, inline]

abbrev Miri.Interpreter.IntrinsicVectorMachine.User (User : Type) : Type

Equations

• Miri.Interpreter.IntrinsicVectorMachine.User = Miri.Interpreter.ValidityMachine.UserState

@[reducible, inline]

abbrev Miri.Interpreter.IntrinsicVectorMachine.State (K U : Type) : Type

Equations

• Miri.Interpreter.IntrinsicVectorMachine.State K U = Miri.Interpreter.ValidityMachine.State K U

@[reducible, inline]

abbrev Miri.Interpreter.IntrinsicVectorMachine.M (K U A : Type) : Type

Equations

• Miri.Interpreter.IntrinsicVectorMachine.M K U = Miri.Interpreter.ValidityMachine.M K U

def Miri.Interpreter.IntrinsicVectorMachine.projectionError : ProjectionError → StepError

Classification is retained explicitly for nonportable compiler/machine errors; numeric bounds and scalar reads have their source interpreter classes.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.IntrinsicVectorMachine.projectionError (Miri.Interpreter.ProjectionError.machineError error) = error
• Miri.Interpreter.IntrinsicVectorMachine.projectionError (Miri.Interpreter.ProjectionError.obligation message) = Miri.Interpreter.StepError.callback message
• Miri.Interpreter.IntrinsicVectorMachine.projectionError (Miri.Interpreter.ProjectionError.invariant message) = Miri.Interpreter.StepError.invalidProgram message
• Miri.Interpreter.IntrinsicVectorMachine.projectionError Miri.Interpreter.ProjectionError.pointerArithOverflow = Miri.Interpreter.StepError.undefinedBehavior "overflowing in-bounds pointer offset"
• Miri.Interpreter.IntrinsicVectorMachine.projectionError (Miri.Interpreter.ProjectionError.scalar error) = Miri.Interpreter.ScalarOps.scalarError error
• Miri.Interpreter.IntrinsicVectorMachine.projectionError (Miri.Interpreter.ProjectionError.immediate error) = Miri.Interpreter.ScalarOps.immediateError error

def Miri.Interpreter.IntrinsicVectorMachine.transmuteWrite {K U C : Type} (projection : PlaceProjectionHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (choice : C) (source : RuntimePlace Memory.Provenance) (target : LocalLayout) : M K U (RuntimePlace Memory.Provenance)

Source Projectable::transmute assertions, then zero-offset wrapping projection. The operation never erases/recreates pointer provenance.

Equations

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

def Miri.Interpreter.IntrinsicVectorMachine.bindSimd {K U C : Type} [DecidableEq K] (base : IntrinsicSimdHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (access : PlaceMachine.AccessConfig K (User U)) (projection : PlaceProjectionHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (copy : PlaceCopyHooks Memory.Provenance (State K U) C) (pointerCompiler : PointerPlaceMachine.Compiler K U C) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) : IntrinsicSimdHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Source field/index projection is retained for every lane: initialization, provenance and hooks are checked by the later actual read/write, not simulated by extracting an untyped array of values.

Equations

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

def Miri.Interpreter.IntrinsicVectorMachine.bindArchitecture {K U C : Type} (base : ArchitectureHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (simd : IntrinsicSimdHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (projection : PlaceProjectionHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (u128Layout : LocalLayout) : ArchitectureHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

Shared backing dictionary for AArch64/LoongArch and all x86 families.

Equations

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

def Miri.Interpreter.IntrinsicVectorMachine.bindX86 {K U C : Type} [DecidableEq K] (base : IntrinsicX86.Hooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (architecture : ArchitectureHooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)) (access : PlaceMachine.AccessConfig K (User U)) (projection : PlaceProjectionHooks Memory.Provenance (State K U) C MachineHooks.FrameExtra) (pointers : PointerMachine.Hooks K (ValidityMachine.Control U)) : IntrinsicX86.Hooks Memory.Provenance (State K U) C (RuntimePlace Memory.Provenance)

x86 reinterpretation remains source Projectable wrapping projection; actual gathers use the full canonical global-aware memory copy.

Equations

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