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

Module db.
  Module states.
    Module cache.
      (* StructRecord
        {
          name := "CacheState";
          const_params := [];
          ty_params := [];
          fields :=
            [
              ("accounts",
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.path "alloy_primitives::bits::address::Address";
                    Ty.path "revm::db::states::cache_account::CacheAccount";
                    Ty.path "std::hash::random::RandomState"
                  ]);
              ("contracts",
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [];
                    Ty.path "revm_primitives::bytecode::Bytecode";
                    Ty.path "std::hash::random::RandomState"
                  ]);
              ("has_state_clear", Ty.path "bool")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_cache_CacheState.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache::CacheState".
        
        (* Clone *)
        Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "revm::db::states::cache::CacheState"
                [
                  ("accounts",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.path "revm::db::states::cache_account::CacheAccount";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache::CacheState",
                          "accounts"
                        |)
                      ]
                    |));
                  ("contracts",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [];
                            Ty.path "revm_primitives::bytecode::Bytecode";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache::CacheState",
                          "contracts"
                        |)
                      ]
                    |));
                  ("has_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::cache::CacheState",
                          "has_state_clear"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::clone::Clone"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("clone", InstanceField.Method clone) ].
      End Impl_core_clone_Clone_for_revm_db_states_cache_CacheState.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_cache_CacheState.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache::CacheState".
        
        (* Debug *)
        Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; f ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let f := M.alloc (| f |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_field3_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "CacheState" |);
                  M.read (| Value.String "accounts" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::cache::CacheState",
                    "accounts"
                  |);
                  M.read (| Value.String "contracts" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::cache::CacheState",
                    "contracts"
                  |);
                  M.read (| Value.String "has_state_clear" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache::CacheState",
                      "has_state_clear"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::fmt::Debug"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
      End Impl_core_fmt_Debug_for_revm_db_states_cache_CacheState.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_cache_CacheState.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache::CacheState".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_cache_CacheState.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_cache_CacheState.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache::CacheState".
        
        (* PartialEq *)
        Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              LogicalOp.and (|
                LogicalOp.and (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.path "alloy_primitives::bits::address::Address";
                          Ty.path "revm::db::states::cache_account::CacheAccount";
                          Ty.path "std::hash::random::RandomState"
                        ],
                      [
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.path "revm::db::states::cache_account::CacheAccount";
                            Ty.path "std::hash::random::RandomState"
                          ]
                      ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::cache::CacheState",
                        "accounts"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm::db::states::cache::CacheState",
                        "accounts"
                      |)
                    ]
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [];
                            Ty.path "revm_primitives::bytecode::Bytecode";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [
                          Ty.apply
                            (Ty.path "std::collections::hash::map::HashMap")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                [ Value.Integer IntegerKind.Usize 32 ]
                                [];
                              Ty.path "revm_primitives::bytecode::Bytecode";
                              Ty.path "std::hash::random::RandomState"
                            ]
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache::CacheState",
                          "contracts"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm::db::states::cache::CacheState",
                          "contracts"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::cache::CacheState",
                        "has_state_clear"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm::db::states::cache::CacheState",
                        "has_state_clear"
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::PartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("eq", InstanceField.Method eq) ].
      End Impl_core_cmp_PartialEq_for_revm_db_states_cache_CacheState.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_cache_CacheState.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache::CacheState".
        
        (* Eq *)
        Definition assert_receiver_is_total_eq
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          Value.DeclaredButUndefined,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  Value.DeclaredButUndefined,
                                  [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                                |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::cmp::Eq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
      End Impl_core_cmp_Eq_for_revm_db_states_cache_CacheState.
      
      Module Impl_core_default_Default_for_revm_db_states_cache_CacheState.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache::CacheState".
        
        (*
            fn default() -> Self {
                Self::new(true)
            }
        *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.path "revm::db::states::cache::CacheState",
                  "new",
                  []
                |),
                [ Value.Bool true ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_revm_db_states_cache_CacheState.
      
      Module Impl_revm_db_states_cache_CacheState.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache::CacheState".
        
        (*
            pub fn new(has_state_clear: bool) -> Self {
                Self {
                    accounts: HashMap::default(),
                    contracts: HashMap::default(),
                    has_state_clear,
                }
            }
        *)
        Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ has_state_clear ] =>
            ltac:(M.monadic
              (let has_state_clear := M.alloc (| has_state_clear |) in
              Value.StructRecord
                "revm::db::states::cache::CacheState"
                [
                  ("accounts",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.path "revm::db::states::cache_account::CacheAccount";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("contracts",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [];
                            Ty.path "revm_primitives::bytecode::Bytecode";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("has_state_clear", M.read (| has_state_clear |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
        
        (*
            pub fn set_state_clear_flag(&mut self, has_state_clear: bool) {
                self.has_state_clear = has_state_clear;
            }
        *)
        Definition set_state_clear_flag (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; has_state_clear ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let has_state_clear := M.alloc (| has_state_clear |) in
              M.read (|
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache::CacheState",
                      "has_state_clear"
                    |),
                    M.read (| has_state_clear |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_set_state_clear_flag :
          M.IsAssociatedFunction Self "set_state_clear_flag" set_state_clear_flag.
        
        (*
            pub fn trie_account(&self) -> impl IntoIterator<Item = (Address, &PlainAccount)> {
                self.accounts.iter().filter_map(|(address, account)| {
                    account
                        .account
                        .as_ref()
                        .map(|plain_acc| ( *address, plain_acc))
                })
            }
        *)
        Definition trie_account (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply
                    (Ty.path "std::collections::hash::map::Iter")
                    []
                    [
                      Ty.path "alloy_primitives::bits::address::Address";
                      Ty.path "revm::db::states::cache_account::CacheAccount"
                    ],
                  [],
                  "filter_map",
                  [
                    Ty.tuple
                      [
                        Ty.path "alloy_primitives::bits::address::Address";
                        Ty.apply
                          (Ty.path "&")
                          []
                          [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                      ];
                    Ty.function
                      [
                        Ty.tuple
                          [
                            Ty.tuple
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "alloy_primitives::bits::address::Address" ];
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "revm::db::states::cache_account::CacheAccount" ]
                              ]
                          ]
                      ]
                      (Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [
                          Ty.tuple
                            [
                              Ty.path "alloy_primitives::bits::address::Address";
                              Ty.apply
                                (Ty.path "&")
                                []
                                [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                            ]
                        ])
                  ]
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.path "alloy_primitives::bits::address::Address";
                          Ty.path "revm::db::states::cache_account::CacheAccount";
                          Ty.path "std::hash::random::RandomState"
                        ],
                      "iter",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::cache::CacheState",
                        "accounts"
                      |)
                    ]
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                    let address := M.copy (| γ0_0 |) in
                                    let account := M.copy (| γ0_1 |) in
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.path
                                                  "revm::db::states::plain_account::PlainAccount"
                                              ]
                                          ],
                                        "map",
                                        [
                                          Ty.tuple
                                            [
                                              Ty.path "alloy_primitives::bits::address::Address";
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [
                                                  Ty.path
                                                    "revm::db::states::plain_account::PlainAccount"
                                                ]
                                            ];
                                          Ty.function
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.apply
                                                    (Ty.path "&")
                                                    []
                                                    [
                                                      Ty.path
                                                        "revm::db::states::plain_account::PlainAccount"
                                                    ]
                                                ]
                                            ]
                                            (Ty.tuple
                                              [
                                                Ty.path "alloy_primitives::bits::address::Address";
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [
                                                    Ty.path
                                                      "revm::db::states::plain_account::PlainAccount"
                                                  ]
                                              ])
                                        ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [
                                                Ty.path
                                                  "revm::db::states::plain_account::PlainAccount"
                                              ],
                                            "as_ref",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| account |),
                                              "revm::db::states::cache_account::CacheAccount",
                                              "account"
                                            |)
                                          ]
                                        |);
                                        M.closure
                                          (fun γ =>
                                            ltac:(M.monadic
                                              match γ with
                                              | [ α0 ] =>
                                                ltac:(M.monadic
                                                  (M.match_operator (|
                                                    M.alloc (| α0 |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let plain_acc := M.copy (| γ |) in
                                                          Value.Tuple
                                                            [
                                                              M.read (| M.read (| address |) |);
                                                              M.read (| plain_acc |)
                                                            ]))
                                                    ]
                                                  |)))
                                              | _ => M.impossible "wrong number of arguments"
                                              end))
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_trie_account :
          M.IsAssociatedFunction Self "trie_account" trie_account.
        
        (*
            pub fn insert_not_existing(&mut self, address: Address) {
                self.accounts
                    .insert(address, CacheAccount::new_loaded_not_existing());
            }
        *)
        Definition insert_not_existing (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; address ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let address := M.alloc (| address |) in
              M.read (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.path "revm::db::states::cache_account::CacheAccount";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "insert",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache::CacheState",
                          "accounts"
                        |);
                        M.read (| address |);
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm::db::states::cache_account::CacheAccount",
                            "new_loaded_not_existing",
                            []
                          |),
                          []
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_insert_not_existing :
          M.IsAssociatedFunction Self "insert_not_existing" insert_not_existing.
        
        (*
            pub fn insert_account(&mut self, address: Address, info: AccountInfo) {
                let account = if !info.is_empty() {
                    CacheAccount::new_loaded(info, HashMap::default())
                } else {
                    CacheAccount::new_loaded_empty_eip161(HashMap::default())
                };
                self.accounts.insert(address, account);
            }
        *)
        Definition insert_account (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; address; info ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let address := M.alloc (| address |) in
              let info := M.alloc (| info |) in
              M.read (|
                let~ account :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::state::AccountInfo",
                                        "is_empty",
                                        []
                                      |),
                                      [ info ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm::db::states::cache_account::CacheAccount",
                                  "new_loaded",
                                  []
                                |),
                                [
                                  M.read (| info |);
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::default::Default",
                                      Ty.apply
                                        (Ty.path "std::collections::hash::map::HashMap")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [];
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [];
                                          Ty.path "std::hash::random::RandomState"
                                        ],
                                      [],
                                      "default",
                                      []
                                    |),
                                    []
                                  |)
                                ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm::db::states::cache_account::CacheAccount",
                                  "new_loaded_empty_eip161",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::default::Default",
                                      Ty.apply
                                        (Ty.path "std::collections::hash::map::HashMap")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [];
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [];
                                          Ty.path "std::hash::random::RandomState"
                                        ],
                                      [],
                                      "default",
                                      []
                                    |),
                                    []
                                  |)
                                ]
                              |)
                            |)))
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.path "revm::db::states::cache_account::CacheAccount";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "insert",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache::CacheState",
                          "accounts"
                        |);
                        M.read (| address |);
                        M.read (| account |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_insert_account :
          M.IsAssociatedFunction Self "insert_account" insert_account.
        
        (*
            pub fn insert_account_with_storage(
                &mut self,
                address: Address,
                info: AccountInfo,
                storage: PlainStorage,
            ) {
                let account = if !info.is_empty() {
                    CacheAccount::new_loaded(info, storage)
                } else {
                    CacheAccount::new_loaded_empty_eip161(storage)
                };
                self.accounts.insert(address, account);
            }
        *)
        Definition insert_account_with_storage
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; address; info; storage ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let address := M.alloc (| address |) in
              let info := M.alloc (| info |) in
              let storage := M.alloc (| storage |) in
              M.read (|
                let~ account :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::state::AccountInfo",
                                        "is_empty",
                                        []
                                      |),
                                      [ info ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm::db::states::cache_account::CacheAccount",
                                  "new_loaded",
                                  []
                                |),
                                [ M.read (| info |); M.read (| storage |) ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm::db::states::cache_account::CacheAccount",
                                  "new_loaded_empty_eip161",
                                  []
                                |),
                                [ M.read (| storage |) ]
                              |)
                            |)))
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.path "revm::db::states::cache_account::CacheAccount";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "insert",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache::CacheState",
                          "accounts"
                        |);
                        M.read (| address |);
                        M.read (| account |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_insert_account_with_storage :
          M.IsAssociatedFunction Self "insert_account_with_storage" insert_account_with_storage.
        
        (*
            pub fn apply_evm_state(&mut self, evm_state: EVMState) -> Vec<(Address, TransitionAccount)> {
                let mut transitions = Vec::with_capacity(evm_state.len());
                for (address, account) in evm_state {
                    if let Some(transition) = self.apply_account_state(address, account) {
                        transitions.push((address, transition));
                    }
                }
                transitions
            }
        *)
        Definition apply_evm_state (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; evm_state ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let evm_state := M.alloc (| evm_state |) in
              M.read (|
                let~ transitions :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.tuple
                              [
                                Ty.path "alloy_primitives::bits::address::Address";
                                Ty.path "revm::db::states::transition_account::TransitionAccount"
                              ];
                            Ty.path "alloc::alloc::Global"
                          ],
                        "with_capacity",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "std::collections::hash::map::HashMap")
                              []
                              [
                                Ty.path "alloy_primitives::bits::address::Address";
                                Ty.path "revm_primitives::state::Account";
                                Ty.path "std::hash::random::RandomState"
                              ],
                            "len",
                            []
                          |),
                          [ evm_state ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "std::collections::hash::map::HashMap")
                              []
                              [
                                Ty.path "alloy_primitives::bits::address::Address";
                                Ty.path "revm_primitives::state::Account";
                                Ty.path "std::hash::random::RandomState"
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [ M.read (| evm_state |) ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "std::collections::hash::map::IntoIter")
                                            []
                                            [
                                              Ty.path "alloy_primitives::bits::address::Address";
                                              Ty.path "revm_primitives::state::Account"
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let γ1_0 := M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                          let γ1_1 := M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                          let address := M.copy (| γ1_0 |) in
                                          let account := M.copy (| γ1_1 |) in
                                          M.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "revm::db::states::cache::CacheState",
                                                          "apply_account_state",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| self |);
                                                          M.read (| address |);
                                                          M.read (| account |)
                                                        ]
                                                      |)
                                                    |) in
                                                  let γ0_0 :=
                                                    M.SubPointer.get_struct_tuple_field (|
                                                      γ,
                                                      "core::option::Option::Some",
                                                      0
                                                    |) in
                                                  let transition := M.copy (| γ0_0 |) in
                                                  let~ _ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "alloc::vec::Vec")
                                                            []
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.path
                                                                    "alloy_primitives::bits::address::Address";
                                                                  Ty.path
                                                                    "revm::db::states::transition_account::TransitionAccount"
                                                                ];
                                                              Ty.path "alloc::alloc::Global"
                                                            ],
                                                          "push",
                                                          []
                                                        |),
                                                        [
                                                          transitions;
                                                          Value.Tuple
                                                            [
                                                              M.read (| address |);
                                                              M.read (| transition |)
                                                            ]
                                                        ]
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)));
                                              fun γ =>
                                                ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                            ]
                                          |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                transitions
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_apply_evm_state :
          M.IsAssociatedFunction Self "apply_evm_state" apply_evm_state.
        
        (*
            fn apply_account_state(
                &mut self,
                address: Address,
                account: Account,
            ) -> Option<TransitionAccount> {
                // not touched account are never changed.
                if !account.is_touched() {
                    return None;
                }
        
                let this_account = self
                    .accounts
                    .get_mut(&address)
                    .expect("All accounts should be present inside cache");
        
                // If it is marked as selfdestructed inside revm
                // we need to changed state to destroyed.
                if account.is_selfdestructed() {
                    return this_account.selfdestruct();
                }
        
                // Note: it can happen that created contract get selfdestructed in same block
                // that is why is_created is checked after selfdestructed
                //
                // Note: Create2 opcode (Petersburg) was after state clear EIP (Spurious Dragon)
                //
                // Note: It is possibility to create KECCAK_EMPTY contract with some storage
                // by just setting storage inside CRATE constructor. Overlap of those contracts
                // is not possible because CREATE2 is introduced later.
                if account.is_created() {
                    return Some(this_account.newly_created(account.info, account.storage));
                }
        
                // Account is touched, but not selfdestructed or newly created.
                // Account can be touched and not changed.
                // And when empty account is touched it needs to be removed from database.
                // EIP-161 state clear
                if account.is_empty() {
                    if self.has_state_clear {
                        // touch empty account.
                        this_account.touch_empty_eip161()
                    } else {
                        // if account is empty and state clear is not enabled we should save
                        // empty account.
                        this_account.touch_create_pre_eip161(account.storage)
                    }
                } else {
                    Some(this_account.change(account.info, account.storage))
                }
            }
        *)
        Definition apply_account_state (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; address; account ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let address := M.alloc (| address |) in
              let account := M.alloc (| account |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    UnOp.not (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm_primitives::state::Account",
                                          "is_touched",
                                          []
                                        |),
                                        [ account ]
                                      |)
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      Value.StructTuple "core::option::Option::None" []
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ this_account :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [ Ty.path "revm::db::states::cache_account::CacheAccount" ]
                              ],
                            "expect",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::HashMap")
                                  []
                                  [
                                    Ty.path "alloy_primitives::bits::address::Address";
                                    Ty.path "revm::db::states::cache_account::CacheAccount";
                                    Ty.path "std::hash::random::RandomState"
                                  ],
                                "get_mut",
                                [ Ty.path "alloy_primitives::bits::address::Address" ]
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::cache::CacheState",
                                  "accounts"
                                |);
                                address
                              ]
                            |);
                            M.read (| Value.String "All accounts should be present inside cache" |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::state::Account",
                                        "is_selfdestructed",
                                        []
                                      |),
                                      [ account ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm::db::states::cache_account::CacheAccount",
                                          "selfdestruct",
                                          []
                                        |),
                                        [ M.read (| this_account |) ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::state::Account",
                                        "is_created",
                                        []
                                      |),
                                      [ account ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      Value.StructTuple
                                        "core::option::Option::Some"
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path
                                                "revm::db::states::cache_account::CacheAccount",
                                              "newly_created",
                                              []
                                            |),
                                            [
                                              M.read (| this_account |);
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  account,
                                                  "revm_primitives::state::Account",
                                                  "info"
                                                |)
                                              |);
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  account,
                                                  "revm_primitives::state::Account",
                                                  "storage"
                                                |)
                                              |)
                                            ]
                                          |)
                                        ]
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_primitives::state::Account",
                                      "is_empty",
                                      []
                                    |),
                                    [ account ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::db::states::cache::CacheState",
                                          "has_state_clear"
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm::db::states::cache_account::CacheAccount",
                                          "touch_empty_eip161",
                                          []
                                        |),
                                        [ M.read (| this_account |) ]
                                      |)
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm::db::states::cache_account::CacheAccount",
                                          "touch_create_pre_eip161",
                                          []
                                        |),
                                        [
                                          M.read (| this_account |);
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              account,
                                              "revm_primitives::state::Account",
                                              "storage"
                                            |)
                                          |)
                                        ]
                                      |)
                                    |)))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              Value.StructTuple
                                "core::option::Option::Some"
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm::db::states::cache_account::CacheAccount",
                                      "change",
                                      []
                                    |),
                                    [
                                      M.read (| this_account |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          account,
                                          "revm_primitives::state::Account",
                                          "info"
                                        |)
                                      |);
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          account,
                                          "revm_primitives::state::Account",
                                          "storage"
                                        |)
                                      |)
                                    ]
                                  |)
                                ]
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_apply_account_state :
          M.IsAssociatedFunction Self "apply_account_state" apply_account_state.
      End Impl_revm_db_states_cache_CacheState.
    End cache.
  End states.
End db.
