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

Module db.
  Module states.
    Module state_builder.
      (* StructRecord
        {
          name := "StateBuilder";
          const_params := [];
          ty_params := [ "DB" ];
          fields :=
            [
              ("database", DB);
              ("with_state_clear", Ty.path "bool");
              ("with_bundle_prestate",
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "revm::db::states::bundle_state::BundleState" ]);
              ("with_cache_prestate",
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "revm::db::states::cache::CacheState" ]);
              ("with_bundle_update", Ty.path "bool");
              ("with_background_transition_merge", Ty.path "bool");
              ("with_block_hashes",
                Ty.apply
                  (Ty.path "alloc::collections::btree::map::BTreeMap")
                  []
                  [
                    Ty.path "u64";
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [];
                    Ty.path "alloc::alloc::Global"
                  ])
            ];
        } *)
      
      Module Impl_core_clone_Clone_where_core_clone_Clone_DB_for_revm_db_states_state_builder_StateBuilder_DB.
        Definition Self (DB : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ].
        
        (* Clone *)
        Definition clone (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "revm::db::states::state_builder::StateBuilder"
                [
                  ("database",
                    M.call_closure (|
                      M.get_trait_method (| "core::clone::Clone", DB, [], "clone", [] |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::state_builder::StateBuilder",
                          "database"
                        |)
                      ]
                    |));
                  ("with_state_clear",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "bool",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::state_builder::StateBuilder",
                          "with_state_clear"
                        |)
                      ]
                    |));
                  ("with_bundle_prestate",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm::db::states::bundle_state::BundleState" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::state_builder::StateBuilder",
                          "with_bundle_prestate"
                        |)
                      ]
                    |));
                  ("with_cache_prestate",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm::db::states::cache::CacheState" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::state_builder::StateBuilder",
                          "with_cache_prestate"
                        |)
                      ]
                    |));
                  ("with_bundle_update",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "bool",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::state_builder::StateBuilder",
                          "with_bundle_update"
                        |)
                      ]
                    |));
                  ("with_background_transition_merge",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "bool",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::state_builder::StateBuilder",
                          "with_background_transition_merge"
                        |)
                      ]
                    |));
                  ("with_block_hashes",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "alloc::collections::btree::map::BTreeMap")
                          []
                          [
                            Ty.path "u64";
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [];
                            Ty.path "alloc::alloc::Global"
                          ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::state_builder::StateBuilder",
                          "with_block_hashes"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (DB : Ty.t),
          M.IsTraitInstance
            "core::clone::Clone"
            (Self DB)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method (clone DB)) ].
      End Impl_core_clone_Clone_where_core_clone_Clone_DB_for_revm_db_states_state_builder_StateBuilder_DB.
      
      Module Impl_core_fmt_Debug_where_core_fmt_Debug_DB_for_revm_db_states_state_builder_StateBuilder_DB.
        Definition Self (DB : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ].
        
        (* Debug *)
        Definition fmt (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.read (|
                let~ names :=
                  M.alloc (|
                    M.alloc (|
                      Value.Array
                        [
                          M.read (| Value.String "database" |);
                          M.read (| Value.String "with_state_clear" |);
                          M.read (| Value.String "with_bundle_prestate" |);
                          M.read (| Value.String "with_cache_prestate" |);
                          M.read (| Value.String "with_bundle_update" |);
                          M.read (| Value.String "with_background_transition_merge" |);
                          M.read (| Value.String "with_block_hashes" |)
                        ]
                    |)
                  |) in
                let~ values :=
                  M.alloc (|
                    M.alloc (|
                      Value.Array
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::state_builder::StateBuilder",
                            "database"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::state_builder::StateBuilder",
                            "with_state_clear"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::state_builder::StateBuilder",
                            "with_bundle_prestate"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::state_builder::StateBuilder",
                            "with_cache_prestate"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::state_builder::StateBuilder",
                            "with_bundle_update"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::state_builder::StateBuilder",
                            "with_background_transition_merge"
                          |);
                          M.alloc (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::state_builder::StateBuilder",
                              "with_block_hashes"
                            |)
                          |)
                        ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::Formatter",
                      "debug_struct_fields_finish",
                      []
                    |),
                    [
                      M.read (| f |);
                      M.read (| Value.String "StateBuilder" |);
                      M.read (| names |);
                      M.read (| values |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (DB : Ty.t),
          M.IsTraitInstance
            "core::fmt::Debug"
            (Self DB)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method (fmt DB)) ].
      End Impl_core_fmt_Debug_where_core_fmt_Debug_DB_for_revm_db_states_state_builder_StateBuilder_DB.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_state_builder_StateBuilder_DB.
        Definition Self (DB : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ].
        
        Axiom Implements :
          forall (DB : Ty.t),
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            (Self DB)
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_state_builder_StateBuilder_DB.
      
      Module Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_DB_for_revm_db_states_state_builder_StateBuilder_DB.
        Definition Self (DB : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ].
        
        (* PartialEq *)
        Definition eq (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self DB in
          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 (|
                    LogicalOp.and (|
                      LogicalOp.and (|
                        LogicalOp.and (|
                          M.call_closure (|
                            M.get_trait_method (| "core::cmp::PartialEq", DB, [ DB ], "eq", [] |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm::db::states::state_builder::StateBuilder",
                                "database"
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| other |),
                                "revm::db::states::state_builder::StateBuilder",
                                "database"
                              |)
                            ]
                          |),
                          ltac:(M.monadic
                            (BinOp.eq (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::state_builder::StateBuilder",
                                  "with_state_clear"
                                |)
                              |),
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| other |),
                                  "revm::db::states::state_builder::StateBuilder",
                                  "with_state_clear"
                                |)
                              |)
                            |)))
                        |),
                        ltac:(M.monadic
                          (M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialEq",
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [ Ty.path "revm::db::states::bundle_state::BundleState" ],
                              [
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "revm::db::states::bundle_state::BundleState" ]
                              ],
                              "eq",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm::db::states::state_builder::StateBuilder",
                                "with_bundle_prestate"
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| other |),
                                "revm::db::states::state_builder::StateBuilder",
                                "with_bundle_prestate"
                              |)
                            ]
                          |)))
                      |),
                      ltac:(M.monadic
                        (M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::cache::CacheState" ],
                            [
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [ Ty.path "revm::db::states::cache::CacheState" ]
                            ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::state_builder::StateBuilder",
                              "with_cache_prestate"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "revm::db::states::state_builder::StateBuilder",
                              "with_cache_prestate"
                            |)
                          ]
                        |)))
                    |),
                    ltac:(M.monadic
                      (BinOp.eq (|
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::state_builder::StateBuilder",
                            "with_bundle_update"
                          |)
                        |),
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "revm::db::states::state_builder::StateBuilder",
                            "with_bundle_update"
                          |)
                        |)
                      |)))
                  |),
                  ltac:(M.monadic
                    (BinOp.eq (|
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::state_builder::StateBuilder",
                          "with_background_transition_merge"
                        |)
                      |),
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm::db::states::state_builder::StateBuilder",
                          "with_background_transition_merge"
                        |)
                      |)
                    |)))
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.apply
                        (Ty.path "alloc::collections::btree::map::BTreeMap")
                        []
                        [
                          Ty.path "u64";
                          Ty.apply
                            (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [
                        Ty.apply
                          (Ty.path "alloc::collections::btree::map::BTreeMap")
                          []
                          [
                            Ty.path "u64";
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [];
                            Ty.path "alloc::alloc::Global"
                          ]
                      ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::state_builder::StateBuilder",
                        "with_block_hashes"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm::db::states::state_builder::StateBuilder",
                        "with_block_hashes"
                      |)
                    ]
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (DB : Ty.t),
          M.IsTraitInstance
            "core::cmp::PartialEq"
            (Self DB)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("eq", InstanceField.Method (eq DB)) ].
      End Impl_core_cmp_PartialEq_where_core_cmp_PartialEq_DB_for_revm_db_states_state_builder_StateBuilder_DB.
      
      Module Impl_core_cmp_Eq_where_core_cmp_Eq_DB_for_revm_db_states_state_builder_StateBuilder_DB.
        Definition Self (DB : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ].
        
        (* Eq *)
        Definition assert_receiver_is_total_eq
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          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.match_operator (|
                                                  Value.DeclaredButUndefined,
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (M.alloc (| Value.Tuple [] |)))
                                                  ]
                                                |)))
                                          ]
                                        |)))
                                  ]
                                |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (DB : Ty.t),
          M.IsTraitInstance
            "core::cmp::Eq"
            (Self DB)
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("assert_receiver_is_total_eq", InstanceField.Method (assert_receiver_is_total_eq DB))
            ].
      End Impl_core_cmp_Eq_where_core_cmp_Eq_DB_for_revm_db_states_state_builder_StateBuilder_DB.
      
      Module Impl_revm_db_states_state_builder_StateBuilder_revm_db_emptydb_EmptyDBTyped_core_convert_Infallible.
        Definition Self : Ty.t :=
          Ty.apply
            (Ty.path "revm::db::states::state_builder::StateBuilder")
            []
            [
              Ty.apply
                (Ty.path "revm::db::emptydb::EmptyDBTyped")
                []
                [ Ty.path "core::convert::Infallible" ]
            ].
        
        (*
            pub fn new() -> Self {
                Self::default()
            }
        *)
        Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "revm::db::states::state_builder::StateBuilder")
                    []
                    [
                      Ty.apply
                        (Ty.path "revm::db::emptydb::EmptyDBTyped")
                        []
                        [ Ty.path "core::convert::Infallible" ]
                    ],
                  [],
                  "default",
                  []
                |),
                []
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      End Impl_revm_db_states_state_builder_StateBuilder_revm_db_emptydb_EmptyDBTyped_core_convert_Infallible.
      
      Module Impl_core_default_Default_where_revm_primitives_db_Database_DB_where_core_default_Default_DB_for_revm_db_states_state_builder_StateBuilder_DB.
        Definition Self (DB : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ].
        
        (*
            fn default() -> Self {
                Self::new_with_database(DB::default())
            }
        *)
        Definition default (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ],
                  "new_with_database",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", DB, [], "default", [] |),
                    []
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          forall (DB : Ty.t),
          M.IsTraitInstance
            "core::default::Default"
            (Self DB)
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method (default DB)) ].
      End Impl_core_default_Default_where_revm_primitives_db_Database_DB_where_core_default_Default_DB_for_revm_db_states_state_builder_StateBuilder_DB.
      
      Module Impl_revm_db_states_state_builder_StateBuilder_DB.
        Definition Self (DB : Ty.t) : Ty.t :=
          Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ].
        
        (*
            pub fn new_with_database(database: DB) -> Self {
                Self {
                    database,
                    with_state_clear: true,
                    with_cache_prestate: None,
                    with_bundle_prestate: None,
                    with_bundle_update: false,
                    with_background_transition_merge: false,
                    with_block_hashes: BTreeMap::new(),
                }
            }
        *)
        Definition new_with_database
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ database ] =>
            ltac:(M.monadic
              (let database := M.alloc (| database |) in
              Value.StructRecord
                "revm::db::states::state_builder::StateBuilder"
                [
                  ("database", M.read (| database |));
                  ("with_state_clear", Value.Bool true);
                  ("with_cache_prestate", Value.StructTuple "core::option::Option::None" []);
                  ("with_bundle_prestate", Value.StructTuple "core::option::Option::None" []);
                  ("with_bundle_update", Value.Bool false);
                  ("with_background_transition_merge", Value.Bool false);
                  ("with_block_hashes",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::collections::btree::map::BTreeMap")
                          []
                          [
                            Ty.path "u64";
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [];
                            Ty.path "alloc::alloc::Global"
                          ],
                        "new",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_with_database :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "new_with_database" (new_with_database DB).
        
        (*
            pub fn with_database<ODB: Database>(self, database: ODB) -> StateBuilder<ODB> {
                // cast to the different database,
                // Note that we return different type depending of the database NewDBError.
                StateBuilder {
                    with_state_clear: self.with_state_clear,
                    database,
                    with_cache_prestate: self.with_cache_prestate,
                    with_bundle_prestate: self.with_bundle_prestate,
                    with_bundle_update: self.with_bundle_update,
                    with_background_transition_merge: self.with_background_transition_merge,
                    with_block_hashes: self.with_block_hashes,
                }
            }
        *)
        Definition with_database
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [ ODB ], [ self; database ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let database := M.alloc (| database |) in
              Value.StructRecord
                "revm::db::states::state_builder::StateBuilder"
                [
                  ("with_state_clear",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "revm::db::states::state_builder::StateBuilder",
                        "with_state_clear"
                      |)
                    |));
                  ("database", M.read (| database |));
                  ("with_cache_prestate",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "revm::db::states::state_builder::StateBuilder",
                        "with_cache_prestate"
                      |)
                    |));
                  ("with_bundle_prestate",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "revm::db::states::state_builder::StateBuilder",
                        "with_bundle_prestate"
                      |)
                    |));
                  ("with_bundle_update",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "revm::db::states::state_builder::StateBuilder",
                        "with_bundle_update"
                      |)
                    |));
                  ("with_background_transition_merge",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "revm::db::states::state_builder::StateBuilder",
                        "with_background_transition_merge"
                      |)
                    |));
                  ("with_block_hashes",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        self,
                        "revm::db::states::state_builder::StateBuilder",
                        "with_block_hashes"
                      |)
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_with_database :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "with_database" (with_database DB).
        
        (*
            pub fn with_database_ref<ODB: DatabaseRef>(
                self,
                database: ODB,
            ) -> StateBuilder<WrapDatabaseRef<ODB>> {
                self.with_database(WrapDatabaseRef(database))
            }
        *)
        Definition with_database_ref
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [ ODB ], [ self; database ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let database := M.alloc (| database |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ],
                  "with_database",
                  [ Ty.apply (Ty.path "revm_primitives::db::WrapDatabaseRef") [] [ ODB ] ]
                |),
                [
                  M.read (| self |);
                  Value.StructTuple "revm_primitives::db::WrapDatabaseRef" [ M.read (| database |) ]
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_with_database_ref :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "with_database_ref" (with_database_ref DB).
        
        (*
            pub fn with_database_boxed<Error>(
                self,
                database: DBBox<'_, Error>,
            ) -> StateBuilder<DBBox<'_, Error>> {
                self.with_database(database)
            }
        *)
        Definition with_database_boxed
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [ Error ], [ self; database ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let database := M.alloc (| database |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "revm::db::states::state_builder::StateBuilder") [] [ DB ],
                  "with_database",
                  [
                    Ty.apply
                      (Ty.path "alloc::boxed::Box")
                      []
                      [
                        Ty.dyn
                          [
                            ("revm_primitives::db::Database::Trait", []);
                            ("core::marker::Send::AutoTrait", [])
                          ];
                        Ty.path "alloc::alloc::Global"
                      ]
                  ]
                |),
                [ M.read (| self |); M.read (| database |) ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_with_database_boxed :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "with_database_boxed" (with_database_boxed DB).
        
        (*
            pub fn without_state_clear(self) -> Self {
                Self {
                    with_state_clear: false,
                    ..self
                }
            }
        *)
        Definition without_state_clear
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.struct_record_update
                (M.read (| self |))
                [ ("with_state_clear", Value.Bool false) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_without_state_clear :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "without_state_clear" (without_state_clear DB).
        
        (*
            pub fn with_bundle_prestate(self, bundle: BundleState) -> Self {
                Self {
                    with_bundle_prestate: Some(bundle),
                    ..self
                }
            }
        *)
        Definition with_bundle_prestate
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self; bundle ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let bundle := M.alloc (| bundle |) in
              M.struct_record_update
                (M.read (| self |))
                [
                  ("with_bundle_prestate",
                    Value.StructTuple "core::option::Option::Some" [ M.read (| bundle |) ])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_with_bundle_prestate :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "with_bundle_prestate" (with_bundle_prestate DB).
        
        (*
            pub fn with_bundle_update(self) -> Self {
                Self {
                    with_bundle_update: true,
                    ..self
                }
            }
        *)
        Definition with_bundle_update
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.struct_record_update
                (M.read (| self |))
                [ ("with_bundle_update", Value.Bool true) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_with_bundle_update :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "with_bundle_update" (with_bundle_update DB).
        
        (*
            pub fn with_cached_prestate(self, cache: CacheState) -> Self {
                Self {
                    with_cache_prestate: Some(cache),
                    ..self
                }
            }
        *)
        Definition with_cached_prestate
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self; cache ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let cache := M.alloc (| cache |) in
              M.struct_record_update
                (M.read (| self |))
                [
                  ("with_cache_prestate",
                    Value.StructTuple "core::option::Option::Some" [ M.read (| cache |) ])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_with_cached_prestate :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "with_cached_prestate" (with_cached_prestate DB).
        
        (*
            pub fn with_background_transition_merge(self) -> Self {
                Self {
                    with_background_transition_merge: true,
                    ..self
                }
            }
        *)
        Definition with_background_transition_merge
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.struct_record_update
                (M.read (| self |))
                [ ("with_background_transition_merge", Value.Bool true) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_with_background_transition_merge :
          forall (DB : Ty.t),
          M.IsAssociatedFunction
            (Self DB)
            "with_background_transition_merge"
            (with_background_transition_merge DB).
        
        (*
            pub fn with_block_hashes(self, block_hashes: BTreeMap<u64, B256>) -> Self {
                Self {
                    with_block_hashes: block_hashes,
                    ..self
                }
            }
        *)
        Definition with_block_hashes
            (DB : Ty.t)
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self; block_hashes ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let block_hashes := M.alloc (| block_hashes |) in
              M.struct_record_update
                (M.read (| self |))
                [ ("with_block_hashes", M.read (| block_hashes |)) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_with_block_hashes :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "with_block_hashes" (with_block_hashes DB).
        
        (*
            pub fn build(mut self) -> State<DB> {
                let use_preloaded_bundle = if self.with_cache_prestate.is_some() {
                    self.with_bundle_prestate = None;
                    false
                } else {
                    self.with_bundle_prestate.is_some()
                };
                State {
                    cache: self
                        .with_cache_prestate
                        .unwrap_or_else(|| CacheState::new(self.with_state_clear)),
                    database: self.database,
                    transition_state: self.with_bundle_update.then(TransitionState::default),
                    bundle_state: self.with_bundle_prestate.unwrap_or_default(),
                    use_preloaded_bundle,
                    block_hashes: self.with_block_hashes,
                }
            }
        *)
        Definition build (DB : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          let Self : Ty.t := Self DB in
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ use_preloaded_bundle :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "revm::db::states::cache::CacheState" ],
                                      "is_some",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        self,
                                        "revm::db::states::state_builder::StateBuilder",
                                        "with_cache_prestate"
                                      |)
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  self,
                                  "revm::db::states::state_builder::StateBuilder",
                                  "with_bundle_prestate"
                                |),
                                Value.StructTuple "core::option::Option::None" []
                              |) in
                            M.alloc (| Value.Bool false |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [ Ty.path "revm::db::states::bundle_state::BundleState" ],
                                  "is_some",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    self,
                                    "revm::db::states::state_builder::StateBuilder",
                                    "with_bundle_prestate"
                                  |)
                                ]
                              |)
                            |)))
                      ]
                    |)
                  |) in
                M.alloc (|
                  Value.StructRecord
                    "revm::db::states::state::State"
                    [
                      ("cache",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::cache::CacheState" ],
                            "unwrap_or_else",
                            [
                              Ty.function
                                [ Ty.tuple [] ]
                                (Ty.path "revm::db::states::cache::CacheState")
                            ]
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "revm::db::states::state_builder::StateBuilder",
                                "with_cache_prestate"
                              |)
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "revm::db::states::cache::CacheState",
                                                  "new",
                                                  []
                                                |),
                                                [
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      self,
                                                      "revm::db::states::state_builder::StateBuilder",
                                                      "with_state_clear"
                                                    |)
                                                  |)
                                                ]
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |));
                      ("database",
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "revm::db::states::state_builder::StateBuilder",
                            "database"
                          |)
                        |));
                      ("transition_state",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "bool",
                            "then",
                            [
                              Ty.path "revm::db::states::transition_state::TransitionState";
                              Ty.function
                                []
                                (Ty.path "revm::db::states::transition_state::TransitionState")
                            ]
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "revm::db::states::state_builder::StateBuilder",
                                "with_bundle_update"
                              |)
                            |);
                            M.get_trait_method (|
                              "core::default::Default",
                              Ty.path "revm::db::states::transition_state::TransitionState",
                              [],
                              "default",
                              []
                            |)
                          ]
                        |));
                      ("bundle_state",
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::bundle_state::BundleState" ],
                            "unwrap_or_default",
                            []
                          |),
                          [
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                self,
                                "revm::db::states::state_builder::StateBuilder",
                                "with_bundle_prestate"
                              |)
                            |)
                          ]
                        |));
                      ("use_preloaded_bundle", M.read (| use_preloaded_bundle |));
                      ("block_hashes",
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            self,
                            "revm::db::states::state_builder::StateBuilder",
                            "with_block_hashes"
                          |)
                        |))
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_build :
          forall (DB : Ty.t),
          M.IsAssociatedFunction (Self DB) "build" (build DB).
      End Impl_revm_db_states_state_builder_StateBuilder_DB.
    End state_builder.
  End states.
End db.
