Compiler-only scalar leaves and the integer subpath used by source pointer arithmetic. No placeholder float/pointer/dereference callbacks are constructed merely to run an integer operation. The scalar-size/type/overflow checks are identical to ScalarOps.binary's integer arm.

structure Miri.Interpreter.ExecutionScalar.Leaves (S C : Type) : Type

• classify : C → MIR.TyId → RvalueM S ScalarTypeClass
• boolLayout : C → RvalueM S LocalLayout
• orderingLayout : C → RvalueM S LocalLayout
• overflowLayout : C → LocalLayout → RvalueM S LocalLayout
• metadataLayout : C → MIR.TyId → RvalueM S LocalLayout
• unitLayout : C → RvalueM S LocalLayout

def Miri.Interpreter.ExecutionScalar.Leaves.ofHooks {P S C : Type} (h : ScalarOpsHooks P S C) : Leaves S C

Equations

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

def Miri.Interpreter.ExecutionScalar.finish {S C P : Type} (h : Leaves S C) (choice : C) (input : LocalLayout) : IntegerResult → RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.ExecutionScalar.integerBinary {P S C : Type} [Memory.PointerProvenance P] (h : Leaves S C) (choice : C) (op : MIR.BinOp) (left right : RvalueImmTy P) : RvalueM S (RvalueImmTy P)

Equations

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

def Miri.Interpreter.ExecutionScalar.pointerBinary {P S C : Type} [Memory.PointerProvenance P] (target : ABI.TargetDataLayout) (queries : Leaves S C) (isRaw : C → MIR.TyId → RvalueM S Bool) (usizeLayout : C → RvalueM S LocalLayout) (choice : C) (op : MIR.BinOp) (left right : RvalueImmTy P) : RvalueM S (RvalueImmTy P)

Pinned Miri machine pointer comparison/atomic arithmetic fallback. Only actual result-layout and integer actions are required, not a full scalar record.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.ExecutionScalar.pointerBinary target queries isRaw usizeLayout choice op left right = throw (Miri.Interpreter.StepError.invalidProgram "unsupported Miri pointer binary operation")

def Miri.Interpreter.ExecutionScalar.hooks {K U C : Type} (queries : Leaves (MachineHooks.State K U) C) (access : PlaceMachine.AccessConfig K U) (arithmetic : Memory.PointerArithmetic) (isRaw : C → MIR.TyId → MachineHooks.M K U Bool) (usizeLayout : C → MachineHooks.M K U LocalLayout) (pointeeLayout : C → MIR.TyId → MachineHooks.M K U LocalLayout) (dereference : C → OpTy Memory.Provenance → MachineHooks.M K U (MPlaceTy Memory.Provenance)) (floats : FloatOpsHooks Memory.Provenance (MachineHooks.State K U) C) : ScalarOpsHooks Memory.Provenance (MachineHooks.State K U) C

Full scalar dictionary constructed without overwritten input callbacks. Pointer offsets retain compiler layout→multiply/overflow→signed conversion→ allocation bounds→wrapping-address order; dereference uses the actual source operand driver supplied by the physical factory.

Equations

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