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

Module constant.
  (*
  fn sig_to_ty(sig: &SignatureToken) -> Option<MoveTypeLayout> {
      match sig {
          SignatureToken::Signer => Some(MoveTypeLayout::Signer),
          SignatureToken::Address => Some(MoveTypeLayout::Address),
          SignatureToken::Bool => Some(MoveTypeLayout::Bool),
          SignatureToken::U8 => Some(MoveTypeLayout::U8),
          SignatureToken::U16 => Some(MoveTypeLayout::U16),
          SignatureToken::U32 => Some(MoveTypeLayout::U32),
          SignatureToken::U64 => Some(MoveTypeLayout::U64),
          SignatureToken::U128 => Some(MoveTypeLayout::U128),
          SignatureToken::U256 => Some(MoveTypeLayout::U256),
          SignatureToken::Vector(v) => Some(MoveTypeLayout::Vector(Box::new(sig_to_ty(v.as_ref())?))),
          SignatureToken::Reference(_)
          | SignatureToken::MutableReference(_)
          | SignatureToken::Struct(_)
          | SignatureToken::TypeParameter(_)
          | SignatureToken::StructInstantiation(_) => None,
      }
  }
  *)
  Definition sig_to_ty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ sig ] =>
      ltac:(M.monadic
        (let sig := M.alloc (| sig |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              M.match_operator (|
                sig,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::Signer"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::Signer"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::Address"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::Address"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::Bool"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::Bool"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::U8"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::U8"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::U16"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::U16"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::U32"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::U32"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::U64"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::U64"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::U128"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::U128"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::U256"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::U256"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "move_binary_format::file_format::SignatureToken::Vector",
                          0
                        |) in
                      let v := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_core_types::runtime_value::MoveTypeLayout::Vector"
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::boxed::Box")
                                      []
                                      [
                                        Ty.path "move_core_types::runtime_value::MoveTypeLayout";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    "new",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::Try",
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [
                                                  Ty.path
                                                    "move_core_types::runtime_value::MoveTypeLayout"
                                                ],
                                              [],
                                              "branch",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_function (|
                                                  "move_binary_format::constant::sig_to_ty",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::convert::AsRef",
                                                      Ty.apply
                                                        (Ty.path "alloc::boxed::Box")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_binary_format::file_format::SignatureToken";
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      [
                                                        Ty.path
                                                          "move_binary_format::file_format::SignatureToken"
                                                      ],
                                                      "as_ref",
                                                      []
                                                    |),
                                                    [ 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::option::Option")
                                                            []
                                                            [
                                                              Ty.path
                                                                "move_core_types::runtime_value::MoveTypeLayout"
                                                            ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "core::convert::Infallible"
                                                              ]
                                                          ],
                                                          "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
                      (M.find_or_pattern (|
                        γ,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.read (| γ |) in
                              let γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "move_binary_format::file_format::SignatureToken::Reference",
                                  0
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.read (| γ |) in
                              let γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "move_binary_format::file_format::SignatureToken::MutableReference",
                                  0
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.read (| γ |) in
                              let γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "move_binary_format::file_format::SignatureToken::Struct",
                                  0
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.read (| γ |) in
                              let γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "move_binary_format::file_format::SignatureToken::TypeParameter",
                                  0
                                |) in
                              Value.Tuple []));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ := M.read (| γ |) in
                              let γ1_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "move_binary_format::file_format::SignatureToken::StructInstantiation",
                                  0
                                |) in
                              Value.Tuple []))
                        ],
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [] =>
                                ltac:(M.monadic
                                  (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      |)))
                ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_sig_to_ty : M.IsFunction "move_binary_format::constant::sig_to_ty" sig_to_ty.
  
  (*
  fn ty_to_sig(ty: &MoveTypeLayout) -> Option<SignatureToken> {
      match ty {
          MoveTypeLayout::Address => Some(SignatureToken::Address),
          MoveTypeLayout::Signer => Some(SignatureToken::Signer),
          MoveTypeLayout::U8 => Some(SignatureToken::U8),
          MoveTypeLayout::U16 => Some(SignatureToken::U16),
          MoveTypeLayout::U32 => Some(SignatureToken::U32),
          MoveTypeLayout::U64 => Some(SignatureToken::U64),
          MoveTypeLayout::U128 => Some(SignatureToken::U128),
          MoveTypeLayout::U256 => Some(SignatureToken::U256),
          MoveTypeLayout::Vector(v) => Some(SignatureToken::Vector(Box::new(ty_to_sig(v.as_ref())?))),
          MoveTypeLayout::Struct(_) => None,
          MoveTypeLayout::Bool => Some(SignatureToken::Bool),
      }
  }
  *)
  Definition ty_to_sig (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ ty ] =>
      ltac:(M.monadic
        (let ty := M.alloc (| ty |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              M.match_operator (|
                ty,
                [
                  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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::Address"
                              []
                          ]
                      |)));
                  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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::Signer"
                              []
                          ]
                      |)));
                  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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::U8"
                              []
                          ]
                      |)));
                  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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::U32"
                              []
                          ]
                      |)));
                  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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::U128"
                              []
                          ]
                      |)));
                  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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::U256"
                              []
                          ]
                      |)));
                  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 v := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::Vector"
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::boxed::Box")
                                      []
                                      [
                                        Ty.path "move_binary_format::file_format::SignatureToken";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    "new",
                                    []
                                  |),
                                  [
                                    M.read (|
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::Try",
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::SignatureToken"
                                                ],
                                              [],
                                              "branch",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_function (|
                                                  "move_binary_format::constant::ty_to_sig",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::convert::AsRef",
                                                      Ty.apply
                                                        (Ty.path "alloc::boxed::Box")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_core_types::runtime_value::MoveTypeLayout";
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      [
                                                        Ty.path
                                                          "move_core_types::runtime_value::MoveTypeLayout"
                                                      ],
                                                      "as_ref",
                                                      []
                                                    |),
                                                    [ 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::option::Option")
                                                            []
                                                            [
                                                              Ty.path
                                                                "move_binary_format::file_format::SignatureToken"
                                                            ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [ Ty.path "core::convert::Infallible"
                                                              ]
                                                          ],
                                                          "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::Struct",
                          0
                        |) in
                      M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                  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
                          "core::option::Option::Some"
                          [
                            Value.StructTuple
                              "move_binary_format::file_format::SignatureToken::Bool"
                              []
                          ]
                      |)))
                ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_ty_to_sig : M.IsFunction "move_binary_format::constant::ty_to_sig" ty_to_sig.
  
  Module Impl_move_binary_format_file_format_Constant.
    Definition Self : Ty.t := Ty.path "move_binary_format::file_format::Constant".
    
    (*
        pub fn serialize_constant(ty: &MoveTypeLayout, v: &MoveValue) -> Option<Self> {
            Some(Self {
                type_: ty_to_sig(ty)?,
                data: v.simple_serialize()?,
            })
        }
    *)
    Definition serialize_constant (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ ty; v ] =>
        ltac:(M.monadic
          (let ty := M.alloc (| ty |) in
          let v := M.alloc (| v |) in
          M.catch_return (|
            ltac:(M.monadic
              (Value.StructTuple
                "core::option::Option::Some"
                [
                  Value.StructRecord
                    "move_binary_format::file_format::Constant"
                    [
                      ("type_",
                        M.read (|
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::try_trait::Try",
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [ Ty.path "move_binary_format::file_format::SignatureToken" ],
                                  [],
                                  "branch",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_function (|
                                      "move_binary_format::constant::ty_to_sig",
                                      []
                                    |),
                                    [ M.read (| ty |) ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              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::option::Option")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::Constant"
                                                ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "core::convert::Infallible" ]
                                              ],
                                              "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))
                            ]
                          |)
                        |));
                      ("data",
                        M.read (|
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::try_trait::Try",
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                                    ],
                                  [],
                                  "branch",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_core_types::runtime_value::MoveValue",
                                      "simple_serialize",
                                      []
                                    |),
                                    [ 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::option::Option")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::Constant"
                                                ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "core::convert::Infallible" ]
                                              ],
                                              "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_serialize_constant :
      M.IsAssociatedFunction Self "serialize_constant" serialize_constant.
    
    (*
        pub fn deserialize_constant(&self) -> Option<MoveValue> {
            let ty = sig_to_ty(&self.type_)?;
            MoveValue::simple_deserialize(&self.data, &ty).ok()
        }
    *)
    Definition deserialize_constant (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ ty :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "move_core_types::runtime_value::MoveTypeLayout" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_function (| "move_binary_format::constant::sig_to_ty", [] |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "move_binary_format::file_format::Constant",
                                  "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::option::Option")
                                          []
                                          [ Ty.path "move_core_types::runtime_value::MoveValue" ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "core::convert::Infallible" ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::result::Result")
                        []
                        [
                          Ty.path "move_core_types::runtime_value::MoveValue";
                          Ty.path "anyhow::Error"
                        ],
                      "ok",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_core_types::runtime_value::MoveValue",
                          "simple_deserialize",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                              [],
                              "deref",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "move_binary_format::file_format::Constant",
                                "data"
                              |)
                            ]
                          |);
                          ty
                        ]
                      |)
                    ]
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_deserialize_constant :
      M.IsAssociatedFunction Self "deserialize_constant" deserialize_constant.
  End Impl_move_binary_format_file_format_Constant.
End constant.
