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

Module runtime_value.
  Definition value_MOVE_STRUCT_NAME : Value.t := M.run ltac:(M.monadic (Value.String "struct")).
  
  Definition value_MOVE_STRUCT_TYPE : Value.t := M.run ltac:(M.monadic (Value.String "type")).
  
  Definition value_MOVE_STRUCT_FIELDS : Value.t := M.run ltac:(M.monadic (Value.String "fields")).
  
  (* StructTuple
    {
      name := "MoveStruct";
      const_params := [];
      ty_params := [];
      fields :=
        [
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [ Ty.path "move_core_types::runtime_value::MoveValue"; Ty.path "alloc::alloc::Global" ]
        ];
    } *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_runtime_value_MoveStruct.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_tuple_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "MoveStruct" |);
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::runtime_value::MoveStruct",
                  0
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_runtime_value_MoveStruct.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_runtime_value_MoveStruct.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_runtime_value_MoveStruct.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_runtime_value_MoveStruct.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    (* 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 "alloc::vec::Vec")
                []
                [
                  Ty.path "move_core_types::runtime_value::MoveValue";
                  Ty.path "alloc::alloc::Global"
                ],
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.path "move_core_types::runtime_value::MoveValue";
                    Ty.path "alloc::alloc::Global"
                  ]
              ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::runtime_value::MoveStruct",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_core_types::runtime_value::MoveStruct",
                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_runtime_value_MoveStruct.
  
  Module Impl_core_cmp_Eq_for_move_core_types_runtime_value_MoveStruct.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    (* 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_runtime_value_MoveStruct.
  
  Module Impl_core_clone_Clone_for_move_core_types_runtime_value_MoveStruct.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    (* 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
          Value.StructTuple
            "move_core_types::runtime_value::MoveStruct"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.path "move_core_types::runtime_value::MoveValue";
                      Ty.path "alloc::alloc::Global"
                    ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "move_core_types::runtime_value::MoveStruct",
                    0
                  |)
                ]
              |)
            ]))
      | _, _, _ => 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_runtime_value_MoveStruct.
  
  (*
  Enum MoveValue
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "U8";
          item := StructTuple [ Ty.path "u8" ];
          discriminant := None;
        };
        {
          name := "U64";
          item := StructTuple [ Ty.path "u64" ];
          discriminant := None;
        };
        {
          name := "U128";
          item := StructTuple [ Ty.path "u128" ];
          discriminant := None;
        };
        {
          name := "Bool";
          item := StructTuple [ Ty.path "bool" ];
          discriminant := None;
        };
        {
          name := "Address";
          item := StructTuple [ Ty.path "move_core_types::account_address::AccountAddress" ];
          discriminant := None;
        };
        {
          name := "Vector";
          item :=
            StructTuple
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.path "move_core_types::runtime_value::MoveValue";
                    Ty.path "alloc::alloc::Global"
                  ]
              ];
          discriminant := None;
        };
        {
          name := "Struct";
          item := StructTuple [ Ty.path "move_core_types::runtime_value::MoveStruct" ];
          discriminant := None;
        };
        {
          name := "Signer";
          item := StructTuple [ Ty.path "move_core_types::account_address::AccountAddress" ];
          discriminant := None;
        };
        {
          name := "U16";
          item := StructTuple [ Ty.path "u16" ];
          discriminant := None;
        };
        {
          name := "U32";
          item := StructTuple [ Ty.path "u32" ];
          discriminant := None;
        };
        {
          name := "U256";
          item := StructTuple [ Ty.path "move_core_types::u256::U256" ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_runtime_value_MoveValue.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    (* 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.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U8",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U8" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U64",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U64" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U128",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U128" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Bool",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Bool" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Address",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Address" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Vector",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Vector" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Struct",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Struct" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Signer",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Signer" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U16",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U16" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U32",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U32" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U256",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U256" |); __self_0 ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_runtime_value_MoveValue.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_core_types_runtime_value_MoveValue.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_core_types_runtime_value_MoveValue.
  
  Module Impl_core_cmp_PartialEq_for_move_core_types_runtime_value_MoveValue.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::runtime_value::MoveValue" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_core_types::runtime_value::MoveValue" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              LogicalOp.and (|
                BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                ltac:(M.monadic
                  (M.read (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::U8",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::U8",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply (Ty.path "&") [] [ Ty.path "u8" ],
                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::U64",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::U64",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply (Ty.path "&") [] [ Ty.path "u64" ],
                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u64" ] ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::U128",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::U128",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply (Ty.path "&") [] [ Ty.path "u128" ],
                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u128" ] ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::Bool",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::Bool",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply (Ty.path "&") [] [ Ty.path "bool" ],
                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "bool" ] ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::Address",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::Address",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_core_types::account_address::AccountAddress" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "move_core_types::account_address::AccountAddress" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::Vector",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::Vector",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path "move_core_types::runtime_value::MoveValue";
                                          Ty.path "alloc::alloc::Global"
                                        ]
                                    ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path "move_core_types::runtime_value::MoveValue";
                                            Ty.path "alloc::alloc::Global"
                                          ]
                                      ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::Struct",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::Struct",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_core_types::runtime_value::MoveStruct" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "move_core_types::runtime_value::MoveStruct" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::Signer",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::Signer",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_core_types::account_address::AccountAddress" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "move_core_types::account_address::AccountAddress" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::U16",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::U16",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply (Ty.path "&") [] [ Ty.path "u16" ],
                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::U32",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::U32",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ] ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "move_core_types::runtime_value::MoveValue::U256",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "move_core_types::runtime_value::MoveValue::U256",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_core_types::u256::U256" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "move_core_types::u256::U256" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.never_to_any (|
                                M.call_closure (|
                                  M.get_function (| "core::intrinsics::unreachable", [] |),
                                  []
                                |)
                              |)
                            |)))
                      ]
                    |)
                  |)))
              |)
            |)
          |)))
      | _, _, _ => 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_runtime_value_MoveValue.
  
  Module Impl_core_cmp_Eq_for_move_core_types_runtime_value_MoveValue.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    (* 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.match_operator (|
                      Value.DeclaredButUndefined,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              Value.DeclaredButUndefined,
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      Value.DeclaredButUndefined,
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              Value.DeclaredButUndefined,
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      Value.DeclaredButUndefined,
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              Value.DeclaredButUndefined,
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.match_operator (|
                                                                      Value.DeclaredButUndefined,
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (M.match_operator (|
                                                                              Value.DeclaredButUndefined,
                                                                              [
                                                                                fun γ =>
                                                                                  ltac:(M.monadic
                                                                                    (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_runtime_value_MoveValue.
  
  Module Impl_core_clone_Clone_for_move_core_types_runtime_value_MoveValue.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    (* 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 (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U8",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::U8"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "u8",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U64",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::U64"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "u64",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U128",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::U128"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "u128",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Bool",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::Bool"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "bool",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Address",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::Address"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "move_core_types::account_address::AccountAddress",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Vector",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::Vector"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.path "move_core_types::runtime_value::MoveValue";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Struct",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::Struct"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "move_core_types::runtime_value::MoveStruct",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Signer",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::Signer"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "move_core_types::account_address::AccountAddress",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U16",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::U16"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "u16",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U32",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::U32"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "u32",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U256",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveValue::U256"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "move_core_types::u256::U256",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_runtime_value_MoveValue.
  
  (* StructTuple
    {
      name := "MoveStructLayout";
      const_params := [];
      ty_params := [];
      fields :=
        [
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [
              Ty.path "move_core_types::runtime_value::MoveTypeLayout";
              Ty.path "alloc::alloc::Global"
            ]
        ];
    } *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_runtime_value_MoveStructLayout.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStructLayout".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_tuple_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "MoveStructLayout" |);
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::runtime_value::MoveStructLayout",
                  0
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_core_types_runtime_value_MoveStructLayout.
  
  Module Impl_core_clone_Clone_for_move_core_types_runtime_value_MoveStructLayout.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStructLayout".
    
    (* 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
          Value.StructTuple
            "move_core_types::runtime_value::MoveStructLayout"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.path "move_core_types::runtime_value::MoveTypeLayout";
                      Ty.path "alloc::alloc::Global"
                    ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "move_core_types::runtime_value::MoveStructLayout",
                    0
                  |)
                ]
              |)
            ]))
      | _, _, _ => 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_runtime_value_MoveStructLayout.
  
  Module underscore.
    Module Impl_serde_ser_Serialize_for_move_core_types_runtime_value_MoveStructLayout.
      Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStructLayout".
      
      (* Serialize *)
      Definition serialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __S ], [ self; __serializer ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let __serializer := M.alloc (| __serializer |) in
            M.call_closure (|
              M.get_trait_method (|
                "serde::ser::Serializer",
                __S,
                [],
                "serialize_newtype_struct",
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.path "move_core_types::runtime_value::MoveTypeLayout";
                      Ty.path "alloc::alloc::Global"
                    ]
                ]
              |),
              [
                M.read (| __serializer |);
                M.read (| Value.String "MoveStructLayout" |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_core_types::runtime_value::MoveStructLayout",
                  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_runtime_value_MoveStructLayout.
    Module Impl_serde_de_Deserialize_for_move_core_types_runtime_value_MoveStructLayout.
      Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStructLayout".
      
      (* Deserialize *)
      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.call_closure (|
              M.get_trait_method (|
                "serde::de::Deserializer",
                __D,
                [],
                "deserialize_newtype_struct",
                [ Ty.path "move_core_types::runtime_value::_'1::deserialize::__Visitor" ]
              |),
              [
                M.read (| __deserializer |);
                M.read (| Value.String "MoveStructLayout" |);
                Value.StructRecord
                  "move_core_types::runtime_value::_'1::deserialize::__Visitor"
                  [
                    ("marker", Value.StructTuple "core::marker::PhantomData" []);
                    ("lifetime", Value.StructTuple "core::marker::PhantomData" [])
                  ]
              ]
            |)))
        | _, _, _ => 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_runtime_value_MoveStructLayout.
    Module Impl_serde_ser_Serialize_for_move_core_types_runtime_value_MoveTypeLayout.
      Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveTypeLayout".
      
      (* Serialize *)
      Definition serialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __S ], [ self; __serializer ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let __serializer := M.alloc (| __serializer |) in
            M.read (|
              M.match_operator (|
                M.read (| self |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::Bool"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 0;
                            M.read (| Value.String "bool" |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::U8"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 1;
                            M.read (| Value.String "u8" |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::U64"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 2;
                            M.read (| Value.String "u64" |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::U128"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 3;
                            M.read (| Value.String "u128" |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::Address"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 4;
                            M.read (| Value.String "address" |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::Vector",
                          0
                        |) in
                      let __field0 := M.alloc (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_newtype_variant",
                            [
                              Ty.apply
                                (Ty.path "alloc::boxed::Box")
                                []
                                [
                                  Ty.path "move_core_types::runtime_value::MoveTypeLayout";
                                  Ty.path "alloc::alloc::Global"
                                ]
                            ]
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 5;
                            M.read (| Value.String "vector" |);
                            M.read (| __field0 |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::Struct",
                          0
                        |) in
                      let __field0 := M.alloc (| γ0_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_newtype_variant",
                            [ Ty.path "move_core_types::runtime_value::MoveStructLayout" ]
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 6;
                            M.read (| Value.String "struct" |);
                            M.read (| __field0 |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::Signer"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 7;
                            M.read (| Value.String "signer" |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::U16"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 8;
                            M.read (| Value.String "u16" |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::U32"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 9;
                            M.read (| Value.String "u32" |)
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_core_types::runtime_value::MoveTypeLayout::U256"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "serde::ser::Serializer",
                            __S,
                            [],
                            "serialize_unit_variant",
                            []
                          |),
                          [
                            M.read (| __serializer |);
                            M.read (| Value.String "MoveTypeLayout" |);
                            Value.Integer IntegerKind.U32 10;
                            M.read (| Value.String "u256" |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => 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_runtime_value_MoveTypeLayout.
    Module Impl_serde_de_Deserialize_for_move_core_types_runtime_value_MoveTypeLayout.
      Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveTypeLayout".
      
      (* Deserialize *)
      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.call_closure (|
              M.get_trait_method (|
                "serde::de::Deserializer",
                __D,
                [],
                "deserialize_enum",
                [ Ty.path "move_core_types::runtime_value::_'3::deserialize::__Visitor" ]
              |),
              [
                M.read (| __deserializer |);
                M.read (| Value.String "MoveTypeLayout" |);
                M.read (|
                  M.get_constant (| "move_core_types::runtime_value::_'3::deserialize::VARIANTS" |)
                |);
                Value.StructRecord
                  "move_core_types::runtime_value::_'3::deserialize::__Visitor"
                  [
                    ("marker", Value.StructTuple "core::marker::PhantomData" []);
                    ("lifetime", Value.StructTuple "core::marker::PhantomData" [])
                  ]
              ]
            |)))
        | _, _, _ => 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_runtime_value_MoveTypeLayout.
  End underscore.
  
  
  (*
  Enum MoveTypeLayout
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Bool";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "U8";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "U64";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "U128";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Address";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Vector";
          item :=
            StructTuple
              [
                Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [
                    Ty.path "move_core_types::runtime_value::MoveTypeLayout";
                    Ty.path "alloc::alloc::Global"
                  ]
              ];
          discriminant := None;
        };
        {
          name := "Struct";
          item := StructTuple [ Ty.path "move_core_types::runtime_value::MoveStructLayout" ];
          discriminant := None;
        };
        {
          name := "Signer";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "U16";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "U32";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "U256";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_fmt_Debug_for_move_core_types_runtime_value_MoveTypeLayout.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveTypeLayout".
    
    (* 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.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Bool"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Bool" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U8"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U8" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U64"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U64" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U128"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U128" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Address"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Address" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Vector",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Vector" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Struct",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Struct" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Signer"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Signer" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U16"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U16" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U32"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U32" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U256"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "U256" |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_runtime_value_MoveTypeLayout.
  
  Module Impl_core_clone_Clone_for_move_core_types_runtime_value_MoveTypeLayout.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveTypeLayout".
    
    (* 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 (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Bool"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::Bool" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U8"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::U8" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U64"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::U64" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U128"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::U128" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Address"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::Address" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Vector",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveTypeLayout::Vector"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.apply
                                (Ty.path "alloc::boxed::Box")
                                []
                                [
                                  Ty.path "move_core_types::runtime_value::MoveTypeLayout";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Struct",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::runtime_value::MoveTypeLayout::Struct"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "move_core_types::runtime_value::MoveStructLayout",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Signer"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::Signer" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U16"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::U16" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U32"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::U32" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U256"
                      |) in
                    M.alloc (|
                      Value.StructTuple "move_core_types::runtime_value::MoveTypeLayout::U256" []
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_runtime_value_MoveTypeLayout.
  
  
  
  Module Impl_move_core_types_runtime_value_MoveValue.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    (*
        pub fn simple_deserialize(blob: &[u8], ty: &MoveTypeLayout) -> AResult<Self> {
            Ok(bcs::from_bytes_seed(ty, blob)?)
        }
    *)
    Definition simple_deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ blob; ty ] =>
        ltac:(M.monadic
          (let blob := M.alloc (| blob |) in
          let ty := M.alloc (| ty |) in
          M.catch_return (|
            ltac:(M.monadic
              (Value.StructTuple
                "core::result::Result::Ok"
                [
                  M.read (|
                    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::runtime_value::MoveValue";
                                Ty.path "bcs::error::Error"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_function (|
                                "bcs::de::from_bytes_seed",
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ]
                                ]
                              |),
                              [ M.read (| ty |); M.read (| blob |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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::runtime_value::MoveValue";
                                            Ty.path "anyhow::Error"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "bcs::error::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))
                      ]
                    |)
                  |)
                ]))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_simple_deserialize :
      M.IsAssociatedFunction Self "simple_deserialize" simple_deserialize.
    
    (*
        pub fn simple_serialize(&self) -> Option<Vec<u8>> {
            bcs::to_bytes(self).ok()
        }
    *)
    Definition simple_serialize (ε : 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 "core::result::Result")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ];
                  Ty.path "bcs::error::Error"
                ],
              "ok",
              []
            |),
            [
              M.call_closure (|
                M.get_function (|
                  "bcs::ser::to_bytes",
                  [ Ty.path "move_core_types::runtime_value::MoveValue" ]
                |),
                [ M.read (| self |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_simple_serialize :
      M.IsAssociatedFunction Self "simple_serialize" simple_serialize.
    
    (*
        pub fn vector_u8(v: Vec<u8>) -> Self {
            MoveValue::Vector(v.into_iter().map(MoveValue::U8).collect())
        }
    *)
    Definition vector_u8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          Value.StructTuple
            "move_core_types::runtime_value::MoveValue::Vector"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply
                    (Ty.path "core::iter::adapters::map::Map")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::into_iter::IntoIter")
                        []
                        [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ];
                      Ty.function
                        [ Ty.path "u8" ]
                        (Ty.path "move_core_types::runtime_value::MoveValue")
                    ],
                  [],
                  "collect",
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "move_core_types::runtime_value::MoveValue";
                        Ty.path "alloc::alloc::Global"
                      ]
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.apply
                        (Ty.path "alloc::vec::into_iter::IntoIter")
                        []
                        [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                      [],
                      "map",
                      [
                        Ty.path "move_core_types::runtime_value::MoveValue";
                        Ty.function
                          [ Ty.path "u8" ]
                          (Ty.path "move_core_types::runtime_value::MoveValue")
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                          [],
                          "into_iter",
                          []
                        |),
                        [ M.read (| v |) ]
                      |);
                      M.constructor_as_closure "move_core_types::runtime_value::MoveValue::U8"
                    ]
                  |)
                ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_vector_u8 : M.IsAssociatedFunction Self "vector_u8" vector_u8.
    
    (*
        pub fn vec_to_vec_u8(vec: Vec<MoveValue>) -> AResult<Vec<u8>> {
            let mut vec_u8 = Vec::with_capacity(vec.len());
    
            for byte in vec {
                match byte {
                    MoveValue::U8(u8) => {
                        vec_u8.push(u8);
                    }
                    _ => {
                        return Err(anyhow!(
                            "Expected inner MoveValue in Vec<MoveValue> to be a MoveValue::U8"
                                .to_string(),
                        ));
                    }
                }
            }
            Ok(vec_u8)
        }
    *)
    Definition vec_to_vec_u8 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ vec ] =>
        ltac:(M.monadic
          (let vec := M.alloc (| vec |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ vec_u8 :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                        "with_capacity",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.path "alloc::alloc::Global"
                              ],
                            "len",
                            []
                          |),
                          [ vec ]
                        |)
                      ]
                    |)
                  |) 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 "alloc::vec::Vec")
                              []
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.path "alloc::alloc::Global"
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| vec |) ]
                        |)
                      |),
                      [
                        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 "alloc::vec::into_iter::IntoIter")
                                            []
                                            [
                                              Ty.path "move_core_types::runtime_value::MoveValue";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          [],
                                          "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
                                          M.match_operator (|
                                            byte,
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_core_types::runtime_value::MoveValue::U8",
                                                      0
                                                    |) in
                                                  let u8 := M.copy (| γ0_0 |) in
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "alloc::vec::Vec")
                                                            []
                                                            [
                                                              Ty.path "u8";
                                                              Ty.path "alloc::alloc::Global"
                                                            ],
                                                          "push",
                                                          []
                                                        |),
                                                        [ vec_u8; M.read (| u8 |) ]
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          Value.StructTuple
                                                            "core::result::Result::Err"
                                                            [
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "anyhow::__private::must_use",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (|
                                                                    let~ error :=
                                                                      M.copy (|
                                                                        M.match_operator (|
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "alloc::string::ToString",
                                                                                Ty.path "str",
                                                                                [],
                                                                                "to_string",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.read (|
                                                                                  Value.String
                                                                                    "Expected inner MoveValue in Vec<MoveValue> to be a MoveValue::U8"
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          |),
                                                                          [
                                                                            fun γ =>
                                                                              ltac:(M.monadic
                                                                                (let error :=
                                                                                  M.copy (| γ |) in
                                                                                M.alloc (|
                                                                                  M.call_closure (|
                                                                                    M.get_associated_function (|
                                                                                      Ty.path
                                                                                        "anyhow::kind::Adhoc",
                                                                                      "new",
                                                                                      [
                                                                                        Ty.path
                                                                                          "alloc::string::String"
                                                                                      ]
                                                                                    |),
                                                                                    [
                                                                                      M.call_closure (|
                                                                                        M.get_trait_method (|
                                                                                          "anyhow::kind::AdhocKind",
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "&")
                                                                                            []
                                                                                            [
                                                                                              Ty.path
                                                                                                "alloc::string::String"
                                                                                            ],
                                                                                          [],
                                                                                          "anyhow_kind",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.alloc (|
                                                                                            error
                                                                                          |)
                                                                                        ]
                                                                                      |);
                                                                                      M.read (|
                                                                                        error
                                                                                      |)
                                                                                    ]
                                                                                  |)
                                                                                |)))
                                                                          ]
                                                                        |)
                                                                      |) in
                                                                    error
                                                                  |)
                                                                ]
                                                              |)
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| vec_u8 |) ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_vec_to_vec_u8 :
      M.IsAssociatedFunction Self "vec_to_vec_u8" vec_to_vec_u8.
    
    (*
        pub fn vector_address(v: Vec<AccountAddress>) -> Self {
            MoveValue::Vector(v.into_iter().map(MoveValue::Address).collect())
        }
    *)
    Definition vector_address (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ v ] =>
        ltac:(M.monadic
          (let v := M.alloc (| v |) in
          Value.StructTuple
            "move_core_types::runtime_value::MoveValue::Vector"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply
                    (Ty.path "core::iter::adapters::map::Map")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::into_iter::IntoIter")
                        []
                        [
                          Ty.path "move_core_types::account_address::AccountAddress";
                          Ty.path "alloc::alloc::Global"
                        ];
                      Ty.function
                        [ Ty.path "move_core_types::account_address::AccountAddress" ]
                        (Ty.path "move_core_types::runtime_value::MoveValue")
                    ],
                  [],
                  "collect",
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "move_core_types::runtime_value::MoveValue";
                        Ty.path "alloc::alloc::Global"
                      ]
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.apply
                        (Ty.path "alloc::vec::into_iter::IntoIter")
                        []
                        [
                          Ty.path "move_core_types::account_address::AccountAddress";
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "map",
                      [
                        Ty.path "move_core_types::runtime_value::MoveValue";
                        Ty.function
                          [ Ty.path "move_core_types::account_address::AccountAddress" ]
                          (Ty.path "move_core_types::runtime_value::MoveValue")
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.path "move_core_types::account_address::AccountAddress";
                              Ty.path "alloc::alloc::Global"
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [ M.read (| v |) ]
                      |);
                      M.constructor_as_closure "move_core_types::runtime_value::MoveValue::Address"
                    ]
                  |)
                ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_vector_address :
      M.IsAssociatedFunction Self "vector_address" vector_address.
    
    (*
        pub fn decorate(self, layout: &A::MoveTypeLayout) -> A::MoveValue {
            match (self, layout) {
                (MoveValue::Struct(s), A::MoveTypeLayout::Struct(l)) => {
                    A::MoveValue::Struct(s.decorate(l))
                }
                (MoveValue::Vector(vals), A::MoveTypeLayout::Vector(t)) => {
                    A::MoveValue::Vector(vals.into_iter().map(|v| v.decorate(t)).collect())
                }
                (MoveValue::U8(a), _) => A::MoveValue::U8(a),
                (MoveValue::U64(u), _) => A::MoveValue::U64(u),
                (MoveValue::U128(u), _) => A::MoveValue::U128(u),
                (MoveValue::Bool(b), _) => A::MoveValue::Bool(b),
                (MoveValue::Address(a), _) => A::MoveValue::Address(a),
                (MoveValue::Signer(a), _) => A::MoveValue::Signer(a),
                (MoveValue::U16(u), _) => A::MoveValue::U16(u),
                (MoveValue::U32(u), _) => A::MoveValue::U32(u),
                (MoveValue::U256(u), _) => A::MoveValue::U256(u),
                _ => panic!("Invalid decoration"),
            }
        }
    *)
    Definition decorate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let layout := M.alloc (| layout |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [ M.read (| self |); M.read (| layout |) ] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::Struct",
                        0
                      |) in
                    let s := M.copy (| γ1_0 |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "move_core_types::annotated_value::MoveTypeLayout::Struct",
                        0
                      |) in
                    let l := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::Struct"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_core_types::runtime_value::MoveStruct",
                              "decorate",
                              []
                            |),
                            [ M.read (| s |); M.read (| l |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::Vector",
                        0
                      |) in
                    let vals := M.copy (| γ1_0 |) in
                    let γ0_1 := M.read (| γ0_1 |) in
                    let γ2_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_1,
                        "move_core_types::annotated_value::MoveTypeLayout::Vector",
                        0
                      |) in
                    let t := M.alloc (| γ2_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::Vector"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply
                                (Ty.path "core::iter::adapters::map::Map")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloc::vec::into_iter::IntoIter")
                                    []
                                    [
                                      Ty.path "move_core_types::runtime_value::MoveValue";
                                      Ty.path "alloc::alloc::Global"
                                    ];
                                  Ty.function
                                    [
                                      Ty.tuple
                                        [ Ty.path "move_core_types::runtime_value::MoveValue" ]
                                    ]
                                    (Ty.path "move_core_types::annotated_value::MoveValue")
                                ],
                              [],
                              "collect",
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.path "move_core_types::annotated_value::MoveValue";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "alloc::vec::into_iter::IntoIter")
                                    []
                                    [
                                      Ty.path "move_core_types::runtime_value::MoveValue";
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  [],
                                  "map",
                                  [
                                    Ty.path "move_core_types::annotated_value::MoveValue";
                                    Ty.function
                                      [
                                        Ty.tuple
                                          [ Ty.path "move_core_types::runtime_value::MoveValue" ]
                                      ]
                                      (Ty.path "move_core_types::annotated_value::MoveValue")
                                  ]
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::collect::IntoIterator",
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path "move_core_types::runtime_value::MoveValue";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      [],
                                      "into_iter",
                                      []
                                    |),
                                    [ M.read (| vals |) ]
                                  |);
                                  M.closure
                                    (fun γ =>
                                      ltac:(M.monadic
                                        match γ with
                                        | [ α0 ] =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              M.alloc (| α0 |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let v := M.copy (| γ |) in
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "move_core_types::runtime_value::MoveValue",
                                                        "decorate",
                                                        []
                                                      |),
                                                      [ M.read (| v |); M.read (| M.read (| t |) |)
                                                      ]
                                                    |)))
                                              ]
                                            |)))
                                        | _ => M.impossible "wrong number of arguments"
                                        end))
                                ]
                              |)
                            ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::U8",
                        0
                      |) in
                    let a := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::U8"
                        [ M.read (| a |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::U64",
                        0
                      |) in
                    let u := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::U64"
                        [ M.read (| u |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::U128",
                        0
                      |) in
                    let u := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::U128"
                        [ M.read (| u |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::Bool",
                        0
                      |) in
                    let b := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::Bool"
                        [ M.read (| b |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::Address",
                        0
                      |) in
                    let a := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::Address"
                        [ M.read (| a |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::Signer",
                        0
                      |) in
                    let a := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::Signer"
                        [ M.read (| a |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::U16",
                        0
                      |) in
                    let u := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::U16"
                        [ M.read (| u |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::U32",
                        0
                      |) in
                    let u := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::U32"
                        [ M.read (| u |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ0_0,
                        "move_core_types::runtime_value::MoveValue::U256",
                        0
                      |) in
                    let u := M.copy (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_core_types::annotated_value::MoveValue::U256"
                        [ M.read (| u |) ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_fmt", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_const",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array [ M.read (| Value.String "Invalid decoration" |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_decorate : M.IsAssociatedFunction Self "decorate" decorate.
  End Impl_move_core_types_runtime_value_MoveValue.
  
  (*
  pub fn serialize_values<'a, I>(vals: I) -> Vec<Vec<u8>>
  where
      I: IntoIterator<Item = &'a MoveValue>,
  {
      vals.into_iter()
          .map(|val| {
              val.simple_serialize()
                  .expect("serialization should succeed")
          })
          .collect()
  }
  *)
  Definition serialize_values (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ _ as I ], [ vals ] =>
      ltac:(M.monadic
        (let vals := M.alloc (| vals |) in
        M.call_closure (|
          M.get_trait_method (|
            "core::iter::traits::iterator::Iterator",
            Ty.apply
              (Ty.path "core::iter::adapters::map::Map")
              []
              [
                Ty.associated;
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [ Ty.path "move_core_types::runtime_value::MoveValue" ]
                      ]
                  ]
                  (Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ])
              ],
            [],
            "collect",
            [
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ];
                  Ty.path "alloc::alloc::Global"
                ]
            ]
          |),
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.associated,
                [],
                "map",
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ];
                  Ty.function
                    [
                      Ty.tuple
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [ Ty.path "move_core_types::runtime_value::MoveValue" ]
                        ]
                    ]
                    (Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::IntoIterator",
                    I,
                    [],
                    "into_iter",
                    []
                  |),
                  [ M.read (| vals |) ]
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let val := M.copy (| γ |) in
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                                        ],
                                      "expect",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_core_types::runtime_value::MoveValue",
                                          "simple_serialize",
                                          []
                                        |),
                                        [ M.read (| val |) ]
                                      |);
                                      M.read (| Value.String "serialization should succeed" |)
                                    ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_serialize_values :
    M.IsFunction "move_core_types::runtime_value::serialize_values" serialize_values.
  
  Module Impl_move_core_types_runtime_value_MoveStruct.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    (*
        pub fn new(value: Vec<MoveValue>) -> Self {
            Self(value)
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ value ] =>
        ltac:(M.monadic
          (let value := M.alloc (| value |) in
          Value.StructTuple "move_core_types::runtime_value::MoveStruct" [ M.read (| value |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn simple_deserialize(blob: &[u8], ty: &MoveStructLayout) -> AResult<Self> {
            Ok(bcs::from_bytes_seed(ty, blob)?)
        }
    *)
    Definition simple_deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ blob; ty ] =>
        ltac:(M.monadic
          (let blob := M.alloc (| blob |) in
          let ty := M.alloc (| ty |) in
          M.catch_return (|
            ltac:(M.monadic
              (Value.StructTuple
                "core::result::Result::Ok"
                [
                  M.read (|
                    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::runtime_value::MoveStruct";
                                Ty.path "bcs::error::Error"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_function (|
                                "bcs::de::from_bytes_seed",
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "move_core_types::runtime_value::MoveStructLayout" ]
                                ]
                              |),
                              [ M.read (| ty |); M.read (| blob |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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::runtime_value::MoveStruct";
                                            Ty.path "anyhow::Error"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "bcs::error::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))
                      ]
                    |)
                  |)
                ]))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_simple_deserialize :
      M.IsAssociatedFunction Self "simple_deserialize" simple_deserialize.
    
    (*
        pub fn decorate(self, layout: &A::MoveStructLayout) -> A::MoveStruct {
            let MoveStruct(vals) = self;
            let A::MoveStructLayout { type_, fields } = layout;
            A::MoveStruct {
                type_: type_.clone(),
                fields: vals
                    .into_iter()
                    .zip(fields)
                    .map(|(v, l)| (l.name.clone(), v.decorate(&l.layout)))
                    .collect(),
            }
        }
    *)
    Definition decorate (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; layout ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let layout := M.alloc (| layout |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveStruct",
                        0
                      |) in
                    let vals := M.copy (| γ0_0 |) in
                    M.match_operator (|
                      layout,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_record_field (|
                                γ,
                                "move_core_types::annotated_value::MoveStructLayout",
                                "type_"
                              |) in
                            let γ1_1 :=
                              M.SubPointer.get_struct_record_field (|
                                γ,
                                "move_core_types::annotated_value::MoveStructLayout",
                                "fields"
                              |) in
                            let type_ := M.alloc (| γ1_0 |) in
                            let fields := M.alloc (| γ1_1 |) in
                            M.alloc (|
                              Value.StructRecord
                                "move_core_types::annotated_value::MoveStruct"
                                [
                                  ("type_",
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::clone::Clone",
                                        Ty.path "move_core_types::language_storage::StructTag",
                                        [],
                                        "clone",
                                        []
                                      |),
                                      [ M.read (| type_ |) ]
                                    |));
                                  ("fields",
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::iter::traits::iterator::Iterator",
                                        Ty.apply
                                          (Ty.path "core::iter::adapters::map::Map")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::iter::adapters::zip::Zip")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::vec::into_iter::IntoIter")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::runtime_value::MoveValue";
                                                    Ty.path "alloc::alloc::Global"
                                                  ];
                                                Ty.apply
                                                  (Ty.path "core::slice::iter::Iter")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::annotated_value::MoveFieldLayout"
                                                  ]
                                              ];
                                            Ty.function
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.path
                                                          "move_core_types::runtime_value::MoveValue";
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_core_types::annotated_value::MoveFieldLayout"
                                                          ]
                                                      ]
                                                  ]
                                              ]
                                              (Ty.tuple
                                                [
                                                  Ty.path "move_core_types::identifier::Identifier";
                                                  Ty.path
                                                    "move_core_types::annotated_value::MoveValue"
                                                ])
                                          ],
                                        [],
                                        "collect",
                                        [
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.path "move_core_types::identifier::Identifier";
                                                  Ty.path
                                                    "move_core_types::annotated_value::MoveValue"
                                                ];
                                              Ty.path "alloc::alloc::Global"
                                            ]
                                        ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::iter::adapters::zip::Zip")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::vec::into_iter::IntoIter")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::runtime_value::MoveValue";
                                                    Ty.path "alloc::alloc::Global"
                                                  ];
                                                Ty.apply
                                                  (Ty.path "core::slice::iter::Iter")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::annotated_value::MoveFieldLayout"
                                                  ]
                                              ],
                                            [],
                                            "map",
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.path "move_core_types::identifier::Identifier";
                                                  Ty.path
                                                    "move_core_types::annotated_value::MoveValue"
                                                ];
                                              Ty.function
                                                [
                                                  Ty.tuple
                                                    [
                                                      Ty.tuple
                                                        [
                                                          Ty.path
                                                            "move_core_types::runtime_value::MoveValue";
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              Ty.path
                                                                "move_core_types::annotated_value::MoveFieldLayout"
                                                            ]
                                                        ]
                                                    ]
                                                ]
                                                (Ty.tuple
                                                  [
                                                    Ty.path
                                                      "move_core_types::identifier::Identifier";
                                                    Ty.path
                                                      "move_core_types::annotated_value::MoveValue"
                                                  ])
                                            ]
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::iter::traits::iterator::Iterator",
                                                Ty.apply
                                                  (Ty.path "alloc::vec::into_iter::IntoIter")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::runtime_value::MoveValue";
                                                    Ty.path "alloc::alloc::Global"
                                                  ],
                                                [],
                                                "zip",
                                                [
                                                  Ty.apply
                                                    (Ty.path "&")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_core_types::annotated_value::MoveFieldLayout";
                                                          Ty.path "alloc::alloc::Global"
                                                        ]
                                                    ]
                                                ]
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::collect::IntoIterator",
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::Vec")
                                                      []
                                                      [
                                                        Ty.path
                                                          "move_core_types::runtime_value::MoveValue";
                                                        Ty.path "alloc::alloc::Global"
                                                      ],
                                                    [],
                                                    "into_iter",
                                                    []
                                                  |),
                                                  [ M.read (| vals |) ]
                                                |);
                                                M.read (| fields |)
                                              ]
                                            |);
                                            M.closure
                                              (fun γ =>
                                                ltac:(M.monadic
                                                  match γ with
                                                  | [ α0 ] =>
                                                    ltac:(M.monadic
                                                      (M.match_operator (|
                                                        M.alloc (| α0 |),
                                                        [
                                                          fun γ =>
                                                            ltac:(M.monadic
                                                              (let γ0_0 :=
                                                                M.SubPointer.get_tuple_field (|
                                                                  γ,
                                                                  0
                                                                |) in
                                                              let γ0_1 :=
                                                                M.SubPointer.get_tuple_field (|
                                                                  γ,
                                                                  1
                                                                |) in
                                                              let v := M.copy (| γ0_0 |) in
                                                              let l := M.copy (| γ0_1 |) in
                                                              Value.Tuple
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::clone::Clone",
                                                                      Ty.path
                                                                        "move_core_types::identifier::Identifier",
                                                                      [],
                                                                      "clone",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| l |),
                                                                        "move_core_types::annotated_value::MoveFieldLayout",
                                                                        "name"
                                                                      |)
                                                                    ]
                                                                  |);
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "move_core_types::runtime_value::MoveValue",
                                                                      "decorate",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.read (| v |);
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| l |),
                                                                        "move_core_types::annotated_value::MoveFieldLayout",
                                                                        "layout"
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]))
                                                        ]
                                                      |)))
                                                  | _ => M.impossible "wrong number of arguments"
                                                  end))
                                          ]
                                        |)
                                      ]
                                    |))
                                ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_decorate : M.IsAssociatedFunction Self "decorate" decorate.
    
    (*
        pub fn fields(&self) -> &[MoveValue] {
            &self.0
        }
    *)
    Definition fields (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::deref::Deref",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.path "move_core_types::runtime_value::MoveValue";
                  Ty.path "alloc::alloc::Global"
                ],
              [],
              "deref",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::runtime_value::MoveStruct",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_fields : M.IsAssociatedFunction Self "fields" fields.
    
    (*
        pub fn into_fields(self) -> Vec<MoveValue> {
            self.0
        }
    *)
    Definition into_fields (ε : 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::runtime_value::MoveStruct",
              0
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_fields : M.IsAssociatedFunction Self "into_fields" into_fields.
  End Impl_move_core_types_runtime_value_MoveStruct.
  
  Module Impl_move_core_types_runtime_value_MoveStructLayout.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStructLayout".
    
    (*
        pub fn new(types: Vec<MoveTypeLayout>) -> Self {
            Self(types)
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ types ] =>
        ltac:(M.monadic
          (let types := M.alloc (| types |) in
          Value.StructTuple
            "move_core_types::runtime_value::MoveStructLayout"
            [ M.read (| types |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn fields(&self) -> &[MoveTypeLayout] {
            &self.0
        }
    *)
    Definition fields (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::deref::Deref",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.path "move_core_types::runtime_value::MoveTypeLayout";
                  Ty.path "alloc::alloc::Global"
                ],
              [],
              "deref",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::runtime_value::MoveStructLayout",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_fields : M.IsAssociatedFunction Self "fields" fields.
    
    (*
        pub fn into_fields(self) -> Vec<MoveTypeLayout> {
            self.0
        }
    *)
    Definition into_fields (ε : 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::runtime_value::MoveStructLayout",
              0
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_into_fields : M.IsAssociatedFunction Self "into_fields" into_fields.
  End Impl_move_core_types_runtime_value_MoveStructLayout.
  
  Module Impl_serde_de_DeserializeSeed_for_ref__move_core_types_runtime_value_MoveTypeLayout.
    Definition Self : Ty.t :=
      Ty.apply (Ty.path "&") [] [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ].
    
    (*     type Value = MoveValue; *)
    Definition _Value : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    (*
        fn deserialize<D: serde::de::Deserializer<'d>>(
            self,
            deserializer: D,
        ) -> Result<Self::Value, D::Error> {
            match self {
                MoveTypeLayout::Bool => bool::deserialize(deserializer).map(MoveValue::Bool),
                MoveTypeLayout::U8 => u8::deserialize(deserializer).map(MoveValue::U8),
                MoveTypeLayout::U16 => u16::deserialize(deserializer).map(MoveValue::U16),
                MoveTypeLayout::U32 => u32::deserialize(deserializer).map(MoveValue::U32),
                MoveTypeLayout::U64 => u64::deserialize(deserializer).map(MoveValue::U64),
                MoveTypeLayout::U128 => u128::deserialize(deserializer).map(MoveValue::U128),
                MoveTypeLayout::U256 => u256::U256::deserialize(deserializer).map(MoveValue::U256),
                MoveTypeLayout::Address => {
                    AccountAddress::deserialize(deserializer).map(MoveValue::Address)
                }
                MoveTypeLayout::Signer => {
                    AccountAddress::deserialize(deserializer).map(MoveValue::Signer)
                }
                MoveTypeLayout::Struct(ty) => Ok(MoveValue::Struct(ty.deserialize(deserializer)?)),
                MoveTypeLayout::Vector(layout) => Ok(MoveValue::Vector(
                    deserializer.deserialize_seq(VectorElementVisitor(layout))?,
                )),
            }
        }
    *)
    Definition deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ D ], [ self; deserializer ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let deserializer := M.alloc (| deserializer |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::Bool"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [ Ty.path "bool"; Ty.associated ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "bool" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "bool",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::Bool"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::U8"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [ Ty.path "u8"; Ty.associated ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "u8" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "u8",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::U8"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::U16"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [ Ty.path "u16"; Ty.associated ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "u16" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "u16",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::U16"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::U32"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [ Ty.path "u32"; Ty.associated ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "u32" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "u32",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::U32"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::U64"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [ Ty.path "u64"; Ty.associated ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "u64" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "u64",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::U64"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::U128"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [ Ty.path "u128"; Ty.associated ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "u128" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "u128",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::U128"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::U256"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [ Ty.path "move_core_types::u256::U256"; Ty.associated ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "move_core_types::u256::U256" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "move_core_types::u256::U256",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::U256"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::Address"
                          |) 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.associated
                                ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "move_core_types::account_address::AccountAddress" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "move_core_types::account_address::AccountAddress",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::Address"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::Signer"
                          |) 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.associated
                                ],
                              "map",
                              [
                                Ty.path "move_core_types::runtime_value::MoveValue";
                                Ty.function
                                  [ Ty.path "move_core_types::account_address::AccountAddress" ]
                                  (Ty.path "move_core_types::runtime_value::MoveValue")
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "serde::de::Deserialize",
                                  Ty.path "move_core_types::account_address::AccountAddress",
                                  [],
                                  "deserialize",
                                  [ D ]
                                |),
                                [ M.read (| deserializer |) ]
                              |);
                              M.constructor_as_closure
                                "move_core_types::runtime_value::MoveValue::Signer"
                            ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::Struct",
                            0
                          |) in
                        let ty := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              Value.StructTuple
                                "move_core_types::runtime_value::MoveValue::Struct"
                                [
                                  M.read (|
                                    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::runtime_value::MoveStruct";
                                                Ty.associated
                                              ],
                                            [],
                                            "branch",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "serde::de::DeserializeSeed",
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::runtime_value::MoveStructLayout"
                                                  ],
                                                [],
                                                "deserialize",
                                                [ D ]
                                              |),
                                              [ M.read (| ty |); 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::runtime_value::MoveValue";
                                                            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))
                                      ]
                                    |)
                                  |)
                                ]
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveTypeLayout::Vector",
                            0
                          |) in
                        let layout := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "core::result::Result::Ok"
                            [
                              Value.StructTuple
                                "move_core_types::runtime_value::MoveValue::Vector"
                                [
                                  M.read (|
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::Try",
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::runtime_value::MoveValue";
                                                    Ty.path "alloc::alloc::Global"
                                                  ];
                                                Ty.associated
                                              ],
                                            [],
                                            "branch",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "serde::de::Deserializer",
                                                D,
                                                [],
                                                "deserialize_seq",
                                                [
                                                  Ty.path
                                                    "move_core_types::runtime_value::VectorElementVisitor"
                                                ]
                                              |),
                                              [
                                                M.read (| deserializer |);
                                                Value.StructTuple
                                                  "move_core_types::runtime_value::VectorElementVisitor"
                                                  [ M.read (| M.read (| layout |) |) ]
                                              ]
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        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::runtime_value::MoveValue";
                                                            Ty.associated
                                                          ],
                                                        [
                                                          Ty.apply
                                                            (Ty.path "core::result::Result")
                                                            []
                                                            [
                                                              Ty.path "core::convert::Infallible";
                                                              Ty.associated
                                                            ]
                                                        ],
                                                        "from_residual",
                                                        []
                                                      |),
                                                      [ M.read (| residual |) ]
                                                    |)
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::ops::control_flow::ControlFlow::Continue",
                                                0
                                              |) in
                                            let val := M.copy (| γ0_0 |) in
                                            val))
                                      ]
                                    |)
                                  |)
                                ]
                            ]
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "serde::de::DeserializeSeed"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("Value", InstanceField.Ty _Value); ("deserialize", InstanceField.Method deserialize) ].
  End Impl_serde_de_DeserializeSeed_for_ref__move_core_types_runtime_value_MoveTypeLayout.
  
  (* StructTuple
    {
      name := "VectorElementVisitor";
      const_params := [];
      ty_params := [];
      fields :=
        [ Ty.apply (Ty.path "&") [] [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ] ];
    } *)
  
  Module Impl_serde_de_Visitor_for_move_core_types_runtime_value_VectorElementVisitor.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::VectorElementVisitor".
    
    (*     type Value = Vec<MoveValue>; *)
    Definition _Value : Ty.t :=
      Ty.apply
        (Ty.path "alloc::vec::Vec")
        []
        [ Ty.path "move_core_types::runtime_value::MoveValue"; Ty.path "alloc::alloc::Global" ].
    
    (*
        fn expecting(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
            formatter.write_str("Vector")
        }
    *)
    Definition expecting (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; formatter ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let formatter := M.alloc (| formatter |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [ M.read (| formatter |); M.read (| Value.String "Vector" |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn visit_seq<A>(self, mut seq: A) -> Result<Self::Value, A::Error>
        where
            A: serde::de::SeqAccess<'d>,
        {
            let mut vals = Vec::new();
            while let Some(elem) = seq.next_element_seed(self.0)? {
                vals.push(elem)
            }
            Ok(vals)
        }
    *)
    Definition visit_seq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ A ], [ self; seq ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let seq := M.alloc (| seq |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ vals :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.path "move_core_types::runtime_value::MoveValue";
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      []
                    |)
                  |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (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.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "move_core_types::runtime_value::MoveValue"
                                              ];
                                            Ty.associated
                                          ],
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "serde::de::SeqAccess",
                                            A,
                                            [],
                                            "next_element_seed",
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [
                                                  Ty.path
                                                    "move_core_types::runtime_value::MoveTypeLayout"
                                                ]
                                            ]
                                          |),
                                          [
                                            seq;
                                            M.read (|
                                              M.SubPointer.get_struct_tuple_field (|
                                                self,
                                                "move_core_types::runtime_value::VectorElementVisitor",
                                                0
                                              |)
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    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.apply
                                                          (Ty.path "alloc::vec::Vec")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_core_types::runtime_value::MoveValue";
                                                            Ty.path "alloc::alloc::Global"
                                                          ];
                                                        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
                              let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::option::Option::Some",
                                  0
                                |) in
                              let elem := M.copy (| γ0_0 |) in
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path "move_core_types::runtime_value::MoveValue";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    "push",
                                    []
                                  |),
                                  [ vals; M.read (| elem |) ]
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    let~ _ :=
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| vals |) ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "serde::de::Visitor"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Value", InstanceField.Ty _Value);
          ("expecting", InstanceField.Method expecting);
          ("visit_seq", InstanceField.Method visit_seq)
        ].
  End Impl_serde_de_Visitor_for_move_core_types_runtime_value_VectorElementVisitor.
  
  (* StructTuple
    {
      name := "StructFieldVisitor";
      const_params := [];
      ty_params := [];
      fields :=
        [
          Ty.apply
            (Ty.path "&")
            []
            [
              Ty.apply
                (Ty.path "slice")
                []
                [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ]
            ]
        ];
    } *)
  
  Module Impl_serde_de_Visitor_for_move_core_types_runtime_value_StructFieldVisitor.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::StructFieldVisitor".
    
    (*     type Value = Vec<MoveValue>; *)
    Definition _Value : Ty.t :=
      Ty.apply
        (Ty.path "alloc::vec::Vec")
        []
        [ Ty.path "move_core_types::runtime_value::MoveValue"; Ty.path "alloc::alloc::Global" ].
    
    (*
        fn expecting(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
            formatter.write_str("Struct")
        }
    *)
    Definition expecting (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; formatter ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let formatter := M.alloc (| formatter |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [ M.read (| formatter |); M.read (| Value.String "Struct" |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn visit_seq<A>(self, mut seq: A) -> Result<Self::Value, A::Error>
        where
            A: serde::de::SeqAccess<'d>,
        {
            let mut val = Vec::new();
            for (i, field_type) in self.0.iter().enumerate() {
                match seq.next_element_seed(field_type)? {
                    Some(elem) => val.push(elem),
                    None => return Err(A::Error::invalid_length(i, &self)),
                }
            }
            Ok(val)
        }
    *)
    Definition visit_seq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ A ], [ self; seq ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let seq := M.alloc (| seq |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ val :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.path "move_core_types::runtime_value::MoveValue";
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      []
                    |)
                  |) 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::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.SubPointer.get_struct_tuple_field (|
                                        self,
                                        "move_core_types::runtime_value::StructFieldVisitor",
                                        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::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_core_types::runtime_value::MoveTypeLayout"
                                                ]
                                            ],
                                          [],
                                          "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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let i := M.copy (| γ1_0 |) in
                                          let field_type := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::try_trait::Try",
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::option::Option")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_core_types::runtime_value::MoveValue"
                                                          ];
                                                        Ty.associated
                                                      ],
                                                    [],
                                                    "branch",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "serde::de::SeqAccess",
                                                        A,
                                                        [],
                                                        "next_element_seed",
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              Ty.path
                                                                "move_core_types::runtime_value::MoveTypeLayout"
                                                            ]
                                                        ]
                                                      |),
                                                      [ seq; M.read (| field_type |) ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                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.apply
                                                                      (Ty.path "alloc::vec::Vec")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "move_core_types::runtime_value::MoveValue";
                                                                        Ty.path
                                                                          "alloc::alloc::Global"
                                                                      ];
                                                                    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))
                                              ]
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let elem := M.copy (| γ0_0 |) in
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "alloc::vec::Vec")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_core_types::runtime_value::MoveValue";
                                                            Ty.path "alloc::alloc::Global"
                                                          ],
                                                        "push",
                                                        []
                                                      |),
                                                      [ val; M.read (| elem |) ]
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (|
                                                        M.return_ (|
                                                          Value.StructTuple
                                                            "core::result::Result::Err"
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "serde::de::Error",
                                                                  Ty.associated,
                                                                  [],
                                                                  "invalid_length",
                                                                  []
                                                                |),
                                                                [ M.read (| i |); self ]
                                                              |)
                                                            ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ M.read (| val |) ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "serde::de::Visitor"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("Value", InstanceField.Ty _Value);
          ("expecting", InstanceField.Method expecting);
          ("visit_seq", InstanceField.Method visit_seq)
        ].
  End Impl_serde_de_Visitor_for_move_core_types_runtime_value_StructFieldVisitor.
  
  Module Impl_serde_de_DeserializeSeed_for_ref__move_core_types_runtime_value_MoveStructLayout.
    Definition Self : Ty.t :=
      Ty.apply (Ty.path "&") [] [ Ty.path "move_core_types::runtime_value::MoveStructLayout" ].
    
    (*     type Value = MoveStruct; *)
    Definition _Value : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    (*
        fn deserialize<D: serde::de::Deserializer<'d>>(
            self,
            deserializer: D,
        ) -> Result<Self::Value, D::Error> {
            Ok(MoveStruct(deserializer.deserialize_tuple(
                self.0.len(),
                StructFieldVisitor(&self.0),
            )?))
        }
    *)
    Definition deserialize (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ D ], [ self; deserializer ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let deserializer := M.alloc (| deserializer |) in
          M.catch_return (|
            ltac:(M.monadic
              (Value.StructTuple
                "core::result::Result::Ok"
                [
                  Value.StructTuple
                    "move_core_types::runtime_value::MoveStruct"
                    [
                      M.read (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path "move_core_types::runtime_value::MoveValue";
                                        Ty.path "alloc::alloc::Global"
                                      ];
                                    Ty.associated
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "serde::de::Deserializer",
                                    D,
                                    [],
                                    "deserialize_tuple",
                                    [ Ty.path "move_core_types::runtime_value::StructFieldVisitor" ]
                                  |),
                                  [
                                    M.read (| deserializer |);
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path
                                              "move_core_types::runtime_value::MoveTypeLayout";
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        "len",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_tuple_field (|
                                          M.read (| self |),
                                          "move_core_types::runtime_value::MoveStructLayout",
                                          0
                                        |)
                                      ]
                                    |);
                                    Value.StructTuple
                                      "move_core_types::runtime_value::StructFieldVisitor"
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::deref::Deref",
                                            Ty.apply
                                              (Ty.path "alloc::vec::Vec")
                                              []
                                              [
                                                Ty.path
                                                  "move_core_types::runtime_value::MoveTypeLayout";
                                                Ty.path "alloc::alloc::Global"
                                              ],
                                            [],
                                            "deref",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_tuple_field (|
                                              M.read (| self |),
                                              "move_core_types::runtime_value::MoveStructLayout",
                                              0
                                            |)
                                          ]
                                        |)
                                      ]
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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::runtime_value::MoveStruct";
                                                Ty.associated
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                []
                                                [ Ty.path "core::convert::Infallible"; Ty.associated
                                                ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |)
                    ]
                ]))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "serde::de::DeserializeSeed"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("Value", InstanceField.Ty _Value); ("deserialize", InstanceField.Method deserialize) ].
  End Impl_serde_de_DeserializeSeed_for_ref__move_core_types_runtime_value_MoveStructLayout.
  
  Module Impl_serde_ser_Serialize_for_move_core_types_runtime_value_MoveValue.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    (*
        fn serialize<S: serde::Serializer>(&self, serializer: S) -> Result<S::Ok, S::Error> {
            match self {
                MoveValue::Struct(s) => s.serialize(serializer),
                MoveValue::Bool(b) => serializer.serialize_bool( *b),
                MoveValue::U8(i) => serializer.serialize_u8( *i),
                MoveValue::U16(i) => serializer.serialize_u16( *i),
                MoveValue::U32(i) => serializer.serialize_u32( *i),
                MoveValue::U64(i) => serializer.serialize_u64( *i),
                MoveValue::U128(i) => serializer.serialize_u128( *i),
                MoveValue::U256(i) => i.serialize(serializer),
                MoveValue::Address(a) => a.serialize(serializer),
                MoveValue::Signer(a) => a.serialize(serializer),
                MoveValue::Vector(v) => {
                    let mut t = serializer.serialize_seq(Some(v.len()))?;
                    for val in v {
                        t.serialize_element(val)?;
                    }
                    t.end()
                }
            }
        }
    *)
    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.catch_return (|
            ltac:(M.monadic
              (M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::Struct",
                            0
                          |) in
                        let s := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serialize",
                              Ty.path "move_core_types::runtime_value::MoveStruct",
                              [],
                              "serialize",
                              [ S ]
                            |),
                            [ M.read (| s |); M.read (| serializer |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::Bool",
                            0
                          |) in
                        let b := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              S,
                              [],
                              "serialize_bool",
                              []
                            |),
                            [ M.read (| serializer |); M.read (| M.read (| b |) |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::U8",
                            0
                          |) in
                        let i := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              S,
                              [],
                              "serialize_u8",
                              []
                            |),
                            [ M.read (| serializer |); M.read (| M.read (| i |) |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::U16",
                            0
                          |) in
                        let i := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              S,
                              [],
                              "serialize_u16",
                              []
                            |),
                            [ M.read (| serializer |); M.read (| M.read (| i |) |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::U32",
                            0
                          |) in
                        let i := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              S,
                              [],
                              "serialize_u32",
                              []
                            |),
                            [ M.read (| serializer |); M.read (| M.read (| i |) |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::U64",
                            0
                          |) in
                        let i := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              S,
                              [],
                              "serialize_u64",
                              []
                            |),
                            [ M.read (| serializer |); M.read (| M.read (| i |) |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::U128",
                            0
                          |) in
                        let i := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serializer",
                              S,
                              [],
                              "serialize_u128",
                              []
                            |),
                            [ M.read (| serializer |); M.read (| M.read (| i |) |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::U256",
                            0
                          |) in
                        let i := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serialize",
                              Ty.path "move_core_types::u256::U256",
                              [],
                              "serialize",
                              [ S ]
                            |),
                            [ M.read (| i |); M.read (| serializer |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::Address",
                            0
                          |) in
                        let a := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serialize",
                              Ty.path "move_core_types::account_address::AccountAddress",
                              [],
                              "serialize",
                              [ S ]
                            |),
                            [ M.read (| a |); M.read (| serializer |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::Signer",
                            0
                          |) in
                        let a := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::Serialize",
                              Ty.path "move_core_types::account_address::AccountAddress",
                              [],
                              "serialize",
                              [ S ]
                            |),
                            [ M.read (| a |); M.read (| serializer |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "move_core_types::runtime_value::MoveValue::Vector",
                            0
                          |) in
                        let v := M.alloc (| γ1_0 |) in
                        let~ t :=
                          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.associated; Ty.associated ],
                                    [],
                                    "branch",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "serde::ser::Serializer",
                                        S,
                                        [],
                                        "serialize_seq",
                                        []
                                      |),
                                      [
                                        M.read (| serializer |);
                                        Value.StructTuple
                                          "core::option::Option::Some"
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::runtime_value::MoveValue";
                                                    Ty.path "alloc::alloc::Global"
                                                  ],
                                                "len",
                                                []
                                              |),
                                              [ M.read (| v |) ]
                                            |)
                                          ]
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                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.associated; 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
                        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 "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path "move_core_types::runtime_value::MoveValue";
                                            Ty.path "alloc::alloc::Global"
                                          ]
                                      ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [ M.read (| v |) ]
                                |)
                              |),
                              [
                                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
                                                        "move_core_types::runtime_value::MoveValue"
                                                    ],
                                                  [],
                                                  "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 val := 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.associated ],
                                                            [],
                                                            "branch",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "serde::ser::SerializeSeq",
                                                                Ty.associated,
                                                                [],
                                                                "serialize_element",
                                                                [
                                                                  Ty.path
                                                                    "move_core_types::runtime_value::MoveValue"
                                                                ]
                                                              |),
                                                              [ t; M.read (| val |) ]
                                                            |)
                                                          ]
                                                        |)
                                                      |),
                                                      [
                                                        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.associated;
                                                                            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.Tuple [] |)))
                                            ]
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                    |)))
                              ]
                            |)) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "serde::ser::SerializeSeq",
                              Ty.associated,
                              [],
                              "end",
                              []
                            |),
                            [ M.read (| t |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          |)))
      | _, _, _ => 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_runtime_value_MoveValue.
  
  Module Impl_serde_ser_Serialize_for_move_core_types_runtime_value_MoveStruct.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    (*
        fn serialize<S: serde::Serializer>(&self, serializer: S) -> Result<S::Ok, S::Error> {
            let mut t = serializer.serialize_tuple(self.0.len())?;
            for v in self.0.iter() {
                t.serialize_element(v)?;
            }
            t.end()
        }
    *)
    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.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ t :=
                  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.associated; Ty.associated ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "serde::ser::Serializer",
                                S,
                                [],
                                "serialize_tuple",
                                []
                              |),
                              [
                                M.read (| serializer |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path "move_core_types::runtime_value::MoveValue";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    "len",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_tuple_field (|
                                      M.read (| self |),
                                      "move_core_types::runtime_value::MoveStruct",
                                      0
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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.associated; 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
                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::slice::iter::Iter")
                              []
                              [ Ty.path "move_core_types::runtime_value::MoveValue" ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_core_types::runtime_value::MoveValue" ],
                                "iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path "move_core_types::runtime_value::MoveValue";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_tuple_field (|
                                      M.read (| self |),
                                      "move_core_types::runtime_value::MoveStruct",
                                      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 "move_core_types::runtime_value::MoveValue" ],
                                          [],
                                          "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 v := 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.associated ],
                                                    [],
                                                    "branch",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "serde::ser::SerializeTuple",
                                                        Ty.associated,
                                                        [],
                                                        "serialize_element",
                                                        [
                                                          Ty.path
                                                            "move_core_types::runtime_value::MoveValue"
                                                        ]
                                                      |),
                                                      [ t; M.read (| v |) ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                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.associated; 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.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "serde::ser::SerializeTuple",
                      Ty.associated,
                      [],
                      "end",
                      []
                    |),
                    [ M.read (| t |) ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => 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_runtime_value_MoveStruct.
  
  Module Impl_core_fmt_Display_for_move_core_types_runtime_value_MoveTypeLayout.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveTypeLayout".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter) -> std::fmt::Result {
            use MoveTypeLayout::*;
            match self {
                Bool => write!(f, "bool"),
                U8 => write!(f, "u8"),
                U16 => write!(f, "u16"),
                U32 => write!(f, "u32"),
                U64 => write!(f, "u64"),
                U128 => write!(f, "u128"),
                U256 => write!(f, "u256"),
                Address => write!(f, "address"),
                Signer => write!(f, "signer"),
                Vector(typ) if f.alternate() => write!(f, "vector<{typ:#}>"),
                Vector(typ) => write!(f, "vector<{typ}>"),
                Struct(s) if f.alternate() => write!(f, "{s:#}"),
                Struct(s) => write!(f, "{s}"),
            }
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Bool"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "bool" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U8"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "u8" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U16"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "u16" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U32"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "u32" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U64"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "u64" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U128"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "u128" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::U256"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "u256" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Address"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "address" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Signer"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "signer" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Vector",
                        0
                      |) in
                    let typ := M.alloc (| γ1_0 |) in
                    let γ :=
                      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
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1_formatted",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [
                                    M.read (| Value.String "vector<" |);
                                    M.read (| Value.String ">" |)
                                  ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "alloc::boxed::Box")
                                                []
                                                [
                                                  Ty.path
                                                    "move_core_types::runtime_value::MoveTypeLayout";
                                                  Ty.path "alloc::alloc::Global"
                                                ]
                                            ]
                                        ]
                                      |),
                                      [ typ ]
                                    |)
                                  ]
                              |);
                              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 4;
                                        Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                        Value.StructTuple "core::fmt::rt::Count::Implied" []
                                      ]
                                    |)
                                  ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::UnsafeArg",
                                  "new",
                                  []
                                |),
                                []
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Vector",
                        0
                      |) in
                    let typ := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [
                                    M.read (| Value.String "vector<" |);
                                    M.read (| Value.String ">" |)
                                  ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "alloc::boxed::Box")
                                                []
                                                [
                                                  Ty.path
                                                    "move_core_types::runtime_value::MoveTypeLayout";
                                                  Ty.path "alloc::alloc::Global"
                                                ]
                                            ]
                                        ]
                                      |),
                                      [ typ ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Struct",
                        0
                      |) in
                    let s := M.alloc (| γ1_0 |) in
                    let γ :=
                      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
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1_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_display",
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.path
                                                "move_core_types::runtime_value::MoveStructLayout"
                                            ]
                                        ]
                                      |),
                                      [ s ]
                                    |)
                                  ]
                              |);
                              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 4;
                                        Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                        Value.StructTuple "core::fmt::rt::Count::Implied" []
                                      ]
                                    |)
                                  ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::UnsafeArg",
                                  "new",
                                  []
                                |),
                                []
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveTypeLayout::Struct",
                        0
                      |) in
                    let s := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.path
                                                "move_core_types::runtime_value::MoveStructLayout"
                                            ]
                                        ]
                                      |),
                                      [ s ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_runtime_value_MoveTypeLayout.
  
  (* StructTuple
    {
      name := "DebugAsDisplay";
      const_params := [];
      ty_params := [ "T" ];
      fields := [ Ty.apply (Ty.path "&") [] [ T ] ];
    } *)
  
  Module Impl_core_fmt_Debug_where_core_fmt_Display_T_for_move_core_types_runtime_value_DebugAsDisplay_T.
    Definition Self (T : Ty.t) : Ty.t :=
      Ty.apply (Ty.path "move_core_types::runtime_value::DebugAsDisplay") [] [ T ].
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            if f.alternate() {
                write!(f, "{:#}", self.0)
            } else {
                write!(f, "{}", self.0)
            }
        }
    *)
    Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      let Self : Ty.t := Self T in
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            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
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1_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_display",
                                        [ Ty.apply (Ty.path "&") [] [ T ] ]
                                      |),
                                      [
                                        M.SubPointer.get_struct_tuple_field (|
                                          M.read (| self |),
                                          "move_core_types::runtime_value::DebugAsDisplay",
                                          0
                                        |)
                                      ]
                                    |)
                                  ]
                              |);
                              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 4;
                                        Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                        Value.StructTuple "core::fmt::rt::Count::Implied" []
                                      ]
                                    |)
                                  ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "core::fmt::rt::UnsafeArg",
                                  "new",
                                  []
                                |),
                                []
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.apply (Ty.path "&") [] [ T ] ]
                                      |),
                                      [
                                        M.SubPointer.get_struct_tuple_field (|
                                          M.read (| self |),
                                          "move_core_types::runtime_value::DebugAsDisplay",
                                          0
                                        |)
                                      ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      forall (T : Ty.t),
      M.IsTraitInstance
        "core::fmt::Debug"
        (Self T)
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
  End Impl_core_fmt_Debug_where_core_fmt_Display_T_for_move_core_types_runtime_value_DebugAsDisplay_T.
  
  Module Impl_core_fmt_Display_for_move_core_types_runtime_value_MoveStructLayout.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStructLayout".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter) -> std::fmt::Result {
            use DebugAsDisplay as DD;
    
            write!(f, "struct ")?;
            let mut map = f.debug_map();
            for (i, l) in self.0.iter().enumerate() {
                map.entry(&i, &DD(&l));
            }
    
            map.finish()
        }
    *)
    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 (|
                      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 "struct " |) ] |)
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |),
                    [
                      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
                let~ map :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Formatter",
                        "debug_map",
                        []
                      |),
                      [ M.read (| f |) ]
                    |)
                  |) 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::iter::adapters::enumerate::Enumerate")
                              []
                              [
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ],
                                [],
                                "enumerate",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path
                                              "move_core_types::runtime_value::MoveTypeLayout";
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_tuple_field (|
                                          M.read (| self |),
                                          "move_core_types::runtime_value::MoveStructLayout",
                                          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::iter::adapters::enumerate::Enumerate")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.path
                                                    "move_core_types::runtime_value::MoveTypeLayout"
                                                ]
                                            ],
                                          [],
                                          "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 γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let i := M.copy (| γ1_0 |) in
                                          let l := M.copy (| γ1_1 |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::builders::DebugMap",
                                                  "entry",
                                                  []
                                                |),
                                                [
                                                  map;
                                                  i;
                                                  M.alloc (|
                                                    Value.StructTuple
                                                      "move_core_types::runtime_value::DebugAsDisplay"
                                                      [ l ]
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::builders::DebugMap",
                      "finish",
                      []
                    |),
                    [ map ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => 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_runtime_value_MoveStructLayout.
  
  Module Impl_core_fmt_Display_for_move_core_types_runtime_value_MoveValue.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveValue".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            match self {
                MoveValue::U8(u) => write!(f, "{}u8", u),
                MoveValue::U16(u) => write!(f, "{}u16", u),
                MoveValue::U32(u) => write!(f, "{}u32", u),
                MoveValue::U64(u) => write!(f, "{}u64", u),
                MoveValue::U128(u) => write!(f, "{}u128", u),
                MoveValue::U256(u) => write!(f, "{}u256", u),
                MoveValue::Bool(false) => write!(f, "false"),
                MoveValue::Bool(true) => write!(f, "true"),
                MoveValue::Address(a) => write!(f, "{}", a.to_hex_literal()),
                MoveValue::Signer(a) => write!(f, "signer({})", a.to_hex_literal()),
                MoveValue::Vector(v) => fmt_list(f, "vector[", v, "]"),
                MoveValue::Struct(s) => fmt::Display::fmt(s, f),
            }
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U8",
                        0
                      |) in
                    let u := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "" |); M.read (| Value.String "u8" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.apply (Ty.path "&") [] [ Ty.path "u8" ] ]
                                      |),
                                      [ u ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U16",
                        0
                      |) in
                    let u := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "" |); M.read (| Value.String "u16" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ]
                                      |),
                                      [ u ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U32",
                        0
                      |) in
                    let u := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "" |); M.read (| Value.String "u32" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ] ]
                                      |),
                                      [ u ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U64",
                        0
                      |) in
                    let u := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "" |); M.read (| Value.String "u64" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.apply (Ty.path "&") [] [ Ty.path "u64" ] ]
                                      |),
                                      [ u ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U128",
                        0
                      |) in
                    let u := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "" |); M.read (| Value.String "u128" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.apply (Ty.path "&") [] [ Ty.path "u128" ] ]
                                      |),
                                      [ u ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::U256",
                        0
                      |) in
                    let u := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [ M.read (| Value.String "" |); M.read (| Value.String "u256" |) ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.path "move_core_types::u256::U256" ]
                                        ]
                                      |),
                                      [ u ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Bool",
                        0
                      |) in
                    let _ :=
                      M.is_constant_or_break_match (| M.read (| γ1_0 |), Value.Bool false |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "false" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Bool",
                        0
                      |) in
                    let _ :=
                      M.is_constant_or_break_match (| M.read (| γ1_0 |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_const",
                              []
                            |),
                            [ M.alloc (| Value.Array [ M.read (| Value.String "true" |) ] |) ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Address",
                        0
                      |) in
                    let a := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (| Value.Array [ M.read (| Value.String "" |) ] |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.path "alloc::string::String" ]
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_core_types::account_address::AccountAddress",
                                              "to_hex_literal",
                                              []
                                            |),
                                            [ M.read (| a |) ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Signer",
                        0
                      |) in
                    let a := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_fmt",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Arguments",
                              "new_v1",
                              []
                            |),
                            [
                              M.alloc (|
                                Value.Array
                                  [
                                    M.read (| Value.String "signer(" |);
                                    M.read (| Value.String ")" |)
                                  ]
                              |);
                              M.alloc (|
                                Value.Array
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::rt::Argument",
                                        "new_display",
                                        [ Ty.path "alloc::string::String" ]
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_core_types::account_address::AccountAddress",
                                              "to_hex_literal",
                                              []
                                            |),
                                            [ M.read (| a |) ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Vector",
                        0
                      |) in
                    let v := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "move_core_types::fmt_list",
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.path "move_core_types::runtime_value::MoveValue" ];
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.path "move_core_types::runtime_value::MoveValue";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ]
                          ]
                        |),
                        [
                          M.read (| f |);
                          M.read (| Value.String "vector[" |);
                          M.read (| v |);
                          M.read (| Value.String "]" |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_core_types::runtime_value::MoveValue::Struct",
                        0
                      |) in
                    let s := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::fmt::Display",
                          Ty.path "move_core_types::runtime_value::MoveStruct",
                          [],
                          "fmt",
                          []
                        |),
                        [ M.read (| s |); M.read (| f |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_move_core_types_runtime_value_MoveValue.
  
  Module Impl_core_fmt_Display_for_move_core_types_runtime_value_MoveStruct.
    Definition Self : Ty.t := Ty.path "move_core_types::runtime_value::MoveStruct".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            fmt_list(f, "struct[", &self.0, "]")
        }
    *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_function (|
              "move_core_types::fmt_list",
              [
                Ty.apply (Ty.path "&") [] [ Ty.path "move_core_types::runtime_value::MoveValue" ];
                Ty.apply
                  (Ty.path "&")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "move_core_types::runtime_value::MoveValue";
                        Ty.path "alloc::alloc::Global"
                      ]
                  ]
              ]
            |),
            [
              M.read (| f |);
              M.read (| Value.String "struct[" |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_core_types::runtime_value::MoveStruct",
                0
              |);
              M.read (| Value.String "]" |)
            ]
          |)))
      | _, _, _ => 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_runtime_value_MoveStruct.
End runtime_value.
