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

(* StructRecord
  {
    name := "AbstractStack";
    const_params := [];
    ty_params := [ "T" ];
    fields :=
      [
        ("values",
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [ Ty.tuple [ Ty.path "u64"; T ]; Ty.path "alloc::alloc::Global" ]);
        ("len", Ty.path "u64")
      ];
  } *)

Module Impl_core_default_Default_where_core_default_Default_T_for_move_abstract_stack_AbstractStack_T.
  Definition Self (T : Ty.t) : Ty.t :=
    Ty.apply (Ty.path "move_abstract_stack::AbstractStack") [] [ T ].
  
  (* Default *)
  Definition default (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "move_abstract_stack::AbstractStack"
          [
            ("values",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.tuple [ Ty.path "u64"; T ]; Ty.path "alloc::alloc::Global" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("len",
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", Ty.path "u64", [], "default", [] |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "core::default::Default"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method (default T)) ].
End Impl_core_default_Default_where_core_default_Default_T_for_move_abstract_stack_AbstractStack_T.

Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_move_abstract_stack_AbstractStack_T.
  Definition Self (T : Ty.t) : Ty.t :=
    Ty.apply (Ty.path "move_abstract_stack::AbstractStack") [] [ T ].
  
  (* Debug *)
  Definition fmt (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "core::fmt::Formatter",
            "debug_struct_field2_finish",
            []
          |),
          [
            M.read (| f |);
            M.read (| Value.String "AbstractStack" |);
            M.read (| Value.String "values" |);
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "move_abstract_stack::AbstractStack",
              "values"
            |);
            M.read (| Value.String "len" |);
            M.alloc (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "move_abstract_stack::AbstractStack",
                "len"
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (T : Ty.t),
    M.IsTraitInstance
      "core::fmt::Debug"
      (Self T)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
End Impl_core_fmt_Debug_where_core_fmt_Debug_T_for_move_abstract_stack_AbstractStack_T.

Module Impl_move_abstract_stack_AbstractStack_T.
  Definition Self (T : Ty.t) : Ty.t :=
    Ty.apply (Ty.path "move_abstract_stack::AbstractStack") [] [ T ].
  
  (*
      pub fn new() -> Self {
          Self {
              values: vec![],
              len: 0,
          }
      }
  *)
  Definition new (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "move_abstract_stack::AbstractStack"
          [
            ("values",
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.tuple [ Ty.path "u64"; T ]; Ty.path "alloc::alloc::Global" ],
                  "new",
                  []
                |),
                []
              |));
            ("len", Value.Integer IntegerKind.U64 0)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "new" (new T).
  
  (*
      pub fn is_empty(&self) -> bool {
          // empty ==> len is 0
          debug_assert!(!self.values.is_empty() || self.len == 0);
          // !empty ==> last element len <= len
          debug_assert!(self.values.is_empty() || self.values.last().unwrap().0 <= self.len);
          self.values.is_empty()
      }
  *)
  Definition is_empty (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) 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 (|
                                      LogicalOp.or (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.tuple [ Ty.path "u64"; T ];
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "is_empty",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "move_abstract_stack::AbstractStack",
                                                "values"
                                              |)
                                            ]
                                          |)
                                        |),
                                        ltac:(M.monadic
                                          (BinOp.eq (|
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "move_abstract_stack::AbstractStack",
                                                "len"
                                              |)
                                            |),
                                            Value.Integer IntegerKind.U64 0
                                          |)))
                                      |)
                                    |)
                                  |)) 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.values.is_empty() || self.len == 0"
                                      |)
                                    ]
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use (M.alloc (| 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 (|
                                      LogicalOp.or (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::vec::Vec")
                                              []
                                              [
                                                Ty.tuple [ Ty.path "u64"; T ];
                                                Ty.path "alloc::alloc::Global"
                                              ],
                                            "is_empty",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_abstract_stack::AbstractStack",
                                              "values"
                                            |)
                                          ]
                                        |),
                                        ltac:(M.monadic
                                          (BinOp.le (|
                                            M.read (|
                                              M.SubPointer.get_tuple_field (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "core::option::Option")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "&")
                                                          []
                                                          [ Ty.tuple [ Ty.path "u64"; T ] ]
                                                      ],
                                                    "unwrap",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "slice")
                                                          []
                                                          [ Ty.tuple [ Ty.path "u64"; T ] ],
                                                        "last",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::deref::Deref",
                                                            Ty.apply
                                                              (Ty.path "alloc::vec::Vec")
                                                              []
                                                              [
                                                                Ty.tuple [ Ty.path "u64"; T ];
                                                                Ty.path "alloc::alloc::Global"
                                                              ],
                                                            [],
                                                            "deref",
                                                            []
                                                          |),
                                                          [
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "move_abstract_stack::AbstractStack",
                                                              "values"
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |),
                                                0
                                              |)
                                            |),
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "move_abstract_stack::AbstractStack",
                                                "len"
                                              |)
                                            |)
                                          |)))
                                      |)
                                    |)
                                  |)) 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.values.is_empty() || self.values.last().unwrap().0 <= self.len"
                                      |)
                                    ]
                                  |)
                                |)
                              |)));
                          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 "alloc::vec::Vec")
                  []
                  [ Ty.tuple [ Ty.path "u64"; T ]; Ty.path "alloc::alloc::Global" ],
                "is_empty",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "move_abstract_stack::AbstractStack",
                  "values"
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_is_empty :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "is_empty" (is_empty T).
  
  (*
      pub fn len(&self) -> u64 {
          // len is 0 ==> empty
          debug_assert!(self.len != 0 || self.values.is_empty());
          // len not 0 ==> !empty and last element len <= len
          debug_assert!(
              self.len == 0 || (!self.values.is_empty() && self.values.last().unwrap().0 <= self.len)
          );
          self.len
      }
  *)
  Definition len (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) 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 (|
                                      LogicalOp.or (|
                                        BinOp.ne (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_abstract_stack::AbstractStack",
                                              "len"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U64 0
                                        |),
                                        ltac:(M.monadic
                                          (M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.tuple [ Ty.path "u64"; T ];
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "is_empty",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "move_abstract_stack::AbstractStack",
                                                "values"
                                              |)
                                            ]
                                          |)))
                                      |)
                                    |)
                                  |)) 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.len != 0 || self.values.is_empty()"
                                      |)
                                    ]
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use (M.alloc (| 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 (|
                                      LogicalOp.or (|
                                        BinOp.eq (|
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_abstract_stack::AbstractStack",
                                              "len"
                                            |)
                                          |),
                                          Value.Integer IntegerKind.U64 0
                                        |),
                                        ltac:(M.monadic
                                          (LogicalOp.and (|
                                            UnOp.not (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.tuple [ Ty.path "u64"; T ];
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "is_empty",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "move_abstract_stack::AbstractStack",
                                                    "values"
                                                  |)
                                                ]
                                              |)
                                            |),
                                            ltac:(M.monadic
                                              (BinOp.le (|
                                                M.read (|
                                                  M.SubPointer.get_tuple_field (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "core::option::Option")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [ Ty.tuple [ Ty.path "u64"; T ] ]
                                                          ],
                                                        "unwrap",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.tuple [ Ty.path "u64"; T ] ],
                                                            "last",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::deref::Deref",
                                                                Ty.apply
                                                                  (Ty.path "alloc::vec::Vec")
                                                                  []
                                                                  [
                                                                    Ty.tuple [ Ty.path "u64"; T ];
                                                                    Ty.path "alloc::alloc::Global"
                                                                  ],
                                                                [],
                                                                "deref",
                                                                []
                                                              |),
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "move_abstract_stack::AbstractStack",
                                                                  "values"
                                                                |)
                                                              ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |),
                                                    0
                                                  |)
                                                |),
                                                M.read (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "move_abstract_stack::AbstractStack",
                                                    "len"
                                                  |)
                                                |)
                                              |)))
                                          |)))
                                      |)
                                    |)
                                  |)) 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.len == 0 ||
    (!self.values.is_empty() && self.values.last().unwrap().0 <= self.len)"
                                      |)
                                    ]
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.SubPointer.get_struct_record_field (|
            M.read (| self |),
            "move_abstract_stack::AbstractStack",
            "len"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_len : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "len" (len T).
  
  (*
      pub fn push(&mut self, item: T) -> Result<(), AbsStackError> {
          self.push_n(item, 1)
      }
  *)
  Definition push (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; item ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let item := M.alloc (| item |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "move_abstract_stack::AbstractStack") [] [ T ],
            "push_n",
            []
          |),
          [ M.read (| self |); M.read (| item |); Value.Integer IntegerKind.U64 1 ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_push :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "push" (push T).
  
  (*
      pub fn push_n(&mut self, item: T, n: u64) -> Result<(), AbsStackError> {
          if n == 0 {
              return Ok(());
          }
  
          let Some(new_len) = self.len.checked_add(n) else {
              return Err(AbsStackError::Overflow);
          };
          self.len = new_len;
          match self.values.last_mut() {
              Some((count, last_item)) if &item == last_item => {
                  debug_assert!( *count > 0);
                  *count += n
              }
              _ => self.values.push((n, item)),
          }
          Ok(())
      }
  *)
  Definition push_n (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; item; n ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let item := M.alloc (| item |) in
        let n := M.alloc (| n |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.eq (| M.read (| n |), Value.Integer IntegerKind.U64 0 |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "u64", "checked_add", [] |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "move_abstract_stack::AbstractStack",
                          "len"
                        |)
                      |);
                      M.read (| n |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let new_len := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.write (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_abstract_stack::AbstractStack",
                            "len"
                          |),
                          M.read (| new_len |)
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply (Ty.path "slice") [] [ Ty.tuple [ Ty.path "u64"; T ] ],
                                "last_mut",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::deref::DerefMut",
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.tuple [ Ty.path "u64"; T ];
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    [],
                                    "deref_mut",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_abstract_stack::AbstractStack",
                                      "values"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            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 γ2_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                let γ2_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                let count := M.alloc (| γ2_0 |) in
                                let last_item := M.alloc (| γ2_1 |) in
                                let γ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply (Ty.path "&") [] [ T ],
                                        [ Ty.apply (Ty.path "&mut") [] [ T ] ],
                                        "eq",
                                        []
                                      |),
                                      [ M.alloc (| item |); last_item ]
                                    |)
                                  |) 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 (| 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.gt (|
                                                              M.read (| M.read (| count |) |),
                                                              Value.Integer IntegerKind.U64 0
                                                            |)
                                                          |)
                                                        |)) 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: *count > 0"
                                                            |)
                                                          ]
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                let β := M.read (| count |) in
                                M.write (|
                                  β,
                                  BinOp.Wrap.add (| M.read (| β |), M.read (| n |) |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.tuple [ Ty.path "u64"; T ];
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "push",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_abstract_stack::AbstractStack",
                                        "values"
                                      |);
                                      Value.Tuple [ M.read (| n |); M.read (| item |) ]
                                    ]
                                  |)
                                |)))
                          ]
                        |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                      |)))
                ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_push_n :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "push_n" (push_n T).
  
  (*
      pub fn pop(&mut self) -> Result<T, AbsStackError> {
          self.pop_eq_n(NonZeroU64::new(1).unwrap())
      }
  *)
  Definition pop (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "move_abstract_stack::AbstractStack") [] [ T ],
            "pop_eq_n",
            []
          |),
          [
            M.read (| self |);
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u64" ] ],
                "unwrap",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u64" ],
                    "new",
                    []
                  |),
                  [ Value.Integer IntegerKind.U64 1 ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_pop : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "pop" (pop T).
  
  (*
      pub fn pop_eq_n(&mut self, n: NonZeroU64) -> Result<T, AbsStackError> {
          let n: u64 = n.get();
          if self.is_empty() || n > self.len {
              return Err(AbsStackError::Underflow);
          }
          let (count, last) = self.values.last_mut().unwrap();
          debug_assert!( *count > 0);
          let ret = match ( *count).cmp(&n) {
              Ordering::Less => return Err(AbsStackError::ElementNotEqual),
              Ordering::Equal => {
                  let (_, last) = self.values.pop().unwrap();
                  last
              }
              Ordering::Greater => {
                  *count -= n;
                  last.clone()
              }
          };
          self.len -= n;
          Ok(ret)
      }
  *)
  Definition pop_eq_n (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; n ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let n := M.alloc (| n |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ n :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u64" ],
                      "get",
                      []
                    |),
                    [ M.read (| n |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              LogicalOp.or (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "move_abstract_stack::AbstractStack")
                                      []
                                      [ T ],
                                    "is_empty",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |),
                                ltac:(M.monadic
                                  (BinOp.gt (|
                                    M.read (| n |),
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_abstract_stack::AbstractStack",
                                        "len"
                                      |)
                                    |)
                                  |)))
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [
                                    Value.StructTuple
                                      "move_abstract_stack::AbsStackError::Underflow"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.apply (Ty.path "&mut") [] [ Ty.tuple [ Ty.path "u64"; T ] ] ],
                      "unwrap",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.tuple [ Ty.path "u64"; T ] ],
                          "last_mut",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::DerefMut",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [ Ty.tuple [ Ty.path "u64"; T ]; Ty.path "alloc::alloc::Global" ],
                              [],
                              "deref_mut",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "move_abstract_stack::AbstractStack",
                                "values"
                              |)
                            ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ1_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let count := M.alloc (| γ1_0 |) in
                      let last := M.alloc (| γ1_1 |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                let~ _ :=
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                UnOp.not (|
                                                  BinOp.gt (|
                                                    M.read (| M.read (| count |) |),
                                                    Value.Integer IntegerKind.U64 0
                                                  |)
                                                |)
                                              |)) 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: *count > 0"
                                                  |)
                                                ]
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ ret :=
                        M.copy (|
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::Ord",
                                  Ty.path "u64",
                                  [],
                                  "cmp",
                                  []
                                |),
                                [ M.read (| count |); n ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructTuple
                                                "move_abstract_stack::AbsStackError::ElementNotEqual"
                                                []
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.tuple [ Ty.path "u64"; T ] ],
                                          "unwrap",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.tuple [ Ty.path "u64"; T ];
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "pop",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "move_abstract_stack::AbstractStack",
                                                "values"
                                              |)
                                            ]
                                          |)
                                        ]
                                      |)
                                    |),
                                    [
                                      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 last := M.copy (| γ0_1 |) in
                                          last))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                                  let~ _ :=
                                    let β := M.read (| count |) in
                                    M.write (|
                                      β,
                                      BinOp.Wrap.sub (| M.read (| β |), M.read (| n |) |)
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::clone::Clone",
                                        T,
                                        [],
                                        "clone",
                                        []
                                      |),
                                      [ M.read (| last |) ]
                                    |)
                                  |)))
                            ]
                          |)
                        |) in
                      let~ _ :=
                        let β :=
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "move_abstract_stack::AbstractStack",
                            "len"
                          |) in
                        M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| n |) |) |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ M.read (| ret |) ]
                      |)))
                ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_pop_eq_n :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "pop_eq_n" (pop_eq_n T).
  
  (*
      pub fn pop_any_n(&mut self, n: NonZeroU64) -> Result<(), AbsStackError> {
          let n: u64 = n.get();
          if self.is_empty() || n > self.len {
              return Err(AbsStackError::Underflow);
          }
          let mut rem: u64 = n;
          while rem > 0 {
              let (count, _last) = self.values.last_mut().unwrap();
              debug_assert!( *count > 0);
              match ( *count).cmp(&rem) {
                  Ordering::Less | Ordering::Equal => {
                      rem -= *count;
                      self.values.pop().unwrap();
                  }
                  Ordering::Greater => {
                      *count -= rem;
                      break;
                  }
              }
          }
          self.len -= n;
          Ok(())
      }
  *)
  Definition pop_any_n (T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self T in
    match ε, τ, α with
    | [], [], [ self; n ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let n := M.alloc (| n |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ n :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "core::num::nonzero::NonZero") [] [ Ty.path "u64" ],
                      "get",
                      []
                    |),
                    [ M.read (| n |) ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              LogicalOp.or (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "move_abstract_stack::AbstractStack")
                                      []
                                      [ T ],
                                    "is_empty",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |),
                                ltac:(M.monadic
                                  (BinOp.gt (|
                                    M.read (| n |),
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "move_abstract_stack::AbstractStack",
                                        "len"
                                      |)
                                    |)
                                  |)))
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [
                                    Value.StructTuple
                                      "move_abstract_stack::AbsStackError::Underflow"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ rem := M.copy (| n |) in
              let~ _ :=
                M.loop (|
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.gt (| M.read (| rem |), Value.Integer IntegerKind.U64 0 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "&mut")
                                          []
                                          [ Ty.tuple [ Ty.path "u64"; T ] ]
                                      ],
                                    "unwrap",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "slice")
                                          []
                                          [ Ty.tuple [ Ty.path "u64"; T ] ],
                                        "last_mut",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::deref::DerefMut",
                                            Ty.apply
                                              (Ty.path "alloc::vec::Vec")
                                              []
                                              [
                                                Ty.tuple [ Ty.path "u64"; T ];
                                                Ty.path "alloc::alloc::Global"
                                              ],
                                            [],
                                            "deref_mut",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "move_abstract_stack::AbstractStack",
                                              "values"
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ := M.read (| γ |) in
                                    let γ1_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                    let γ1_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                    let count := M.alloc (| γ1_0 |) in
                                    let _last := M.alloc (| γ1_1 |) in
                                    let~ _ :=
                                      M.match_operator (|
                                        M.alloc (| Value.Tuple [] |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ := M.use (M.alloc (| Value.Bool true |)) in
                                              let _ :=
                                                M.is_constant_or_break_match (|
                                                  M.read (| γ |),
                                                  Value.Bool true
                                                |) in
                                              let~ _ :=
                                                M.match_operator (|
                                                  M.alloc (| Value.Tuple [] |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ :=
                                                          M.use
                                                            (M.alloc (|
                                                              UnOp.not (|
                                                                BinOp.gt (|
                                                                  M.read (| M.read (| count |) |),
                                                                  Value.Integer IntegerKind.U64 0
                                                                |)
                                                              |)
                                                            |)) 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: *count > 0"
                                                                |)
                                                              ]
                                                            |)
                                                          |)
                                                        |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |) in
                                              M.alloc (| Value.Tuple [] |)));
                                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::cmp::Ord",
                                            Ty.path "u64",
                                            [],
                                            "cmp",
                                            []
                                          |),
                                          [ M.read (| count |); rem ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.find_or_pattern (|
                                              γ,
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let _ :=
                                                      M.is_struct_tuple (|
                                                        γ,
                                                        "core::cmp::Ordering::Less"
                                                      |) in
                                                    Value.Tuple []));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let _ :=
                                                      M.is_struct_tuple (|
                                                        γ,
                                                        "core::cmp::Ordering::Equal"
                                                      |) in
                                                    Value.Tuple []))
                                              ],
                                              M.closure
                                                (fun γ =>
                                                  ltac:(M.monadic
                                                    match γ with
                                                    | [] =>
                                                      ltac:(M.monadic
                                                        (let~ _ :=
                                                          let β := rem in
                                                          M.write (|
                                                            β,
                                                            BinOp.Wrap.sub (|
                                                              M.read (| β |),
                                                              M.read (| M.read (| count |) |)
                                                            |)
                                                          |) in
                                                        let~ _ :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "core::option::Option")
                                                                  []
                                                                  [ Ty.tuple [ Ty.path "u64"; T ] ],
                                                                "unwrap",
                                                                []
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path "alloc::vec::Vec")
                                                                      []
                                                                      [
                                                                        Ty.tuple
                                                                          [ Ty.path "u64"; T ];
                                                                        Ty.path
                                                                          "alloc::alloc::Global"
                                                                      ],
                                                                    "pop",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| self |),
                                                                      "move_abstract_stack::AbstractStack",
                                                                      "values"
                                                                    |)
                                                                  ]
                                                                |)
                                                              ]
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)))
                                                    | _ => M.impossible "wrong number of arguments"
                                                    end))
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::cmp::Ordering::Greater"
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  let~ _ :=
                                                    let β := M.read (| count |) in
                                                    M.write (|
                                                      β,
                                                      BinOp.Wrap.sub (|
                                                        M.read (| β |),
                                                        M.read (| rem |)
                                                      |)
                                                    |) in
                                                  M.break (||)
                                                |)
                                              |)
                                            |)))
                                      ]
                                    |)))
                              ]
                            |)));
                        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~ _ :=
                let β :=
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "move_abstract_stack::AbstractStack",
                    "len"
                  |) in
                M.write (| β, BinOp.Wrap.sub (| M.read (| β |), M.read (| n |) |) |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_pop_any_n :
    forall (T : Ty.t),
    M.IsAssociatedFunction (Self T) "pop_any_n" (pop_any_n T).
End Impl_move_abstract_stack_AbstractStack_T.

(*
Enum AbsStackError
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "ElementNotEqual";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Underflow";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "Overflow";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_cmp_Eq_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  (* Eq *)
  Definition assert_receiver_is_total_eq
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        Value.Tuple []))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Eq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
End Impl_core_cmp_Eq_for_move_abstract_stack_AbsStackError.

