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

Module account_address.
  (* StructTuple
    {
      name := "AccountAddress";
      const_params := [];
      ty_params := [];
      fields :=
        [
          Ty.apply
            (Ty.path "array")
            [
              M.unevaluated_const
                (M.get_constant (|
                  "move_core_types::account_address::AccountAddress::0_discriminant"
                |))
            ]
            [ Ty.path "u8" ]
        ];
    } *)
  
  Module Impl_core_cmp_Ord_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (* 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.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ],
              [],
              "cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::account_address::AccountAddress",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_core_types::account_address::AccountAddress",
                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_account_address_AccountAddress.
  
  Module Impl_core_cmp_PartialOrd_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (* 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.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ],
              [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ]
              ],
              "partial_cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::account_address::AccountAddress",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_core_types::account_address::AccountAddress",
                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_account_address_AccountAddress.
  
  Module Impl_core_cmp_Eq_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (* 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_account_address_AccountAddress.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_account_address_AccountAddress.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (* 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.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ],
              [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ]
              ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::account_address::AccountAddress",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_core_types::account_address::AccountAddress",
                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_account_address_AccountAddress.
  
  Module Impl_core_hash_Hash_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (* 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.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ],
              [],
              "hash",
              [ __H ]
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::account_address::AccountAddress",
                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_account_address_AccountAddress.
  
  Module Impl_core_clone_Clone_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (* 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_account_address_AccountAddress.
  
  Module Impl_core_marker_Copy_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_core_types_account_address_AccountAddress.
  
  Module Impl_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        pub const fn new(address: [u8; Self::LENGTH]) -> Self {
            Self(address)
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ address ] =>
        ltac:(M.monadic
          (let address := M.alloc (| address |) in
          Value.StructTuple
            "move_core_types::account_address::AccountAddress"
            [ M.read (| address |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*     pub const LENGTH: usize = 32; *)
    (* Ty.path "usize" *)
    Definition value_LENGTH : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 32 |))).
    
    Axiom AssociatedConstant_value_LENGTH : M.IsAssociatedConstant Self "value_LENGTH" value_LENGTH.
    
    (*     pub const ZERO: Self = Self([0u8; Self::LENGTH]); *)
    (* Ty.path "move_core_types::account_address::AccountAddress" *)
    Definition value_ZERO : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            Value.StructTuple
              "move_core_types::account_address::AccountAddress"
              [ repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) ]
          |))).
    
    Axiom AssociatedConstant_value_ZERO : M.IsAssociatedConstant Self "value_ZERO" value_ZERO.
    
    (*     pub const ONE: Self = Self::get_hex_address_one(); *)
    (* Ty.path "move_core_types::account_address::AccountAddress" *)
    Definition value_ONE : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "move_core_types::account_address::AccountAddress",
                "get_hex_address_one",
                []
              |),
              []
            |)
          |))).
    
    Axiom AssociatedConstant_value_ONE : M.IsAssociatedConstant Self "value_ONE" value_ONE.
    
    (*     pub const TWO: Self = Self::get_hex_address_two(); *)
    (* Ty.path "move_core_types::account_address::AccountAddress" *)
    Definition value_TWO : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "move_core_types::account_address::AccountAddress",
                "get_hex_address_two",
                []
              |),
              []
            |)
          |))).
    
    Axiom AssociatedConstant_value_TWO : M.IsAssociatedConstant Self "value_TWO" value_TWO.
    
    (*
        const fn get_hex_address_one() -> Self {
            let mut addr = [0u8; AccountAddress::LENGTH];
            addr[AccountAddress::LENGTH - 1] = 1u8;
            Self(addr)
        }
    *)
    Definition get_hex_address_one (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.read (|
            let~ addr :=
              M.alloc (|
                repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (|
                  addr,
                  M.alloc (|
                    BinOp.Wrap.sub (|
                      M.read (| M.get_constant (| "move_core_types::account_address::LENGTH" |) |),
                      Value.Integer IntegerKind.Usize 1
                    |)
                  |)
                |),
                Value.Integer IntegerKind.U8 1
              |) in
            M.alloc (|
              Value.StructTuple
                "move_core_types::account_address::AccountAddress"
                [ M.read (| addr |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_hex_address_one :
      M.IsAssociatedFunction Self "get_hex_address_one" get_hex_address_one.
    
    (*
        const fn get_hex_address_two() -> Self {
            let mut addr = [0u8; AccountAddress::LENGTH];
            addr[AccountAddress::LENGTH - 1] = 2u8;
            Self(addr)
        }
    *)
    Definition get_hex_address_two (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.read (|
            let~ addr :=
              M.alloc (|
                repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_array_field (|
                  addr,
                  M.alloc (|
                    BinOp.Wrap.sub (|
                      M.read (| M.get_constant (| "move_core_types::account_address::LENGTH" |) |),
                      Value.Integer IntegerKind.Usize 1
                    |)
                  |)
                |),
                Value.Integer IntegerKind.U8 2
              |) in
            M.alloc (|
              Value.StructTuple
                "move_core_types::account_address::AccountAddress"
                [ M.read (| addr |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_hex_address_two :
      M.IsAssociatedFunction Self "get_hex_address_two" get_hex_address_two.
    
    (*
        pub fn random() -> Self {
            let mut rng = OsRng;
            let buf: [u8; Self::LENGTH] = rng.gen();
            Self(buf)
        }
    *)
    Definition random (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.read (|
            let~ rng := M.alloc (| Value.StructTuple "rand_core::os::OsRng" [] |) in
            let~ buf :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "rand::rng::Rng",
                    Ty.path "rand_core::os::OsRng",
                    [],
                    "gen",
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ]
                    ]
                  |),
                  [ rng ]
                |)
              |) in
            M.alloc (|
              Value.StructTuple
                "move_core_types::account_address::AccountAddress"
                [ M.read (| buf |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_random : M.IsAssociatedFunction Self "random" random.
    
    (*
        pub fn to_canonical_string(&self, with_prefix: bool) -> String {
            self.to_canonical_display(with_prefix).to_string()
        }
    *)
    Definition to_canonical_string (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; with_prefix ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let with_prefix := M.alloc (| with_prefix |) in
          M.call_closure (|
            M.get_trait_method (| "alloc::string::ToString", Ty.associated, [], "to_string", [] |),
            [
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_core_types::account_address::AccountAddress",
                    "to_canonical_display",
                    []
                  |),
                  [ M.read (| self |); M.read (| with_prefix |) ]
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_canonical_string :
      M.IsAssociatedFunction Self "to_canonical_string" to_canonical_string.
    
    (*
        pub fn to_canonical_display(&self, with_prefix: bool) -> impl fmt::Display + '_ {
            struct HexDisplay<'a> {
                data: &'a [u8],
                with_prefix: bool,
            }
    
            impl<'a> fmt::Display for HexDisplay<'a> {
                fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
                    if self.with_prefix {
                        write!(f, "0x{}", hex::encode(self.data))
                    } else {
                        write!(f, "{}", hex::encode(self.data))
                    }
                }
            }
            HexDisplay {
                data: &self.0,
                with_prefix,
            }
        }
    *)
    Definition to_canonical_display (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; with_prefix ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let with_prefix := M.alloc (| with_prefix |) in
          Value.StructRecord
            "move_core_types::account_address::to_canonical_display::HexDisplay"
            [
              ("data",
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::account_address::AccountAddress",
                  0
                |));
              ("with_prefix", M.read (| with_prefix |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_canonical_display :
      M.IsAssociatedFunction Self "to_canonical_display" to_canonical_display.
    
    (*
        pub fn short_str_lossless(&self) -> String {
            let hex_str = hex::encode(self.0).trim_start_matches('0').to_string();
            if hex_str.is_empty() {
                "0".to_string()
            } else {
                hex_str
            }
        }
    *)
    Definition short_str_lossless (ε : 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~ hex_str :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "alloc::string::ToString",
                    Ty.path "str",
                    [],
                    "to_string",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "str",
                        "trim_start_matches",
                        [ Ty.path "char" ]
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.path "alloc::string::String",
                            [],
                            "deref",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "hex::encode",
                                  [
                                    Ty.apply
                                      (Ty.path "array")
                                      [ Value.Integer IntegerKind.Usize 32 ]
                                      [ Ty.path "u8" ]
                                  ]
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_tuple_field (|
                                      M.read (| self |),
                                      "move_core_types::account_address::AccountAddress",
                                      0
                                    |)
                                  |)
                                ]
                              |)
                            |)
                          ]
                        |);
                        Value.UnicodeChar 48
                      ]
                    |)
                  ]
                |)
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "alloc::string::String",
                              "is_empty",
                              []
                            |),
                            [ hex_str ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "alloc::string::ToString",
                          Ty.path "str",
                          [],
                          "to_string",
                          []
                        |),
                        [ M.read (| Value.String "0" |) ]
                      |)
                    |)));
                fun γ => ltac:(M.monadic hex_str)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_short_str_lossless :
      M.IsAssociatedFunction Self "short_str_lossless" short_str_lossless.
    
    (*
        pub fn to_vec(&self) -> Vec<u8> {
            self.0.to_vec()
        }
    *)
    Definition to_vec (ε : 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.apply (Ty.path "slice") [] [ Ty.path "u8" ],
              "to_vec",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::account_address::AccountAddress",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_vec : M.IsAssociatedFunction Self "to_vec" to_vec.
    
    (*
        pub fn into_bytes(self) -> [u8; Self::LENGTH] {
            self.0
        }
    *)
    Definition into_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 (|
            M.SubPointer.get_struct_tuple_field (|
              self,
              "move_core_types::account_address::AccountAddress",
              0
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_bytes : M.IsAssociatedFunction Self "into_bytes" into_bytes.
    
    (*
        pub fn from_hex_literal(literal: &str) -> Result<Self, AccountAddressParseError> {
            if !literal.starts_with("0x") {
                return Err(AccountAddressParseError);
            }
    
            let hex_len = literal.len() - 2;
    
            // If the string is too short, pad it
            if hex_len < Self::LENGTH * 2 {
                let mut hex_str = String::with_capacity(Self::LENGTH * 2);
                for _ in 0..Self::LENGTH * 2 - hex_len {
                    hex_str.push('0');
                }
                hex_str.push_str(&literal[2..]);
                AccountAddress::from_hex(hex_str)
            } else {
                AccountAddress::from_hex(&literal[2..])
            }
        }
    *)
    Definition from_hex_literal (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ literal ] =>
        ltac:(M.monadic
          (let literal := M.alloc (| literal |) 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 (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "str",
                                      "starts_with",
                                      [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                                    |),
                                    [ M.read (| literal |); M.read (| Value.String "0x" |) ]
                                  |)
                                |)
                              |)) 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::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "move_core_types::account_address::AccountAddressParseError"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ hex_len :=
                  M.alloc (|
                    BinOp.Wrap.sub (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "str", "len", [] |),
                        [ M.read (| literal |) ]
                      |),
                      Value.Integer IntegerKind.Usize 2
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (|
                                M.read (| hex_len |),
                                BinOp.Wrap.mul (|
                                  M.read (|
                                    M.get_constant (| "move_core_types::account_address::LENGTH" |)
                                  |),
                                  Value.Integer IntegerKind.Usize 2
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ hex_str :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "alloc::string::String",
                                "with_capacity",
                                []
                              |),
                              [
                                BinOp.Wrap.mul (|
                                  M.read (|
                                    M.get_constant (| "move_core_types::account_address::LENGTH" |)
                                  |),
                                  Value.Integer IntegerKind.Usize 2
                                |)
                              ]
                            |)
                          |) in
                        let~ _ :=
                          M.use
                            (M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    Ty.apply
                                      (Ty.path "core::ops::range::Range")
                                      []
                                      [ Ty.path "usize" ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [
                                    Value.StructRecord
                                      "core::ops::range::Range"
                                      [
                                        ("start", Value.Integer IntegerKind.Usize 0);
                                        ("end_",
                                          BinOp.Wrap.sub (|
                                            BinOp.Wrap.mul (|
                                              M.read (|
                                                M.get_constant (|
                                                  "move_core_types::account_address::LENGTH"
                                                |)
                                              |),
                                              Value.Integer IntegerKind.Usize 2
                                            |),
                                            M.read (| hex_len |)
                                          |))
                                      ]
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.apply
                                                    (Ty.path "core::ops::range::Range")
                                                    []
                                                    [ Ty.path "usize" ],
                                                  [],
                                                  "next",
                                                  []
                                                |),
                                                [ iter ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (| M.read (| M.break (||) |) |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "alloc::string::String",
                                                          "push",
                                                          []
                                                        |),
                                                        [ hex_str; Value.UnicodeChar 48 ]
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "alloc::string::String",
                                "push_str",
                                []
                              |),
                              [
                                hex_str;
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::index::Index",
                                    Ty.path "str",
                                    [
                                      Ty.apply
                                        (Ty.path "core::ops::range::RangeFrom")
                                        []
                                        [ Ty.path "usize" ]
                                    ],
                                    "index",
                                    []
                                  |),
                                  [
                                    M.read (| literal |);
                                    Value.StructRecord
                                      "core::ops::range::RangeFrom"
                                      [ ("start", Value.Integer IntegerKind.Usize 2) ]
                                  ]
                                |)
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::account_address::AccountAddress",
                              "from_hex",
                              [ Ty.path "alloc::string::String" ]
                            |),
                            [ M.read (| hex_str |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::account_address::AccountAddress",
                              "from_hex",
                              [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::index::Index",
                                  Ty.path "str",
                                  [
                                    Ty.apply
                                      (Ty.path "core::ops::range::RangeFrom")
                                      []
                                      [ Ty.path "usize" ]
                                  ],
                                  "index",
                                  []
                                |),
                                [
                                  M.read (| literal |);
                                  Value.StructRecord
                                    "core::ops::range::RangeFrom"
                                    [ ("start", Value.Integer IntegerKind.Usize 2) ]
                                ]
                              |)
                            ]
                          |)
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_hex_literal :
      M.IsAssociatedFunction Self "from_hex_literal" from_hex_literal.
    
    (*
        pub fn to_hex_literal(&self) -> String {
            format!("0x{}", self.short_str_lossless())
        }
    *)
    Definition to_hex_literal (ε : 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_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 "0x" |) ] |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "alloc::string::String" ]
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path
                                              "move_core_types::account_address::AccountAddress",
                                            "short_str_lossless",
                                            []
                                          |),
                                          [ M.read (| self |) ]
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                res
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_hex_literal :
      M.IsAssociatedFunction Self "to_hex_literal" to_hex_literal.
    
    (*
        pub fn from_hex<T: AsRef<[u8]>>(hex: T) -> Result<Self, AccountAddressParseError> {
            <[u8; Self::LENGTH]>::from_hex(hex)
                .map_err(|_| AccountAddressParseError)
                .map(Self)
        }
    *)
    Definition from_hex (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ hex ] =>
        ltac:(M.monadic
          (let hex := M.alloc (| hex |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 32 ]
                    [ Ty.path "u8" ];
                  Ty.path "move_core_types::account_address::AccountAddressParseError"
                ],
              "map",
              [
                Ty.path "move_core_types::account_address::AccountAddress";
                Ty.function
                  [
                    Ty.apply
                      (Ty.path "array")
                      [
                        M.unevaluated_const
                          (M.get_constant (|
                            "move_core_types::account_address::AccountAddress::0_discriminant"
                          |))
                      ]
                      [ Ty.path "u8" ]
                  ]
                  (Ty.path "move_core_types::account_address::AccountAddress")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ];
                      Ty.path "hex::error::FromHexError"
                    ],
                  "map_err",
                  [
                    Ty.path "move_core_types::account_address::AccountAddressParseError";
                    Ty.function
                      [ Ty.tuple [ Ty.path "hex::error::FromHexError" ] ]
                      (Ty.path "move_core_types::account_address::AccountAddressParseError")
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "hex::FromHex",
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ],
                      [],
                      "from_hex",
                      [ T ]
                    |),
                    [ M.read (| hex |) ]
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (Value.StructTuple
                                      "move_core_types::account_address::AccountAddressParseError"
                                      []))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |);
              M.constructor_as_closure "move_core_types::account_address::AccountAddress"
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_hex : M.IsAssociatedFunction Self "from_hex" from_hex.
    
    (*
        pub fn to_hex(&self) -> String {
            format!("{:x}", self)
        }
    *)
    Definition to_hex (ε : 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_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_lower_hex",
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.path
                                              "move_core_types::account_address::AccountAddress"
                                          ]
                                      ]
                                    |),
                                    [ self ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                res
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_to_hex : M.IsAssociatedFunction Self "to_hex" to_hex.
    
    (*
        pub fn from_bytes<T: AsRef<[u8]>>(bytes: T) -> Result<Self, AccountAddressParseError> {
            <[u8; Self::LENGTH]>::try_from(bytes.as_ref())
                .map_err(|_| AccountAddressParseError)
                .map(Self)
        }
    *)
    Definition from_bytes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ T ], [ bytes ] =>
        ltac:(M.monadic
          (let bytes := M.alloc (| bytes |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 32 ]
                    [ Ty.path "u8" ];
                  Ty.path "move_core_types::account_address::AccountAddressParseError"
                ],
              "map",
              [
                Ty.path "move_core_types::account_address::AccountAddress";
                Ty.function
                  [
                    Ty.apply
                      (Ty.path "array")
                      [
                        M.unevaluated_const
                          (M.get_constant (|
                            "move_core_types::account_address::AccountAddress::0_discriminant"
                          |))
                      ]
                      [ Ty.path "u8" ]
                  ]
                  (Ty.path "move_core_types::account_address::AccountAddress")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ];
                      Ty.path "core::array::TryFromSliceError"
                    ],
                  "map_err",
                  [
                    Ty.path "move_core_types::account_address::AccountAddressParseError";
                    Ty.function
                      [ Ty.tuple [ Ty.path "core::array::TryFromSliceError" ] ]
                      (Ty.path "move_core_types::account_address::AccountAddressParseError")
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::TryFrom",
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ],
                      [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                      ],
                      "try_from",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::convert::AsRef",
                          T,
                          [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                          "as_ref",
                          []
                        |),
                        [ bytes ]
                      |)
                    ]
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (Value.StructTuple
                                      "move_core_types::account_address::AccountAddressParseError"
                                      []))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |);
              M.constructor_as_closure "move_core_types::account_address::AccountAddress"
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_bytes : M.IsAssociatedFunction Self "from_bytes" from_bytes.
    
    (*
        pub fn abstract_size_for_gas_metering(&self) -> AbstractMemorySize {
            AbstractMemorySize::new(Self::LENGTH as u64)
        }
    *)
    Definition abstract_size_for_gas_metering
        (ε : 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.apply
                (Ty.path "move_core_types::gas_algebra::GasQuantity")
                []
                [ Ty.path "move_core_types::gas_algebra::AbstractMemoryUnit" ],
              "new",
              []
            |),
            [
              M.rust_cast
                (M.read (| M.get_constant (| "move_core_types::account_address::LENGTH" |) |))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_abstract_size_for_gas_metering :
      M.IsAssociatedFunction Self "abstract_size_for_gas_metering" abstract_size_for_gas_metering.
  End Impl_move_core_types_account_address_AccountAddress.
  
  Module Impl_core_convert_AsRef_slice_u8_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        fn as_ref(&self) -> &[u8] {
            &self.0
        }
    *)
    Definition as_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.SubPointer.get_struct_tuple_field (|
            M.read (| self |),
            "move_core_types::account_address::AccountAddress",
            0
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::AsRef"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
        (* Instance *) [ ("as_ref", InstanceField.Method as_ref) ].
  End Impl_core_convert_AsRef_slice_u8_for_move_core_types_account_address_AccountAddress.
  
  Module Impl_core_ops_deref_Deref_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*     type Target = [u8; Self::LENGTH]; *)
    Definition _Target : Ty.t :=
      Ty.apply
        (Ty.path "array")
        [
          M.unevaluated_const
            (M.get_constant (| "move_core_types::account_address::Target_discriminant" |))
        ]
        [ Ty.path "u8" ].
    
    (*
        fn deref(&self) -> &Self::Target {
            &self.0
        }
    *)
    Definition deref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.SubPointer.get_struct_tuple_field (|
            M.read (| self |),
            "move_core_types::account_address::AccountAddress",
            0
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::ops::deref::Deref"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("Target", InstanceField.Ty _Target); ("deref", InstanceField.Method deref) ].
  End Impl_core_ops_deref_Deref_for_move_core_types_account_address_AccountAddress.
  
  Module Impl_core_fmt_Display_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter) -> std::fmt::Result {
            write!(f, "{:x}", self)
        }
    *)
    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_lower_hex",
                            [
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.path "move_core_types::account_address::AccountAddress" ]
                            ]
                          |),
                          [ self ]
                        |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => 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_account_address_AccountAddress.
  
  Module Impl_core_fmt_Debug_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            write!(f, "{:x}", self)
        }
    *)
    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_lower_hex",
                            [
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.path "move_core_types::account_address::AccountAddress" ]
                            ]
                          |),
                          [ self ]
                        |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => 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_account_address_AccountAddress.
  
  Module Impl_core_fmt_LowerHex_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            if f.alternate() {
                write!(f, "0x")?;
            }
    
            for byte in &self.0 {
                write!(f, "{:02x}", byte)?;
            }
    
            Ok(())
        }
    *)
    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.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::Formatter",
                                    "alternate",
                                    []
                                  |),
                                  [ M.read (| f |) ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            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.tuple []; Ty.path "core::fmt::Error" ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    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_const",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              Value.Array [ M.read (| Value.String "0x" |) ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                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.tuple []; Ty.path "core::fmt::Error" ],
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.path "core::convert::Infallible";
                                                      Ty.path "core::fmt::Error"
                                                    ]
                                                ],
                                                "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))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "array")
                                  [ Value.Integer IntegerKind.Usize 32 ]
                                  [ Ty.path "u8" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_core_types::account_address::AccountAddress",
                              0
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [ Ty.path "u8" ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let byte := M.copy (| γ0_0 |) in
                                          let~ _ :=
                                            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.tuple []; Ty.path "core::fmt::Error" ],
                                                    [],
                                                    "branch",
                                                    []
                                                  |),
                                                  [
                                                    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_formatted",
                                                            []
                                                          |),
                                                          [
                                                            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_lower_hex",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ Ty.path "u8" ]
                                                                      ]
                                                                    |),
                                                                    [ byte ]
                                                                  |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Placeholder",
                                                                      "new",
                                                                      []
                                                                    |),
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        0;
                                                                      Value.UnicodeChar 32;
                                                                      Value.StructTuple
                                                                        "core::fmt::rt::Alignment::Unknown"
                                                                        [];
                                                                      Value.Integer
                                                                        IntegerKind.U32
                                                                        8;
                                                                      Value.StructTuple
                                                                        "core::fmt::rt::Count::Implied"
                                                                        [];
                                                                      Value.StructTuple
                                                                        "core::fmt::rt::Count::Is"
                                                                        [
                                                                          Value.Integer
                                                                            IntegerKind.Usize
                                                                            2
                                                                        ]
                                                                    ]
                                                                  |)
                                                                ]
                                                            |);
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path "core::fmt::rt::UnsafeArg",
                                                                "new",
                                                                []
                                                              |),
                                                              []
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                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.tuple [];
                                                                    Ty.path "core::fmt::Error"
                                                                  ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::convert::Infallible";
                                                                      Ty.path "core::fmt::Error"
                                                                    ]
                                                                ],
                                                                "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))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => 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_account_address_AccountAddress.
  
  Module Impl_core_fmt_UpperHex_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            if f.alternate() {
                write!(f, "0x")?;
            }
    
            for byte in &self.0 {
                write!(f, "{:02X}", byte)?;
            }
    
            Ok(())
        }
    *)
    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.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::Formatter",
                                    "alternate",
                                    []
                                  |),
                                  [ M.read (| f |) ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            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.tuple []; Ty.path "core::fmt::Error" ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    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_const",
                                            []
                                          |),
                                          [
                                            M.alloc (|
                                              Value.Array [ M.read (| Value.String "0x" |) ]
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                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.tuple []; Ty.path "core::fmt::Error" ],
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::result::Result")
                                                    []
                                                    [
                                                      Ty.path "core::convert::Infallible";
                                                      Ty.path "core::fmt::Error"
                                                    ]
                                                ],
                                                "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))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "array")
                                  [ Value.Integer IntegerKind.Usize 32 ]
                                  [ Ty.path "u8" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| self |),
                              "move_core_types::account_address::AccountAddress",
                              0
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [ Ty.path "u8" ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let byte := M.copy (| γ0_0 |) in
                                          let~ _ :=
                                            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.tuple []; Ty.path "core::fmt::Error" ],
                                                    [],
                                                    "branch",
                                                    []
                                                  |),
                                                  [
                                                    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_formatted",
                                                            []
                                                          |),
                                                          [
                                                            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.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ Ty.path "u8" ]
                                                                      ]
                                                                    |),
                                                                    [ byte ]
                                                                  |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Placeholder",
                                                                      "new",
                                                                      []
                                                                    |),
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        0;
                                                                      Value.UnicodeChar 32;
                                                                      Value.StructTuple
                                                                        "core::fmt::rt::Alignment::Unknown"
                                                                        [];
                                                                      Value.Integer
                                                                        IntegerKind.U32
                                                                        8;
                                                                      Value.StructTuple
                                                                        "core::fmt::rt::Count::Implied"
                                                                        [];
                                                                      Value.StructTuple
                                                                        "core::fmt::rt::Count::Is"
                                                                        [
                                                                          Value.Integer
                                                                            IntegerKind.Usize
                                                                            2
                                                                        ]
                                                                    ]
                                                                  |)
                                                                ]
                                                            |);
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path "core::fmt::rt::UnsafeArg",
                                                                "new",
                                                                []
                                                              |),
                                                              []
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                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.tuple [];
                                                                    Ty.path "core::fmt::Error"
                                                                  ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::convert::Infallible";
                                                                      Ty.path "core::fmt::Error"
                                                                    ]
                                                                ],
                                                                "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))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => 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_account_address_AccountAddress.
  
  Module Impl_core_convert_From_array_expr_u8_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        fn from(bytes: [u8; AccountAddress::LENGTH]) -> Self {
            Self::new(bytes)
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytes ] =>
        ltac:(M.monadic
          (let bytes := M.alloc (| bytes |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::account_address::AccountAddress",
              "new",
              []
            |),
            [ M.read (| bytes |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [
          (* T *)
          Ty.apply
            (Ty.path "array")
            [
              M.unevaluated_const
                (M.get_constant (| "move_core_types::account_address_discriminant" |))
            ]
            [ Ty.path "u8" ]
        ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_array_expr_u8_for_move_core_types_account_address_AccountAddress.
  
  Module Impl_core_convert_TryFrom_ref__slice_u8_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*     type Error = AccountAddressParseError; *)
    Definition _Error : Ty.t :=
      Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    (*
        fn try_from(bytes: &[u8]) -> Result<AccountAddress, AccountAddressParseError> {
            Self::from_bytes(bytes)
        }
    *)
    Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytes ] =>
        ltac:(M.monadic
          (let bytes := M.alloc (| bytes |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::account_address::AccountAddress",
              "from_bytes",
              [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ]
            |),
            [ M.read (| bytes |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *)
        [ (* T *) Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_ref__slice_u8_for_move_core_types_account_address_AccountAddress.
  
  Module Impl_core_convert_TryFrom_alloc_vec_Vec_u8_alloc_alloc_Global_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*     type Error = AccountAddressParseError; *)
    Definition _Error : Ty.t :=
      Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    (*
        fn try_from(bytes: Vec<u8>) -> Result<AccountAddress, AccountAddressParseError> {
            Self::from_bytes(bytes)
        }
    *)
    Definition try_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ bytes ] =>
        ltac:(M.monadic
          (let bytes := M.alloc (| bytes |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_core_types::account_address::AccountAddress",
              "from_bytes",
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
              ]
            |),
            [ M.read (| bytes |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *)
        [
          (* T *)
          Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
        ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_alloc_vec_Vec_u8_alloc_alloc_Global_for_move_core_types_account_address_AccountAddress.
  
  Module Impl_core_convert_From_move_core_types_account_address_AccountAddress_for_alloc_vec_Vec_u8_alloc_alloc_Global.
    Definition Self : Ty.t :=
      Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ].
    
    (*
        fn from(addr: AccountAddress) -> Vec<u8> {
            addr.0.to_vec()
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
              "to_vec",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                addr,
                "move_core_types::account_address::AccountAddress",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [ (* T *) Ty.path "move_core_types::account_address::AccountAddress" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_move_core_types_account_address_AccountAddress_for_alloc_vec_Vec_u8_alloc_alloc_Global.
  
  Module Impl_core_convert_From_ref__move_core_types_account_address_AccountAddress_for_alloc_vec_Vec_u8_alloc_alloc_Global.
    Definition Self : Ty.t :=
      Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ].
    
    (*
        fn from(addr: &AccountAddress) -> Vec<u8> {
            addr.0.to_vec()
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
              "to_vec",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| addr |),
                "move_core_types::account_address::AccountAddress",
                0
              |)
            ]
          |)))
      | _, _, _ => 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::account_address::AccountAddress" ]
        ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_ref__move_core_types_account_address_AccountAddress_for_alloc_vec_Vec_u8_alloc_alloc_Global.
  
  Module Impl_core_convert_From_move_core_types_account_address_AccountAddress_for_array_expr_u8.
    Definition Self : Ty.t :=
      Ty.apply
        (Ty.path "array")
        [ M.unevaluated_const (M.get_constant (| "move_core_types::account_address_discriminant" |))
        ]
        [ Ty.path "u8" ].
    
    (*
        fn from(addr: AccountAddress) -> Self {
            addr.0
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          M.read (|
            M.SubPointer.get_struct_tuple_field (|
              addr,
              "move_core_types::account_address::AccountAddress",
              0
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [ (* T *) Ty.path "move_core_types::account_address::AccountAddress" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_move_core_types_account_address_AccountAddress_for_array_expr_u8.
  
  Module Impl_core_convert_From_ref__move_core_types_account_address_AccountAddress_for_array_expr_u8.
    Definition Self : Ty.t :=
      Ty.apply
        (Ty.path "array")
        [ M.unevaluated_const (M.get_constant (| "move_core_types::account_address_discriminant" |))
        ]
        [ Ty.path "u8" ].
    
    (*
        fn from(addr: &AccountAddress) -> Self {
            addr.0
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          M.read (|
            M.SubPointer.get_struct_tuple_field (|
              M.read (| addr |),
              "move_core_types::account_address::AccountAddress",
              0
            |)
          |)))
      | _, _, _ => 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::account_address::AccountAddress" ]
        ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_ref__move_core_types_account_address_AccountAddress_for_array_expr_u8.
  
  Module Impl_core_convert_From_ref__move_core_types_account_address_AccountAddress_for_alloc_string_String.
    Definition Self : Ty.t := Ty.path "alloc::string::String".
    
    (*
        fn from(addr: &AccountAddress) -> String {
            ::hex::encode(addr.as_ref())
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ addr ] =>
        ltac:(M.monadic
          (let addr := M.alloc (| addr |) in
          M.call_closure (|
            M.get_function (|
              "hex::encode",
              [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ]
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::AsRef",
                  Ty.path "move_core_types::account_address::AccountAddress",
                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                  "as_ref",
                  []
                |),
                [ M.read (| addr |) ]
              |)
            ]
          |)))
      | _, _, _ => 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::account_address::AccountAddress" ]
        ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_ref__move_core_types_account_address_AccountAddress_for_alloc_string_String.
  
  Module Impl_core_convert_TryFrom_alloc_string_String_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*     type Error = AccountAddressParseError; *)
    Definition _Error : Ty.t :=
      Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    (*
        fn try_from(s: String) -> Result<AccountAddress, AccountAddressParseError> {
            Self::from_hex(s)
        }
    *)
    Definition try_from (ε : 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::account_address::AccountAddress",
              "from_hex",
              [ Ty.path "alloc::string::String" ]
            |),
            [ M.read (| s |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::TryFrom"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "alloc::string::String" ]
        (* Instance *)
        [ ("Error", InstanceField.Ty _Error); ("try_from", InstanceField.Method try_from) ].
  End Impl_core_convert_TryFrom_alloc_string_String_for_move_core_types_account_address_AccountAddress.
  
  Module Impl_core_str_traits_FromStr_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*     type Err = AccountAddressParseError; *)
    Definition _Err : Ty.t := Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    (*
        fn from_str(s: &str) -> Result<Self, AccountAddressParseError> {
            // Accept 0xADDRESS or ADDRESS
            if let Ok(address) = AccountAddress::from_hex_literal(s) {
                Ok(address)
            } else {
                Self::from_hex(s)
            }
        }
    *)
    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.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_core_types::account_address::AccountAddress",
                            "from_hex_literal",
                            []
                          |),
                          [ M.read (| s |) ]
                        |)
                      |) in
                    let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (| γ, "core::result::Result::Ok", 0 |) in
                    let address := M.copy (| γ0_0 |) in
                    M.alloc (|
                      Value.StructTuple "core::result::Result::Ok" [ M.read (| address |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_core_types::account_address::AccountAddress",
                          "from_hex",
                          [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                        |),
                        [ M.read (| s |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_account_address_AccountAddress.
  
  Module Impl_serde_de_Deserialize_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        fn deserialize<D>(deserializer: D) -> std::result::Result<Self, D::Error>
        where
            D: Deserializer<'de>,
        {
            if deserializer.is_human_readable() {
                let s = <String>::deserialize(deserializer)?;
                AccountAddress::from_str(&s).map_err(D::Error::custom)
            } else {
                // In order to preserve the Serde data model and help analysis tools,
                // make sure to wrap our value in a container with the same name
                // as the original type.
                #[derive(::serde::Deserialize)]
                #[serde(rename = "AccountAddress")]
                struct Value([u8; AccountAddress::LENGTH]);
    
                let value = Value::deserialize(deserializer)?;
                Ok(AccountAddress::new(value.0))
            }
        }
    *)
    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
              (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 (|
                                  "serde::de::Deserializer",
                                  D,
                                  [],
                                  "is_human_readable",
                                  []
                                |),
                                [ deserializer ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ s :=
                          M.copy (|
                            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.path "alloc::string::String"; Ty.associated ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "serde::de::Deserialize",
                                        Ty.path "alloc::string::String",
                                        [],
                                        "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::account_address::AccountAddress";
                                                    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))
                              ]
                            |)
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.path "move_core_types::account_address::AccountAddress";
                                  Ty.path
                                    "move_core_types::account_address::AccountAddressParseError"
                                ],
                              "map_err",
                              [
                                Ty.associated;
                                Ty.function
                                  [
                                    Ty.path
                                      "move_core_types::account_address::AccountAddressParseError"
                                  ]
                                  Ty.associated
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::str::traits::FromStr",
                                  Ty.path "move_core_types::account_address::AccountAddress",
                                  [],
                                  "from_str",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::deref::Deref",
                                      Ty.path "alloc::string::String",
                                      [],
                                      "deref",
                                      []
                                    |),
                                    [ s ]
                                  |)
                                ]
                              |);
                              M.get_trait_method (|
                                "serde::de::Error",
                                Ty.associated,
                                [],
                                "custom",
                                [
                                  Ty.path
                                    "move_core_types::account_address::AccountAddressParseError"
                                ]
                              |)
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let~ value :=
                          M.copy (|
                            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.path
                                          "move_core_types::account_address::deserialize::Value";
                                        Ty.associated
                                      ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "serde::de::Deserialize",
                                        Ty.path
                                          "move_core_types::account_address::deserialize::Value",
                                        [],
                                        "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::account_address::AccountAddress";
                                                    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))
                              ]
                            |)
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_core_types::account_address::AccountAddress",
                                  "new",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_tuple_field (|
                                      value,
                                      "move_core_types::account_address::deserialize::Value",
                                      0
                                    |)
                                  |)
                                ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => 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_account_address_AccountAddress.
  
  Module Impl_serde_ser_Serialize_for_move_core_types_account_address_AccountAddress.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddress".
    
    (*
        fn serialize<S>(&self, serializer: S) -> std::result::Result<S::Ok, S::Error>
        where
            S: Serializer,
        {
            if serializer.is_human_readable() {
                self.to_hex().serialize(serializer)
            } else {
                // See comment in deserialize.
                serializer.serialize_newtype_struct("AccountAddress", &self.0)
            }
        }
    *)
    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.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              S,
                              [],
                              "is_human_readable",
                              []
                            |),
                            [ serializer ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "serde::ser::Serialize",
                          Ty.path "alloc::string::String",
                          [],
                          "serialize",
                          [ S ]
                        |),
                        [
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_core_types::account_address::AccountAddress",
                                "to_hex",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |);
                          M.read (| serializer |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "serde::ser::Serializer",
                          S,
                          [],
                          "serialize_newtype_struct",
                          [
                            Ty.apply
                              (Ty.path "array")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [ Ty.path "u8" ]
                          ]
                        |),
                        [
                          M.read (| serializer |);
                          M.read (| Value.String "AccountAddress" |);
                          M.SubPointer.get_struct_tuple_field (|
                            M.read (| self |),
                            "move_core_types::account_address::AccountAddress",
                            0
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_account_address_AccountAddress.
  
  (* StructTuple
    {
      name := "AccountAddressParseError";
      const_params := [];
      ty_params := [];
      fields := [];
    } *)
  
  Module Impl_core_clone_Clone_for_move_core_types_account_address_AccountAddressParseError.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    (* 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_account_address_AccountAddressParseError.
  
  Module Impl_core_marker_Copy_for_move_core_types_account_address_AccountAddressParseError.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_core_types_account_address_AccountAddressParseError.
  
  Module Impl_core_fmt_Debug_for_move_core_types_account_address_AccountAddressParseError.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    (* 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 (| Value.String "AccountAddressParseError" |) ]
          |)))
      | _, _, _ => 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_account_address_AccountAddressParseError.
  
  Module Impl_core_fmt_Display_for_move_core_types_account_address_AccountAddressParseError.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter) -> std::fmt::Result {
            write!(
                f,
                "Unable to parse AccountAddress (must be hex string of length {})",
                AccountAddress::LENGTH
            )
        }
    *)
    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
                            "Unable to parse AccountAddress (must be hex string of length "
                        |);
                        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 "usize" ]
                          |),
                          [ M.get_constant (| "move_core_types::account_address::LENGTH" |) ]
                        |)
                      ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => 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_account_address_AccountAddressParseError.
  
  Module Impl_core_error_Error_for_move_core_types_account_address_AccountAddressParseError.
    Definition Self : Ty.t := Ty.path "move_core_types::account_address::AccountAddressParseError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_move_core_types_account_address_AccountAddressParseError.
End account_address.
