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

Module handler.
  Module handle_types.
    Module execution.
      Axiom LastFrameReturnHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::LastFrameReturnHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom FrameCallHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::FrameCallHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom FrameCallReturnHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::FrameCallReturnHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom InsertCallOutcomeHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::InsertCallOutcomeHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom FrameCreateHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::FrameCreateHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom FrameCreateReturnHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::FrameCreateReturnHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom InsertCreateOutcomeHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::InsertCreateOutcomeHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom FrameEOFCreateHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::FrameEOFCreateHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom FrameEOFCreateReturnHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::FrameEOFCreateReturnHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      Axiom InsertEOFCreateOutcomeHandle :
        forall (EXT DB : Ty.t),
        (Ty.apply
            (Ty.path "revm::handler::handle_types::execution::InsertEOFCreateOutcomeHandle")
            []
            [ EXT; DB ]) =
          (Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn
                [
                  ("existential predicate with variables", []);
                  ("existential predicate with variables", [])
                ];
              Ty.path "alloc::alloc::Global"
            ]).
      
      (* StructRecord
        {
          name := "ExecutionHandler";
          const_params := [];
          ty_params := [ "EXT"; "DB" ];
          fields :=
            [
              ("last_frame_return",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("call",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("call_return",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("insert_call_outcome",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("create",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("create_return",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("insert_create_outcome",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("eofcreate",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("eofcreate_return",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ]);
              ("insert_eofcreate_outcome",
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn
                      [
                        ("existential predicate with variables", []);
                        ("existential predicate with variables", [])
                      ];
                    Ty.path "alloc::alloc::Global"
                  ])
            ];
        } *)
      
      Module Impl_revm_handler_handle_types_execution_ExecutionHandler_EXT_DB.
        Definition Self (EXT DB : Ty.t) : Ty.t :=
          Ty.apply
            (Ty.path "revm::handler::handle_types::execution::ExecutionHandler")
            []
            [ EXT; DB ].
        
        (*
            pub fn new<SPEC: Spec + 'a>() -> Self {
                Self {
                    last_frame_return: Arc::new(mainnet::last_frame_return::<SPEC, EXT, DB>),
                    call: Arc::new(mainnet::call::<SPEC, EXT, DB>),
                    call_return: Arc::new(mainnet::call_return::<EXT, DB>),
                    insert_call_outcome: Arc::new(mainnet::insert_call_outcome),
                    create: Arc::new(mainnet::create::<SPEC, EXT, DB>),
                    create_return: Arc::new(mainnet::create_return::<SPEC, EXT, DB>),
                    insert_create_outcome: Arc::new(mainnet::insert_create_outcome),
                    eofcreate: Arc::new(mainnet::eofcreate::<SPEC, EXT, DB>),
                    eofcreate_return: Arc::new(mainnet::eofcreate_return::<SPEC, EXT, DB>),
                    insert_eofcreate_outcome: Arc::new(mainnet::insert_eofcreate_outcome),
                }
            }
        *)
        Definition new (EXT DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [ SPEC ], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "revm::handler::handle_types::execution::ExecutionHandler"
                [
                  ("last_frame_return",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply (Ty.path "&mut") [] [ Ty.path "revm::frame::FrameResult" ]
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.tuple [];
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::last_frame_return",
                          [ SPEC; EXT; DB ]
                        |)
                      ]
                    |));
                  ("call",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply
                                  (Ty.path "alloc::boxed::Box")
                                  []
                                  [
                                    Ty.path
                                      "revm_interpreter::interpreter_action::call_inputs::CallInputs";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.path "revm::frame::FrameOrResult";
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::call",
                          [ SPEC; EXT; DB ]
                        |)
                      ]
                    |));
                  ("call_return",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply
                                  (Ty.path "alloc::boxed::Box")
                                  []
                                  [ Ty.path "revm::frame::CallFrame"; Ty.path "alloc::alloc::Global"
                                  ];
                                Ty.path "revm_interpreter::interpreter::InterpreterResult"
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.path
                                    "revm_interpreter::interpreter_action::call_outcome::CallOutcome";
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::call_return",
                          [ EXT; DB ]
                        |)
                      ]
                    |));
                  ("insert_call_outcome",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply (Ty.path "&mut") [] [ Ty.path "revm::frame::Frame" ];
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [
                                    Ty.path
                                      "revm_interpreter::interpreter::shared_memory::SharedMemory"
                                  ];
                                Ty.path
                                  "revm_interpreter::interpreter_action::call_outcome::CallOutcome"
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.tuple [];
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::insert_call_outcome",
                          [ EXT; DB ]
                        |)
                      ]
                    |));
                  ("create",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply
                                  (Ty.path "alloc::boxed::Box")
                                  []
                                  [
                                    Ty.path
                                      "revm_interpreter::interpreter_action::create_inputs::CreateInputs";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.path "revm::frame::FrameOrResult";
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::create",
                          [ SPEC; EXT; DB ]
                        |)
                      ]
                    |));
                  ("create_return",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply
                                  (Ty.path "alloc::boxed::Box")
                                  []
                                  [
                                    Ty.path "revm::frame::CreateFrame";
                                    Ty.path "alloc::alloc::Global"
                                  ];
                                Ty.path "revm_interpreter::interpreter::InterpreterResult"
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.path
                                    "revm_interpreter::interpreter_action::create_outcome::CreateOutcome";
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::create_return",
                          [ SPEC; EXT; DB ]
                        |)
                      ]
                    |));
                  ("insert_create_outcome",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply (Ty.path "&mut") [] [ Ty.path "revm::frame::Frame" ];
                                Ty.path
                                  "revm_interpreter::interpreter_action::create_outcome::CreateOutcome"
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.tuple [];
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::insert_create_outcome",
                          [ EXT; DB ]
                        |)
                      ]
                    |));
                  ("eofcreate",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply
                                  (Ty.path "alloc::boxed::Box")
                                  []
                                  [
                                    Ty.path
                                      "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput";
                                    Ty.path "alloc::alloc::Global"
                                  ]
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.path "revm::frame::FrameOrResult";
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::eofcreate",
                          [ SPEC; EXT; DB ]
                        |)
                      ]
                    |));
                  ("eofcreate_return",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply
                                  (Ty.path "alloc::boxed::Box")
                                  []
                                  [
                                    Ty.path "revm::frame::EOFCreateFrame";
                                    Ty.path "alloc::alloc::Global"
                                  ];
                                Ty.path "revm_interpreter::interpreter::InterpreterResult"
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.path
                                    "revm_interpreter::interpreter_action::eof_create_outcome::EOFCreateOutcome";
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::eofcreate_return",
                          [ SPEC; EXT; DB ]
                        |)
                      ]
                    |));
                  ("insert_eofcreate_outcome",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [
                            Ty.function
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                                Ty.apply (Ty.path "&mut") [] [ Ty.path "revm::frame::Frame" ];
                                Ty.path
                                  "revm_interpreter::interpreter_action::eof_create_outcome::EOFCreateOutcome"
                              ]
                              (Ty.apply
                                (Ty.path "core::result::Result")
                                []
                                [
                                  Ty.tuple [];
                                  Ty.apply
                                    (Ty.path "revm_primitives::result::EVMError")
                                    []
                                    [ Ty.associated ]
                                ]);
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      [
                        M.get_function (|
                          "revm::handler::mainnet::execution::insert_eofcreate_outcome",
                          [ EXT; DB ]
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "new" (new EXT DB).
        (*
            pub fn last_frame_return(
                &self,
                context: &mut Context<EXT, DB>,
                frame_result: &mut FrameResult,
            ) -> Result<(), EVMError<DB::Error>> {
                (self.last_frame_return)(context, frame_result)
            }
        *)
        Definition last_frame_return
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; frame_result ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let frame_result := M.alloc (| frame_result |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply (Ty.path "&mut") [] [ Ty.path "revm::frame::FrameResult" ]
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "last_frame_return"
                      |)
                    ]
                  |);
                  Value.Tuple [ M.read (| context |); M.read (| frame_result |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_last_frame_return :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "last_frame_return" (last_frame_return EXT DB).
        
        (*
            pub fn call(
                &self,
                context: &mut Context<EXT, DB>,
                inputs: Box<CallInputs>,
            ) -> Result<FrameOrResult, EVMError<DB::Error>> {
                (self.call)(context, inputs.clone())
            }
        *)
        Definition call (EXT DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; inputs ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let inputs := M.alloc (| inputs |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [
                            Ty.path "revm_interpreter::interpreter_action::call_inputs::CallInputs";
                            Ty.path "alloc::alloc::Global"
                          ]
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "call"
                      |)
                    ]
                  |);
                  Value.Tuple
                    [
                      M.read (| context |);
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::clone::Clone",
                          Ty.apply
                            (Ty.path "alloc::boxed::Box")
                            []
                            [
                              Ty.path
                                "revm_interpreter::interpreter_action::call_inputs::CallInputs";
                              Ty.path "alloc::alloc::Global"
                            ],
                          [],
                          "clone",
                          []
                        |),
                        [ inputs ]
                      |)
                    ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_call :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "call" (call EXT DB).
        
        (*
            pub fn call_return(
                &self,
                context: &mut Context<EXT, DB>,
                frame: Box<CallFrame>,
                interpreter_result: InterpreterResult,
            ) -> Result<CallOutcome, EVMError<DB::Error>> {
                (self.call_return)(context, frame, interpreter_result)
            }
        *)
        Definition call_return
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; frame; interpreter_result ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let frame := M.alloc (| frame |) in
              let interpreter_result := M.alloc (| interpreter_result |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [ Ty.path "revm::frame::CallFrame"; Ty.path "alloc::alloc::Global" ];
                        Ty.path "revm_interpreter::interpreter::InterpreterResult"
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "call_return"
                      |)
                    ]
                  |);
                  Value.Tuple
                    [ M.read (| context |); M.read (| frame |); M.read (| interpreter_result |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_call_return :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "call_return" (call_return EXT DB).
        
        (*
            pub fn insert_call_outcome(
                &self,
                context: &mut Context<EXT, DB>,
                frame: &mut Frame,
                shared_memory: &mut SharedMemory,
                outcome: CallOutcome,
            ) -> Result<(), EVMError<DB::Error>> {
                (self.insert_call_outcome)(context, frame, shared_memory, outcome)
            }
        *)
        Definition insert_call_outcome
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; frame; shared_memory; outcome ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let frame := M.alloc (| frame |) in
              let shared_memory := M.alloc (| shared_memory |) in
              let outcome := M.alloc (| outcome |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply (Ty.path "&mut") [] [ Ty.path "revm::frame::Frame" ];
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.path "revm_interpreter::interpreter::shared_memory::SharedMemory" ];
                        Ty.path "revm_interpreter::interpreter_action::call_outcome::CallOutcome"
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "insert_call_outcome"
                      |)
                    ]
                  |);
                  Value.Tuple
                    [
                      M.read (| context |);
                      M.read (| frame |);
                      M.read (| shared_memory |);
                      M.read (| outcome |)
                    ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_insert_call_outcome :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "insert_call_outcome" (insert_call_outcome EXT DB).
        
        (*
            pub fn create(
                &self,
                context: &mut Context<EXT, DB>,
                inputs: Box<CreateInputs>,
            ) -> Result<FrameOrResult, EVMError<DB::Error>> {
                (self.create)(context, inputs)
            }
        *)
        Definition create
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; inputs ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let inputs := M.alloc (| inputs |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [
                            Ty.path
                              "revm_interpreter::interpreter_action::create_inputs::CreateInputs";
                            Ty.path "alloc::alloc::Global"
                          ]
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "create"
                      |)
                    ]
                  |);
                  Value.Tuple [ M.read (| context |); M.read (| inputs |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_create :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "create" (create EXT DB).
        
        (*
            pub fn create_return(
                &self,
                context: &mut Context<EXT, DB>,
                frame: Box<CreateFrame>,
                interpreter_result: InterpreterResult,
            ) -> Result<CreateOutcome, EVMError<DB::Error>> {
                (self.create_return)(context, frame, interpreter_result)
            }
        *)
        Definition create_return
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; frame; interpreter_result ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let frame := M.alloc (| frame |) in
              let interpreter_result := M.alloc (| interpreter_result |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [ Ty.path "revm::frame::CreateFrame"; Ty.path "alloc::alloc::Global" ];
                        Ty.path "revm_interpreter::interpreter::InterpreterResult"
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "create_return"
                      |)
                    ]
                  |);
                  Value.Tuple
                    [ M.read (| context |); M.read (| frame |); M.read (| interpreter_result |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_create_return :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "create_return" (create_return EXT DB).
        
        (*
            pub fn insert_create_outcome(
                &self,
                context: &mut Context<EXT, DB>,
                frame: &mut Frame,
                outcome: CreateOutcome,
            ) -> Result<(), EVMError<DB::Error>> {
                (self.insert_create_outcome)(context, frame, outcome)
            }
        *)
        Definition insert_create_outcome
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; frame; outcome ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let frame := M.alloc (| frame |) in
              let outcome := M.alloc (| outcome |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply (Ty.path "&mut") [] [ Ty.path "revm::frame::Frame" ];
                        Ty.path
                          "revm_interpreter::interpreter_action::create_outcome::CreateOutcome"
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "insert_create_outcome"
                      |)
                    ]
                  |);
                  Value.Tuple [ M.read (| context |); M.read (| frame |); M.read (| outcome |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_insert_create_outcome :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction
            (Self EXT DB)
            "insert_create_outcome"
            (insert_create_outcome EXT DB).
        
        (*
            pub fn eofcreate(
                &self,
                context: &mut Context<EXT, DB>,
                inputs: Box<EOFCreateInput>,
            ) -> Result<FrameOrResult, EVMError<DB::Error>> {
                (self.eofcreate)(context, inputs)
            }
        *)
        Definition eofcreate
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; inputs ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let inputs := M.alloc (| inputs |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [
                            Ty.path
                              "revm_interpreter::interpreter_action::eof_create_inputs::EOFCreateInput";
                            Ty.path "alloc::alloc::Global"
                          ]
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "eofcreate"
                      |)
                    ]
                  |);
                  Value.Tuple [ M.read (| context |); M.read (| inputs |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_eofcreate :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "eofcreate" (eofcreate EXT DB).
        
        (*
            pub fn eofcreate_return(
                &self,
                context: &mut Context<EXT, DB>,
                frame: Box<EOFCreateFrame>,
                interpreter_result: InterpreterResult,
            ) -> Result<EOFCreateOutcome, EVMError<DB::Error>> {
                (self.eofcreate_return)(context, frame, interpreter_result)
            }
        *)
        Definition eofcreate_return
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; frame; interpreter_result ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let frame := M.alloc (| frame |) in
              let interpreter_result := M.alloc (| interpreter_result |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [ Ty.path "revm::frame::EOFCreateFrame"; Ty.path "alloc::alloc::Global" ];
                        Ty.path "revm_interpreter::interpreter::InterpreterResult"
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "eofcreate_return"
                      |)
                    ]
                  |);
                  Value.Tuple
                    [ M.read (| context |); M.read (| frame |); M.read (| interpreter_result |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_eofcreate_return :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction (Self EXT DB) "eofcreate_return" (eofcreate_return EXT DB).
        
        (*
            pub fn insert_eofcreate_outcome(
                &self,
                context: &mut Context<EXT, DB>,
                frame: &mut Frame,
                outcome: EOFCreateOutcome,
            ) -> Result<(), EVMError<DB::Error>> {
                (self.insert_eofcreate_outcome)(context, frame, outcome)
            }
        *)
        Definition insert_eofcreate_outcome
            (EXT DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self EXT DB in
          match ε, τ, α with
          | [], [], [ self; context; frame; outcome ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let context := M.alloc (| context |) in
              let frame := M.alloc (| frame |) in
              let outcome := M.alloc (| outcome |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::function::Fn",
                  Ty.dyn
                    [
                      ("existential predicate with variables", []);
                      ("existential predicate with variables", [])
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&mut")
                          []
                          [ Ty.apply (Ty.path "revm::context::Context") [] [ EXT; DB ] ];
                        Ty.apply (Ty.path "&mut") [] [ Ty.path "revm::frame::Frame" ];
                        Ty.path
                          "revm_interpreter::interpreter_action::eof_create_outcome::EOFCreateOutcome"
                      ]
                  ],
                  "call",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "alloc::sync::Arc")
                        []
                        [
                          Ty.dyn
                            [
                              ("existential predicate with variables", []);
                              ("existential predicate with variables", [])
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::handler::handle_types::execution::ExecutionHandler",
                        "insert_eofcreate_outcome"
                      |)
                    ]
                  |);
                  Value.Tuple [ M.read (| context |); M.read (| frame |); M.read (| outcome |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_insert_eofcreate_outcome :
          forall (EXT DB : Ty.t),
          M.IsAssociatedFunction
            (Self EXT DB)
            "insert_eofcreate_outcome"
            (insert_eofcreate_outcome EXT DB).
      End Impl_revm_handler_handle_types_execution_ExecutionHandler_EXT_DB.
      
    End execution.
  End handle_types.
End handler.
