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

Module control_flow_graph.
  Axiom Map :
    forall (K V : Ty.t),
    (Ty.apply (Ty.path "move_binary_format::control_flow_graph::Map") [] [ K; V ]) =
      (Ty.apply
        (Ty.path "alloc::collections::btree::map::BTreeMap")
        []
        [ K; V; Ty.path "alloc::alloc::Global" ]).
  
  Axiom Set_ :
    forall (V : Ty.t),
    (Ty.apply (Ty.path "move_binary_format::control_flow_graph::Set") [] [ V ]) =
      (Ty.apply
        (Ty.path "alloc::collections::btree::set::BTreeSet")
        []
        [ V; Ty.path "alloc::alloc::Global" ]).
  
  Axiom BlockId : (Ty.path "move_binary_format::control_flow_graph::BlockId") = (Ty.path "u16").
  
  (* Trait *)
  (* Empty module 'ControlFlowGraph' *)
  
  (* StructRecord
    {
      name := "BasicBlock";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("exit", Ty.path "u16");
          ("successors",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ])
        ];
    } *)
  
  (* StructRecord
    {
      name := "VMControlFlowGraph";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("blocks",
            Ty.apply
              (Ty.path "alloc::collections::btree::map::BTreeMap")
              []
              [
                Ty.path "u16";
                Ty.path "move_binary_format::control_flow_graph::BasicBlock";
                Ty.path "alloc::alloc::Global"
              ]);
          ("traversal_successors",
            Ty.apply
              (Ty.path "alloc::collections::btree::map::BTreeMap")
              []
              [ Ty.path "u16"; Ty.path "u16"; Ty.path "alloc::alloc::Global" ]);
          ("loop_heads",
            Ty.apply
              (Ty.path "alloc::collections::btree::map::BTreeMap")
              []
              [
                Ty.path "u16";
                Ty.apply
                  (Ty.path "alloc::collections::btree::set::BTreeSet")
                  []
                  [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ];
                Ty.path "alloc::alloc::Global"
              ])
        ];
    } *)
  
  Module Impl_move_binary_format_control_flow_graph_BasicBlock.
    Definition Self : Ty.t := Ty.path "move_binary_format::control_flow_graph::BasicBlock".
    
    (*
        pub fn display(&self, entry: BlockId) {
            println!("+=======================+");
            println!("| Enter:  {}            |", entry);
            println!("+-----------------------+");
            println!("==> Children: {:?}", self.successors);
            println!("+-----------------------+");
            println!("| Exit:   {}            |", self.exit);
            println!("+=======================+");
        }
    *)
    Definition display (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; entry ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let entry := M.alloc (| entry |) in
          M.read (|
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_const",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array [ M.read (| Value.String "+=======================+
" |) ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_v1",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array
                              [
                                M.read (| Value.String "| Enter:  " |);
                                M.read (| Value.String "            |
" |)
                              ]
                          |);
                          M.alloc (|
                            Value.Array
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::rt::Argument",
                                    "new_display",
                                    [ Ty.path "u16" ]
                                  |),
                                  [ entry ]
                                |)
                              ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_const",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array [ M.read (| Value.String "+-----------------------+
" |) ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_v1",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array
                              [
                                M.read (| Value.String "==> Children: " |);
                                M.read (| Value.String "
" |)
                              ]
                          |);
                          M.alloc (|
                            Value.Array
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::rt::Argument",
                                    "new_debug",
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]
                                    ]
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::control_flow_graph::BasicBlock",
                                      "successors"
                                    |)
                                  ]
                                |)
                              ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_const",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array [ M.read (| Value.String "+-----------------------+
" |) ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_v1",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array
                              [
                                M.read (| Value.String "| Exit:   " |);
                                M.read (| Value.String "            |
" |)
                              ]
                          |);
                          M.alloc (|
                            Value.Array
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::rt::Argument",
                                    "new_display",
                                    [ Ty.path "u16" ]
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::control_flow_graph::BasicBlock",
                                      "exit"
                                    |)
                                  ]
                                |)
                              ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_const",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array [ M.read (| Value.String "+=======================+
