Documentation

Miri.Input.EvalEntrySymbols

Outer bootstrap view of the same source intrinsic registry used by the inner execution core. Reassociation changes no allocation/type identity.

source
@[reducible, inline]
abbrev Miri.Input.EvalEntrySymbols.W (Os R Payload H D O Aff B Host : Type) :
Type
Equations
Instances For
    source
    def Miri.Input.EvalEntrySymbols.access {Os R P H D O Aff B Host : Type} :
    Interpreter.IntrinsicSymbolsMachine.Access (EvalWorld.User Os R P H D O Aff B Host)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Miri.Input.EvalEntrySymbols.get_put {Os R P H D O Aff B Host : Type} (user : EvalWorld.User Os R P H D O Aff B Host) (registry : Interpreter.IntrinsicSymbolsMachine.Registry) :
      access.get (access.put user registry) = registry
      source
      theorem Miri.Input.EvalEntrySymbols.put_get {Os R P H D O Aff B Host : Type} (user : EvalWorld.User Os R P H D O Aff B Host) :
      access.put user (access.get user) = user
      source
      def Miri.Input.EvalEntrySymbols.attach {Os R P H D O Aff B Host : Type} (p : CompilerProviders.Prepared) (image : AllocationImage.Imported) :
      Interpreter.MachineHooks.M Memory.MiriMemoryKind (EvalWorld.User Os R P H D O Aff B Host) Unit
      Equations
      Instances For