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

Module inspector.
  Module customprinter.
    (* StructRecord
      {
        name := "CustomPrintTracer";
        const_params := [];
        ty_params := [];
        fields := [ ("gas_inspector", Ty.path "revm::inspector::gas::GasInspector") ];
      } *)
    
    Module Impl_core_clone_Clone_for_revm_inspector_customprinter_CustomPrintTracer.
      Definition Self : Ty.t := Ty.path "revm::inspector::customprinter::CustomPrintTracer".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.StructRecord
              "revm::inspector::customprinter::CustomPrintTracer"
              [
                ("gas_inspector",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm::inspector::gas::GasInspector",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::inspector::customprinter::CustomPrintTracer",
                        "gas_inspector"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_revm_inspector_customprinter_CustomPrintTracer.
    
    Module Impl_core_fmt_Debug_for_revm_inspector_customprinter_CustomPrintTracer.
      Definition Self : Ty.t := Ty.path "revm::inspector::customprinter::CustomPrintTracer".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "core::fmt::Formatter",
                "debug_struct_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "CustomPrintTracer" |);
                M.read (| Value.String "gas_inspector" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::inspector::customprinter::CustomPrintTracer",
                    "gas_inspector"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_revm_inspector_customprinter_CustomPrintTracer.
    
    Module Impl_core_default_Default_for_revm_inspector_customprinter_CustomPrintTracer.
      Definition Self : Ty.t := Ty.path "revm::inspector::customprinter::CustomPrintTracer".
      
      (* Default *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "revm::inspector::customprinter::CustomPrintTracer"
              [
                ("gas_inspector",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "revm::inspector::gas::GasInspector",
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::default::Default"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method default) ].
    End Impl_core_default_Default_for_revm_inspector_customprinter_CustomPrintTracer.
    
    Module Impl_revm_inspector_Inspector_where_revm_primitives_db_Database_DB_DB_for_revm_inspector_customprinter_CustomPrintTracer.
      Definition Self (DB : Ty.t) : Ty.t :=
        Ty.path "revm::inspector::customprinter::CustomPrintTracer".
      
      (*
          fn initialize_interp(&mut self, interp: &mut Interpreter, context: &mut EvmContext<DB>) {
              self.gas_inspector.initialize_interp(interp, context);
          }
      *)
      Definition initialize_interp
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB 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.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "revm::inspector::Inspector",
                      Ty.path "revm::inspector::gas::GasInspector",
                      [ DB ],
                      "initialize_interp",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::inspector::customprinter::CustomPrintTracer",
                        "gas_inspector"
                      |);
                      M.read (| interp |);
                      M.read (| context |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn step(&mut self, interp: &mut Interpreter, context: &mut EvmContext<DB>) {
              let opcode = interp.current_opcode();
              let name = OpCode::name_by_op(opcode);
      
              let gas_remaining = self.gas_inspector.gas_remaining();
      
              let memory_size = interp.shared_memory.len();
      
              println!(
                  "depth:{}, PC:{}, gas:{:#x}({}), OPCODE: {:?}({:?})  refund:{:#x}({}) Stack:{:?}, Data size:{}",
                  context.journaled_state.depth(),
                  interp.program_counter(),
                  gas_remaining,
                  gas_remaining,
                  name,
                  opcode,
                  interp.gas.refunded(),
                  interp.gas.refunded(),
                  interp.stack.data(),
                  memory_size,
              );
      
              self.gas_inspector.step(interp, context);
          }
      *)
      Definition step (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB 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.read (|
              let~ opcode :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::Interpreter",
                      "current_opcode",
                      []
                    |),
                    [ M.read (| interp |) ]
                  |)
                |) in
              let~ name :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::opcode::OpCode",
                      "name_by_op",
                      []
                    |),
                    [ M.read (| opcode |) ]
                  |)
                |) in
              let~ gas_remaining :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm::inspector::gas::GasInspector",
                      "gas_remaining",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::inspector::customprinter::CustomPrintTracer",
                        "gas_inspector"
                      |)
                    ]
                  |)
                |) in
              let~ memory_size :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_interpreter::interpreter::shared_memory::SharedMemory",
                      "len",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| interp |),
                        "revm_interpreter::interpreter::Interpreter",
                        "shared_memory"
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "std::io::stdio::_print", [] |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Arguments",
                            "new_v1_formatted",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (| Value.String "depth:" |);
                                  M.read (| Value.String ", PC:" |);
                                  M.read (| Value.String ", gas:" |);
                                  M.read (| Value.String "(" |);
                                  M.read (| Value.String "), OPCODE: " |);
                                  M.read (| Value.String "(" |);
                                  M.read (| Value.String ")  refund:" |);
                                  M.read (| Value.String "(" |);
                                  M.read (| Value.String ") Stack:" |);
                                  M.read (| Value.String ", Data size:" |);
                                  M.read (| Value.String "
" |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "u64" ]
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm::journaled_state::JournaledState",
                                            "depth",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::deref::Deref",
                                                  Ty.apply
                                                    (Ty.path
                                                      "revm::context::evm_context::EvmContext")
                                                    []
                                                    [ DB ],
                                                  [],
                                                  "deref",
                                                  []
                                                |),
                                                [ M.read (| context |) ]
                                              |),
                                              "revm::context::inner_evm_context::InnerEvmContext",
                                              "journaled_state"
                                            |)
                                          ]
                                        |)
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "usize" ]
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_interpreter::interpreter::Interpreter",
                                            "program_counter",
                                            []
                                          |),
                                          [ M.read (| interp |) ]
                                        |)
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_lower_hex",
                                      [ Ty.path "u64" ]
                                    |),
                                    [ gas_remaining ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "u64" ]
                                    |),
                                    [ gas_remaining ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                                    |),
                                    [ name ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "u8" ]
                                    |),
                                    [ opcode ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_lower_hex",
                                      [ Ty.path "i64" ]
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_interpreter::gas::Gas",
                                            "refunded",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interp |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "gas"
                                            |)
                                          ]
                                        |)
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "i64" ]
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_interpreter::gas::Gas",
                                            "refunded",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interp |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "gas"
                                            |)
                                          ]
                                        |)
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "alloc::vec::Vec")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [];
                                                Ty.path "alloc::alloc::Global"
                                              ]
                                          ]
                                      ]
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_interpreter::interpreter::stack::Stack",
                                            "data",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| interp |),
                                              "revm_interpreter::interpreter::Interpreter",
                                              "stack"
                                            |)
                                          ]
                                        |)
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_display",
                                      [ Ty.path "usize" ]
                                    |),
                                    [ memory_size ]
                                  |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 0;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 0;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 1;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 0;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 2;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 4;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 3;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 0;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 4;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 0;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 5;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 0;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 6;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 4;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 7;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 0;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 8;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 0;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Placeholder",
                                      "new",
                                      []
                                    |),
                                    [
                                      Value.Integer IntegerKind.Usize 9;
                                      Value.UnicodeChar 32;
                                      Value.StructTuple "core::fmt::rt::Alignment::Unknown" [];
                                      Value.Integer IntegerKind.U32 0;
                                      Value.StructTuple "core::fmt::rt::Count::Implied" [];
                                      Value.StructTuple "core::fmt::rt::Count::Implied" []
                                    ]
                                  |)
                                ]
                            |);
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::rt::UnsafeArg",
                                "new",
                                []
                              |),
                              []
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "revm::inspector::Inspector",
                      Ty.path "revm::inspector::gas::GasInspector",
                      [ DB ],
                      "step",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::inspector::customprinter::CustomPrintTracer",
                        "gas_inspector"
                      |);
                      M.read (| interp |);
                      M.read (| context |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn step_end(&mut self, interp: &mut Interpreter, context: &mut EvmContext<DB>) {
              self.gas_inspector.step_end(interp, context);
          }
      *)
      Definition step_end (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB 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.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "revm::inspector::Inspector",
                      Ty.path "revm::inspector::gas::GasInspector",
                      [ DB ],
                      "step_end",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::inspector::customprinter::CustomPrintTracer",
                        "gas_inspector"
                      |);
                      M.read (| interp |);
                      M.read (| context |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn call_end(
              &mut self,
              context: &mut EvmContext<DB>,
              inputs: &CallInputs,
              outcome: CallOutcome,
          ) -> CallOutcome {
              self.gas_inspector.call_end(context, inputs, outcome)
          }
      *)
      Definition call_end (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB 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",
                Ty.path "revm::inspector::gas::GasInspector",
                [ DB ],
                "call_end",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::inspector::customprinter::CustomPrintTracer",
                  "gas_inspector"
                |);
                M.read (| context |);
                M.read (| inputs |);
                M.read (| outcome |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn create_end(
              &mut self,
              context: &mut EvmContext<DB>,
              inputs: &CreateInputs,
              outcome: CreateOutcome,
          ) -> CreateOutcome {
              self.gas_inspector.create_end(context, inputs, outcome)
          }
      *)
      Definition create_end (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self DB 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",
                Ty.path "revm::inspector::gas::GasInspector",
                [ DB ],
                "create_end",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm::inspector::customprinter::CustomPrintTracer",
                  "gas_inspector"
                |);
                M.read (| context |);
                M.read (| inputs |);
                M.read (| outcome |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn call(
              &mut self,
              _context: &mut EvmContext<DB>,
              inputs: &mut CallInputs,
          ) -> Option<CallOutcome> {
              println!(
                  "SM Address: {:?}, caller:{:?},target:{:?} is_static:{:?}, transfer:{:?}, input_size:{:?}",
                  inputs.bytecode_address,
                  inputs.caller,
                  inputs.target_address,
                  inputs.is_static,
                  inputs.value,
                  inputs.input.len(),
              );
              None
          }
      *)
      Definition call (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self 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.read (|
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "std::io::stdio::_print", [] |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Arguments",
                            "new_v1",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (| Value.String "SM Address: " |);
                                  M.read (| Value.String ", caller:" |);
                                  M.read (| Value.String ",target:" |);
                                  M.read (| Value.String " is_static:" |);
                                  M.read (| Value.String ", transfer:" |);
                                  M.read (| Value.String ", input_size:" |);
                                  M.read (| Value.String "
" |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "alloy_primitives::bits::address::Address" ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                        "bytecode_address"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "alloy_primitives::bits::address::Address" ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                        "caller"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "alloy_primitives::bits::address::Address" ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                        "target_address"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "bool" ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                        "is_static"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [
                                        Ty.path
                                          "revm_interpreter::interpreter_action::call_inputs::CallValue"
                                      ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                        "value"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "usize" ]
                                    |),
                                    [
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "bytes::bytes::Bytes",
                                            "len",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::ops::deref::Deref",
                                                Ty.path "alloy_primitives::bytes_::Bytes",
                                                [],
                                                "deref",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| inputs |),
                                                  "revm_interpreter::interpreter_action::call_inputs::CallInputs",
                                                  "input"
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn create(
              &mut self,
              _context: &mut EvmContext<DB>,
              inputs: &mut CreateInputs,
          ) -> Option<CreateOutcome> {
              println!(
                  "CREATE CALL: caller:{:?}, scheme:{:?}, value:{:?}, init_code:{:?}, gas:{:?}",
                  inputs.caller, inputs.scheme, inputs.value, inputs.init_code, inputs.gas_limit
              );
              None
          }
      *)
      Definition create (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self 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.read (|
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "std::io::stdio::_print", [] |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Arguments",
                            "new_v1",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (| Value.String "CREATE CALL: caller:" |);
                                  M.read (| Value.String ", scheme:" |);
                                  M.read (| Value.String ", value:" |);
                                  M.read (| Value.String ", init_code:" |);
                                  M.read (| Value.String ", gas:" |);
                                  M.read (| Value.String "
" |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "alloy_primitives::bits::address::Address" ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                        "caller"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "revm_primitives::env::CreateScheme" ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                        "scheme"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                        "value"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "alloy_primitives::bytes_::Bytes" ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                        "init_code"
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "u64" ]
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| inputs |),
                                        "revm_interpreter::interpreter_action::create_inputs::CreateInputs",
                                        "gas_limit"
                                      |)
                                    ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn selfdestruct(&mut self, contract: Address, target: Address, value: U256) {
              println!(
                  "SELFDESTRUCT: contract: {:?}, refund target: {:?}, value {:?}",
                  contract, target, value
              );
          }
      *)
      Definition selfdestruct
          (DB : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self DB 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.read (|
              let~ _ :=
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (| "std::io::stdio::_print", [] |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Arguments",
                            "new_v1",
                            []
                          |),
                          [
                            M.alloc (|
                              Value.Array
                                [
                                  M.read (| Value.String "SELFDESTRUCT: contract: " |);
                                  M.read (| Value.String ", refund target: " |);
                                  M.read (| Value.String ", value " |);
                                  M.read (| Value.String "
" |)
                                ]
                            |);
                            M.alloc (|
                              Value.Array
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "alloy_primitives::bits::address::Address" ]
                                    |),
                                    [ contract ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [ Ty.path "alloy_primitives::bits::address::Address" ]
                                    |),
                                    [ target ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "core::fmt::rt::Argument",
                                      "new_debug",
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ]
                                    |),
                                    [ value ]
                                  |)
                                ]
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (DB : Ty.t),
        M.IsTraitInstance
          "revm::inspector::Inspector"
          (Self DB)
          (* Trait polymorphic types *) [ (* DB *) DB ]
          (* Instance *)
          [
            ("initialize_interp", InstanceField.Method (initialize_interp DB));
            ("step", InstanceField.Method (step DB));
            ("step_end", InstanceField.Method (step_end DB));
            ("call_end", InstanceField.Method (call_end DB));
            ("create_end", InstanceField.Method (create_end DB));
            ("call", InstanceField.Method (call DB));
            ("create", InstanceField.Method (create DB));
            ("selfdestruct", InstanceField.Method (selfdestruct DB))
          ].
    End Impl_revm_inspector_Inspector_where_revm_primitives_db_Database_DB_DB_for_revm_inspector_customprinter_CustomPrintTracer.
  End customprinter.
End inspector.
