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

Module u256.
  Definition value_NUM_BITS_PER_BYTE : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 8 |))).
  
  Definition value_U256_NUM_BITS : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 256 |))).
  
  Definition value_U256_NUM_BYTES : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          BinOp.Wrap.div (|
            M.read (| M.get_constant (| "move_core_types::u256::U256_NUM_BITS" |) |),
            M.read (| M.get_constant (| "move_core_types::u256::NUM_BITS_PER_BYTE" |) |)
          |)
        |))).
  
  (* StructTuple
    {
      name := "U256FromStrError";
      const_params := [];
      ty_params := [];
      fields := [ Ty.path "uint::uint::FromStrRadixErr" ];
    } *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_u256_U256FromStrError.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256FromStrError".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_tuple_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "U256FromStrError" |);
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::u256::U256FromStrError",
                  0
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_u256_U256FromStrError.
  
  (*
  Enum U256CastErrorKind
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "TooLargeForU8";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "TooLargeForU16";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "TooLargeForU32";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "TooLargeForU64";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "TooLargeForU128";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_u256_U256CastErrorKind.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastErrorKind".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [
              M.read (| f |);
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU8"
                          |) in
                        M.alloc (| M.read (| Value.String "TooLargeForU8" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU16"
                          |) in
                        M.alloc (| M.read (| Value.String "TooLargeForU16" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU32"
                          |) in
                        M.alloc (| M.read (| Value.String "TooLargeForU32" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU64"
                          |) in
                        M.alloc (| M.read (| Value.String "TooLargeForU64" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU128"
                          |) in
                        M.alloc (| M.read (| Value.String "TooLargeForU128" |) |)))
                  ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_u256_U256CastErrorKind.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_u256_U256CastErrorKind.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastErrorKind".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_u256_U256CastErrorKind.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_u256_U256CastErrorKind.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastErrorKind".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::u256::U256CastErrorKind" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::u256::U256CastErrorKind" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_move_core_types_u256_U256CastErrorKind.
  
  Module Impl_core_cmp_Eq_for_move_core_types_u256_U256CastErrorKind.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastErrorKind".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.Tuple []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_move_core_types_u256_U256CastErrorKind.
  
  Module Impl_core_clone_Clone_for_move_core_types_u256_U256CastErrorKind.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastErrorKind".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (| M.read (| self |) |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_move_core_types_u256_U256CastErrorKind.
  
  Module Impl_core_marker_Copy_for_move_core_types_u256_U256CastErrorKind.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastErrorKind".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_core_types_u256_U256CastErrorKind.
  
  Module Impl_core_hash_Hash_for_move_core_types_u256_U256CastErrorKind.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastErrorKind".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::u256::U256CastErrorKind" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
                [ __self_discr; M.read (| state |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_move_core_types_u256_U256CastErrorKind.
  
  (* StructRecord
    {
      name := "U256CastError";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("kind", Ty.path "move_core_types::u256::U256CastErrorKind");
          ("val", Ty.path "move_core_types::u256::U256")
        ];
    } *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_u256_U256CastError.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field2_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "U256CastError" |);
              M.read (| Value.String "kind" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_core_types::u256::U256CastError",
                "kind"
              |);
              M.read (| Value.String "val" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_core_types::u256::U256CastError",
                  "val"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_u256_U256CastError.
  
  Module Impl_move_core_types_u256_U256CastError.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    (*
        pub fn new<T: std::convert::Into<U256>>(val: T, kind: U256CastErrorKind) -> Self {
            Self {
                kind,
                val: val.into(),
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ val; kind ] =>
        ltac:(M.monadic
          (let val := M.alloc (| val |) in
          let kind := M.alloc (| kind |) in
          Value.StructRecord
            "move_core_types::u256::U256CastError"
            [
              ("kind", M.read (| kind |));
              ("val",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::Into",
                    T,
                    [ Ty.path "move_core_types::u256::U256" ],
                    "into",
                    []
                  |),
                  [ M.read (| val |) ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  End Impl_move_core_types_u256_U256CastError.
  
  Module Impl_core_error_Error_for_move_core_types_u256_U256CastError.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_move_core_types_u256_U256CastError.
  
  Module Impl_core_fmt_Display_for_move_core_types_u256_U256CastError.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            let type_str = match self.kind {
                U256CastErrorKind::TooLargeForU8 => "u8",
                U256CastErrorKind::TooLargeForU16 => "u16",
                U256CastErrorKind::TooLargeForU32 => "u32",
                U256CastErrorKind::TooLargeForU64 => "u64",
                U256CastErrorKind::TooLargeForU128 => "u128",
            };
            let err_str = format!("Cast failed. {} too large for {}.", self.val, type_str);
            write!(f, "{err_str}")
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ type_str :=
              M.copy (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_core_types::u256::U256CastError",
                    "kind"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU8"
                          |) in
                        Value.String "u8"));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU16"
                          |) in
                        M.alloc (| M.read (| Value.String "u16" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU32"
                          |) in
                        M.alloc (| M.read (| Value.String "u32" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU64"
                          |) in
                        M.alloc (| M.read (| Value.String "u64" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::u256::U256CastErrorKind::TooLargeForU128"
                          |) in
                        M.alloc (| M.read (| Value.String "u128" |) |)))
                  ]
                |)
              |) in
            let~ err_str :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::hint::must_use", [ Ty.path "alloc::string::String" ] |),
                  [
                    M.read (|
                      let~ res :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "alloc::fmt::format", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_v1",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (| Value.String "Cast failed. " |);
                                        M.read (| Value.String " too large for " |);
                                        M.read (| Value.String "." |)
                                      ]
                                  |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_display",
                                            [ Ty.path "move_core_types::u256::U256" ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_core_types::u256::U256CastError",
                                              "val"
                                            |)
                                          ]
                                        |);
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_display",
                                            [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                                          |),
                                          [ type_str ]
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |) in
                      res
                    |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_fmt", [] |),
                [
                  M.read (| f |);
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                    [
                      M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                      M.alloc (|
                        Value.Array
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::Argument",
                                "new_display",
                                [ Ty.path "alloc::string::String" ]
                              |),
                              [ err_str ]
                            |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_move_core_types_u256_U256CastError.
  
  Module Impl_core_error_Error_for_move_core_types_u256_U256FromStrError.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256FromStrError".
    
    (*
        fn source(&self) -> Option<&(dyn std::error::Error + 'static)> {
            self.0.source()
        }
    *)
    Definition source (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::error::Error",
              Ty.path "uint::uint::FromStrRadixErr",
              [],
              "source",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256FromStrError",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("source", InstanceField.Method source) ].
  End Impl_core_error_Error_for_move_core_types_u256_U256FromStrError.
  
  Module Impl_core_fmt_Display_for_move_core_types_u256_U256FromStrError.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256FromStrError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            write!(f, "{}", self.0)
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_fmt", [] |),
            [
              M.read (| f |);
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_v1", [] |),
                [
                  M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                  M.alloc (|
                    Value.Array
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::rt::Argument",
                            "new_display",
                            [ Ty.path "uint::uint::FromStrRadixErr" ]
                          |),
                          [
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_core_types::u256::U256FromStrError",
                              0
                            |)
                          ]
                        |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_move_core_types_u256_U256FromStrError.
  
  (* StructTuple
    {
      name := "U256";
      const_params := [];
      ty_params := [];
      fields := [ Ty.path "primitive_types::U256" ];
    } *)
  
  Module Impl_core_clone_Clone_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_move_core_types_u256_U256.
  
  Module Impl_core_fmt_Debug_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_tuple_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "U256" |);
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::u256::U256",
                  0
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_u256_U256.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_u256_U256.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.path "primitive_types::U256",
              [ Ty.path "primitive_types::U256" ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_core_types::u256::U256",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_move_core_types_u256_U256.
  
  Module Impl_core_cmp_Eq_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_move_core_types_u256_U256.
  
  Module Impl_core_hash_Hash_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::hash::Hash",
              Ty.path "primitive_types::U256",
              [],
              "hash",
              [ __H ]
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |);
              M.read (| state |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_move_core_types_u256_U256.
  
  Module Impl_core_marker_Copy_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_core_types_u256_U256.
  
  Module Impl_core_cmp_PartialOrd_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (* PartialOrd *)
    Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.path "primitive_types::U256",
              [ Ty.path "primitive_types::U256" ],
              "partial_cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_core_types::u256::U256",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
  End Impl_core_cmp_PartialOrd_for_move_core_types_u256_U256.
  
  Module Impl_core_cmp_Ord_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (* Ord *)
    Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::Ord",
              Ty.path "primitive_types::U256",
              [],
              "cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_core_types::u256::U256",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Ord"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
  End Impl_core_cmp_Ord_for_move_core_types_u256_U256.
  
  Module Impl_core_default_Default_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "primitive_types::U256",
                  [],
                  "default",
                  []
                |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::default::Default"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method default) ].
  End Impl_core_default_Default_for_move_core_types_u256_U256.
  
  Module Impl_core_fmt_Display_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter) -> std::fmt::Result {
            self.0.fmt(f)
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::fmt::Display",
              Ty.path "primitive_types::U256",
              [],
              "fmt",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_move_core_types_u256_U256.
  
  Module Impl_core_fmt_UpperHex_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::UpperHex::fmt(&self.0, f)
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::fmt::UpperHex",
              Ty.path "primitive_types::U256",
              [],
              "fmt",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::UpperHex"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_UpperHex_for_move_core_types_u256_U256.
  
  Module Impl_core_fmt_LowerHex_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt::LowerHex::fmt(&self.0, f)
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::fmt::LowerHex",
              Ty.path "primitive_types::U256",
              [],
              "fmt",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |);
              M.read (| f |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::LowerHex"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_LowerHex_for_move_core_types_u256_U256.
  
  Module Impl_core_str_traits_FromStr_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Err = U256FromStrError; *)
    Definition _Err : Ty.t := Ty.path "move_core_types::u256::U256FromStrError".
    
    (*
        fn from_str(s: &str) -> Result<Self, Self::Err> {
            Self::from_str_radix(s, 10)
        }
    *)
    Definition from_str (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ s ] =>
        ltac:(M.monadic
          (let s := M.alloc (| s |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::u256::U256",
              "from_str_radix",
              []
            |),
            [ M.read (| s |); Value.Integer IntegerKind.U32 10 ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::str::traits::FromStr"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("Err", InstanceField.Ty _Err); ("from_str", InstanceField.Method from_str) ].
  End Impl_core_str_traits_FromStr_for_move_core_types_u256_U256.
  
  Module Impl_serde_de_Deserialize_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn deserialize<D>(deserializer: D) -> std::result::Result<Self, D::Error>
        where
            D: Deserializer<'de>,
        {
            Ok(U256::from_le_bytes(
                &(<[u8; U256_NUM_BYTES]>::deserialize(deserializer)?),
            ))
        }
    *)
    Definition deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ D ], [ deserializer ] =>
        ltac:(M.monadic
          (let deserializer := M.alloc (| deserializer |) in
          M.catch_return (|
            ltac:(M.monadic
              (Value.StructTuple
                "core::result::Result::Ok"
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "move_core_types::u256::U256",
                      "from_le_bytes",
                      []
                    |),
                    [
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::try_trait::Try",
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 32 ]
                                    [ Ty.path "u8" ];
                                  Ty.associated
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 32 ]
                                    [ Ty.path "u8" ],
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Break",
                                  0
                                |) in
                              let residual := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::try_trait::FromResidual",
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [ Ty.path "move_core_types::u256::U256"; Ty.associated
                                            ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              []
                                              [ Ty.path "core::convert::Infallible"; Ty.associated ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    ]
                  |)
                ]))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "serde::de::Deserialize"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("deserialize", InstanceField.Method deserialize) ].
  End Impl_serde_de_Deserialize_for_move_core_types_u256_U256.
  
  Module Impl_serde_ser_Serialize_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn serialize<S>(&self, serializer: S) -> std::result::Result<S::Ok, S::Error>
        where
            S: Serializer,
        {
            self.to_le_bytes().serialize(serializer)
        }
    *)
    Definition serialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ _ as S ], [ self; serializer ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let serializer := M.alloc (| serializer |) in
          M.call_closure (|
            M.get_trait_method (|
              "serde::ser::Serialize",
              Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ],
              [],
              "serialize",
              [ S ]
            |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_core_types::u256::U256",
                    "to_le_bytes",
                    []
                  |),
                  [ M.read (| M.read (| self |) |) ]
                |)
              |);
              M.read (| serializer |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "serde::ser::Serialize"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("serialize", InstanceField.Method serialize) ].
  End Impl_serde_ser_Serialize_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_bit_Shl_u32_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn shl(self, rhs: u32) -> Self::Output {
            let Self(lhs) = self;
            Self(lhs << rhs)
        }
    *)
    Definition shl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::u256::U256",
                        0
                      |) in
                    let lhs := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::u256::U256"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::bit::Shl",
                              Ty.path "primitive_types::U256",
                              [ Ty.path "u32" ],
                              "shl",
                              []
                            |),
                            [ M.read (| lhs |); M.read (| rhs |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::bit::Shl"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "u32" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("shl", InstanceField.Method shl) ].
  End Impl_core_ops_bit_Shl_u32_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_bit_Shl_u8_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn shl(self, rhs: u8) -> Self::Output {
            let Self(lhs) = self;
            Self(lhs << rhs)
        }
    *)
    Definition shl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::u256::U256",
                        0
                      |) in
                    let lhs := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::u256::U256"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::bit::Shl",
                              Ty.path "primitive_types::U256",
                              [ Ty.path "u8" ],
                              "shl",
                              []
                            |),
                            [ M.read (| lhs |); M.read (| rhs |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::bit::Shl"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "u8" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("shl", InstanceField.Method shl) ].
  End Impl_core_ops_bit_Shl_u8_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_bit_Shr_u8_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn shr(self, rhs: u8) -> Self::Output {
            let Self(lhs) = self;
            Self(lhs >> rhs)
        }
    *)
    Definition shr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::u256::U256",
                        0
                      |) in
                    let lhs := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::u256::U256"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::bit::Shr",
                              Ty.path "primitive_types::U256",
                              [ Ty.path "u8" ],
                              "shr",
                              []
                            |),
                            [ M.read (| lhs |); M.read (| rhs |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::bit::Shr"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "u8" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("shr", InstanceField.Method shr) ].
  End Impl_core_ops_bit_Shr_u8_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_bit_BitOr_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn bitor(self, rhs: U256) -> Self::Output {
            let Self(lhs) = self;
            let Self(rhs) = rhs;
            Self(lhs | rhs)
        }
    *)
    Definition bitor (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::u256::U256",
                        0
                      |) in
                    let lhs := M.copy (| γ0_0 |) in
                    M.match_operator (|
                      rhs,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_core_types::u256::U256",
                                0
                              |) in
                            let rhs := M.copy (| γ0_0 |) in
                            M.alloc (|
                              Value.StructTuple
                                "move_core_types::u256::U256"
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::bit::BitOr",
                                      Ty.path "primitive_types::U256",
                                      [ Ty.path "primitive_types::U256" ],
                                      "bitor",
                                      []
                                    |),
                                    [ M.read (| lhs |); M.read (| rhs |) ]
                                  |)
                                ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::bit::BitOr"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *)
        [ ("Output", InstanceField.Ty _Output); ("bitor", InstanceField.Method bitor) ].
  End Impl_core_ops_bit_BitOr_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_bit_BitAnd_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn bitand(self, rhs: U256) -> Self::Output {
            let Self(lhs) = self;
            let Self(rhs) = rhs;
            Self(lhs & rhs)
        }
    *)
    Definition bitand (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::u256::U256",
                        0
                      |) in
                    let lhs := M.copy (| γ0_0 |) in
                    M.match_operator (|
                      rhs,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_core_types::u256::U256",
                                0
                              |) in
                            let rhs := M.copy (| γ0_0 |) in
                            M.alloc (|
                              Value.StructTuple
                                "move_core_types::u256::U256"
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::bit::BitAnd",
                                      Ty.path "primitive_types::U256",
                                      [ Ty.path "primitive_types::U256" ],
                                      "bitand",
                                      []
                                    |),
                                    [ M.read (| lhs |); M.read (| rhs |) ]
                                  |)
                                ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::bit::BitAnd"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *)
        [ ("Output", InstanceField.Ty _Output); ("bitand", InstanceField.Method bitand) ].
  End Impl_core_ops_bit_BitAnd_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_bit_BitXor_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn bitxor(self, rhs: U256) -> Self::Output {
            let Self(lhs) = self;
            let Self(rhs) = rhs;
            Self(lhs ^ rhs)
        }
    *)
    Definition bitxor (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::u256::U256",
                        0
                      |) in
                    let lhs := M.copy (| γ0_0 |) in
                    M.match_operator (|
                      rhs,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_core_types::u256::U256",
                                0
                              |) in
                            let rhs := M.copy (| γ0_0 |) in
                            M.alloc (|
                              Value.StructTuple
                                "move_core_types::u256::U256"
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::bit::BitXor",
                                      Ty.path "primitive_types::U256",
                                      [ Ty.path "primitive_types::U256" ],
                                      "bitxor",
                                      []
                                    |),
                                    [ M.read (| lhs |); M.read (| rhs |) ]
                                  |)
                                ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::bit::BitXor"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *)
        [ ("Output", InstanceField.Ty _Output); ("bitxor", InstanceField.Method bitxor) ].
  End Impl_core_ops_bit_BitXor_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_bit_BitAndAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn bitand_assign(&mut self, rhs: U256) {
            *self = *self & rhs;
        }
    *)
    Definition bitand_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::BitAnd",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "bitand",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::bit::BitAndAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("bitand_assign", InstanceField.Method bitand_assign) ].
  End Impl_core_ops_bit_BitAndAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_Add_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn add(self, rhs: U256) -> Self::Output {
            self.wrapping_add(rhs)
        }
    *)
    Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::u256::U256",
              "wrapping_add",
              []
            |),
            [ M.read (| self |); M.read (| rhs |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Add"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("add", InstanceField.Method add) ].
  End Impl_core_ops_arith_Add_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_AddAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn add_assign(&mut self, rhs: U256) {
            *self = *self + rhs;
        }
    *)
    Definition add_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::Add",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "add",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::AddAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("add_assign", InstanceField.Method add_assign) ].
  End Impl_core_ops_arith_AddAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_Sub_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn sub(self, rhs: U256) -> Self::Output {
            self.wrapping_sub(rhs)
        }
    *)
    Definition sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::u256::U256",
              "wrapping_sub",
              []
            |),
            [ M.read (| self |); M.read (| rhs |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Sub"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("sub", InstanceField.Method sub) ].
  End Impl_core_ops_arith_Sub_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_SubAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn sub_assign(&mut self, rhs: U256) {
            *self = *self - rhs;
        }
    *)
    Definition sub_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::Sub",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "sub",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::SubAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("sub_assign", InstanceField.Method sub_assign) ].
  End Impl_core_ops_arith_SubAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_Mul_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn mul(self, rhs: U256) -> Self::Output {
            self.wrapping_mul(rhs)
        }
    *)
    Definition mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::u256::U256",
              "wrapping_mul",
              []
            |),
            [ M.read (| self |); M.read (| rhs |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Mul"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("mul", InstanceField.Method mul) ].
  End Impl_core_ops_arith_Mul_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_MulAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn mul_assign(&mut self, rhs: U256) {
            *self = *self * rhs;
        }
    *)
    Definition mul_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::Mul",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "mul",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::MulAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("mul_assign", InstanceField.Method mul_assign) ].
  End Impl_core_ops_arith_MulAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_Div_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn div(self, rhs: U256) -> Self::Output {
            Self(self.0 / rhs.0)
        }
    *)
    Definition div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::arith::Div",
                  Ty.path "primitive_types::U256",
                  [ Ty.path "primitive_types::U256" ],
                  "div",
                  []
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| self, "move_core_types::u256::U256", 0 |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| rhs, "move_core_types::u256::U256", 0 |)
                  |)
                ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Div"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("div", InstanceField.Method div) ].
  End Impl_core_ops_arith_Div_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_DivAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn div_assign(&mut self, rhs: U256) {
            *self = *self / rhs;
        }
    *)
    Definition div_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::Div",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "div",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| rhs |) ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::DivAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("div_assign", InstanceField.Method div_assign) ].
  End Impl_core_ops_arith_DivAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_Rem_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Output = Self; *)
    Definition _Output : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn rem(self, rhs: U256) -> Self::Output {
            Self(self.0 % rhs.0)
        }
    *)
    Definition rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::arith::Rem",
                  Ty.path "primitive_types::U256",
                  [ Ty.path "primitive_types::U256" ],
                  "rem",
                  []
                |),
                [
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| self, "move_core_types::u256::U256", 0 |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| rhs, "move_core_types::u256::U256", 0 |)
                  |)
                ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::Rem"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("Output", InstanceField.Ty _Output); ("rem", InstanceField.Method rem) ].
  End Impl_core_ops_arith_Rem_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_core_ops_arith_RemAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn rem_assign(&mut self, rhs: U256) {
            *self = Self(self.0 % rhs.0);
        }
    *)
    Definition rem_assign (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.read (| self |),
                Value.StructTuple
                  "move_core_types::u256::U256"
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::arith::Rem",
                        Ty.path "primitive_types::U256",
                        [ Ty.path "primitive_types::U256" ],
                        "rem",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            M.read (| self |),
                            "move_core_types::u256::U256",
                            0
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            rhs,
                            "move_core_types::u256::U256",
                            0
                          |)
                        |)
                      ]
                    |)
                  ]
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::arith::RemAssign"
        Self
        (* Trait polymorphic types *) [ (* Rhs *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("rem_assign", InstanceField.Method rem_assign) ].
  End Impl_core_ops_arith_RemAssign_move_core_types_u256_U256_for_move_core_types_u256_U256.
  
  Module Impl_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        pub const fn zero() -> Self {
            Self(PrimitiveU256::zero())
        }
    *)
    Definition zero (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "primitive_types::U256", "zero", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_zero : M.IsAssociatedFunction Self "zero" zero.
    
    (*
        pub const fn one() -> Self {
            Self(PrimitiveU256::one())
        }
    *)
    Definition one (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "primitive_types::U256", "one", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_one : M.IsAssociatedFunction Self "one" one.
    
    (*
        pub const fn max_value() -> Self {
            Self(PrimitiveU256::max_value())
        }
    *)
    Definition max_value (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "primitive_types::U256", "max_value", [] |),
                []
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_max_value : M.IsAssociatedFunction Self "max_value" max_value.
    
    (*
        pub fn from_str_radix(src: &str, radix: u32) -> Result<Self, U256FromStrError> {
            PrimitiveU256::from_str_radix(src.trim_start_matches('0'), radix)
                .map(Self)
                .map_err(U256FromStrError)
        }
    *)
    Definition from_str_radix (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ src; radix ] =>
        ltac:(M.monadic
          (let src := M.alloc (| src |) in
          let radix := M.alloc (| radix |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.path "move_core_types::u256::U256"; Ty.path "uint::uint::FromStrRadixErr" ],
              "map_err",
              [
                Ty.path "move_core_types::u256::U256FromStrError";
                Ty.function
                  [ Ty.path "uint::uint::FromStrRadixErr" ]
                  (Ty.path "move_core_types::u256::U256FromStrError")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [ Ty.path "primitive_types::U256"; Ty.path "uint::uint::FromStrRadixErr" ],
                  "map",
                  [
                    Ty.path "move_core_types::u256::U256";
                    Ty.function
                      [ Ty.path "primitive_types::U256" ]
                      (Ty.path "move_core_types::u256::U256")
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "primitive_types::U256",
                      "from_str_radix",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "str",
                          "trim_start_matches",
                          [ Ty.path "char" ]
                        |),
                        [ M.read (| src |); Value.UnicodeChar 48 ]
                      |);
                      M.read (| radix |)
                    ]
                  |);
                  M.constructor_as_closure "move_core_types::u256::U256"
                ]
              |);
              M.constructor_as_closure "move_core_types::u256::U256FromStrError"
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_str_radix :
      M.IsAssociatedFunction Self "from_str_radix" from_str_radix.
    
    (*
        pub fn from_le_bytes(slice: &[u8; U256_NUM_BYTES]) -> Self {
            Self(PrimitiveU256::from_little_endian(slice))
        }
    *)
    Definition from_le_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ slice ] =>
        ltac:(M.monadic
          (let slice := M.alloc (| slice |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "primitive_types::U256",
                  "from_little_endian",
                  []
                |),
                [ M.read (| slice |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_le_bytes :
      M.IsAssociatedFunction Self "from_le_bytes" from_le_bytes.
    
    (*
        pub fn to_le_bytes(self) -> [u8; U256_NUM_BYTES] {
            let mut bytes = [0u8; U256_NUM_BYTES];
            self.0.to_little_endian(&mut bytes);
            bytes
        }
    *)
    Definition to_le_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ bytes :=
              M.alloc (|
                repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "primitive_types::U256",
                    "to_little_endian",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      self,
                      "move_core_types::u256::U256",
                      0
                    |);
                    bytes
                  ]
                |)
              |) in
            bytes
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_le_bytes : M.IsAssociatedFunction Self "to_le_bytes" to_le_bytes.
    
    (*
        pub fn leading_zeros(&self) -> u32 {
            self.0.leading_zeros()
        }
    *)
    Definition leading_zeros (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "primitive_types::U256", "leading_zeros", [] |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_leading_zeros :
      M.IsAssociatedFunction Self "leading_zeros" leading_zeros.
    
    (*
        pub fn unchecked_as_u8(&self) -> u8 {
            self.0.low_u128() as u8
        }
    *)
    Definition unchecked_as_u8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.rust_cast
            (M.call_closure (|
              M.get_associated_function (| Ty.path "primitive_types::U256", "low_u128", [] |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::u256::U256",
                  0
                |)
              ]
            |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unchecked_as_u8 :
      M.IsAssociatedFunction Self "unchecked_as_u8" unchecked_as_u8.
    
    (*
        pub fn unchecked_as_u16(&self) -> u16 {
            self.0.low_u128() as u16
        }
    *)
    Definition unchecked_as_u16 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.rust_cast
            (M.call_closure (|
              M.get_associated_function (| Ty.path "primitive_types::U256", "low_u128", [] |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::u256::U256",
                  0
                |)
              ]
            |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unchecked_as_u16 :
      M.IsAssociatedFunction Self "unchecked_as_u16" unchecked_as_u16.
    
    (*
        pub fn unchecked_as_u32(&self) -> u32 {
            self.0.low_u128() as u32
        }
    *)
    Definition unchecked_as_u32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.rust_cast
            (M.call_closure (|
              M.get_associated_function (| Ty.path "primitive_types::U256", "low_u128", [] |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::u256::U256",
                  0
                |)
              ]
            |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unchecked_as_u32 :
      M.IsAssociatedFunction Self "unchecked_as_u32" unchecked_as_u32.
    
    (*
        pub fn unchecked_as_u64(&self) -> u64 {
            self.0.low_u128() as u64
        }
    *)
    Definition unchecked_as_u64 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.rust_cast
            (M.call_closure (|
              M.get_associated_function (| Ty.path "primitive_types::U256", "low_u128", [] |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::u256::U256",
                  0
                |)
              ]
            |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unchecked_as_u64 :
      M.IsAssociatedFunction Self "unchecked_as_u64" unchecked_as_u64.
    
    (*
        pub fn unchecked_as_u128(&self) -> u128 {
            self.0.low_u128()
        }
    *)
    Definition unchecked_as_u128 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "primitive_types::U256", "low_u128", [] |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::u256::U256",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unchecked_as_u128 :
      M.IsAssociatedFunction Self "unchecked_as_u128" unchecked_as_u128.
    
    (*
        pub fn checked_add(self, rhs: Self) -> Option<Self> {
            self.0.checked_add(rhs.0).map(Self)
        }
    *)
    Definition checked_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "primitive_types::U256" ],
              "map",
              [
                Ty.path "move_core_types::u256::U256";
                Ty.function
                  [ Ty.path "primitive_types::U256" ]
                  (Ty.path "move_core_types::u256::U256")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "primitive_types::U256", "checked_add", [] |),
                [
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| self, "move_core_types::u256::U256", 0 |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| rhs, "move_core_types::u256::U256", 0 |)
                  |)
                ]
              |);
              M.constructor_as_closure "move_core_types::u256::U256"
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_add : M.IsAssociatedFunction Self "checked_add" checked_add.
    
    (*
        pub fn checked_sub(self, rhs: Self) -> Option<Self> {
            self.0.checked_sub(rhs.0).map(Self)
        }
    *)
    Definition checked_sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "primitive_types::U256" ],
              "map",
              [
                Ty.path "move_core_types::u256::U256";
                Ty.function
                  [ Ty.path "primitive_types::U256" ]
                  (Ty.path "move_core_types::u256::U256")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "primitive_types::U256", "checked_sub", [] |),
                [
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| self, "move_core_types::u256::U256", 0 |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| rhs, "move_core_types::u256::U256", 0 |)
                  |)
                ]
              |);
              M.constructor_as_closure "move_core_types::u256::U256"
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_sub : M.IsAssociatedFunction Self "checked_sub" checked_sub.
    
    (*
        pub fn checked_mul(self, rhs: Self) -> Option<Self> {
            self.0.checked_mul(rhs.0).map(Self)
        }
    *)
    Definition checked_mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "primitive_types::U256" ],
              "map",
              [
                Ty.path "move_core_types::u256::U256";
                Ty.function
                  [ Ty.path "primitive_types::U256" ]
                  (Ty.path "move_core_types::u256::U256")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "primitive_types::U256", "checked_mul", [] |),
                [
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| self, "move_core_types::u256::U256", 0 |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| rhs, "move_core_types::u256::U256", 0 |)
                  |)
                ]
              |);
              M.constructor_as_closure "move_core_types::u256::U256"
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_mul : M.IsAssociatedFunction Self "checked_mul" checked_mul.
    
    (*
        pub fn checked_div(self, rhs: Self) -> Option<Self> {
            self.0.checked_div(rhs.0).map(Self)
        }
    *)
    Definition checked_div (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "primitive_types::U256" ],
              "map",
              [
                Ty.path "move_core_types::u256::U256";
                Ty.function
                  [ Ty.path "primitive_types::U256" ]
                  (Ty.path "move_core_types::u256::U256")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "primitive_types::U256", "checked_div", [] |),
                [
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| self, "move_core_types::u256::U256", 0 |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| rhs, "move_core_types::u256::U256", 0 |)
                  |)
                ]
              |);
              M.constructor_as_closure "move_core_types::u256::U256"
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_div : M.IsAssociatedFunction Self "checked_div" checked_div.
    
    (*
        pub fn checked_rem(self, rhs: Self) -> Option<Self> {
            self.0.checked_rem(rhs.0).map(Self)
        }
    *)
    Definition checked_rem (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "primitive_types::U256" ],
              "map",
              [
                Ty.path "move_core_types::u256::U256";
                Ty.function
                  [ Ty.path "primitive_types::U256" ]
                  (Ty.path "move_core_types::u256::U256")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (| Ty.path "primitive_types::U256", "checked_rem", [] |),
                [
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| self, "move_core_types::u256::U256", 0 |)
                  |);
                  M.read (|
                    M.SubPointer.get_struct_tuple_field (| rhs, "move_core_types::u256::U256", 0 |)
                  |)
                ]
              |);
              M.constructor_as_closure "move_core_types::u256::U256"
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_rem : M.IsAssociatedFunction Self "checked_rem" checked_rem.
    
    (*
        pub fn checked_shl(self, rhs: u32) -> Option<Self> {
            if rhs >= U256_NUM_BITS as u32 {
                return None;
            }
            Some(Self(self.0.shl(rhs)))
        }
    *)
    Definition checked_shl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.ge (|
                                  M.read (| rhs |),
                                  M.rust_cast
                                    (M.read (|
                                      M.get_constant (| "move_core_types::u256::U256_NUM_BITS" |)
                                    |))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (|
                  Value.StructTuple
                    "core::option::Option::Some"
                    [
                      Value.StructTuple
                        "move_core_types::u256::U256"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::bit::Shl",
                              Ty.path "primitive_types::U256",
                              [ Ty.path "u32" ],
                              "shl",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_tuple_field (|
                                  self,
                                  "move_core_types::u256::U256",
                                  0
                                |)
                              |);
                              M.read (| rhs |)
                            ]
                          |)
                        ]
                    ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_shl : M.IsAssociatedFunction Self "checked_shl" checked_shl.
    
    (*
        pub fn checked_shr(self, rhs: u32) -> Option<Self> {
            if rhs >= U256_NUM_BITS as u32 {
                return None;
            }
            Some(Self(self.0.shr(rhs)))
        }
    *)
    Definition checked_shr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.ge (|
                                  M.read (| rhs |),
                                  M.rust_cast
                                    (M.read (|
                                      M.get_constant (| "move_core_types::u256::U256_NUM_BITS" |)
                                    |))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (| Value.StructTuple "core::option::Option::None" [] |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (|
                  Value.StructTuple
                    "core::option::Option::Some"
                    [
                      Value.StructTuple
                        "move_core_types::u256::U256"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::bit::Shr",
                              Ty.path "primitive_types::U256",
                              [ Ty.path "u32" ],
                              "shr",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_tuple_field (|
                                  self,
                                  "move_core_types::u256::U256",
                                  0
                                |)
                              |);
                              M.read (| rhs |)
                            ]
                          |)
                        ]
                    ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_checked_shr : M.IsAssociatedFunction Self "checked_shr" checked_shr.
    
    (*
        pub fn down_cast_lossy<T: std::convert::TryFrom<u128>>(self) -> T {
            // Size of this type
            let type_size = size_of::<T>();
            // Maximum value for this type
            let max_val: u128 = if type_size < 16 {
                (1u128 << (NUM_BITS_PER_BYTE * type_size)) - 1u128
            } else {
                u128::MAX
            };
            // This should never fail
            match T::try_from(self.0.low_u128() & max_val) {
                Ok(w) => w,
                Err(_) => panic!("Fatal! Downcast failed"),
            }
        }
    *)
    Definition down_cast_lossy (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ type_size :=
              M.alloc (|
                M.call_closure (| M.get_function (| "core::mem::size_of", [ T ] |), [] |)
              |) in
            let~ max_val :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (|
                                M.read (| type_size |),
                                Value.Integer IntegerKind.Usize 16
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          BinOp.Wrap.sub (|
                            BinOp.Wrap.shl (|
                              Value.Integer IntegerKind.U128 1,
                              BinOp.Wrap.mul (|
                                M.read (|
                                  M.get_constant (| "move_core_types::u256::NUM_BITS_PER_BYTE" |)
                                |),
                                M.read (| type_size |)
                              |)
                            |),
                            Value.Integer IntegerKind.U128 1
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.get_constant (| "core::num::MAX" |)))
                  ]
                |)
              |) in
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::TryFrom",
                    T,
                    [ Ty.path "u128" ],
                    "try_from",
                    []
                  |),
                  [
                    BinOp.bit_and
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "primitive_types::U256",
                          "low_u128",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_tuple_field (|
                            self,
                            "move_core_types::u256::U256",
                            0
                          |)
                        ]
                      |))
                      (M.read (| max_val |))
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let w := M.copy (| γ0_0 |) in
                    w));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Err", 0 |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_fmt", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_const",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array [ M.read (| Value.String "Fatal! Downcast failed" |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_down_cast_lossy :
      M.IsAssociatedFunction Self "down_cast_lossy" down_cast_lossy.
    
    (*
        pub fn wrapping_add(self, rhs: Self) -> Self {
            Self(self.0.overflowing_add(rhs.0).0)
        }
    *)
    Definition wrapping_add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.read (|
                M.SubPointer.get_tuple_field (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "primitive_types::U256",
                        "overflowing_add",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            self,
                            "move_core_types::u256::U256",
                            0
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            rhs,
                            "move_core_types::u256::U256",
                            0
                          |)
                        |)
                      ]
                    |)
                  |),
                  0
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_wrapping_add : M.IsAssociatedFunction Self "wrapping_add" wrapping_add.
    
    (*
        pub fn wrapping_sub(self, rhs: Self) -> Self {
            Self(self.0.overflowing_sub(rhs.0).0)
        }
    *)
    Definition wrapping_sub (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.read (|
                M.SubPointer.get_tuple_field (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "primitive_types::U256",
                        "overflowing_sub",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            self,
                            "move_core_types::u256::U256",
                            0
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            rhs,
                            "move_core_types::u256::U256",
                            0
                          |)
                        |)
                      ]
                    |)
                  |),
                  0
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_wrapping_sub : M.IsAssociatedFunction Self "wrapping_sub" wrapping_sub.
    
    (*
        pub fn wrapping_mul(self, rhs: Self) -> Self {
            Self(self.0.overflowing_mul(rhs.0).0)
        }
    *)
    Definition wrapping_mul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; rhs ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rhs := M.alloc (| rhs |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.read (|
                M.SubPointer.get_tuple_field (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "primitive_types::U256",
                        "overflowing_mul",
                        []
                      |),
                      [
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            self,
                            "move_core_types::u256::U256",
                            0
                          |)
                        |);
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            rhs,
                            "move_core_types::u256::U256",
                            0
                          |)
                        |)
                      ]
                    |)
                  |),
                  0
                |)
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_wrapping_mul : M.IsAssociatedFunction Self "wrapping_mul" wrapping_mul.
    
    (*
        fn wmul(self, b: Self) -> (Self, Self) {
            let half = 128;
            #[allow(non_snake_case)]
            let LOWER_MASK: U256 = Self::max_value() >> half;
    
            let mut low = (self & LOWER_MASK).wrapping_mul(b & LOWER_MASK);
            let mut t = low >> half;
            low &= LOWER_MASK;
            t += (self >> half).wrapping_mul(b & LOWER_MASK);
            low += (t & LOWER_MASK) << half;
            let mut high = t >> half;
            t = low >> half;
            low &= LOWER_MASK;
            t += (b >> half).wrapping_mul(self & LOWER_MASK);
            low += (t & LOWER_MASK) << half;
            high += t >> half;
            high += (self >> half).wrapping_mul(b >> half);
    
            (high, low)
        }
    *)
    Definition wmul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; b ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let b := M.alloc (| b |) in
          M.read (|
            let~ half := M.alloc (| Value.Integer IntegerKind.U8 128 |) in
            let~ value_LOWER_MASK :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::Shr",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "u8" ],
                    "shr",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_core_types::u256::U256",
                        "max_value",
                        []
                      |),
                      []
                    |);
                    M.read (| half |)
                  ]
                |)
              |) in
            let~ low :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_core_types::u256::U256",
                    "wrapping_mul",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::bit::BitAnd",
                        Ty.path "move_core_types::u256::U256",
                        [ Ty.path "move_core_types::u256::U256" ],
                        "bitand",
                        []
                      |),
                      [ M.read (| self |); M.read (| value_LOWER_MASK |) ]
                    |);
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::bit::BitAnd",
                        Ty.path "move_core_types::u256::U256",
                        [ Ty.path "move_core_types::u256::U256" ],
                        "bitand",
                        []
                      |),
                      [ M.read (| b |); M.read (| value_LOWER_MASK |) ]
                    |)
                  ]
                |)
              |) in
            let~ t :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::Shr",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "u8" ],
                    "shr",
                    []
                  |),
                  [ M.read (| low |); M.read (| half |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::BitAndAssign",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "bitand_assign",
                    []
                  |),
                  [ low; M.read (| value_LOWER_MASK |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::AddAssign",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "add_assign",
                    []
                  |),
                  [
                    t;
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_core_types::u256::U256",
                        "wrapping_mul",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::Shr",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "u8" ],
                            "shr",
                            []
                          |),
                          [ M.read (| self |); M.read (| half |) ]
                        |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::BitAnd",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "move_core_types::u256::U256" ],
                            "bitand",
                            []
                          |),
                          [ M.read (| b |); M.read (| value_LOWER_MASK |) ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::AddAssign",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "add_assign",
                    []
                  |),
                  [
                    low;
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::bit::Shl",
                        Ty.path "move_core_types::u256::U256",
                        [ Ty.path "u8" ],
                        "shl",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::BitAnd",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "move_core_types::u256::U256" ],
                            "bitand",
                            []
                          |),
                          [ M.read (| t |); M.read (| value_LOWER_MASK |) ]
                        |);
                        M.read (| half |)
                      ]
                    |)
                  ]
                |)
              |) in
            let~ high :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::Shr",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "u8" ],
                    "shr",
                    []
                  |),
                  [ M.read (| t |); M.read (| half |) ]
                |)
              |) in
            let~ _ :=
              M.write (|
                t,
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::Shr",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "u8" ],
                    "shr",
                    []
                  |),
                  [ M.read (| low |); M.read (| half |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::BitAndAssign",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "bitand_assign",
                    []
                  |),
                  [ low; M.read (| value_LOWER_MASK |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::AddAssign",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "add_assign",
                    []
                  |),
                  [
                    t;
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_core_types::u256::U256",
                        "wrapping_mul",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::Shr",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "u8" ],
                            "shr",
                            []
                          |),
                          [ M.read (| b |); M.read (| half |) ]
                        |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::BitAnd",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "move_core_types::u256::U256" ],
                            "bitand",
                            []
                          |),
                          [ M.read (| self |); M.read (| value_LOWER_MASK |) ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::AddAssign",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "add_assign",
                    []
                  |),
                  [
                    low;
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::bit::Shl",
                        Ty.path "move_core_types::u256::U256",
                        [ Ty.path "u8" ],
                        "shl",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::BitAnd",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "move_core_types::u256::U256" ],
                            "bitand",
                            []
                          |),
                          [ M.read (| t |); M.read (| value_LOWER_MASK |) ]
                        |);
                        M.read (| half |)
                      ]
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::AddAssign",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "add_assign",
                    []
                  |),
                  [
                    high;
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::bit::Shr",
                        Ty.path "move_core_types::u256::U256",
                        [ Ty.path "u8" ],
                        "shr",
                        []
                      |),
                      [ M.read (| t |); M.read (| half |) ]
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::AddAssign",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "add_assign",
                    []
                  |),
                  [
                    high;
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_core_types::u256::U256",
                        "wrapping_mul",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::Shr",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "u8" ],
                            "shr",
                            []
                          |),
                          [ M.read (| self |); M.read (| half |) ]
                        |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::Shr",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "u8" ],
                            "shr",
                            []
                          |),
                          [ M.read (| b |); M.read (| half |) ]
                        |)
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [ M.read (| high |); M.read (| low |) ] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_wmul : M.IsAssociatedFunction Self "wmul" wmul.
  End Impl_move_core_types_u256_U256.
  
  Module Impl_core_convert_From_u8_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn from(n: u8) -> Self {
            U256(PrimitiveU256::from(n))
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "primitive_types::U256",
                  [ Ty.path "u8" ],
                  "from",
                  []
                |),
                [ M.read (| n |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "u8" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_u8_for_move_core_types_u256_U256.
  
  Module Impl_core_convert_From_u16_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn from(n: u16) -> Self {
            U256(PrimitiveU256::from(n))
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "primitive_types::U256",
                  [ Ty.path "u16" ],
                  "from",
                  []
                |),
                [ M.read (| n |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "u16" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_u16_for_move_core_types_u256_U256.
  
  Module Impl_core_convert_From_u32_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn from(n: u32) -> Self {
            U256(PrimitiveU256::from(n))
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "primitive_types::U256",
                  [ Ty.path "u32" ],
                  "from",
                  []
                |),
                [ M.read (| n |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "u32" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_u32_for_move_core_types_u256_U256.
  
  Module Impl_core_convert_From_u64_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn from(n: u64) -> Self {
            U256(PrimitiveU256::from(n))
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "primitive_types::U256",
                  [ Ty.path "u64" ],
                  "from",
                  []
                |),
                [ M.read (| n |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "u64" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_u64_for_move_core_types_u256_U256.
  
  Module Impl_core_convert_From_u128_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn from(n: u128) -> Self {
            U256(PrimitiveU256::from(n))
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          Value.StructTuple
            "move_core_types::u256::U256"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "primitive_types::U256",
                  [ Ty.path "u128" ],
                  "from",
                  []
                |),
                [ M.read (| n |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "u128" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_u128_for_move_core_types_u256_U256.
  
  Module Impl_core_convert_From_ref__move_core_types_u256_U256_for_num_bigint_bigint_BigInt.
    Definition Self : Ty.t := Ty.path "num_bigint::bigint::BigInt".
    
    (*
        fn from(n: &U256) -> Self {
            BigInt::from_bytes_le(Sign::Plus, &n.to_le_bytes())
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "num_bigint::bigint::BigInt",
              "from_bytes_le",
              []
            |),
            [
              Value.StructTuple "num_bigint::bigint::Sign::Plus" [];
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_core_types::u256::U256",
                    "to_le_bytes",
                    []
                  |),
                  [ M.read (| M.read (| n |) |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "&") [] [ Ty.path "move_core_types::u256::U256" ] ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_ref__move_core_types_u256_U256_for_num_bigint_bigint_BigInt.
  
  Module Impl_core_convert_From_ref__move_core_types_u256_U256_for_ethnum_uint_U256.
    Definition Self : Ty.t := Ty.path "ethnum::uint::U256".
    
    (*
        fn from(n: &U256) -> EthnumU256 {
            // TODO (ade): use better solution for conversion
            // Currently using str because EthnumU256 can be little or big endian
            let num_str = format!("{:X}", n.0);
            // TODO (ade): remove expect()
            EthnumU256::from_str_radix(&num_str, 16).expect("Cannot convert to U256")
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          M.read (|
            let~ num_str :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::hint::must_use", [ Ty.path "alloc::string::String" ] |),
                  [
                    M.read (|
                      let~ res :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_function (| "alloc::fmt::format", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_v1",
                                  []
                                |),
                                [
                                  M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "core::fmt::rt::Argument",
                                            "new_upper_hex",
                                            [ Ty.path "primitive_types::U256" ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_tuple_field (|
                                              M.read (| n |),
                                              "move_core_types::u256::U256",
                                              0
                                            |)
                                          ]
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |) in
                      res
                    |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [ Ty.path "ethnum::uint::U256"; Ty.path "core::num::error::ParseIntError" ],
                  "expect",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "ethnum::uint::U256",
                      "from_str_radix",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::deref::Deref",
                          Ty.path "alloc::string::String",
                          [],
                          "deref",
                          []
                        |),
                        [ num_str ]
                      |);
                      Value.Integer IntegerKind.U32 16
                    ]
                  |);
                  M.read (| Value.String "Cannot convert to U256" |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "&") [] [ Ty.path "move_core_types::u256::U256" ] ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_ref__move_core_types_u256_U256_for_ethnum_uint_U256.
  
  Module Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u8.
    Definition Self : Ty.t := Ty.path "u8".
    
    (*     type Error = U256CastError; *)
    Definition _Error : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    (*
        fn try_from(n: U256) -> Result<Self, Self::Error> {
            let n = n.0.low_u64();
            if n > u8::MAX as u64 {
                Err(U256CastError::new(n, U256CastErrorKind::TooLargeForU8))
            } else {
                Ok(n as u8)
            }
        }
    *)
    Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          M.read (|
            let~ n :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "primitive_types::U256", "low_u64", [] |),
                  [ M.SubPointer.get_struct_tuple_field (| n, "move_core_types::u256::U256", 0 |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.gt (|
                            M.read (| n |),
                            M.rust_cast (M.read (| M.get_constant (| "core::num::MAX" |) |))
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::u256::U256CastError",
                              "new",
                              [ Ty.path "u64" ]
                            |),
                            [
                              M.read (| n |);
                              Value.StructTuple
                                "move_core_types::u256::U256CastErrorKind::TooLargeForU8"
                                []
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple "core::result::Result::Ok" [ M.rust_cast (M.read (| n |)) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u8.
  
  Module Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u16.
    Definition Self : Ty.t := Ty.path "u16".
    
    (*     type Error = U256CastError; *)
    Definition _Error : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    (*
        fn try_from(n: U256) -> Result<Self, Self::Error> {
            let n = n.0.low_u64();
            if n > u16::MAX as u64 {
                Err(U256CastError::new(n, U256CastErrorKind::TooLargeForU16))
            } else {
                Ok(n as u16)
            }
        }
    *)
    Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          M.read (|
            let~ n :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "primitive_types::U256", "low_u64", [] |),
                  [ M.SubPointer.get_struct_tuple_field (| n, "move_core_types::u256::U256", 0 |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.gt (|
                            M.read (| n |),
                            M.rust_cast (M.read (| M.get_constant (| "core::num::MAX" |) |))
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::u256::U256CastError",
                              "new",
                              [ Ty.path "u64" ]
                            |),
                            [
                              M.read (| n |);
                              Value.StructTuple
                                "move_core_types::u256::U256CastErrorKind::TooLargeForU16"
                                []
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple "core::result::Result::Ok" [ M.rust_cast (M.read (| n |)) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u16.
  
  Module Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u32.
    Definition Self : Ty.t := Ty.path "u32".
    
    (*     type Error = U256CastError; *)
    Definition _Error : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    (*
        fn try_from(n: U256) -> Result<Self, Self::Error> {
            let n = n.0.low_u64();
            if n > u32::MAX as u64 {
                Err(U256CastError::new(n, U256CastErrorKind::TooLargeForU32))
            } else {
                Ok(n as u32)
            }
        }
    *)
    Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          M.read (|
            let~ n :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "primitive_types::U256", "low_u64", [] |),
                  [ M.SubPointer.get_struct_tuple_field (| n, "move_core_types::u256::U256", 0 |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.gt (|
                            M.read (| n |),
                            M.rust_cast (M.read (| M.get_constant (| "core::num::MAX" |) |))
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::u256::U256CastError",
                              "new",
                              [ Ty.path "u64" ]
                            |),
                            [
                              M.read (| n |);
                              Value.StructTuple
                                "move_core_types::u256::U256CastErrorKind::TooLargeForU32"
                                []
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple "core::result::Result::Ok" [ M.rust_cast (M.read (| n |)) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u32.
  
  Module Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u64.
    Definition Self : Ty.t := Ty.path "u64".
    
    (*     type Error = U256CastError; *)
    Definition _Error : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    (*
        fn try_from(n: U256) -> Result<Self, Self::Error> {
            let n = n.0.low_u128();
            if n > u64::MAX as u128 {
                Err(U256CastError::new(n, U256CastErrorKind::TooLargeForU64))
            } else {
                Ok(n as u64)
            }
        }
    *)
    Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          M.read (|
            let~ n :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "primitive_types::U256", "low_u128", [] |),
                  [ M.SubPointer.get_struct_tuple_field (| n, "move_core_types::u256::U256", 0 |) ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.gt (|
                            M.read (| n |),
                            M.rust_cast (M.read (| M.get_constant (| "core::num::MAX" |) |))
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::u256::U256CastError",
                              "new",
                              [ Ty.path "u128" ]
                            |),
                            [
                              M.read (| n |);
                              Value.StructTuple
                                "move_core_types::u256::U256CastErrorKind::TooLargeForU64"
                                []
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple "core::result::Result::Ok" [ M.rust_cast (M.read (| n |)) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u64.
  
  Module Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u128.
    Definition Self : Ty.t := Ty.path "u128".
    
    (*     type Error = U256CastError; *)
    Definition _Error : Ty.t := Ty.path "move_core_types::u256::U256CastError".
    
    (*
        fn try_from(n: U256) -> Result<Self, Self::Error> {
            if n > U256::from(u128::MAX) {
                Err(U256CastError::new(n, U256CastErrorKind::TooLargeForU128))
            } else {
                Ok(n.0.low_u128())
            }
        }
    *)
    Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ n ] =>
        ltac:(M.monadic
          (let n := M.alloc (| n |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialOrd",
                              Ty.path "move_core_types::u256::U256",
                              [ Ty.path "move_core_types::u256::U256" ],
                              "gt",
                              []
                            |),
                            [
                              n;
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::convert::From",
                                    Ty.path "move_core_types::u256::U256",
                                    [ Ty.path "u128" ],
                                    "from",
                                    []
                                  |),
                                  [ M.read (| M.get_constant (| "core::num::MAX" |) |) ]
                                |)
                              |)
                            ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::u256::U256CastError",
                              "new",
                              [ Ty.path "move_core_types::u256::U256" ]
                            |),
                            [
                              M.read (| n |);
                              Value.StructTuple
                                "move_core_types::u256::U256CastErrorKind::TooLargeForU128"
                                []
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Ok"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "primitive_types::U256",
                              "low_u128",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_tuple_field (|
                                n,
                                "move_core_types::u256::U256",
                                0
                              |)
                            ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_move_core_types_u256_U256_for_u128.
  
  Module Impl_rand_distributions_distribution_Distribution_move_core_types_u256_U256_for_rand_distributions_Standard.
    Definition Self : Ty.t := Ty.path "rand::distributions::Standard".
    
    (*
        fn sample<R: Rng + ?Sized>(&self, rng: &mut R) -> U256 {
            let mut dest = [0; U256_NUM_BYTES];
            rng.fill_bytes(&mut dest);
            U256::from_le_bytes(&dest)
        }
    *)
    Definition sample (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ R ], [ self; rng ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rng := M.alloc (| rng |) in
          M.read (|
            let~ dest :=
              M.alloc (|
                repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "rand_core::RngCore", R, [], "fill_bytes", [] |),
                  [ M.read (| rng |); dest ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_core_types::u256::U256",
                  "from_le_bytes",
                  []
                |),
                [ dest ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "rand::distributions::distribution::Distribution"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "move_core_types::u256::U256" ]
        (* Instance *) [ ("sample", InstanceField.Method sample) ].
  End Impl_rand_distributions_distribution_Distribution_move_core_types_u256_U256_for_rand_distributions_Standard.
  
  (* StructRecord
    {
      name := "UniformU256";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("low", Ty.path "move_core_types::u256::U256");
          ("range", Ty.path "move_core_types::u256::U256");
          ("z", Ty.path "move_core_types::u256::U256")
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_move_core_types_u256_UniformU256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::UniformU256".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_move_core_types_u256_UniformU256.
  
  Module Impl_core_marker_Copy_for_move_core_types_u256_UniformU256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::UniformU256".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_core_types_u256_UniformU256.
  
  Module Impl_core_fmt_Debug_for_move_core_types_u256_UniformU256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::UniformU256".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field3_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "UniformU256" |);
              M.read (| Value.String "low" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_core_types::u256::UniformU256",
                "low"
              |);
              M.read (| Value.String "range" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_core_types::u256::UniformU256",
                "range"
              |);
              M.read (| Value.String "z" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_core_types::u256::UniformU256",
                  "z"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_u256_UniformU256.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_u256_UniformU256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::UniformU256".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_u256_UniformU256.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_u256_UniformU256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::UniformU256".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            LogicalOp.and (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.path "move_core_types::u256::U256",
                  [ Ty.path "move_core_types::u256::U256" ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_core_types::u256::UniformU256",
                    "low"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "move_core_types::u256::UniformU256",
                    "low"
                  |)
                ]
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "move_core_types::u256::U256",
                    [ Ty.path "move_core_types::u256::U256" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_core_types::u256::UniformU256",
                      "range"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "move_core_types::u256::UniformU256",
                      "range"
                    |)
                  ]
                |)))
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.path "move_core_types::u256::U256",
                  [ Ty.path "move_core_types::u256::U256" ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_core_types::u256::UniformU256",
                    "z"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "move_core_types::u256::UniformU256",
                    "z"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_move_core_types_u256_UniformU256.
  
  Module Impl_core_cmp_Eq_for_move_core_types_u256_UniformU256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::UniformU256".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_move_core_types_u256_UniformU256.
  
  Module Impl_rand_distributions_uniform_SampleUniform_for_move_core_types_u256_U256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*     type Sampler = UniformU256; *)
    Definition _Sampler : Ty.t := Ty.path "move_core_types::u256::UniformU256".
    
    Axiom Implements :
      M.IsTraitInstance
        "rand::distributions::uniform::SampleUniform"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("Sampler", InstanceField.Ty _Sampler) ].
  End Impl_rand_distributions_uniform_SampleUniform_for_move_core_types_u256_U256.
  
  Module Impl_rand_distributions_uniform_UniformSampler_for_move_core_types_u256_UniformU256.
    Definition Self : Ty.t := Ty.path "move_core_types::u256::UniformU256".
    
    (*     type X = U256; *)
    Definition _X : Ty.t := Ty.path "move_core_types::u256::U256".
    
    (*
        fn new<B1, B2>(low: B1, high: B2) -> Self
        where
            B1: rand::distributions::uniform::SampleBorrow<Self::X> + Sized,
            B2: rand::distributions::uniform::SampleBorrow<Self::X> + Sized,
        {
            let low = *low.borrow();
            let high = *high.borrow();
            assert!(low < high, "Uniform::new called with `low >= high`");
            UniformSampler::new_inclusive(low, high - U256::one())
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ B1; B2 ], [ low; high ] =>
        ltac:(M.monadic
          (let low := M.alloc (| low |) in
          let high := M.alloc (| high |) in
          M.read (|
            let~ low :=
              M.copy (|
                M.call_closure (|
                  M.get_trait_method (|
                    "rand::distributions::uniform::SampleBorrow",
                    B1,
                    [ Ty.path "move_core_types::u256::U256" ],
                    "borrow",
                    []
                  |),
                  [ low ]
                |)
              |) in
            let~ high :=
              M.copy (|
                M.call_closure (|
                  M.get_trait_method (|
                    "rand::distributions::uniform::SampleBorrow",
                    B2,
                    [ Ty.path "move_core_types::u256::U256" ],
                    "borrow",
                    []
                  |),
                  [ high ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialOrd",
                                  Ty.path "move_core_types::u256::U256",
                                  [ Ty.path "move_core_types::u256::U256" ],
                                  "lt",
                                  []
                                |),
                                [ low; high ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String "Uniform::new called with `low >= high`"
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "rand::distributions::uniform::UniformSampler",
                  Ty.path "move_core_types::u256::UniformU256",
                  [],
                  "new_inclusive",
                  [ Ty.path "move_core_types::u256::U256"; Ty.path "move_core_types::u256::U256" ]
                |),
                [
                  M.read (| low |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::arith::Sub",
                      Ty.path "move_core_types::u256::U256",
                      [ Ty.path "move_core_types::u256::U256" ],
                      "sub",
                      []
                    |),
                    [
                      M.read (| high |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_core_types::u256::U256",
                          "one",
                          []
                        |),
                        []
                      |)
                    ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn new_inclusive<B1, B2>(low: B1, high: B2) -> Self
        where
            B1: rand::distributions::uniform::SampleBorrow<Self::X> + Sized,
            B2: rand::distributions::uniform::SampleBorrow<Self::X> + Sized,
        {
            let low = *low.borrow();
            let high = *high.borrow();
            assert!(
                low <= high,
                "Uniform::new_inclusive called with `low > high`"
            );
            let unsigned_max = U256::max_value();
    
            let range = high.wrapping_sub(low).wrapping_add(U256::one());
    
            let ints_to_reject = if range > U256::zero() {
                (unsigned_max - range) + U256::one() % range
            } else {
                U256::zero()
            };
    
            UniformU256 {
                low,
                range,
                z: ints_to_reject,
            }
        }
    *)
    Definition new_inclusive (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ B1; B2 ], [ low; high ] =>
        ltac:(M.monadic
          (let low := M.alloc (| low |) in
          let high := M.alloc (| high |) in
          M.read (|
            let~ low :=
              M.copy (|
                M.call_closure (|
                  M.get_trait_method (|
                    "rand::distributions::uniform::SampleBorrow",
                    B1,
                    [ Ty.path "move_core_types::u256::U256" ],
                    "borrow",
                    []
                  |),
                  [ low ]
                |)
              |) in
            let~ high :=
              M.copy (|
                M.call_closure (|
                  M.get_trait_method (|
                    "rand::distributions::uniform::SampleBorrow",
                    B2,
                    [ Ty.path "move_core_types::u256::U256" ],
                    "borrow",
                    []
                  |),
                  [ high ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialOrd",
                                  Ty.path "move_core_types::u256::U256",
                                  [ Ty.path "move_core_types::u256::U256" ],
                                  "le",
                                  []
                                |),
                                [ low; high ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String
                                            "Uniform::new_inclusive called with `low > high`"
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ unsigned_max :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_core_types::u256::U256",
                    "max_value",
                    []
                  |),
                  []
                |)
              |) in
            let~ range :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_core_types::u256::U256",
                    "wrapping_add",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_core_types::u256::U256",
                        "wrapping_sub",
                        []
                      |),
                      [ M.read (| high |); M.read (| low |) ]
                    |);
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_core_types::u256::U256",
                        "one",
                        []
                      |),
                      []
                    |)
                  ]
                |)
              |) in
            let~ ints_to_reject :=
              M.copy (|
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialOrd",
                                  Ty.path "move_core_types::u256::U256",
                                  [ Ty.path "move_core_types::u256::U256" ],
                                  "gt",
                                  []
                                |),
                                [
                                  range;
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_core_types::u256::U256",
                                        "zero",
                                        []
                                      |),
                                      []
                                    |)
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::arith::Add",
                              Ty.path "move_core_types::u256::U256",
                              [ Ty.path "move_core_types::u256::U256" ],
                              "add",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::arith::Sub",
                                  Ty.path "move_core_types::u256::U256",
                                  [ Ty.path "move_core_types::u256::U256" ],
                                  "sub",
                                  []
                                |),
                                [ M.read (| unsigned_max |); M.read (| range |) ]
                              |);
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::arith::Rem",
                                  Ty.path "move_core_types::u256::U256",
                                  [ Ty.path "move_core_types::u256::U256" ],
                                  "rem",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_core_types::u256::U256",
                                      "one",
                                      []
                                    |),
                                    []
                                  |);
                                  M.read (| range |)
                                ]
                              |)
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::u256::U256",
                              "zero",
                              []
                            |),
                            []
                          |)
                        |)))
                  ]
                |)
              |) in
            M.alloc (|
              Value.StructRecord
                "move_core_types::u256::UniformU256"
                [
                  ("low", M.read (| low |));
                  ("range", M.read (| range |));
                  ("z", M.read (| ints_to_reject |))
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn sample<R: rand::Rng + ?Sized>(&self, rng: &mut R) -> Self::X {
            let range = self.range;
            if range > U256::zero() {
                let unsigned_max = U256::max_value();
                let zone = unsigned_max - self.z;
                loop {
                    let v: U256 = rng.gen();
                    let (hi, lo) = v.wmul(range);
                    if lo <= zone {
                        return self.low.wrapping_add(hi);
                    }
                }
            } else {
                // Sample from the entire integer range.
                rng.gen()
            }
        }
    *)
    Definition sample (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ R ], [ self; rng ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let rng := M.alloc (| rng |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ range :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_core_types::u256::UniformU256",
                      "range"
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialOrd",
                                  Ty.path "move_core_types::u256::U256",
                                  [ Ty.path "move_core_types::u256::U256" ],
                                  "gt",
                                  []
                                |),
                                [
                                  range;
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "move_core_types::u256::U256",
                                        "zero",
                                        []
                                      |),
                                      []
                                    |)
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ unsigned_max :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_core_types::u256::U256",
                                "max_value",
                                []
                              |),
                              []
                            |)
                          |) in
                        let~ zone :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::arith::Sub",
                                Ty.path "move_core_types::u256::U256",
                                [ Ty.path "move_core_types::u256::U256" ],
                                "sub",
                                []
                              |),
                              [
                                M.read (| unsigned_max |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "move_core_types::u256::UniformU256",
                                    "z"
                                  |)
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ v :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "rand::rng::Rng",
                                          R,
                                          [],
                                          "gen",
                                          [ Ty.path "move_core_types::u256::U256" ]
                                        |),
                                        [ M.read (| rng |) ]
                                      |)
                                    |) in
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_core_types::u256::U256",
                                          "wmul",
                                          []
                                        |),
                                        [ M.read (| v |); M.read (| range |) ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                          let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                          let hi := M.copy (| γ0_0 |) in
                                          let lo := M.copy (| γ0_1 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::cmp::PartialOrd",
                                                            Ty.path "move_core_types::u256::U256",
                                                            [ Ty.path "move_core_types::u256::U256"
                                                            ],
                                                            "le",
                                                            []
                                                          |),
                                                          [ lo; zone ]
                                                        |)
                                                      |)) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "move_core_types::u256::U256",
                                                              "wrapping_add",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "move_core_types::u256::UniformU256",
                                                                  "low"
                                                                |)
                                                              |);
                                                              M.read (| hi |)
                                                            ]
                                                          |)
                                                        |)
                                                      |)
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |)))
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "rand::rng::Rng",
                              R,
                              [],
                              "gen",
                              [ Ty.path "move_core_types::u256::U256" ]
                            |),
                            [ M.read (| rng |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn sample_single<R: rand::Rng + ?Sized, B1, B2>(low: B1, high: B2, rng: &mut R) -> Self::X
        where
            B1: rand::distributions::uniform::SampleBorrow<Self::X> + Sized,
            B2: rand::distributions::uniform::SampleBorrow<Self::X> + Sized,
        {
            let low = *low.borrow();
            let high = *high.borrow();
            assert!(low < high, "UniformSampler::sample_single: low >= high");
            Self::sample_single_inclusive(low, high - U256::one(), rng)
        }
    *)
    Definition sample_single (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ R; B1; B2 ], [ low; high; rng ] =>
        ltac:(M.monadic
          (let low := M.alloc (| low |) in
          let high := M.alloc (| high |) in
          let rng := M.alloc (| rng |) in
          M.read (|
            let~ low :=
              M.copy (|
                M.call_closure (|
                  M.get_trait_method (|
                    "rand::distributions::uniform::SampleBorrow",
                    B1,
                    [ Ty.path "move_core_types::u256::U256" ],
                    "borrow",
                    []
                  |),
                  [ low ]
                |)
              |) in
            let~ high :=
              M.copy (|
                M.call_closure (|
                  M.get_trait_method (|
                    "rand::distributions::uniform::SampleBorrow",
                    B2,
                    [ Ty.path "move_core_types::u256::U256" ],
                    "borrow",
                    []
                  |),
                  [ high ]
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            UnOp.not (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialOrd",
                                  Ty.path "move_core_types::u256::U256",
                                  [ Ty.path "move_core_types::u256::U256" ],
                                  "lt",
                                  []
                                |),
                                [ low; high ]
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        M.never_to_any (|
                          M.call_closure (|
                            M.get_function (| "core::panicking::panic_fmt", [] |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::Arguments",
                                  "new_const",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    Value.Array
                                      [
                                        M.read (|
                                          Value.String "UniformSampler::sample_single: low >= high"
                                        |)
                                      ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "rand::distributions::uniform::UniformSampler",
                  Ty.path "move_core_types::u256::UniformU256",
                  [],
                  "sample_single_inclusive",
                  [ R; Ty.path "move_core_types::u256::U256"; Ty.path "move_core_types::u256::U256"
                  ]
                |),
                [
                  M.read (| low |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::arith::Sub",
                      Ty.path "move_core_types::u256::U256",
                      [ Ty.path "move_core_types::u256::U256" ],
                      "sub",
                      []
                    |),
                    [
                      M.read (| high |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_core_types::u256::U256",
                          "one",
                          []
                        |),
                        []
                      |)
                    ]
                  |);
                  M.read (| rng |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn sample_single_inclusive<R: rand::Rng + ?Sized, B1, B2>(
            low: B1,
            high: B2,
            rng: &mut R,
        ) -> Self::X
        where
            B1: rand::distributions::uniform::SampleBorrow<Self::X> + Sized,
            B2: rand::distributions::uniform::SampleBorrow<Self::X> + Sized,
        {
            let low = *low.borrow();
            let high = *high.borrow();
            assert!(
                low <= high,
                "UniformSampler::sample_single_inclusive: low > high"
            );
            let range = high.wrapping_sub(low).wrapping_add(U256::one());
            // If the above resulted in wrap-around to 0, the range is U256::MIN..=U256::MAX,
            // and any integer will do.
            if range == U256::zero() {
                return rng.gen();
            }
            // conservative but fast approximation. `- 1` is necessary to allow the
            // same comparison without bias.
            let zone = (range << range.leading_zeros()).wrapping_sub(U256::one());
    
            loop {
                let v: U256 = rng.gen();
                let (hi, lo) = v.wmul(range);
                if lo <= zone {
                    return low.wrapping_add(hi);
                }
            }
        }
    *)
    Definition sample_single_inclusive (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ R; B1; B2 ], [ low; high; rng ] =>
        ltac:(M.monadic
          (let low := M.alloc (| low |) in
          let high := M.alloc (| high |) in
          let rng := M.alloc (| rng |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ low :=
                  M.copy (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "rand::distributions::uniform::SampleBorrow",
                        B1,
                        [ Ty.path "move_core_types::u256::U256" ],
                        "borrow",
                        []
                      |),
                      [ low ]
                    |)
                  |) in
                let~ high :=
                  M.copy (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "rand::distributions::uniform::SampleBorrow",
                        B2,
                        [ Ty.path "move_core_types::u256::U256" ],
                        "borrow",
                        []
                      |),
                      [ high ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialOrd",
                                      Ty.path "move_core_types::u256::U256",
                                      [ Ty.path "move_core_types::u256::U256" ],
                                      "le",
                                      []
                                    |),
                                    [ low; high ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.call_closure (|
                                M.get_function (| "core::panicking::panic_fmt", [] |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::Arguments",
                                      "new_const",
                                      []
                                    |),
                                    [
                                      M.alloc (|
                                        Value.Array
                                          [
                                            M.read (|
                                              Value.String
                                                "UniformSampler::sample_single_inclusive: low > high"
                                            |)
                                          ]
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ range :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_core_types::u256::U256",
                        "wrapping_add",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_core_types::u256::U256",
                            "wrapping_sub",
                            []
                          |),
                          [ M.read (| high |); M.read (| low |) ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_core_types::u256::U256",
                            "one",
                            []
                          |),
                          []
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path "move_core_types::u256::U256",
                                    [ Ty.path "move_core_types::u256::U256" ],
                                    "eq",
                                    []
                                  |),
                                  [
                                    range;
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_core_types::u256::U256",
                                          "zero",
                                          []
                                        |),
                                        []
                                      |)
                                    |)
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "rand::rng::Rng",
                                      R,
                                      [],
                                      "gen",
                                      [ Ty.path "move_core_types::u256::U256" ]
                                    |),
                                    [ M.read (| rng |) ]
                                  |)
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ zone :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_core_types::u256::U256",
                        "wrapping_sub",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::bit::Shl",
                            Ty.path "move_core_types::u256::U256",
                            [ Ty.path "u32" ],
                            "shl",
                            []
                          |),
                          [
                            M.read (| range |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_core_types::u256::U256",
                                "leading_zeros",
                                []
                              |),
                              [ range ]
                            |)
                          ]
                        |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_core_types::u256::U256",
                            "one",
                            []
                          |),
                          []
                        |)
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.never_to_any (|
                    M.read (|
                      M.loop (|
                        ltac:(M.monadic
                          (let~ v :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "rand::rng::Rng",
                                  R,
                                  [],
                                  "gen",
                                  [ Ty.path "move_core_types::u256::U256" ]
                                |),
                                [ M.read (| rng |) ]
                              |)
                            |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_core_types::u256::U256",
                                  "wmul",
                                  []
                                |),
                                [ M.read (| v |); M.read (| range |) ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                  let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                  let hi := M.copy (| γ0_0 |) in
                                  let lo := M.copy (| γ0_1 |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::cmp::PartialOrd",
                                                    Ty.path "move_core_types::u256::U256",
                                                    [ Ty.path "move_core_types::u256::U256" ],
                                                    "le",
                                                    []
                                                  |),
                                                  [ lo; zone ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.return_ (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "move_core_types::u256::U256",
                                                      "wrapping_add",
                                                      []
                                                    |),
                                                    [ M.read (| low |); M.read (| hi |) ]
                                                  |)
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |)))
                      |)
                    |)
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "rand::distributions::uniform::UniformSampler"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("X", InstanceField.Ty _X);
          ("new", InstanceField.Method new);
          ("new_inclusive", InstanceField.Method new_inclusive);
          ("sample", InstanceField.Method sample);
          ("sample_single", InstanceField.Method sample_single);
          ("sample_single_inclusive", InstanceField.Method sample_single_inclusive)
        ].
  End Impl_rand_distributions_uniform_UniformSampler_for_move_core_types_u256_UniformU256.
End u256.
