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

Module function_stack.
  (* StructRecord
    {
      name := "FunctionReturnFrame";
      const_params := [];
      ty_params := [];
      fields := [ ("idx", Ty.path "usize"); ("pc", Ty.path "usize") ];
    } *)
  
  Module Impl_core_fmt_Debug_for_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    (* 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_field2_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "FunctionReturnFrame" |);
              M.read (| Value.String "idx" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_interpreter::function_stack::FunctionReturnFrame",
                "idx"
              |);
              M.read (| Value.String "pc" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::function_stack::FunctionReturnFrame",
                  "pc"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_function_stack_FunctionReturnFrame.
  
  Module Impl_core_default_Default_for_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_interpreter::function_stack::FunctionReturnFrame"
            [
              ("idx",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "usize",
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("pc",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "usize",
                    [],
                    "default",
                    []
                  |),
                  []
                |))
            ]))
      | _, _, _ => 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_function_stack_FunctionReturnFrame.
  
  Module Impl_core_clone_Clone_for_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_revm_interpreter_function_stack_FunctionReturnFrame.
  
  Module Impl_core_marker_Copy_for_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_revm_interpreter_function_stack_FunctionReturnFrame.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_interpreter_function_stack_FunctionReturnFrame.
  
  Module Impl_core_cmp_PartialEq_for_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            BinOp.eq (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::function_stack::FunctionReturnFrame",
                  "idx"
                |)
              |),
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "revm_interpreter::function_stack::FunctionReturnFrame",
                  "idx"
                |)
              |)
            |),
            ltac:(M.monadic
              (BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_interpreter::function_stack::FunctionReturnFrame",
                    "pc"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_interpreter::function_stack::FunctionReturnFrame",
                    "pc"
                  |)
                |)
              |)))
          |)))
      | _, _, _ => 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_function_stack_FunctionReturnFrame.
  
  Module Impl_core_cmp_Eq_for_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    (* 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_function_stack_FunctionReturnFrame.
  
  Module Impl_core_hash_Hash_for_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "usize", [], "hash", [ __H ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::function_stack::FunctionReturnFrame",
                      "idx"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "usize", [], "hash", [ __H ] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_interpreter::function_stack::FunctionReturnFrame",
                    "pc"
                  |);
                  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_function_stack_FunctionReturnFrame.
  
  Module Impl_revm_interpreter_function_stack_FunctionReturnFrame.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionReturnFrame".
    
    (*
        pub fn new(idx: usize, pc: usize) -> Self {
            Self { idx, pc }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ idx; pc ] =>
        ltac:(M.monadic
          (let idx := M.alloc (| idx |) in
          let pc := M.alloc (| pc |) in
          Value.StructRecord
            "revm_interpreter::function_stack::FunctionReturnFrame"
            [ ("idx", M.read (| idx |)); ("pc", M.read (| pc |)) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  End Impl_revm_interpreter_function_stack_FunctionReturnFrame.
  
  (* StructRecord
    {
      name := "FunctionStack";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("return_stack",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.path "revm_interpreter::function_stack::FunctionReturnFrame";
                Ty.path "alloc::alloc::Global"
              ]);
          ("current_code_idx", Ty.path "usize")
        ];
    } *)
  
  Module Impl_core_fmt_Debug_for_revm_interpreter_function_stack_FunctionStack.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionStack".
    
    (* 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_field2_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "FunctionStack" |);
              M.read (| Value.String "return_stack" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_interpreter::function_stack::FunctionStack",
                "return_stack"
              |);
              M.read (| Value.String "current_code_idx" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::function_stack::FunctionStack",
                  "current_code_idx"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_function_stack_FunctionStack.
  
  Module Impl_core_default_Default_for_revm_interpreter_function_stack_FunctionStack.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionStack".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_interpreter::function_stack::FunctionStack"
            [
              ("return_stack",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "revm_interpreter::function_stack::FunctionReturnFrame";
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("current_code_idx",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "usize",
                    [],
                    "default",
                    []
                  |),
                  []
                |))
            ]))
      | _, _, _ => 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_function_stack_FunctionStack.
  
  Module Impl_revm_interpreter_function_stack_FunctionStack.
    Definition Self : Ty.t := Ty.path "revm_interpreter::function_stack::FunctionStack".
    
    (*
        pub fn new() -> Self {
            Self {
                return_stack: Vec::new(),
                current_code_idx: 0,
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_interpreter::function_stack::FunctionStack"
            [
              ("return_stack",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "revm_interpreter::function_stack::FunctionReturnFrame";
                        Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |));
              ("current_code_idx", Value.Integer IntegerKind.Usize 0)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn push(&mut self, program_counter: usize, new_idx: usize) {
            self.return_stack.push(FunctionReturnFrame {
                idx: self.current_code_idx,
                pc: program_counter,
            });
            self.current_code_idx = new_idx;
        }
    *)
    Definition push (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; program_counter; new_idx ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let program_counter := M.alloc (| program_counter |) in
          let new_idx := M.alloc (| new_idx |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.path "revm_interpreter::function_stack::FunctionReturnFrame";
                        Ty.path "alloc::alloc::Global"
                      ],
                    "push",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::function_stack::FunctionStack",
                      "return_stack"
                    |);
                    Value.StructRecord
                      "revm_interpreter::function_stack::FunctionReturnFrame"
                      [
                        ("idx",
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm_interpreter::function_stack::FunctionStack",
                              "current_code_idx"
                            |)
                          |));
                        ("pc", M.read (| program_counter |))
                      ]
                  ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::function_stack::FunctionStack",
                  "current_code_idx"
                |),
                M.read (| new_idx |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_push : M.IsAssociatedFunction Self "push" push.
    
    (*
        pub fn return_stack_len(&self) -> usize {
            self.return_stack.len()
        }
    *)
    Definition return_stack_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.path "revm_interpreter::function_stack::FunctionReturnFrame";
                  Ty.path "alloc::alloc::Global"
                ],
              "len",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_interpreter::function_stack::FunctionStack",
                "return_stack"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_return_stack_len :
      M.IsAssociatedFunction Self "return_stack_len" return_stack_len.
    
    (*
        pub fn pop(&mut self) -> Option<FunctionReturnFrame> {
            self.return_stack.pop().map(|frame| {
                self.current_code_idx = frame.idx;
                frame
            })
        }
    *)
    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.path "revm_interpreter::function_stack::FunctionReturnFrame" ],
              "map",
              [
                Ty.path "revm_interpreter::function_stack::FunctionReturnFrame";
                Ty.function
                  [ Ty.tuple [ Ty.path "revm_interpreter::function_stack::FunctionReturnFrame" ] ]
                  (Ty.path "revm_interpreter::function_stack::FunctionReturnFrame")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.path "revm_interpreter::function_stack::FunctionReturnFrame";
                      Ty.path "alloc::alloc::Global"
                    ],
                  "pop",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_interpreter::function_stack::FunctionStack",
                    "return_stack"
                  |)
                ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let frame := M.copy (| γ |) in
                                M.read (|
                                  let~ _ :=
                                    M.write (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm_interpreter::function_stack::FunctionStack",
                                        "current_code_idx"
                                      |),
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          frame,
                                          "revm_interpreter::function_stack::FunctionReturnFrame",
                                          "idx"
                                        |)
                                      |)
                                    |) in
                                  frame
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_pop : M.IsAssociatedFunction Self "pop" pop.
    
    (*
        pub fn set_current_code_idx(&mut self, idx: usize) {
            self.current_code_idx = idx;
        }
    *)
    Definition set_current_code_idx (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; idx ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let idx := M.alloc (| idx |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::function_stack::FunctionStack",
                  "current_code_idx"
                |),
                M.read (| idx |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_set_current_code_idx :
      M.IsAssociatedFunction Self "set_current_code_idx" set_current_code_idx.
  End Impl_revm_interpreter_function_stack_FunctionStack.
End function_stack.
