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

Module locals_safety.
  Module abstract_state.
    (*
    Enum LocalState
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Unavailable";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "MaybeAvailable";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Available";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_clone_Clone_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (| M.read (| self |) |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
    
    Module Impl_core_marker_Copy_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
    
    Module Impl_core_fmt_Debug_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
              [
                M.read (| f |);
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                            |) in
                          M.alloc (| M.read (| Value.String "Unavailable" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState::MaybeAvailable"
                            |) in
                          M.alloc (| M.read (| Value.String "MaybeAvailable" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                            |) in
                          M.alloc (| M.read (| Value.String "Available" |) |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_bytecode_verifier_locals_safety_abstract_state_LocalState.
    
    Module Impl_core_cmp_Eq_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.Tuple []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
    
    Module Impl_core_marker_StructuralPartialEq_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
    
    Module Impl_core_cmp_PartialEq_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState".
      
      (* 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_bytecode_verifier::locals_safety::abstract_state::LocalState"
                      ]
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ __arg1_discr :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (|
                      "core::intrinsics::discriminant_value",
                      [ Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                      ]
                    |),
                    [ M.read (| other |) ]
                  |)
                |) in
              M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_move_bytecode_verifier_locals_safety_abstract_state_LocalState.
    
    Definition value_STEP_BASE_COST : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U128 15 |))).
    
    Definition value_RET_PER_LOCAL_COST : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U128 30 |))).
    
    Definition value_JOIN_BASE_COST : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U128 10 |))).
    
    Definition value_JOIN_PER_LOCAL_COST : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U128 5 |))).
    
    (* StructRecord
      {
        name := "AbstractState";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("current_function",
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ]);
            ("all_local_abilities",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.path "move_binary_format::file_format::AbilitySet";
                  Ty.path "alloc::alloc::Global"
                ]);
            ("local_states",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                  Ty.path "alloc::alloc::Global"
                ])
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::AbstractState".
      
      (* 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.StructRecord
              "move_bytecode_verifier::locals_safety::abstract_state::AbstractState"
              [
                ("current_function",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                        "current_function"
                      |)
                    ]
                  |));
                ("all_local_abilities",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.path "move_binary_format::file_format::AbilitySet";
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                        "all_local_abilities"
                      |)
                    ]
                  |));
                ("local_states",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.path
                            "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                        "local_states"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_bytecode_verifier_locals_safety_abstract_state_AbstractState.
    
    Module Impl_core_fmt_Debug_for_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::AbstractState".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field3_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "AbstractState" |);
                M.read (| Value.String "current_function" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                  "current_function"
                |);
                M.read (| Value.String "all_local_abilities" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                  "all_local_abilities"
                |);
                M.read (| Value.String "local_states" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                    "local_states"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_bytecode_verifier_locals_safety_abstract_state_AbstractState.
    
    Module Impl_core_cmp_Eq_for_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::AbstractState".
      
      (* 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.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_bytecode_verifier_locals_safety_abstract_state_AbstractState.
    
    Module Impl_core_marker_StructuralPartialEq_for_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::AbstractState".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
    
    Module Impl_core_cmp_PartialEq_for_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::AbstractState".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            LogicalOp.and (|
              LogicalOp.and (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ],
                    [
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                      "current_function"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                      "current_function"
                    |)
                  ]
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.path "move_binary_format::file_format::AbilitySet";
                          Ty.path "alloc::alloc::Global"
                        ],
                      [
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.path "move_binary_format::file_format::AbilitySet";
                            Ty.path "alloc::alloc::Global"
                          ]
                      ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                        "all_local_abilities"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                        "all_local_abilities"
                      |)
                    ]
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                        Ty.path "alloc::alloc::Global"
                      ],
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.path
                            "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                          Ty.path "alloc::alloc::Global"
                        ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                      "local_states"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                      "local_states"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => 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_bytecode_verifier_locals_safety_abstract_state_AbstractState.
    
    Module Impl_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::AbstractState".
      
      (*
          pub fn new(
              module: &CompiledModule,
              function_context: &FunctionContext,
          ) -> PartialVMResult<Self> {
              let num_args = function_context.parameters().len();
              let num_locals = num_args + function_context.locals().len();
              let local_states = (0..num_locals)
                  .map(|i| if i < num_args { Available } else { Unavailable })
                  .collect();
      
              let all_local_abilities = function_context
                  .parameters()
                  .0
                  .iter()
                  .chain(function_context.locals().0.iter())
                  .map(|st| module.abilities(st, function_context.type_parameters()))
                  .collect::<PartialVMResult<Vec<_>>>()?;
      
              Ok(Self {
                  current_function: function_context.index(),
                  local_states,
                  all_local_abilities,
              })
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ module; function_context ] =>
          ltac:(M.monadic
            (let module := M.alloc (| module |) in
            let function_context := M.alloc (| function_context |) in
            M.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ num_args :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "move_binary_format::file_format::Signature",
                          "len",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_bytecode_verifier::absint::FunctionContext",
                              "parameters",
                              []
                            |),
                            [ M.read (| function_context |) ]
                          |)
                        ]
                      |)
                    |) in
                  let~ num_locals :=
                    M.alloc (|
                      BinOp.Wrap.add (|
                        M.read (| num_args |),
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_binary_format::file_format::Signature",
                            "len",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_bytecode_verifier::absint::FunctionContext",
                                "locals",
                                []
                              |),
                              [ M.read (| function_context |) ]
                            |)
                          ]
                        |)
                      |)
                    |) in
                  let~ local_states :=
                    M.alloc (|
                      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::ops::range::Range") [] [ Ty.path "usize" ];
                              Ty.function
                                [ Ty.tuple [ Ty.path "usize" ] ]
                                (Ty.path
                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState")
                            ],
                          [],
                          "collect",
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.path
                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                Ty.path "alloc::alloc::Global"
                              ]
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                              [],
                              "map",
                              [
                                Ty.path
                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                Ty.function
                                  [ Ty.tuple [ Ty.path "usize" ] ]
                                  (Ty.path
                                    "move_bytecode_verifier::locals_safety::abstract_state::LocalState")
                              ]
                            |),
                            [
                              Value.StructRecord
                                "core::ops::range::Range"
                                [
                                  ("start", Value.Integer IntegerKind.Usize 0);
                                  ("end_", M.read (| num_locals |))
                                ];
                              M.closure
                                (fun γ =>
                                  ltac:(M.monadic
                                    match γ with
                                    | [ α0 ] =>
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.alloc (| α0 |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let i := M.copy (| γ |) in
                                                M.read (|
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                BinOp.lt (|
                                                                  M.read (| i |),
                                                                  M.read (| num_args |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.alloc (|
                                                            Value.StructTuple
                                                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                                              []
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (|
                                                            Value.StructTuple
                                                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                                                              []
                                                          |)))
                                                    ]
                                                  |)
                                                |)))
                                          ]
                                        |)))
                                    | _ => M.impossible "wrong number of arguments"
                                    end))
                            ]
                          |)
                        ]
                      |)
                    |) in
                  let~ all_local_abilities :=
                    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.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.path "move_binary_format::file_format::AbilitySet";
                                      Ty.path "alloc::alloc::Global"
                                    ];
                                  Ty.path "move_binary_format::errors::PartialVMError"
                                ],
                              [],
                              "branch",
                              []
                            |),
                            [
                              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::chain::Chain")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::SignatureToken"
                                            ];
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::SignatureToken"
                                            ]
                                        ];
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::SignatureToken"
                                                ]
                                            ]
                                        ]
                                        (Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "move_binary_format::file_format::AbilitySet";
                                            Ty.path "move_binary_format::errors::PartialVMError"
                                          ])
                                    ],
                                  [],
                                  "collect",
                                  [
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path "move_binary_format::file_format::AbilitySet";
                                            Ty.path "alloc::alloc::Global"
                                          ];
                                        Ty.path "move_binary_format::errors::PartialVMError"
                                      ]
                                  ]
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::iter::adapters::chain::Chain")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::SignatureToken"
                                            ];
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::SignatureToken"
                                            ]
                                        ],
                                      [],
                                      "map",
                                      [
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.path "move_binary_format::file_format::AbilitySet";
                                            Ty.path "move_binary_format::errors::PartialVMError"
                                          ];
                                        Ty.function
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_binary_format::file_format::SignatureToken"
                                                  ]
                                              ]
                                          ]
                                          (Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "move_binary_format::file_format::AbilitySet";
                                              Ty.path "move_binary_format::errors::PartialVMError"
                                            ])
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::Iter")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::SignatureToken"
                                            ],
                                          [],
                                          "chain",
                                          [
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [
                                                Ty.path
                                                  "move_binary_format::file_format::SignatureToken"
                                              ]
                                          ]
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::SignatureToken"
                                                ],
                                              "iter",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::deref::Deref",
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_binary_format::file_format::SignatureToken";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  [],
                                                  "deref",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "move_bytecode_verifier::absint::FunctionContext",
                                                        "parameters",
                                                        []
                                                      |),
                                                      [ M.read (| function_context |) ]
                                                    |),
                                                    "move_binary_format::file_format::Signature",
                                                    0
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |);
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "slice")
                                                []
                                                [
                                                  Ty.path
                                                    "move_binary_format::file_format::SignatureToken"
                                                ],
                                              "iter",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::deref::Deref",
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_binary_format::file_format::SignatureToken";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  [],
                                                  "deref",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_tuple_field (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "move_bytecode_verifier::absint::FunctionContext",
                                                        "locals",
                                                        []
                                                      |),
                                                      [ M.read (| function_context |) ]
                                                    |),
                                                    "move_binary_format::file_format::Signature",
                                                    0
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        ]
                                      |);
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [ α0 ] =>
                                              ltac:(M.monadic
                                                (M.match_operator (|
                                                  M.alloc (| α0 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let st := M.copy (| γ |) in
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path
                                                              "move_binary_format::file_format::CompiledModule",
                                                            "abilities",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| module |);
                                                            M.read (| st |);
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::absint::FunctionContext",
                                                                "type_parameters",
                                                                []
                                                              |),
                                                              [ M.read (| function_context |) ]
                                                            |)
                                                          ]
                                                        |)))
                                                  ]
                                                |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          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_bytecode_verifier::locals_safety::abstract_state::AbstractState";
                                              Ty.path "move_binary_format::errors::PartialVMError"
                                            ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              []
                                              [
                                                Ty.path "core::convert::Infallible";
                                                Ty.path "move_binary_format::errors::PartialVMError"
                                              ]
                                          ],
                                          "from_residual",
                                          []
                                        |),
                                        [ M.read (| residual |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::ops::control_flow::ControlFlow::Continue",
                                  0
                                |) in
                              let val := M.copy (| γ0_0 |) in
                              val))
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        Value.StructRecord
                          "move_bytecode_verifier::locals_safety::abstract_state::AbstractState"
                          [
                            ("current_function",
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_bytecode_verifier::absint::FunctionContext",
                                  "index",
                                  []
                                |),
                                [ M.read (| function_context |) ]
                              |));
                            ("local_states", M.read (| local_states |));
                            ("all_local_abilities", M.read (| all_local_abilities |))
                          ]
                      ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub fn local_abilities(&self, idx: LocalIndex) -> AbilitySet {
              self.all_local_abilities[idx as usize]
          }
      *)
      Definition local_abilities (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; idx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let idx := M.alloc (| idx |) in
            M.read (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::index::Index",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.path "move_binary_format::file_format::AbilitySet";
                      Ty.path "alloc::alloc::Global"
                    ],
                  [ Ty.path "usize" ],
                  "index",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                    "all_local_abilities"
                  |);
                  M.rust_cast (M.read (| idx |))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_local_abilities :
        M.IsAssociatedFunction Self "local_abilities" local_abilities.
      
      (*
          pub fn all_local_abilities(&self) -> &Vec<AbilitySet> {
              &self.all_local_abilities
          }
      *)
      Definition all_local_abilities (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
              "all_local_abilities"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_all_local_abilities :
        M.IsAssociatedFunction Self "all_local_abilities" all_local_abilities.
      
      (*
          pub fn local_state(&self, idx: LocalIndex) -> LocalState {
              self.local_states[idx as usize]
          }
      *)
      Definition local_state (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; idx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let idx := M.alloc (| idx |) in
            M.read (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::index::Index",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                      Ty.path "alloc::alloc::Global"
                    ],
                  [ Ty.path "usize" ],
                  "index",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                    "local_states"
                  |);
                  M.rust_cast (M.read (| idx |))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_local_state : M.IsAssociatedFunction Self "local_state" local_state.
      
      (*
          pub fn local_states(&self) -> &Vec<LocalState> {
              &self.local_states
          }
      *)
      Definition local_states (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
              "local_states"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_local_states :
        M.IsAssociatedFunction Self "local_states" local_states.
      
      (*
          pub fn set_available(&mut self, idx: LocalIndex) {
              self.local_states[idx as usize] = Available
          }
      *)
      Definition set_available (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; idx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let idx := M.alloc (| idx |) in
            M.read (|
              M.write (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::IndexMut",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                        Ty.path "alloc::alloc::Global"
                      ],
                    [ Ty.path "usize" ],
                    "index_mut",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                      "local_states"
                    |);
                    M.rust_cast (M.read (| idx |))
                  ]
                |),
                Value.StructTuple
                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                  []
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_set_available :
        M.IsAssociatedFunction Self "set_available" set_available.
      
      (*
          pub fn set_unavailable(&mut self, idx: LocalIndex) {
              assert!(self.local_states[idx as usize] == Available);
              self.local_states[idx as usize] = Unavailable
          }
      *)
      Definition set_unavailable (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; idx ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let idx := M.alloc (| idx |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.path
                                      "move_bytecode_verifier::locals_safety::abstract_state::LocalState",
                                    [
                                      Ty.path
                                        "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                    ],
                                    "eq",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::index::Index",
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path
                                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        [ Ty.path "usize" ],
                                        "index",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                          "local_states"
                                        |);
                                        M.rust_cast (M.read (| idx |))
                                      ]
                                    |);
                                    M.alloc (|
                                      Value.StructTuple
                                        "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                        []
                                    |)
                                  ]
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [
                                M.read (|
                                  Value.String
                                    "assertion failed: self.local_states[idx as usize] == Available"
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.write (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::IndexMut",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                        Ty.path "alloc::alloc::Global"
                      ],
                    [ Ty.path "usize" ],
                    "index_mut",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                      "local_states"
                    |);
                    M.rust_cast (M.read (| idx |))
                  ]
                |),
                Value.StructTuple
                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                  []
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_set_unavailable :
        M.IsAssociatedFunction Self "set_unavailable" set_unavailable.
      
      (*
          pub fn error(&self, status: StatusCode, offset: CodeOffset) -> PartialVMError {
              PartialVMError::new(status).at_code_offset(
                  self.current_function.unwrap_or(FunctionDefinitionIndex(0)),
                  offset,
              )
          }
      *)
      Definition error (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; status; offset ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let status := M.alloc (| status |) in
            let offset := M.alloc (| offset |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "move_binary_format::errors::PartialVMError",
                "at_code_offset",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_binary_format::errors::PartialVMError",
                    "new",
                    []
                  |),
                  [ M.read (| status |) ]
                |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ],
                    "unwrap_or",
                    []
                  |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                        "current_function"
                      |)
                    |);
                    Value.StructTuple
                      "move_binary_format::file_format::FunctionDefinitionIndex"
                      [ Value.Integer IntegerKind.U16 0 ]
                  ]
                |);
                M.read (| offset |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_error : M.IsAssociatedFunction Self "error" error.
      
      (*
          fn join_(&self, other: &Self) -> Self {
              assert!(self.current_function == other.current_function);
              assert!(self.all_local_abilities.len() == other.all_local_abilities.len());
              assert!(self.local_states.len() == other.local_states.len());
              let current_function = self.current_function;
              let all_local_abilities = self.all_local_abilities.clone();
              let local_states = self
                  .local_states
                  .iter()
                  .zip(&other.local_states)
                  .map(|(self_state, other_state)| {
                      use LocalState::*;
                      match (self_state, other_state) {
                          // Unavailable on both sides, nothing to add
                          (Unavailable, Unavailable) => Unavailable,
      
                          (MaybeAvailable, Unavailable)
                          | (Unavailable, MaybeAvailable)
                          | (MaybeAvailable, MaybeAvailable)
                          | (MaybeAvailable, Available)
                          | (Available, MaybeAvailable)
                          | (Unavailable, Available)
                          | (Available, Unavailable) => MaybeAvailable,
      
                          (Available, Available) => Available,
                      }
                  })
                  .collect();
      
              Self {
                  current_function,
                  all_local_abilities,
                  local_states,
              }
          }
      *)
      Definition join_ (ε : 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~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialEq",
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinitionIndex"
                                      ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::FunctionDefinitionIndex"
                                        ]
                                    ],
                                    "eq",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                      "current_function"
                                    |);
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| other |),
                                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                      "current_function"
                                    |)
                                  ]
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [
                                M.read (|
                                  Value.String
                                    "assertion failed: self.current_function == other.current_function"
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                BinOp.eq (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path "move_binary_format::file_format::AbilitySet";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                        "all_local_abilities"
                                      |)
                                    ]
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path "move_binary_format::file_format::AbilitySet";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| other |),
                                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                        "all_local_abilities"
                                      |)
                                    ]
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [
                                M.read (|
                                  Value.String
                                    "assertion failed: self.all_local_abilities.len() == other.all_local_abilities.len()"
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                BinOp.eq (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path
                                            "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                        "local_states"
                                      |)
                                    ]
                                  |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path
                                            "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "len",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| other |),
                                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                        "local_states"
                                      |)
                                    ]
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.call_closure (|
                              M.get_function (| "core::panicking::panic", [] |),
                              [
                                M.read (|
                                  Value.String
                                    "assertion failed: self.local_states.len() == other.local_states.len()"
                                |)
                              ]
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ current_function :=
                M.copy (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                    "current_function"
                  |)
                |) in
              let~ all_local_abilities :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.path "move_binary_format::file_format::AbilitySet";
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                        "all_local_abilities"
                      |)
                    ]
                  |)
                |) in
              let~ local_states :=
                M.alloc (|
                  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 "core::slice::iter::Iter")
                                []
                                [
                                  Ty.path
                                    "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                ];
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                []
                                [
                                  Ty.path
                                    "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                ]
                            ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [
                                          Ty.path
                                            "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                        ];
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [
                                          Ty.path
                                            "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                        ]
                                    ]
                                ]
                            ]
                            (Ty.path
                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState")
                        ],
                      [],
                      "collect",
                      [
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.path
                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                            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 "core::slice::iter::Iter")
                                []
                                [
                                  Ty.path
                                    "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                ];
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                []
                                [
                                  Ty.path
                                    "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                ]
                            ],
                          [],
                          "map",
                          [
                            Ty.path
                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.path
                                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                          ];
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.path
                                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                          ]
                                      ]
                                  ]
                              ]
                              (Ty.path
                                "move_bytecode_verifier::locals_safety::abstract_state::LocalState")
                          ]
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::iterator::Iterator",
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                []
                                [
                                  Ty.path
                                    "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                ],
                              [],
                              "zip",
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path
                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                        Ty.path "alloc::alloc::Global"
                                      ]
                                  ]
                              ]
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [
                                      Ty.path
                                        "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                    ],
                                  "iter",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::deref::Deref",
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path
                                            "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      [],
                                      "deref",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                        "local_states"
                                      |)
                                    ]
                                  |)
                                ]
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| other |),
                                "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                "local_states"
                              |)
                            ]
                          |);
                          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 self_state := M.copy (| γ0_0 |) in
                                            let other_state := M.copy (| γ0_1 |) in
                                            M.read (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  Value.Tuple
                                                    [
                                                      M.read (| self_state |);
                                                      M.read (| other_state |)
                                                    ]
                                                |),
                                                [
                                                  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 _ :=
                                                        M.is_struct_tuple (|
                                                          γ0_0,
                                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                                                        |) in
                                                      let γ0_1 := M.read (| γ0_1 |) in
                                                      let _ :=
                                                        M.is_struct_tuple (|
                                                          γ0_1,
                                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                                                        |) in
                                                      M.alloc (|
                                                        Value.StructTuple
                                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                                                          []
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (M.find_or_pattern (|
                                                        γ,
                                                        [
                                                          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 _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_0,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::MaybeAvailable"
                                                                |) in
                                                              let γ0_1 := M.read (| γ0_1 |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_1,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                                                                |) in
                                                              Value.Tuple []));
                                                          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 _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_0,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                                                                |) in
                                                              let γ0_1 := M.read (| γ0_1 |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_1,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::MaybeAvailable"
                                                                |) in
                                                              Value.Tuple []));
                                                          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 _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_0,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::MaybeAvailable"
                                                                |) in
                                                              let γ0_1 := M.read (| γ0_1 |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_1,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::MaybeAvailable"
                                                                |) in
                                                              Value.Tuple []));
                                                          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 _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_0,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::MaybeAvailable"
                                                                |) in
                                                              let γ0_1 := M.read (| γ0_1 |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_1,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                                                |) in
                                                              Value.Tuple []));
                                                          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 _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_0,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                                                |) in
                                                              let γ0_1 := M.read (| γ0_1 |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_1,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::MaybeAvailable"
                                                                |) in
                                                              Value.Tuple []));
                                                          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 _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_0,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                                                                |) in
                                                              let γ0_1 := M.read (| γ0_1 |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_1,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                                                |) in
                                                              Value.Tuple []));
                                                          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 _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_0,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                                                |) in
                                                              let γ0_1 := M.read (| γ0_1 |) in
                                                              let _ :=
                                                                M.is_struct_tuple (|
                                                                  γ0_1,
                                                                  "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Unavailable"
                                                                |) in
                                                              Value.Tuple []))
                                                        ],
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [] =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (|
                                                                    Value.StructTuple
                                                                      "move_bytecode_verifier::locals_safety::abstract_state::LocalState::MaybeAvailable"
                                                                      []
                                                                  |)))
                                                              | _ =>
                                                                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 γ0_0 := M.read (| γ0_0 |) in
                                                      let _ :=
                                                        M.is_struct_tuple (|
                                                          γ0_0,
                                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                                        |) in
                                                      let γ0_1 := M.read (| γ0_1 |) in
                                                      let _ :=
                                                        M.is_struct_tuple (|
                                                          γ0_1,
                                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                                        |) in
                                                      M.alloc (|
                                                        Value.StructTuple
                                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState::Available"
                                                          []
                                                      |)))
                                                ]
                                              |)
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                Value.StructRecord
                  "move_bytecode_verifier::locals_safety::abstract_state::AbstractState"
                  [
                    ("current_function", M.read (| current_function |));
                    ("all_local_abilities", M.read (| all_local_abilities |));
                    ("local_states", M.read (| local_states |))
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_join_ : M.IsAssociatedFunction Self "join_" join_.
    End Impl_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
    
    Module Impl_move_bytecode_verifier_absint_AbstractDomain_for_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
      Definition Self : Ty.t :=
        Ty.path "move_bytecode_verifier::locals_safety::abstract_state::AbstractState".
      
      (*
          fn join(
              &mut self,
              state: &AbstractState,
              meter: &mut (impl Meter + ?Sized),
          ) -> PartialVMResult<JoinResult> {
              meter.add(Scope::Function, JOIN_BASE_COST)?;
              meter.add_items(
                  Scope::Function,
                  JOIN_PER_LOCAL_COST,
                  state.local_states.len(),
              )?;
              let joined = Self::join_(self, state);
              assert!(self.local_states.len() == joined.local_states.len());
              let locals_unchanged = self
                  .local_states
                  .iter()
                  .zip(&joined.local_states)
                  .all(|(self_state, other_state)| self_state == other_state);
              if locals_unchanged {
                  Ok(JoinResult::Unchanged)
              } else {
                  *self = joined;
                  Ok(JoinResult::Changed)
              }
          }
      *)
      Definition join (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ impl_Meter__plus___Sized ], [ self; state; meter ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            let meter := M.alloc (| meter |) 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 "move_binary_format::errors::PartialVMError" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "move_bytecode_verifier_meter::Meter",
                                impl_Meter__plus___Sized,
                                [],
                                "add",
                                []
                              |),
                              [
                                M.read (| meter |);
                                Value.StructTuple
                                  "move_bytecode_verifier_meter::Scope::Function"
                                  [];
                                M.read (|
                                  M.get_constant (|
                                    "move_bytecode_verifier::locals_safety::abstract_state::JOIN_BASE_COST"
                                  |)
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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_bytecode_verifier::absint::JoinResult";
                                            Ty.path "move_binary_format::errors::PartialVMError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "move_binary_format::errors::PartialVMError"
                                            ]
                                        ],
                                        "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.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 "move_binary_format::errors::PartialVMError" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "move_bytecode_verifier_meter::Meter",
                                impl_Meter__plus___Sized,
                                [],
                                "add_items",
                                []
                              |),
                              [
                                M.read (| meter |);
                                Value.StructTuple
                                  "move_bytecode_verifier_meter::Scope::Function"
                                  [];
                                M.read (|
                                  M.get_constant (|
                                    "move_bytecode_verifier::locals_safety::abstract_state::JOIN_PER_LOCAL_COST"
                                  |)
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path
                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    "len",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| state |),
                                      "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                      "local_states"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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_bytecode_verifier::absint::JoinResult";
                                            Ty.path "move_binary_format::errors::PartialVMError"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "move_binary_format::errors::PartialVMError"
                                            ]
                                        ],
                                        "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~ joined :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path
                            "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                          "join_",
                          []
                        |),
                        [ M.read (| self |); M.read (| state |) ]
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    BinOp.eq (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.path
                                                "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "len",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                            "local_states"
                                          |)
                                        ]
                                      |),
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.path
                                                "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "len",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            joined,
                                            "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                            "local_states"
                                          |)
                                        ]
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.call_closure (|
                                  M.get_function (| "core::panicking::panic", [] |),
                                  [
                                    M.read (|
                                      Value.String
                                        "assertion failed: self.local_states.len() == joined.local_states.len()"
                                    |)
                                  ]
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ locals_unchanged :=
                    M.alloc (|
                      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 "core::slice::iter::Iter")
                                []
                                [
                                  Ty.path
                                    "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                ];
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                []
                                [
                                  Ty.path
                                    "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                ]
                            ],
                          [],
                          "all",
                          [
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.path
                                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                          ];
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.path
                                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                          ]
                                      ]
                                  ]
                              ]
                              (Ty.path "bool")
                          ]
                        |),
                        [
                          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_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                  ],
                                [],
                                "zip",
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.path
                                            "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                          Ty.path "alloc::alloc::Global"
                                        ]
                                    ]
                                ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "slice")
                                      []
                                      [
                                        Ty.path
                                          "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                      ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path
                                              "move_bytecode_verifier::locals_safety::abstract_state::LocalState";
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                          "local_states"
                                        |)
                                      ]
                                    |)
                                  ]
                                |);
                                M.SubPointer.get_struct_record_field (|
                                  joined,
                                  "move_bytecode_verifier::locals_safety::abstract_state::AbstractState",
                                  "local_states"
                                |)
                              ]
                            |)
                          |);
                          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 self_state := M.copy (| γ0_0 |) in
                                            let other_state := M.copy (| γ0_1 |) in
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::PartialEq",
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                                  ],
                                                [
                                                  Ty.apply
                                                    (Ty.path "&")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_bytecode_verifier::locals_safety::abstract_state::LocalState"
                                                    ]
                                                ],
                                                "eq",
                                                []
                                              |),
                                              [ self_state; other_state ]
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |)
                    |) in
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.use locals_unchanged in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::result::Result::Ok"
                              [
                                Value.StructTuple
                                  "move_bytecode_verifier::absint::JoinResult::Unchanged"
                                  []
                              ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _ := M.write (| M.read (| self |), M.read (| joined |) |) in
                          M.alloc (|
                            Value.StructTuple
                              "core::result::Result::Ok"
                              [
                                Value.StructTuple
                                  "move_bytecode_verifier::absint::JoinResult::Changed"
                                  []
                              ]
                          |)))
                    ]
                  |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "move_bytecode_verifier::absint::AbstractDomain"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("join", InstanceField.Method join) ].
    End Impl_move_bytecode_verifier_absint_AbstractDomain_for_move_bytecode_verifier_locals_safety_abstract_state_AbstractState.
  End abstract_state.
End locals_safety.
