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

Module instantiation_loops.
  (* StructTuple
    {
      name := "Node";
      const_params := [];
      ty_params := [];
      fields :=
        [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex"; Ty.path "u16" ];
    } *)
  
  Module Impl_core_cmp_Eq_for_move_bytecode_verifier_instantiation_loops_Node.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::instantiation_loops::Node".
    
    (* 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_bytecode_verifier_instantiation_loops_Node.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_bytecode_verifier_instantiation_loops_Node.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::instantiation_loops::Node".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_bytecode_verifier_instantiation_loops_Node.
  
  Module Impl_core_cmp_PartialEq_for_move_bytecode_verifier_instantiation_loops_Node.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::instantiation_loops::Node".
    
    (* 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 (|
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "move_binary_format::file_format::FunctionDefinitionIndex",
                [ Ty.path "move_binary_format::file_format::FunctionDefinitionIndex" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::instantiation_loops::Node",
                  0
                |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| other |),
                  "move_bytecode_verifier::instantiation_loops::Node",
                  0
                |)
              ]
            |),
            ltac:(M.monadic
              (BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "move_bytecode_verifier::instantiation_loops::Node",
                    1
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| other |),
                    "move_bytecode_verifier::instantiation_loops::Node",
                    1
                  |)
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_move_bytecode_verifier_instantiation_loops_Node.
  
  Module Impl_core_hash_Hash_for_move_bytecode_verifier_instantiation_loops_Node.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::instantiation_loops::Node".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.path "move_binary_format::file_format::FunctionDefinitionIndex",
                    [],
                    "hash",
                    [ __H ]
                  |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "move_bytecode_verifier::instantiation_loops::Node",
                      0
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "u16", [], "hash", [ __H ] |),
                [
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "move_bytecode_verifier::instantiation_loops::Node",
                    1
                  |);
                  M.read (| state |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_move_bytecode_verifier_instantiation_loops_Node.
  
  Module Impl_core_marker_Copy_for_move_bytecode_verifier_instantiation_loops_Node.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::instantiation_loops::Node".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_bytecode_verifier_instantiation_loops_Node.
  
  Module Impl_core_clone_Clone_for_move_bytecode_verifier_instantiation_loops_Node.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::instantiation_loops::Node".
    
    (* 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_bytecode_verifier_instantiation_loops_Node.
  
  (*
  Enum Edge
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Identity";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "TyConApp";
          item :=
            StructTuple
              [
                Ty.apply
                  (Ty.path "&")
                  []
                  [ Ty.path "move_binary_format::file_format::SignatureToken" ]
              ];
          discriminant := None;
        }
      ];
  }
  *)
  
  (* StructRecord
    {
      name := "InstantiationLoopChecker";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("module",
            Ty.apply
              (Ty.path "&")
              []
              [ Ty.path "move_binary_format::file_format::CompiledModule" ]);
          ("graph",
            Ty.apply
              (Ty.path "petgraph::graph_impl::Graph")
              []
              [
                Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                Ty.path "move_bytecode_verifier::instantiation_loops::Edge";
                Ty.path "petgraph::Directed";
                Ty.path "u32"
              ]);
          ("node_map",
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                Ty.apply (Ty.path "petgraph::graph_impl::NodeIndex") [] [ Ty.path "u32" ];
                Ty.path "std::hash::random::RandomState"
              ]);
          ("func_handle_def_map",
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                Ty.path "std::hash::random::RandomState"
              ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_instantiation_loops_InstantiationLoopChecker.
    Definition Self : Ty.t :=
      Ty.path "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker".
    
    (*
        fn new(module: &'a CompiledModule) -> Self {
            Self {
                module,
                graph: Graph::new(),
                node_map: HashMap::new(),
                func_handle_def_map: module
                    .function_defs()
                    .iter()
                    .enumerate()
                    .map(|(def_idx, def)| (def.function, FunctionDefinitionIndex::new(def_idx as u16)))
                    .collect(),
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ module ] =>
        ltac:(M.monadic
          (let module := M.alloc (| module |) in
          Value.StructRecord
            "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker"
            [
              ("module", M.read (| module |));
              ("graph",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "petgraph::graph_impl::Graph")
                      []
                      [
                        Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                        Ty.path "move_bytecode_verifier::instantiation_loops::Edge";
                        Ty.path "petgraph::Directed";
                        Ty.path "u32"
                      ],
                    "new",
                    []
                  |),
                  []
                |));
              ("node_map",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "std::collections::hash::map::HashMap")
                      []
                      [
                        Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                        Ty.apply (Ty.path "petgraph::graph_impl::NodeIndex") [] [ Ty.path "u32" ];
                        Ty.path "std::hash::random::RandomState"
                      ],
                    "new",
                    []
                  |),
                  []
                |));
              ("func_handle_def_map",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Ty.apply
                      (Ty.path "core::iter::adapters::map::Map")
                      []
                      [
                        Ty.apply
                          (Ty.path "core::iter::adapters::enumerate::Enumerate")
                          []
                          [
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                          ];
                        Ty.function
                          [
                            Ty.tuple
                              [
                                Ty.tuple
                                  [
                                    Ty.path "usize";
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.path
                                          "move_binary_format::file_format::FunctionDefinition"
                                      ]
                                  ]
                              ]
                          ]
                          (Ty.tuple
                            [
                              Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                              Ty.path "move_binary_format::file_format::FunctionDefinitionIndex"
                            ])
                      ],
                    [],
                    "collect",
                    [
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                          Ty.path "move_binary_format::file_format::FunctionDefinitionIndex";
                          Ty.path "std::hash::random::RandomState"
                        ]
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::enumerate::Enumerate")
                          []
                          [
                            Ty.apply
                              (Ty.path "core::slice::iter::Iter")
                              []
                              [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                          ],
                        [],
                        "map",
                        [
                          Ty.tuple
                            [
                              Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                              Ty.path "move_binary_format::file_format::FunctionDefinitionIndex"
                            ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.tuple
                                    [
                                      Ty.path "usize";
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [
                                          Ty.path
                                            "move_binary_format::file_format::FunctionDefinition"
                                        ]
                                    ]
                                ]
                            ]
                            (Ty.tuple
                              [
                                Ty.path "move_binary_format::file_format::FunctionHandleIndex";
                                Ty.path "move_binary_format::file_format::FunctionDefinitionIndex"
                              ])
                        ]
                      |),
                      [
                        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::FunctionDefinition" ],
                            [],
                            "enumerate",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "slice")
                                  []
                                  [ Ty.path "move_binary_format::file_format::FunctionDefinition" ],
                                "iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::file_format::CompiledModule",
                                    "function_defs",
                                    []
                                  |),
                                  [ M.read (| module |) ]
                                |)
                              ]
                            |)
                          ]
                        |);
                        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 def_idx := M.copy (| γ0_0 |) in
                                          let def := M.copy (| γ0_1 |) in
                                          Value.Tuple
                                            [
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| def |),
                                                  "move_binary_format::file_format::FunctionDefinition",
                                                  "function"
                                                |)
                                              |);
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionDefinitionIndex",
                                                  "new",
                                                  []
                                                |),
                                                [ M.rust_cast (M.read (| def_idx |)) ]
                                              |)
                                            ]))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn verify_module(module: &'a CompiledModule) -> VMResult<()> {
            Self::verify_module_impl(module).map_err(|e| e.finish(Location::Module(module.self_id())))
        }
    *)
    Definition verify_module (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ module ] =>
        ltac:(M.monadic
          (let module := M.alloc (| module |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::result::Result")
                []
                [ Ty.tuple []; Ty.path "move_binary_format::errors::PartialVMError" ],
              "map_err",
              [
                Ty.path "move_binary_format::errors::VMError";
                Ty.function
                  [ Ty.tuple [ Ty.path "move_binary_format::errors::PartialVMError" ] ]
                  (Ty.path "move_binary_format::errors::VMError")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                  "verify_module_impl",
                  []
                |),
                [ M.read (| module |) ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let e := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_binary_format::errors::PartialVMError",
                                    "finish",
                                    []
                                  |),
                                  [
                                    M.read (| e |);
                                    Value.StructTuple
                                      "move_binary_format::errors::Location::Module"
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path
                                              "move_binary_format::file_format::CompiledModule",
                                            "self_id",
                                            []
                                          |),
                                          [ M.read (| module |) ]
                                        |)
                                      ]
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module :
      M.IsAssociatedFunction Self "verify_module" verify_module.
    
    (*
        fn verify_module_impl(module: &'a CompiledModule) -> PartialVMResult<()> {
            let mut checker = Self::new(module);
            checker.build_graph();
            let mut components = checker.find_non_trivial_components();
    
            match components.pop() {
                None => Ok(()),
                Some((nodes, edges)) => {
                    let msg_edges = edges
                        .into_iter()
                        .filter_map(
                            |edge_idx| match checker.graph.edge_weight(edge_idx).unwrap() {
                                Edge::TyConApp(_) => Some(checker.format_edge(edge_idx)),
                                _ => None,
                            },
                        )
                        .collect::<Vec<_>>()
                        .join(", ");
                    let msg_nodes = nodes
                        .into_iter()
                        .map(|node_idx| checker.format_node(node_idx))
                        .collect::<Vec<_>>()
                        .join(", ");
                    let msg = format!(
                        "edges with constructors: [{}], nodes: [{}]",
                        msg_edges, msg_nodes
                    );
                    Err(PartialVMError::new(StatusCode::LOOP_IN_INSTANTIATION_GRAPH).with_message(msg))
                }
            }
        }
    *)
    Definition verify_module_impl (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ module ] =>
        ltac:(M.monadic
          (let module := M.alloc (| module |) in
          M.read (|
            let~ checker :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                    "new",
                    []
                  |),
                  [ M.read (| module |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                    "build_graph",
                    []
                  |),
                  [ checker ]
                |)
              |) in
            let~ components :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                    "find_non_trivial_components",
                    []
                  |),
                  [ checker ]
                |)
              |) in
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "petgraph::graph_impl::NodeIndex")
                                  []
                                  [ Ty.path "u32" ];
                                Ty.path "alloc::alloc::Global"
                              ];
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "petgraph::graph_impl::EdgeIndex")
                                  []
                                  [ Ty.path "u32" ];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "pop",
                    []
                  |),
                  [ components ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                    M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)));
                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 nodes := M.copy (| γ1_0 |) in
                    let edges := M.copy (| γ1_1 |) in
                    let~ msg_edges :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "alloc::string::String" ],
                            "join",
                            [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [ Ty.path "alloc::string::String"; Ty.path "alloc::alloc::Global"
                                  ],
                                [],
                                "deref",
                                []
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::iter::adapters::filter_map::FilterMap")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "alloc::vec::into_iter::IntoIter")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "petgraph::graph_impl::EdgeIndex")
                                                []
                                                [ Ty.path "u32" ];
                                              Ty.path "alloc::alloc::Global"
                                            ];
                                          Ty.function
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.apply
                                                    (Ty.path "petgraph::graph_impl::EdgeIndex")
                                                    []
                                                    [ Ty.path "u32" ]
                                                ]
                                            ]
                                            (Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [ Ty.path "alloc::string::String" ])
                                        ],
                                      [],
                                      "collect",
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path "alloc::string::String";
                                            Ty.path "alloc::alloc::Global"
                                          ]
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "alloc::vec::into_iter::IntoIter")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "petgraph::graph_impl::EdgeIndex")
                                                []
                                                [ Ty.path "u32" ];
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          [],
                                          "filter_map",
                                          [
                                            Ty.path "alloc::string::String";
                                            Ty.function
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply
                                                      (Ty.path "petgraph::graph_impl::EdgeIndex")
                                                      []
                                                      [ Ty.path "u32" ]
                                                  ]
                                              ]
                                              (Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "alloc::string::String" ])
                                          ]
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::collect::IntoIterator",
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "petgraph::graph_impl::EdgeIndex")
                                                    []
                                                    [ Ty.path "u32" ];
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              [],
                                              "into_iter",
                                              []
                                            |),
                                            [ M.read (| edges |) ]
                                          |);
                                          M.closure
                                            (fun γ =>
                                              ltac:(M.monadic
                                                match γ with
                                                | [ α0 ] =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| α0 |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let edge_idx := M.copy (| γ |) in
                                                            M.read (|
                                                              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_bytecode_verifier::instantiation_loops::Edge"
                                                                            ]
                                                                        ],
                                                                      "unwrap",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "petgraph::graph_impl::Graph")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "move_bytecode_verifier::instantiation_loops::Node";
                                                                              Ty.path
                                                                                "move_bytecode_verifier::instantiation_loops::Edge";
                                                                              Ty.path
                                                                                "petgraph::Directed";
                                                                              Ty.path "u32"
                                                                            ],
                                                                          "edge_weight",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            checker,
                                                                            "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                            "graph"
                                                                          |);
                                                                          M.read (| edge_idx |)
                                                                        ]
                                                                      |)
                                                                    ]
                                                                  |)
                                                                |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ := M.read (| γ |) in
                                                                      let γ1_0 :=
                                                                        M.SubPointer.get_struct_tuple_field (|
                                                                          γ,
                                                                          "move_bytecode_verifier::instantiation_loops::Edge::TyConApp",
                                                                          0
                                                                        |) in
                                                                      M.alloc (|
                                                                        Value.StructTuple
                                                                          "core::option::Option::Some"
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                                "format_edge",
                                                                                []
                                                                              |),
                                                                              [
                                                                                checker;
                                                                                M.read (|
                                                                                  edge_idx
                                                                                |)
                                                                              ]
                                                                            |)
                                                                          ]
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (M.alloc (|
                                                                        Value.StructTuple
                                                                          "core::option::Option::None"
                                                                          []
                                                                      |)))
                                                                ]
                                                              |)
                                                            |)))
                                                      ]
                                                    |)))
                                                | _ => M.impossible "wrong number of arguments"
                                                end))
                                        ]
                                      |)
                                    ]
                                  |)
                                |)
                              ]
                            |);
                            M.read (| Value.String ", " |)
                          ]
                        |)
                      |) in
                    let~ msg_nodes :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "alloc::string::String" ],
                            "join",
                            [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [ Ty.path "alloc::string::String"; Ty.path "alloc::alloc::Global"
                                  ],
                                [],
                                "deref",
                                []
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::iter::adapters::map::Map")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "alloc::vec::into_iter::IntoIter")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "petgraph::graph_impl::NodeIndex")
                                                []
                                                [ Ty.path "u32" ];
                                              Ty.path "alloc::alloc::Global"
                                            ];
                                          Ty.function
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.apply
                                                    (Ty.path "petgraph::graph_impl::NodeIndex")
                                                    []
                                                    [ Ty.path "u32" ]
                                                ]
                                            ]
                                            (Ty.path "alloc::string::String")
                                        ],
                                      [],
                                      "collect",
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path "alloc::string::String";
                                            Ty.path "alloc::alloc::Global"
                                          ]
                                      ]
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "alloc::vec::into_iter::IntoIter")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "petgraph::graph_impl::NodeIndex")
                                                []
                                                [ Ty.path "u32" ];
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          [],
                                          "map",
                                          [
                                            Ty.path "alloc::string::String";
                                            Ty.function
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply
                                                      (Ty.path "petgraph::graph_impl::NodeIndex")
                                                      []
                                                      [ Ty.path "u32" ]
                                                  ]
                                              ]
                                              (Ty.path "alloc::string::String")
                                          ]
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::collect::IntoIterator",
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "petgraph::graph_impl::NodeIndex")
                                                    []
                                                    [ Ty.path "u32" ];
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              [],
                                              "into_iter",
                                              []
                                            |),
                                            [ M.read (| nodes |) ]
                                          |);
                                          M.closure
                                            (fun γ =>
                                              ltac:(M.monadic
                                                match γ with
                                                | [ α0 ] =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| α0 |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let node_idx := M.copy (| γ |) in
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                "format_node",
                                                                []
                                                              |),
                                                              [ checker; M.read (| node_idx |) ]
                                                            |)))
                                                      ]
                                                    |)))
                                                | _ => M.impossible "wrong number of arguments"
                                                end))
                                        ]
                                      |)
                                    ]
                                  |)
                                |)
                              ]
                            |);
                            M.read (| Value.String ", " |)
                          ]
                        |)
                      |) in
                    let~ msg :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::hint::must_use",
                            [ Ty.path "alloc::string::String" ]
                          |),
                          [
                            M.read (|
                              let~ res :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_function (| "alloc::fmt::format", [] |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "core::fmt::Arguments",
                                          "new_v1",
                                          []
                                        |),
                                        [
                                          M.alloc (|
                                            Value.Array
                                              [
                                                M.read (|
                                                  Value.String "edges with constructors: ["
                                                |);
                                                M.read (| Value.String "], nodes: [" |);
                                                M.read (| Value.String "]" |)
                                              ]
                                          |);
                                          M.alloc (|
                                            Value.Array
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::fmt::rt::Argument",
                                                    "new_display",
                                                    [ Ty.path "alloc::string::String" ]
                                                  |),
                                                  [ msg_edges ]
                                                |);
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::fmt::rt::Argument",
                                                    "new_display",
                                                    [ Ty.path "alloc::string::String" ]
                                                  |),
                                                  [ msg_nodes ]
                                                |)
                                              ]
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |) in
                              res
                            |)
                          ]
                        |)
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::result::Result::Err"
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_binary_format::errors::PartialVMError",
                              "with_message",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "move_binary_format::errors::PartialVMError",
                                  "new",
                                  []
                                |),
                                [
                                  Value.StructTuple
                                    "move_core_types::vm_status::StatusCode::LOOP_IN_INSTANTIATION_GRAPH"
                                    []
                                ]
                              |);
                              M.read (| msg |)
                            ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_verify_module_impl :
      M.IsAssociatedFunction Self "verify_module_impl" verify_module_impl.
    
    (*
        fn get_or_add_node(&mut self, node: Node) -> NodeIndex {
            match self.node_map.entry(node) {
                hash_map::Entry::Occupied(entry) => *entry.get(),
                hash_map::Entry::Vacant(entry) => {
                    let idx = self.graph.add_node(node);
                    entry.insert(idx);
                    idx
                }
            }
        }
    *)
    Definition get_or_add_node (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; node ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let node := M.alloc (| node |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "std::collections::hash::map::HashMap")
                      []
                      [
                        Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                        Ty.apply (Ty.path "petgraph::graph_impl::NodeIndex") [] [ Ty.path "u32" ];
                        Ty.path "std::hash::random::RandomState"
                      ],
                    "entry",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                      "node_map"
                    |);
                    M.read (| node |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "std::collections::hash::map::Entry::Occupied",
                        0
                      |) in
                    let entry := M.copy (| γ0_0 |) in
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::OccupiedEntry")
                          []
                          [
                            Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                            Ty.apply
                              (Ty.path "petgraph::graph_impl::NodeIndex")
                              []
                              [ Ty.path "u32" ]
                          ],
                        "get",
                        []
                      |),
                      [ entry ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "std::collections::hash::map::Entry::Vacant",
                        0
                      |) in
                    let entry := M.copy (| γ0_0 |) in
                    let~ idx :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "petgraph::graph_impl::Graph")
                              []
                              [
                                Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                                Ty.path "move_bytecode_verifier::instantiation_loops::Edge";
                                Ty.path "petgraph::Directed";
                                Ty.path "u32"
                              ],
                            "add_node",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                              "graph"
                            |);
                            M.read (| node |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "std::collections::hash::map::VacantEntry")
                              []
                              [
                                Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                                Ty.apply
                                  (Ty.path "petgraph::graph_impl::NodeIndex")
                                  []
                                  [ Ty.path "u32" ]
                              ],
                            "insert",
                            []
                          |),
                          [ M.read (| entry |); M.read (| idx |) ]
                        |)
                      |) in
                    idx))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_or_add_node :
      M.IsAssociatedFunction Self "get_or_add_node" get_or_add_node.
    
    (*
        fn extract_type_parameters(&self, ty: &SignatureToken) -> HashSet<TypeParameterIndex> {
            use SignatureToken::*;
    
            let mut type_params = HashSet::new();
    
            fn rec(type_params: &mut HashSet<TypeParameterIndex>, ty: &SignatureToken) {
                match ty {
                    Bool | Address | U8 | U16 | U32 | U64 | U128 | U256 | Signer | Struct(_) => (),
                    TypeParameter(idx) => {
                        type_params.insert( *idx);
                    }
                    Vector(ty) => rec(type_params, ty),
                    Reference(ty) | MutableReference(ty) => rec(type_params, ty),
                    StructInstantiation(struct_inst) => {
                        let (_, tys) = &**struct_inst;
                        for ty in tys {
                            rec(type_params, ty);
                        }
                    }
                }
            }
    
            rec(&mut type_params, ty);
            type_params
        }
    *)
    Definition extract_type_parameters (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; ty ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let ty := M.alloc (| ty |) in
          M.read (|
            let~ type_params :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "std::collections::hash::set::HashSet")
                      []
                      [ Ty.path "u16"; Ty.path "std::hash::random::RandomState" ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Self, "rec.extract_type_parameters", [] |),
                  [ type_params; M.read (| ty |) ]
                |)
              |) in
            type_params
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_extract_type_parameters :
      M.IsAssociatedFunction Self "extract_type_parameters" extract_type_parameters.
    
    (*
        fn add_edge(&mut self, node_from: Node, node_to: Node, edge: Edge<'a>) {
            let node_from_idx = self.get_or_add_node(node_from);
            let node_to_idx = self.get_or_add_node(node_to);
            self.graph.add_edge(node_from_idx, node_to_idx, edge);
        }
    *)
    Definition add_edge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; node_from; node_to; edge ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let node_from := M.alloc (| node_from |) in
          let node_to := M.alloc (| node_to |) in
          let edge := M.alloc (| edge |) in
          M.read (|
            let~ node_from_idx :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                    "get_or_add_node",
                    []
                  |),
                  [ M.read (| self |); M.read (| node_from |) ]
                |)
              |) in
            let~ node_to_idx :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                    "get_or_add_node",
                    []
                  |),
                  [ M.read (| self |); M.read (| node_to |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "petgraph::graph_impl::Graph")
                      []
                      [
                        Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                        Ty.path "move_bytecode_verifier::instantiation_loops::Edge";
                        Ty.path "petgraph::Directed";
                        Ty.path "u32"
                      ],
                    "add_edge",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                      "graph"
                    |);
                    M.read (| node_from_idx |);
                    M.read (| node_to_idx |);
                    M.read (| edge |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_add_edge : M.IsAssociatedFunction Self "add_edge" add_edge.
    
    (*
        fn build_graph_call(
            &mut self,
            caller_idx: FunctionDefinitionIndex,
            callee_idx: FunctionDefinitionIndex,
            type_actuals_idx: SignatureIndex,
        ) {
            let type_actuals = &self.module.signature_at(type_actuals_idx).0;
    
            for (formal_idx, ty) in type_actuals.iter().enumerate() {
                let formal_idx = formal_idx as TypeParameterIndex;
                match ty {
                    SignatureToken::TypeParameter(actual_idx) => self.add_edge(
                        Node(caller_idx, *actual_idx),
                        Node(callee_idx, formal_idx),
                        Edge::Identity,
                    ),
                    _ => {
                        for type_param in self.extract_type_parameters(ty) {
                            self.add_edge(
                                Node(caller_idx, type_param),
                                Node(callee_idx, formal_idx),
                                Edge::TyConApp(ty),
                            );
                        }
                    }
                }
            }
        }
    *)
    Definition build_graph_call (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; caller_idx; callee_idx; type_actuals_idx ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let caller_idx := M.alloc (| caller_idx |) in
          let callee_idx := M.alloc (| callee_idx |) in
          let type_actuals_idx := M.alloc (| type_actuals_idx |) in
          M.read (|
            let~ type_actuals :=
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "move_binary_format::file_format::CompiledModule",
                      "signature_at",
                      []
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                          "module"
                        |)
                      |);
                      M.read (| type_actuals_idx |)
                    ]
                  |),
                  "move_binary_format::file_format::Signature",
                  0
                |)
              |) in
            M.use
              (M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      Ty.apply
                        (Ty.path "core::iter::adapters::enumerate::Enumerate")
                        []
                        [
                          Ty.apply
                            (Ty.path "core::slice::iter::Iter")
                            []
                            [ Ty.path "move_binary_format::file_format::SignatureToken" ]
                        ],
                      [],
                      "into_iter",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Ty.apply
                            (Ty.path "core::slice::iter::Iter")
                            []
                            [ Ty.path "move_binary_format::file_format::SignatureToken" ],
                          [],
                          "enumerate",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "slice")
                                []
                                [ Ty.path "move_binary_format::file_format::SignatureToken" ],
                              "iter",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.path "move_binary_format::file_format::SignatureToken";
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  [],
                                  "deref",
                                  []
                                |),
                                [ M.read (| type_actuals |) ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let iter := M.copy (| γ |) in
                      M.loop (|
                        ltac:(M.monadic
                          (let~ _ :=
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply
                                      (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "core::slice::iter::Iter")
                                          []
                                          [
                                            Ty.path
                                              "move_binary_format::file_format::SignatureToken"
                                          ]
                                      ],
                                    [],
                                    "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 formal_idx := M.copy (| γ1_0 |) in
                                    let ty := M.copy (| γ1_1 |) in
                                    let~ formal_idx :=
                                      M.alloc (| M.rust_cast (M.read (| formal_idx |)) |) in
                                    M.match_operator (|
                                      ty,
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ := M.read (| γ |) in
                                            let γ1_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "move_binary_format::file_format::SignatureToken::TypeParameter",
                                                0
                                              |) in
                                            let actual_idx := M.alloc (| γ1_0 |) in
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                  "add_edge",
                                                  []
                                                |),
                                                [
                                                  M.read (| self |);
                                                  Value.StructTuple
                                                    "move_bytecode_verifier::instantiation_loops::Node"
                                                    [
                                                      M.read (| caller_idx |);
                                                      M.read (| M.read (| actual_idx |) |)
                                                    ];
                                                  Value.StructTuple
                                                    "move_bytecode_verifier::instantiation_loops::Node"
                                                    [
                                                      M.read (| callee_idx |);
                                                      M.read (| formal_idx |)
                                                    ];
                                                  Value.StructTuple
                                                    "move_bytecode_verifier::instantiation_loops::Edge::Identity"
                                                    []
                                                ]
                                              |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.use
                                              (M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::iter::traits::collect::IntoIterator",
                                                      Ty.apply
                                                        (Ty.path
                                                          "std::collections::hash::set::HashSet")
                                                        []
                                                        [
                                                          Ty.path "u16";
                                                          Ty.path "std::hash::random::RandomState"
                                                        ],
                                                      [],
                                                      "into_iter",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                          "extract_type_parameters",
                                                          []
                                                        |),
                                                        [ M.read (| self |); M.read (| ty |) ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  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
                                                                        "std::collections::hash::set::IntoIter")
                                                                      []
                                                                      [ Ty.path "u16" ],
                                                                    [],
                                                                    "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 type_param :=
                                                                      M.copy (| γ0_0 |) in
                                                                    let~ _ :=
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                            "add_edge",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.read (| self |);
                                                                            Value.StructTuple
                                                                              "move_bytecode_verifier::instantiation_loops::Node"
                                                                              [
                                                                                M.read (|
                                                                                  caller_idx
                                                                                |);
                                                                                M.read (|
                                                                                  type_param
                                                                                |)
                                                                              ];
                                                                            Value.StructTuple
                                                                              "move_bytecode_verifier::instantiation_loops::Node"
                                                                              [
                                                                                M.read (|
                                                                                  callee_idx
                                                                                |);
                                                                                M.read (|
                                                                                  formal_idx
                                                                                |)
                                                                              ];
                                                                            Value.StructTuple
                                                                              "move_bytecode_verifier::instantiation_loops::Edge::TyConApp"
                                                                              [ M.read (| ty |) ]
                                                                          ]
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)))
                                                      |)))
                                                ]
                                              |))))
                                      ]
                                    |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                      |)))
                ]
              |))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_build_graph_call :
      M.IsAssociatedFunction Self "build_graph_call" build_graph_call.
    
    (*
        fn build_graph_function_def(
            &mut self,
            caller_idx: FunctionDefinitionIndex,
            caller_def: &FunctionDefinition,
        ) {
            if let Some(code) = &caller_def.code {
                for instr in &code.code {
                    if let Bytecode::CallGeneric(callee_inst_idx) = instr {
                        // Get the id of the definition of the function being called.
                        // Skip if the function is not defined in the current module, as we do not
                        // have mutual recursions across module boundaries.
                        let callee_si = self.module.function_instantiation_at( *callee_inst_idx);
                        if let Some(callee_idx) = self.func_handle_def_map.get(&callee_si.handle) {
                            let callee_idx = *callee_idx;
                            self.build_graph_call(caller_idx, callee_idx, callee_si.type_parameters)
                        }
                    }
                }
            }
        }
    *)
    Definition build_graph_function_def (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; caller_idx; caller_def ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let caller_idx := M.alloc (| caller_idx |) in
          let caller_def := M.alloc (| caller_def |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.alloc (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| caller_def |),
                          "move_binary_format::file_format::FunctionDefinition",
                          "code"
                        |)
                      |) in
                    let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let code := M.alloc (| γ1_0 |) in
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply
                                (Ty.path "&")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.path "move_binary_format::file_format::Bytecode";
                                      Ty.path "alloc::alloc::Global"
                                    ]
                                ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| code |),
                                "move_binary_format::file_format::CodeUnit",
                                "code"
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [ Ty.path "move_binary_format::file_format::Bytecode"
                                              ],
                                            [],
                                            "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 instr := M.copy (| γ0_0 |) in
                                            M.match_operator (|
                                              M.alloc (| Value.Tuple [] |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ := instr in
                                                    let γ := M.read (| γ |) in
                                                    let γ1_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "move_binary_format::file_format::Bytecode::CallGeneric",
                                                        0
                                                      |) in
                                                    let callee_inst_idx := M.alloc (| γ1_0 |) in
                                                    let~ callee_si :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path
                                                              "move_binary_format::file_format::CompiledModule",
                                                            "function_instantiation_at",
                                                            []
                                                          |),
                                                          [
                                                            M.read (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| self |),
                                                                "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                "module"
                                                              |)
                                                            |);
                                                            M.read (|
                                                              M.read (| callee_inst_idx |)
                                                            |)
                                                          ]
                                                        |)
                                                      |) in
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "std::collections::hash::map::HashMap")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "move_binary_format::file_format::FunctionHandleIndex";
                                                                        Ty.path
                                                                          "move_binary_format::file_format::FunctionDefinitionIndex";
                                                                        Ty.path
                                                                          "std::hash::random::RandomState"
                                                                      ],
                                                                    "get",
                                                                    [
                                                                      Ty.path
                                                                        "move_binary_format::file_format::FunctionHandleIndex"
                                                                    ]
                                                                  |),
                                                                  [
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| self |),
                                                                      "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                      "func_handle_def_map"
                                                                    |);
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| callee_si |),
                                                                      "move_binary_format::file_format::FunctionInstantiation",
                                                                      "handle"
                                                                    |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::option::Option::Some",
                                                                0
                                                              |) in
                                                            let callee_idx := M.copy (| γ0_0 |) in
                                                            let~ callee_idx :=
                                                              M.copy (|
                                                                M.read (| callee_idx |)
                                                              |) in
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.path
                                                                    "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                  "build_graph_call",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| self |);
                                                                  M.read (| caller_idx |);
                                                                  M.read (| callee_idx |);
                                                                  M.read (|
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| callee_si |),
                                                                      "move_binary_format::file_format::FunctionInstantiation",
                                                                      "type_parameters"
                                                                    |)
                                                                  |)
                                                                ]
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (| Value.Tuple [] |)))
                                                      ]
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |))));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_build_graph_function_def :
      M.IsAssociatedFunction Self "build_graph_function_def" build_graph_function_def.
    
    (*
        fn build_graph(&mut self) {
            for (def_idx, func_def) in self
                .module
                .function_defs()
                .iter()
                .enumerate()
                .filter(|(_, def)| !def.is_native())
            {
                self.build_graph_function_def(FunctionDefinitionIndex::new(def_idx as u16), func_def)
            }
        }
    *)
    Definition build_graph (ε : 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.use
              (M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      Ty.apply
                        (Ty.path "core::iter::adapters::filter::Filter")
                        []
                        [
                          Ty.apply
                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                []
                                [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                            ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [
                                      Ty.tuple
                                        [
                                          Ty.path "usize";
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.path
                                                "move_binary_format::file_format::FunctionDefinition"
                                            ]
                                        ]
                                    ]
                                ]
                            ]
                            (Ty.path "bool")
                        ],
                      [],
                      "into_iter",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::iterator::Iterator",
                          Ty.apply
                            (Ty.path "core::iter::adapters::enumerate::Enumerate")
                            []
                            [
                              Ty.apply
                                (Ty.path "core::slice::iter::Iter")
                                []
                                [ Ty.path "move_binary_format::file_format::FunctionDefinition" ]
                            ],
                          [],
                          "filter",
                          [
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.tuple
                                          [
                                            Ty.path "usize";
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.path
                                                  "move_binary_format::file_format::FunctionDefinition"
                                              ]
                                          ]
                                      ]
                                  ]
                              ]
                              (Ty.path "bool")
                          ]
                        |),
                        [
                          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::FunctionDefinition" ],
                              [],
                              "enumerate",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [ Ty.path "move_binary_format::file_format::FunctionDefinition"
                                    ],
                                  "iter",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_binary_format::file_format::CompiledModule",
                                      "function_defs",
                                      []
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                          "module"
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |);
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [ α0 ] =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      M.alloc (| α0 |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ := M.read (| γ |) in
                                            let γ1_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                            let γ1_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                            let def := M.alloc (| γ1_1 |) in
                                            UnOp.not (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_binary_format::file_format::FunctionDefinition",
                                                  "is_native",
                                                  []
                                                |),
                                                [ M.read (| M.read (| def |) |) ]
                                              |)
                                            |)))
                                      ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        ]
                      |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let iter := M.copy (| γ |) in
                      M.loop (|
                        ltac:(M.monadic
                          (let~ _ :=
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply
                                      (Ty.path "core::iter::adapters::filter::Filter")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "core::slice::iter::Iter")
                                              []
                                              [
                                                Ty.path
                                                  "move_binary_format::file_format::FunctionDefinition"
                                              ]
                                          ];
                                        Ty.function
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.path "usize";
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_binary_format::file_format::FunctionDefinition"
                                                          ]
                                                      ]
                                                  ]
                                              ]
                                          ]
                                          (Ty.path "bool")
                                      ],
                                    [],
                                    "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 def_idx := M.copy (| γ1_0 |) in
                                    let func_def := M.copy (| γ1_1 |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path
                                            "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                          "build_graph_function_def",
                                          []
                                        |),
                                        [
                                          M.read (| self |);
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_binary_format::file_format::FunctionDefinitionIndex",
                                              "new",
                                              []
                                            |),
                                            [ M.rust_cast (M.read (| def_idx |)) ]
                                          |);
                                          M.read (| func_def |)
                                        ]
                                      |)
                                    |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                      |)))
                ]
              |))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_build_graph : M.IsAssociatedFunction Self "build_graph" build_graph.
    
    (*
        fn find_non_trivial_components(&self) -> Vec<(Vec<NodeIndex>, Vec<EdgeIndex>)> {
            tarjan_scc(&self.graph)
                .into_iter()
                .filter_map(move |nodes| {
                    let node_set: HashSet<_> = nodes.iter().cloned().collect();
    
                    let edges: Vec<_> = nodes
                        .iter()
                        .flat_map(|node_idx| {
                            self.graph.edges( *node_idx).filter_map(|edge| {
                                if node_set.contains(&edge.target()) {
                                    Some(edge.id())
                                } else {
                                    None
                                }
                            })
                        })
                        .collect();
    
                    if edges.iter().any(
                        |edge_idx| match self.graph.edge_weight( *edge_idx).unwrap() {
                            Edge::Identity => false,
                            Edge::TyConApp(_) => true,
                        },
                    ) {
                        Some((nodes, edges))
                    } else {
                        None
                    }
                })
                .collect()
        }
    *)
    Definition find_non_trivial_components
        (ε : 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::iter::traits::iterator::Iterator",
              Ty.apply
                (Ty.path "core::iter::adapters::filter_map::FilterMap")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::into_iter::IntoIter")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply (Ty.path "petgraph::graph_impl::NodeIndex") [] [ Ty.path "u32" ];
                          Ty.path "alloc::alloc::Global"
                        ];
                      Ty.path "alloc::alloc::Global"
                    ];
                  Ty.function
                    [
                      Ty.tuple
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.apply
                                (Ty.path "petgraph::graph_impl::NodeIndex")
                                []
                                [ Ty.path "u32" ];
                              Ty.path "alloc::alloc::Global"
                            ]
                        ]
                    ]
                    (Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "petgraph::graph_impl::NodeIndex")
                                  []
                                  [ Ty.path "u32" ];
                                Ty.path "alloc::alloc::Global"
                              ];
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "petgraph::graph_impl::EdgeIndex")
                                  []
                                  [ Ty.path "u32" ];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ]
                      ])
                ],
              [],
              "collect",
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply
                              (Ty.path "petgraph::graph_impl::NodeIndex")
                              []
                              [ Ty.path "u32" ];
                            Ty.path "alloc::alloc::Global"
                          ];
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply
                              (Ty.path "petgraph::graph_impl::EdgeIndex")
                              []
                              [ Ty.path "u32" ];
                            Ty.path "alloc::alloc::Global"
                          ]
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]
              ]
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply
                    (Ty.path "alloc::vec::into_iter::IntoIter")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply (Ty.path "petgraph::graph_impl::NodeIndex") [] [ Ty.path "u32" ];
                          Ty.path "alloc::alloc::Global"
                        ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  [],
                  "filter_map",
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply
                              (Ty.path "petgraph::graph_impl::NodeIndex")
                              []
                              [ Ty.path "u32" ];
                            Ty.path "alloc::alloc::Global"
                          ];
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply
                              (Ty.path "petgraph::graph_impl::EdgeIndex")
                              []
                              [ Ty.path "u32" ];
                            Ty.path "alloc::alloc::Global"
                          ]
                      ];
                    Ty.function
                      [
                        Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "petgraph::graph_impl::NodeIndex")
                                  []
                                  [ Ty.path "u32" ];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ]
                      ]
                      (Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [
                          Ty.tuple
                            [
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "petgraph::graph_impl::NodeIndex")
                                    []
                                    [ Ty.path "u32" ];
                                  Ty.path "alloc::alloc::Global"
                                ];
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "petgraph::graph_impl::EdgeIndex")
                                    []
                                    [ Ty.path "u32" ];
                                  Ty.path "alloc::alloc::Global"
                                ]
                            ]
                        ])
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.apply
                                (Ty.path "petgraph::graph_impl::NodeIndex")
                                []
                                [ Ty.path "u32" ];
                              Ty.path "alloc::alloc::Global"
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "into_iter",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_function (|
                          "petgraph::algo::tarjan_scc",
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "petgraph::graph_impl::Graph")
                                  []
                                  [
                                    Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                                    Ty.path "move_bytecode_verifier::instantiation_loops::Edge";
                                    Ty.path "petgraph::Directed";
                                    Ty.path "u32"
                                  ]
                              ]
                          ]
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                            "graph"
                          |)
                        ]
                      |)
                    ]
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let nodes := M.copy (| γ |) in
                                    M.read (|
                                      let~ node_set :=
                                        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.apply
                                                        (Ty.path "petgraph::graph_impl::NodeIndex")
                                                        []
                                                        [ Ty.path "u32" ]
                                                    ]
                                                ],
                                              [],
                                              "collect",
                                              [
                                                Ty.apply
                                                  (Ty.path "std::collections::hash::set::HashSet")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "petgraph::graph_impl::NodeIndex")
                                                      []
                                                      [ Ty.path "u32" ];
                                                    Ty.path "std::hash::random::RandomState"
                                                  ]
                                              ]
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::Iter")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "petgraph::graph_impl::NodeIndex")
                                                        []
                                                        [ Ty.path "u32" ]
                                                    ],
                                                  [],
                                                  "cloned",
                                                  [
                                                    Ty.apply
                                                      (Ty.path "petgraph::graph_impl::NodeIndex")
                                                      []
                                                      [ Ty.path "u32" ]
                                                  ]
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "slice")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path
                                                              "petgraph::graph_impl::NodeIndex")
                                                            []
                                                            [ Ty.path "u32" ]
                                                        ],
                                                      "iter",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::deref::Deref",
                                                          Ty.apply
                                                            (Ty.path "alloc::vec::Vec")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "petgraph::graph_impl::NodeIndex")
                                                                []
                                                                [ Ty.path "u32" ];
                                                              Ty.path "alloc::alloc::Global"
                                                            ],
                                                          [],
                                                          "deref",
                                                          []
                                                        |),
                                                        [ nodes ]
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ edges :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::iter::adapters::flatten::FlatMap")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::Iter")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "petgraph::graph_impl::NodeIndex")
                                                        []
                                                        [ Ty.path "u32" ]
                                                    ];
                                                  Ty.apply
                                                    (Ty.path
                                                      "core::iter::adapters::filter_map::FilterMap")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "petgraph::graph_impl::Edges")
                                                        []
                                                        [
                                                          Ty.path
                                                            "move_bytecode_verifier::instantiation_loops::Edge";
                                                          Ty.path "petgraph::Directed";
                                                          Ty.path "u32"
                                                        ];
                                                      Ty.function
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "petgraph::graph_impl::EdgeReference")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "move_bytecode_verifier::instantiation_loops::Edge";
                                                                  Ty.path "u32"
                                                                ]
                                                            ]
                                                        ]
                                                        (Ty.apply
                                                          (Ty.path "core::option::Option")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "petgraph::graph_impl::EdgeIndex")
                                                              []
                                                              [ Ty.path "u32" ]
                                                          ])
                                                    ];
                                                  Ty.function
                                                    [
                                                      Ty.tuple
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "petgraph::graph_impl::NodeIndex")
                                                                []
                                                                [ Ty.path "u32" ]
                                                            ]
                                                        ]
                                                    ]
                                                    (Ty.apply
                                                      (Ty.path
                                                        "core::iter::adapters::filter_map::FilterMap")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "petgraph::graph_impl::Edges")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_bytecode_verifier::instantiation_loops::Edge";
                                                            Ty.path "petgraph::Directed";
                                                            Ty.path "u32"
                                                          ];
                                                        Ty.function
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "petgraph::graph_impl::EdgeReference")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "move_bytecode_verifier::instantiation_loops::Edge";
                                                                    Ty.path "u32"
                                                                  ]
                                                              ]
                                                          ]
                                                          (Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "petgraph::graph_impl::EdgeIndex")
                                                                []
                                                                [ Ty.path "u32" ]
                                                            ])
                                                      ])
                                                ],
                                              [],
                                              "collect",
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "petgraph::graph_impl::EdgeIndex")
                                                      []
                                                      [ Ty.path "u32" ];
                                                    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.apply
                                                        (Ty.path "petgraph::graph_impl::NodeIndex")
                                                        []
                                                        [ Ty.path "u32" ]
                                                    ],
                                                  [],
                                                  "flat_map",
                                                  [
                                                    Ty.apply
                                                      (Ty.path
                                                        "core::iter::adapters::filter_map::FilterMap")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "petgraph::graph_impl::Edges")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_bytecode_verifier::instantiation_loops::Edge";
                                                            Ty.path "petgraph::Directed";
                                                            Ty.path "u32"
                                                          ];
                                                        Ty.function
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "petgraph::graph_impl::EdgeReference")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "move_bytecode_verifier::instantiation_loops::Edge";
                                                                    Ty.path "u32"
                                                                  ]
                                                              ]
                                                          ]
                                                          (Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "petgraph::graph_impl::EdgeIndex")
                                                                []
                                                                [ Ty.path "u32" ]
                                                            ])
                                                      ];
                                                    Ty.function
                                                      [
                                                        Ty.tuple
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "petgraph::graph_impl::NodeIndex")
                                                                  []
                                                                  [ Ty.path "u32" ]
                                                              ]
                                                          ]
                                                      ]
                                                      (Ty.apply
                                                        (Ty.path
                                                          "core::iter::adapters::filter_map::FilterMap")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "petgraph::graph_impl::Edges")
                                                            []
                                                            [
                                                              Ty.path
                                                                "move_bytecode_verifier::instantiation_loops::Edge";
                                                              Ty.path "petgraph::Directed";
                                                              Ty.path "u32"
                                                            ];
                                                          Ty.function
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "petgraph::graph_impl::EdgeReference")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "move_bytecode_verifier::instantiation_loops::Edge";
                                                                      Ty.path "u32"
                                                                    ]
                                                                ]
                                                            ]
                                                            (Ty.apply
                                                              (Ty.path "core::option::Option")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "petgraph::graph_impl::EdgeIndex")
                                                                  []
                                                                  [ Ty.path "u32" ]
                                                              ])
                                                        ])
                                                  ]
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "slice")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path
                                                              "petgraph::graph_impl::NodeIndex")
                                                            []
                                                            [ Ty.path "u32" ]
                                                        ],
                                                      "iter",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::deref::Deref",
                                                          Ty.apply
                                                            (Ty.path "alloc::vec::Vec")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "petgraph::graph_impl::NodeIndex")
                                                                []
                                                                [ Ty.path "u32" ];
                                                              Ty.path "alloc::alloc::Global"
                                                            ],
                                                          [],
                                                          "deref",
                                                          []
                                                        |),
                                                        [ nodes ]
                                                      |)
                                                    ]
                                                  |);
                                                  M.closure
                                                    (fun γ =>
                                                      ltac:(M.monadic
                                                        match γ with
                                                        | [ α0 ] =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              M.alloc (| α0 |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let node_idx :=
                                                                      M.copy (| γ |) in
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::iter::traits::iterator::Iterator",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "petgraph::graph_impl::Edges")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "move_bytecode_verifier::instantiation_loops::Edge";
                                                                            Ty.path
                                                                              "petgraph::Directed";
                                                                            Ty.path "u32"
                                                                          ],
                                                                        [],
                                                                        "filter_map",
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "petgraph::graph_impl::EdgeIndex")
                                                                            []
                                                                            [ Ty.path "u32" ];
                                                                          Ty.function
                                                                            [
                                                                              Ty.tuple
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "petgraph::graph_impl::EdgeReference")
                                                                                    []
                                                                                    [
                                                                                      Ty.path
                                                                                        "move_bytecode_verifier::instantiation_loops::Edge";
                                                                                      Ty.path "u32"
                                                                                    ]
                                                                                ]
                                                                            ]
                                                                            (Ty.apply
                                                                              (Ty.path
                                                                                "core::option::Option")
                                                                              []
                                                                              [
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "petgraph::graph_impl::EdgeIndex")
                                                                                  []
                                                                                  [ Ty.path "u32" ]
                                                                              ])
                                                                        ]
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "petgraph::graph_impl::Graph")
                                                                              []
                                                                              [
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::instantiation_loops::Node";
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::instantiation_loops::Edge";
                                                                                Ty.path
                                                                                  "petgraph::Directed";
                                                                                Ty.path "u32"
                                                                              ],
                                                                            "edges",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| self |),
                                                                              "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                              "graph"
                                                                            |);
                                                                            M.read (|
                                                                              M.read (| node_idx |)
                                                                            |)
                                                                          ]
                                                                        |);
                                                                        M.closure
                                                                          (fun γ =>
                                                                            ltac:(M.monadic
                                                                              match γ with
                                                                              | [ α0 ] =>
                                                                                ltac:(M.monadic
                                                                                  (M.match_operator (|
                                                                                    M.alloc (|
                                                                                      α0
                                                                                    |),
                                                                                    [
                                                                                      fun γ =>
                                                                                        ltac:(M.monadic
                                                                                          (let
                                                                                                edge :=
                                                                                            M.copy (|
                                                                                              γ
                                                                                            |) in
                                                                                          M.read (|
                                                                                            M.match_operator (|
                                                                                              M.alloc (|
                                                                                                Value.Tuple
                                                                                                  []
                                                                                              |),
                                                                                              [
                                                                                                fun
                                                                                                    γ =>
                                                                                                  ltac:(M.monadic
                                                                                                    (let
                                                                                                          γ :=
                                                                                                      M.use
                                                                                                        (M.alloc (|
                                                                                                          M.call_closure (|
                                                                                                            M.get_associated_function (|
                                                                                                              Ty.apply
                                                                                                                (Ty.path
                                                                                                                  "std::collections::hash::set::HashSet")
                                                                                                                []
                                                                                                                [
                                                                                                                  Ty.apply
                                                                                                                    (Ty.path
                                                                                                                      "petgraph::graph_impl::NodeIndex")
                                                                                                                    []
                                                                                                                    [
                                                                                                                      Ty.path
                                                                                                                        "u32"
                                                                                                                    ];
                                                                                                                  Ty.path
                                                                                                                    "std::hash::random::RandomState"
                                                                                                                ],
                                                                                                              "contains",
                                                                                                              [
                                                                                                                Ty.apply
                                                                                                                  (Ty.path
                                                                                                                    "petgraph::graph_impl::NodeIndex")
                                                                                                                  []
                                                                                                                  [
                                                                                                                    Ty.path
                                                                                                                      "u32"
                                                                                                                  ]
                                                                                                              ]
                                                                                                            |),
                                                                                                            [
                                                                                                              node_set;
                                                                                                              M.alloc (|
                                                                                                                M.call_closure (|
                                                                                                                  M.get_trait_method (|
                                                                                                                    "petgraph::visit::EdgeRef",
                                                                                                                    Ty.apply
                                                                                                                      (Ty.path
                                                                                                                        "petgraph::graph_impl::EdgeReference")
                                                                                                                      []
                                                                                                                      [
                                                                                                                        Ty.path
                                                                                                                          "move_bytecode_verifier::instantiation_loops::Edge";
                                                                                                                        Ty.path
                                                                                                                          "u32"
                                                                                                                      ],
                                                                                                                    [],
                                                                                                                    "target",
                                                                                                                    []
                                                                                                                  |),
                                                                                                                  [
                                                                                                                    edge
                                                                                                                  ]
                                                                                                                |)
                                                                                                              |)
                                                                                                            ]
                                                                                                          |)
                                                                                                        |)) in
                                                                                                    let
                                                                                                          _ :=
                                                                                                      M.is_constant_or_break_match (|
                                                                                                        M.read (|
                                                                                                          γ
                                                                                                        |),
                                                                                                        Value.Bool
                                                                                                          true
                                                                                                      |) in
                                                                                                    M.alloc (|
                                                                                                      Value.StructTuple
                                                                                                        "core::option::Option::Some"
                                                                                                        [
                                                                                                          M.call_closure (|
                                                                                                            M.get_trait_method (|
                                                                                                              "petgraph::visit::EdgeRef",
                                                                                                              Ty.apply
                                                                                                                (Ty.path
                                                                                                                  "petgraph::graph_impl::EdgeReference")
                                                                                                                []
                                                                                                                [
                                                                                                                  Ty.path
                                                                                                                    "move_bytecode_verifier::instantiation_loops::Edge";
                                                                                                                  Ty.path
                                                                                                                    "u32"
                                                                                                                ],
                                                                                                              [],
                                                                                                              "id",
                                                                                                              []
                                                                                                            |),
                                                                                                            [
                                                                                                              edge
                                                                                                            ]
                                                                                                          |)
                                                                                                        ]
                                                                                                    |)));
                                                                                                fun
                                                                                                    γ =>
                                                                                                  ltac:(M.monadic
                                                                                                    (M.alloc (|
                                                                                                      Value.StructTuple
                                                                                                        "core::option::Option::None"
                                                                                                        []
                                                                                                    |)))
                                                                                              ]
                                                                                            |)
                                                                                          |)))
                                                                                    ]
                                                                                  |)))
                                                                              | _ =>
                                                                                M.impossible
                                                                                  "wrong number of arguments"
                                                                              end))
                                                                      ]
                                                                    |)))
                                                              ]
                                                            |)))
                                                        | _ =>
                                                          M.impossible "wrong number of arguments"
                                                        end))
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) 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::iter::traits::iterator::Iterator",
                                                        Ty.apply
                                                          (Ty.path "core::slice::iter::Iter")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "petgraph::graph_impl::EdgeIndex")
                                                              []
                                                              [ Ty.path "u32" ]
                                                          ],
                                                        [],
                                                        "any",
                                                        [
                                                          Ty.function
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "&")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "petgraph::graph_impl::EdgeIndex")
                                                                        []
                                                                        [ Ty.path "u32" ]
                                                                    ]
                                                                ]
                                                            ]
                                                            (Ty.path "bool")
                                                        ]
                                                      |),
                                                      [
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path "slice")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "petgraph::graph_impl::EdgeIndex")
                                                                    []
                                                                    [ Ty.path "u32" ]
                                                                ],
                                                              "iter",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::deref::Deref",
                                                                  Ty.apply
                                                                    (Ty.path "alloc::vec::Vec")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "petgraph::graph_impl::EdgeIndex")
                                                                        []
                                                                        [ Ty.path "u32" ];
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ],
                                                                  [],
                                                                  "deref",
                                                                  []
                                                                |),
                                                                [ edges ]
                                                              |)
                                                            ]
                                                          |)
                                                        |);
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [ α0 ] =>
                                                                ltac:(M.monadic
                                                                  (M.match_operator (|
                                                                    M.alloc (| α0 |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (let edge_idx :=
                                                                            M.copy (| γ |) in
                                                                          M.read (|
                                                                            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_bytecode_verifier::instantiation_loops::Edge"
                                                                                          ]
                                                                                      ],
                                                                                    "unwrap",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    M.call_closure (|
                                                                                      M.get_associated_function (|
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "petgraph::graph_impl::Graph")
                                                                                          []
                                                                                          [
                                                                                            Ty.path
                                                                                              "move_bytecode_verifier::instantiation_loops::Node";
                                                                                            Ty.path
                                                                                              "move_bytecode_verifier::instantiation_loops::Edge";
                                                                                            Ty.path
                                                                                              "petgraph::Directed";
                                                                                            Ty.path
                                                                                              "u32"
                                                                                          ],
                                                                                        "edge_weight",
                                                                                        []
                                                                                      |),
                                                                                      [
                                                                                        M.SubPointer.get_struct_record_field (|
                                                                                          M.read (|
                                                                                            self
                                                                                          |),
                                                                                          "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                                                                          "graph"
                                                                                        |);
                                                                                        M.read (|
                                                                                          M.read (|
                                                                                            edge_idx
                                                                                          |)
                                                                                        |)
                                                                                      ]
                                                                                    |)
                                                                                  ]
                                                                                |)
                                                                              |),
                                                                              [
                                                                                fun γ =>
                                                                                  ltac:(M.monadic
                                                                                    (let γ :=
                                                                                      M.read (|
                                                                                        γ
                                                                                      |) in
                                                                                    let _ :=
                                                                                      M.is_struct_tuple (|
                                                                                        γ,
                                                                                        "move_bytecode_verifier::instantiation_loops::Edge::Identity"
                                                                                      |) in
                                                                                    M.alloc (|
                                                                                      Value.Bool
                                                                                        false
                                                                                    |)));
                                                                                fun γ =>
                                                                                  ltac:(M.monadic
                                                                                    (let γ :=
                                                                                      M.read (|
                                                                                        γ
                                                                                      |) in
                                                                                    let γ1_0 :=
                                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                                        γ,
                                                                                        "move_bytecode_verifier::instantiation_loops::Edge::TyConApp",
                                                                                        0
                                                                                      |) in
                                                                                    M.alloc (|
                                                                                      Value.Bool
                                                                                        true
                                                                                    |)))
                                                                              ]
                                                                            |)
                                                                          |)))
                                                                    ]
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      ]
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              M.alloc (|
                                                Value.StructTuple
                                                  "core::option::Option::Some"
                                                  [
                                                    Value.Tuple
                                                      [ M.read (| nodes |); M.read (| edges |) ]
                                                  ]
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.alloc (|
                                                Value.StructTuple "core::option::Option::None" []
                                              |)))
                                        ]
                                      |)
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_find_non_trivial_components :
      M.IsAssociatedFunction Self "find_non_trivial_components" find_non_trivial_components.
    
    (*
        fn format_node(&self, node_idx: NodeIndex) -> String {
            let Node(def_idx, param_idx) = self.graph.node_weight(node_idx).unwrap();
            format!("f{}#{}", def_idx, param_idx)
        }
    *)
    Definition format_node (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; node_idx ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let node_idx := M.alloc (| node_idx |) in
          M.read (|
            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_bytecode_verifier::instantiation_loops::Node" ]
                      ],
                    "unwrap",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "petgraph::graph_impl::Graph")
                          []
                          [
                            Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                            Ty.path "move_bytecode_verifier::instantiation_loops::Edge";
                            Ty.path "petgraph::Directed";
                            Ty.path "u32"
                          ],
                        "node_weight",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                          "graph"
                        |);
                        M.read (| node_idx |)
                      ]
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_bytecode_verifier::instantiation_loops::Node",
                        0
                      |) in
                    let γ1_1 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "move_bytecode_verifier::instantiation_loops::Node",
                        1
                      |) in
                    let def_idx := M.alloc (| γ1_0 |) in
                    let param_idx := M.alloc (| γ1_1 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::hint::must_use",
                          [ Ty.path "alloc::string::String" ]
                        |),
                        [
                          M.read (|
                            let~ res :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_function (| "alloc::fmt::format", [] |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "core::fmt::Arguments",
                                        "new_v1",
                                        []
                                      |),
                                      [
                                        M.alloc (|
                                          Value.Array
                                            [
                                              M.read (| Value.String "f" |);
                                              M.read (| Value.String "#" |)
                                            ]
                                        |);
                                        M.alloc (|
                                          Value.Array
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::rt::Argument",
                                                  "new_display",
                                                  [
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      []
                                                      [
                                                        Ty.path
                                                          "move_binary_format::file_format::FunctionDefinitionIndex"
                                                      ]
                                                  ]
                                                |),
                                                [ def_idx ]
                                              |);
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::rt::Argument",
                                                  "new_display",
                                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ]
                                                |),
                                                [ param_idx ]
                                              |)
                                            ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |) in
                            res
                          |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_format_node : M.IsAssociatedFunction Self "format_node" format_node.
    
    (*
        fn format_edge(&self, edge_idx: EdgeIndex) -> String {
            let (node_idx_1, node_idx_2) = self.graph.edge_endpoints(edge_idx).unwrap();
            let node_1 = self.format_node(node_idx_1);
            let node_2 = self.format_node(node_idx_2);
    
            match self.graph.edge_weight(edge_idx).unwrap() {
                Edge::TyConApp(ty) => format!("{} --{:?}--> {}", node_1, ty, node_2,),
                Edge::Identity => format!("{} ----> {}", node_1, node_2),
            }
        }
    *)
    Definition format_edge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; edge_idx ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let edge_idx := M.alloc (| edge_idx |) in
          M.read (|
            M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "petgraph::graph_impl::NodeIndex")
                              []
                              [ Ty.path "u32" ];
                            Ty.apply
                              (Ty.path "petgraph::graph_impl::NodeIndex")
                              []
                              [ Ty.path "u32" ]
                          ]
                      ],
                    "unwrap",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "petgraph::graph_impl::Graph")
                          []
                          [
                            Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                            Ty.path "move_bytecode_verifier::instantiation_loops::Edge";
                            Ty.path "petgraph::Directed";
                            Ty.path "u32"
                          ],
                        "edge_endpoints",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                          "graph"
                        |);
                        M.read (| edge_idx |)
                      ]
                    |)
                  ]
                |)
              |),
              [
                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 node_idx_1 := M.copy (| γ0_0 |) in
                    let node_idx_2 := M.copy (| γ0_1 |) in
                    let~ node_1 :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path
                              "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                            "format_node",
                            []
                          |),
                          [ M.read (| self |); M.read (| node_idx_1 |) ]
                        |)
                      |) in
                    let~ node_2 :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path
                              "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                            "format_node",
                            []
                          |),
                          [ M.read (| self |); M.read (| node_idx_2 |) ]
                        |)
                      |) 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_bytecode_verifier::instantiation_loops::Edge" ]
                              ],
                            "unwrap",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "petgraph::graph_impl::Graph")
                                  []
                                  [
                                    Ty.path "move_bytecode_verifier::instantiation_loops::Node";
                                    Ty.path "move_bytecode_verifier::instantiation_loops::Edge";
                                    Ty.path "petgraph::Directed";
                                    Ty.path "u32"
                                  ],
                                "edge_weight",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "move_bytecode_verifier::instantiation_loops::InstantiationLoopChecker",
                                  "graph"
                                |);
                                M.read (| edge_idx |)
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let γ1_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "move_bytecode_verifier::instantiation_loops::Edge::TyConApp",
                                0
                              |) in
                            let ty := M.alloc (| γ1_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::hint::must_use",
                                  [ Ty.path "alloc::string::String" ]
                                |),
                                [
                                  M.read (|
                                    let~ res :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_function (| "alloc::fmt::format", [] |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_v1",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (| Value.String "" |);
                                                      M.read (| Value.String " --" |);
                                                      M.read (| Value.String "--> " |)
                                                    ]
                                                |);
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_display",
                                                          [ Ty.path "alloc::string::String" ]
                                                        |),
                                                        [ node_1 ]
                                                      |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_debug",
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "move_binary_format::file_format::SignatureToken"
                                                                  ]
                                                              ]
                                                          ]
                                                        |),
                                                        [ ty ]
                                                      |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_display",
                                                          [ Ty.path "alloc::string::String" ]
                                                        |),
                                                        [ node_2 ]
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |) in
                                    res
                                  |)
                                ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "move_bytecode_verifier::instantiation_loops::Edge::Identity"
                              |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_function (|
                                  "core::hint::must_use",
                                  [ Ty.path "alloc::string::String" ]
                                |),
                                [
                                  M.read (|
                                    let~ res :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_function (| "alloc::fmt::format", [] |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_v1",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (| Value.String "" |);
                                                      M.read (| Value.String " ----> " |)
                                                    ]
                                                |);
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_display",
                                                          [ Ty.path "alloc::string::String" ]
                                                        |),
                                                        [ node_1 ]
                                                      |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_display",
                                                          [ Ty.path "alloc::string::String" ]
                                                        |),
                                                        [ node_2 ]
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |) in
                                    res
                                  |)
                                ]
                              |)
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_format_edge : M.IsAssociatedFunction Self "format_edge" format_edge.
  End Impl_move_bytecode_verifier_instantiation_loops_InstantiationLoopChecker.
End instantiation_loops.
