Narrow source-backed allocation-access contracts. These do not assert that arbitrary supplied machine hooks implement the fixed Miri machine.

theorem Miri.Memory.AllocationAccess.zero_write {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (target : PointerArithmetic) (ptr : Pointer (Option Prov)) (ghostMode : Bool) (globalKind : Option MachineKind) (globalHooks : GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) : getPtrAllocMut memory hooksState target ptr (ABI.Size.ofBytes 0) ghostMode globalKind globalHooks accessHooks = { memory := memory, hooks := hooksState, touched := none, outcome := Except.ok none }

theorem Miri.Memory.AllocationAccess.zero_ghost_read {Prov Extra MachineKind HookState ProvExtra : Type} [DecidableEq MachineKind] (memory : MemoryState Prov Extra MachineKind) (hooksState : HookState) (target : PointerArithmetic) (ptr : Pointer (Option Prov)) (globalKind : Option MachineKind) (globalHooks : GlobalAllocationHooks Prov Extra MachineKind HookState) (accessHooks : AllocationAccessHooks Prov Extra MachineKind HookState ProvExtra) : getPtrAlloc memory hooksState target ptr (ABI.Size.ofBytes 0) true globalKind globalHooks accessHooks = { memory := memory, hooks := hooksState, touched := none, outcome := Except.ok none }