" |) ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_display : M.IsAssociatedFunction Self "display" display.
  End Impl_move_binary_format_control_flow_graph_BasicBlock.
  
  Definition value_ENTRY_BLOCK_ID : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U16 0 |))).
  
  Module Impl_move_binary_format_control_flow_graph_VMControlFlowGraph.
    Definition Self : Ty.t := Ty.path "move_binary_format::control_flow_graph::VMControlFlowGraph".
    
    (*
        pub fn new(code: &[Bytecode]) -> Self {
            let code_len = code.len() as CodeOffset;
            // First go through and collect block ids, i.e., offsets that begin basic blocks.
            // Need to do this first in order to handle backwards edges.
            let mut block_ids = Set::new();
            block_ids.insert(ENTRY_BLOCK_ID);
            for pc in 0..code.len() {
                VMControlFlowGraph::record_block_ids(pc as CodeOffset, code, &mut block_ids);
            }
    
            // Create basic blocks
            let mut blocks = Map::new();
            let mut entry = 0;
            let mut exit_to_entry = Map::new();
            for pc in 0..code.len() {
                let co_pc = pc as CodeOffset;
    
                // Create a basic block
                if Self::is_end_of_block(co_pc, code, &block_ids) {
                    let exit = co_pc;
                    exit_to_entry.insert(exit, entry);
                    let successors = Bytecode::get_successors(co_pc, code);
                    let bb = BasicBlock { exit, successors };
                    blocks.insert(entry, bb);
                    entry = co_pc + 1;
                }
            }
            let blocks = blocks;
            assert_eq!(entry, code_len);
    
            // # Loop analysis
            //
            // This section identifies loops in the control-flow graph, picks a back edge and loop head
            // (the basic block the back edge returns to), and decides the order that blocks are
            // traversed during abstract interpretation (reverse post-order).
            //
            // The implementation is based on the algorithm for finding widening points in Section 4.1,
            // "Depth-first numbering" of Bourdoncle [1993], "Efficient chaotic iteration strategies
            // with widenings."
            //
            // NB. The comments below refer to a block's sub-graph -- the reflexive transitive closure
            // of its successor edges, modulo cycles.
    
            #[derive(Copy, Clone)]
            enum Exploration {
                InProgress,
                Done,
            }
    
            let mut exploration: Map<BlockId, Exploration> = Map::new();
            let mut stack = vec![ENTRY_BLOCK_ID];
    
            // For every loop in the CFG that is reachable from the entry block, there is an entry in
            // `loop_heads` mapping to all the back edges pointing to it, and vice versa.
            //
            // Entry in `loop_heads` implies loop in the CFG is justified by the comments in the loop
            // below.  Loop in the CFG implies entry in `loop_heads` is justified by considering the
            // point at which the first node in that loop, `F` is added to the `exploration` map:
            //
            // - By definition `F` is part of a loop, meaning there is a block `L` such that:
            //
            //     F - ... -> L -> F
            //
            // - `F` will not transition to `Done` until all the nodes reachable from it (including `L`)
            //   have been visited.
            // - Because `F` is the first node seen in the loop, all the other nodes in the loop
            //   (including `L`) will be visited while `F` is `InProgress`.
            // - Therefore, we will process the `L -> F` edge while `F` is `InProgress`.
            // - Therefore, we will record a back edge to it.
            let mut loop_heads: Map<BlockId, Set<BlockId>> = Map::new();
    
            // Blocks appear in `post_order` after all the blocks in their (non-reflexive) sub-graph.
            let mut post_order = Vec::with_capacity(blocks.len());
    
            while let Some(block) = stack.pop() {
                match exploration.entry(block) {
                    Entry::Vacant(entry) => {
                        // Record the fact that exploration of this block and its sub-graph has started.
                        entry.insert(Exploration::InProgress);
    
                        // Push the block back on the stack to finish processing it, and mark it as done
                        // once its sub-graph has been traversed.
                        stack.push(block);
    
                        for succ in &blocks[&block].successors {
                            match exploration.get(succ) {
                                // This successor has never been visited before, add it to the stack to
                                // be explored before `block` gets marked `Done`.
                                None => stack.push( *succ),
    
                                // This block's sub-graph was being explored, meaning it is a (reflexive
                                // transitive) predecessor of `block` as well as being a successor,
                                // implying a loop has been detected -- greedily choose the successor
                                // block as the loop head.
                                Some(Exploration::InProgress) => {
                                    loop_heads.entry( *succ).or_default().insert(block);
                                }
    
                                // Cross-edge detected, this block and its entire sub-graph (modulo
                                // cycles) has already been explored via a different path, and is
                                // already present in `post_order`.
                                Some(Exploration::Done) => { /* skip */ }
                            };
                        }
                    }
    
                    Entry::Occupied(mut entry) => match entry.get() {
                        // Already traversed the sub-graph reachable from this block, so skip it.
                        Exploration::Done => continue,
    
                        // Finish up the traversal by adding this block to the post-order traversal
                        // after its sub-graph (modulo cycles).
                        Exploration::InProgress => {
                            post_order.push(block);
                            entry.insert(Exploration::Done);
                        }
                    },
                }
            }
    
            let traversal_order = {
                // This reverse post order is akin to a topological sort (ignoring cycles) and is
                // different from a pre-order in the presence of diamond patterns in the graph.
                post_order.reverse();
                post_order
            };
    
            // build a mapping from a block id to the next block id in the traversal order
            let traversal_successors = traversal_order
                .windows(2)
                .map(|window| {
                    debug_assert!(window.len() == 2);
                    (window[0], window[1])
                })
                .collect();
    
            VMControlFlowGraph {
                blocks,
                traversal_successors,
                loop_heads,
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ code ] =>
        ltac:(M.monadic
          (let code := M.alloc (| code |) in
          M.read (|
            let~ code_len :=
              M.alloc (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "slice")
                        []
                        [ Ty.path "move_binary_format::file_format::Bytecode" ],
                      "len",
                      []
                    |),
                    [ M.read (| code |) ]
                  |))
              |) in
            let~ block_ids :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::set::BTreeSet")
                      []
                      [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::set::BTreeSet")
                      []
                      [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                    "insert",
                    []
                  |),
                  [
                    block_ids;
                    M.read (|
                      M.get_constant (| "move_binary_format::control_flow_graph::ENTRY_BLOCK_ID" |)
                    |)
                  ]
                |)
              |) 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 "core::ops::range::Range") [] [ Ty.path "usize" ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        Value.StructRecord
                          "core::ops::range::Range"
                          [
                            ("start", Value.Integer IntegerKind.Usize 0);
                            ("end_",
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [ Ty.path "move_binary_format::file_format::Bytecode" ],
                                  "len",
                                  []
                                |),
                                [ M.read (| code |) ]
                              |))
                          ]
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::ops::range::Range")
                                        []
                                        [ Ty.path "usize" ],
                                      [],
                                      "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 pc := M.copy (| γ0_0 |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_binary_format::control_flow_graph::VMControlFlowGraph",
                                              "record_block_ids",
                                              []
                                            |),
                                            [
                                              M.rust_cast (M.read (| pc |));
                                              M.read (| code |);
                                              block_ids
                                            ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ blocks :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [
                        Ty.path "u16";
                        Ty.path "move_binary_format::control_flow_graph::BasicBlock";
                        Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ entry := M.alloc (| Value.Integer IntegerKind.U16 0 |) in
            let~ exit_to_entry :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [ Ty.path "u16"; Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                    "new",
                    []
                  |),
                  []
                |)
              |) 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 "core::ops::range::Range") [] [ Ty.path "usize" ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        Value.StructRecord
                          "core::ops::range::Range"
                          [
                            ("start", Value.Integer IntegerKind.Usize 0);
                            ("end_",
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "slice")
                                    []
                                    [ Ty.path "move_binary_format::file_format::Bytecode" ],
                                  "len",
                                  []
                                |),
                                [ M.read (| code |) ]
                              |))
                          ]
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "core::ops::range::Range")
                                        []
                                        [ Ty.path "usize" ],
                                      [],
                                      "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 pc := M.copy (| γ0_0 |) in
                                      let~ co_pc := M.alloc (| M.rust_cast (M.read (| pc |)) |) in
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ :=
                                                M.use
                                                  (M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "move_binary_format::control_flow_graph::VMControlFlowGraph",
                                                        "is_end_of_block",
                                                        []
                                                      |),
                                                      [
                                                        M.read (| co_pc |);
                                                        M.read (| code |);
                                                        block_ids
                                                      ]
                                                    |)
                                                  |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ exit := M.copy (| co_pc |) 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 "u16";
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      "insert",
                                                      []
                                                    |),
                                                    [
                                                      exit_to_entry;
                                                      M.read (| exit |);
                                                      M.read (| entry |)
                                                    ]
                                                  |)
                                                |) in
                                              let~ successors :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path
                                                        "move_binary_format::file_format::Bytecode",
                                                      "get_successors",
                                                      []
                                                    |),
                                                    [ M.read (| co_pc |); M.read (| code |) ]
                                                  |)
                                                |) in
                                              let~ bb :=
                                                M.alloc (|
                                                  Value.StructRecord
                                                    "move_binary_format::control_flow_graph::BasicBlock"
                                                    [
                                                      ("exit", M.read (| exit |));
                                                      ("successors", M.read (| successors |))
                                                    ]
                                                |) 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_binary_format::control_flow_graph::BasicBlock";
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      "insert",
                                                      []
                                                    |),
                                                    [ blocks; M.read (| entry |); M.read (| bb |) ]
                                                  |)
                                                |) in
                                              let~ _ :=
                                                M.write (|
                                                  entry,
                                                  BinOp.Wrap.add (|
                                                    M.read (| co_pc |),
                                                    Value.Integer IntegerKind.U16 1
                                                  |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ blocks := M.copy (| blocks |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [ entry; code_len ] |),
                [
                  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 (|
                                      BinOp.eq (|
                                        M.read (| M.read (| left_val |) |),
                                        M.read (| 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 "u16"; Ty.path "u16" ]
                                        |),
                                        [
                                          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
            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_binary_format::control_flow_graph::new::Exploration";
                        Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ stack :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u16" ],
                    "into_vec",
                    [ Ty.path "alloc::alloc::Global" ]
                  |),
                  [
                    M.read (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::boxed::Box")
                            []
                            [
                              Ty.apply
                                (Ty.path "array")
                                [ Value.Integer IntegerKind.Usize 1 ]
                                [ Ty.path "u16" ];
                              Ty.path "alloc::alloc::Global"
                            ],
                          "new",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array
                              [
                                M.read (|
                                  M.get_constant (|
                                    "move_binary_format::control_flow_graph::ENTRY_BLOCK_ID"
                                  |)
                                |)
                              ]
                          |)
                        ]
                      |)
                    |)
                  ]
                |)
              |) in
            let~ loop_heads :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::map::BTreeMap")
                      []
                      [
                        Ty.path "u16";
                        Ty.apply
                          (Ty.path "alloc::collections::btree::set::BTreeSet")
                          []
                          [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ post_order :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                    "with_capacity",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::map::BTreeMap")
                          []
                          [
                            Ty.path "u16";
                            Ty.path "move_binary_format::control_flow_graph::BasicBlock";
                            Ty.path "alloc::alloc::Global"
                          ],
                        "len",
                        []
                      |),
                      [ blocks ]
                    |)
                  ]
                |)
              |) 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 "u16"; Ty.path "alloc::alloc::Global" ],
                                  "pop",
                                  []
                                |),
                                [ stack ]
                              |)
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let block := 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::BTreeMap")
                                    []
                                    [
                                      Ty.path "u16";
                                      Ty.path
                                        "move_binary_format::control_flow_graph::new::Exploration";
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "entry",
                                  []
                                |),
                                [ exploration; M.read (| block |) ]
                              |)
                            |),
                            [
                              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~ _ :=
                                    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_binary_format::control_flow_graph::new::Exploration";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "insert",
                                          []
                                        |),
                                        [
                                          M.read (| entry |);
                                          Value.StructTuple
                                            "move_binary_format::control_flow_graph::new::Exploration::InProgress"
                                            []
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                          "push",
                                          []
                                        |),
                                        [ stack; M.read (| block |) ]
                                      |)
                                    |) in
                                  M.use
                                    (M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::collect::IntoIterator",
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]
                                              ],
                                            [],
                                            "into_iter",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::index::Index",
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloc::collections::btree::map::BTreeMap")
                                                    []
                                                    [
                                                      Ty.path "u16";
                                                      Ty.path
                                                        "move_binary_format::control_flow_graph::BasicBlock";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ],
                                                  "index",
                                                  []
                                                |),
                                                [ blocks; block ]
                                              |),
                                              "move_binary_format::control_flow_graph::BasicBlock",
                                              "successors"
                                            |)
                                          ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let iter := M.copy (| γ |) in
                                            M.loop (|
                                              ltac:(M.monadic
                                                (let~ _ :=
                                                  M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::iter::traits::iterator::Iterator",
                                                          Ty.apply
                                                            (Ty.path "core::slice::iter::Iter")
                                                            []
                                                            [ Ty.path "u16" ],
                                                          [],
                                                          "next",
                                                          []
                                                        |),
                                                        [ iter ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let _ :=
                                                            M.is_struct_tuple (|
                                                              γ,
                                                              "core::option::Option::None"
                                                            |) in
                                                          M.alloc (|
                                                            M.never_to_any (|
                                                              M.read (| M.break (||) |)
                                                            |)
                                                          |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ0_0 :=
                                                            M.SubPointer.get_struct_tuple_field (|
                                                              γ,
                                                              "core::option::Option::Some",
                                                              0
                                                            |) in
                                                          let succ := M.copy (| γ0_0 |) in
                                                          let~ _ :=
                                                            M.match_operator (|
                                                              M.alloc (|
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "alloc::collections::btree::map::BTreeMap")
                                                                      []
                                                                      [
                                                                        Ty.path "u16";
                                                                        Ty.path
                                                                          "move_binary_format::control_flow_graph::new::Exploration";
                                                                        Ty.path
                                                                          "alloc::alloc::Global"
                                                                      ],
                                                                    "get",
                                                                    [ Ty.path "u16" ]
                                                                  |),
                                                                  [ exploration; M.read (| succ |) ]
                                                                |)
                                                              |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "core::option::Option::None"
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_associated_function (|
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "alloc::vec::Vec")
                                                                            []
                                                                            [
                                                                              Ty.path "u16";
                                                                              Ty.path
                                                                                "alloc::alloc::Global"
                                                                            ],
                                                                          "push",
                                                                          []
                                                                        |),
                                                                        [
                                                                          stack;
                                                                          M.read (|
                                                                            M.read (| succ |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        γ,
                                                                        "core::option::Option::Some",
                                                                        0
                                                                      |) in
                                                                    let γ0_0 := M.read (| γ0_0 |) in
                                                                    let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ0_0,
                                                                        "move_binary_format::control_flow_graph::new::Exploration::InProgress"
                                                                      |) in
                                                                    let~ _ :=
                                                                      M.alloc (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "alloc::collections::btree::set::BTreeSet")
                                                                              []
                                                                              [
                                                                                Ty.path "u16";
                                                                                Ty.path
                                                                                  "alloc::alloc::Global"
                                                                              ],
                                                                            "insert",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "alloc::collections::btree::map::entry::Entry")
                                                                                  []
                                                                                  [
                                                                                    Ty.path "u16";
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "alloc::collections::btree::set::BTreeSet")
                                                                                      []
                                                                                      [
                                                                                        Ty.path
                                                                                          "u16";
                                                                                        Ty.path
                                                                                          "alloc::alloc::Global"
                                                                                      ];
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ],
                                                                                "or_default",
                                                                                []
                                                                              |),
                                                                              [
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "alloc::collections::btree::map::BTreeMap")
                                                                                      []
                                                                                      [
                                                                                        Ty.path
                                                                                          "u16";
                                                                                        Ty.apply
                                                                                          (Ty.path
                                                                                            "alloc::collections::btree::set::BTreeSet")
                                                                                          []
                                                                                          [
                                                                                            Ty.path
                                                                                              "u16";
                                                                                            Ty.path
                                                                                              "alloc::alloc::Global"
                                                                                          ];
                                                                                        Ty.path
                                                                                          "alloc::alloc::Global"
                                                                                      ],
                                                                                    "entry",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    loop_heads;
                                                                                    M.read (|
                                                                                      M.read (|
                                                                                        succ
                                                                                      |)
                                                                                    |)
                                                                                  ]
                                                                                |)
                                                                              ]
                                                                            |);
                                                                            M.read (| block |)
                                                                          ]
                                                                        |)
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        γ,
                                                                        "core::option::Option::Some",
                                                                        0
                                                                      |) in
                                                                    let γ0_0 := M.read (| γ0_0 |) in
                                                                    let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ0_0,
                                                                        "move_binary_format::control_flow_graph::new::Exploration::Done"
                                                                      |) in
                                                                    M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |) in
                                                M.alloc (| Value.Tuple [] |)))
                                            |)))
                                      ]
                                    |))));
                              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_binary_format::control_flow_graph::new::Exploration";
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "get",
                                          []
                                        |),
                                        [ entry ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ := M.read (| γ |) in
                                          let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "move_binary_format::control_flow_graph::new::Exploration::Done"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.continue (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ := M.read (| γ |) in
                                          let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "move_binary_format::control_flow_graph::new::Exploration::InProgress"
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [ Ty.path "u16"; Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "push",
                                                  []
                                                |),
                                                [ post_order; M.read (| block |) ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            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_binary_format::control_flow_graph::new::Exploration";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "insert",
                                                  []
                                                |),
                                                [
                                                  entry;
                                                  Value.StructTuple
                                                    "move_binary_format::control_flow_graph::new::Exploration::Done"
                                                    []
                                                ]
                                              |)
                                            |) 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
            let~ traversal_order :=
              M.copy (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "u16" ],
                        "reverse",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::DerefMut",
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                            [],
                            "deref_mut",
                            []
                          |),
                          [ post_order ]
                        |)
                      ]
                    |)
                  |) in
                post_order
              |) in
            let~ traversal_successors :=
              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::Windows") [] [ Ty.path "u16" ];
                        Ty.function
                          [
                            Ty.tuple
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.apply (Ty.path "slice") [] [ Ty.path "u16" ] ]
                              ]
                          ]
                          (Ty.tuple [ Ty.path "u16"; Ty.path "u16" ])
                      ],
                    [],
                    "collect",
                    [
                      Ty.apply
                        (Ty.path "alloc::collections::btree::map::BTreeMap")
                        []
                        [ Ty.path "u16"; Ty.path "u16"; Ty.path "alloc::alloc::Global" ]
                    ]
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply (Ty.path "core::slice::iter::Windows") [] [ Ty.path "u16" ],
                        [],
                        "map",
                        [
                          Ty.tuple [ Ty.path "u16"; Ty.path "u16" ];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u16" ] ]
                                ]
                            ]
                            (Ty.tuple [ Ty.path "u16"; Ty.path "u16" ])
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "u16" ],
                            "windows",
                            []
                          |),
                          [
                            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",
                                []
                              |),
                              [ traversal_order ]
                            |);
                            Value.Integer IntegerKind.Usize 2
                          ]
                        |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let window := M.copy (| γ |) 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 [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      UnOp.not (|
                                                                        BinOp.eq (|
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.apply
                                                                                (Ty.path "slice")
                                                                                []
                                                                                [ Ty.path "u16" ],
                                                                              "len",
                                                                              []
                                                                            |),
                                                                            [ M.read (| window |) ]
                                                                          |),
                                                                          Value.Integer
                                                                            IntegerKind.Usize
                                                                            2
                                                                        |)
                                                                      |)
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                M.alloc (|
                                                                  M.never_to_any (|
                                                                    M.call_closure (|
                                                                      M.get_function (|
                                                                        "core::panicking::panic",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (|
                                                                          Value.String
                                                                            "assertion failed: window.len() == 2"
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |)
                                                                |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            M.alloc (|
                                              Value.Tuple
                                                [
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| window |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 0
                                                      |)
                                                    |)
                                                  |);
                                                  M.read (|
                                                    M.SubPointer.get_array_field (|
                                                      M.read (| window |),
                                                      M.alloc (|
                                                        Value.Integer IntegerKind.Usize 1
                                                      |)
                                                    |)
                                                  |)
                                                ]
                                            |)
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  ]
                |)
              |) in
            M.alloc (|
              Value.StructRecord
                "move_binary_format::control_flow_graph::VMControlFlowGraph"
                [
                  ("blocks", M.read (| blocks |));
                  ("traversal_successors", M.read (| traversal_successors |));
                  ("loop_heads", M.read (| loop_heads |))
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn display(&self) {
            for (entry, block) in &self.blocks {
                block.display( *entry);
            }
            println!("Traversal: {:#?}", self.traversal_successors);
        }
    *)
    Definition display (ε : 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~ _ :=
              M.use
                (M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::IntoIterator",
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::collections::btree::map::BTreeMap")
                              []
                              [
                                Ty.path "u16";
                                Ty.path "move_binary_format::control_flow_graph::BasicBlock";
                                Ty.path "alloc::alloc::Global"
                              ]
                          ],
                        [],
                        "into_iter",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_binary_format::control_flow_graph::VMControlFlowGraph",
                          "blocks"
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let iter := M.copy (| γ |) in
                        M.loop (|
                          ltac:(M.monadic
                            (let~ _ :=
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::iter::traits::iterator::Iterator",
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::map::Iter")
                                        []
                                        [
                                          Ty.path "u16";
                                          Ty.path
                                            "move_binary_format::control_flow_graph::BasicBlock"
                                        ],
                                      [],
                                      "next",
                                      []
                                    |),
                                    [ iter ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                      M.alloc (|
                                        M.never_to_any (| M.read (| M.break (||) |) |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::option::Option::Some",
                                          0
                                        |) in
                                      let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                      let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                      let entry := M.copy (| γ1_0 |) in
                                      let block := M.copy (| γ1_1 |) in
                                      let~ _ :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "move_binary_format::control_flow_graph::BasicBlock",
                                              "display",
                                              []
                                            |),
                                            [ M.read (| block |); M.read (| M.read (| entry |) |) ]
                                          |)
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            M.alloc (| Value.Tuple [] |)))
                        |)))
                  ]
                |)) in
            let~ _ :=
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "std::io::stdio::_print", [] |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Arguments",
                          "new_v1_formatted",
                          []
                        |),
                        [
                          M.alloc (|
                            Value.Array
                              [
                                M.read (| Value.String "Traversal: " |);
                                M.read (| Value.String "
" |)
                              ]
                          |);
                          M.alloc (|
                            Value.Array
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::rt::Argument",
                                    "new_debug",
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::collections::btree::map::BTreeMap")
                                        []
                                        [
                                          Ty.path "u16";
                                          Ty.path "u16";
                                          Ty.path "alloc::alloc::Global"
                                        ]
                                    ]
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_binary_format::control_flow_graph::VMControlFlowGraph",
                                      "traversal_successors"
                                    |)
                                  ]
                                |)
                              ]
                          |);
                          M.alloc (|
                            Value.Array
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "core::fmt::rt::Placeholder",
                                    "new",
                                    []
                                  |),
                                  [
                                    Value.Integer IntegerKind.Usize 0;
                                    Value.UnicodeChar 32;
                                    Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                    Value.Integer IntegerKind.U32 4;
                                    Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                    Value.StructTuple "core::fmt::rt::Count::Implied" []
                                  ]
                                |)
                              ]
                          |);
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::rt::UnsafeArg",
                              "new",
                              []
                            |),
                            []
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_display : M.IsAssociatedFunction Self "display" display.
    
    (*
        fn is_end_of_block(pc: CodeOffset, code: &[Bytecode], block_ids: &Set<BlockId>) -> bool {
            pc + 1 == (code.len() as CodeOffset) || block_ids.contains(&(pc + 1))
        }
    *)
    Definition is_end_of_block (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ pc; code; block_ids ] =>
        ltac:(M.monadic
          (let pc := M.alloc (| pc |) in
          let code := M.alloc (| code |) in
          let block_ids := M.alloc (| block_ids |) in
          LogicalOp.or (|
            BinOp.eq (|
              BinOp.Wrap.add (| M.read (| pc |), Value.Integer IntegerKind.U16 1 |),
              M.rust_cast
                (M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "slice")
                      []
                      [ Ty.path "move_binary_format::file_format::Bytecode" ],
                    "len",
                    []
                  |),
                  [ M.read (| code |) ]
                |))
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::collections::btree::set::BTreeSet")
                    []
                    [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                  "contains",
                  [ Ty.path "u16" ]
                |),
                [
                  M.read (| block_ids |);
                  M.alloc (|
                    BinOp.Wrap.add (| M.read (| pc |), Value.Integer IntegerKind.U16 1 |)
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_end_of_block :
      M.IsAssociatedFunction Self "is_end_of_block" is_end_of_block.
    
    (*
        fn record_block_ids(pc: CodeOffset, code: &[Bytecode], block_ids: &mut Set<BlockId>) {
            let bytecode = &code[pc as usize];
    
            if let Some(offset) = bytecode.offset() {
                block_ids.insert( *offset);
            }
    
            if bytecode.is_branch() && pc + 1 < (code.len() as CodeOffset) {
                block_ids.insert(pc + 1);
            }
        }
    *)
    Definition record_block_ids (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ pc; code; block_ids ] =>
        ltac:(M.monadic
          (let pc := M.alloc (| pc |) in
          let code := M.alloc (| code |) in
          let block_ids := M.alloc (| block_ids |) in
          M.read (|
            let~ bytecode :=
              M.alloc (|
                M.SubPointer.get_array_field (|
                  M.read (| code |),
                  M.alloc (| M.rust_cast (M.read (| pc |)) |)
                |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_binary_format::file_format::Bytecode",
                              "offset",
                              []
                            |),
                            [ M.read (| bytecode |) ]
                          |)
                        |) in
                      let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let offset := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::collections::btree::set::BTreeSet")
                                []
                                [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                              "insert",
                              []
                            |),
                            [ M.read (| block_ids |); M.read (| M.read (| offset |) |) ]
                          |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          LogicalOp.and (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "move_binary_format::file_format::Bytecode",
                                "is_branch",
                                []
                              |),
                              [ M.read (| bytecode |) ]
                            |),
                            ltac:(M.monadic
                              (BinOp.lt (|
                                BinOp.Wrap.add (|
                                  M.read (| pc |),
                                  Value.Integer IntegerKind.U16 1
                                |),
                                M.rust_cast
                                  (M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "slice")
                                        []
                                        [ Ty.path "move_binary_format::file_format::Bytecode" ],
                                      "len",
                                      []
                                    |),
                                    [ M.read (| code |) ]
                                  |))
                              |)))
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::collections::btree::set::BTreeSet")
                              []
                              [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                            "insert",
                            []
                          |),
                          [
                            M.read (| block_ids |);
                            BinOp.Wrap.add (| M.read (| pc |), Value.Integer IntegerKind.U16 1 |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_record_block_ids :
      M.IsAssociatedFunction Self "record_block_ids" record_block_ids.
    
    (*
        fn traverse_by(&self, block_id: BlockId) -> Vec<BlockId> {
            let mut ret = Vec::new();
            // We use this index to keep track of our frontier.
            let mut index = 0;
            // Guard against cycles
            let mut seen = Set::new();
    
            ret.push(block_id);
            seen.insert(&block_id);
    
            while index < ret.len() {
                let block_id = ret[index];
                index += 1;
                let successors = self.successors(block_id);
                for block_id in successors.iter() {
                    if !seen.contains(&block_id) {
                        ret.push( *block_id);
                        seen.insert(block_id);
                    }
                }
            }
    
            ret
        }
    *)
    Definition traverse_by (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; block_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let block_id := M.alloc (| block_id |) in
          M.read (|
            let~ ret :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ index := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
            let~ seen :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::set::BTreeSet")
                      []
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ]; Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                    "push",
                    []
                  |),
                  [ ret; M.read (| block_id |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::collections::btree::set::BTreeSet")
                      []
                      [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ]; Ty.path "alloc::alloc::Global"
                      ],
                    "insert",
                    []
                  |),
                  [ seen; block_id ]
                |)
              |) in
            let~ _ :=
              M.loop (|
                ltac:(M.monadic
                  (M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.lt (|
                                  M.read (| index |),
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                      "len",
                                      []
                                    |),
                                    [ ret ]
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ block_id :=
                            M.copy (|
                              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",
                                  []
                                |),
                                [ ret; M.read (| index |) ]
                              |)
                            |) in
                          let~ _ :=
                            let β := index in
                            M.write (|
                              β,
                              BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.Usize 1 |)
                            |) in
                          let~ successors :=
                            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",
                                  [],
                                  "successors",
                                  []
                                |),
                                [ M.read (| self |); M.read (| block_id |) ]
                              |)
                            |) in
                          M.use
                            (M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::collect::IntoIterator",
                                    Ty.apply
                                      (Ty.path "core::slice::iter::Iter")
                                      []
                                      [ Ty.path "u16" ],
                                    [],
                                    "into_iter",
                                    []
                                  |),
                                  [
                                    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.read (| successors |) ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let iter := M.copy (| γ |) in
                                    M.loop (|
                                      ltac:(M.monadic
                                        (let~ _ :=
                                          M.match_operator (|
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::iter::traits::iterator::Iterator",
                                                  Ty.apply
                                                    (Ty.path "core::slice::iter::Iter")
                                                    []
                                                    [ Ty.path "u16" ],
                                                  [],
                                                  "next",
                                                  []
                                                |),
                                                [ iter ]
                                              |)
                                            |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let _ :=
                                                    M.is_struct_tuple (|
                                                      γ,
                                                      "core::option::Option::None"
                                                    |) in
                                                  M.alloc (|
                                                    M.never_to_any (| M.read (| M.break (||) |) |)
                                                  |)));
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let block_id := M.copy (| γ0_0 |) in
                                                  M.match_operator (|
                                                    M.alloc (| Value.Tuple [] |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let γ :=
                                                            M.use
                                                              (M.alloc (|
                                                                UnOp.not (|
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "alloc::collections::btree::set::BTreeSet")
                                                                        []
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "&")
                                                                            []
                                                                            [ Ty.path "u16" ];
                                                                          Ty.path
                                                                            "alloc::alloc::Global"
                                                                        ],
                                                                      "contains",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [ Ty.path "u16" ]
                                                                      ]
                                                                    |),
                                                                    [ seen; block_id ]
                                                                  |)
                                                                |)
                                                              |)) in
                                                          let _ :=
                                                            M.is_constant_or_break_match (|
                                                              M.read (| γ |),
                                                              Value.Bool true
                                                            |) in
                                                          let~ _ :=
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "alloc::vec::Vec")
                                                                    []
                                                                    [
                                                                      Ty.path "u16";
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ],
                                                                  "push",
                                                                  []
                                                                |),
                                                                [
                                                                  ret;
                                                                  M.read (| M.read (| block_id |) |)
                                                                ]
                                                              |)
                                                            |) in
                                                          let~ _ :=
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path
                                                                      "alloc::collections::btree::set::BTreeSet")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "&")
                                                                        []
                                                                        [ Ty.path "u16" ];
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ],
                                                                  "insert",
                                                                  []
                                                                |),
                                                                [ seen; M.read (| block_id |) ]
                                                              |)
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)));
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (M.alloc (| Value.Tuple [] |)))
                                                    ]
                                                  |)))
                                            ]
                                          |) 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
            ret
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_traverse_by : M.IsAssociatedFunction Self "traverse_by" traverse_by.
    
    (*
        pub fn reachable_from(&self, block_id: BlockId) -> Vec<BlockId> {
            self.traverse_by(block_id)
        }
    *)
    Definition reachable_from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; block_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let block_id := M.alloc (| block_id |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_binary_format::control_flow_graph::VMControlFlowGraph",
              "traverse_by",
              []
            |),
            [ M.read (| self |); M.read (| block_id |) ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_reachable_from :
      M.IsAssociatedFunction Self "reachable_from" reachable_from.
  End Impl_move_binary_format_control_flow_graph_VMControlFlowGraph.
  
  Module Impl_move_binary_format_control_flow_graph_ControlFlowGraph_for_move_binary_format_control_flow_graph_VMControlFlowGraph.
    Definition Self : Ty.t := Ty.path "move_binary_format::control_flow_graph::VMControlFlowGraph".
    
    (*
        fn block_start(&self, block_id: BlockId) -> CodeOffset {
            block_id
        }
    *)
    Definition block_start (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; block_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let block_id := M.alloc (| block_id |) in
          M.read (| block_id |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn block_end(&self, block_id: BlockId) -> CodeOffset {
            self.blocks[&block_id].exit
        }
    *)
    Definition block_end (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; block_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let block_id := M.alloc (| block_id |) in
          M.read (|
            M.SubPointer.get_struct_record_field (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::index::Index",
                  Ty.apply
                    (Ty.path "alloc::collections::btree::map::BTreeMap")
                    []
                    [
                      Ty.path "u16";
                      Ty.path "move_binary_format::control_flow_graph::BasicBlock";
                      Ty.path "alloc::alloc::Global"
                    ],
                  [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ],
                  "index",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_binary_format::control_flow_graph::VMControlFlowGraph",
                    "blocks"
                  |);
                  block_id
                ]
              |),
              "move_binary_format::control_flow_graph::BasicBlock",
              "exit"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn successors(&self, block_id: BlockId) -> &Vec<BlockId> {
            &self.blocks[&block_id].successors
        }
    *)
    Definition successors (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; block_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let block_id := M.alloc (| block_id |) in
          M.SubPointer.get_struct_record_field (|
            M.call_closure (|
              M.get_trait_method (|
                "core::ops::index::Index",
                Ty.apply
                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                  []
                  [
                    Ty.path "u16";
                    Ty.path "move_binary_format::control_flow_graph::BasicBlock";
                    Ty.path "alloc::alloc::Global"
                  ],
                [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ],
                "index",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_binary_format::control_flow_graph::VMControlFlowGraph",
                  "blocks"
                |);
                block_id
              ]
            |),
            "move_binary_format::control_flow_graph::BasicBlock",
            "successors"
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn next_block(&self, block_id: BlockId) -> Option<CodeOffset> {
            debug_assert!(self.blocks.contains_key(&block_id));
            self.traversal_successors.get(&block_id).copied()
        }
    *)
    Definition next_block (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; block_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let block_id := M.alloc (| block_id |) 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 [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      UnOp.not (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::collections::btree::map::BTreeMap")
                                              []
                                              [
                                                Ty.path "u16";
                                                Ty.path
                                                  "move_binary_format::control_flow_graph::BasicBlock";
                                                Ty.path "alloc::alloc::Global"
                                              ],
                                            "contains_key",
                                            [ Ty.path "u16" ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_binary_format::control_flow_graph::VMControlFlowGraph",
                                              "blocks"
                                            |);
                                            block_id
                                          ]
                                        |)
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.call_closure (|
                                      M.get_function (| "core::panicking::panic", [] |),
                                      [
                                        M.read (|
                                          Value.String
                                            "assertion failed: self.blocks.contains_key(&block_id)"
                                        |)
                                      ]
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.apply (Ty.path "&") [] [ Ty.path "u16" ] ],
                  "copied",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::collections::btree::map::BTreeMap")
                        []
                        [ Ty.path "u16"; Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                      "get",
                      [ Ty.path "u16" ]
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::control_flow_graph::VMControlFlowGraph",
                        "traversal_successors"
                      |);
                      block_id
                    ]
                  |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn instr_indexes(&self, block_id: BlockId) -> Box<dyn Iterator<Item = CodeOffset>> {
            Box::new(self.block_start(block_id)..=self.block_end(block_id))
        }
    *)
    Definition instr_indexes (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; block_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let block_id := M.alloc (| block_id |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [
                  Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "u16" ];
                  Ty.path "alloc::alloc::Global"
                ],
              "new",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::ops::range::RangeInclusive") [] [ Ty.path "u16" ],
                  "new",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "move_binary_format::control_flow_graph::ControlFlowGraph",
                      Ty.path "move_binary_format::control_flow_graph::VMControlFlowGraph",
                      [],
                      "block_start",
                      []
                    |),
                    [ M.read (| self |); M.read (| block_id |) ]
                  |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "move_binary_format::control_flow_graph::ControlFlowGraph",
                      Ty.path "move_binary_format::control_flow_graph::VMControlFlowGraph",
                      [],
                      "block_end",
                      []
                    |),
                    [ M.read (| self |); M.read (| block_id |) ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn blocks(&self) -> Vec<BlockId> {
            self.blocks.keys().cloned().collect()
        }
    *)
    Definition blocks (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply
                (Ty.path "core::iter::adapters::cloned::Cloned")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::collections::btree::map::Keys")
                    []
                    [ Ty.path "u16"; Ty.path "move_binary_format::control_flow_graph::BasicBlock" ]
                ],
              [],
              "collect",
              [
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]
              ]
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply
                    (Ty.path "alloc::collections::btree::map::Keys")
                    []
                    [ Ty.path "u16"; Ty.path "move_binary_format::control_flow_graph::BasicBlock" ],
                  [],
                  "cloned",
                  [ Ty.path "u16" ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::collections::btree::map::BTreeMap")
                        []
                        [
                          Ty.path "u16";
                          Ty.path "move_binary_format::control_flow_graph::BasicBlock";
                          Ty.path "alloc::alloc::Global"
                        ],
                      "keys",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_binary_format::control_flow_graph::VMControlFlowGraph",
                        "blocks"
                      |)
                    ]
                  |)
                ]
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn num_blocks(&self) -> u16 {
            self.blocks.len() as u16
        }
    *)
    Definition num_blocks (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.rust_cast
            (M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                  []
                  [
                    Ty.path "u16";
                    Ty.path "move_binary_format::control_flow_graph::BasicBlock";
                    Ty.path "alloc::alloc::Global"
                  ],
                "len",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_binary_format::control_flow_graph::VMControlFlowGraph",
                  "blocks"
                |)
              ]
            |))))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn entry_block_id(&self) -> BlockId {
            ENTRY_BLOCK_ID
        }
    *)
    Definition entry_block_id (ε : 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.get_constant (| "move_binary_format::control_flow_graph::ENTRY_BLOCK_ID" |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn is_loop_head(&self, block_id: BlockId) -> bool {
            self.loop_heads.contains_key(&block_id)
        }
    *)
    Definition is_loop_head (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; block_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let block_id := M.alloc (| block_id |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "alloc::collections::btree::map::BTreeMap")
                []
                [
                  Ty.path "u16";
                  Ty.apply
                    (Ty.path "alloc::collections::btree::set::BTreeSet")
                    []
                    [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ];
                  Ty.path "alloc::alloc::Global"
                ],
              "contains_key",
              [ Ty.path "u16" ]
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_binary_format::control_flow_graph::VMControlFlowGraph",
                "loop_heads"
              |);
              block_id
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn is_back_edge(&self, cur: BlockId, next: BlockId) -> bool {
            self.loop_heads
                .get(&next)
                .map_or(false, |back_edges| back_edges.contains(&cur))
        }
    *)
    Definition is_back_edge (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; cur; next ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let cur := M.alloc (| cur |) in
          let next := M.alloc (| next |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.apply
                    (Ty.path "&")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::collections::btree::set::BTreeSet")
                        []
                        [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]
                    ]
                ],
              "map_or",
              [
                Ty.path "bool";
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::collections::btree::set::BTreeSet")
                              []
                              [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]
                          ]
                      ]
                  ]
                  (Ty.path "bool")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::collections::btree::map::BTreeMap")
                    []
                    [
                      Ty.path "u16";
                      Ty.apply
                        (Ty.path "alloc::collections::btree::set::BTreeSet")
                        []
                        [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  "get",
                  [ Ty.path "u16" ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_binary_format::control_flow_graph::VMControlFlowGraph",
                    "loop_heads"
                  |);
                  next
                ]
              |);
              Value.Bool false;
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let back_edges := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::collections::btree::set::BTreeSet")
                                      []
                                      [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                    "contains",
                                    [ Ty.path "u16" ]
                                  |),
                                  [ M.read (| back_edges |); cur ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn num_back_edges(&self) -> usize {
            self.loop_heads
                .iter()
                .fold(0, |acc, (_, edges)| acc + edges.len())
        }
    *)
    Definition num_back_edges (ε : 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 "alloc::collections::btree::map::Iter")
                []
                [
                  Ty.path "u16";
                  Ty.apply
                    (Ty.path "alloc::collections::btree::set::BTreeSet")
                    []
                    [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]
                ],
              [],
              "fold",
              [
                Ty.path "usize";
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.path "usize";
                        Ty.tuple
                          [
                            Ty.apply (Ty.path "&") [] [ Ty.path "u16" ];
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::collections::btree::set::BTreeSet")
                                  []
                                  [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ]
                              ]
                          ]
                      ]
                  ]
                  (Ty.path "usize")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::collections::btree::map::BTreeMap")
                    []
                    [
                      Ty.path "u16";
                      Ty.apply
                        (Ty.path "alloc::collections::btree::set::BTreeSet")
                        []
                        [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  "iter",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_binary_format::control_flow_graph::VMControlFlowGraph",
                    "loop_heads"
                  |)
                ]
              |);
              Value.Integer IntegerKind.Usize 0;
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0; α1 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let acc := M.copy (| γ |) in
                                M.match_operator (|
                                  M.alloc (| α1 |),
                                  [
                                    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 edges := M.copy (| γ0_1 |) in
                                        BinOp.Wrap.add (|
                                          M.read (| acc |),
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::collections::btree::set::BTreeSet")
                                                []
                                                [ Ty.path "u16"; Ty.path "alloc::alloc::Global" ],
                                              "len",
                                              []
                                            |),
                                            [ M.read (| edges |) ]
                                          |)
                                        |)))
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "move_binary_format::control_flow_graph::ControlFlowGraph"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("block_start", InstanceField.Method block_start);
          ("block_end", InstanceField.Method block_end);
          ("successors", InstanceField.Method successors);
          ("next_block", InstanceField.Method next_block);
          ("instr_indexes", InstanceField.Method instr_indexes);
          ("blocks", InstanceField.Method blocks);
          ("num_blocks", InstanceField.Method num_blocks);
          ("entry_block_id", InstanceField.Method entry_block_id);
          ("is_loop_head", InstanceField.Method is_loop_head);
          ("is_back_edge", InstanceField.Method is_back_edge);
          ("num_back_edges", InstanceField.Method num_back_edges)
        ].
  End Impl_move_binary_format_control_flow_graph_ControlFlowGraph_for_move_binary_format_control_flow_graph_VMControlFlowGraph.
End control_flow_graph.
