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

Module compatibility.
  (* StructRecord
    {
      name := "Compatibility";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("check_struct_and_pub_function_linking", Ty.path "bool");
          ("check_struct_layout", Ty.path "bool");
          ("check_friend_linking", Ty.path "bool");
          ("check_private_entry_linking", Ty.path "bool");
          ("disallowed_new_abilities", Ty.path "move_binary_format::file_format::AbilitySet");
          ("disallow_change_struct_type_params", Ty.path "bool")
        ];
    } *)
  
  Module Impl_core_marker_StructuralPartialEq_for_move_binary_format_compatibility_Compatibility.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::Compatibility".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_binary_format_compatibility_Compatibility.
  
  Module Impl_core_cmp_PartialEq_for_move_binary_format_compatibility_Compatibility.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::Compatibility".
    
    (* 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 (|
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    BinOp.eq (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_binary_format::compatibility::Compatibility",
                          "check_struct_and_pub_function_linking"
                        |)
                      |),
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "move_binary_format::compatibility::Compatibility",
                          "check_struct_and_pub_function_linking"
                        |)
                      |)
                    |),
                    ltac:(M.monadic
                      (BinOp.eq (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_binary_format::compatibility::Compatibility",
                            "check_struct_layout"
                          |)
                        |),
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "move_binary_format::compatibility::Compatibility",
                            "check_struct_layout"
                          |)
                        |)
                      |)))
                  |),
                  ltac:(M.monadic
                    (BinOp.eq (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_binary_format::compatibility::Compatibility",
                          "check_friend_linking"
                        |)
                      |),
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "move_binary_format::compatibility::Compatibility",
                          "check_friend_linking"
                        |)
                      |)
                    |)))
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::compatibility::Compatibility",
                        "check_private_entry_linking"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "move_binary_format::compatibility::Compatibility",
                        "check_private_entry_linking"
                      |)
                    |)
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "move_binary_format::file_format::AbilitySet",
                    [ Ty.path "move_binary_format::file_format::AbilitySet" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_binary_format::compatibility::Compatibility",
                      "disallowed_new_abilities"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "move_binary_format::compatibility::Compatibility",
                      "disallowed_new_abilities"
                    |)
                  ]
                |)))
            |),
            ltac:(M.monadic
              (BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_binary_format::compatibility::Compatibility",
                    "disallow_change_struct_type_params"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "move_binary_format::compatibility::Compatibility",
                    "disallow_change_struct_type_params"
                  |)
                |)
              |)))
          |)))
      | _, _, _ => 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_binary_format_compatibility_Compatibility.
  
  Module Impl_core_cmp_Eq_for_move_binary_format_compatibility_Compatibility.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::Compatibility".
    
    (* 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.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_binary_format_compatibility_Compatibility.
  
  Module Impl_core_fmt_Debug_for_move_binary_format_compatibility_Compatibility.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::Compatibility".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ names :=
              M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      M.read (| Value.String "check_struct_and_pub_function_linking" |);
                      M.read (| Value.String "check_struct_layout" |);
                      M.read (| Value.String "check_friend_linking" |);
                      M.read (| Value.String "check_private_entry_linking" |);
                      M.read (| Value.String "disallowed_new_abilities" |);
                      M.read (| Value.String "disallow_change_struct_type_params" |)
                    ]
                |)
              |) in
            let~ values :=
              M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::compatibility::Compatibility",
                        "check_struct_and_pub_function_linking"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::compatibility::Compatibility",
                        "check_struct_layout"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::compatibility::Compatibility",
                        "check_friend_linking"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::compatibility::Compatibility",
                        "check_private_entry_linking"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::compatibility::Compatibility",
                        "disallowed_new_abilities"
                      |);
                      M.alloc (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_binary_format::compatibility::Compatibility",
                          "disallow_change_struct_type_params"
                        |)
                      |)
                    ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_fields_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "Compatibility" |);
                  M.read (| names |);
                  M.read (| values |)
                ]
              |)
            |)
          |)))
      | _, _, _ => 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_binary_format_compatibility_Compatibility.
  
  Module Impl_core_clone_Clone_for_move_binary_format_compatibility_Compatibility.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::Compatibility".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_move_binary_format_compatibility_Compatibility.
  
  Module Impl_core_marker_Copy_for_move_binary_format_compatibility_Compatibility.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::Compatibility".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_binary_format_compatibility_Compatibility.
  
  Module Impl_core_default_Default_for_move_binary_format_compatibility_Compatibility.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::Compatibility".
    
    (*
        fn default() -> Self {
            Self {
                check_struct_and_pub_function_linking: true,
                check_struct_layout: true,
                check_friend_linking: true,
                check_private_entry_linking: true,
                disallowed_new_abilities: AbilitySet::EMPTY,
                disallow_change_struct_type_params: true,
            }
        }
    *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "move_binary_format::compatibility::Compatibility"
            [
              ("check_struct_and_pub_function_linking", Value.Bool true);
              ("check_struct_layout", Value.Bool true);
              ("check_friend_linking", Value.Bool true);
              ("check_private_entry_linking", Value.Bool true);
              ("disallowed_new_abilities",
                M.read (| M.get_constant (| "move_binary_format::file_format::EMPTY" |) |));
              ("disallow_change_struct_type_params", Value.Bool true)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::default::Default"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("default", InstanceField.Method default) ].
  End Impl_core_default_Default_for_move_binary_format_compatibility_Compatibility.
  
  Module Impl_move_binary_format_compatibility_Compatibility.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::Compatibility".
    
    (*
        pub fn full_check() -> Self {
            Self::default()
        }
    *)
    Definition full_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (M.call_closure (|
            M.get_trait_method (|
              "core::default::Default",
              Ty.path "move_binary_format::compatibility::Compatibility",
              [],
              "default",
              []
            |),
            []
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_full_check : M.IsAssociatedFunction Self "full_check" full_check.
    
    (*
        pub fn no_check() -> Self {
            Self {
                check_struct_and_pub_function_linking: false,
                check_struct_layout: false,
                check_friend_linking: false,
                check_private_entry_linking: false,
                disallowed_new_abilities: AbilitySet::EMPTY,
                disallow_change_struct_type_params: false,
            }
        }
    *)
    Definition no_check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "move_binary_format::compatibility::Compatibility"
            [
              ("check_struct_and_pub_function_linking", Value.Bool false);
              ("check_struct_layout", Value.Bool false);
              ("check_friend_linking", Value.Bool false);
              ("check_private_entry_linking", Value.Bool false);
              ("disallowed_new_abilities",
                M.read (| M.get_constant (| "move_binary_format::file_format::EMPTY" |) |));
              ("disallow_change_struct_type_params", Value.Bool false)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_no_check : M.IsAssociatedFunction Self "no_check" no_check.
    
    (*
        pub fn need_check_compat(&self) -> bool {
            self != &Self::no_check()
        }
    *)
    Definition need_check_compat (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.apply
                (Ty.path "&")
                []
                [ Ty.path "move_binary_format::compatibility::Compatibility" ],
              [
                Ty.apply
                  (Ty.path "&")
                  []
                  [ Ty.path "move_binary_format::compatibility::Compatibility" ]
              ],
              "ne",
              []
            |),
            [
              self;
              M.alloc (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "move_binary_format::compatibility::Compatibility",
                      "no_check",
                      []
                    |),
                    []
                  |)
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_need_check_compat :
      M.IsAssociatedFunction Self "need_check_compat" need_check_compat.
    
    (*
        pub fn check(&self, old_module: &Module, new_module: &Module) -> PartialVMResult<()> {
            let mut struct_and_function_linking = true;
            let mut struct_layout = true;
            let mut friend_linking = true;
            let mut entry_linking = true;
    
            // module's name and address are unchanged
            if old_module.address != new_module.address || old_module.name != new_module.name {
                struct_and_function_linking = false;
            }
    
            // old module's structs are a subset of the new module's structs
            for (name, old_struct) in &old_module.structs {
                let Some(new_struct) = new_module.structs.get(name) else {
                    // Struct not present in new . Existing modules that depend on this struct will fail to link with the new version of the module.
                    // Also, struct layout cannot be guaranteed transitively, because after
                    // removing the struct, it could be re-added later with a different layout.
                    struct_and_function_linking = false;
                    struct_layout = false;
                    break;
                };
    
                if !struct_abilities_compatible(
                    self.disallowed_new_abilities,
                    old_struct.abilities,
                    new_struct.abilities,
                ) || !struct_type_parameters_compatible(
                    self.disallow_change_struct_type_params,
                    &old_struct.type_parameters,
                    &new_struct.type_parameters,
                ) {
                    struct_and_function_linking = false;
                }
                if new_struct.fields != old_struct.fields {
                    // Fields changed. Code in this module will fail at runtime if it tries to
                    // read a previously published struct value
                    // TODO: this is a stricter definition than required. We could in principle
                    // choose that changing the name (but not position or type) of a field is
                    // compatible. The VM does not care about the name of a field
                    // (it's purely informational), but clients presumably do.
                    struct_layout = false
                }
            }
    
            // The modules are considered as compatible function-wise when all the conditions are met:
            //
            // - old module's public functions are a subset of the new module's public functions
            //   (i.e. we cannot remove or change public functions)
            // - old module's script functions are a subset of the new module's script functions
            //   (i.e. we cannot remove or change script functions)
            // - for any friend function that is removed or changed in the old module
            //   - if the function visibility is upgraded to public, it is OK
            //   - otherwise, it is considered as incompatible.
            //
            // NOTE: it is possible to relax the compatibility checking for a friend function, i.e.,
            // we can remove/change a friend function if the function is not used by any module in the
            // friend list. But for simplicity, we decided to go to the more restrictive form now and
            // we may revisit this in the future.
            for (name, old_func) in &old_module.functions {
                let Some(new_func) = new_module.functions.get(name) else {
                    if old_func.visibility == Visibility::Friend {
                        friend_linking = false;
                    } else if old_func.visibility != Visibility::Private {
                        struct_and_function_linking = false;
                    } else if old_func.is_entry && self.check_private_entry_linking {
                        // This must be a private entry function. So set the link breakage if we're
                        // checking for that.
                        entry_linking = false;
                    }
                    continue;
                };
    
                // Check visibility compatibility
                match (old_func.visibility, new_func.visibility) {
                    (Visibility::Public, Visibility::Private | Visibility::Friend) => {
                        struct_and_function_linking = false
                    }
                    (Visibility::Friend, Visibility::Private) => friend_linking = false,
                    _ => (),
                }
    
                // Check entry compatibility
                if old_module.file_format_version < VERSION_5
                    && new_module.file_format_version < VERSION_5
                    && old_func.visibility != Visibility::Private
                    && old_func.is_entry != new_func.is_entry
                {
                    entry_linking = false
                } else if old_func.is_entry && !new_func.is_entry {
                    entry_linking = false;
                }
    
                // Check signature compatibility
                if old_func.parameters != new_func.parameters
                    || old_func.return_ != new_func.return_
                    || !fun_type_parameters_compatible(
                        &old_func.type_parameters,
                        &new_func.type_parameters,
                    )
                {
                    match old_func.visibility {
                        Visibility::Friend => friend_linking = false,
                        Visibility::Public => struct_and_function_linking = false,
                        Visibility::Private => (),
                    }
    
                    if old_func.is_entry {
                        entry_linking = false;
                    }
                }
            }
    
            // check friend declarations compatibility
            //
            // - additions to the list are allowed
            // - removals are not allowed
            //
            let old_friend_module_ids: BTreeSet<_> = old_module.friends.iter().cloned().collect();
            let new_friend_module_ids: BTreeSet<_> = new_module.friends.iter().cloned().collect();
            if !old_friend_module_ids.is_subset(&new_friend_module_ids) {
                friend_linking = false;
            }
    
            if self.check_struct_and_pub_function_linking && !struct_and_function_linking {
                return Err(PartialVMError::new(
                    StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE,
                ));
            }
            if self.check_struct_layout && !struct_layout {
                return Err(PartialVMError::new(
                    StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE,
                ));
            }
            if self.check_friend_linking && !friend_linking {
                return Err(PartialVMError::new(
                    StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE,
                ));
            }
            if self.check_private_entry_linking && !entry_linking {
                return Err(PartialVMError::new(
                    StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE,
                ));
            }
    
            Ok(())
        }
    *)
    Definition check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; old_module; new_module ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let old_module := M.alloc (| old_module |) in
          let new_module := M.alloc (| new_module |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ struct_and_function_linking := M.alloc (| Value.Bool true |) in
                let~ struct_layout := M.alloc (| Value.Bool true |) in
                let~ friend_linking := M.alloc (| Value.Bool true |) in
                let~ entry_linking := M.alloc (| Value.Bool true |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.or (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.path "move_core_types::account_address::AccountAddress",
                                      [ Ty.path "move_core_types::account_address::AccountAddress"
                                      ],
                                      "ne",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| old_module |),
                                        "move_binary_format::normalized::Module",
                                        "address"
                                      |);
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| new_module |),
                                        "move_binary_format::normalized::Module",
                                        "address"
                                      |)
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "move_core_types::identifier::Identifier",
                                        [ Ty.path "move_core_types::identifier::Identifier" ],
                                        "ne",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| old_module |),
                                          "move_binary_format::normalized::Module",
                                          "name"
                                        |);
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| new_module |),
                                          "move_binary_format::normalized::Module",
                                          "name"
                                        |)
                                      ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ := M.write (| struct_and_function_linking, Value.Bool false |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                                  []
                                  [
                                    Ty.path "move_core_types::identifier::Identifier";
                                    Ty.path "move_binary_format::normalized::Struct";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| old_module |),
                              "move_binary_format::normalized::Module",
                              "structs"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::map::Iter")
                                            []
                                            [
                                              Ty.path "move_core_types::identifier::Identifier";
                                              Ty.path "move_binary_format::normalized::Struct"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let name := M.copy (| γ1_0 |) in
                                          let old_struct := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::map::BTreeMap")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_core_types::identifier::Identifier";
                                                      Ty.path
                                                        "move_binary_format::normalized::Struct";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "get",
                                                  [
                                                    Ty.path
                                                      "move_core_types::identifier::Identifier"
                                                  ]
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| new_module |),
                                                    "move_binary_format::normalized::Module",
                                                    "structs"
                                                  |);
                                                  M.read (| name |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let new_struct := M.copy (| γ0_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.alloc (|
                                                                  LogicalOp.or (|
                                                                    UnOp.not (|
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "move_binary_format::compatibility::struct_abilities_compatible",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_binary_format::compatibility::Compatibility",
                                                                              "disallowed_new_abilities"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (|
                                                                                old_struct
                                                                              |),
                                                                              "move_binary_format::normalized::Struct",
                                                                              "abilities"
                                                                            |)
                                                                          |);
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (|
                                                                                new_struct
                                                                              |),
                                                                              "move_binary_format::normalized::Struct",
                                                                              "abilities"
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |),
                                                                    ltac:(M.monadic
                                                                      (UnOp.not (|
                                                                        M.call_closure (|
                                                                          M.get_function (|
                                                                            "move_binary_format::compatibility::struct_type_parameters_compatible",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (| self |),
                                                                                "move_binary_format::compatibility::Compatibility",
                                                                                "disallow_change_struct_type_params"
                                                                              |)
                                                                            |);
                                                                            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::StructTypeParameter";
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ],
                                                                                [],
                                                                                "deref",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (|
                                                                                    old_struct
                                                                                  |),
                                                                                  "move_binary_format::normalized::Struct",
                                                                                  "type_parameters"
                                                                                |)
                                                                              ]
                                                                            |);
                                                                            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::StructTypeParameter";
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ],
                                                                                [],
                                                                                "deref",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (|
                                                                                    new_struct
                                                                                  |),
                                                                                  "move_binary_format::normalized::Struct",
                                                                                  "type_parameters"
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                        |)
                                                                      |)))
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            let~ _ :=
                                                              M.write (|
                                                                struct_and_function_linking,
                                                                Value.Bool false
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_trait_method (|
                                                                    "core::cmp::PartialEq",
                                                                    Ty.apply
                                                                      (Ty.path "alloc::vec::Vec")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "move_binary_format::normalized::Field";
                                                                        Ty.path
                                                                          "alloc::alloc::Global"
                                                                      ],
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "alloc::vec::Vec")
                                                                        []
                                                                        [
                                                                          Ty.path
                                                                            "move_binary_format::normalized::Field";
                                                                          Ty.path
                                                                            "alloc::alloc::Global"
                                                                        ]
                                                                    ],
                                                                    "ne",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| new_struct |),
                                                                      "move_binary_format::normalized::Struct",
                                                                      "fields"
                                                                    |);
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| old_struct |),
                                                                      "move_binary_format::normalized::Struct",
                                                                      "fields"
                                                                    |)
                                                                  ]
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          M.write (|
                                                            struct_layout,
                                                            Value.Bool false
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                                  []
                                  [
                                    Ty.path "move_core_types::identifier::Identifier";
                                    Ty.path "move_binary_format::normalized::Function";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| old_module |),
                              "move_binary_format::normalized::Module",
                              "functions"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::map::Iter")
                                            []
                                            [
                                              Ty.path "move_core_types::identifier::Identifier";
                                              Ty.path "move_binary_format::normalized::Function"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let name := M.copy (| γ1_0 |) in
                                          let old_func := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::map::BTreeMap")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_core_types::identifier::Identifier";
                                                      Ty.path
                                                        "move_binary_format::normalized::Function";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "get",
                                                  [
                                                    Ty.path
                                                      "move_core_types::identifier::Identifier"
                                                  ]
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| new_module |),
                                                    "move_binary_format::normalized::Module",
                                                    "functions"
                                                  |);
                                                  M.read (| name |)
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let new_func := M.copy (| γ0_0 |) in
                                                  let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        Value.Tuple
                                                          [
                                                            M.read (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| old_func |),
                                                                "move_binary_format::normalized::Function",
                                                                "visibility"
                                                              |)
                                                            |);
                                                            M.read (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| new_func |),
                                                                "move_binary_format::normalized::Function",
                                                                "visibility"
                                                              |)
                                                            |)
                                                          ]
                                                      |),
                                                      [
                                                        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 _ :=
                                                              M.is_struct_tuple (|
                                                                γ0_0,
                                                                "move_binary_format::file_format::Visibility::Public"
                                                              |) in
                                                            M.find_or_pattern (|
                                                              γ0_1,
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "move_binary_format::file_format::Visibility::Private"
                                                                      |) in
                                                                    Value.Tuple []));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "move_binary_format::file_format::Visibility::Friend"
                                                                      |) in
                                                                    Value.Tuple []))
                                                              ],
                                                              M.closure
                                                                (fun γ =>
                                                                  ltac:(M.monadic
                                                                    match γ with
                                                                    | [] =>
                                                                      ltac:(M.monadic
                                                                        (M.write (|
                                                                          struct_and_function_linking,
                                                                          Value.Bool false
                                                                        |)))
                                                                    | _ =>
                                                                      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 _ :=
                                                              M.is_struct_tuple (|
                                                                γ0_0,
                                                                "move_binary_format::file_format::Visibility::Friend"
                                                              |) in
                                                            let _ :=
                                                              M.is_struct_tuple (|
                                                                γ0_1,
                                                                "move_binary_format::file_format::Visibility::Private"
                                                              |) in
                                                            M.write (|
                                                              friend_linking,
                                                              Value.Bool false
                                                            |)));
                                                        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 (|
                                                                  LogicalOp.and (|
                                                                    LogicalOp.and (|
                                                                      LogicalOp.and (|
                                                                        BinOp.lt (|
                                                                          M.read (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (|
                                                                                old_module
                                                                              |),
                                                                              "move_binary_format::normalized::Module",
                                                                              "file_format_version"
                                                                            |)
                                                                          |),
                                                                          M.read (|
                                                                            M.get_constant (|
                                                                              "move_binary_format::file_format_common::VERSION_5"
                                                                            |)
                                                                          |)
                                                                        |),
                                                                        ltac:(M.monadic
                                                                          (BinOp.lt (|
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (|
                                                                                  new_module
                                                                                |),
                                                                                "move_binary_format::normalized::Module",
                                                                                "file_format_version"
                                                                              |)
                                                                            |),
                                                                            M.read (|
                                                                              M.get_constant (|
                                                                                "move_binary_format::file_format_common::VERSION_5"
                                                                              |)
                                                                            |)
                                                                          |)))
                                                                      |),
                                                                      ltac:(M.monadic
                                                                        (M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::cmp::PartialEq",
                                                                            Ty.path
                                                                              "move_binary_format::file_format::Visibility",
                                                                            [
                                                                              Ty.path
                                                                                "move_binary_format::file_format::Visibility"
                                                                            ],
                                                                            "ne",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| old_func |),
                                                                              "move_binary_format::normalized::Function",
                                                                              "visibility"
                                                                            |);
                                                                            M.alloc (|
                                                                              Value.StructTuple
                                                                                "move_binary_format::file_format::Visibility::Private"
                                                                                []
                                                                            |)
                                                                          ]
                                                                        |)))
                                                                    |),
                                                                    ltac:(M.monadic
                                                                      (BinOp.ne (|
                                                                        M.read (|
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.read (| old_func |),
                                                                            "move_binary_format::normalized::Function",
                                                                            "is_entry"
                                                                          |)
                                                                        |),
                                                                        M.read (|
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.read (| new_func |),
                                                                            "move_binary_format::normalized::Function",
                                                                            "is_entry"
                                                                          |)
                                                                        |)
                                                                      |)))
                                                                  |)
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            M.write (|
                                                              entry_linking,
                                                              Value.Bool false
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              M.alloc (| Value.Tuple [] |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ :=
                                                                      M.use
                                                                        (M.alloc (|
                                                                          LogicalOp.and (|
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (|
                                                                                  old_func
                                                                                |),
                                                                                "move_binary_format::normalized::Function",
                                                                                "is_entry"
                                                                              |)
                                                                            |),
                                                                            ltac:(M.monadic
                                                                              (UnOp.not (|
                                                                                M.read (|
                                                                                  M.SubPointer.get_struct_record_field (|
                                                                                    M.read (|
                                                                                      new_func
                                                                                    |),
                                                                                    "move_binary_format::normalized::Function",
                                                                                    "is_entry"
                                                                                  |)
                                                                                |)
                                                                              |)))
                                                                          |)
                                                                        |)) in
                                                                    let _ :=
                                                                      M.is_constant_or_break_match (|
                                                                        M.read (| γ |),
                                                                        Value.Bool true
                                                                      |) in
                                                                    let~ _ :=
                                                                      M.write (|
                                                                        entry_linking,
                                                                        Value.Bool false
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |)))
                                                      ]
                                                    |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                LogicalOp.or (|
                                                                  LogicalOp.or (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::cmp::PartialEq",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::vec::Vec")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_binary_format::normalized::Type";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ],
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "alloc::vec::Vec")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "move_binary_format::normalized::Type";
                                                                              Ty.path
                                                                                "alloc::alloc::Global"
                                                                            ]
                                                                        ],
                                                                        "ne",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          M.read (| old_func |),
                                                                          "move_binary_format::normalized::Function",
                                                                          "parameters"
                                                                        |);
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          M.read (| new_func |),
                                                                          "move_binary_format::normalized::Function",
                                                                          "parameters"
                                                                        |)
                                                                      ]
                                                                    |),
                                                                    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::normalized::Type";
                                                                              Ty.path
                                                                                "alloc::alloc::Global"
                                                                            ],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "alloc::vec::Vec")
                                                                              []
                                                                              [
                                                                                Ty.path
                                                                                  "move_binary_format::normalized::Type";
                                                                                Ty.path
                                                                                  "alloc::alloc::Global"
                                                                              ]
                                                                          ],
                                                                          "ne",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.read (| old_func |),
                                                                            "move_binary_format::normalized::Function",
                                                                            "return_"
                                                                          |);
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.read (| new_func |),
                                                                            "move_binary_format::normalized::Function",
                                                                            "return_"
                                                                          |)
                                                                        ]
                                                                      |)))
                                                                  |),
                                                                  ltac:(M.monadic
                                                                    (UnOp.not (|
                                                                      M.call_closure (|
                                                                        M.get_function (|
                                                                          "move_binary_format::compatibility::fun_type_parameters_compatible",
                                                                          []
                                                                        |),
                                                                        [
                                                                          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::AbilitySet";
                                                                                  Ty.path
                                                                                    "alloc::alloc::Global"
                                                                                ],
                                                                              [],
                                                                              "deref",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (|
                                                                                  old_func
                                                                                |),
                                                                                "move_binary_format::normalized::Function",
                                                                                "type_parameters"
                                                                              |)
                                                                            ]
                                                                          |);
                                                                          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::AbilitySet";
                                                                                  Ty.path
                                                                                    "alloc::alloc::Global"
                                                                                ],
                                                                              [],
                                                                              "deref",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                M.read (|
                                                                                  new_func
                                                                                |),
                                                                                "move_binary_format::normalized::Function",
                                                                                "type_parameters"
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |)))
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          let~ _ :=
                                                            M.match_operator (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| old_func |),
                                                                "move_binary_format::normalized::Function",
                                                                "visibility"
                                                              |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "move_binary_format::file_format::Visibility::Friend"
                                                                      |) in
                                                                    M.write (|
                                                                      friend_linking,
                                                                      Value.Bool false
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "move_binary_format::file_format::Visibility::Public"
                                                                      |) in
                                                                    M.write (|
                                                                      struct_and_function_linking,
                                                                      Value.Bool false
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "move_binary_format::file_format::Visibility::Private"
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |) in
                                                          M.match_operator (|
                                                            M.alloc (| Value.Tuple [] |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ :=
                                                                    M.use
                                                                      (M.SubPointer.get_struct_record_field (|
                                                                        M.read (| old_func |),
                                                                        "move_binary_format::normalized::Function",
                                                                        "is_entry"
                                                                      |)) in
                                                                  let _ :=
                                                                    M.is_constant_or_break_match (|
                                                                      M.read (| γ |),
                                                                      Value.Bool true
                                                                    |) in
                                                                  let~ _ :=
                                                                    M.write (|
                                                                      entry_linking,
                                                                      Value.Bool false
                                                                    |) in
                                                                  M.alloc (| Value.Tuple [] |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ old_friend_module_ids :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::cloned::Cloned")
                          []
                          [
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_core_types::language_storage::ModuleId" ]
                          ],
                        [],
                        "collect",
                        [
                          Ty.apply
                            (Ty.path "alloc::collections::btree::set::BTreeSet")
                            []
                            [
                              Ty.path "move_core_types::language_storage::ModuleId";
                              Ty.path "alloc::alloc::Global"
                            ]
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_core_types::language_storage::ModuleId" ],
                            [],
                            "cloned",
                            [ Ty.path "move_core_types::language_storage::ModuleId" ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_core_types::language_storage::ModuleId" ],
                                "iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path "move_core_types::language_storage::ModuleId";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| old_module |),
                                      "move_binary_format::normalized::Module",
                                      "friends"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ new_friend_module_ids :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::cloned::Cloned")
                          []
                          [
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_core_types::language_storage::ModuleId" ]
                          ],
                        [],
                        "collect",
                        [
                          Ty.apply
                            (Ty.path "alloc::collections::btree::set::BTreeSet")
                            []
                            [
                              Ty.path "move_core_types::language_storage::ModuleId";
                              Ty.path "alloc::alloc::Global"
                            ]
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_core_types::language_storage::ModuleId" ],
                            [],
                            "cloned",
                            [ Ty.path "move_core_types::language_storage::ModuleId" ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_core_types::language_storage::ModuleId" ],
                                "iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::Deref",
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.path "move_core_types::language_storage::ModuleId";
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    [],
                                    "deref",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| new_module |),
                                      "move_binary_format::normalized::Module",
                                      "friends"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                UnOp.not (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::set::BTreeSet")
                                        []
                                        [
                                          Ty.path "move_core_types::language_storage::ModuleId";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "is_subset",
                                      []
                                    |),
                                    [ old_friend_module_ids; new_friend_module_ids ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ := M.write (| friend_linking, Value.Bool false |) in
                          M.alloc (| Value.Tuple [] |)));
                      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 (|
                                LogicalOp.and (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::compatibility::Compatibility",
                                      "check_struct_and_pub_function_linking"
                                    |)
                                  |),
                                  ltac:(M.monadic
                                    (UnOp.not (| M.read (| struct_and_function_linking |) |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "new",
                                          []
                                        |),
                                        [
                                          Value.StructTuple
                                            "move_core_types::vm_status::StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE"
                                            []
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      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 (|
                                LogicalOp.and (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::compatibility::Compatibility",
                                      "check_struct_layout"
                                    |)
                                  |),
                                  ltac:(M.monadic (UnOp.not (| M.read (| struct_layout |) |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "new",
                                          []
                                        |),
                                        [
                                          Value.StructTuple
                                            "move_core_types::vm_status::StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE"
                                            []
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      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 (|
                                LogicalOp.and (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::compatibility::Compatibility",
                                      "check_friend_linking"
                                    |)
                                  |),
                                  ltac:(M.monadic (UnOp.not (| M.read (| friend_linking |) |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "new",
                                          []
                                        |),
                                        [
                                          Value.StructTuple
                                            "move_core_types::vm_status::StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE"
                                            []
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      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 (|
                                LogicalOp.and (|
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::compatibility::Compatibility",
                                      "check_private_entry_linking"
                                    |)
                                  |),
                                  ltac:(M.monadic (UnOp.not (| M.read (| entry_linking |) |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::errors::PartialVMError",
                                          "new",
                                          []
                                        |),
                                        [
                                          Value.StructTuple
                                            "move_core_types::vm_status::StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE"
                                            []
                                        ]
                                      |)
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check : M.IsAssociatedFunction Self "check" check.
  End Impl_move_binary_format_compatibility_Compatibility.
  
  (*
  fn struct_abilities_compatible(
      disallowed_new_abilities: AbilitySet,
      old_abilities: AbilitySet,
      new_abilities: AbilitySet,
  ) -> bool {
      old_abilities.is_subset(new_abilities)
          && disallowed_new_abilities.into_iter().all(|ability| {
              // If the new abilities have the ability the old ones must have it to
              !new_abilities.has_ability(ability) || old_abilities.has_ability(ability)
          })
  }
  *)
  Definition struct_abilities_compatible
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ disallowed_new_abilities; old_abilities; new_abilities ] =>
      ltac:(M.monadic
        (let disallowed_new_abilities := M.alloc (| disallowed_new_abilities |) in
        let old_abilities := M.alloc (| old_abilities |) in
        let new_abilities := M.alloc (| new_abilities |) in
        LogicalOp.and (|
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_binary_format::file_format::AbilitySet",
              "is_subset",
              []
            |),
            [ M.read (| old_abilities |); M.read (| new_abilities |) ]
          |),
          ltac:(M.monadic
            (M.call_closure (|
              M.get_trait_method (|
                "core::iter::traits::iterator::Iterator",
                Ty.path "move_binary_format::file_format::AbilitySetIterator",
                [],
                "all",
                [
                  Ty.function
                    [ Ty.tuple [ Ty.path "move_binary_format::file_format::Ability" ] ]
                    (Ty.path "bool")
                ]
              |),
              [
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      Ty.path "move_binary_format::file_format::AbilitySet",
                      [],
                      "into_iter",
                      []
                    |),
                    [ M.read (| disallowed_new_abilities |) ]
                  |)
                |);
                M.closure
                  (fun γ =>
                    ltac:(M.monadic
                      match γ with
                      | [ α0 ] =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| α0 |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let ability := M.copy (| γ |) in
                                  LogicalOp.or (|
                                    UnOp.not (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::file_format::AbilitySet",
                                          "has_ability",
                                          []
                                        |),
                                        [ M.read (| new_abilities |); M.read (| ability |) ]
                                      |)
                                    |),
                                    ltac:(M.monadic
                                      (M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "move_binary_format::file_format::AbilitySet",
                                          "has_ability",
                                          []
                                        |),
                                        [ M.read (| old_abilities |); M.read (| ability |) ]
                                      |)))
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_struct_abilities_compatible :
    M.IsFunction
      "move_binary_format::compatibility::struct_abilities_compatible"
      struct_abilities_compatible.
  
  (*
  fn fun_type_parameters_compatible(
      old_type_parameters: &[AbilitySet],
      new_type_parameters: &[AbilitySet],
  ) -> bool {
      old_type_parameters.len() == new_type_parameters.len()
          && old_type_parameters.iter().zip(new_type_parameters).all(
              |(old_type_parameter_constraint, new_type_parameter_constraint)| {
                  type_parameter_constraints_compatible(
                      false, // generic abilities can change for functions
                      *old_type_parameter_constraint,
                      *new_type_parameter_constraint,
                  )
              },
          )
  }
  *)
  Definition fun_type_parameters_compatible
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ old_type_parameters; new_type_parameters ] =>
      ltac:(M.monadic
        (let old_type_parameters := M.alloc (| old_type_parameters |) in
        let new_type_parameters := M.alloc (| new_type_parameters |) in
        LogicalOp.and (|
          BinOp.eq (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "slice")
                  []
                  [ Ty.path "move_binary_format::file_format::AbilitySet" ],
                "len",
                []
              |),
              [ M.read (| old_type_parameters |) ]
            |),
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "slice")
                  []
                  [ Ty.path "move_binary_format::file_format::AbilitySet" ],
                "len",
                []
              |),
              [ M.read (| new_type_parameters |) ]
            |)
          |),
          ltac:(M.monadic
            (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_binary_format::file_format::AbilitySet" ];
                    Ty.apply
                      (Ty.path "core::slice::iter::Iter")
                      []
                      [ Ty.path "move_binary_format::file_format::AbilitySet" ]
                  ],
                [],
                "all",
                [
                  Ty.function
                    [
                      Ty.tuple
                        [
                          Ty.tuple
                            [
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.path "move_binary_format::file_format::AbilitySet" ];
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.path "move_binary_format::file_format::AbilitySet" ]
                            ]
                        ]
                    ]
                    (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_binary_format::file_format::AbilitySet" ],
                      [],
                      "zip",
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.path "move_binary_format::file_format::AbilitySet" ]
                          ]
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_binary_format::file_format::AbilitySet" ],
                          "iter",
                          []
                        |),
                        [ M.read (| old_type_parameters |) ]
                      |);
                      M.read (| new_type_parameters |)
                    ]
                  |)
                |);
                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 old_type_parameter_constraint := M.copy (| γ0_0 |) in
                                  let new_type_parameter_constraint := M.copy (| γ0_1 |) in
                                  M.call_closure (|
                                    M.get_function (|
                                      "move_binary_format::compatibility::type_parameter_constraints_compatible",
                                      []
                                    |),
                                    [
                                      Value.Bool false;
                                      M.read (| M.read (| old_type_parameter_constraint |) |);
                                      M.read (| M.read (| new_type_parameter_constraint |) |)
                                    ]
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_fun_type_parameters_compatible :
    M.IsFunction
      "move_binary_format::compatibility::fun_type_parameters_compatible"
      fun_type_parameters_compatible.
  
  (*
  fn struct_type_parameters_compatible(
      disallow_changing_generic_abilities: bool,
      old_type_parameters: &[StructTypeParameter],
      new_type_parameters: &[StructTypeParameter],
  ) -> bool {
      old_type_parameters.len() == new_type_parameters.len()
          && old_type_parameters.iter().zip(new_type_parameters).all(
              |(old_type_parameter, new_type_parameter)| {
                  type_parameter_phantom_decl_compatible(
                      disallow_changing_generic_abilities,
                      old_type_parameter,
                      new_type_parameter,
                  ) && type_parameter_constraints_compatible(
                      disallow_changing_generic_abilities,
                      old_type_parameter.constraints,
                      new_type_parameter.constraints,
                  )
              },
          )
  }
  *)
  Definition struct_type_parameters_compatible
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ disallow_changing_generic_abilities; old_type_parameters; new_type_parameters ] =>
      ltac:(M.monadic
        (let disallow_changing_generic_abilities :=
          M.alloc (| disallow_changing_generic_abilities |) in
        let old_type_parameters := M.alloc (| old_type_parameters |) in
        let new_type_parameters := M.alloc (| new_type_parameters |) in
        LogicalOp.and (|
          BinOp.eq (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "slice")
                  []
                  [ Ty.path "move_binary_format::file_format::StructTypeParameter" ],
                "len",
                []
              |),
              [ M.read (| old_type_parameters |) ]
            |),
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "slice")
                  []
                  [ Ty.path "move_binary_format::file_format::StructTypeParameter" ],
                "len",
                []
              |),
              [ M.read (| new_type_parameters |) ]
            |)
          |),
          ltac:(M.monadic
            (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_binary_format::file_format::StructTypeParameter" ];
                    Ty.apply
                      (Ty.path "core::slice::iter::Iter")
                      []
                      [ Ty.path "move_binary_format::file_format::StructTypeParameter" ]
                  ],
                [],
                "all",
                [
                  Ty.function
                    [
                      Ty.tuple
                        [
                          Ty.tuple
                            [
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.path "move_binary_format::file_format::StructTypeParameter" ];
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.path "move_binary_format::file_format::StructTypeParameter" ]
                            ]
                        ]
                    ]
                    (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_binary_format::file_format::StructTypeParameter" ],
                      [],
                      "zip",
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "slice")
                              []
                              [ Ty.path "move_binary_format::file_format::StructTypeParameter" ]
                          ]
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "slice")
                            []
                            [ Ty.path "move_binary_format::file_format::StructTypeParameter" ],
                          "iter",
                          []
                        |),
                        [ M.read (| old_type_parameters |) ]
                      |);
                      M.read (| new_type_parameters |)
                    ]
                  |)
                |);
                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 old_type_parameter := M.copy (| γ0_0 |) in
                                  let new_type_parameter := M.copy (| γ0_1 |) in
                                  LogicalOp.and (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "move_binary_format::compatibility::type_parameter_phantom_decl_compatible",
                                        []
                                      |),
                                      [
                                        M.read (| disallow_changing_generic_abilities |);
                                        M.read (| old_type_parameter |);
                                        M.read (| new_type_parameter |)
                                      ]
                                    |),
                                    ltac:(M.monadic
                                      (M.call_closure (|
                                        M.get_function (|
                                          "move_binary_format::compatibility::type_parameter_constraints_compatible",
                                          []
                                        |),
                                        [
                                          M.read (| disallow_changing_generic_abilities |);
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| old_type_parameter |),
                                              "move_binary_format::file_format::StructTypeParameter",
                                              "constraints"
                                            |)
                                          |);
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| new_type_parameter |),
                                              "move_binary_format::file_format::StructTypeParameter",
                                              "constraints"
                                            |)
                                          |)
                                        ]
                                      |)))
                                  |)))
                            ]
                          |)))
                      | _ => M.impossible "wrong number of arguments"
                      end))
              ]
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_struct_type_parameters_compatible :
    M.IsFunction
      "move_binary_format::compatibility::struct_type_parameters_compatible"
      struct_type_parameters_compatible.
  
  (*
  fn type_parameter_constraints_compatible(
      disallow_changing_generic_abilities: bool,
      old_type_constraints: AbilitySet,
      new_type_constraints: AbilitySet,
  ) -> bool {
      if disallow_changing_generic_abilities {
          old_type_constraints == new_type_constraints
      } else {
          new_type_constraints.is_subset(old_type_constraints)
      }
  }
  *)
  Definition type_parameter_constraints_compatible
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ disallow_changing_generic_abilities; old_type_constraints; new_type_constraints ] =>
      ltac:(M.monadic
        (let disallow_changing_generic_abilities :=
          M.alloc (| disallow_changing_generic_abilities |) in
        let old_type_constraints := M.alloc (| old_type_constraints |) in
        let new_type_constraints := M.alloc (| new_type_constraints |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use disallow_changing_generic_abilities in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.path "move_binary_format::file_format::AbilitySet",
                        [ Ty.path "move_binary_format::file_format::AbilitySet" ],
                        "eq",
                        []
                      |),
                      [ old_type_constraints; new_type_constraints ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_binary_format::file_format::AbilitySet",
                        "is_subset",
                        []
                      |),
                      [ M.read (| new_type_constraints |); M.read (| old_type_constraints |) ]
                    |)
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_type_parameter_constraints_compatible :
    M.IsFunction
      "move_binary_format::compatibility::type_parameter_constraints_compatible"
      type_parameter_constraints_compatible.
  
  (*
  fn type_parameter_phantom_decl_compatible(
      disallow_changing_generic_abilities: bool,
      old_type_parameter: &StructTypeParameter,
      new_type_parameter: &StructTypeParameter,
  ) -> bool {
      if disallow_changing_generic_abilities {
          // phantom/non-phantom cannot change from one version to the next.
          old_type_parameter.is_phantom == new_type_parameter.is_phantom
      } else {
          // old_type_paramter.is_phantom => new_type_parameter.is_phantom
          !old_type_parameter.is_phantom || new_type_parameter.is_phantom
      }
  }
  *)
  Definition type_parameter_phantom_decl_compatible
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ disallow_changing_generic_abilities; old_type_parameter; new_type_parameter ] =>
      ltac:(M.monadic
        (let disallow_changing_generic_abilities :=
          M.alloc (| disallow_changing_generic_abilities |) in
        let old_type_parameter := M.alloc (| old_type_parameter |) in
        let new_type_parameter := M.alloc (| new_type_parameter |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use disallow_changing_generic_abilities in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    BinOp.eq (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| old_type_parameter |),
                          "move_binary_format::file_format::StructTypeParameter",
                          "is_phantom"
                        |)
                      |),
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| new_type_parameter |),
                          "move_binary_format::file_format::StructTypeParameter",
                          "is_phantom"
                        |)
                      |)
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.alloc (|
                    LogicalOp.or (|
                      UnOp.not (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| old_type_parameter |),
                            "move_binary_format::file_format::StructTypeParameter",
                            "is_phantom"
                          |)
                        |)
                      |),
                      ltac:(M.monadic
                        (M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| new_type_parameter |),
                            "move_binary_format::file_format::StructTypeParameter",
                            "is_phantom"
                          |)
                        |)))
                    |)
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_type_parameter_phantom_decl_compatible :
    M.IsFunction
      "move_binary_format::compatibility::type_parameter_phantom_decl_compatible"
      type_parameter_phantom_decl_compatible.
  
  (*
  Enum InclusionCheck
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Subset";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Equal";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_move_binary_format_compatibility_InclusionCheck.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::InclusionCheck".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_binary_format::compatibility::InclusionCheck::Subset"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_binary_format::compatibility::InclusionCheck::Subset"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_binary_format::compatibility::InclusionCheck::Equal"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "move_binary_format::compatibility::InclusionCheck::Equal"
                        []
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_binary_format_compatibility_InclusionCheck.
  
  Module Impl_core_fmt_Debug_for_move_binary_format_compatibility_InclusionCheck.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::InclusionCheck".
    
    (* 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_binary_format::compatibility::InclusionCheck::Subset"
                          |) in
                        M.alloc (| M.read (| Value.String "Subset" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "move_binary_format::compatibility::InclusionCheck::Equal"
                          |) in
                        M.alloc (| M.read (| Value.String "Equal" |) |)))
                  ]
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_binary_format_compatibility_InclusionCheck.
  
  Module Impl_core_cmp_Ord_for_move_binary_format_compatibility_InclusionCheck.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::InclusionCheck".
    
    (* Ord *)
    Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_binary_format::compatibility::InclusionCheck" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_binary_format::compatibility::InclusionCheck" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
                [ __self_discr; __arg1_discr ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Ord"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
  End Impl_core_cmp_Ord_for_move_binary_format_compatibility_InclusionCheck.
  
  Module Impl_core_cmp_PartialOrd_for_move_binary_format_compatibility_InclusionCheck.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::InclusionCheck".
    
    (* PartialOrd *)
    Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_binary_format::compatibility::InclusionCheck" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_binary_format::compatibility::InclusionCheck" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialOrd",
                  Ty.path "isize",
                  [ Ty.path "isize" ],
                  "partial_cmp",
                  []
                |),
                [ __self_discr; __arg1_discr ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
  End Impl_core_cmp_PartialOrd_for_move_binary_format_compatibility_InclusionCheck.
  
  Module Impl_core_cmp_Eq_for_move_binary_format_compatibility_InclusionCheck.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::InclusionCheck".
    
    (* 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_binary_format_compatibility_InclusionCheck.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_binary_format_compatibility_InclusionCheck.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::InclusionCheck".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_binary_format_compatibility_InclusionCheck.
  
  Module Impl_core_cmp_PartialEq_for_move_binary_format_compatibility_InclusionCheck.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::InclusionCheck".
    
    (* 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_binary_format::compatibility::InclusionCheck" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "move_binary_format::compatibility::InclusionCheck" ]
                  |),
                  [ 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_binary_format_compatibility_InclusionCheck.
  
  Module Impl_move_binary_format_compatibility_InclusionCheck.
    Definition Self : Ty.t := Ty.path "move_binary_format::compatibility::InclusionCheck".
    
    (*
        pub fn check(&self, old_module: &Module, new_module: &Module) -> PartialVMResult<()> {
            let err = Err(PartialVMError::new(
                StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE,
            ));
    
            // Module checks
            if old_module.address != new_module.address
                || old_module.name != new_module.name
                || old_module.file_format_version > new_module.file_format_version
            {
                return err;
            }
    
            // If we're checking exactness we make sure there's an inclusion, and that the size of all
            // of the tables are the exact same except for constants.
            if (self == &Self::Equal)
                && (old_module.structs.len() != new_module.structs.len()
                    || old_module.functions.len() != new_module.functions.len()
                    || old_module.friends.len() != new_module.friends.len())
            {
                return err;
            }
    
            // Struct checks
            for (name, old_struct) in &old_module.structs {
                match new_module.structs.get(name) {
                    Some(new_struct) if old_struct == new_struct => (),
                    _ => {
                        return err;
                    }
                };
            }
    
            // Function checks
            for (name, old_func) in &old_module.functions {
                match new_module
                    .functions
                    .get(name)
                    .or_else(|| new_module.functions.get(name))
                {
                    Some(new_func) if old_func == new_func => (),
                    _ => {
                        return err;
                    }
                }
            }
    
            Ok(())
        }
    *)
    Definition check (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; old_module; new_module ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let old_module := M.alloc (| old_module |) in
          let new_module := M.alloc (| new_module |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ err :=
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Err"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "move_binary_format::errors::PartialVMError",
                            "new",
                            []
                          |),
                          [
                            Value.StructTuple
                              "move_core_types::vm_status::StatusCode::BACKWARD_INCOMPATIBLE_MODULE_UPDATE"
                              []
                          ]
                        |)
                      ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.or (|
                                  LogicalOp.or (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "move_core_types::account_address::AccountAddress",
                                        [ Ty.path "move_core_types::account_address::AccountAddress"
                                        ],
                                        "ne",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| old_module |),
                                          "move_binary_format::normalized::Module",
                                          "address"
                                        |);
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| new_module |),
                                          "move_binary_format::normalized::Module",
                                          "address"
                                        |)
                                      ]
                                    |),
                                    ltac:(M.monadic
                                      (M.call_closure (|
                                        M.get_trait_method (|
                                          "core::cmp::PartialEq",
                                          Ty.path "move_core_types::identifier::Identifier",
                                          [ Ty.path "move_core_types::identifier::Identifier" ],
                                          "ne",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| old_module |),
                                            "move_binary_format::normalized::Module",
                                            "name"
                                          |);
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| new_module |),
                                            "move_binary_format::normalized::Module",
                                            "name"
                                          |)
                                        ]
                                      |)))
                                  |),
                                  ltac:(M.monadic
                                    (BinOp.gt (|
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| old_module |),
                                          "move_binary_format::normalized::Module",
                                          "file_format_version"
                                        |)
                                      |),
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| new_module |),
                                          "move_binary_format::normalized::Module",
                                          "file_format_version"
                                        |)
                                      |)
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (| M.read (| M.return_ (| M.read (| err |) |) |) |)
                          |)));
                      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 (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::compatibility::InclusionCheck"
                                        ],
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::compatibility::InclusionCheck"
                                          ]
                                      ],
                                      "eq",
                                      []
                                    |),
                                    [
                                      self;
                                      M.alloc (|
                                        M.alloc (|
                                          Value.StructTuple
                                            "move_binary_format::compatibility::InclusionCheck::Equal"
                                            []
                                        |)
                                      |)
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (LogicalOp.or (|
                                      LogicalOp.or (|
                                        BinOp.ne (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::collections::btree::map::BTreeMap")
                                                []
                                                [
                                                  Ty.path "move_core_types::identifier::Identifier";
                                                  Ty.path "move_binary_format::normalized::Struct";
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "len",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| old_module |),
                                                "move_binary_format::normalized::Module",
                                                "structs"
                                              |)
                                            ]
                                          |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::collections::btree::map::BTreeMap")
                                                []
                                                [
                                                  Ty.path "move_core_types::identifier::Identifier";
                                                  Ty.path "move_binary_format::normalized::Struct";
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "len",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| new_module |),
                                                "move_binary_format::normalized::Module",
                                                "structs"
                                              |)
                                            ]
                                          |)
                                        |),
                                        ltac:(M.monadic
                                          (BinOp.ne (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path
                                                    "alloc::collections::btree::map::BTreeMap")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::identifier::Identifier";
                                                    Ty.path
                                                      "move_binary_format::normalized::Function";
                                                    Ty.path "alloc::alloc::Global"
                                                  ],
                                                "len",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| old_module |),
                                                  "move_binary_format::normalized::Module",
                                                  "functions"
                                                |)
                                              ]
                                            |),
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path
                                                    "alloc::collections::btree::map::BTreeMap")
                                                  []
                                                  [
                                                    Ty.path
                                                      "move_core_types::identifier::Identifier";
                                                    Ty.path
                                                      "move_binary_format::normalized::Function";
                                                    Ty.path "alloc::alloc::Global"
                                                  ],
                                                "len",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| new_module |),
                                                  "move_binary_format::normalized::Module",
                                                  "functions"
                                                |)
                                              ]
                                            |)
                                          |)))
                                      |),
                                      ltac:(M.monadic
                                        (BinOp.ne (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.path
                                                    "move_core_types::language_storage::ModuleId";
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "len",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| old_module |),
                                                "move_binary_format::normalized::Module",
                                                "friends"
                                              |)
                                            ]
                                          |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.path
                                                    "move_core_types::language_storage::ModuleId";
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "len",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| new_module |),
                                                "move_binary_format::normalized::Module",
                                                "friends"
                                              |)
                                            ]
                                          |)
                                        |)))
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (| M.read (| M.return_ (| M.read (| err |) |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                                  []
                                  [
                                    Ty.path "move_core_types::identifier::Identifier";
                                    Ty.path "move_binary_format::normalized::Struct";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| old_module |),
                              "move_binary_format::normalized::Module",
                              "structs"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::map::Iter")
                                            []
                                            [
                                              Ty.path "move_core_types::identifier::Identifier";
                                              Ty.path "move_binary_format::normalized::Struct"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let name := M.copy (| γ1_0 |) in
                                          let old_struct := M.copy (| γ1_1 |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path
                                                        "alloc::collections::btree::map::BTreeMap")
                                                      []
                                                      [
                                                        Ty.path
                                                          "move_core_types::identifier::Identifier";
                                                        Ty.path
                                                          "move_binary_format::normalized::Struct";
                                                        Ty.path "alloc::alloc::Global"
                                                      ],
                                                    "get",
                                                    [
                                                      Ty.path
                                                        "move_core_types::identifier::Identifier"
                                                    ]
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| new_module |),
                                                      "move_binary_format::normalized::Module",
                                                      "structs"
                                                    |);
                                                    M.read (| name |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::option::Option::Some",
                                                        0
                                                      |) in
                                                    let new_struct := M.copy (| γ0_0 |) in
                                                    let γ :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::cmp::PartialEq",
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::normalized::Struct"
                                                              ],
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "move_binary_format::normalized::Struct"
                                                                ]
                                                            ],
                                                            "eq",
                                                            []
                                                          |),
                                                          [ old_struct; new_struct ]
                                                        |)
                                                      |) in
                                                    let _ :=
                                                      M.is_constant_or_break_match (|
                                                        M.read (| γ |),
                                                        Value.Bool true
                                                      |) in
                                                    M.alloc (| Value.Tuple [] |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (| M.read (| err |) |)
                                                        |)
                                                      |)
                                                    |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                                  []
                                  [
                                    Ty.path "move_core_types::identifier::Identifier";
                                    Ty.path "move_binary_format::normalized::Function";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| old_module |),
                              "move_binary_format::normalized::Module",
                              "functions"
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::map::Iter")
                                            []
                                            [
                                              Ty.path "move_core_types::identifier::Identifier";
                                              Ty.path "move_binary_format::normalized::Function"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let name := M.copy (| γ1_0 |) in
                                          let old_func := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "&")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_binary_format::normalized::Function"
                                                        ]
                                                    ],
                                                  "or_else",
                                                  [
                                                    Ty.function
                                                      [ Ty.tuple [] ]
                                                      (Ty.apply
                                                        (Ty.path "core::option::Option")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              Ty.path
                                                                "move_binary_format::normalized::Function"
                                                            ]
                                                        ])
                                                  ]
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path
                                                          "alloc::collections::btree::map::BTreeMap")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_core_types::identifier::Identifier";
                                                          Ty.path
                                                            "move_binary_format::normalized::Function";
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      "get",
                                                      [
                                                        Ty.path
                                                          "move_core_types::identifier::Identifier"
                                                      ]
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| new_module |),
                                                        "move_binary_format::normalized::Module",
                                                        "functions"
                                                      |);
                                                      M.read (| name |)
                                                    ]
                                                  |);
                                                  M.closure
                                                    (fun γ =>
                                                      ltac:(M.monadic
                                                        match γ with
                                                        | [ α0 ] =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              M.alloc (| α0 |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::collections::btree::map::BTreeMap")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_core_types::identifier::Identifier";
                                                                            Ty.path
                                                                              "move_binary_format::normalized::Function";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ],
                                                                        "get",
                                                                        [
                                                                          Ty.path
                                                                            "move_core_types::identifier::Identifier"
                                                                        ]
                                                                      |),
                                                                      [
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          M.read (| new_module |),
                                                                          "move_binary_format::normalized::Module",
                                                                          "functions"
                                                                        |);
                                                                        M.read (| name |)
                                                                      ]
                                                                    |)))
                                                              ]
                                                            |)))
                                                        | _ =>
                                                          M.impossible "wrong number of arguments"
                                                        end))
                                                ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let new_func := M.copy (| γ0_0 |) in
                                                  let γ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::cmp::PartialEq",
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              Ty.path
                                                                "move_binary_format::normalized::Function"
                                                            ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "move_binary_format::normalized::Function"
                                                              ]
                                                          ],
                                                          "eq",
                                                          []
                                                        |),
                                                        [ old_func; new_func ]
                                                      |)
                                                    |) in
                                                  let _ :=
                                                    M.is_constant_or_break_match (|
                                                      M.read (| γ |),
                                                      Value.Bool true
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (M.alloc (|
                                                    M.never_to_any (|
                                                      M.read (| M.return_ (| M.read (| err |) |) |)
                                                    |)
                                                  |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_check : M.IsAssociatedFunction Self "check" check.
  End Impl_move_binary_format_compatibility_InclusionCheck.
End compatibility.
