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

Module host.
  Module dummy.
    (* StructRecord
      {
        name := "DummyHost";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("env", Ty.path "revm_primitives::env::Env");
            ("storage",
              Ty.apply
                (Ty.path "std::collections::hash::map::HashMap")
                []
                [
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [];
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [];
                  Ty.path "std::hash::random::RandomState"
                ]);
            ("transient_storage",
              Ty.apply
                (Ty.path "std::collections::hash::map::HashMap")
                []
                [
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [];
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [];
                  Ty.path "std::hash::random::RandomState"
                ]);
            ("log",
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.apply
                    (Ty.path "alloy_primitives::log::Log")
                    []
                    [ Ty.path "alloy_primitives::log::LogData" ];
                  Ty.path "alloc::alloc::Global"
                ])
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_revm_interpreter_host_dummy_DummyHost.
      Definition Self : Ty.t := Ty.path "revm_interpreter::host::dummy::DummyHost".
      
      (* 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_interpreter::host::dummy::DummyHost"
              [
                ("env",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm_primitives::env::Env",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "env"
                      |)
                    ]
                  |));
                ("storage",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "storage"
                      |)
                    ]
                  |));
                ("transient_storage",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "transient_storage"
                      |)
                    ]
                  |));
                ("log",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloy_primitives::log::Log")
                            []
                            [ Ty.path "alloy_primitives::log::LogData" ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "log"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_revm_interpreter_host_dummy_DummyHost.
    
    Module Impl_core_fmt_Debug_for_revm_interpreter_host_dummy_DummyHost.
      Definition Self : Ty.t := Ty.path "revm_interpreter::host::dummy::DummyHost".
      
      (* 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_field4_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "DummyHost" |);
                M.read (| Value.String "env" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::host::dummy::DummyHost",
                  "env"
                |);
                M.read (| Value.String "storage" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::host::dummy::DummyHost",
                  "storage"
                |);
                M.read (| Value.String "transient_storage" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::host::dummy::DummyHost",
                  "transient_storage"
                |);
                M.read (| Value.String "log" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_interpreter::host::dummy::DummyHost",
                    "log"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_revm_interpreter_host_dummy_DummyHost.
    
    Module Impl_core_default_Default_for_revm_interpreter_host_dummy_DummyHost.
      Definition Self : Ty.t := Ty.path "revm_interpreter::host::dummy::DummyHost".
      
      (* Default *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "revm_interpreter::host::dummy::DummyHost"
              [
                ("env",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "revm_primitives::env::Env",
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("storage",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("transient_storage",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("log",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloy_primitives::log::Log")
                            []
                            [ Ty.path "alloy_primitives::log::LogData" ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |))
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::default::Default"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method default) ].
    End Impl_core_default_Default_for_revm_interpreter_host_dummy_DummyHost.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_interpreter_host_dummy_DummyHost.
      Definition Self : Ty.t := Ty.path "revm_interpreter::host::dummy::DummyHost".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_interpreter_host_dummy_DummyHost.
    
    Module Impl_core_cmp_PartialEq_for_revm_interpreter_host_dummy_DummyHost.
      Definition Self : Ty.t := Ty.path "revm_interpreter::host::dummy::DummyHost".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            LogicalOp.and (|
              LogicalOp.and (|
                LogicalOp.and (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path "revm_primitives::env::Env",
                      [ Ty.path "revm_primitives::env::Env" ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "env"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "env"
                      |)
                    ]
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [
                          Ty.apply
                            (Ty.path "std::collections::hash::map::HashMap")
                            []
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [];
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [];
                              Ty.path "std::hash::random::RandomState"
                            ]
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::host::dummy::DummyHost",
                          "storage"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm_interpreter::host::dummy::DummyHost",
                          "storage"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      [
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "std::hash::random::RandomState"
                          ]
                      ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "transient_storage"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "transient_storage"
                      |)
                    ]
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloy_primitives::log::Log")
                          []
                          [ Ty.path "alloy_primitives::log::LogData" ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloy_primitives::log::Log")
                            []
                            [ Ty.path "alloy_primitives::log::LogData" ];
                          Ty.path "alloc::alloc::Global"
                        ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_interpreter::host::dummy::DummyHost",
                      "log"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_interpreter::host::dummy::DummyHost",
                      "log"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_revm_interpreter_host_dummy_DummyHost.
    
    Module Impl_core_cmp_Eq_for_revm_interpreter_host_dummy_DummyHost.
      Definition Self : Ty.t := Ty.path "revm_interpreter::host::dummy::DummyHost".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        Value.DeclaredButUndefined,
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                Value.DeclaredButUndefined,
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        Value.DeclaredButUndefined,
                                        [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_revm_interpreter_host_dummy_DummyHost.
    
    Module Impl_revm_interpreter_host_dummy_DummyHost.
      Definition Self : Ty.t := Ty.path "revm_interpreter::host::dummy::DummyHost".
      
      (*
          pub fn new(env: Env) -> Self {
              Self {
                  env,
                  ..Default::default()
              }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ env ] =>
          ltac:(M.monadic
            (let env := M.alloc (| env |) in
            M.struct_record_update
              (M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "revm_interpreter::host::dummy::DummyHost",
                  [],
                  "default",
                  []
                |),
                []
              |))
              [ ("env", M.read (| env |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub fn clear(&mut self) {
              self.storage.clear();
              self.log.clear();
          }
      *)
      Definition clear (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      "clear",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "storage"
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloy_primitives::log::Log")
                            []
                            [ Ty.path "alloy_primitives::log::LogData" ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      "clear",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "log"
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_clear : M.IsAssociatedFunction Self "clear" clear.
    End Impl_revm_interpreter_host_dummy_DummyHost.
    
    Module Impl_revm_interpreter_host_Host_for_revm_interpreter_host_dummy_DummyHost.
      Definition Self : Ty.t := Ty.path "revm_interpreter::host::dummy::DummyHost".
      
      (*
          fn env(&self) -> &Env {
              &self.env
          }
      *)
      Definition env (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_interpreter::host::dummy::DummyHost",
              "env"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn env_mut(&mut self) -> &mut Env {
              &mut self.env
          }
      *)
      Definition env_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_interpreter::host::dummy::DummyHost",
              "env"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn load_account(&mut self, _address: Address) -> Option<LoadAccountResult> {
              Some(LoadAccountResult::default())
          }
      *)
      Definition load_account (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _address := M.alloc (| _address |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_interpreter::host::LoadAccountResult",
                    [],
                    "default",
                    []
                  |),
                  []
                |)
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn block_hash(&mut self, _number: U256) -> Option<B256> {
              Some(B256::ZERO)
          }
      *)
      Definition block_hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _number ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _number := M.alloc (| _number |) in
            Value.StructTuple
              "core::option::Option::Some"
              [ M.read (| M.get_constant (| "alloy_primitives::bits::fixed::ZERO" |) |) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn balance(&mut self, _address: Address) -> Option<(U256, bool)> {
              Some((U256::ZERO, false))
          }
      *)
      Definition balance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _address := M.alloc (| _address |) in
            Value.StructTuple
              "core::option::Option::Some"
              [ Value.Tuple [ M.read (| M.get_constant (| "ruint::ZERO" |) |); Value.Bool false ]
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn code(&mut self, _address: Address) -> Option<(Bytecode, bool)> {
              Some((Bytecode::default(), false))
          }
      *)
      Definition code (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _address := M.alloc (| _address |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                Value.Tuple
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "revm_primitives::bytecode::Bytecode",
                        [],
                        "default",
                        []
                      |),
                      []
                    |);
                    Value.Bool false
                  ]
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn code_hash(&mut self, __address: Address) -> Option<(B256, bool)> {
              Some((KECCAK_EMPTY, false))
          }
      *)
      Definition code_hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; __address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let __address := M.alloc (| __address |) in
            Value.StructTuple
              "core::option::Option::Some"
              [
                Value.Tuple
                  [
                    M.read (| M.get_constant (| "revm_primitives::utilities::KECCAK_EMPTY" |) |);
                    Value.Bool false
                  ]
              ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn sload(&mut self, __address: Address, index: U256) -> Option<(U256, bool)> {
              match self.storage.entry(index) {
                  Entry::Occupied(entry) => Some(( *entry.get(), false)),
                  Entry::Vacant(entry) => {
                      entry.insert(U256::ZERO);
                      Some((U256::ZERO, true))
                  }
              }
          }
      *)
      Definition sload (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; __address; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let __address := M.alloc (| __address |) in
            let index := M.alloc (| index |) in
            M.read (|
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      "entry",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "storage"
                      |);
                      M.read (| index |)
                    ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "std::collections::hash::map::Entry::Occupied",
                          0
                        |) in
                      let entry := M.copy (| γ0_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.Tuple
                              [
                                M.read (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "std::collections::hash::map::OccupiedEntry")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [];
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            []
                                        ],
                                      "get",
                                      []
                                    |),
                                    [ entry ]
                                  |)
                                |);
                                Value.Bool false
                              ]
                          ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "std::collections::hash::map::Entry::Vacant",
                          0
                        |) in
                      let entry := M.copy (| γ0_0 |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "std::collections::hash::map::VacantEntry")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [];
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    []
                                ],
                              "insert",
                              []
                            |),
                            [ M.read (| entry |); M.read (| M.get_constant (| "ruint::ZERO" |) |) ]
                          |)
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.Tuple
                              [ M.read (| M.get_constant (| "ruint::ZERO" |) |); Value.Bool true ]
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn sstore(&mut self, _address: Address, index: U256, value: U256) -> Option<SStoreResult> {
              let (present, is_cold) = match self.storage.entry(index) {
                  Entry::Occupied(mut entry) => (entry.insert(value), false),
                  Entry::Vacant(entry) => {
                      entry.insert(value);
                      (U256::ZERO, true)
                  }
              };
      
              Some(SStoreResult {
                  original_value: U256::ZERO,
                  present_value: present,
                  new_value: value,
                  is_cold,
              })
          }
      *)
      Definition sstore (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _address; index; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _address := M.alloc (| _address |) in
            let index := M.alloc (| index |) in
            let value := M.alloc (| value |) in
            M.read (|
              M.match_operator (|
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "entry",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::host::dummy::DummyHost",
                          "storage"
                        |);
                        M.read (| index |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "std::collections::hash::map::Entry::Occupied",
                            0
                          |) in
                        let entry := M.copy (| γ0_0 |) in
                        M.alloc (|
                          Value.Tuple
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "std::collections::hash::map::OccupiedEntry")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [];
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        []
                                    ],
                                  "insert",
                                  []
                                |),
                                [ entry; M.read (| value |) ]
                              |);
                              Value.Bool false
                            ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "std::collections::hash::map::Entry::Vacant",
                            0
                          |) in
                        let entry := M.copy (| γ0_0 |) in
                        let~ _ :=
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::VacantEntry")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                "insert",
                                []
                              |),
                              [ M.read (| entry |); M.read (| value |) ]
                            |)
                          |) in
                        M.alloc (|
                          Value.Tuple
                            [ M.read (| M.get_constant (| "ruint::ZERO" |) |); Value.Bool true ]
                        |)))
                  ]
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let present := M.copy (| γ0_0 |) in
                      let is_cold := M.copy (| γ0_1 |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            Value.StructRecord
                              "revm_interpreter::host::SStoreResult"
                              [
                                ("original_value", M.read (| M.get_constant (| "ruint::ZERO" |) |));
                                ("present_value", M.read (| present |));
                                ("new_value", M.read (| value |));
                                ("is_cold", M.read (| is_cold |))
                              ]
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn tload(&mut self, _address: Address, index: U256) -> U256 {
              self.transient_storage
                  .get(&index)
                  .copied()
                  .unwrap_or_default()
          }
      *)
      Definition tload (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _address; index ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _address := M.alloc (| _address |) in
            let index := M.alloc (| index |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      []
                  ],
                "unwrap_or_default",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              []
                          ]
                      ],
                    "copied",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "get",
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ]
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_interpreter::host::dummy::DummyHost",
                          "transient_storage"
                        |);
                        index
                      ]
                    |)
                  ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn tstore(&mut self, _address: Address, index: U256, value: U256) {
              self.transient_storage.insert(index, value);
          }
      *)
      Definition tstore (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _address; index; value ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _address := M.alloc (| _address |) in
            let index := M.alloc (| index |) in
            let value := M.alloc (| value |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "std::hash::random::RandomState"
                        ],
                      "insert",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_interpreter::host::dummy::DummyHost",
                        "transient_storage"
                      |);
                      M.read (| index |);
                      M.read (| value |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn log(&mut self, log: Log) {
              self.log.push(log)
          }
      *)
      Definition log (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; log ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let log := M.alloc (| log |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloy_primitives::log::Log")
                      []
                      [ Ty.path "alloy_primitives::log::LogData" ];
                    Ty.path "alloc::alloc::Global"
                  ],
                "push",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_interpreter::host::dummy::DummyHost",
                  "log"
                |);
                M.read (| log |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn selfdestruct(&mut self, _address: Address, _target: Address) -> Option<SelfDestructResult> {
              panic!("Selfdestruct is not supported for this host")
          }
      *)
      Definition selfdestruct (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; _address; _target ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let _address := M.alloc (| _address |) in
            let _target := M.alloc (| _target |) in
            M.never_to_any (|
              M.call_closure (|
                M.get_function (| "core::panicking::panic_fmt", [] |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "core::fmt::Arguments", "new_const", [] |),
                    [
                      M.alloc (|
                        Value.Array
                          [ M.read (| Value.String "Selfdestruct is not supported for this host" |)
                          ]
                      |)
                    ]
                  |)
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "revm_interpreter::host::Host"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("env", InstanceField.Method env);
            ("env_mut", InstanceField.Method env_mut);
            ("load_account", InstanceField.Method load_account);
            ("block_hash", InstanceField.Method block_hash);
            ("balance", InstanceField.Method balance);
            ("code", InstanceField.Method code);
            ("code_hash", InstanceField.Method code_hash);
            ("sload", InstanceField.Method sload);
            ("sstore", InstanceField.Method sstore);
            ("tload", InstanceField.Method tload);
            ("tstore", InstanceField.Method tstore);
            ("log", InstanceField.Method log);
            ("selfdestruct", InstanceField.Method selfdestruct)
          ].
    End Impl_revm_interpreter_host_Host_for_revm_interpreter_host_dummy_DummyHost.
  End dummy.
End host.
