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

Module db.
  Module components.
    Module block_hash.
      (* Trait *)
      (* Empty module 'BlockHash' *)
      
      Module underscore.
        Module Impl_revm_primitives_db_components_block_hash_BlockHash_where_revm_primitives_db_components_block_hash_BlockHash_T_where_core_marker_Sized_T_for_ref_mut_T.
          Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
          
          (* #[auto_impl(&mut, Box)] *)
          Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
          
          (* #[auto_impl(&mut, Box)] *)
          Definition block_hash
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self; number ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let number := M.alloc (| number |) in
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHash",
                    T,
                    [],
                    "block_hash",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| number |) ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "revm_primitives::db::components::block_hash::BlockHash"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("Error", InstanceField.Ty (_Error T));
                ("block_hash", InstanceField.Method (block_hash T))
              ].
        End Impl_revm_primitives_db_components_block_hash_BlockHash_where_revm_primitives_db_components_block_hash_BlockHash_T_where_core_marker_Sized_T_for_ref_mut_T.
        Module Impl_revm_primitives_db_components_block_hash_BlockHash_where_revm_primitives_db_components_block_hash_BlockHash_T_where_core_marker_Sized_T_for_alloc_boxed_Box_T_alloc_alloc_Global.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "alloc::boxed::Box") [] [ T; Ty.path "alloc::alloc::Global" ].
          
          (* #[auto_impl(&mut, Box)] *)
          Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
          
          (* #[auto_impl(&mut, Box)] *)
          Definition block_hash
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self; number ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let number := M.alloc (| number |) in
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHash",
                    T,
                    [],
                    "block_hash",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| number |) ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "revm_primitives::db::components::block_hash::BlockHash"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("Error", InstanceField.Ty (_Error T));
                ("block_hash", InstanceField.Method (block_hash T))
              ].
        End Impl_revm_primitives_db_components_block_hash_BlockHash_where_revm_primitives_db_components_block_hash_BlockHash_T_where_core_marker_Sized_T_for_alloc_boxed_Box_T_alloc_alloc_Global.
        Module Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_ref__T.
          Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition block_hash
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self; number ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let number := M.alloc (| number |) in
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHashRef",
                    T,
                    [],
                    "block_hash",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| number |) ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "revm_primitives::db::components::block_hash::BlockHashRef"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("Error", InstanceField.Ty (_Error T));
                ("block_hash", InstanceField.Method (block_hash T))
              ].
        End Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_ref__T.
        Module Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_ref_mut_T.
          Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&mut") [] [ T ].
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition block_hash
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self; number ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let number := M.alloc (| number |) in
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHashRef",
                    T,
                    [],
                    "block_hash",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| number |) ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "revm_primitives::db::components::block_hash::BlockHashRef"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("Error", InstanceField.Ty (_Error T));
                ("block_hash", InstanceField.Method (block_hash T))
              ].
        End Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_ref_mut_T.
        Module Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_alloc_boxed_Box_T_alloc_alloc_Global.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "alloc::boxed::Box") [] [ T; Ty.path "alloc::alloc::Global" ].
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition block_hash
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self; number ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let number := M.alloc (| number |) in
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHashRef",
                    T,
                    [],
                    "block_hash",
                    []
                  |),
                  [ M.read (| M.read (| self |) |); M.read (| number |) ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "revm_primitives::db::components::block_hash::BlockHashRef"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("Error", InstanceField.Ty (_Error T));
                ("block_hash", InstanceField.Method (block_hash T))
              ].
        End Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_alloc_boxed_Box_T_alloc_alloc_Global.
        Module Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_alloc_rc_Rc_T_alloc_alloc_Global.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "alloc::rc::Rc") [] [ T; Ty.path "alloc::alloc::Global" ].
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition block_hash
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self; number ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let number := M.alloc (| number |) in
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHashRef",
                    T,
                    [],
                    "block_hash",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply (Ty.path "alloc::rc::Rc") [] [ T; Ty.path "alloc::alloc::Global" ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| number |)
                  ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "revm_primitives::db::components::block_hash::BlockHashRef"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("Error", InstanceField.Ty (_Error T));
                ("block_hash", InstanceField.Method (block_hash T))
              ].
        End Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_alloc_rc_Rc_T_alloc_alloc_Global.
        Module Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_alloc_sync_Arc_T_alloc_alloc_Global.
          Definition Self (T : Ty.t) : Ty.t :=
            Ty.apply (Ty.path "alloc::sync::Arc") [] [ T; Ty.path "alloc::alloc::Global" ].
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
          
          (* #[auto_impl(&, &mut, Box, Rc, Arc)] *)
          Definition block_hash
              (T : Ty.t)
              (ε : list Value.t)
              (τ : list Ty.t)
              (α : list Value.t)
              : M :=
            let Self : Ty.t := Self T in
            match ε, τ, α with
            | [], [], [ self; number ] =>
              ltac:(M.monadic
                (let self := M.alloc (| self |) in
                let number := M.alloc (| number |) in
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHashRef",
                    T,
                    [],
                    "block_hash",
                    []
                  |),
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::deref::Deref",
                        Ty.apply
                          (Ty.path "alloc::sync::Arc")
                          []
                          [ T; Ty.path "alloc::alloc::Global" ],
                        [],
                        "deref",
                        []
                      |),
                      [ M.read (| self |) ]
                    |);
                    M.read (| number |)
                  ]
                |)))
            | _, _, _ => M.impossible "wrong number of arguments"
            end.
          
          Axiom Implements :
            forall (T : Ty.t),
            M.IsTraitInstance
              "revm_primitives::db::components::block_hash::BlockHashRef"
              (Self T)
              (* Trait polymorphic types *) []
              (* Instance *)
              [
                ("Error", InstanceField.Ty (_Error T));
                ("block_hash", InstanceField.Method (block_hash T))
              ].
        End Impl_revm_primitives_db_components_block_hash_BlockHashRef_where_revm_primitives_db_components_block_hash_BlockHashRef_T_where_core_marker_Sized_T_for_alloc_sync_Arc_T_alloc_alloc_Global.
      End underscore.
      
      
      (* Trait *)
      (* Empty module 'BlockHashRef' *)
      
      
      
      
      
      
      Module Impl_revm_primitives_db_components_block_hash_BlockHash_where_revm_primitives_db_components_block_hash_BlockHashRef_T_for_ref__T.
        Definition Self (T : Ty.t) : Ty.t := Ty.apply (Ty.path "&") [] [ T ].
        
        (*     type Error = <T as BlockHashRef>::Error; *)
        Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
        
        (*
            fn block_hash(&mut self, number: U256) -> Result<B256, Self::Error> {
                BlockHashRef::block_hash( *self, number)
            }
        *)
        Definition block_hash
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self; number ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let number := M.alloc (| number |) in
              M.call_closure (|
                M.get_trait_method (|
                  "revm_primitives::db::components::block_hash::BlockHashRef",
                  T,
                  [],
                  "block_hash",
                  []
                |),
                [ M.read (| M.read (| self |) |); M.read (| number |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "revm_primitives::db::components::block_hash::BlockHash"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Error", InstanceField.Ty (_Error T));
              ("block_hash", InstanceField.Method (block_hash T))
            ].
      End Impl_revm_primitives_db_components_block_hash_BlockHash_where_revm_primitives_db_components_block_hash_BlockHashRef_T_for_ref__T.
      
      Module Impl_revm_primitives_db_components_block_hash_BlockHash_where_revm_primitives_db_components_block_hash_BlockHashRef_T_for_alloc_sync_Arc_T_alloc_alloc_Global.
        Definition Self (T : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "alloc::sync::Arc") [] [ T; Ty.path "alloc::alloc::Global" ].
        
        (*     type Error = <T as BlockHashRef>::Error; *)
        Definition _Error (T : Ty.t) : Ty.t := Ty.associated.
        
        (*
            fn block_hash(&mut self, number: U256) -> Result<B256, Self::Error> {
                self.deref().block_hash(number)
            }
        *)
        Definition block_hash
            (T : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self T in
          match ε, τ, α with
          | [], [], [ self; number ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let number := M.alloc (| number |) in
              M.call_closure (|
                M.get_trait_method (|
                  "revm_primitives::db::components::block_hash::BlockHashRef",
                  Ty.apply (Ty.path "alloc::sync::Arc") [] [ T; Ty.path "alloc::alloc::Global" ],
                  [],
                  "block_hash",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::Deref",
                      Ty.apply
                        (Ty.path "&mut")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloc::sync::Arc")
                            []
                            [ T; Ty.path "alloc::alloc::Global" ]
                        ],
                      [],
                      "deref",
                      []
                    |),
                    [ self ]
                  |);
                  M.read (| number |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (T : Ty.t),
          M.IsTraitInstance
            "revm_primitives::db::components::block_hash::BlockHash"
            (Self T)
            (* Trait polymorphic types *) []
            (* Instance *)
            [
              ("Error", InstanceField.Ty (_Error T));
              ("block_hash", InstanceField.Method (block_hash T))
            ].
      End Impl_revm_primitives_db_components_block_hash_BlockHash_where_revm_primitives_db_components_block_hash_BlockHashRef_T_for_alloc_sync_Arc_T_alloc_alloc_Global.
    End block_hash.
  End components.
End db.
