Documentation

Miri.Interpreter.IntrinsicX86.Crypto

source
def Miri.Interpreter.IntrinsicX86.sbox :
Array UInt8

Constants transcribed from pinned math.rs::aes::SBOX.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Miri.Interpreter.IntrinsicX86.subWord (value : UInt32) :
    Except StepError UInt32
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Miri.Interpreter.IntrinsicX86.aesKeygen (value : ABI.U128) (rcon : UInt8) :
      Except StepError ABI.U128
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Miri.Interpreter.IntrinsicX86.gfMultiply (left right : UInt8) :
        UInt8
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Miri.Interpreter.IntrinsicX86.gfInverse (value : UInt8) :
          UInt8
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Miri.Interpreter.IntrinsicX86.gfni {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (full name : String) (args : Array (OpTy P)) (dest : V) :
            M S Bool
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Miri.Interpreter.IntrinsicX86.aesni {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (full name : String) (args : Array (OpTy P)) (dest : V) :
              M S Bool
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Miri.Interpreter.IntrinsicX86.pclmul {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (left right immediate : OpTy P) (dest : V) (n : UInt64) :
                M S Unit
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Miri.Interpreter.IntrinsicX86.readReverseQuad {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (source : OpTy P) :
                  M S (IntrinsicCrypto.Quad UInt32)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Miri.Interpreter.IntrinsicX86.sha {P S C V : Type} [Memory.PointerProvenance P] (h : Hooks P S C V) (choice : C) (full name : String) (args : Array (OpTy P)) (dest : V) :
                    M S Bool
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For