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

Module db.
  Module components.
    (* StructRecord
      {
        name := "DatabaseComponents";
        const_params := [];
        ty_params := [ "S"; "BH" ];
        fields := [ ("state", S); ("block_hash", BH) ];
      } *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_S_where_core_fmt_Debug_BH_for_revm_primitives_db_components_DatabaseComponents_S_BH.
      Definition Self (S BH : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm_primitives::db::components::DatabaseComponents") [] [ S; BH ].
      
      (* Debug *)
      Definition fmt (S BH : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self S BH in
        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_field2_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "DatabaseComponents" |);
                M.read (| Value.String "state" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::db::components::DatabaseComponents",
                  "state"
                |);
                M.read (| Value.String "block_hash" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::db::components::DatabaseComponents",
                    "block_hash"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (S BH : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self S BH)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt S BH)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_S_where_core_fmt_Debug_BH_for_revm_primitives_db_components_DatabaseComponents_S_BH.
    
    (*
    Enum DatabaseComponentError
    {
      const_params := [];
      ty_params := [ "SE"; "BHE" ];
      variants :=
        [
          {
            name := "State";
            item := StructTuple [ SE ];
            discriminant := None;
          };
          {
            name := "BlockHash";
            item := StructTuple [ BHE ];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_where_core_fmt_Debug_SE_where_core_fmt_Debug_BHE_for_revm_primitives_db_components_DatabaseComponentError_SE_BHE.
      Definition Self (SE BHE : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm_primitives::db::components::DatabaseComponentError") [] [ SE; BHE ].
      
      (* Debug *)
      Definition fmt (SE BHE : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self SE BHE in
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm_primitives::db::components::DatabaseComponentError::State",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple_field1_finish",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "State" |); __self_0 ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm_primitives::db::components::DatabaseComponentError::BlockHash",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple_field1_finish",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "BlockHash" |); __self_0 ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (SE BHE : Ty.t),
        M.IsTraitInstance
          "core::fmt::Debug"
          (Self SE BHE)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method (fmt SE BHE)) ].
    End Impl_core_fmt_Debug_where_core_fmt_Debug_SE_where_core_fmt_Debug_BHE_for_revm_primitives_db_components_DatabaseComponentError_SE_BHE.
    
    Module Impl_revm_primitives_db_Database_where_revm_primitives_db_components_state_State_S_where_revm_primitives_db_components_block_hash_BlockHash_BH_for_revm_primitives_db_components_DatabaseComponents_S_BH.
      Definition Self (S BH : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm_primitives::db::components::DatabaseComponents") [] [ S; BH ].
      
      (*     type Error = DatabaseComponentError<S::Error, BH::Error>; *)
      Definition _Error (S BH : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "revm_primitives::db::components::DatabaseComponentError")
          []
          [ Ty.associated; Ty.associated ].
      
      (*
          fn basic(&mut self, address: Address) -> Result<Option<AccountInfo>, Self::Error> {
              self.state.basic(address).map_err(Self::Error::State)
          }
      *)
      Definition basic (S BH : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self S BH in
        match ε, τ, α with
        | [], [], [ self; address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "revm_primitives::state::AccountInfo" ];
                    Ty.associated
                  ],
                "map_err",
                [
                  Ty.apply
                    (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                    []
                    [ Ty.associated; Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply
                      (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                      []
                      [ Ty.associated; Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::state::State",
                    S,
                    [],
                    "basic",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::db::components::DatabaseComponents",
                      "state"
                    |);
                    M.read (| address |)
                  ]
                |);
                M.constructor_as_closure
                  "revm_primitives::db::components::DatabaseComponentError::State"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn code_by_hash(&mut self, code_hash: B256) -> Result<Bytecode, Self::Error> {
              self.state
                  .code_by_hash(code_hash)
                  .map_err(Self::Error::State)
          }
      *)
      Definition code_by_hash
          (S BH : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self S BH in
        match ε, τ, α with
        | [], [], [ self; code_hash ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let code_hash := M.alloc (| code_hash |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.path "revm_primitives::bytecode::Bytecode"; Ty.associated ],
                "map_err",
                [
                  Ty.apply
                    (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                    []
                    [ Ty.associated; Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply
                      (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                      []
                      [ Ty.associated; Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::state::State",
                    S,
                    [],
                    "code_by_hash",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::db::components::DatabaseComponents",
                      "state"
                    |);
                    M.read (| code_hash |)
                  ]
                |);
                M.constructor_as_closure
                  "revm_primitives::db::components::DatabaseComponentError::State"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn storage(&mut self, address: Address, index: U256) -> Result<U256, Self::Error> {
              self.state
                  .storage(address, index)
                  .map_err(Self::Error::State)
          }
      *)
      Definition storage (S BH : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self S BH in
        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::result::Result")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [];
                    Ty.associated
                  ],
                "map_err",
                [
                  Ty.apply
                    (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                    []
                    [ Ty.associated; Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply
                      (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                      []
                      [ Ty.associated; Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::state::State",
                    S,
                    [],
                    "storage",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::db::components::DatabaseComponents",
                      "state"
                    |);
                    M.read (| address |);
                    M.read (| index |)
                  ]
                |);
                M.constructor_as_closure
                  "revm_primitives::db::components::DatabaseComponentError::State"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn block_hash(&mut self, number: U256) -> Result<B256, Self::Error> {
              self.block_hash
                  .block_hash(number)
                  .map_err(Self::Error::BlockHash)
          }
      *)
      Definition block_hash
          (S BH : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self S BH 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_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [];
                    Ty.associated
                  ],
                "map_err",
                [
                  Ty.apply
                    (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                    []
                    [ Ty.associated; Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply
                      (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                      []
                      [ Ty.associated; Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHash",
                    BH,
                    [],
                    "block_hash",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::db::components::DatabaseComponents",
                      "block_hash"
                    |);
                    M.read (| number |)
                  ]
                |);
                M.constructor_as_closure
                  "revm_primitives::db::components::DatabaseComponentError::BlockHash"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (S BH : Ty.t),
        M.IsTraitInstance
          "revm_primitives::db::Database"
          (Self S BH)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Error", InstanceField.Ty (_Error S BH));
            ("basic", InstanceField.Method (basic S BH));
            ("code_by_hash", InstanceField.Method (code_by_hash S BH));
            ("storage", InstanceField.Method (storage S BH));
            ("block_hash", InstanceField.Method (block_hash S BH))
          ].
    End Impl_revm_primitives_db_Database_where_revm_primitives_db_components_state_State_S_where_revm_primitives_db_components_block_hash_BlockHash_BH_for_revm_primitives_db_components_DatabaseComponents_S_BH.
    
    Module Impl_revm_primitives_db_DatabaseRef_where_revm_primitives_db_components_state_StateRef_S_where_revm_primitives_db_components_block_hash_BlockHashRef_BH_for_revm_primitives_db_components_DatabaseComponents_S_BH.
      Definition Self (S BH : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm_primitives::db::components::DatabaseComponents") [] [ S; BH ].
      
      (*     type Error = DatabaseComponentError<S::Error, BH::Error>; *)
      Definition _Error (S BH : Ty.t) : Ty.t :=
        Ty.apply
          (Ty.path "revm_primitives::db::components::DatabaseComponentError")
          []
          [ Ty.associated; Ty.associated ].
      
      (*
          fn basic_ref(&self, address: Address) -> Result<Option<AccountInfo>, Self::Error> {
              self.state.basic(address).map_err(Self::Error::State)
          }
      *)
      Definition basic_ref
          (S BH : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self S BH in
        match ε, τ, α with
        | [], [], [ self; address ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let address := M.alloc (| address |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "revm_primitives::state::AccountInfo" ];
                    Ty.associated
                  ],
                "map_err",
                [
                  Ty.apply
                    (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                    []
                    [ Ty.associated; Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply
                      (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                      []
                      [ Ty.associated; Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::state::StateRef",
                    S,
                    [],
                    "basic",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::db::components::DatabaseComponents",
                      "state"
                    |);
                    M.read (| address |)
                  ]
                |);
                M.constructor_as_closure
                  "revm_primitives::db::components::DatabaseComponentError::State"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn code_by_hash_ref(&self, code_hash: B256) -> Result<Bytecode, Self::Error> {
              self.state
                  .code_by_hash(code_hash)
                  .map_err(Self::Error::State)
          }
      *)
      Definition code_by_hash_ref
          (S BH : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self S BH in
        match ε, τ, α with
        | [], [], [ self; code_hash ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let code_hash := M.alloc (| code_hash |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [ Ty.path "revm_primitives::bytecode::Bytecode"; Ty.associated ],
                "map_err",
                [
                  Ty.apply
                    (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                    []
                    [ Ty.associated; Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply
                      (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                      []
                      [ Ty.associated; Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::state::StateRef",
                    S,
                    [],
                    "code_by_hash",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::db::components::DatabaseComponents",
                      "state"
                    |);
                    M.read (| code_hash |)
                  ]
                |);
                M.constructor_as_closure
                  "revm_primitives::db::components::DatabaseComponentError::State"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn storage_ref(&self, address: Address, index: U256) -> Result<U256, Self::Error> {
              self.state
                  .storage(address, index)
                  .map_err(Self::Error::State)
          }
      *)
      Definition storage_ref
          (S BH : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self S BH in
        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::result::Result")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [];
                    Ty.associated
                  ],
                "map_err",
                [
                  Ty.apply
                    (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                    []
                    [ Ty.associated; Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply
                      (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                      []
                      [ Ty.associated; Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::state::StateRef",
                    S,
                    [],
                    "storage",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::db::components::DatabaseComponents",
                      "state"
                    |);
                    M.read (| address |);
                    M.read (| index |)
                  ]
                |);
                M.constructor_as_closure
                  "revm_primitives::db::components::DatabaseComponentError::State"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      (*
          fn block_hash_ref(&self, number: U256) -> Result<B256, Self::Error> {
              self.block_hash
                  .block_hash(number)
                  .map_err(Self::Error::BlockHash)
          }
      *)
      Definition block_hash_ref
          (S BH : Ty.t)
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        let Self : Ty.t := Self S BH 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_associated_function (|
                Ty.apply
                  (Ty.path "core::result::Result")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [];
                    Ty.associated
                  ],
                "map_err",
                [
                  Ty.apply
                    (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                    []
                    [ Ty.associated; Ty.associated ];
                  Ty.function
                    [ Ty.associated ]
                    (Ty.apply
                      (Ty.path "revm_primitives::db::components::DatabaseComponentError")
                      []
                      [ Ty.associated; Ty.associated ])
                ]
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "revm_primitives::db::components::block_hash::BlockHashRef",
                    BH,
                    [],
                    "block_hash",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::db::components::DatabaseComponents",
                      "block_hash"
                    |);
                    M.read (| number |)
                  ]
                |);
                M.constructor_as_closure
                  "revm_primitives::db::components::DatabaseComponentError::BlockHash"
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (S BH : Ty.t),
        M.IsTraitInstance
          "revm_primitives::db::DatabaseRef"
          (Self S BH)
          (* Trait polymorphic types *) []
          (* Instance *)
          [
            ("Error", InstanceField.Ty (_Error S BH));
            ("basic_ref", InstanceField.Method (basic_ref S BH));
            ("code_by_hash_ref", InstanceField.Method (code_by_hash_ref S BH));
            ("storage_ref", InstanceField.Method (storage_ref S BH));
            ("block_hash_ref", InstanceField.Method (block_hash_ref S BH))
          ].
    End Impl_revm_primitives_db_DatabaseRef_where_revm_primitives_db_components_state_StateRef_S_where_revm_primitives_db_components_block_hash_BlockHashRef_BH_for_revm_primitives_db_components_DatabaseComponents_S_BH.
    
    Module Impl_revm_primitives_db_DatabaseCommit_where_revm_primitives_db_DatabaseCommit_S_where_revm_primitives_db_components_block_hash_BlockHashRef_BH_for_revm_primitives_db_components_DatabaseComponents_S_BH.
      Definition Self (S BH : Ty.t) : Ty.t :=
        Ty.apply (Ty.path "revm_primitives::db::components::DatabaseComponents") [] [ S; BH ].
      
      (*
          fn commit(&mut self, changes: HashMap<Address, Account>) {
              self.state.commit(changes);
          }
      *)
      Definition commit (S BH : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        let Self : Ty.t := Self S BH in
        match ε, τ, α with
        | [], [], [ self; changes ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let changes := M.alloc (| changes |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "revm_primitives::db::DatabaseCommit",
                      S,
                      [],
                      "commit",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::db::components::DatabaseComponents",
                        "state"
                      |);
                      M.read (| changes |)
                    ]
                  |)
                |) in
              M.alloc (| Value.Tuple [] |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        forall (S BH : Ty.t),
        M.IsTraitInstance
          "revm_primitives::db::DatabaseCommit"
          (Self S BH)
          (* Trait polymorphic types *) []
          (* Instance *) [ ("commit", InstanceField.Method (commit S BH)) ].
    End Impl_revm_primitives_db_DatabaseCommit_where_revm_primitives_db_DatabaseCommit_S_where_revm_primitives_db_components_block_hash_BlockHashRef_BH_for_revm_primitives_db_components_DatabaseComponents_S_BH.
  End components.
End db.
