(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module instructions.
  Module utility.
    (*
    pub(crate) unsafe fn read_i16(ptr: *const u8) -> i16 {
        i16::from_be_bytes(core::slice::from_raw_parts(ptr, 2).try_into().unwrap())
    }
    *)
    Definition read_i16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ ptr ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "i16", "from_be_bytes", [] |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 2 ]
                        [ Ty.path "u8" ];
                      Ty.path "core::array::TryFromSliceError"
                    ],
                  "unwrap",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::TryInto",
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      [
                        Ty.apply
                          (Ty.path "array")
                          [ Value.Integer IntegerKind.Usize 2 ]
                          [ Ty.path "u8" ]
                      ],
                      "try_into",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_function (| "core::slice::raw::from_raw_parts", [ Ty.path "u8" ] |),
                        [ M.read (| ptr |); Value.Integer IntegerKind.Usize 2 ]
                      |)
                    ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_read_i16 :
      M.IsFunction "revm_interpreter::instructions::utility::read_i16" read_i16.
    
    (*
    pub(crate) unsafe fn read_u16(ptr: *const u8) -> u16 {
        u16::from_be_bytes(core::slice::from_raw_parts(ptr, 2).try_into().unwrap())
    }
    *)
    Definition read_u16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ ptr ] =>
        ltac:(M.monadic
          (let ptr := M.alloc (| ptr |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "u16", "from_be_bytes", [] |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 2 ]
                        [ Ty.path "u8" ];
                      Ty.path "core::array::TryFromSliceError"
                    ],
                  "unwrap",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::TryInto",
                      Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                      [
                        Ty.apply
                          (Ty.path "array")
                          [ Value.Integer IntegerKind.Usize 2 ]
                          [ Ty.path "u8" ]
                      ],
                      "try_into",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_function (| "core::slice::raw::from_raw_parts", [ Ty.path "u8" ] |),
                        [ M.read (| ptr |); Value.Integer IntegerKind.Usize 2 ]
                      |)
                    ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_read_u16 :
      M.IsFunction "revm_interpreter::instructions::utility::read_u16" read_u16.
  End utility.
End instructions.
