Stateful consumers of canonical runtime array constructors. The accessors must refer to one persistent interpreter World; reconstruction per call loses canonical allocation of type identities. Memory/host actions remain unchanged.

structure Miri.Input.RuntimeArrayQueries.Access (S : Type) : Type

• get : S → RuntimeArrayTypes.World
• set : S → RuntimeArrayTypes.World → S

def Miri.Input.RuntimeArrayQueries.arrayLayout {S : Type} (access : Access S) (element : MIR.TyId) (count : UInt64) : EStateM Interpreter.StepError S Interpreter.LocalLayout

Canonical constructor provider for EntryArguments and other runtime-sized arrays, using the actual supplied element type identity and persistent World.

Equations

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

def Miri.Input.RuntimeArrayQueries.osStringsHooks {S P Os Kind : Type} (access : Access S) (base : Interpreter.OsStrings.Hooks P S Os Kind) : Interpreter.OsStrings.Hooks P S Os Kind

Equations

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

def Miri.Input.RuntimeArrayQueries.layoutOf {S : Type} (access : Access S) (id : MIR.TyId) : EStateM Interpreter.StepError S Interpreter.LocalLayout

Equations

• Miri.Input.RuntimeArrayQueries.layoutOf access id = do let __do_lift ← get Miri.Input.RuntimeArrayQueries.lift✝ (Miri.Input.RuntimeArrayTypes.lookup (access.get __do_lift) id)

def Miri.Input.RuntimeArrayQueries.fieldLayout {S : Type} (access : Access S) (base : Interpreter.LocalLayout → Nat → EStateM Interpreter.StepError S Interpreter.LocalLayout) (parent : Interpreter.LocalLayout) (index : Nat) : EStateM Interpreter.StepError S Interpreter.LocalLayout

Source array field type is the constructor's element type. This does not infer an element from a stride, size, memory content or diagnostic spelling.

Equations

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

def Miri.Input.RuntimeArrayQueries.validityHooks {S P C E Fn Abi Pad : Type} (access : Access S) (base : Interpreter.ValidityVisitor.Hooks P S C E Fn Abi Pad) : Interpreter.ValidityVisitor.Hooks P S C E Fn Abi Pad

Bind classification for interned arrays; all other compiler leaves remain mandatory. Portable memory/validation actions still execute in the base hooks.

Equations

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