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

Module interpreter.
  Module stack.
    Definition value_STACK_LIMIT : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 1024 |))).
    
    (* StructRecord
      {
        name := "Stack";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("data",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [];
                  Ty.path "alloc::alloc::Global"
                ])
          ];
      } *)
    
    Module Impl_core_fmt_Debug_for_revm_interpreter_interpreter_stack_Stack.
      Definition Self : Ty.t := Ty.path "revm_interpreter::interpreter::stack::Stack".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "Stack" |);
                M.read (| Value.String "data" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_interpreter::interpreter::stack::Stack",
                    "data"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_revm_interpreter_interpreter_stack_Stack.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_interpreter_interpreter_stack_Stack.
      Definition Self : Ty.t := Ty.path "revm_interpreter::interpreter::stack::Stack".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_interpreter_interpreter_stack_Stack.
    
    Module Impl_core_cmp_PartialEq_for_revm_interpreter_interpreter_stack_Stack.
      Definition Self : Ty.t := Ty.path "revm_interpreter::interpreter::stack::Stack".
      
      (* 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.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [];
                    Ty.path "alloc::alloc::Global"
                  ],
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [];
                      Ty.path "alloc::alloc::Global"
                    ]
                ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::interpreter::stack::Stack",
                  "data"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "revm_interpreter::interpreter::stack::Stack",
                  "data"
                |)
              ]
            |)))
        | _, _, _ => 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_revm_interpreter_interpreter_stack_Stack.
    
    Module Impl_core_cmp_Eq_for_revm_interpreter_interpreter_stack_Stack.
      Definition Self : Ty.t := Ty.path "revm_interpreter::interpreter::stack::Stack".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_revm_interpreter_interpreter_stack_Stack.
    
    Module Impl_core_hash_Hash_for_revm_interpreter_interpreter_stack_Stack.
      Definition Self : Ty.t := Ty.path "revm_interpreter::interpreter::stack::Stack".
      
      (* Hash *)
      Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ __H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::hash::Hash",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [];
                    Ty.path "alloc::alloc::Global"
                  ],
                [],
                "hash",
                [ __H ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::interpreter::stack::Stack",
                  "data"
                |);
                M.read (| state |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::hash::Hash"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method hash) ].
    End Impl_core_hash_Hash_for_revm_interpreter_interpreter_stack_Stack.
    
    Module Impl_core_fmt_Display_for_revm_interpreter_interpreter_stack_Stack.
      Definition Self : Ty.t := Ty.path "revm_interpreter::interpreter::stack::Stack".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              f.write_str("[")?;
              for (i, x) in self.data.iter().enumerate() {
                  if i > 0 {
                      f.write_str(", ")?;
                  }
                  write!(f, "{x}")?;
              }
              f.write_str("]")
          }
      *)
      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.catch_return (|
              ltac:(M.monadic
                (M.read (|
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Formatter",
                                "write_str",
                                []
                              |),
                              [ M.read (| f |); M.read (| Value.String "[" |) ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "core::fmt::Error"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |) in
                  let~ _ :=
                    M.use
                      (M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::iter::traits::collect::IntoIterator",
                              Ty.apply
                                (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "core::slice::iter::Iter")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        []
                                    ]
                                ],
                              [],
                              "into_iter",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply
                                    (Ty.path "core::slice::iter::Iter")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        []
                                    ],
                                  [],
                                  "enumerate",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "slice")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            []
                                        ],
                                      "iter",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::deref::Deref",
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [];
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          [],
                                          "deref",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_interpreter::interpreter::stack::Stack",
                                            "data"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                ]
                              |)
                            ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let iter := M.copy (| γ |) in
                              M.loop (|
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::iter::traits::iterator::Iterator",
                                            Ty.apply
                                              (Ty.path "core::iter::adapters::enumerate::Enumerate")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "core::slice::iter::Iter")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path "ruint::Uint")
                                                      [
                                                        Value.Integer IntegerKind.Usize 256;
                                                        Value.Integer IntegerKind.Usize 4
                                                      ]
                                                      []
                                                  ]
                                              ],
                                            [],
                                            "next",
                                            []
                                          |),
                                          [ iter ]
                                        |)
                                      |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "core::option::Option::None"
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (| M.read (| M.break (||) |) |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ0_0 :=
                                              M.SubPointer.get_struct_tuple_field (|
                                                γ,
                                                "core::option::Option::Some",
                                                0
                                              |) in
                                            let γ1_0 :=
                                              M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                            let γ1_1 :=
                                              M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                            let i := M.copy (| γ1_0 |) in
                                            let x := M.copy (| γ1_1 |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (| Value.Tuple [] |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ :=
                                                        M.use
                                                          (M.alloc (|
                                                            BinOp.gt (|
                                                              M.read (| i |),
                                                              Value.Integer IntegerKind.Usize 0
                                                            |)
                                                          |)) in
                                                      let _ :=
                                                        M.is_constant_or_break_match (|
                                                          M.read (| γ |),
                                                          Value.Bool true
                                                        |) in
                                                      let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::try_trait::Try",
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.tuple [];
                                                                    Ty.path "core::fmt::Error"
                                                                  ],
                                                                [],
                                                                "branch",
                                                                []
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path "core::fmt::Formatter",
                                                                    "write_str",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.read (| f |);
                                                                    M.read (| Value.String ", " |)
                                                                  ]
                                                                |)
                                                              ]
                                                            |)
                                                          |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ0_0 :=
                                                                  M.SubPointer.get_struct_tuple_field (|
                                                                    γ,
                                                                    "core::ops::control_flow::ControlFlow::Break",
                                                                    0
                                                                  |) in
                                                                let residual := M.copy (| γ0_0 |) in
                                                                M.alloc (|
                                                                  M.never_to_any (|
                                                                    M.read (|
                                                                      M.return_ (|
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::ops::try_trait::FromResidual",
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "core::result::Result")
                                                                              []
                                                                              [
                                                                                Ty.tuple [];
                                                                                Ty.path
                                                                                  "core::fmt::Error"
                                                                              ],
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "core::result::Result")
                                                                                []
                                                                                [
                                                                                  Ty.path
                                                                                    "core::convert::Infallible";
                                                                                  Ty.path
                                                                                    "core::fmt::Error"
                                                                                ]
                                                                            ],
                                                                            "from_residual",
                                                                            []
                                                                          |),
                                                                          [ M.read (| residual |) ]
                                                                        |)
                                                                      |)
                                                                    |)
                                                                  |)
                                                                |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ0_0 :=
                                                                  M.SubPointer.get_struct_tuple_field (|
                                                                    γ,
                                                                    "core::ops::control_flow::ControlFlow::Continue",
                                                                    0
                                                                  |) in
                                                                let val := M.copy (| γ0_0 |) in
                                                                val))
                                                          ]
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |) in
                                            let~ _ :=
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [ Ty.tuple []; Ty.path "core::fmt::Error" ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      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_v1",
                                                              []
                                                            |),
                                                            [
                                                              M.alloc (|
                                                                Value.Array
                                                                  [ M.read (| Value.String "" |) ]
                                                              |);
                                                              M.alloc (|
                                                                Value.Array
                                                                  [
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "core::fmt::rt::Argument",
                                                                        "new_display",
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "&")
                                                                            []
                                                                            [
                                                                              Ty.apply
                                                                                (Ty.path
                                                                                  "ruint::Uint")
                                                                                [
                                                                                  Value.Integer
                                                                                    IntegerKind.Usize
                                                                                    256;
                                                                                  Value.Integer
                                                                                    IntegerKind.Usize
                                                                                    4
                                                                                ]
                                                                                []
                                                                            ]
                                                                        ]
                                                                      |),
                                                                      [ x ]
                                                                    |)
                                                                  ]
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Break",
                                                          0
                                                        |) in
                                                      let residual := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::FromResidual",
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.tuple [];
                                                                      Ty.path "core::fmt::Error"
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::result::Result")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible";
                                                                        Ty.path "core::fmt::Error"
                                                                      ]
                                                                  ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |) in
                                            M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)))
                              |)))
                        ]
                      |)) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "core::fmt::Formatter",
                        "write_str",
                        []
                      |),
                      [ M.read (| f |); M.read (| Value.String "]" |) ]
                    |)
                  |)
                |)))
            |)))
        | _, _, _ => 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_revm_interpreter_interpreter_stack_Stack.
    
    Module Impl_core_default_Default_for_revm_interpreter_interpreter_stack_Stack.
      Definition Self : Ty.t := Ty.path "revm_interpreter::interpreter::stack::Stack".
      
      (*
          fn default() -> Self {
              Self::new()
          }
      *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_interpreter::interpreter::stack::Stack",
                "new",
                []
              |),
              []
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::default::Default"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method default) ].
    End Impl_core_default_Default_for_revm_interpreter_interpreter_stack_Stack.
    
    Module Impl_revm_interpreter_interpreter_stack_Stack.
      Definition Self : Ty.t := Ty.path "revm_interpreter::interpreter::stack::Stack".
      
      (*
          pub fn new() -> Self {
              Self {
                  // SAFETY: expansion functions assume that capacity is `STACK_LIMIT`.
                  data: Vec::with_capacity(STACK_LIMIT),
              }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "revm_interpreter::interpreter::stack::Stack"
              [
                ("data",
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "alloc::alloc::Global"
                        ],
                      "with_capacity",
                      []
                    |),
                    [
                      M.read (|
                        M.get_constant (| "revm_interpreter::interpreter::stack::STACK_LIMIT" |)
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub fn len(&self) -> usize {
              self.data.len()
          }
      *)
      Definition len (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [];
                    Ty.path "alloc::alloc::Global"
                  ],
                "len",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::interpreter::stack::Stack",
                  "data"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_len : M.IsAssociatedFunction Self "len" len.
      
      (*
          pub fn is_empty(&self) -> bool {
              self.data.is_empty()
          }
      *)
      Definition is_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [];
                    Ty.path "alloc::alloc::Global"
                  ],
                "is_empty",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::interpreter::stack::Stack",
                  "data"
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_empty : M.IsAssociatedFunction Self "is_empty" is_empty.
      
      (*
          pub fn data(&self) -> &Vec<U256> {
              &self.data
          }
      *)
      Definition data (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_interpreter::interpreter::stack::Stack",
              "data"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_data : M.IsAssociatedFunction Self "data" data.
      
      (*
          pub fn data_mut(&mut self) -> &mut Vec<U256> {
              &mut self.data
          }
      *)
      Definition data_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_interpreter::interpreter::stack::Stack",
              "data"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_data_mut : M.IsAssociatedFunction Self "data_mut" data_mut.
      
      (*
          pub fn into_data(self) -> Vec<U256> {
              self.data
          }
      *)
      Definition into_data (ε : 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.SubPointer.get_struct_record_field (|
                self,
                "revm_interpreter::interpreter::stack::Stack",
                "data"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_into_data : M.IsAssociatedFunction Self "into_data" into_data.
      
      (*
          pub fn pop(&mut self) -> Result<U256, InstructionResult> {
              self.data.pop().ok_or(InstructionResult::StackUnderflow)
          }
      *)
      Definition pop (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      []
                  ],
                "ok_or",
                [ Ty.path "revm_interpreter::instruction_result::InstructionResult" ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "pop",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::interpreter::stack::Stack",
                      "data"
                    |)
                  ]
                |);
                Value.StructTuple
                  "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                  []
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pop : M.IsAssociatedFunction Self "pop" pop.
      
      (*
          pub unsafe fn pop_unsafe(&mut self) -> U256 {
              self.data.pop().unwrap_unchecked()
          }
      *)
      Definition pop_unsafe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      []
                  ],
                "unwrap_unchecked",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "pop",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::interpreter::stack::Stack",
                      "data"
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pop_unsafe : M.IsAssociatedFunction Self "pop_unsafe" pop_unsafe.
      
      (*
          pub unsafe fn top_unsafe(&mut self) -> &mut U256 {
              let len = self.data.len();
              self.data.get_unchecked_mut(len - 1)
          }
      *)
      Definition top_unsafe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "alloc::alloc::Global"
                        ],
                      "len",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::interpreter::stack::Stack",
                        "data"
                      |)
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "slice")
                      []
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          []
                      ],
                    "get_unchecked_mut",
                    [ Ty.path "usize" ]
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::DerefMut",
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "alloc::alloc::Global"
                          ],
                        [],
                        "deref_mut",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::interpreter::stack::Stack",
                          "data"
                        |)
                      ]
                    |);
                    BinOp.Wrap.sub (| M.read (| len |), Value.Integer IntegerKind.Usize 1 |)
                  ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_top_unsafe : M.IsAssociatedFunction Self "top_unsafe" top_unsafe.
      
      (*
          pub unsafe fn pop_top_unsafe(&mut self) -> (U256, &mut U256) {
              let pop = self.pop_unsafe();
              let top = self.top_unsafe();
              (pop, top)
          }
      *)
      Definition pop_top_unsafe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ pop :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ top :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "top_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [ M.read (| pop |); M.read (| top |) ] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pop_top_unsafe :
        M.IsAssociatedFunction Self "pop_top_unsafe" pop_top_unsafe.
      
      (*
          pub unsafe fn pop2_unsafe(&mut self) -> (U256, U256) {
              let pop1 = self.pop_unsafe();
              let pop2 = self.pop_unsafe();
              (pop1, pop2)
          }
      *)
      Definition pop2_unsafe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ pop1 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop2 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [ M.read (| pop1 |); M.read (| pop2 |) ] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pop2_unsafe : M.IsAssociatedFunction Self "pop2_unsafe" pop2_unsafe.
      
      (*
          pub unsafe fn pop2_top_unsafe(&mut self) -> (U256, U256, &mut U256) {
              let pop1 = self.pop_unsafe();
              let pop2 = self.pop_unsafe();
              let top = self.top_unsafe();
      
              (pop1, pop2, top)
          }
      *)
      Definition pop2_top_unsafe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ pop1 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop2 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ top :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "top_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [ M.read (| pop1 |); M.read (| pop2 |); M.read (| top |) ] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pop2_top_unsafe :
        M.IsAssociatedFunction Self "pop2_top_unsafe" pop2_top_unsafe.
      
      (*
          pub unsafe fn pop3_unsafe(&mut self) -> (U256, U256, U256) {
              let pop1 = self.pop_unsafe();
              let pop2 = self.pop_unsafe();
              let pop3 = self.pop_unsafe();
      
              (pop1, pop2, pop3)
          }
      *)
      Definition pop3_unsafe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ pop1 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop2 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop3 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (| Value.Tuple [ M.read (| pop1 |); M.read (| pop2 |); M.read (| pop3 |) ] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pop3_unsafe : M.IsAssociatedFunction Self "pop3_unsafe" pop3_unsafe.
      
      (*
          pub unsafe fn pop4_unsafe(&mut self) -> (U256, U256, U256, U256) {
              let pop1 = self.pop_unsafe();
              let pop2 = self.pop_unsafe();
              let pop3 = self.pop_unsafe();
              let pop4 = self.pop_unsafe();
      
              (pop1, pop2, pop3, pop4)
          }
      *)
      Definition pop4_unsafe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ pop1 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop2 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop3 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop4 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (|
                Value.Tuple
                  [ M.read (| pop1 |); M.read (| pop2 |); M.read (| pop3 |); M.read (| pop4 |) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pop4_unsafe : M.IsAssociatedFunction Self "pop4_unsafe" pop4_unsafe.
      
      (*
          pub unsafe fn pop5_unsafe(&mut self) -> (U256, U256, U256, U256, U256) {
              let pop1 = self.pop_unsafe();
              let pop2 = self.pop_unsafe();
              let pop3 = self.pop_unsafe();
              let pop4 = self.pop_unsafe();
              let pop5 = self.pop_unsafe();
      
              (pop1, pop2, pop3, pop4, pop5)
          }
      *)
      Definition pop5_unsafe (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ pop1 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop2 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop3 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop4 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              let~ pop5 :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::stack::Stack",
                      "pop_unsafe",
                      []
                    |),
                    [ M.read (| self |) ]
                  |)
                |) in
              M.alloc (|
                Value.Tuple
                  [
                    M.read (| pop1 |);
                    M.read (| pop2 |);
                    M.read (| pop3 |);
                    M.read (| pop4 |);
                    M.read (| pop5 |)
                  ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_pop5_unsafe : M.IsAssociatedFunction Self "pop5_unsafe" pop5_unsafe.
      
      (*
          pub fn push_b256(&mut self, value: B256) -> Result<(), InstructionResult> {
              self.push(value.into())
          }
      *)
      Definition push_b256 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let value := M.alloc (| value |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_interpreter::interpreter::stack::Stack",
                "push",
                []
              |),
              [
                M.read (| self |);
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::Into",
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [],
                    [
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        []
                    ],
                    "into",
                    []
                  |),
                  [ M.read (| value |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_push_b256 : M.IsAssociatedFunction Self "push_b256" push_b256.
      
      (*
          pub fn push(&mut self, value: U256) -> Result<(), InstructionResult> {
              // Allows the compiler to optimize out the `Vec::push` capacity check.
              assume!(self.data.capacity() == STACK_LIMIT);
              if self.data.len() == STACK_LIMIT {
                  return Err(InstructionResult::StackOverflow);
              }
              self.data.push(value);
              Ok(())
          }
      *)
      Definition push (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let value := M.alloc (| value |) 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 (|
                                  UnOp.not (|
                                    BinOp.eq (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [];
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "capacity",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_interpreter::interpreter::stack::Stack",
                                            "data"
                                          |)
                                        ]
                                      |),
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::interpreter::stack::STACK_LIMIT"
                                        |)
                                      |)
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                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
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::panicking::panic_fmt",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "core::fmt::Arguments",
                                                        "new_v1",
                                                        []
                                                      |),
                                                      [
                                                        M.alloc (|
                                                          Value.Array
                                                            [
                                                              M.read (|
                                                                Value.String
                                                                  "internal error: entered unreachable code: self.data.capacity() == STACK_LIMIT"
                                                              |)
                                                            ]
                                                        |);
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::rt::Argument",
                                                              "none",
                                                              []
                                                            |),
                                                            []
                                                          |)
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::hint::unreachable_unchecked",
                                                            []
                                                          |),
                                                          []
                                                        |)
                                                      |)
                                                    |) in
                                                  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 (|
                                  BinOp.eq (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [];
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        "len",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm_interpreter::interpreter::stack::Stack",
                                          "data"
                                        |)
                                      ]
                                    |),
                                    M.read (|
                                      M.get_constant (|
                                        "revm_interpreter::interpreter::stack::STACK_LIMIT"
                                      |)
                                    |)
                                  |)
                                |)) 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
                                          "revm_interpreter::instruction_result::InstructionResult::StackOverflow"
                                          []
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [];
                              Ty.path "alloc::alloc::Global"
                            ],
                          "push",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm_interpreter::interpreter::stack::Stack",
                            "data"
                          |);
                          M.read (| value |)
                        ]
                      |)
                    |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_push : M.IsAssociatedFunction Self "push" push.
      
      (*
          pub fn peek(&self, no_from_top: usize) -> Result<U256, InstructionResult> {
              if self.data.len() > no_from_top {
                  Ok(self.data[self.data.len() - no_from_top - 1])
              } else {
                  Err(InstructionResult::StackUnderflow)
              }
          }
      *)
      Definition peek (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; no_from_top ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let no_from_top := M.alloc (| no_from_top |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [];
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "len",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm_interpreter::interpreter::stack::Stack",
                                    "data"
                                  |)
                                ]
                              |),
                              M.read (| no_from_top |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Ok"
                          [
                            M.read (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::index::Index",
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [];
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  [ Ty.path "usize" ],
                                  "index",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm_interpreter::interpreter::stack::Stack",
                                    "data"
                                  |);
                                  BinOp.Wrap.sub (|
                                    BinOp.Wrap.sub (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [];
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "len",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_interpreter::interpreter::stack::Stack",
                                            "data"
                                          |)
                                        ]
                                      |),
                                      M.read (| no_from_top |)
                                    |),
                                    Value.Integer IntegerKind.Usize 1
                                  |)
                                ]
                              |)
                            |)
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            Value.StructTuple
                              "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                              []
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_peek : M.IsAssociatedFunction Self "peek" peek.
      
      (*
          pub fn dup(&mut self, n: usize) -> Result<(), InstructionResult> {
              assume!(n > 0, "attempted to dup 0");
              let len = self.data.len();
              if len < n {
                  Err(InstructionResult::StackUnderflow)
              } else if len + 1 > STACK_LIMIT {
                  Err(InstructionResult::StackOverflow)
              } else {
                  // SAFETY: check for out of bounds is done above and it makes this safe to do.
                  unsafe {
                      let ptr = self.data.as_mut_ptr().add(len);
                      ptr::copy_nonoverlapping(ptr.sub(n), ptr, 1);
                      self.data.set_len(len + 1);
                  }
                  Ok(())
              }
          }
      *)
      Definition dup (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                BinOp.gt (| M.read (| n |), Value.Integer IntegerKind.Usize 0 |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            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
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.call_closure (|
                                              M.get_function (| "core::panicking::panic_fmt", [] |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::fmt::Arguments",
                                                    "new_v1",
                                                    []
                                                  |),
                                                  [
                                                    M.alloc (|
                                                      Value.Array
                                                        [
                                                          M.read (|
                                                            Value.String
                                                              "internal error: entered unreachable code: attempted to dup 0"
                                                          |)
                                                        ]
                                                    |);
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "none",
                                                          []
                                                        |),
                                                        []
                                                      |)
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              let~ _ :=
                                                M.alloc (|
                                                  M.never_to_any (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::hint::unreachable_unchecked",
                                                        []
                                                      |),
                                                      []
                                                    |)
                                                  |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)
                                            |)
                                          |)
                                        |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "alloc::alloc::Global"
                        ],
                      "len",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::interpreter::stack::Stack",
                        "data"
                      |)
                    ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use (M.alloc (| BinOp.lt (| M.read (| len |), M.read (| n |) |) |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            Value.StructTuple
                              "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                              []
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    BinOp.gt (|
                                      BinOp.Wrap.add (|
                                        M.read (| len |),
                                        Value.Integer IntegerKind.Usize 1
                                      |),
                                      M.read (|
                                        M.get_constant (|
                                          "revm_interpreter::interpreter::stack::STACK_LIMIT"
                                        |)
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [
                                    Value.StructTuple
                                      "revm_interpreter::instruction_result::InstructionResult::StackOverflow"
                                      []
                                  ]
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let~ _ :=
                                let~ ptr :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "*mut")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ],
                                        "add",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "alloc::vec::Vec")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [];
                                                Ty.path "alloc::alloc::Global"
                                              ],
                                            "as_mut_ptr",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm_interpreter::interpreter::stack::Stack",
                                              "data"
                                            |)
                                          ]
                                        |);
                                        M.read (| len |)
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::intrinsics::copy_nonoverlapping",
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            []
                                        ]
                                      |),
                                      [
                                        (* MutToConstPointer *)
                                        M.pointer_coercion
                                          (M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "*mut")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "ruint::Uint")
                                                    [
                                                      Value.Integer IntegerKind.Usize 256;
                                                      Value.Integer IntegerKind.Usize 4
                                                    ]
                                                    []
                                                ],
                                              "sub",
                                              []
                                            |),
                                            [ M.read (| ptr |); M.read (| n |) ]
                                          |));
                                        M.read (| ptr |);
                                        Value.Integer IntegerKind.Usize 1
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [];
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        "set_len",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm_interpreter::interpreter::stack::Stack",
                                          "data"
                                        |);
                                        BinOp.Wrap.add (|
                                          M.read (| len |),
                                          Value.Integer IntegerKind.Usize 1
                                        |)
                                      ]
                                    |)
                                  |) in
                                M.alloc (| Value.Tuple [] |) in
                              M.alloc (|
                                Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_dup : M.IsAssociatedFunction Self "dup" dup.
      
      (*
          pub fn swap(&mut self, n: usize) -> Result<(), InstructionResult> {
              self.exchange(0, n)
          }
      *)
      Definition swap (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_interpreter::interpreter::stack::Stack",
                "exchange",
                []
              |),
              [ M.read (| self |); Value.Integer IntegerKind.Usize 0; M.read (| n |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_swap : M.IsAssociatedFunction Self "swap" swap.
      
      (*
          pub fn exchange(&mut self, n: usize, m: usize) -> Result<(), InstructionResult> {
              assume!(m > 0, "overlapping exchange");
              let len = self.data.len();
              let n_m_index = n + m;
              if n_m_index >= len {
                  return Err(InstructionResult::StackUnderflow);
              }
              // SAFETY: `n` and `n_m` are checked to be within bounds, and they don't overlap.
              unsafe {
                  // NOTE: `ptr::swap_nonoverlapping` is more efficient than `slice::swap` or `ptr::swap`
                  // because it operates under the assumption that the pointers do not overlap,
                  // eliminating an intemediate copy,
                  // which is a condition we know to be true in this context.
                  let top = self.data.as_mut_ptr().add(len - 1);
                  core::ptr::swap_nonoverlapping(top.sub(n), top.sub(n_m_index), 1);
              }
              Ok(())
          }
      *)
      Definition exchange (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; n; m ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let n := M.alloc (| n |) in
            let m := M.alloc (| m |) 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 (|
                                  UnOp.not (|
                                    BinOp.gt (| M.read (| m |), Value.Integer IntegerKind.Usize 0 |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                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
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.call_closure (|
                                                  M.get_function (|
                                                    "core::panicking::panic_fmt",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path "core::fmt::Arguments",
                                                        "new_v1",
                                                        []
                                                      |),
                                                      [
                                                        M.alloc (|
                                                          Value.Array
                                                            [
                                                              M.read (|
                                                                Value.String
                                                                  "internal error: entered unreachable code: overlapping exchange"
                                                              |)
                                                            ]
                                                        |);
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::rt::Argument",
                                                              "none",
                                                              []
                                                            |),
                                                            []
                                                          |)
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |)
                                            |)));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::hint::unreachable_unchecked",
                                                            []
                                                          |),
                                                          []
                                                        |)
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)
                                                |)
                                              |)
                                            |)))
                                      ]
                                    |) in
                                  M.alloc (| Value.Tuple [] |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ len :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [];
                              Ty.path "alloc::alloc::Global"
                            ],
                          "len",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm_interpreter::interpreter::stack::Stack",
                            "data"
                          |)
                        ]
                      |)
                    |) in
                  let~ n_m_index :=
                    M.alloc (| BinOp.Wrap.add (| M.read (| n |), M.read (| m |) |) |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ge (| M.read (| n_m_index |), M.read (| 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
                                          "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                                          []
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    let~ top :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "*mut")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  []
                              ],
                            "add",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.path "alloc::alloc::Global"
                                  ],
                                "as_mut_ptr",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm_interpreter::interpreter::stack::Stack",
                                  "data"
                                |)
                              ]
                            |);
                            BinOp.Wrap.sub (| M.read (| len |), Value.Integer IntegerKind.Usize 1 |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::ptr::swap_nonoverlapping",
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                []
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "*mut")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                "sub",
                                []
                              |),
                              [ M.read (| top |); M.read (| n |) ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "*mut")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                "sub",
                                []
                              |),
                              [ M.read (| top |); M.read (| n_m_index |) ]
                            |);
                            Value.Integer IntegerKind.Usize 1
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_exchange : M.IsAssociatedFunction Self "exchange" exchange.
      
      (*
          pub fn push_slice(&mut self, slice: &[u8]) -> Result<(), InstructionResult> {
              if slice.is_empty() {
                  return Ok(());
              }
      
              let n_words = (slice.len() + 31) / 32;
              let new_len = self.data.len() + n_words;
              if new_len > STACK_LIMIT {
                  return Err(InstructionResult::StackOverflow);
              }
      
              // SAFETY: length checked above.
              unsafe {
                  let dst = self.data.as_mut_ptr().add(self.data.len()).cast::<u64>();
                  self.data.set_len(new_len);
      
                  let mut i = 0;
      
                  // write full words
                  let words = slice.chunks_exact(32);
                  let partial_last_word = words.remainder();
                  for word in words {
                      // Note: we unroll `U256::from_be_bytes` here to write directly into the buffer,
                      // instead of creating a 32 byte array on the stack and then copying it over.
                      for l in word.rchunks_exact(8) {
                          dst.add(i).write(u64::from_be_bytes(l.try_into().unwrap()));
                          i += 1;
                      }
                  }
      
                  if partial_last_word.is_empty() {
                      return Ok(());
                  }
      
                  // write limbs of partial last word
                  let limbs = partial_last_word.rchunks_exact(8);
                  let partial_last_limb = limbs.remainder();
                  for l in limbs {
                      dst.add(i).write(u64::from_be_bytes(l.try_into().unwrap()));
                      i += 1;
                  }
      
                  // write partial last limb by padding with zeros
                  if !partial_last_limb.is_empty() {
                      let mut tmp = [0u8; 8];
                      tmp[8 - partial_last_limb.len()..].copy_from_slice(partial_last_limb);
                      dst.add(i).write(u64::from_be_bytes(tmp));
                      i += 1;
                  }
      
                  debug_assert_eq!((i + 3) / 4, n_words, "wrote too much");
      
                  // zero out upper bytes of last word
                  let m = i % 4; // 32 / 8
                  if m != 0 {
                      dst.add(i).write_bytes(0, 4 - m);
                  }
              }
      
              Ok(())
          }
      *)
      Definition push_slice (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; slice ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let slice := M.alloc (| slice |) 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 (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      "is_empty",
                                      []
                                    |),
                                    [ M.read (| slice |) ]
                                  |)
                                |)) 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
                  let~ n_words :=
                    M.alloc (|
                      BinOp.Wrap.div (|
                        BinOp.Wrap.add (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                              "len",
                              []
                            |),
                            [ M.read (| slice |) ]
                          |),
                          Value.Integer IntegerKind.Usize 31
                        |),
                        Value.Integer IntegerKind.Usize 32
                      |)
                    |) in
                  let~ new_len :=
                    M.alloc (|
                      BinOp.Wrap.add (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "alloc::alloc::Global"
                              ],
                            "len",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm_interpreter::interpreter::stack::Stack",
                              "data"
                            |)
                          ]
                        |),
                        M.read (| n_words |)
                      |)
                    |) in
                  let~ _ :=
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.gt (|
                                    M.read (| new_len |),
                                    M.read (|
                                      M.get_constant (|
                                        "revm_interpreter::interpreter::stack::STACK_LIMIT"
                                      |)
                                    |)
                                  |)
                                |)) 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
                                          "revm_interpreter::instruction_result::InstructionResult::StackOverflow"
                                          []
                                      ]
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  let~ _ :=
                    let~ dst :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "*mut")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  []
                              ],
                            "cast",
                            [ Ty.path "u64" ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "*mut")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                "add",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [];
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    "as_mut_ptr",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "revm_interpreter::interpreter::stack::Stack",
                                      "data"
                                    |)
                                  ]
                                |);
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [];
                                        Ty.path "alloc::alloc::Global"
                                      ],
                                    "len",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "revm_interpreter::interpreter::stack::Stack",
                                      "data"
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "alloc::alloc::Global"
                              ],
                            "set_len",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm_interpreter::interpreter::stack::Stack",
                              "data"
                            |);
                            M.read (| new_len |)
                          ]
                        |)
                      |) in
                    let~ i := M.alloc (| Value.Integer IntegerKind.Usize 0 |) in
                    let~ words :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                            "chunks_exact",
                            []
                          |),
                          [ M.read (| slice |); Value.Integer IntegerKind.Usize 32 ]
                        |)
                      |) in
                    let~ partial_last_word :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::slice::iter::ChunksExact") [] [ Ty.path "u8" ],
                            "remainder",
                            []
                          |),
                          [ words ]
                        |)
                      |) in
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::ChunksExact")
                                  []
                                  [ Ty.path "u8" ],
                                [],
                                "into_iter",
                                []
                              |),
                              [ M.read (| words |) ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let iter := M.copy (| γ |) in
                                M.loop (|
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::slice::iter::ChunksExact")
                                                []
                                                [ Ty.path "u8" ],
                                              [],
                                              "next",
                                              []
                                            |),
                                            [ iter ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let _ :=
                                                M.is_struct_tuple (|
                                                  γ,
                                                  "core::option::Option::None"
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let word := M.copy (| γ0_0 |) in
                                              M.use
                                                (M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_trait_method (|
                                                        "core::iter::traits::collect::IntoIterator",
                                                        Ty.apply
                                                          (Ty.path
                                                            "core::slice::iter::RChunksExact")
                                                          []
                                                          [ Ty.path "u8" ],
                                                        [],
                                                        "into_iter",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "slice")
                                                              []
                                                              [ Ty.path "u8" ],
                                                            "rchunks_exact",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| word |);
                                                            Value.Integer IntegerKind.Usize 8
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let iter := M.copy (| γ |) in
                                                        M.loop (|
                                                          ltac:(M.monadic
                                                            (let~ _ :=
                                                              M.match_operator (|
                                                                M.alloc (|
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::iter::traits::iterator::Iterator",
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::slice::iter::RChunksExact")
                                                                        []
                                                                        [ Ty.path "u8" ],
                                                                      [],
                                                                      "next",
                                                                      []
                                                                    |),
                                                                    [ iter ]
                                                                  |)
                                                                |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let _ :=
                                                                        M.is_struct_tuple (|
                                                                          γ,
                                                                          "core::option::Option::None"
                                                                        |) in
                                                                      M.alloc (|
                                                                        M.never_to_any (|
                                                                          M.read (| M.break (||) |)
                                                                        |)
                                                                      |)));
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ0_0 :=
                                                                        M.SubPointer.get_struct_tuple_field (|
                                                                          γ,
                                                                          "core::option::Option::Some",
                                                                          0
                                                                        |) in
                                                                      let l := M.copy (| γ0_0 |) in
                                                                      let~ _ :=
                                                                        M.alloc (|
                                                                          M.call_closure (|
                                                                            M.get_associated_function (|
                                                                              Ty.apply
                                                                                (Ty.path "*mut")
                                                                                []
                                                                                [ Ty.path "u64" ],
                                                                              "write",
                                                                              []
                                                                            |),
                                                                            [
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path "*mut")
                                                                                    []
                                                                                    [ Ty.path "u64"
                                                                                    ],
                                                                                  "add",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (| dst |);
                                                                                  M.read (| i |)
                                                                                ]
                                                                              |);
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.path "u64",
                                                                                  "from_be_bytes",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.call_closure (|
                                                                                    M.get_associated_function (|
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "core::result::Result")
                                                                                        []
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "array")
                                                                                            [
                                                                                              Value.Integer
                                                                                                IntegerKind.Usize
                                                                                                8
                                                                                            ]
                                                                                            [
                                                                                              Ty.path
                                                                                                "u8"
                                                                                            ];
                                                                                          Ty.path
                                                                                            "core::array::TryFromSliceError"
                                                                                        ],
                                                                                      "unwrap",
                                                                                      []
                                                                                    |),
                                                                                    [
                                                                                      M.call_closure (|
                                                                                        M.get_trait_method (|
                                                                                          "core::convert::TryInto",
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "&")
                                                                                            []
                                                                                            [
                                                                                              Ty.apply
                                                                                                (Ty.path
                                                                                                  "slice")
                                                                                                []
                                                                                                [
                                                                                                  Ty.path
                                                                                                    "u8"
                                                                                                ]
                                                                                            ],
                                                                                          [
                                                                                            Ty.apply
                                                                                              (Ty.path
                                                                                                "array")
                                                                                              [
                                                                                                Value.Integer
                                                                                                  IntegerKind.Usize
                                                                                                  8
                                                                                              ]
                                                                                              [
                                                                                                Ty.path
                                                                                                  "u8"
                                                                                              ]
                                                                                          ],
                                                                                          "try_into",
                                                                                          []
                                                                                        |),
                                                                                        [
                                                                                          M.read (|
                                                                                            l
                                                                                          |)
                                                                                        ]
                                                                                      |)
                                                                                    ]
                                                                                  |)
                                                                                ]
                                                                              |)
                                                                            ]
                                                                          |)
                                                                        |) in
                                                                      let~ _ :=
                                                                        let β := i in
                                                                        M.write (|
                                                                          β,
                                                                          BinOp.Wrap.add (|
                                                                            M.read (| β |),
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              1
                                                                          |)
                                                                        |) in
                                                                      M.alloc (| Value.Tuple [] |)))
                                                                ]
                                                              |) in
                                                            M.alloc (| Value.Tuple [] |)))
                                                        |)))
                                                  ]
                                                |))))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                        "is_empty",
                                        []
                                      |),
                                      [ M.read (| partial_last_word |) ]
                                    |)
                                  |)) 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
                    let~ limbs :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                            "rchunks_exact",
                            []
                          |),
                          [ M.read (| partial_last_word |); Value.Integer IntegerKind.Usize 8 ]
                        |)
                      |) in
                    let~ partial_last_limb :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::slice::iter::RChunksExact")
                              []
                              [ Ty.path "u8" ],
                            "remainder",
                            []
                          |),
                          [ limbs ]
                        |)
                      |) in
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::RChunksExact")
                                  []
                                  [ Ty.path "u8" ],
                                [],
                                "into_iter",
                                []
                              |),
                              [ M.read (| limbs |) ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let iter := M.copy (| γ |) in
                                M.loop (|
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::slice::iter::RChunksExact")
                                                []
                                                [ Ty.path "u8" ],
                                              [],
                                              "next",
                                              []
                                            |),
                                            [ iter ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let _ :=
                                                M.is_struct_tuple (|
                                                  γ,
                                                  "core::option::Option::None"
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let l := M.copy (| γ0_0 |) in
                                              let~ _ :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "*mut")
                                                        []
                                                        [ Ty.path "u64" ],
                                                      "write",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "*mut")
                                                            []
                                                            [ Ty.path "u64" ],
                                                          "add",
                                                          []
                                                        |),
                                                        [ M.read (| dst |); M.read (| i |) ]
                                                      |);
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "u64",
                                                          "from_be_bytes",
                                                          []
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.apply
                                                                (Ty.path "core::result::Result")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "array")
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        8
                                                                    ]
                                                                    [ Ty.path "u8" ];
                                                                  Ty.path
                                                                    "core::array::TryFromSliceError"
                                                                ],
                                                              "unwrap",
                                                              []
                                                            |),
                                                            [
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::convert::TryInto",
                                                                  Ty.apply
                                                                    (Ty.path "&")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "slice")
                                                                        []
                                                                        [ Ty.path "u8" ]
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path "array")
                                                                      [
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          8
                                                                      ]
                                                                      [ Ty.path "u8" ]
                                                                  ],
                                                                  "try_into",
                                                                  []
                                                                |),
                                                                [ M.read (| l |) ]
                                                              |)
                                                            ]
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |) in
                                              let~ _ :=
                                                let β := i in
                                                M.write (|
                                                  β,
                                                  BinOp.Wrap.add (|
                                                    M.read (| β |),
                                                    Value.Integer IntegerKind.Usize 1
                                                  |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    UnOp.not (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                          "is_empty",
                                          []
                                        |),
                                        [ M.read (| partial_last_limb |) ]
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              let~ tmp :=
                                M.alloc (|
                                  repeat (|
                                    Value.Integer IntegerKind.U8 0,
                                    Value.Integer IntegerKind.Usize 8
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                      "copy_from_slice",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::index::IndexMut",
                                          Ty.apply
                                            (Ty.path "array")
                                            [ Value.Integer IntegerKind.Usize 8 ]
                                            [ Ty.path "u8" ],
                                          [
                                            Ty.apply
                                              (Ty.path "core::ops::range::RangeFrom")
                                              []
                                              [ Ty.path "usize" ]
                                          ],
                                          "index_mut",
                                          []
                                        |),
                                        [
                                          tmp;
                                          Value.StructRecord
                                            "core::ops::range::RangeFrom"
                                            [
                                              ("start",
                                                BinOp.Wrap.sub (|
                                                  Value.Integer IntegerKind.Usize 8,
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "slice")
                                                        []
                                                        [ Ty.path "u8" ],
                                                      "len",
                                                      []
                                                    |),
                                                    [ M.read (| partial_last_limb |) ]
                                                  |)
                                                |))
                                            ]
                                        ]
                                      |);
                                      M.read (| partial_last_limb |)
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "*mut") [] [ Ty.path "u64" ],
                                      "write",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "*mut") [] [ Ty.path "u64" ],
                                          "add",
                                          []
                                        |),
                                        [ M.read (| dst |); M.read (| i |) ]
                                      |);
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "u64",
                                          "from_be_bytes",
                                          []
                                        |),
                                        [ M.read (| tmp |) ]
                                      |)
                                    ]
                                  |)
                                |) in
                              let~ _ :=
                                let β := i in
                                M.write (|
                                  β,
                                  BinOp.Wrap.add (|
                                    M.read (| β |),
                                    Value.Integer IntegerKind.Usize 1
                                  |)
                                |) 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
                                      [
                                        M.alloc (|
                                          BinOp.Wrap.div (|
                                            BinOp.Wrap.add (|
                                              M.read (| i |),
                                              Value.Integer IntegerKind.Usize 3
                                            |),
                                            Value.Integer IntegerKind.Usize 4
                                          |)
                                        |);
                                        n_words
                                      ]
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                        let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                        let left_val := M.copy (| γ0_0 |) in
                                        let right_val := M.copy (| γ0_1 |) in
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      UnOp.not (|
                                                        BinOp.eq (|
                                                          M.read (| M.read (| left_val |) |),
                                                          M.read (| M.read (| right_val |) |)
                                                        |)
                                                      |)
                                                    |)) in
                                                let _ :=
                                                  M.is_constant_or_break_match (|
                                                    M.read (| γ |),
                                                    Value.Bool true
                                                  |) in
                                                M.alloc (|
                                                  M.never_to_any (|
                                                    M.read (|
                                                      let~ kind :=
                                                        M.alloc (|
                                                          Value.StructTuple
                                                            "core::panicking::AssertKind::Eq"
                                                            []
                                                        |) in
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "core::panicking::assert_failed",
                                                            [ Ty.path "usize"; Ty.path "usize" ]
                                                          |),
                                                          [
                                                            M.read (| kind |);
                                                            M.read (| left_val |);
                                                            M.read (| right_val |);
                                                            Value.StructTuple
                                                              "core::option::Option::Some"
                                                              [
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path "core::fmt::Arguments",
                                                                    "new_const",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.alloc (|
                                                                      Value.Array
                                                                        [
                                                                          M.read (|
                                                                            Value.String
                                                                              "wrote too much"
                                                                          |)
                                                                        ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              ]
                                                          ]
                                                        |)
                                                      |)
                                                    |)
                                                  |)
                                                |)));
                                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                          ]
                                        |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ m :=
                      M.alloc (|
                        BinOp.Wrap.rem (| M.read (| i |), Value.Integer IntegerKind.Usize 4 |)
                      |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.ne (| M.read (| m |), Value.Integer IntegerKind.Usize 0 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "*mut") [] [ Ty.path "u64" ],
                                    "write_bytes",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "*mut") [] [ Ty.path "u64" ],
                                        "add",
                                        []
                                      |),
                                      [ M.read (| dst |); M.read (| i |) ]
                                    |);
                                    Value.Integer IntegerKind.U8 0;
                                    BinOp.Wrap.sub (|
                                      Value.Integer IntegerKind.Usize 4,
                                      M.read (| m |)
                                    |)
                                  ]
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |) in
                  M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_push_slice : M.IsAssociatedFunction Self "push_slice" push_slice.
      
      (*
          pub fn set(&mut self, no_from_top: usize, val: U256) -> Result<(), InstructionResult> {
              if self.data.len() > no_from_top {
                  let len = self.data.len();
                  self.data[len - no_from_top - 1] = val;
                  Ok(())
              } else {
                  Err(InstructionResult::StackUnderflow)
              }
          }
      *)
      Definition set (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; no_from_top; val ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let no_from_top := M.alloc (| no_from_top |) in
            let val := M.alloc (| val |) in
            M.read (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [];
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "len",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm_interpreter::interpreter::stack::Stack",
                                    "data"
                                  |)
                                ]
                              |),
                              M.read (| no_from_top |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ len :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [];
                                  Ty.path "alloc::alloc::Global"
                                ],
                              "len",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm_interpreter::interpreter::stack::Stack",
                                "data"
                              |)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.write (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::index::IndexMut",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [];
                                  Ty.path "alloc::alloc::Global"
                                ],
                              [ Ty.path "usize" ],
                              "index_mut",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm_interpreter::interpreter::stack::Stack",
                                "data"
                              |);
                              BinOp.Wrap.sub (|
                                BinOp.Wrap.sub (| M.read (| len |), M.read (| no_from_top |) |),
                                Value.Integer IntegerKind.Usize 1
                              |)
                            ]
                          |),
                          M.read (| val |)
                        |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [
                            Value.StructTuple
                              "revm_interpreter::instruction_result::InstructionResult::StackUnderflow"
                              []
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_set : M.IsAssociatedFunction Self "set" set.
    End Impl_revm_interpreter_interpreter_stack_Stack.
  End stack.
End interpreter.
