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

Module loop_summary.
  (* StructTuple
    {
      name := "NodeId";
      const_params := [];
      ty_params := [];
      fields := [ Ty.path "u16" ];
    } *)
  
  Module Impl_core_marker_Copy_for_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_move_bytecode_verifier_loop_summary_NodeId.
  
  Module Impl_core_clone_Clone_for_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    (* 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.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_loop_summary_NodeId.
  
  Module Impl_core_fmt_Debug_for_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_tuple_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "NodeId" |);
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::loop_summary::NodeId",
                  0
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_move_bytecode_verifier_loop_summary_NodeId.
  
  Module Impl_core_marker_StructuralPartialEq_for_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_move_bytecode_verifier_loop_summary_NodeId.
  
  Module Impl_core_cmp_PartialEq_for_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    (* 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
          BinOp.eq (|
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_bytecode_verifier::loop_summary::NodeId",
                0
              |)
            |),
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_bytecode_verifier::loop_summary::NodeId",
                0
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_move_bytecode_verifier_loop_summary_NodeId.
  
  Module Impl_core_cmp_Eq_for_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_move_bytecode_verifier_loop_summary_NodeId.
  
  Module Impl_core_cmp_PartialOrd_for_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    (* PartialOrd *)
    Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.path "u16",
              [ Ty.path "u16" ],
              "partial_cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_bytecode_verifier::loop_summary::NodeId",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_bytecode_verifier::loop_summary::NodeId",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
  End Impl_core_cmp_PartialOrd_for_move_bytecode_verifier_loop_summary_NodeId.
  
  Module Impl_core_cmp_Ord_for_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    (* Ord *)
    Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (| "core::cmp::Ord", Ty.path "u16", [], "cmp", [] |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "move_bytecode_verifier::loop_summary::NodeId",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "move_bytecode_verifier::loop_summary::NodeId",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Ord"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
  End Impl_core_cmp_Ord_for_move_bytecode_verifier_loop_summary_NodeId.
  
  Axiom NodeMap :
    forall (T : Ty.t),
    (Ty.apply (Ty.path "move_bytecode_verifier::loop_summary::NodeMap") [] [ T ]) =
      (Ty.apply (Ty.path "alloc::vec::Vec") [] [ T; Ty.path "alloc::alloc::Global" ]).
  
  (* StructRecord
    {
      name := "LoopSummary";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("blocks",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]);
          ("descs",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]);
          ("backs",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                    Ty.path "alloc::alloc::Global"
                  ];
                Ty.path "alloc::alloc::Global"
              ]);
          ("preds",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                    Ty.path "alloc::alloc::Global"
                  ];
                Ty.path "alloc::alloc::Global"
              ])
        ];
    } *)
  
  (* StructRecord
    {
      name := "LoopPartition";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("parents",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                Ty.path "alloc::alloc::Global"
              ]);
          ("depths",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_loop_summary_LoopSummary.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::LoopSummary".
    
    (*
        pub fn new(cfg: &VMControlFlowGraph) -> Self {
            use Exploration::*;
            use Frontier::*;
    
            enum Exploration {
                InProgress(NodeId),
                Done(NodeId),
            }
    
            enum Frontier {
                Visit {
                    from_node: NodeId,
                    to_block: BlockId,
                },
                Finish {
                    block: BlockId,
                    node_id: NodeId,
                    parent: NodeId,
                },
            }
    
            let num_blocks = cfg.num_blocks() as usize;
    
            // Fields in LoopSummary that are filled via a depth-first traversal of `cfg`.
            let mut blocks = vec![0; num_blocks];
            let mut descs = vec![0; num_blocks];
            let mut backs = vec![vec![]; num_blocks];
            let mut preds = vec![vec![]; num_blocks];
    
            let mut next_node = NodeId(0);
    
            let root_block = cfg.entry_block_id();
            let root_node = next_node.bump();
    
            let mut exploration = BTreeMap::new();
            blocks[usize::from(root_node)] = root_block;
            exploration.insert(root_block, InProgress(root_node));
    
            let mut stack: Vec<Frontier> = cfg
                .successors(root_block)
                .iter()
                .map(|succ| Visit {
                    from_node: root_node,
                    to_block: *succ,
                })
                .collect();
    
            while let Some(action) = stack.pop() {
                match action {
                    Finish {
                        block,
                        node_id,
                        parent,
                    } => {
                        descs[usize::from(parent)] += 1 + descs[usize::from(node_id)];
                        *exploration.get_mut(&block).unwrap() = Done(node_id);
                    }
    
                    Visit {
                        from_node,
                        to_block,
                    } => match exploration.entry(to_block) {
                        Entry::Occupied(entry) => match entry.get() {
                            // Cyclic back edge detected by re-visiting `to` while still processing its
                            // children.
                            InProgress(to_node) => backs[usize::from( *to_node)].push(from_node),
    
                            // Cross edge detected by re-visiting `to` after it and its children have
                            // been processed.
                            Done(to_node) => preds[usize::from( *to_node)].push(from_node),
                        },
    
                        // Visiting `to` for the first time: `from` must be its parent in the depth-
                        // -first spanning tree, and we should continue exploring its successors.
                        Entry::Vacant(entry) => {
                            let to_node = next_node.bump();
                            entry.insert(InProgress(to_node));
                            blocks[usize::from(to_node)] = to_block;
                            preds[usize::from(to_node)].push(from_node);
    
                            stack.push(Finish {
                                block: to_block,
                                node_id: to_node,
                                parent: from_node,
                            });
    
                            stack.extend(cfg.successors(to_block).iter().map(|succ| Visit {
                                from_node: to_node,
                                to_block: *succ,
                            }));
                        }
                    },
                }
            }
    
            LoopSummary {
                blocks,
                descs,
                backs,
                preds,
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ cfg ] =>
        ltac:(M.monadic
          (let cfg := M.alloc (| cfg |) in
          M.read (|
            let~ num_blocks :=
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_trait_method (|
                      "move_binary_format::control_flow_graph::ControlFlowGraph",
                      Ty.path "move_binary_format::control_flow_graph::VMControlFlowGraph",
                      [],
                      "num_blocks",
                      []
                    |),
                    [ M.read (| cfg |) ]
                  |))
              |) in
            let~ blocks :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "alloc::vec::from_elem", [ Ty.path "u16" ] |),
                  [ Value.Integer IntegerKind.U16 0; M.read (| num_blocks |) ]
                |)
              |) in
            let~ descs :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "alloc::vec::from_elem", [ Ty.path "u16" ] |),
                  [ Value.Integer IntegerKind.U16 0; M.read (| num_blocks |) ]
                |)
              |) in
            let~ backs :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "alloc::vec::from_elem",
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                          Ty.path "alloc::alloc::Global"
                        ]
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      []
                    |);
                    M.read (| num_blocks |)
                  ]
                |)
              |) in
            let~ preds :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "alloc::vec::from_elem",
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                          Ty.path "alloc::alloc::Global"
                        ]
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      []
                    |);
                    M.read (| num_blocks |)
                  ]
                |)
              |) in
            let~ next_node :=
              M.alloc (|
                Value.StructTuple
                  "move_bytecode_verifier::loop_summary::NodeId"
                  [ Value.Integer IntegerKind.U16 0 ]
              |) in
            let~ root_block :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "move_binary_format::control_flow_graph::ControlFlowGraph",
                    Ty.path "move_binary_format::control_flow_graph::VMControlFlowGraph",
                    [],
                    "entry_block_id",
                    []
                  |),
                  [ M.read (| cfg |) ]
                |)
              |) in
            let~ root_node :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::loop_summary::NodeId",
                    "bump",
                    []
                  |),
                  [ next_node ]
                |)
              |) in
            let~ exploration :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [
                        Ty.path "u16";
                        Ty.path "move_bytecode_verifier::loop_summary::new::Exploration";
                        Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ _ :=
              M.write (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::index::IndexMut",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                    [ Ty.path "usize" ],
                    "index_mut",
                    []
                  |),
                  [
                    blocks;
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::convert::From",
                        Ty.path "usize",
                        [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                        "from",
                        []
                      |),
                      [ M.read (| root_node |) ]
                    |)
                  ]
                |),
                M.read (| root_block |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [
                        Ty.path "u16";
                        Ty.path "move_bytecode_verifier::loop_summary::new::Exploration";
                        Ty.path "alloc::alloc::Global"
                      ],
                    "insert",
                    []
                  |),
                  [
                    exploration;
                    M.read (| root_block |);
                    Value.StructTuple
                      "move_bytecode_verifier::loop_summary::new::Exploration::InProgress"
                      [ M.read (| root_node |) ]
                  ]
                |)
              |) in
            let~ stack :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::iterator::Iterator",
                    Ty.apply
                      (Ty.path "core::iter::adapters::map::Map")
                      []
                      [
                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u16" ];
                        Ty.function
                          [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ] ]
                          (Ty.path "move_bytecode_verifier::loop_summary::new::Frontier")
                      ],
                    [],
                    "collect",
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.path "move_bytecode_verifier::loop_summary::new::Frontier";
                          Ty.path "alloc::alloc::Global"
                        ]
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u16" ],
                        [],
                        "map",
                        [
                          Ty.path "move_bytecode_verifier::loop_summary::new::Frontier";
                          Ty.function
                            [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ] ]
                            (Ty.path "move_bytecode_verifier::loop_summary::new::Frontier")
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "u16" ],
                            "iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::deref::Deref",
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                [],
                                "deref",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "move_binary_format::control_flow_graph::ControlFlowGraph",
                                    Ty.path
                                      "move_binary_format::control_flow_graph::VMControlFlowGraph",
                                    [],
                                    "successors",
                                    []
                                  |),
                                  [ M.read (| cfg |); M.read (| root_block |) ]
                                |)
                              ]
                            |)
                          ]
                        |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let succ := M.copy (| γ |) in
                                          Value.StructRecord
                                            "move_bytecode_verifier::loop_summary::new::Frontier::Visit"
                                            [
                                              ("from_node", M.read (| root_node |));
                                              ("to_block", M.read (| M.read (| succ |) |))
                                            ]))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  ]
                |)
              |) in
            let~ _ :=
              M.loop (|
                ltac:(M.monadic
                  (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 "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.path "move_bytecode_verifier::loop_summary::new::Frontier";
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "pop",
                                  []
                                |),
                                [ stack ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let action := M.copy (| γ0_0 |) in
                          M.match_operator (|
                            action,
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_record_field (|
                                      γ,
                                      "move_bytecode_verifier::loop_summary::new::Frontier::Finish",
                                      "block"
                                    |) in
                                  let γ0_1 :=
                                    M.SubPointer.get_struct_record_field (|
                                      γ,
                                      "move_bytecode_verifier::loop_summary::new::Frontier::Finish",
                                      "node_id"
                                    |) in
                                  let γ0_2 :=
                                    M.SubPointer.get_struct_record_field (|
                                      γ,
                                      "move_bytecode_verifier::loop_summary::new::Frontier::Finish",
                                      "parent"
                                    |) in
                                  let block := M.copy (| γ0_0 |) in
                                  let node_id := M.copy (| γ0_1 |) in
                                  let parent := M.copy (| γ0_2 |) in
                                  let~ _ :=
                                    let β :=
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::index::IndexMut",
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                          [ Ty.path "usize" ],
                                          "index_mut",
                                          []
                                        |),
                                        [
                                          descs;
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::convert::From",
                                              Ty.path "usize",
                                              [
                                                Ty.path
                                                  "move_bytecode_verifier::loop_summary::NodeId"
                                              ],
                                              "from",
                                              []
                                            |),
                                            [ M.read (| parent |) ]
                                          |)
                                        ]
                                      |) in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.add (|
                                        M.read (| β |),
                                        BinOp.Wrap.add (|
                                          Value.Integer IntegerKind.U16 1,
                                          M.read (|
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::index::Index",
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                                [ Ty.path "usize" ],
                                                "index",
                                                []
                                              |),
                                              [
                                                descs;
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::convert::From",
                                                    Ty.path "usize",
                                                    [
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::NodeId"
                                                    ],
                                                    "from",
                                                    []
                                                  |),
                                                  [ M.read (| node_id |) ]
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "&mut")
                                                []
                                                [
                                                  Ty.path
                                                    "move_bytecode_verifier::loop_summary::new::Exploration"
                                                ]
                                            ],
                                          "unwrap",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::collections::btree::map::BTreeMap")
                                                []
                                                [
                                                  Ty.path "u16";
                                                  Ty.path
                                                    "move_bytecode_verifier::loop_summary::new::Exploration";
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "get_mut",
                                              [ Ty.path "u16" ]
                                            |),
                                            [ exploration; block ]
                                          |)
                                        ]
                                      |),
                                      Value.StructTuple
                                        "move_bytecode_verifier::loop_summary::new::Exploration::Done"
                                        [ M.read (| node_id |) ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_record_field (|
                                      γ,
                                      "move_bytecode_verifier::loop_summary::new::Frontier::Visit",
                                      "from_node"
                                    |) in
                                  let γ0_1 :=
                                    M.SubPointer.get_struct_record_field (|
                                      γ,
                                      "move_bytecode_verifier::loop_summary::new::Frontier::Visit",
                                      "to_block"
                                    |) in
                                  let from_node := M.copy (| γ0_0 |) in
                                  let to_block := M.copy (| γ0_1 |) in
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::collections::btree::map::BTreeMap")
                                            []
                                            [
                                              Ty.path "u16";
                                              Ty.path
                                                "move_bytecode_verifier::loop_summary::new::Exploration";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "entry",
                                          []
                                        |),
                                        [ exploration; M.read (| to_block |) ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "alloc::collections::btree::map::entry::Entry::Occupied",
                                              0
                                            |) in
                                          let entry := M.copy (| γ0_0 |) in
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::map::entry::OccupiedEntry")
                                                    []
                                                    [
                                                      Ty.path "u16";
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::new::Exploration";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "get",
                                                  []
                                                |),
                                                [ entry ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_bytecode_verifier::loop_summary::new::Exploration::InProgress",
                                                      0
                                                    |) in
                                                  let to_node := M.alloc (| γ1_0 |) in
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "alloc::vec::Vec")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_bytecode_verifier::loop_summary::NodeId";
                                                            Ty.path "alloc::alloc::Global"
                                                          ],
                                                        "push",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::index::IndexMut",
                                                            Ty.apply
                                                              (Ty.path "alloc::vec::Vec")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "alloc::vec::Vec")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "move_bytecode_verifier::loop_summary::NodeId";
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ];
                                                                Ty.path "alloc::alloc::Global"
                                                              ],
                                                            [ Ty.path "usize" ],
                                                            "index_mut",
                                                            []
                                                          |),
                                                          [
                                                            backs;
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::convert::From",
                                                                Ty.path "usize",
                                                                [
                                                                  Ty.path
                                                                    "move_bytecode_verifier::loop_summary::NodeId"
                                                                ],
                                                                "from",
                                                                []
                                                              |),
                                                              [ M.read (| M.read (| to_node |) |) ]
                                                            |)
                                                          ]
                                                        |);
                                                        M.read (| from_node |)
                                                      ]
                                                    |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ := M.read (| γ |) in
                                                  let γ1_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "move_bytecode_verifier::loop_summary::new::Exploration::Done",
                                                      0
                                                    |) in
                                                  let to_node := M.alloc (| γ1_0 |) in
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "alloc::vec::Vec")
                                                          []
                                                          [
                                                            Ty.path
                                                              "move_bytecode_verifier::loop_summary::NodeId";
                                                            Ty.path "alloc::alloc::Global"
                                                          ],
                                                        "push",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::index::IndexMut",
                                                            Ty.apply
                                                              (Ty.path "alloc::vec::Vec")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "alloc::vec::Vec")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "move_bytecode_verifier::loop_summary::NodeId";
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ];
                                                                Ty.path "alloc::alloc::Global"
                                                              ],
                                                            [ Ty.path "usize" ],
                                                            "index_mut",
                                                            []
                                                          |),
                                                          [
                                                            preds;
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::convert::From",
                                                                Ty.path "usize",
                                                                [
                                                                  Ty.path
                                                                    "move_bytecode_verifier::loop_summary::NodeId"
                                                                ],
                                                                "from",
                                                                []
                                                              |),
                                                              [ M.read (| M.read (| to_node |) |) ]
                                                            |)
                                                          ]
                                                        |);
                                                        M.read (| from_node |)
                                                      ]
                                                    |)
                                                  |)))
                                            ]
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "alloc::collections::btree::map::entry::Entry::Vacant",
                                              0
                                            |) in
                                          let entry := M.copy (| γ0_0 |) in
                                          let~ to_node :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_bytecode_verifier::loop_summary::NodeId",
                                                  "bump",
                                                  []
                                                |),
                                                [ next_node ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::map::entry::VacantEntry")
                                                    []
                                                    [
                                                      Ty.path "u16";
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::new::Exploration";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "insert",
                                                  []
                                                |),
                                                [
                                                  M.read (| entry |);
                                                  Value.StructTuple
                                                    "move_bytecode_verifier::loop_summary::new::Exploration::InProgress"
                                                    [ M.read (| to_node |) ]
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.write (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::index::IndexMut",
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [ Ty.path "u16"; Ty.path "alloc::alloc::Global"
                                                    ],
                                                  [ Ty.path "usize" ],
                                                  "index_mut",
                                                  []
                                                |),
                                                [
                                                  blocks;
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::convert::From",
                                                      Ty.path "usize",
                                                      [
                                                        Ty.path
                                                          "move_bytecode_verifier::loop_summary::NodeId"
                                                      ],
                                                      "from",
                                                      []
                                                    |),
                                                    [ M.read (| to_node |) ]
                                                  |)
                                                ]
                                              |),
                                              M.read (| to_block |)
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::NodeId";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "push",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::index::IndexMut",
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "alloc::vec::Vec")
                                                            []
                                                            [
                                                              Ty.path
                                                                "move_bytecode_verifier::loop_summary::NodeId";
                                                              Ty.path "alloc::alloc::Global"
                                                            ];
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      [ Ty.path "usize" ],
                                                      "index_mut",
                                                      []
                                                    |),
                                                    [
                                                      preds;
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::convert::From",
                                                          Ty.path "usize",
                                                          [
                                                            Ty.path
                                                              "move_bytecode_verifier::loop_summary::NodeId"
                                                          ],
                                                          "from",
                                                          []
                                                        |),
                                                        [ M.read (| to_node |) ]
                                                      |)
                                                    ]
                                                  |);
                                                  M.read (| from_node |)
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::new::Frontier";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "push",
                                                  []
                                                |),
                                                [
                                                  stack;
                                                  Value.StructRecord
                                                    "move_bytecode_verifier::loop_summary::new::Frontier::Finish"
                                                    [
                                                      ("block", M.read (| to_block |));
                                                      ("node_id", M.read (| to_node |));
                                                      ("parent", M.read (| from_node |))
                                                    ]
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::collect::Extend",
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::new::Frontier";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  [
                                                    Ty.path
                                                      "move_bytecode_verifier::loop_summary::new::Frontier"
                                                  ],
                                                  "extend",
                                                  [
                                                    Ty.apply
                                                      (Ty.path "core::iter::adapters::map::Map")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "core::slice::iter::Iter")
                                                          []
                                                          [ Ty.path "u16" ];
                                                        Ty.function
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&")
                                                                  []
                                                                  [ Ty.path "u16" ]
                                                              ]
                                                          ]
                                                          (Ty.path
                                                            "move_bytecode_verifier::loop_summary::new::Frontier")
                                                      ]
                                                  ]
                                                |),
                                                [
                                                  stack;
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::iter::traits::iterator::Iterator",
                                                      Ty.apply
                                                        (Ty.path "core::slice::iter::Iter")
                                                        []
                                                        [ Ty.path "u16" ],
                                                      [],
                                                      "map",
                                                      [
                                                        Ty.path
                                                          "move_bytecode_verifier::loop_summary::new::Frontier";
                                                        Ty.function
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&")
                                                                  []
                                                                  [ Ty.path "u16" ]
                                                              ]
                                                          ]
                                                          (Ty.path
                                                            "move_bytecode_verifier::loop_summary::new::Frontier")
                                                      ]
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "slice")
                                                            []
                                                            [ Ty.path "u16" ],
                                                          "iter",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::ops::deref::Deref",
                                                              Ty.apply
                                                                (Ty.path "alloc::vec::Vec")
                                                                []
                                                                [
                                                                  Ty.path "u16";
                                                                  Ty.path "alloc::alloc::Global"
                                                                ],
                                                              [],
                                                              "deref",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "move_binary_format::control_flow_graph::ControlFlowGraph",
                                                                  Ty.path
                                                                    "move_binary_format::control_flow_graph::VMControlFlowGraph",
                                                                  [],
                                                                  "successors",
                                                                  []
                                                                |),
                                                                [
                                                                  M.read (| cfg |);
                                                                  M.read (| to_block |)
                                                                ]
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |);
                                                      M.closure
                                                        (fun γ =>
                                                          ltac:(M.monadic
                                                            match γ with
                                                            | [ α0 ] =>
                                                              ltac:(M.monadic
                                                                (M.match_operator (|
                                                                  M.alloc (| α0 |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let succ :=
                                                                          M.copy (| γ |) in
                                                                        Value.StructRecord
                                                                          "move_bytecode_verifier::loop_summary::new::Frontier::Visit"
                                                                          [
                                                                            ("from_node",
                                                                              M.read (| to_node |));
                                                                            ("to_block",
                                                                              M.read (|
                                                                                M.read (| succ |)
                                                                              |))
                                                                          ]))
                                                                  ]
                                                                |)))
                                                            | _ =>
                                                              M.impossible
                                                                "wrong number of arguments"
                                                            end))
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                let~ _ :=
                                  M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                                M.alloc (| Value.Tuple [] |)
                              |)
                            |)
                          |)))
                    ]
                  |)))
              |) in
            M.alloc (|
              Value.StructRecord
                "move_bytecode_verifier::loop_summary::LoopSummary"
                [
                  ("blocks", M.read (| blocks |));
                  ("descs", M.read (| descs |));
                  ("backs", M.read (| backs |));
                  ("preds", M.read (| preds |))
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn is_descendant(&self, NodeId(ancestor): NodeId, NodeId(descendant): NodeId) -> bool {
            // All the descendants of `ancestor` in the DFST will have the IDs immediately following it,
            // so we can check for descendants with a bounds check on `NodeId`, given `ancestor`'s
            // transitive descendant count in `self.descs[ancestor]`.
            ancestor <= descendant && descendant <= ancestor + self.descs[ancestor as usize]
        }
    *)
    Definition is_descendant (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; β1; β2 ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let β1 := M.alloc (| β1 |) in
          let β2 := M.alloc (| β2 |) in
          M.match_operator (|
            β1,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (|
                      γ,
                      "move_bytecode_verifier::loop_summary::NodeId",
                      0
                    |) in
                  let ancestor := M.copy (| γ0_0 |) in
                  M.match_operator (|
                    β2,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "move_bytecode_verifier::loop_summary::NodeId",
                              0
                            |) in
                          let descendant := M.copy (| γ0_0 |) in
                          LogicalOp.and (|
                            BinOp.le (| M.read (| ancestor |), M.read (| descendant |) |),
                            ltac:(M.monadic
                              (BinOp.le (|
                                M.read (| descendant |),
                                BinOp.Wrap.add (|
                                  M.read (| ancestor |),
                                  M.read (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::index::Index",
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                        [ Ty.path "usize" ],
                                        "index",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "move_bytecode_verifier::loop_summary::LoopSummary",
                                          "descs"
                                        |);
                                        M.rust_cast (M.read (| ancestor |))
                                      ]
                                    |)
                                  |)
                                |)
                              |)))
                          |)))
                    ]
                  |)))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_descendant :
      M.IsAssociatedFunction Self "is_descendant" is_descendant.
    
    (*
        pub fn preorder(&self) -> impl DoubleEndedIterator<Item = NodeId> {
            // `LoopSummary::new` assigns `NodeId`s to blocks in preorder, so just return the natural
            // order.
            (0..self.blocks.len()).map(|id| NodeId(id as u16))
        }
    *)
    Definition preorder (ε : 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::ops::range::Range") [] [ Ty.path "usize" ],
              [],
              "map",
              [
                Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                Ty.function
                  [ Ty.tuple [ Ty.path "usize" ] ]
                  (Ty.path "move_bytecode_verifier::loop_summary::NodeId")
              ]
            |),
            [
              Value.StructRecord
                "core::ops::range::Range"
                [
                  ("start", Value.Integer IntegerKind.Usize 0);
                  ("end_",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                        "len",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_bytecode_verifier::loop_summary::LoopSummary",
                          "blocks"
                        |)
                      ]
                    |))
                ];
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let id := M.copy (| γ |) in
                                Value.StructTuple
                                  "move_bytecode_verifier::loop_summary::NodeId"
                                  [ M.rust_cast (M.read (| id |)) ]))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_preorder : M.IsAssociatedFunction Self "preorder" preorder.
    
    (*
        pub fn block(&self, l: NodeId) -> BlockId {
            self.blocks[usize::from(l)]
        }
    *)
    Definition block (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; l ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let l := M.alloc (| l |) in
          M.read (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::index::Index",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                [ Ty.path "usize" ],
                "index",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::loop_summary::LoopSummary",
                  "blocks"
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.path "usize",
                    [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                    "from",
                    []
                  |),
                  [ M.read (| l |) ]
                |)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_block : M.IsAssociatedFunction Self "block" block.
    
    (*
        pub fn back_edges(&self, l: NodeId) -> &Vec<NodeId> {
            &self.backs[usize::from(l)]
        }
    *)
    Definition back_edges (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; l ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let l := M.alloc (| l |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::Index",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                      Ty.path "alloc::alloc::Global"
                    ];
                  Ty.path "alloc::alloc::Global"
                ],
              [ Ty.path "usize" ],
              "index",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_bytecode_verifier::loop_summary::LoopSummary",
                "backs"
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "usize",
                  [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                  "from",
                  []
                |),
                [ M.read (| l |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_back_edges : M.IsAssociatedFunction Self "back_edges" back_edges.
    
    (*
        pub fn pred_edges(&self, l: NodeId) -> &Vec<NodeId> {
            &self.preds[usize::from(l)]
        }
    *)
    Definition pred_edges (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; l ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let l := M.alloc (| l |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::Index",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                      Ty.path "alloc::alloc::Global"
                    ];
                  Ty.path "alloc::alloc::Global"
                ],
              [ Ty.path "usize" ],
              "index",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_bytecode_verifier::loop_summary::LoopSummary",
                "preds"
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "usize",
                  [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                  "from",
                  []
                |),
                [ M.read (| l |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_pred_edges : M.IsAssociatedFunction Self "pred_edges" pred_edges.
  End Impl_move_bytecode_verifier_loop_summary_LoopSummary.
  
  Module Impl_move_bytecode_verifier_loop_summary_LoopPartition.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::LoopPartition".
    
    (*
        pub fn new(summary: &LoopSummary) -> Self {
            let num_blocks = summary.blocks.len();
            LoopPartition {
                parents: (0..num_blocks).map(|id| NodeId(id as u16)).collect(),
                depths: vec![0; num_blocks],
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ summary ] =>
        ltac:(M.monadic
          (let summary := M.alloc (| summary |) in
          M.read (|
            let~ num_blocks :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                    "len",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| summary |),
                      "move_bytecode_verifier::loop_summary::LoopSummary",
                      "blocks"
                    |)
                  ]
                |)
              |) in
            M.alloc (|
              Value.StructRecord
                "move_bytecode_verifier::loop_summary::LoopPartition"
                [
                  ("parents",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::map::Map")
                          []
                          [
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ];
                            Ty.function
                              [ Ty.tuple [ Ty.path "usize" ] ]
                              (Ty.path "move_bytecode_verifier::loop_summary::NodeId")
                          ],
                        [],
                        "collect",
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                              Ty.path "alloc::alloc::Global"
                            ]
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ],
                            [],
                            "map",
                            [
                              Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                              Ty.function
                                [ Ty.tuple [ Ty.path "usize" ] ]
                                (Ty.path "move_bytecode_verifier::loop_summary::NodeId")
                            ]
                          |),
                          [
                            Value.StructRecord
                              "core::ops::range::Range"
                              [
                                ("start", Value.Integer IntegerKind.Usize 0);
                                ("end_", M.read (| num_blocks |))
                              ];
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let id := M.copy (| γ |) in
                                              Value.StructTuple
                                                "move_bytecode_verifier::loop_summary::NodeId"
                                                [ M.rust_cast (M.read (| id |)) ]))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |));
                  ("depths",
                    M.call_closure (|
                      M.get_function (| "alloc::vec::from_elem", [ Ty.path "u16" ] |),
                      [ Value.Integer IntegerKind.U16 0; M.read (| num_blocks |) ]
                    |))
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn containing_loop(&mut self, id: NodeId) -> NodeId {
            let mut child = id;
            let mut parent = self.parent(child);
            let mut grandparent = self.parent(parent);
    
            if child == parent || parent == grandparent {
                return parent;
            }
    
            let mut descendants = vec![];
            loop {
                // Invariant: child -> parent -> grandparent
                //       and  parent != grandparent
                //       and  forall d in descendants. parent(d) != parent(parent(d))
                descendants.push(child);
                (child, parent, grandparent) = (parent, grandparent, self.parent(grandparent));
                if parent == grandparent {
                    break;
                }
            }
    
            for descendant in descendants {
                *self.parent_mut(descendant) = parent;
            }
    
            parent
        }
    *)
    Definition containing_loop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let id := M.alloc (| id |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ child := M.copy (| id |) in
                let~ parent :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_bytecode_verifier::loop_summary::LoopPartition",
                        "parent",
                        []
                      |),
                      [ M.read (| self |); M.read (| child |) ]
                    |)
                  |) in
                let~ grandparent :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "move_bytecode_verifier::loop_summary::LoopPartition",
                        "parent",
                        []
                      |),
                      [ M.read (| self |); M.read (| parent |) ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.or (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.path "move_bytecode_verifier::loop_summary::NodeId",
                                      [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                                      "eq",
                                      []
                                    |),
                                    [ child; parent ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "move_bytecode_verifier::loop_summary::NodeId",
                                        [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                                        "eq",
                                        []
                                      |),
                                      [ parent; grandparent ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (| M.read (| M.return_ (| M.read (| parent |) |) |) |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ descendants :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      []
                    |)
                  |) in
                let~ _ :=
                  M.loop (|
                    ltac:(M.monadic
                      (let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "push",
                              []
                            |),
                            [ descendants; M.read (| child |) ]
                          |)
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (|
                            Value.Tuple
                              [
                                M.read (| parent |);
                                M.read (| grandparent |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "move_bytecode_verifier::loop_summary::LoopPartition",
                                    "parent",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| grandparent |) ]
                                |)
                              ]
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                let γ0_2 := M.SubPointer.get_tuple_field (| γ, 2 |) in
                                let lhs := M.copy (| γ0_0 |) in
                                let lhs := M.copy (| γ0_1 |) in
                                let lhs := M.copy (| γ0_2 |) in
                                let~ _ := M.write (| child, M.read (| lhs |) |) in
                                let~ _ := M.write (| parent, M.read (| lhs |) |) in
                                let~ _ := M.write (| grandparent, M.read (| lhs |) |) in
                                M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "move_bytecode_verifier::loop_summary::NodeId",
                                        [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                                        "eq",
                                        []
                                      |),
                                      [ parent; grandparent ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |)))
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                                Ty.path "alloc::alloc::Global"
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| descendants |) ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "alloc::vec::into_iter::IntoIter")
                                            []
                                            [
                                              Ty.path
                                                "move_bytecode_verifier::loop_summary::NodeId";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let descendant := M.copy (| γ0_0 |) in
                                          let~ _ :=
                                            M.write (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_bytecode_verifier::loop_summary::LoopPartition",
                                                  "parent_mut",
                                                  []
                                                |),
                                                [ M.read (| self |); M.read (| descendant |) ]
                                              |),
                                              M.read (| parent |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                parent
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_containing_loop :
      M.IsAssociatedFunction Self "containing_loop" containing_loop.
    
    (*
        pub fn collapse_loop(&mut self, head: NodeId, body: &BTreeSet<NodeId>) -> u16 {
            debug_assert_eq!(head, self.parent(head));
    
            let mut depth = self.depth(head);
            for constituent in body {
                debug_assert_eq!( *constituent, self.parent( *constituent));
                *self.parent_mut( *constituent) = head;
                depth = self.depth( *constituent).max(depth);
            }
    
            depth += 1;
            *self.depth_mut(head) = depth;
            depth
        }
    *)
    Definition collapse_loop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; head; body ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let head := M.alloc (| head |) in
          let body := M.alloc (| body |) in
          M.read (|
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.use (M.alloc (| Value.Bool true |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (|
                            Value.Tuple
                              [
                                head;
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "move_bytecode_verifier::loop_summary::LoopPartition",
                                      "parent",
                                      []
                                    |),
                                    [ M.read (| self |); M.read (| head |) ]
                                  |)
                                |)
                              ]
                          |),
                          [
                            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 left_val := M.copy (| γ0_0 |) in
                                let right_val := M.copy (| γ0_1 |) in
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              UnOp.not (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::cmp::PartialEq",
                                                    Ty.path
                                                      "move_bytecode_verifier::loop_summary::NodeId",
                                                    [
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::NodeId"
                                                    ],
                                                    "eq",
                                                    []
                                                  |),
                                                  [ M.read (| left_val |); M.read (| right_val |) ]
                                                |)
                                              |)
                                            |)) in
                                        let _ :=
                                          M.is_constant_or_break_match (|
                                            M.read (| γ |),
                                            Value.Bool true
                                          |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              let~ kind :=
                                                M.alloc (|
                                                  Value.StructTuple
                                                    "core::panicking::AssertKind::Eq"
                                                    []
                                                |) in
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::panicking::assert_failed",
                                                    [
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::NodeId";
                                                      Ty.path
                                                        "move_bytecode_verifier::loop_summary::NodeId"
                                                    ]
                                                  |),
                                                  [
                                                    M.read (| kind |);
                                                    M.read (| left_val |);
                                                    M.read (| right_val |);
                                                    Value.StructTuple
                                                      "core::option::Option::None"
                                                      []
                                                  ]
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ depth :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::loop_summary::LoopPartition",
                    "depth",
                    []
                  |),
                  [ M.read (| self |); M.read (| head |) ]
                |)
              |) in
            let~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::collections::btree::set::BTreeSet")
                              []
                              [
                                Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                                Ty.path "alloc::alloc::Global"
                              ]
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [ M.read (| body |) ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::set::Iter")
                                        []
                                        [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                                      [],
                                      "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 constituent := M.copy (| γ0_0 |) in
                                      let~ _ :=
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                let~ _ :=
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      Value.Tuple
                                                        [
                                                          M.read (| constituent |);
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.path
                                                                  "move_bytecode_verifier::loop_summary::LoopPartition",
                                                                "parent",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| self |);
                                                                M.read (|
                                                                  M.read (| constituent |)
                                                                |)
                                                              ]
                                                            |)
                                                          |)
                                                        ]
                                                    |),
                                                    [
                                                      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 left_val := M.copy (| γ0_0 |) in
                                                          let right_val := M.copy (| γ0_1 |) in
                                                          M.match_operator (|
                                                            M.alloc (| Value.Tuple [] |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ :=
                                                                    M.use
                                                                      (M.alloc (|
                                                                        UnOp.not (|
                                                                          M.call_closure (|
                                                                            M.get_trait_method (|
                                                                              "core::cmp::PartialEq",
                                                                              Ty.path
                                                                                "move_bytecode_verifier::loop_summary::NodeId",
                                                                              [
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::loop_summary::NodeId"
                                                                              ],
                                                                              "eq",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.read (| left_val |);
                                                                              M.read (| right_val |)
                                                                            ]
                                                                          |)
                                                                        |)
                                                                      |)) in
                                                                  let _ :=
                                                                    M.is_constant_or_break_match (|
                                                                      M.read (| γ |),
                                                                      Value.Bool true
                                                                    |) in
                                                                  M.alloc (|
                                                                    M.never_to_any (|
                                                                      M.read (|
                                                                        let~ kind :=
                                                                          M.alloc (|
                                                                            Value.StructTuple
                                                                              "core::panicking::AssertKind::Eq"
                                                                              []
                                                                          |) in
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_function (|
                                                                              "core::panicking::assert_failed",
                                                                              [
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::loop_summary::NodeId";
                                                                                Ty.path
                                                                                  "move_bytecode_verifier::loop_summary::NodeId"
                                                                              ]
                                                                            |),
                                                                            [
                                                                              M.read (| kind |);
                                                                              M.read (| left_val |);
                                                                              M.read (|
                                                                                right_val
                                                                              |);
                                                                              Value.StructTuple
                                                                                "core::option::Option::None"
                                                                                []
                                                                            ]
                                                                          |)
                                                                        |)
                                                                      |)
                                                                    |)
                                                                  |)));
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (M.alloc (| Value.Tuple [] |)))
                                                            ]
                                                          |)))
                                                    ]
                                                  |) in
                                                M.alloc (| Value.Tuple [] |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_bytecode_verifier::loop_summary::LoopPartition",
                                              "parent_mut",
                                              []
                                            |),
                                            [
                                              M.read (| self |);
                                              M.read (| M.read (| constituent |) |)
                                            ]
                                          |),
                                          M.read (| head |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          depth,
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::cmp::Ord",
                                              Ty.path "u16",
                                              [],
                                              "max",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path
                                                    "move_bytecode_verifier::loop_summary::LoopPartition",
                                                  "depth",
                                                  []
                                                |),
                                                [
                                                  M.read (| self |);
                                                  M.read (| M.read (| constituent |) |)
                                                ]
                                              |);
                                              M.read (| depth |)
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              let β := depth in
              M.write (|
                β,
                BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U16 1 |)
              |) in
            let~ _ :=
              M.write (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier::loop_summary::LoopPartition",
                    "depth_mut",
                    []
                  |),
                  [ M.read (| self |); M.read (| head |) ]
                |),
                M.read (| depth |)
              |) in
            depth
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_collapse_loop :
      M.IsAssociatedFunction Self "collapse_loop" collapse_loop.
    
    (*
        fn parent(&self, l: NodeId) -> NodeId {
            self.parents[usize::from(l)]
        }
    *)
    Definition parent (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; l ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let l := M.alloc (| l |) in
          M.read (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::index::Index",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                    Ty.path "alloc::alloc::Global"
                  ],
                [ Ty.path "usize" ],
                "index",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::loop_summary::LoopPartition",
                  "parents"
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.path "usize",
                    [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                    "from",
                    []
                  |),
                  [ M.read (| l |) ]
                |)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_parent : M.IsAssociatedFunction Self "parent" parent.
    
    (*
        fn parent_mut(&mut self, l: NodeId) -> &mut NodeId {
            &mut self.parents[usize::from(l)]
        }
    *)
    Definition parent_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; l ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let l := M.alloc (| l |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::IndexMut",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.path "move_bytecode_verifier::loop_summary::NodeId";
                  Ty.path "alloc::alloc::Global"
                ],
              [ Ty.path "usize" ],
              "index_mut",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_bytecode_verifier::loop_summary::LoopPartition",
                "parents"
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "usize",
                  [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                  "from",
                  []
                |),
                [ M.read (| l |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_parent_mut : M.IsAssociatedFunction Self "parent_mut" parent_mut.
    
    (*
        fn depth(&self, l: NodeId) -> u16 {
            self.depths[usize::from(l)]
        }
    *)
    Definition depth (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; l ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let l := M.alloc (| l |) in
          M.read (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::index::Index",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                [ Ty.path "usize" ],
                "index",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::loop_summary::LoopPartition",
                  "depths"
                |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::From",
                    Ty.path "usize",
                    [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                    "from",
                    []
                  |),
                  [ M.read (| l |) ]
                |)
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_depth : M.IsAssociatedFunction Self "depth" depth.
    
    (*
        fn depth_mut(&mut self, l: NodeId) -> &mut u16 {
            &mut self.depths[usize::from(l)]
        }
    *)
    Definition depth_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; l ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let l := M.alloc (| l |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::ops::index::IndexMut",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
              [ Ty.path "usize" ],
              "index_mut",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_bytecode_verifier::loop_summary::LoopPartition",
                "depths"
              |);
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::From",
                  Ty.path "usize",
                  [ Ty.path "move_bytecode_verifier::loop_summary::NodeId" ],
                  "from",
                  []
                |),
                [ M.read (| l |) ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_depth_mut : M.IsAssociatedFunction Self "depth_mut" depth_mut.
  End Impl_move_bytecode_verifier_loop_summary_LoopPartition.
  
  Module Impl_move_bytecode_verifier_loop_summary_NodeId.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier::loop_summary::NodeId".
    
    (*
        fn bump(&mut self) -> NodeId {
            let ret = *self;
            self.0 += 1;
            ret
        }
    *)
    Definition bump (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ ret := M.copy (| M.read (| self |) |) in
            let~ _ :=
              let β :=
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "move_bytecode_verifier::loop_summary::NodeId",
                  0
                |) in
              M.write (|
                β,
                BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U16 1 |)
              |) in
            ret
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_bump : M.IsAssociatedFunction Self "bump" bump.
  End Impl_move_bytecode_verifier_loop_summary_NodeId.
  
  Module Impl_core_convert_From_move_bytecode_verifier_loop_summary_NodeId_for_usize.
    Definition Self : Ty.t := Ty.path "usize".
    
    (*
        fn from(NodeId(id): NodeId) -> usize {
            id as usize
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ β0 ] =>
        ltac:(M.monadic
          (let β0 := M.alloc (| β0 |) in
          M.match_operator (|
            β0,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (|
                      γ,
                      "move_bytecode_verifier::loop_summary::NodeId",
                      0
                    |) in
                  let id := M.copy (| γ0_0 |) in
                  M.rust_cast (M.read (| id |))))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [ (* T *) Ty.path "move_bytecode_verifier::loop_summary::NodeId" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_move_bytecode_verifier_loop_summary_NodeId_for_usize.
End loop_summary.
