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

Module db.
  Module states.
    Module cache_account.
      (* StructRecord
        {
          name := "CacheAccount";
          const_params := [];
          ty_params := [];
          fields :=
            [
              ("account",
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "revm::db::states::plain_account::PlainAccount" ]);
              ("status", Ty.path "revm::db::states::account_status::AccountStatus")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_cache_account_CacheAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache_account::CacheAccount".
        
        (* 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_account::CacheAccount"
                [
                  ("account",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "account"
                        |)
                      ]
                    |));
                  ("status",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "status"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_account_CacheAccount.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_cache_account_CacheAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache_account::CacheAccount".
        
        (* 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_field2_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "CacheAccount" |);
                  M.read (| Value.String "account" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::cache_account::CacheAccount",
                    "account"
                  |);
                  M.read (| Value.String "status" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_account_CacheAccount.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_cache_account_CacheAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache_account::CacheAccount".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_cache_account_CacheAccount.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_cache_account_CacheAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache_account::CacheAccount".
        
        (* 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 (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                    [
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "account"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm::db::states::cache_account::CacheAccount",
                      "account"
                    |)
                  ]
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path "revm::db::states::account_status::AccountStatus",
                      [ Ty.path "revm::db::states::account_status::AccountStatus" ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::cache_account::CacheAccount",
                        "status"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm::db::states::cache_account::CacheAccount",
                        "status"
                      |)
                    ]
                  |)))
              |)))
          | _, _, _ => 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_account_CacheAccount.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_cache_account_CacheAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache_account::CacheAccount".
        
        (* 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.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_account_CacheAccount.
      
      Module Impl_core_convert_From_revm_db_states_bundle_account_BundleAccount_for_revm_db_states_cache_account_CacheAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache_account::CacheAccount".
        
        (*
            fn from(account: BundleAccount) -> Self {
                let storage = account
                    .storage
                    .iter()
                    .map(|(k, v)| ( *k, v.present_value))
                    .collect();
                let plain_account = account
                    .account_info()
                    .map(|info| PlainAccount { info, storage });
                Self {
                    account: plain_account,
                    status: account.status,
                }
            }
        *)
        Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ account ] =>
            ltac:(M.monadic
              (let account := M.alloc (| account |) in
              M.read (|
                let~ storage :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::map::Map")
                          []
                          [
                            Ty.apply
                              (Ty.path "std::collections::hash::map::Iter")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "revm_primitives::state::StorageSlot"
                              ];
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ];
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [ Ty.path "revm_primitives::state::StorageSlot" ]
                                      ]
                                  ]
                              ]
                              (Ty.tuple
                                [
                                  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
                                    ]
                                    []
                                ])
                          ],
                        [],
                        "collect",
                        [
                          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"
                            ]
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "std::collections::hash::map::Iter")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "revm_primitives::state::StorageSlot"
                              ],
                            [],
                            "map",
                            [
                              Ty.tuple
                                [
                                  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.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                []
                                            ];
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.path "revm_primitives::state::StorageSlot" ]
                                        ]
                                    ]
                                ]
                                (Ty.tuple
                                  [
                                    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
                                      ]
                                      []
                                  ])
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::HashMap")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.path "revm_primitives::state::StorageSlot";
                                    Ty.path "std::hash::random::RandomState"
                                  ],
                                "iter",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  account,
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "storage"
                                |)
                              ]
                            |);
                            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 k := M.copy (| γ0_0 |) in
                                              let v := M.copy (| γ0_1 |) in
                                              Value.Tuple
                                                [
                                                  M.read (| M.read (| k |) |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| v |),
                                                      "revm_primitives::state::StorageSlot",
                                                      "present_value"
                                                    |)
                                                  |)
                                                ]))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ plain_account :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        "map",
                        [
                          Ty.path "revm::db::states::plain_account::PlainAccount";
                          Ty.function
                            [ Ty.tuple [ Ty.path "revm_primitives::state::AccountInfo" ] ]
                            (Ty.path "revm::db::states::plain_account::PlainAccount")
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm::db::states::bundle_account::BundleAccount",
                            "account_info",
                            []
                          |),
                          [ account ]
                        |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let info := M.copy (| γ |) in
                                          Value.StructRecord
                                            "revm::db::states::plain_account::PlainAccount"
                                            [
                                              ("info", M.read (| info |));
                                              ("storage", M.read (| storage |))
                                            ]))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |) in
                M.alloc (|
                  Value.StructRecord
                    "revm::db::states::cache_account::CacheAccount"
                    [
                      ("account", M.read (| plain_account |));
                      ("status",
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            account,
                            "revm::db::states::bundle_account::BundleAccount",
                            "status"
                          |)
                        |))
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::convert::From"
            Self
            (* Trait polymorphic types *)
            [ (* T *) Ty.path "revm::db::states::bundle_account::BundleAccount" ]
            (* Instance *) [ ("from", InstanceField.Method from) ].
      End Impl_core_convert_From_revm_db_states_bundle_account_BundleAccount_for_revm_db_states_cache_account_CacheAccount.
      
      Module Impl_revm_db_states_cache_account_CacheAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::cache_account::CacheAccount".
        
        (*
            pub fn new_loaded(info: AccountInfo, storage: PlainStorage) -> Self {
                Self {
                    account: Some(PlainAccount { info, storage }),
                    status: AccountStatus::Loaded,
                }
            }
        *)
        Definition new_loaded (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ info; storage ] =>
            ltac:(M.monadic
              (let info := M.alloc (| info |) in
              let storage := M.alloc (| storage |) in
              Value.StructRecord
                "revm::db::states::cache_account::CacheAccount"
                [
                  ("account",
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        Value.StructRecord
                          "revm::db::states::plain_account::PlainAccount"
                          [ ("info", M.read (| info |)); ("storage", M.read (| storage |)) ]
                      ]);
                  ("status",
                    Value.StructTuple "revm::db::states::account_status::AccountStatus::Loaded" [])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_loaded : M.IsAssociatedFunction Self "new_loaded" new_loaded.
        
        (*
            pub fn new_loaded_empty_eip161(storage: PlainStorage) -> Self {
                Self {
                    account: Some(PlainAccount::new_empty_with_storage(storage)),
                    status: AccountStatus::LoadedEmptyEIP161,
                }
            }
        *)
        Definition new_loaded_empty_eip161
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ storage ] =>
            ltac:(M.monadic
              (let storage := M.alloc (| storage |) in
              Value.StructRecord
                "revm::db::states::cache_account::CacheAccount"
                [
                  ("account",
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm::db::states::plain_account::PlainAccount",
                            "new_empty_with_storage",
                            []
                          |),
                          [ M.read (| storage |) ]
                        |)
                      ]);
                  ("status",
                    Value.StructTuple
                      "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                      [])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_loaded_empty_eip161 :
          M.IsAssociatedFunction Self "new_loaded_empty_eip161" new_loaded_empty_eip161.
        
        (*
            pub fn new_loaded_not_existing() -> Self {
                Self {
                    account: None,
                    status: AccountStatus::LoadedNotExisting,
                }
            }
        *)
        Definition new_loaded_not_existing
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "revm::db::states::cache_account::CacheAccount"
                [
                  ("account", Value.StructTuple "core::option::Option::None" []);
                  ("status",
                    Value.StructTuple
                      "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                      [])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_loaded_not_existing :
          M.IsAssociatedFunction Self "new_loaded_not_existing" new_loaded_not_existing.
        
        (*
            pub fn new_newly_created(info: AccountInfo, storage: PlainStorage) -> Self {
                Self {
                    account: Some(PlainAccount { info, storage }),
                    status: AccountStatus::InMemoryChange,
                }
            }
        *)
        Definition new_newly_created (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ info; storage ] =>
            ltac:(M.monadic
              (let info := M.alloc (| info |) in
              let storage := M.alloc (| storage |) in
              Value.StructRecord
                "revm::db::states::cache_account::CacheAccount"
                [
                  ("account",
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        Value.StructRecord
                          "revm::db::states::plain_account::PlainAccount"
                          [ ("info", M.read (| info |)); ("storage", M.read (| storage |)) ]
                      ]);
                  ("status",
                    Value.StructTuple
                      "revm::db::states::account_status::AccountStatus::InMemoryChange"
                      [])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_newly_created :
          M.IsAssociatedFunction Self "new_newly_created" new_newly_created.
        
        (*
            pub fn new_destroyed() -> Self {
                Self {
                    account: None,
                    status: AccountStatus::Destroyed,
                }
            }
        *)
        Definition new_destroyed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "revm::db::states::cache_account::CacheAccount"
                [
                  ("account", Value.StructTuple "core::option::Option::None" []);
                  ("status",
                    Value.StructTuple
                      "revm::db::states::account_status::AccountStatus::Destroyed"
                      [])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_destroyed :
          M.IsAssociatedFunction Self "new_destroyed" new_destroyed.
        
        (*
            pub fn new_changed(info: AccountInfo, storage: PlainStorage) -> Self {
                Self {
                    account: Some(PlainAccount { info, storage }),
                    status: AccountStatus::Changed,
                }
            }
        *)
        Definition new_changed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ info; storage ] =>
            ltac:(M.monadic
              (let info := M.alloc (| info |) in
              let storage := M.alloc (| storage |) in
              Value.StructRecord
                "revm::db::states::cache_account::CacheAccount"
                [
                  ("account",
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        Value.StructRecord
                          "revm::db::states::plain_account::PlainAccount"
                          [ ("info", M.read (| info |)); ("storage", M.read (| storage |)) ]
                      ]);
                  ("status",
                    Value.StructTuple "revm::db::states::account_status::AccountStatus::Changed" [])
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_changed :
          M.IsAssociatedFunction Self "new_changed" new_changed.
        
        (*
            pub fn is_some(&self) -> bool {
                matches!(
                    self.status,
                    AccountStatus::Changed
                        | AccountStatus::InMemoryChange
                        | AccountStatus::DestroyedChanged
                        | AccountStatus::Loaded
                        | AccountStatus::LoadedEmptyEIP161
                )
            }
        *)
        Definition is_some (ε : 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 (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::cache_account::CacheAccount",
                    "status"
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Changed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Loaded"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_is_some : M.IsAssociatedFunction Self "is_some" is_some.
        
        (*
            pub fn storage_slot(&self, slot: U256) -> Option<U256> {
                self.account
                    .as_ref()
                    .and_then(|a| a.storage.get(&slot).cloned())
            }
        *)
        Definition storage_slot (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; slot ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let slot := M.alloc (| slot |) 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" ]
                    ],
                  "and_then",
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [];
                    Ty.function
                      [
                        Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                          ]
                      ]
                      (Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ])
                  ]
                |),
                [
                  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 (| self |),
                        "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 a := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  []
                                              ]
                                          ],
                                        "cloned",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "std::collections::hash::map::HashMap")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [];
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [];
                                                Ty.path "std::hash::random::RandomState"
                                              ],
                                            "get",
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                []
                                            ]
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| a |),
                                              "revm::db::states::plain_account::PlainAccount",
                                              "storage"
                                            |);
                                            slot
                                          ]
                                        |)
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_storage_slot :
          M.IsAssociatedFunction Self "storage_slot" storage_slot.
        
        (*
            pub fn account_info(&self) -> Option<AccountInfo> {
                self.account.as_ref().map(|a| a.info.clone())
            }
        *)
        Definition account_info (ε : 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_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [
                      Ty.apply
                        (Ty.path "&")
                        []
                        [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                    ],
                  "map",
                  [
                    Ty.path "revm_primitives::state::AccountInfo";
                    Ty.function
                      [
                        Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                          ]
                      ]
                      (Ty.path "revm_primitives::state::AccountInfo")
                  ]
                |),
                [
                  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 (| self |),
                        "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 a := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::clone::Clone",
                                        Ty.path "revm_primitives::state::AccountInfo",
                                        [],
                                        "clone",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| a |),
                                          "revm::db::states::plain_account::PlainAccount",
                                          "info"
                                        |)
                                      ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_account_info :
          M.IsAssociatedFunction Self "account_info" account_info.
        
        (*
            pub fn into_components(self) -> (Option<(AccountInfo, PlainStorage)>, AccountStatus) {
                (self.account.map(|a| a.into_components()), self.status)
            }
        *)
        Definition into_components (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.Tuple
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                      "map",
                      [
                        Ty.tuple
                          [
                            Ty.path "revm_primitives::state::AccountInfo";
                            Ty.apply
                              (Ty.path "std::collections::hash::map::HashMap")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "std::hash::random::RandomState"
                              ]
                          ];
                        Ty.function
                          [ Ty.tuple [ Ty.path "revm::db::states::plain_account::PlainAccount" ] ]
                          (Ty.tuple
                            [
                              Ty.path "revm_primitives::state::AccountInfo";
                              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"
                                ]
                            ])
                      ]
                    |),
                    [
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          self,
                          "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 a := M.copy (| γ |) in
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm::db::states::plain_account::PlainAccount",
                                            "into_components",
                                            []
                                          |),
                                          [ M.read (| a |) ]
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      self,
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |)
                  |)
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_into_components :
          M.IsAssociatedFunction Self "into_components" into_components.
        
        (*
            pub fn touch_create_pre_eip161(
                &mut self,
                storage: StorageWithOriginalValues,
            ) -> Option<TransitionAccount> {
                let previous_status = self.status;
        
                let had_no_info = self
                    .account
                    .as_ref()
                    .map(|a| a.info.is_empty())
                    .unwrap_or_default();
                self.status = self.status.on_touched_created_pre_eip161(had_no_info)?;
        
                let plain_storage = storage.iter().map(|(k, v)| ( *k, v.present_value)).collect();
                let previous_info = self.account.take().map(|a| a.info);
        
                self.account = Some(PlainAccount::new_empty_with_storage(plain_storage));
        
                Some(TransitionAccount {
                    info: Some(AccountInfo::default()),
                    status: self.status,
                    previous_info,
                    previous_status,
                    storage,
                    storage_was_destroyed: false,
                })
            }
        *)
        Definition touch_create_pre_eip161
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; storage ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let storage := M.alloc (| storage |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ previous_status :=
                      M.copy (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "status"
                        |)
                      |) in
                    let~ had_no_info :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "bool" ],
                            "unwrap_or_default",
                            []
                          |),
                          [
                            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.path "bool";
                                  Ty.function
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.path
                                                "revm::db::states::plain_account::PlainAccount"
                                            ]
                                        ]
                                    ]
                                    (Ty.path "bool")
                                ]
                              |),
                              [
                                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 (| self |),
                                      "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 a := M.copy (| γ |) in
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_primitives::state::AccountInfo",
                                                      "is_empty",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| a |),
                                                        "revm::db::states::plain_account::PlainAccount",
                                                        "info"
                                                      |)
                                                    ]
                                                  |)))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.write (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "status"
                        |),
                        M.read (|
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::try_trait::Try",
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [ Ty.path "revm::db::states::account_status::AccountStatus" ],
                                  [],
                                  "branch",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm::db::states::account_status::AccountStatus",
                                      "on_touched_created_pre_eip161",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm::db::states::cache_account::CacheAccount",
                                        "status"
                                      |);
                                      M.read (| had_no_info |)
                                    ]
                                  |)
                                ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::ops::control_flow::ControlFlow::Break",
                                      0
                                    |) in
                                  let residual := M.copy (| γ0_0 |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::FromResidual",
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [
                                                  Ty.path
                                                    "revm::db::states::transition_account::TransitionAccount"
                                                ],
                                              [
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "core::convert::Infallible" ]
                                              ],
                                              "from_residual",
                                              []
                                            |),
                                            [ M.read (| residual |) ]
                                          |)
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::ops::control_flow::ControlFlow::Continue",
                                      0
                                    |) in
                                  let val := M.copy (| γ0_0 |) in
                                  val))
                            ]
                          |)
                        |)
                      |) in
                    let~ plain_storage :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "core::iter::adapters::map::Map")
                              []
                              [
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::Iter")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.path "revm_primitives::state::StorageSlot"
                                  ];
                                Ty.function
                                  [
                                    Ty.tuple
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  []
                                              ];
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [ Ty.path "revm_primitives::state::StorageSlot" ]
                                          ]
                                      ]
                                  ]
                                  (Ty.tuple
                                    [
                                      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
                                        ]
                                        []
                                    ])
                              ],
                            [],
                            "collect",
                            [
                              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"
                                ]
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::Iter")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.path "revm_primitives::state::StorageSlot"
                                  ],
                                [],
                                "map",
                                [
                                  Ty.tuple
                                    [
                                      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.function
                                    [
                                      Ty.tuple
                                        [
                                          Ty.tuple
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "ruint::Uint")
                                                    [
                                                      Value.Integer IntegerKind.Usize 256;
                                                      Value.Integer IntegerKind.Usize 4
                                                    ]
                                                    []
                                                ];
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.path "revm_primitives::state::StorageSlot" ]
                                            ]
                                        ]
                                    ]
                                    (Ty.tuple
                                      [
                                        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
                                          ]
                                          []
                                      ])
                                ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "std::collections::hash::map::HashMap")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [];
                                        Ty.path "revm_primitives::state::StorageSlot";
                                        Ty.path "std::hash::random::RandomState"
                                      ],
                                    "iter",
                                    []
                                  |),
                                  [ storage ]
                                |);
                                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 k := M.copy (| γ0_0 |) in
                                                  let v := M.copy (| γ0_1 |) in
                                                  Value.Tuple
                                                    [
                                                      M.read (| M.read (| k |) |);
                                                      M.read (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| v |),
                                                          "revm_primitives::state::StorageSlot",
                                                          "present_value"
                                                        |)
                                                      |)
                                                    ]))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |)
                          ]
                        |)
                      |) in
                    let~ previous_info :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                            "map",
                            [
                              Ty.path "revm_primitives::state::AccountInfo";
                              Ty.function
                                [
                                  Ty.tuple
                                    [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                                ]
                                (Ty.path "revm_primitives::state::AccountInfo")
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                                "take",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "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 a := M.copy (| γ |) in
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  a,
                                                  "revm::db::states::plain_account::PlainAccount",
                                                  "info"
                                                |)
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.write (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "account"
                        |),
                        Value.StructTuple
                          "core::option::Option::Some"
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm::db::states::plain_account::PlainAccount",
                                "new_empty_with_storage",
                                []
                              |),
                              [ M.read (| plain_storage |) ]
                            |)
                          ]
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "core::option::Option::Some"
                        [
                          Value.StructRecord
                            "revm::db::states::transition_account::TransitionAccount"
                            [
                              ("info",
                                Value.StructTuple
                                  "core::option::Option::Some"
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::default::Default",
                                        Ty.path "revm_primitives::state::AccountInfo",
                                        [],
                                        "default",
                                        []
                                      |),
                                      []
                                    |)
                                  ]);
                              ("status",
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm::db::states::cache_account::CacheAccount",
                                    "status"
                                  |)
                                |));
                              ("previous_info", M.read (| previous_info |));
                              ("previous_status", M.read (| previous_status |));
                              ("storage", M.read (| storage |));
                              ("storage_was_destroyed", Value.Bool false)
                            ]
                        ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_touch_create_pre_eip161 :
          M.IsAssociatedFunction Self "touch_create_pre_eip161" touch_create_pre_eip161.
        
        (*
            pub fn touch_empty_eip161(&mut self) -> Option<TransitionAccount> {
                let previous_status = self.status;
        
                // Set account to None.
                let previous_info = self.account.take().map(|acc| acc.info);
        
                // Set account state to Destroyed as we need to clear the storage if it exist.
                self.status = self.status.on_touched_empty_post_eip161();
        
                if matches!(
                    previous_status,
                    AccountStatus::LoadedNotExisting
                        | AccountStatus::Destroyed
                        | AccountStatus::DestroyedAgain
                ) {
                    None
                } else {
                    Some(TransitionAccount {
                        info: None,
                        status: self.status,
                        previous_info,
                        previous_status,
                        storage: HashMap::default(),
                        storage_was_destroyed: true,
                    })
                }
            }
        *)
        Definition touch_empty_eip161 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ previous_status :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |)
                  |) in
                let~ previous_info :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                        "map",
                        [
                          Ty.path "revm_primitives::state::AccountInfo";
                          Ty.function
                            [ Ty.tuple [ Ty.path "revm::db::states::plain_account::PlainAccount" ] ]
                            (Ty.path "revm_primitives::state::AccountInfo")
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                            "take",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "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 acc := M.copy (| γ |) in
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              acc,
                                              "revm::db::states::plain_account::PlainAccount",
                                              "info"
                                            |)
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        "on_touched_empty_post_eip161",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "status"
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.match_operator (|
                              previous_status,
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.find_or_pattern (|
                                      γ,
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                              |) in
                                            Value.Tuple []));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "revm::db::states::account_status::AccountStatus::Destroyed"
                                              |) in
                                            Value.Tuple []));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                              |) in
                                            Value.Tuple []))
                                      ],
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                              ]
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              Value.StructRecord
                                "revm::db::states::transition_account::TransitionAccount"
                                [
                                  ("info", Value.StructTuple "core::option::Option::None" []);
                                  ("status",
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm::db::states::cache_account::CacheAccount",
                                        "status"
                                      |)
                                    |));
                                  ("previous_info", M.read (| previous_info |));
                                  ("previous_status", M.read (| previous_status |));
                                  ("storage",
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::default::Default",
                                        Ty.apply
                                          (Ty.path "std::collections::hash::map::HashMap")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [];
                                            Ty.path "revm_primitives::state::StorageSlot";
                                            Ty.path "std::hash::random::RandomState"
                                          ],
                                        [],
                                        "default",
                                        []
                                      |),
                                      []
                                    |));
                                  ("storage_was_destroyed", Value.Bool true)
                                ]
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_touch_empty_eip161 :
          M.IsAssociatedFunction Self "touch_empty_eip161" touch_empty_eip161.
        
        (*
            pub fn selfdestruct(&mut self) -> Option<TransitionAccount> {
                // account should be None after selfdestruct so we can take it.
                let previous_info = self.account.take().map(|a| a.info);
                let previous_status = self.status;
        
                self.status = self.status.on_selfdestructed();
        
                if previous_status == AccountStatus::LoadedNotExisting {
                    None
                } else {
                    Some(TransitionAccount {
                        info: None,
                        status: self.status,
                        previous_info,
                        previous_status,
                        storage: HashMap::new(),
                        storage_was_destroyed: true,
                    })
                }
            }
        *)
        Definition selfdestruct (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ previous_info :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                        "map",
                        [
                          Ty.path "revm_primitives::state::AccountInfo";
                          Ty.function
                            [ Ty.tuple [ Ty.path "revm::db::states::plain_account::PlainAccount" ] ]
                            (Ty.path "revm_primitives::state::AccountInfo")
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                            "take",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "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 a := M.copy (| γ |) in
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              a,
                                              "revm::db::states::plain_account::PlainAccount",
                                              "info"
                                            |)
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |) in
                let~ previous_status :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        "on_selfdestructed",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "status"
                        |)
                      ]
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.path "revm::db::states::account_status::AccountStatus",
                                  [ Ty.path "revm::db::states::account_status::AccountStatus" ],
                                  "eq",
                                  []
                                |),
                                [
                                  previous_status;
                                  M.alloc (|
                                    Value.StructTuple
                                      "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                      []
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              Value.StructRecord
                                "revm::db::states::transition_account::TransitionAccount"
                                [
                                  ("info", Value.StructTuple "core::option::Option::None" []);
                                  ("status",
                                    M.read (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm::db::states::cache_account::CacheAccount",
                                        "status"
                                      |)
                                    |));
                                  ("previous_info", M.read (| previous_info |));
                                  ("previous_status", M.read (| previous_status |));
                                  ("storage",
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "std::collections::hash::map::HashMap")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [];
                                            Ty.path "revm_primitives::state::StorageSlot";
                                            Ty.path "std::hash::random::RandomState"
                                          ],
                                        "new",
                                        []
                                      |),
                                      []
                                    |));
                                  ("storage_was_destroyed", Value.Bool true)
                                ]
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_selfdestruct :
          M.IsAssociatedFunction Self "selfdestruct" selfdestruct.
        
        (*
            pub fn newly_created(
                &mut self,
                new_info: AccountInfo,
                new_storage: StorageWithOriginalValues,
            ) -> TransitionAccount {
                let previous_status = self.status;
                let previous_info = self.account.take().map(|a| a.info);
        
                let new_bundle_storage = new_storage
                    .iter()
                    .map(|(k, s)| ( *k, s.present_value))
                    .collect();
        
                self.status = self.status.on_created();
                let transition_account = TransitionAccount {
                    info: Some(new_info.clone()),
                    status: self.status,
                    previous_status,
                    previous_info,
                    storage: new_storage,
                    storage_was_destroyed: false,
                };
                self.account = Some(PlainAccount {
                    info: new_info,
                    storage: new_bundle_storage,
                });
                transition_account
            }
        *)
        Definition newly_created (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; new_info; new_storage ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let new_info := M.alloc (| new_info |) in
              let new_storage := M.alloc (| new_storage |) in
              M.read (|
                let~ previous_status :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |)
                  |) in
                let~ previous_info :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                        "map",
                        [
                          Ty.path "revm_primitives::state::AccountInfo";
                          Ty.function
                            [ Ty.tuple [ Ty.path "revm::db::states::plain_account::PlainAccount" ] ]
                            (Ty.path "revm_primitives::state::AccountInfo")
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                            "take",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "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 a := M.copy (| γ |) in
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              a,
                                              "revm::db::states::plain_account::PlainAccount",
                                              "info"
                                            |)
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |) in
                let~ new_bundle_storage :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::iterator::Iterator",
                        Ty.apply
                          (Ty.path "core::iter::adapters::map::Map")
                          []
                          [
                            Ty.apply
                              (Ty.path "std::collections::hash::map::Iter")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "revm_primitives::state::StorageSlot"
                              ];
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ];
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [ Ty.path "revm_primitives::state::StorageSlot" ]
                                      ]
                                  ]
                              ]
                              (Ty.tuple
                                [
                                  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
                                    ]
                                    []
                                ])
                          ],
                        [],
                        "collect",
                        [
                          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"
                            ]
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "std::collections::hash::map::Iter")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "revm_primitives::state::StorageSlot"
                              ],
                            [],
                            "map",
                            [
                              Ty.tuple
                                [
                                  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.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                []
                                            ];
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.path "revm_primitives::state::StorageSlot" ]
                                        ]
                                    ]
                                ]
                                (Ty.tuple
                                  [
                                    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
                                      ]
                                      []
                                  ])
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::HashMap")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.path "revm_primitives::state::StorageSlot";
                                    Ty.path "std::hash::random::RandomState"
                                  ],
                                "iter",
                                []
                              |),
                              [ new_storage ]
                            |);
                            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 k := M.copy (| γ0_0 |) in
                                              let s := M.copy (| γ0_1 |) in
                                              Value.Tuple
                                                [
                                                  M.read (| M.read (| k |) |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| s |),
                                                      "revm_primitives::state::StorageSlot",
                                                      "present_value"
                                                    |)
                                                  |)
                                                ]))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        "on_created",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "status"
                        |)
                      ]
                    |)
                  |) in
                let~ transition_account :=
                  M.alloc (|
                    Value.StructRecord
                      "revm::db::states::transition_account::TransitionAccount"
                      [
                        ("info",
                          Value.StructTuple
                            "core::option::Option::Some"
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::clone::Clone",
                                  Ty.path "revm_primitives::state::AccountInfo",
                                  [],
                                  "clone",
                                  []
                                |),
                                [ new_info ]
                              |)
                            ]);
                        ("status",
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::cache_account::CacheAccount",
                              "status"
                            |)
                          |));
                        ("previous_status", M.read (| previous_status |));
                        ("previous_info", M.read (| previous_info |));
                        ("storage", M.read (| new_storage |));
                        ("storage_was_destroyed", Value.Bool false)
                      ]
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "account"
                    |),
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        Value.StructRecord
                          "revm::db::states::plain_account::PlainAccount"
                          [
                            ("info", M.read (| new_info |));
                            ("storage", M.read (| new_bundle_storage |))
                          ]
                      ]
                  |) in
                transition_account
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_newly_created :
          M.IsAssociatedFunction Self "newly_created" newly_created.
        
        (*
            pub fn increment_balance(&mut self, balance: u128) -> Option<TransitionAccount> {
                if balance == 0 {
                    return None;
                }
                let (_, transition) = self.account_info_change(|info| {
                    info.balance = info.balance.saturating_add(U256::from(balance));
                });
                Some(transition)
            }
        *)
        Definition increment_balance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; balance ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let balance := M.alloc (| balance |) 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 (|
                                    BinOp.eq (|
                                      M.read (| balance |),
                                      Value.Integer IntegerKind.U128 0
                                    |)
                                  |)) 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
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm::db::states::cache_account::CacheAccount",
                            "account_info_change",
                            [
                              Ty.tuple [];
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&mut")
                                        []
                                        [ Ty.path "revm_primitives::state::AccountInfo" ]
                                    ]
                                ]
                                (Ty.tuple [])
                            ]
                          |),
                          [
                            M.read (| self |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let info := M.copy (| γ |) in
                                              M.read (|
                                                let~ _ :=
                                                  M.write (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| info |),
                                                      "revm_primitives::state::AccountInfo",
                                                      "balance"
                                                    |),
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          [],
                                                        "saturating_add",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| info |),
                                                            "revm_primitives::state::AccountInfo",
                                                            "balance"
                                                          |)
                                                        |);
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "ruint::Uint")
                                                              [
                                                                Value.Integer IntegerKind.Usize 256;
                                                                Value.Integer IntegerKind.Usize 4
                                                              ]
                                                              [],
                                                            "from",
                                                            [ Ty.path "u128" ]
                                                          |),
                                                          [ M.read (| balance |) ]
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                M.alloc (| Value.Tuple [] |)
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      |),
                      [
                        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 transition := M.copy (| γ0_1 |) in
                            M.alloc (|
                              Value.StructTuple
                                "core::option::Option::Some"
                                [ M.read (| transition |) ]
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_increment_balance :
          M.IsAssociatedFunction Self "increment_balance" increment_balance.
        
        (*
            fn account_info_change<T, F: FnOnce(&mut AccountInfo) -> T>(
                &mut self,
                change: F,
            ) -> (T, TransitionAccount) {
                let previous_status = self.status;
                let previous_info = self.account_info();
                let mut account = self.account.take().unwrap_or_default();
                let output = change(&mut account.info);
                self.account = Some(account);
        
                let had_no_nonce_and_code = previous_info
                    .as_ref()
                    .map(AccountInfo::has_no_code_and_nonce)
                    .unwrap_or_default();
                self.status = self.status.on_changed(had_no_nonce_and_code);
        
                (
                    output,
                    TransitionAccount {
                        info: self.account_info(),
                        status: self.status,
                        previous_info,
                        previous_status,
                        storage: HashMap::new(),
                        storage_was_destroyed: false,
                    },
                )
            }
        *)
        Definition account_info_change (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ T; F ], [ self; change ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let change := M.alloc (| change |) in
              M.read (|
                let~ previous_status :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |)
                  |) in
                let~ previous_info :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::db::states::cache_account::CacheAccount",
                        "account_info",
                        []
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ account :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                        "unwrap_or_default",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                            "take",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::cache_account::CacheAccount",
                              "account"
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ output :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::function::FnOnce",
                        F,
                        [
                          Ty.tuple
                            [
                              Ty.apply
                                (Ty.path "&mut")
                                []
                                [ Ty.path "revm_primitives::state::AccountInfo" ]
                            ]
                        ],
                        "call_once",
                        []
                      |),
                      [
                        M.read (| change |);
                        Value.Tuple
                          [
                            M.SubPointer.get_struct_record_field (|
                              account,
                              "revm::db::states::plain_account::PlainAccount",
                              "info"
                            |)
                          ]
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "account"
                    |),
                    Value.StructTuple "core::option::Option::Some" [ M.read (| account |) ]
                  |) in
                let~ had_no_nonce_and_code :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "bool" ],
                        "unwrap_or_default",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ]
                              ],
                            "map",
                            [
                              Ty.path "bool";
                              Ty.function
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "revm_primitives::state::AccountInfo" ]
                                ]
                                (Ty.path "bool")
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ],
                                "as_ref",
                                []
                              |),
                              [ previous_info ]
                            |);
                            M.get_associated_function (|
                              Ty.path "revm_primitives::state::AccountInfo",
                              "has_no_code_and_nonce",
                              []
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        "on_changed",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "status"
                        |);
                        M.read (| had_no_nonce_and_code |)
                      ]
                    |)
                  |) in
                M.alloc (|
                  Value.Tuple
                    [
                      M.read (| output |);
                      Value.StructRecord
                        "revm::db::states::transition_account::TransitionAccount"
                        [
                          ("info",
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "revm::db::states::cache_account::CacheAccount",
                                "account_info",
                                []
                              |),
                              [ M.read (| self |) ]
                            |));
                          ("status",
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm::db::states::cache_account::CacheAccount",
                                "status"
                              |)
                            |));
                          ("previous_info", M.read (| previous_info |));
                          ("previous_status", M.read (| previous_status |));
                          ("storage",
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::HashMap")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.path "revm_primitives::state::StorageSlot";
                                    Ty.path "std::hash::random::RandomState"
                                  ],
                                "new",
                                []
                              |),
                              []
                            |));
                          ("storage_was_destroyed", Value.Bool false)
                        ]
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_account_info_change :
          M.IsAssociatedFunction Self "account_info_change" account_info_change.
        
        (*
            pub fn drain_balance(&mut self) -> (u128, TransitionAccount) {
                self.account_info_change(|info| {
                    let output = info.balance;
                    info.balance = U256::ZERO;
                    output.try_into().unwrap()
                })
            }
        *)
        Definition drain_balance (ε : 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_associated_function (|
                  Ty.path "revm::db::states::cache_account::CacheAccount",
                  "account_info_change",
                  [
                    Ty.path "u128";
                    Ty.function
                      [
                        Ty.tuple
                          [
                            Ty.apply
                              (Ty.path "&mut")
                              []
                              [ Ty.path "revm_primitives::state::AccountInfo" ]
                          ]
                      ]
                      (Ty.path "u128")
                  ]
                |),
                [
                  M.read (| self |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let info := M.copy (| γ |) in
                                    M.read (|
                                      let~ output :=
                                        M.copy (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| info |),
                                            "revm_primitives::state::AccountInfo",
                                            "balance"
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| info |),
                                            "revm_primitives::state::AccountInfo",
                                            "balance"
                                          |),
                                          M.read (| M.get_constant (| "ruint::ZERO" |) |)
                                        |) in
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::result::Result")
                                              []
                                              [
                                                Ty.path "u128";
                                                Ty.apply
                                                  (Ty.path "ruint::from::FromUintError")
                                                  []
                                                  [ Ty.path "u128" ]
                                              ],
                                            "unwrap",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::convert::TryInto",
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                [ Ty.path "u128" ],
                                                "try_into",
                                                []
                                              |),
                                              [ M.read (| output |) ]
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_drain_balance :
          M.IsAssociatedFunction Self "drain_balance" drain_balance.
        
        (*
            pub fn change(
                &mut self,
                new: AccountInfo,
                storage: StorageWithOriginalValues,
            ) -> TransitionAccount {
                let previous_status = self.status;
                let previous_info = self.account.as_ref().map(|a| a.info.clone());
                let mut this_storage = self
                    .account
                    .take()
                    .map(|acc| acc.storage)
                    .unwrap_or_default();
        
                this_storage.extend(storage.iter().map(|(k, s)| ( *k, s.present_value)));
                let changed_account = PlainAccount {
                    info: new,
                    storage: this_storage,
                };
        
                let had_no_nonce_and_code = previous_info
                    .as_ref()
                    .map(AccountInfo::has_no_code_and_nonce)
                    .unwrap_or_default();
                self.status = self.status.on_changed(had_no_nonce_and_code);
                self.account = Some(changed_account);
        
                TransitionAccount {
                    info: self.account.as_ref().map(|a| a.info.clone()),
                    status: self.status,
                    previous_info,
                    previous_status,
                    storage,
                    storage_was_destroyed: false,
                }
            }
        *)
        Definition change (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; new; storage ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let new := M.alloc (| new |) in
              let storage := M.alloc (| storage |) in
              M.read (|
                let~ previous_status :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |)
                  |) in
                let~ previous_info :=
                  M.alloc (|
                    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.path "revm_primitives::state::AccountInfo";
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                                ]
                            ]
                            (Ty.path "revm_primitives::state::AccountInfo")
                        ]
                      |),
                      [
                        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 (| self |),
                              "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 a := M.copy (| γ |) in
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::clone::Clone",
                                              Ty.path "revm_primitives::state::AccountInfo",
                                              [],
                                              "clone",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| a |),
                                                "revm::db::states::plain_account::PlainAccount",
                                                "info"
                                              |)
                                            ]
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |) in
                let~ this_storage :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [
                            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"
                              ]
                          ],
                        "unwrap_or_default",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                            "map",
                            [
                              Ty.apply
                                (Ty.path "std::collections::hash::map::HashMap")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [];
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [];
                                  Ty.path "std::hash::random::RandomState"
                                ];
                              Ty.function
                                [
                                  Ty.tuple
                                    [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                                ]
                                (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"
                                  ])
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "revm::db::states::plain_account::PlainAccount" ],
                                "take",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "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 acc := M.copy (| γ |) in
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  acc,
                                                  "revm::db::states::plain_account::PlainAccount",
                                                  "storage"
                                                |)
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::Extend",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [
                          Ty.tuple
                            [
                              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
                                ]
                                []
                            ]
                        ],
                        "extend",
                        [
                          Ty.apply
                            (Ty.path "core::iter::adapters::map::Map")
                            []
                            [
                              Ty.apply
                                (Ty.path "std::collections::hash::map::Iter")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [];
                                  Ty.path "revm_primitives::state::StorageSlot"
                                ];
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                []
                                            ];
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.path "revm_primitives::state::StorageSlot" ]
                                        ]
                                    ]
                                ]
                                (Ty.tuple
                                  [
                                    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
                                      ]
                                      []
                                  ])
                            ]
                        ]
                      |),
                      [
                        this_storage;
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::iterator::Iterator",
                            Ty.apply
                              (Ty.path "std::collections::hash::map::Iter")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "revm_primitives::state::StorageSlot"
                              ],
                            [],
                            "map",
                            [
                              Ty.tuple
                                [
                                  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.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                []
                                            ];
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [ Ty.path "revm_primitives::state::StorageSlot" ]
                                        ]
                                    ]
                                ]
                                (Ty.tuple
                                  [
                                    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
                                      ]
                                      []
                                  ])
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::HashMap")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.path "revm_primitives::state::StorageSlot";
                                    Ty.path "std::hash::random::RandomState"
                                  ],
                                "iter",
                                []
                              |),
                              [ storage ]
                            |);
                            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 k := M.copy (| γ0_0 |) in
                                              let s := M.copy (| γ0_1 |) in
                                              Value.Tuple
                                                [
                                                  M.read (| M.read (| k |) |);
                                                  M.read (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| s |),
                                                      "revm_primitives::state::StorageSlot",
                                                      "present_value"
                                                    |)
                                                  |)
                                                ]))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ changed_account :=
                  M.alloc (|
                    Value.StructRecord
                      "revm::db::states::plain_account::PlainAccount"
                      [ ("info", M.read (| new |)); ("storage", M.read (| this_storage |)) ]
                  |) in
                let~ had_no_nonce_and_code :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "bool" ],
                        "unwrap_or_default",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ]
                              ],
                            "map",
                            [
                              Ty.path "bool";
                              Ty.function
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "revm_primitives::state::AccountInfo" ]
                                ]
                                (Ty.path "bool")
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ],
                                "as_ref",
                                []
                              |),
                              [ previous_info ]
                            |);
                            M.get_associated_function (|
                              Ty.path "revm_primitives::state::AccountInfo",
                              "has_no_code_and_nonce",
                              []
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "status"
                    |),
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        "on_changed",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::cache_account::CacheAccount",
                          "status"
                        |);
                        M.read (| had_no_nonce_and_code |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::cache_account::CacheAccount",
                      "account"
                    |),
                    Value.StructTuple "core::option::Option::Some" [ M.read (| changed_account |) ]
                  |) in
                M.alloc (|
                  Value.StructRecord
                    "revm::db::states::transition_account::TransitionAccount"
                    [
                      ("info",
                        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.path "revm_primitives::state::AccountInfo";
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [ Ty.path "revm::db::states::plain_account::PlainAccount" ]
                                    ]
                                ]
                                (Ty.path "revm_primitives::state::AccountInfo")
                            ]
                          |),
                          [
                            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 (| self |),
                                  "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 a := M.copy (| γ |) in
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::clone::Clone",
                                                  Ty.path "revm_primitives::state::AccountInfo",
                                                  [],
                                                  "clone",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| a |),
                                                    "revm::db::states::plain_account::PlainAccount",
                                                    "info"
                                                  |)
                                                ]
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |));
                      ("status",
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::cache_account::CacheAccount",
                            "status"
                          |)
                        |));
                      ("previous_info", M.read (| previous_info |));
                      ("previous_status", M.read (| previous_status |));
                      ("storage", M.read (| storage |));
                      ("storage_was_destroyed", Value.Bool false)
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_change : M.IsAssociatedFunction Self "change" change.
      End Impl_revm_db_states_cache_account_CacheAccount.
    End cache_account.
  End states.
End db.
