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

Module inspector.
  (* Trait *)
  Module Inspector.
    Definition initialize_interp
        (DB Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; interp; context ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let interp := M.alloc (| interp |) in
          let context := M.alloc (| context |) in
          M.read (|
            M.match_operator (|
              interp,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      context,
                      [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_initialize_interp :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "initialize_interp" (initialize_interp DB).
    Definition step (DB Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; interp; context ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let interp := M.alloc (| interp |) in
          let context := M.alloc (| context |) in
          M.read (|
            M.match_operator (|
              interp,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      context,
                      [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_step :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "step" (step DB).
    Definition step_end
        (DB Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; interp; context ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let interp := M.alloc (| interp |) in
          let context := M.alloc (| context |) in
          M.read (|
            M.match_operator (|
              interp,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      context,
                      [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_step_end :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "step_end" (step_end DB).
    Definition log (DB Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; context; log ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let context := M.alloc (| context |) in
          let log := M.alloc (| log |) in
          M.read (|
            M.match_operator (|
              context,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      log,
                      [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_log :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "log" (log DB).
    Definition call (DB Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      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.read (|
            M.match_operator (|
              context,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      inputs,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_call :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "call" (call DB).
    Definition call_end
        (DB Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; context; inputs; outcome ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let context := M.alloc (| context |) in
          let inputs := M.alloc (| inputs |) in
          let outcome := M.alloc (| outcome |) in
          M.read (|
            M.match_operator (|
              context,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (| inputs, [ fun γ => ltac:(M.monadic outcome) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_call_end :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "call_end" (call_end DB).
    Definition create (DB Self : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      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.read (|
            M.match_operator (|
              context,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      inputs,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_create :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "create" (create DB).
    Definition create_end
        (DB Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; context; inputs; outcome ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let context := M.alloc (| context |) in
          let inputs := M.alloc (| inputs |) in
          let outcome := M.alloc (| outcome |) in
          M.read (|
            M.match_operator (|
              context,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (| inputs, [ fun γ => ltac:(M.monadic outcome) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_create_end :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "create_end" (create_end DB).
    Definition eofcreate
        (DB Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      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.read (|
            M.match_operator (|
              context,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      inputs,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_eofcreate :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "eofcreate" (eofcreate DB).
    Definition eofcreate_end
        (DB Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; context; inputs; outcome ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let context := M.alloc (| context |) in
          let inputs := M.alloc (| inputs |) in
          let outcome := M.alloc (| outcome |) in
          M.read (|
            M.match_operator (|
              context,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (| inputs, [ fun γ => ltac:(M.monadic outcome) ] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_eofcreate_end :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "eofcreate_end" (eofcreate_end DB).
    Definition selfdestruct
        (DB Self : Ty.t)
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; contract; target; value ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let contract := M.alloc (| contract |) in
          let target := M.alloc (| target |) in
          let value := M.alloc (| value |) in
          M.read (|
            M.match_operator (|
              contract,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      target,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              value,
                              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom ProvidedMethod_selfdestruct :
      forall (DB : Ty.t),
      M.IsProvidedMethod "revm::inspector::Inspector" "selfdestruct" (selfdestruct DB).
  End Inspector.
  
  Module underscore.
    Module Impl_revm_inspector_Inspector_where_revm_primitives_db_Database_DB_where_revm_inspector_Inspector_T_DB_where_core_marker_Sized_T_DB_for_ref_mut_T.
      Definition Self (DB T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
      
      (* #[auto_impl(&mut, Box)] *)
      Definition initialize_interp
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; interp; context ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interp := M.alloc (| interp |) in
            let context := M.alloc (| context |) in
            M.call_closure (|
              M.get_trait_method (|
                "revm::inspector::Inspector",
                T,
                [ DB ],
                "initialize_interp",
                []
              |),
              [ M.read (| M.read (| self |) |); M.read (| interp |); M.read (| context |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition step (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; interp; context ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interp := M.alloc (| interp |) in
            let context := M.alloc (| context |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "step", [] |),
              [ M.read (| M.read (| self |) |); M.read (| interp |); M.read (| context |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition step_end (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; interp; context ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interp := M.alloc (| interp |) in
            let context := M.alloc (| context |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "step_end", [] |),
              [ M.read (| M.read (| self |) |); M.read (| interp |); M.read (| context |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition log (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; context; log ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let context := M.alloc (| context |) in
            let log := M.alloc (| log |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "log", [] |),
              [ M.read (| M.read (| self |) |); M.read (| context |); M.read (| log |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition call (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T 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 (| "revm::inspector::Inspector", T, [ DB ], "call", [] |),
              [ M.read (| M.read (| self |) |); M.read (| context |); M.read (| inputs |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition call_end (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; context; inputs; outcome ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            let outcome := M.alloc (| outcome |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "call_end", [] |),
              [
                M.read (| M.read (| self |) |);
                M.read (| context |);
                M.read (| inputs |);
                M.read (| outcome |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition create (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T 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 (| "revm::inspector::Inspector", T, [ DB ], "create", [] |),
              [ M.read (| M.read (| self |) |); M.read (| context |); M.read (| inputs |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition create_end
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; context; inputs; outcome ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            let outcome := M.alloc (| outcome |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "create_end", [] |),
              [
                M.read (| M.read (| self |) |);
                M.read (| context |);
                M.read (| inputs |);
                M.read (| outcome |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition eofcreate
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T 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 (| "revm::inspector::Inspector", T, [ DB ], "eofcreate", [] |),
              [ M.read (| M.read (| self |) |); M.read (| context |); M.read (| inputs |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition eofcreate_end
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; context; inputs; outcome ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            let outcome := M.alloc (| outcome |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "eofcreate_end", [] |),
              [
                M.read (| M.read (| self |) |);
                M.read (| context |);
                M.read (| inputs |);
                M.read (| outcome |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition selfdestruct
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; contract; target; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let contract := M.alloc (| contract |) in
            let target := M.alloc (| target |) in
            let value := M.alloc (| value |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "selfdestruct", [] |),
              [
                M.read (| M.read (| self |) |);
                M.read (| contract |);
                M.read (| target |);
                M.read (| value |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (DB T : Ty.t),
        M.IsTraitInstance
          "revm::inspector::Inspector"
          (Self DB T)
          (* Trait polymorphic types *) [ (* DB *) DB ]
          (* Instance *)
          [
            ("initialize_interp", InstanceField.Method (initialize_interp DB T));
            ("step", InstanceField.Method (step DB T));
            ("step_end", InstanceField.Method (step_end DB T));
            ("log", InstanceField.Method (log DB T));
            ("call", InstanceField.Method (call DB T));
            ("call_end", InstanceField.Method (call_end DB T));
            ("create", InstanceField.Method (create DB T));
            ("create_end", InstanceField.Method (create_end DB T));
            ("eofcreate", InstanceField.Method (eofcreate DB T));
            ("eofcreate_end", InstanceField.Method (eofcreate_end DB T));
            ("selfdestruct", InstanceField.Method (selfdestruct DB T))
          ].
    End Impl_revm_inspector_Inspector_where_revm_primitives_db_Database_DB_where_revm_inspector_Inspector_T_DB_where_core_marker_Sized_T_DB_for_ref_mut_T.
    Module Impl_revm_inspector_Inspector_where_revm_primitives_db_Database_DB_where_revm_inspector_Inspector_T_DB_where_core_marker_Sized_T_DB_for_alloc_boxed_Box_T_alloc_alloc_Global.
      Definition Self (DB T : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "alloc::boxed::Box") [] [ T; Ty.path "alloc::alloc::Global" ].
      
      (* #[auto_impl(&mut, Box)] *)
      Definition initialize_interp
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; interp; context ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interp := M.alloc (| interp |) in
            let context := M.alloc (| context |) in
            M.call_closure (|
              M.get_trait_method (|
                "revm::inspector::Inspector",
                T,
                [ DB ],
                "initialize_interp",
                []
              |),
              [ M.read (| M.read (| self |) |); M.read (| interp |); M.read (| context |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition step (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; interp; context ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interp := M.alloc (| interp |) in
            let context := M.alloc (| context |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "step", [] |),
              [ M.read (| M.read (| self |) |); M.read (| interp |); M.read (| context |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition step_end (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; interp; context ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let interp := M.alloc (| interp |) in
            let context := M.alloc (| context |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "step_end", [] |),
              [ M.read (| M.read (| self |) |); M.read (| interp |); M.read (| context |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition log (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; context; log ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let context := M.alloc (| context |) in
            let log := M.alloc (| log |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "log", [] |),
              [ M.read (| M.read (| self |) |); M.read (| context |); M.read (| log |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition call (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T 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 (| "revm::inspector::Inspector", T, [ DB ], "call", [] |),
              [ M.read (| M.read (| self |) |); M.read (| context |); M.read (| inputs |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition call_end (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; context; inputs; outcome ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            let outcome := M.alloc (| outcome |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "call_end", [] |),
              [
                M.read (| M.read (| self |) |);
                M.read (| context |);
                M.read (| inputs |);
                M.read (| outcome |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition create (DB T : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB T 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 (| "revm::inspector::Inspector", T, [ DB ], "create", [] |),
              [ M.read (| M.read (| self |) |); M.read (| context |); M.read (| inputs |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition create_end
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; context; inputs; outcome ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            let outcome := M.alloc (| outcome |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "create_end", [] |),
              [
                M.read (| M.read (| self |) |);
                M.read (| context |);
                M.read (| inputs |);
                M.read (| outcome |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition eofcreate
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T 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 (| "revm::inspector::Inspector", T, [ DB ], "eofcreate", [] |),
              [ M.read (| M.read (| self |) |); M.read (| context |); M.read (| inputs |) ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition eofcreate_end
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; context; inputs; outcome ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let context := M.alloc (| context |) in
            let inputs := M.alloc (| inputs |) in
            let outcome := M.alloc (| outcome |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "eofcreate_end", [] |),
              [
                M.read (| M.read (| self |) |);
                M.read (| context |);
                M.read (| inputs |);
                M.read (| outcome |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (* #[auto_impl(&mut, Box)] *)
      Definition selfdestruct
          (DB T : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB T in
        match ε, τ, α with
        | [], [], [ self; contract; target; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let contract := M.alloc (| contract |) in
            let target := M.alloc (| target |) in
            let value := M.alloc (| value |) in
            M.call_closure (|
              M.get_trait_method (| "revm::inspector::Inspector", T, [ DB ], "selfdestruct", [] |),
              [
                M.read (| M.read (| self |) |);
                M.read (| contract |);
                M.read (| target |);
                M.read (| value |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (DB T : Ty.t),
        M.IsTraitInstance
          "revm::inspector::Inspector"
          (Self DB T)
          (* Trait polymorphic types *) [ (* DB *) DB ]
          (* Instance *)
          [
            ("initialize_interp", InstanceField.Method (initialize_interp DB T));
            ("step", InstanceField.Method (step DB T));
            ("step_end", InstanceField.Method (step_end DB T));
            ("log", InstanceField.Method (log DB T));
            ("call", InstanceField.Method (call DB T));
            ("call_end", InstanceField.Method (call_end DB T));
            ("create", InstanceField.Method (create DB T));
            ("create_end", InstanceField.Method (create_end DB T));
            ("eofcreate", InstanceField.Method (eofcreate DB T));
            ("eofcreate_end", InstanceField.Method (eofcreate_end DB T));
            ("selfdestruct", InstanceField.Method (selfdestruct DB T))
          ].
    End Impl_revm_inspector_Inspector_where_revm_primitives_db_Database_DB_where_revm_inspector_Inspector_T_DB_where_core_marker_Sized_T_DB_for_alloc_boxed_Box_T_alloc_alloc_Global.
  End underscore.
  
End inspector.