Module Impl_core_marker_StructuralPartialEq_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_move_abstract_stack_AbsStackError.

Module Impl_core_cmp_PartialEq_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  (* PartialEq *)
  Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_abstract_stack::AbsStackError" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_abstract_stack::AbsStackError" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_move_abstract_stack_AbsStackError.

Module Impl_core_cmp_PartialOrd_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  (* PartialOrd *)
  Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_abstract_stack::AbsStackError" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_abstract_stack::AbsStackError" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialOrd",
                Ty.path "isize",
                [ Ty.path "isize" ],
                "partial_cmp",
                []
              |),
              [ __self_discr; __arg1_discr ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialOrd"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
End Impl_core_cmp_PartialOrd_for_move_abstract_stack_AbsStackError.

Module Impl_core_cmp_Ord_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  (* Ord *)
  Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_abstract_stack::AbsStackError" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "move_abstract_stack::AbsStackError" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
              [ __self_discr; __arg1_discr ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Ord"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
End Impl_core_cmp_Ord_for_move_abstract_stack_AbsStackError.

Module Impl_core_clone_Clone_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  (* Clone *)
  Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (| M.read (| self |) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_move_abstract_stack_AbsStackError.

Module Impl_core_marker_Copy_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_move_abstract_stack_AbsStackError.

Module Impl_core_fmt_Debug_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  (* Debug *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
          [
            M.read (| f |);
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_abstract_stack::AbsStackError::ElementNotEqual"
                        |) in
                      M.alloc (| M.read (| Value.String "ElementNotEqual" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "move_abstract_stack::AbsStackError::Underflow"
                        |) in
                      M.alloc (| M.read (| Value.String "Underflow" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "move_abstract_stack::AbsStackError::Overflow" |) in
                      M.alloc (| M.read (| Value.String "Overflow" |) |)))
                ]
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_move_abstract_stack_AbsStackError.

Module Impl_core_fmt_Display_for_move_abstract_stack_AbsStackError.
  Definition Self : Ty.t := Ty.path "move_abstract_stack::AbsStackError".
  
  (*
      fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
          match self {
              AbsStackError::ElementNotEqual => {
                  write!(f, "Popped element is not equal to specified item")
              }
              AbsStackError::Underflow => {
                  write!(f, "Popped more values than are on the stack")
              }
              AbsStackError::Overflow => {
                  write!(f, "Pushed too many elements on the stack")
              }
          }
      }
  *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.read (|
          M.match_operator (|
            self,
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ :=
                    M.is_struct_tuple (|
                      γ,
                      "move_abstract_stack::AbsStackError::ElementNotEqual"
                    |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Formatter",
                        "write_fmt",
                        []
                      |),
                      [
                        M.read (| f |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Arguments",
                            "new_const",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (|
                                    Value.String "Popped element is not equal to specified item"
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ :=
                    M.is_struct_tuple (| γ, "move_abstract_stack::AbsStackError::Underflow" |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Formatter",
                        "write_fmt",
                        []
                      |),
                      [
                        M.read (| f |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Arguments",
                            "new_const",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (|
                                    Value.String "Popped more values than are on the stack"
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.read (| γ |) in
                  let _ :=
                    M.is_struct_tuple (| γ, "move_abstract_stack::AbsStackError::Overflow" |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Formatter",
                        "write_fmt",
                        []
                      |),
                      [
                        M.read (| f |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Arguments",
                            "new_const",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [ M.read (| Value.String "Pushed too many elements on the stack" |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Display"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Display_for_move_abstract_stack_AbsStackError.
