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

Module db.
  Module states.
    Module bundle_account.
      (* StructRecord
        {
          name := "BundleAccount";
          const_params := [];
          ty_params := [];
          fields :=
            [
              ("info",
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "revm_primitives::state::AccountInfo" ]);
              ("original_info",
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "revm_primitives::state::AccountInfo" ]);
              ("storage",
                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"
                  ]);
              ("status", Ty.path "revm::db::states::account_status::AccountStatus")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_bundle_account_BundleAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::bundle_account::BundleAccount".
        
        (* 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::bundle_account::BundleAccount"
                [
                  ("info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::bundle_account::BundleAccount",
                          "info"
                        |)
                      ]
                    |));
                  ("original_info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::bundle_account::BundleAccount",
                          "original_info"
                        |)
                      ]
                    |));
                  ("storage",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        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"
                          ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::bundle_account::BundleAccount",
                          "storage"
                        |)
                      ]
                    |));
                  ("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::bundle_account::BundleAccount",
                          "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_bundle_account_BundleAccount.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_bundle_account_BundleAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::bundle_account::BundleAccount".
        
        (* 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_field4_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "BundleAccount" |);
                  M.read (| Value.String "info" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::bundle_account::BundleAccount",
                    "info"
                  |);
                  M.read (| Value.String "original_info" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::bundle_account::BundleAccount",
                    "original_info"
                  |);
                  M.read (| Value.String "storage" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::bundle_account::BundleAccount",
                    "storage"
                  |);
                  M.read (| Value.String "status" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::bundle_account::BundleAccount",
                      "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_bundle_account_BundleAccount.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_bundle_account_BundleAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::bundle_account::BundleAccount".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_bundle_account_BundleAccount.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_bundle_account_BundleAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::bundle_account::BundleAccount".
        
        (* PartialEq *)
        Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; other ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let other := M.alloc (| other |) in
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "revm_primitives::state::AccountInfo" ]
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::bundle_account::BundleAccount",
                          "info"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm::db::states::bundle_account::BundleAccount",
                          "info"
                        |)
                      ]
                    |),
                    ltac:(M.monadic
                      (M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "revm_primitives::state::AccountInfo" ],
                          [
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm_primitives::state::AccountInfo" ]
                          ],
                          "eq",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::bundle_account::BundleAccount",
                            "original_info"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "revm::db::states::bundle_account::BundleAccount",
                            "original_info"
                          |)
                        ]
                      |)))
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "revm_primitives::state::StorageSlot";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [
                          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"
                            ]
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::bundle_account::BundleAccount",
                          "storage"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm::db::states::bundle_account::BundleAccount",
                          "storage"
                        |)
                      ]
                    |)))
                |),
                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::bundle_account::BundleAccount",
                        "status"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm::db::states::bundle_account::BundleAccount",
                        "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_bundle_account_BundleAccount.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_bundle_account_BundleAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::bundle_account::BundleAccount".
        
        (* Eq *)
        Definition assert_receiver_is_total_eq
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          Value.DeclaredButUndefined,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  Value.DeclaredButUndefined,
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.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_bundle_account_BundleAccount.
      
      Module Impl_revm_db_states_bundle_account_BundleAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::bundle_account::BundleAccount".
        
        (*
            pub fn new(
                original_info: Option<AccountInfo>,
                present_info: Option<AccountInfo>,
                storage: StorageWithOriginalValues,
                status: AccountStatus,
            ) -> Self {
                Self {
                    info: present_info,
                    original_info,
                    storage,
                    status,
                }
            }
        *)
        Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ original_info; present_info; storage; status ] =>
            ltac:(M.monadic
              (let original_info := M.alloc (| original_info |) in
              let present_info := M.alloc (| present_info |) in
              let storage := M.alloc (| storage |) in
              let status := M.alloc (| status |) in
              Value.StructRecord
                "revm::db::states::bundle_account::BundleAccount"
                [
                  ("info", M.read (| present_info |));
                  ("original_info", M.read (| original_info |));
                  ("storage", M.read (| storage |));
                  ("status", M.read (| status |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
        
        (*
            pub fn size_hint(&self) -> usize {
                1 + self.storage.len()
            }
        *)
        Definition size_hint (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              BinOp.Wrap.add (|
                Value.Integer IntegerKind.Usize 1,
                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"
                      ],
                    "len",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::bundle_account::BundleAccount",
                      "storage"
                    |)
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_size_hint : M.IsAssociatedFunction Self "size_hint" size_hint.
        
        (*
            pub fn storage_slot(&self, slot: U256) -> Option<U256> {
                let slot = self.storage.get(&slot).map(|s| s.present_value);
                if slot.is_some() {
                    slot
                } else if self.status.is_storage_known() {
                    Some(U256::ZERO)
                } else {
                    None
                }
            }
        *)
        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.read (|
                let~ slot :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [
                            Ty.apply
                              (Ty.path "&")
                              []
                              [ Ty.path "revm_primitives::state::StorageSlot" ]
                          ],
                        "map",
                        [
                          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_primitives::state::StorageSlot" ]
                                ]
                            ]
                            (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"
                              ],
                            "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 (| self |),
                              "revm::db::states::bundle_account::BundleAccount",
                              "storage"
                            |);
                            slot
                          ]
                        |);
                        M.closure
                          (fun γ =>
                            ltac:(M.monadic
                              match γ with
                              | [ α0 ] =>
                                ltac:(M.monadic
                                  (M.match_operator (|
                                    M.alloc (| α0 |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let s := M.copy (| γ |) in
                                          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
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        []
                                    ],
                                  "is_some",
                                  []
                                |),
                                [ slot ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        slot));
                    fun γ =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.path "revm::db::states::account_status::AccountStatus",
                                          "is_storage_known",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm::db::states::bundle_account::BundleAccount",
                                            "status"
                                          |)
                                        ]
                                      |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  Value.StructTuple
                                    "core::option::Option::Some"
                                    [ M.read (| M.get_constant (| "ruint::ZERO" |) |) ]
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                          ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => 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.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_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.path "revm_primitives::state::AccountInfo" ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::bundle_account::BundleAccount",
                    "info"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_account_info :
          M.IsAssociatedFunction Self "account_info" account_info.
        
        (*
            pub fn was_destroyed(&self) -> bool {
                self.status.was_destroyed()
            }
        *)
        Definition was_destroyed (ε : 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::account_status::AccountStatus",
                  "was_destroyed",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::bundle_account::BundleAccount",
                    "status"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_was_destroyed :
          M.IsAssociatedFunction Self "was_destroyed" was_destroyed.
        
        (*
            pub fn is_info_changed(&self) -> bool {
                self.info != self.original_info
            }
        *)
        Definition is_info_changed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.path "revm_primitives::state::AccountInfo" ],
                  [
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "revm_primitives::state::AccountInfo" ]
                  ],
                  "ne",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::bundle_account::BundleAccount",
                    "info"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::bundle_account::BundleAccount",
                    "original_info"
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_is_info_changed :
          M.IsAssociatedFunction Self "is_info_changed" is_info_changed.
        
        (*
            pub fn is_contract_changed(&self) -> bool {
                self.info.as_ref().map(|a| a.code_hash) != self.original_info.as_ref().map(|a| a.code_hash)
            }
        *)
        Definition is_contract_changed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        []
                    ],
                  [
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          []
                      ]
                  ],
                  "ne",
                  []
                |),
                [
                  M.alloc (|
                    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.apply
                            (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "revm_primitives::state::AccountInfo" ]
                                ]
                            ]
                            (Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [])
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm_primitives::state::AccountInfo" ],
                            "as_ref",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::bundle_account::BundleAccount",
                              "info"
                            |)
                          ]
                        |);
                        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 (|
                                              M.read (| a |),
                                              "revm_primitives::state::AccountInfo",
                                              "code_hash"
                                            |)
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |);
                  M.alloc (|
                    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.apply
                            (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            [];
                          Ty.function
                            [
                              Ty.tuple
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "revm_primitives::state::AccountInfo" ]
                                ]
                            ]
                            (Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [])
                        ]
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm_primitives::state::AccountInfo" ],
                            "as_ref",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::bundle_account::BundleAccount",
                              "original_info"
                            |)
                          ]
                        |);
                        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 (|
                                              M.read (| a |),
                                              "revm_primitives::state::AccountInfo",
                                              "code_hash"
                                            |)
                                          |)))
                                    ]
                                  |)))
                              | _ => M.impossible "wrong number of arguments"
                              end))
                      ]
                    |)
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_is_contract_changed :
          M.IsAssociatedFunction Self "is_contract_changed" is_contract_changed.
        
        (*
            pub fn revert(&mut self, revert: AccountRevert) -> bool {
                self.status = revert.previous_status;
        
                match revert.account {
                    AccountInfoRevert::DoNothing => (),
                    AccountInfoRevert::DeleteIt => {
                        self.info = None;
                        if self.original_info.is_none() {
                            self.storage = HashMap::new();
                            return true;
                        } else {
                            // set all storage to zero but preserve original values.
                            self.storage.iter_mut().for_each(|(_, v)| {
                                v.present_value = U256::ZERO;
                            });
                            return false;
                        }
                    }
                    AccountInfoRevert::RevertTo(info) => self.info = Some(info),
                };
                // revert storage
                for (key, slot) in revert.storage {
                    match slot {
                        RevertToSlot::Some(value) => {
                            // Don't overwrite original values if present
                            // if storage is not present set original value as current value.
                            self.storage
                                .entry(key)
                                .or_insert(StorageSlot::new(value))
                                .present_value = value;
                        }
                        RevertToSlot::Destroyed => {
                            // if it was destroyed this means that storage was created and we need to remove it.
                            self.storage.remove(&key);
                        }
                    }
                }
                false
            }
        *)
        Definition revert (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; revert ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let revert := M.alloc (| revert |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ _ :=
                      M.write (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::bundle_account::BundleAccount",
                          "status"
                        |),
                        M.read (|
                          M.SubPointer.get_struct_record_field (|
                            revert,
                            "revm::db::states::reverts::AccountRevert",
                            "previous_status"
                          |)
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.SubPointer.get_struct_record_field (|
                          revert,
                          "revm::db::states::reverts::AccountRevert",
                          "account"
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_struct_tuple (|
                                  γ,
                                  "revm::db::states::reverts::AccountInfoRevert::DoNothing"
                                |) in
                              M.alloc (| Value.Tuple [] |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let _ :=
                                M.is_struct_tuple (|
                                  γ,
                                  "revm::db::states::reverts::AccountInfoRevert::DeleteIt"
                                |) in
                              let~ _ :=
                                M.write (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm::db::states::bundle_account::BundleAccount",
                                    "info"
                                  |),
                                  Value.StructTuple "core::option::Option::None" []
                                |) in
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [ Ty.path "revm_primitives::state::AccountInfo" ],
                                                "is_none",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "revm::db::states::bundle_account::BundleAccount",
                                                  "original_info"
                                                |)
                                              ]
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.write (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "revm::db::states::bundle_account::BundleAccount",
                                                  "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",
                                                    []
                                                  |),
                                                  []
                                                |)
                                              |) in
                                            M.return_ (| Value.Bool true |)
                                          |)
                                        |)
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.alloc (|
                                        M.never_to_any (|
                                          M.read (|
                                            let~ _ :=
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::iterator::Iterator",
                                                    Ty.apply
                                                      (Ty.path
                                                        "std::collections::hash::map::IterMut")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          [];
                                                        Ty.path
                                                          "revm_primitives::state::StorageSlot"
                                                      ],
                                                    [],
                                                    "for_each",
                                                    [
                                                      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 "&mut")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "revm_primitives::state::StorageSlot"
                                                                    ]
                                                                ]
                                                            ]
                                                        ]
                                                        (Ty.tuple [])
                                                    ]
                                                  |),
                                                  [
                                                    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_mut",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "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 v := M.copy (| γ0_1 |) in
                                                                      M.read (|
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.read (| v |),
                                                                              "revm_primitives::state::StorageSlot",
                                                                              "present_value"
                                                                            |),
                                                                            M.read (|
                                                                              M.get_constant (|
                                                                                "ruint::ZERO"
                                                                              |)
                                                                            |)
                                                                          |) in
                                                                        M.alloc (| Value.Tuple [] |)
                                                                      |)))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  ]
                                                |)
                                              |) in
                                            M.return_ (| Value.Bool false |)
                                          |)
                                        |)
                                      |)))
                                ]
                              |)));
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "revm::db::states::reverts::AccountInfoRevert::RevertTo",
                                  0
                                |) in
                              let info := M.copy (| γ0_0 |) in
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "info"
                                |),
                                Value.StructTuple "core::option::Option::Some" [ M.read (| info |) ]
                              |)))
                        ]
                      |) in
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.apply
                                  (Ty.path "std::collections::hash::map::HashMap")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [];
                                    Ty.path "revm::db::states::reverts::RevertToSlot";
                                    Ty.path "std::hash::random::RandomState"
                                  ],
                                [],
                                "into_iter",
                                []
                              |),
                              [
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    revert,
                                    "revm::db::states::reverts::AccountRevert",
                                    "storage"
                                  |)
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let iter := M.copy (| γ |) in
                                M.loop (|
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "std::collections::hash::map::IntoIter")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "ruint::Uint")
                                                    [
                                                      Value.Integer IntegerKind.Usize 256;
                                                      Value.Integer IntegerKind.Usize 4
                                                    ]
                                                    [];
                                                  Ty.path "revm::db::states::reverts::RevertToSlot"
                                                ],
                                              [],
                                              "next",
                                              []
                                            |),
                                            [ iter ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let _ :=
                                                M.is_struct_tuple (|
                                                  γ,
                                                  "core::option::Option::None"
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let γ1_0 :=
                                                M.SubPointer.get_tuple_field (| γ0_0, 0 |) in
                                              let γ1_1 :=
                                                M.SubPointer.get_tuple_field (| γ0_0, 1 |) in
                                              let key := M.copy (| γ1_0 |) in
                                              let slot := M.copy (| γ1_1 |) in
                                              M.match_operator (|
                                                slot,
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "revm::db::states::reverts::RevertToSlot::Some",
                                                          0
                                                        |) in
                                                      let value := M.copy (| γ0_0 |) in
                                                      let~ _ :=
                                                        M.write (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "std::collections::hash::map::Entry")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path "ruint::Uint")
                                                                      [
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          256;
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          4
                                                                      ]
                                                                      [];
                                                                    Ty.path
                                                                      "revm_primitives::state::StorageSlot"
                                                                  ],
                                                                "or_insert",
                                                                []
                                                              |),
                                                              [
                                                                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"
                                                                      ],
                                                                    "entry",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| self |),
                                                                      "revm::db::states::bundle_account::BundleAccount",
                                                                      "storage"
                                                                    |);
                                                                    M.read (| key |)
                                                                  ]
                                                                |);
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.path
                                                                      "revm_primitives::state::StorageSlot",
                                                                    "new",
                                                                    []
                                                                  |),
                                                                  [ M.read (| value |) ]
                                                                |)
                                                              ]
                                                            |),
                                                            "revm_primitives::state::StorageSlot",
                                                            "present_value"
                                                          |),
                                                          M.read (| value |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let _ :=
                                                        M.is_struct_tuple (|
                                                          γ,
                                                          "revm::db::states::reverts::RevertToSlot::Destroyed"
                                                        |) in
                                                      let~ _ :=
                                                        M.alloc (|
                                                          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"
                                                                ],
                                                              "remove",
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "ruint::Uint")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      256;
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      4
                                                                  ]
                                                                  []
                                                              ]
                                                            |),
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| self |),
                                                                "revm::db::states::bundle_account::BundleAccount",
                                                                "storage"
                                                              |);
                                                              key
                                                            ]
                                                          |)
                                                        |) in
                                                      M.alloc (| Value.Tuple [] |)))
                                                ]
                                              |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    M.alloc (| Value.Bool false |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_revert : M.IsAssociatedFunction Self "revert" revert.
        
        (*
            pub fn update_and_create_revert(
                &mut self,
                transition: TransitionAccount,
            ) -> Option<AccountRevert> {
                let updated_info = transition.info;
                let updated_storage = transition.storage;
                let updated_status = transition.status;
        
                // the helper that extends this storage but preserves original value.
                let extend_storage =
                    |this_storage: &mut StorageWithOriginalValues,
                     storage_update: StorageWithOriginalValues| {
                        for (key, value) in storage_update {
                            this_storage.entry(key).or_insert(value).present_value = value.present_value;
                        }
                    };
        
                let previous_storage_from_update =
                    |updated_storage: &StorageWithOriginalValues| -> HashMap<U256, RevertToSlot> {
                        updated_storage
                            .iter()
                            .filter(|s| s.1.is_changed())
                            .map(|(key, value)| {
                                ( *key, RevertToSlot::Some(value.previous_or_original_value))
                            })
                            .collect()
                    };
        
                // Needed for some reverts.
                let info_revert = if self.info != updated_info {
                    AccountInfoRevert::RevertTo(self.info.clone().unwrap_or_default())
                } else {
                    AccountInfoRevert::DoNothing
                };
        
                let account_revert = match updated_status {
                    AccountStatus::Changed => {
                        let previous_storage = previous_storage_from_update(&updated_storage);
                        match self.status {
                            AccountStatus::Changed | AccountStatus::Loaded => {
                                // extend the storage. original values is not used inside bundle.
                                extend_storage(&mut self.storage, updated_storage);
                            }
                            AccountStatus::LoadedEmptyEIP161 => {
                                // Do nothing.
                                // Only change that can happen from LoadedEmpty to Changed is if balance
                                // is send to account. So we are only checking account change here.
                            }
                            _ => unreachable!("Invalid state transfer to Changed from {self:?}"),
                        };
                        let previous_status = self.status;
                        self.status = AccountStatus::Changed;
                        self.info = updated_info;
                        Some(AccountRevert {
                            account: info_revert,
                            storage: previous_storage,
                            previous_status,
                            wipe_storage: false,
                        })
                    }
                    AccountStatus::InMemoryChange => {
                        let previous_storage = previous_storage_from_update(&updated_storage);
                        let in_memory_info_revert = match self.status {
                            AccountStatus::Loaded | AccountStatus::InMemoryChange => {
                                // from loaded (Or LoadedEmpty) to InMemoryChange can happen if there is balance change
                                // or new created account but Loaded didn't have contract.
                                extend_storage(&mut self.storage, updated_storage);
                                info_revert
                            }
                            AccountStatus::LoadedEmptyEIP161 => {
                                self.storage = updated_storage;
                                info_revert
                            }
                            AccountStatus::LoadedNotExisting => {
                                self.storage = updated_storage;
                                AccountInfoRevert::DeleteIt
                            }
                            _ => unreachable!("Invalid change to InMemoryChange from {self:?}"),
                        };
                        let previous_status = self.status;
                        self.status = AccountStatus::InMemoryChange;
                        self.info = updated_info;
                        Some(AccountRevert {
                            account: in_memory_info_revert,
                            storage: previous_storage,
                            previous_status,
                            wipe_storage: false,
                        })
                    }
                    AccountStatus::Loaded
                    | AccountStatus::LoadedNotExisting
                    | AccountStatus::LoadedEmptyEIP161 => {
                        // No changeset, maybe just update data
                        // Do nothing for now.
                        None
                    }
                    AccountStatus::Destroyed => {
                        // clear this storage and move it to the Revert.
                        let this_storage = self.storage.drain().collect();
                        let ret = match self.status {
                            AccountStatus::InMemoryChange | AccountStatus::Changed | AccountStatus::Loaded | AccountStatus::LoadedEmptyEIP161 => {
                                Some(AccountRevert::new_selfdestructed(self.status, info_revert, this_storage))
                            }
                            AccountStatus::LoadedNotExisting => {
                                // Do nothing as we have LoadedNotExisting -> Destroyed (It is noop)
                                None
                            }
                            _ => unreachable!("Invalid transition to Destroyed account from: {self:?} to {updated_info:?} {updated_status:?}"),
                        };
        
                        if ret.is_some() {
                            self.status = AccountStatus::Destroyed;
                            self.info = None;
                        }
        
                        // set present to destroyed.
                        ret
                    }
                    AccountStatus::DestroyedChanged => {
                        // Previous block created account or changed.
                        // (It was destroyed on previous block or one before).
        
                        // check common pre destroy paths.
                        // If common path is there it will drain the storage.
                        if let Some(revert_state) = AccountRevert::new_selfdestructed_from_bundle(
                            info_revert.clone(),
                            self,
                            &updated_storage,
                        ) {
                            // set to destroyed and revert state.
                            self.status = AccountStatus::DestroyedChanged;
                            self.info = updated_info;
                            self.storage = updated_storage;
        
                            Some(revert_state)
                        } else {
                            let ret = match self.status {
                                AccountStatus::Destroyed | AccountStatus::LoadedNotExisting => {
                                    // from destroyed state new account is made
                                    Some(AccountRevert {
                                        account: AccountInfoRevert::DeleteIt,
                                        storage: previous_storage_from_update(&updated_storage),
                                        previous_status: self.status,
                                        wipe_storage: false,
                                    })
                                }
                                AccountStatus::DestroyedChanged => {
                                    // Account was destroyed in this transition. So we should clear present storage
                                    // and insert it inside revert.
        
                                    let previous_storage = if transition.storage_was_destroyed {
                                        let mut storage = core::mem::take(&mut self.storage)
                                            .into_iter()
                                            .map(|t| (t.0, RevertToSlot::Some(t.1.present_value)))
                                            .collect::<HashMap<_, _>>();
                                        for key in updated_storage.keys() {
                                            // as it is not existing inside Destroyed storage this means
                                            // that previous values must be zero
                                            storage.entry( *key).or_insert(RevertToSlot::Destroyed);
                                        }
                                        storage
                                    } else {
                                        previous_storage_from_update(&updated_storage)
                                    };
        
                                    Some(AccountRevert {
                                        account: info_revert,
                                        storage: previous_storage,
                                        previous_status: AccountStatus::DestroyedChanged,
                                        wipe_storage: false,
                                    })
                                }
                                AccountStatus::DestroyedAgain => {
                                    Some(AccountRevert::new_selfdestructed_again(
                                        // destroyed again will set empty account.
                                        AccountStatus::DestroyedAgain,
                                        AccountInfoRevert::DeleteIt,
                                        HashMap::default(),
                                        updated_storage.clone(),
                                    ))
                                }
                                _ => unreachable!("Invalid state transfer to DestroyedNew from {self:?}"),
                            };
                            self.status = AccountStatus::DestroyedChanged;
                            self.info = updated_info;
                            // extends current storage.
                            extend_storage(&mut self.storage, updated_storage);
        
                            ret
                        }
                    }
                    AccountStatus::DestroyedAgain => {
                        // Previous block created account
                        // (It was destroyed on previous block or one before).
        
                        // check common pre destroy paths.
                        // This will drain the storage if it is common transition.
                        let ret = if let Some(revert_state) = AccountRevert::new_selfdestructed_from_bundle(
                            info_revert,
                            self,
                            &HashMap::default(),
                        ) {
                            Some(revert_state)
                        } else {
                            match self.status {
                                AccountStatus::Destroyed
                                | AccountStatus::DestroyedAgain
                                | AccountStatus::LoadedNotExisting => {
                                    // From destroyed to destroyed again. is noop
                                    //
                                    // DestroyedAgain to DestroyedAgain is noop
                                    //
                                    // From LoadedNotExisting to DestroyedAgain
                                    // is noop as account is destroyed again
                                    None
                                }
                                AccountStatus::DestroyedChanged => {
                                    // From destroyed changed to destroyed again.
                                    Some(AccountRevert::new_selfdestructed_again(
                                        // destroyed again will set empty account.
                                        AccountStatus::DestroyedChanged,
                                        AccountInfoRevert::RevertTo(self.info.clone().unwrap_or_default()),
                                        self.storage.drain().collect(),
                                        HashMap::default(),
                                    ))
                                }
                                _ => unreachable!("Invalid state to DestroyedAgain from {self:?}"),
                            }
                        };
                        // set to destroyed and revert state.
                        self.status = AccountStatus::DestroyedAgain;
                        self.info = None;
                        self.storage.clear();
                        ret
                    }
                };
        
                account_revert.and_then(|acc| if acc.is_empty() { None } else { Some(acc) })
            }
        *)
        Definition update_and_create_revert
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; transition ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let transition := M.alloc (| transition |) in
              M.read (|
                let~ updated_info :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      transition,
                      "revm::db::states::transition_account::TransitionAccount",
                      "info"
                    |)
                  |) in
                let~ updated_storage :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      transition,
                      "revm::db::states::transition_account::TransitionAccount",
                      "storage"
                    |)
                  |) in
                let~ updated_status :=
                  M.copy (|
                    M.SubPointer.get_struct_record_field (|
                      transition,
                      "revm::db::states::transition_account::TransitionAccount",
                      "status"
                    |)
                  |) in
                let~ extend_storage :=
                  M.alloc (|
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0; α1 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let this_storage := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α1 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let storage_update := M.copy (| γ |) in
                                              M.read (|
                                                M.use
                                                  (M.match_operator (|
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::iter::traits::collect::IntoIterator",
                                                          Ty.apply
                                                            (Ty.path
                                                              "std::collections::hash::map::HashMap")
                                                            []
                                                            [
                                                              Ty.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"
                                                            ],
                                                          [],
                                                          "into_iter",
                                                          []
                                                        |),
                                                        [ M.read (| storage_update |) ]
                                                      |)
                                                    |),
                                                    [
                                                      fun γ =>
                                                        ltac:(M.monadic
                                                          (let iter := M.copy (| γ |) in
                                                          M.loop (|
                                                            ltac:(M.monadic
                                                              (let~ _ :=
                                                                M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::iter::traits::iterator::Iterator",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "std::collections::hash::map::IntoIter")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "ruint::Uint")
                                                                              [
                                                                                Value.Integer
                                                                                  IntegerKind.Usize
                                                                                  256;
                                                                                Value.Integer
                                                                                  IntegerKind.Usize
                                                                                  4
                                                                              ]
                                                                              [];
                                                                            Ty.path
                                                                              "revm_primitives::state::StorageSlot"
                                                                          ],
                                                                        [],
                                                                        "next",
                                                                        []
                                                                      |),
                                                                      [ iter ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let _ :=
                                                                          M.is_struct_tuple (|
                                                                            γ,
                                                                            "core::option::Option::None"
                                                                          |) in
                                                                        M.alloc (|
                                                                          M.never_to_any (|
                                                                            M.read (|
                                                                              M.break (||)
                                                                            |)
                                                                          |)
                                                                        |)));
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let γ0_0 :=
                                                                          M.SubPointer.get_struct_tuple_field (|
                                                                            γ,
                                                                            "core::option::Option::Some",
                                                                            0
                                                                          |) in
                                                                        let γ1_0 :=
                                                                          M.SubPointer.get_tuple_field (|
                                                                            γ0_0,
                                                                            0
                                                                          |) in
                                                                        let γ1_1 :=
                                                                          M.SubPointer.get_tuple_field (|
                                                                            γ0_0,
                                                                            1
                                                                          |) in
                                                                        let key :=
                                                                          M.copy (| γ1_0 |) in
                                                                        let value :=
                                                                          M.copy (| γ1_1 |) in
                                                                        let~ _ :=
                                                                          M.write (|
                                                                            M.SubPointer.get_struct_record_field (|
                                                                              M.call_closure (|
                                                                                M.get_associated_function (|
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "std::collections::hash::map::Entry")
                                                                                    []
                                                                                    [
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "ruint::Uint")
                                                                                        [
                                                                                          Value.Integer
                                                                                            IntegerKind.Usize
                                                                                            256;
                                                                                          Value.Integer
                                                                                            IntegerKind.Usize
                                                                                            4
                                                                                        ]
                                                                                        [];
                                                                                      Ty.path
                                                                                        "revm_primitives::state::StorageSlot"
                                                                                    ],
                                                                                  "or_insert",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  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"
                                                                                        ],
                                                                                      "entry",
                                                                                      []
                                                                                    |),
                                                                                    [
                                                                                      M.read (|
                                                                                        this_storage
                                                                                      |);
                                                                                      M.read (|
                                                                                        key
                                                                                      |)
                                                                                    ]
                                                                                  |);
                                                                                  M.read (| value |)
                                                                                ]
                                                                              |),
                                                                              "revm_primitives::state::StorageSlot",
                                                                              "present_value"
                                                                            |),
                                                                            M.read (|
                                                                              M.SubPointer.get_struct_record_field (|
                                                                                value,
                                                                                "revm_primitives::state::StorageSlot",
                                                                                "present_value"
                                                                              |)
                                                                            |)
                                                                          |) in
                                                                        M.alloc (|
                                                                          Value.Tuple []
                                                                        |)))
                                                                  ]
                                                                |) in
                                                              M.alloc (| Value.Tuple [] |)))
                                                          |)))
                                                    ]
                                                  |))
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |) in
                let~ previous_storage_from_update :=
                  M.alloc (|
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [ α0 ] =>
                            ltac:(M.monadic
                              (M.match_operator (|
                                M.alloc (| α0 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let updated_storage := M.copy (| γ |) in
                                      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 "core::iter::adapters::filter::Filter")
                                                []
                                                [
                                                  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.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              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.path "bool")
                                                ];
                                              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.path
                                                      "revm::db::states::reverts::RevertToSlot"
                                                  ])
                                            ],
                                          [],
                                          "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.path "revm::db::states::reverts::RevertToSlot";
                                                Ty.path "std::hash::random::RandomState"
                                              ]
                                          ]
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::iter::adapters::filter::Filter")
                                                []
                                                [
                                                  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.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              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.path "bool")
                                                ],
                                              [],
                                              "map",
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply
                                                      (Ty.path "ruint::Uint")
                                                      [
                                                        Value.Integer IntegerKind.Usize 256;
                                                        Value.Integer IntegerKind.Usize 4
                                                      ]
                                                      [];
                                                    Ty.path
                                                      "revm::db::states::reverts::RevertToSlot"
                                                  ];
                                                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.path
                                                        "revm::db::states::reverts::RevertToSlot"
                                                    ])
                                              ]
                                            |),
                                            [
                                              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"
                                                    ],
                                                  [],
                                                  "filter",
                                                  [
                                                    Ty.function
                                                      [
                                                        Ty.tuple
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                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.path "bool")
                                                  ]
                                                |),
                                                [
                                                  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.read (| updated_storage |) ]
                                                  |);
                                                  M.closure
                                                    (fun γ =>
                                                      ltac:(M.monadic
                                                        match γ with
                                                        | [ α0 ] =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              M.alloc (| α0 |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let s := M.copy (| γ |) in
                                                                    M.call_closure (|
                                                                      M.get_associated_function (|
                                                                        Ty.path
                                                                          "revm_primitives::state::StorageSlot",
                                                                        "is_changed",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.read (|
                                                                          M.SubPointer.get_tuple_field (|
                                                                            M.read (| s |),
                                                                            1
                                                                          |)
                                                                        |)
                                                                      ]
                                                                    |)))
                                                              ]
                                                            |)))
                                                        | _ =>
                                                          M.impossible "wrong number of arguments"
                                                        end))
                                                ]
                                              |);
                                              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 key := M.copy (| γ0_0 |) in
                                                                let value := M.copy (| γ0_1 |) in
                                                                Value.Tuple
                                                                  [
                                                                    M.read (| M.read (| key |) |);
                                                                    Value.StructTuple
                                                                      "revm::db::states::reverts::RevertToSlot::Some"
                                                                      [
                                                                        M.read (|
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.read (| value |),
                                                                            "revm_primitives::state::StorageSlot",
                                                                            "previous_or_original_value"
                                                                          |)
                                                                        |)
                                                                      ]
                                                                  ]))
                                                          ]
                                                        |)))
                                                    | _ => M.impossible "wrong number of arguments"
                                                    end))
                                            ]
                                          |)
                                        ]
                                      |)))
                                ]
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |) in
                let~ info_revert :=
                  M.copy (|
                    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.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "revm_primitives::state::AccountInfo" ],
                                      [
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.path "revm_primitives::state::AccountInfo" ]
                                      ],
                                      "ne",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm::db::states::bundle_account::BundleAccount",
                                        "info"
                                      |);
                                      updated_info
                                    ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              Value.StructTuple
                                "revm::db::states::reverts::AccountInfoRevert::RevertTo"
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "revm_primitives::state::AccountInfo" ],
                                      "unwrap_or_default",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::clone::Clone",
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "revm_primitives::state::AccountInfo" ],
                                          [],
                                          "clone",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm::db::states::bundle_account::BundleAccount",
                                            "info"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              Value.StructTuple
                                "revm::db::states::reverts::AccountInfoRevert::DoNothing"
                                []
                            |)))
                      ]
                    |)
                  |) in
                let~ account_revert :=
                  M.copy (|
                    M.match_operator (|
                      updated_status,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::Changed"
                              |) in
                            let~ previous_storage :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::function::Fn",
                                    Ty.function
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                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"
                                                  ]
                                              ]
                                          ]
                                      ]
                                      (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::db::states::reverts::RevertToSlot";
                                          Ty.path "std::hash::random::RandomState"
                                        ]),
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              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"
                                                ]
                                            ]
                                        ]
                                    ],
                                    "call",
                                    []
                                  |),
                                  [ previous_storage_from_update; Value.Tuple [ updated_storage ] ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "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::Loaded"
                                                |) in
                                              Value.Tuple []))
                                        ],
                                        M.closure
                                          (fun γ =>
                                            ltac:(M.monadic
                                              match γ with
                                              | [] =>
                                                ltac:(M.monadic
                                                  (let~ _ :=
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::function::Fn",
                                                          Ty.function
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "&mut")
                                                                    []
                                                                    [
                                                                      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"
                                                                        ]
                                                                    ];
                                                                  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"
                                                                    ]
                                                                ]
                                                            ]
                                                            (Ty.tuple []),
                                                          [
                                                            Ty.tuple
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&mut")
                                                                  []
                                                                  [
                                                                    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"
                                                                      ]
                                                                  ];
                                                                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"
                                                                  ]
                                                              ]
                                                          ],
                                                          "call",
                                                          []
                                                        |),
                                                        [
                                                          extend_storage;
                                                          Value.Tuple
                                                            [
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| self |),
                                                                "revm::db::states::bundle_account::BundleAccount",
                                                                "storage"
                                                              |);
                                                              M.read (| updated_storage |)
                                                            ]
                                                        ]
                                                      |)
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                              | _ => M.impossible "wrong number of arguments"
                                              end))
                                      |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let _ :=
                                        M.is_struct_tuple (|
                                          γ,
                                          "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ =>
                                    ltac:(M.monadic
                                      (M.alloc (|
                                        M.never_to_any (|
                                          M.call_closure (|
                                            M.get_function (| "core::panicking::panic_fmt", [] |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "core::fmt::Arguments",
                                                  "new_v1",
                                                  []
                                                |),
                                                [
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.read (|
                                                          Value.String
                                                            "internal error: entered unreachable code: Invalid state transfer to Changed from "
                                                        |)
                                                      ]
                                                  |);
                                                  M.alloc (|
                                                    Value.Array
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::rt::Argument",
                                                            "new_debug",
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&mut")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "revm::db::states::bundle_account::BundleAccount"
                                                                ]
                                                            ]
                                                          |),
                                                          [ self ]
                                                        |)
                                                      ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)))
                                ]
                              |) in
                            let~ previous_status :=
                              M.copy (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "status"
                                |)
                              |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "status"
                                |),
                                Value.StructTuple
                                  "revm::db::states::account_status::AccountStatus::Changed"
                                  []
                              |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "info"
                                |),
                                M.read (| updated_info |)
                              |) in
                            M.alloc (|
                              Value.StructTuple
                                "core::option::Option::Some"
                                [
                                  Value.StructRecord
                                    "revm::db::states::reverts::AccountRevert"
                                    [
                                      ("account", M.read (| info_revert |));
                                      ("storage", M.read (| previous_storage |));
                                      ("previous_status", M.read (| previous_status |));
                                      ("wipe_storage", Value.Bool false)
                                    ]
                                ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::InMemoryChange"
                              |) in
                            let~ previous_storage :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::function::Fn",
                                    Ty.function
                                      [
                                        Ty.tuple
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                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"
                                                  ]
                                              ]
                                          ]
                                      ]
                                      (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::db::states::reverts::RevertToSlot";
                                          Ty.path "std::hash::random::RandomState"
                                        ]),
                                    [
                                      Ty.tuple
                                        [
                                          Ty.apply
                                            (Ty.path "&")
                                            []
                                            [
                                              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"
                                                ]
                                            ]
                                        ]
                                    ],
                                    "call",
                                    []
                                  |),
                                  [ previous_storage_from_update; Value.Tuple [ updated_storage ] ]
                                |)
                              |) in
                            let~ in_memory_info_revert :=
                              M.copy (|
                                M.match_operator (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm::db::states::bundle_account::BundleAccount",
                                    "status"
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.find_or_pattern (|
                                          γ,
                                          [
                                            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::InMemoryChange"
                                                  |) in
                                                Value.Tuple []))
                                          ],
                                          M.closure
                                            (fun γ =>
                                              ltac:(M.monadic
                                                match γ with
                                                | [] =>
                                                  ltac:(M.monadic
                                                    (let~ _ :=
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::ops::function::Fn",
                                                            Ty.function
                                                              [
                                                                Ty.tuple
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path "&mut")
                                                                      []
                                                                      [
                                                                        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"
                                                                          ]
                                                                      ];
                                                                    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"
                                                                      ]
                                                                  ]
                                                              ]
                                                              (Ty.tuple []),
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "&mut")
                                                                    []
                                                                    [
                                                                      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"
                                                                        ]
                                                                    ];
                                                                  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"
                                                                    ]
                                                                ]
                                                            ],
                                                            "call",
                                                            []
                                                          |),
                                                          [
                                                            extend_storage;
                                                            Value.Tuple
                                                              [
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "revm::db::states::bundle_account::BundleAccount",
                                                                  "storage"
                                                                |);
                                                                M.read (| updated_storage |)
                                                              ]
                                                          ]
                                                        |)
                                                      |) in
                                                    info_revert))
                                                | _ => M.impossible "wrong number of arguments"
                                                end))
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (|
                                            γ,
                                            "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm::db::states::bundle_account::BundleAccount",
                                              "storage"
                                            |),
                                            M.read (| updated_storage |)
                                          |) in
                                        info_revert));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (|
                                            γ,
                                            "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                          |) in
                                        let~ _ :=
                                          M.write (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm::db::states::bundle_account::BundleAccount",
                                              "storage"
                                            |),
                                            M.read (| updated_storage |)
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "revm::db::states::reverts::AccountInfoRevert::DeleteIt"
                                            []
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          M.never_to_any (|
                                            M.call_closure (|
                                              M.get_function (| "core::panicking::panic_fmt", [] |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::fmt::Arguments",
                                                    "new_v1",
                                                    []
                                                  |),
                                                  [
                                                    M.alloc (|
                                                      Value.Array
                                                        [
                                                          M.read (|
                                                            Value.String
                                                              "internal error: entered unreachable code: Invalid change to InMemoryChange from "
                                                          |)
                                                        ]
                                                    |);
                                                    M.alloc (|
                                                      Value.Array
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::rt::Argument",
                                                              "new_debug",
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&mut")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "revm::db::states::bundle_account::BundleAccount"
                                                                  ]
                                                              ]
                                                            |),
                                                            [ self ]
                                                          |)
                                                        ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)))
                                  ]
                                |)
                              |) in
                            let~ previous_status :=
                              M.copy (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "status"
                                |)
                              |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "status"
                                |),
                                Value.StructTuple
                                  "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                  []
                              |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "info"
                                |),
                                M.read (| updated_info |)
                              |) in
                            M.alloc (|
                              Value.StructTuple
                                "core::option::Option::Some"
                                [
                                  Value.StructRecord
                                    "revm::db::states::reverts::AccountRevert"
                                    [
                                      ("account", M.read (| in_memory_info_revert |));
                                      ("storage", M.read (| previous_storage |));
                                      ("previous_status", M.read (| previous_status |));
                                      ("wipe_storage", Value.Bool false)
                                    ]
                                ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.find_or_pattern (|
                              γ,
                              [
                                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::LoadedNotExisting"
                                      |) 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.StructTuple "core::option::Option::None" []
                                        |)))
                                    | _ => M.impossible "wrong number of arguments"
                                    end))
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::Destroyed"
                              |) in
                            let~ this_storage :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply
                                      (Ty.path "std::collections::hash::map::Drain")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [];
                                        Ty.path "revm_primitives::state::StorageSlot"
                                      ],
                                    [],
                                    "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.path "revm_primitives::state::StorageSlot";
                                          Ty.path "std::hash::random::RandomState"
                                        ]
                                    ]
                                  |),
                                  [
                                    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"
                                          ],
                                        "drain",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::db::states::bundle_account::BundleAccount",
                                          "storage"
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |) in
                            let~ ret :=
                              M.copy (|
                                M.match_operator (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm::db::states::bundle_account::BundleAccount",
                                    "status"
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.find_or_pattern (|
                                          γ,
                                          [
                                            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::Changed"
                                                  |) 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.StructTuple
                                                        "core::option::Option::Some"
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path
                                                                "revm::db::states::reverts::AccountRevert",
                                                              "new_selfdestructed",
                                                              []
                                                            |),
                                                            [
                                                              M.read (|
                                                                M.SubPointer.get_struct_record_field (|
                                                                  M.read (| self |),
                                                                  "revm::db::states::bundle_account::BundleAccount",
                                                                  "status"
                                                                |)
                                                              |);
                                                              M.read (| info_revert |);
                                                              M.read (| this_storage |)
                                                            ]
                                                          |)
                                                        ]
                                                    |)))
                                                | _ => M.impossible "wrong number of arguments"
                                                end))
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let _ :=
                                          M.is_struct_tuple (|
                                            γ,
                                            "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                          |) in
                                        M.alloc (|
                                          Value.StructTuple "core::option::Option::None" []
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.alloc (|
                                          M.never_to_any (|
                                            M.call_closure (|
                                              M.get_function (| "core::panicking::panic_fmt", [] |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path "core::fmt::Arguments",
                                                    "new_v1",
                                                    []
                                                  |),
                                                  [
                                                    M.alloc (|
                                                      Value.Array
                                                        [
                                                          M.read (|
                                                            Value.String
                                                              "internal error: entered unreachable code: Invalid transition to Destroyed account from: "
                                                          |);
                                                          M.read (| Value.String " to " |);
                                                          M.read (| Value.String " " |)
                                                        ]
                                                    |);
                                                    M.alloc (|
                                                      Value.Array
                                                        [
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::rt::Argument",
                                                              "new_debug",
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "&mut")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "revm::db::states::bundle_account::BundleAccount"
                                                                  ]
                                                              ]
                                                            |),
                                                            [ self ]
                                                          |);
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::rt::Argument",
                                                              "new_debug",
                                                              [
                                                                Ty.apply
                                                                  (Ty.path "core::option::Option")
                                                                  []
                                                                  [
                                                                    Ty.path
                                                                      "revm_primitives::state::AccountInfo"
                                                                  ]
                                                              ]
                                                            |),
                                                            [ updated_info ]
                                                          |);
                                                          M.call_closure (|
                                                            M.get_associated_function (|
                                                              Ty.path "core::fmt::rt::Argument",
                                                              "new_debug",
                                                              [
                                                                Ty.path
                                                                  "revm::db::states::account_status::AccountStatus"
                                                              ]
                                                            |),
                                                            [ updated_status ]
                                                          |)
                                                        ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)))
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.match_operator (|
                                M.alloc (| Value.Tuple [] |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ :=
                                        M.use
                                          (M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "core::option::Option")
                                                  []
                                                  [
                                                    Ty.path
                                                      "revm::db::states::reverts::AccountRevert"
                                                  ],
                                                "is_some",
                                                []
                                              |),
                                              [ ret ]
                                            |)
                                          |)) in
                                      let _ :=
                                        M.is_constant_or_break_match (|
                                          M.read (| γ |),
                                          Value.Bool true
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm::db::states::bundle_account::BundleAccount",
                                            "status"
                                          |),
                                          Value.StructTuple
                                            "revm::db::states::account_status::AccountStatus::Destroyed"
                                            []
                                        |) in
                                      let~ _ :=
                                        M.write (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm::db::states::bundle_account::BundleAccount",
                                            "info"
                                          |),
                                          Value.StructTuple "core::option::Option::None" []
                                        |) in
                                      M.alloc (| Value.Tuple [] |)));
                                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                ]
                              |) in
                            ret));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                              |) in
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm::db::states::reverts::AccountRevert",
                                            "new_selfdestructed_from_bundle",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_trait_method (|
                                                "core::clone::Clone",
                                                Ty.path
                                                  "revm::db::states::reverts::AccountInfoRevert",
                                                [],
                                                "clone",
                                                []
                                              |),
                                              [ info_revert ]
                                            |);
                                            M.read (| self |);
                                            updated_storage
                                          ]
                                        |)
                                      |) in
                                    let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::option::Option::Some",
                                        0
                                      |) in
                                    let revert_state := M.copy (| γ0_0 |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::db::states::bundle_account::BundleAccount",
                                          "status"
                                        |),
                                        Value.StructTuple
                                          "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                          []
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::db::states::bundle_account::BundleAccount",
                                          "info"
                                        |),
                                        M.read (| updated_info |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::db::states::bundle_account::BundleAccount",
                                          "storage"
                                        |),
                                        M.read (| updated_storage |)
                                      |) in
                                    M.alloc (|
                                      Value.StructTuple
                                        "core::option::Option::Some"
                                        [ M.read (| revert_state |) ]
                                    |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let~ ret :=
                                      M.copy (|
                                        M.match_operator (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm::db::states::bundle_account::BundleAccount",
                                            "status"
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.find_or_pattern (|
                                                  γ,
                                                  [
                                                    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::LoadedNotExisting"
                                                          |) in
                                                        Value.Tuple []))
                                                  ],
                                                  M.closure
                                                    (fun γ =>
                                                      ltac:(M.monadic
                                                        match γ with
                                                        | [] =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              Value.StructTuple
                                                                "core::option::Option::Some"
                                                                [
                                                                  Value.StructRecord
                                                                    "revm::db::states::reverts::AccountRevert"
                                                                    [
                                                                      ("account",
                                                                        Value.StructTuple
                                                                          "revm::db::states::reverts::AccountInfoRevert::DeleteIt"
                                                                          []);
                                                                      ("storage",
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::ops::function::Fn",
                                                                            Ty.function
                                                                              [
                                                                                Ty.tuple
                                                                                  [
                                                                                    Ty.apply
                                                                                      (Ty.path "&")
                                                                                      []
                                                                                      [
                                                                                        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"
                                                                                          ]
                                                                                      ]
                                                                                  ]
                                                                              ]
                                                                              (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::db::states::reverts::RevertToSlot";
                                                                                  Ty.path
                                                                                    "std::hash::random::RandomState"
                                                                                ]),
                                                                            [
                                                                              Ty.tuple
                                                                                [
                                                                                  Ty.apply
                                                                                    (Ty.path "&")
                                                                                    []
                                                                                    [
                                                                                      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"
                                                                                        ]
                                                                                    ]
                                                                                ]
                                                                            ],
                                                                            "call",
                                                                            []
                                                                          |),
                                                                          [
                                                                            previous_storage_from_update;
                                                                            Value.Tuple
                                                                              [ updated_storage ]
                                                                          ]
                                                                        |));
                                                                      ("previous_status",
                                                                        M.read (|
                                                                          M.SubPointer.get_struct_record_field (|
                                                                            M.read (| self |),
                                                                            "revm::db::states::bundle_account::BundleAccount",
                                                                            "status"
                                                                          |)
                                                                        |));
                                                                      ("wipe_storage",
                                                                        Value.Bool false)
                                                                    ]
                                                                ]
                                                            |)))
                                                        | _ =>
                                                          M.impossible "wrong number of arguments"
                                                        end))
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let _ :=
                                                  M.is_struct_tuple (|
                                                    γ,
                                                    "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                                  |) in
                                                let~ previous_storage :=
                                                  M.copy (|
                                                    M.match_operator (|
                                                      M.alloc (| Value.Tuple [] |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ :=
                                                              M.use
                                                                (M.SubPointer.get_struct_record_field (|
                                                                  transition,
                                                                  "revm::db::states::transition_account::TransitionAccount",
                                                                  "storage_was_destroyed"
                                                                |)) in
                                                            let _ :=
                                                              M.is_constant_or_break_match (|
                                                                M.read (| γ |),
                                                                Value.Bool true
                                                              |) in
                                                            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::IntoIter")
                                                                          []
                                                                          [
                                                                            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
                                                                                        "ruint::Uint")
                                                                                      [
                                                                                        Value.Integer
                                                                                          IntegerKind.Usize
                                                                                          256;
                                                                                        Value.Integer
                                                                                          IntegerKind.Usize
                                                                                          4
                                                                                      ]
                                                                                      [];
                                                                                    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.path
                                                                                "revm::db::states::reverts::RevertToSlot"
                                                                            ])
                                                                      ],
                                                                    [],
                                                                    "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.path
                                                                            "revm::db::states::reverts::RevertToSlot";
                                                                          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::IntoIter")
                                                                          []
                                                                          [
                                                                            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.path
                                                                                "revm::db::states::reverts::RevertToSlot"
                                                                            ];
                                                                          Ty.function
                                                                            [
                                                                              Ty.tuple
                                                                                [
                                                                                  Ty.tuple
                                                                                    [
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "ruint::Uint")
                                                                                        [
                                                                                          Value.Integer
                                                                                            IntegerKind.Usize
                                                                                            256;
                                                                                          Value.Integer
                                                                                            IntegerKind.Usize
                                                                                            4
                                                                                        ]
                                                                                        [];
                                                                                      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.path
                                                                                  "revm::db::states::reverts::RevertToSlot"
                                                                              ])
                                                                        ]
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_trait_method (|
                                                                            "core::iter::traits::collect::IntoIterator",
                                                                            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"
                                                                              ],
                                                                            [],
                                                                            "into_iter",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_function (|
                                                                                "core::mem::take",
                                                                                [
                                                                                  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"
                                                                                    ]
                                                                                ]
                                                                              |),
                                                                              [
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (| self |),
                                                                                  "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 t :=
                                                                                            M.copy (|
                                                                                              γ
                                                                                            |) in
                                                                                          Value.Tuple
                                                                                            [
                                                                                              M.read (|
                                                                                                M.SubPointer.get_tuple_field (|
                                                                                                  t,
                                                                                                  0
                                                                                                |)
                                                                                              |);
                                                                                              Value.StructTuple
                                                                                                "revm::db::states::reverts::RevertToSlot::Some"
                                                                                                [
                                                                                                  M.read (|
                                                                                                    M.SubPointer.get_struct_record_field (|
                                                                                                      M.SubPointer.get_tuple_field (|
                                                                                                        t,
                                                                                                        1
                                                                                                      |),
                                                                                                      "revm_primitives::state::StorageSlot",
                                                                                                      "present_value"
                                                                                                    |)
                                                                                                  |)
                                                                                                ]
                                                                                            ]))
                                                                                    ]
                                                                                  |)))
                                                                              | _ =>
                                                                                M.impossible
                                                                                  "wrong number of arguments"
                                                                              end))
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              |) in
                                                            let~ _ :=
                                                              M.use
                                                                (M.match_operator (|
                                                                  M.alloc (|
                                                                    M.call_closure (|
                                                                      M.get_trait_method (|
                                                                        "core::iter::traits::collect::IntoIterator",
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "std::collections::hash::map::Keys")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "ruint::Uint")
                                                                              [
                                                                                Value.Integer
                                                                                  IntegerKind.Usize
                                                                                  256;
                                                                                Value.Integer
                                                                                  IntegerKind.Usize
                                                                                  4
                                                                              ]
                                                                              [];
                                                                            Ty.path
                                                                              "revm_primitives::state::StorageSlot"
                                                                          ],
                                                                        [],
                                                                        "into_iter",
                                                                        []
                                                                      |),
                                                                      [
                                                                        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"
                                                                              ],
                                                                            "keys",
                                                                            []
                                                                          |),
                                                                          [ updated_storage ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  |),
                                                                  [
                                                                    fun γ =>
                                                                      ltac:(M.monadic
                                                                        (let iter :=
                                                                          M.copy (| γ |) in
                                                                        M.loop (|
                                                                          ltac:(M.monadic
                                                                            (let~ _ :=
                                                                              M.match_operator (|
                                                                                M.alloc (|
                                                                                  M.call_closure (|
                                                                                    M.get_trait_method (|
                                                                                      "core::iter::traits::iterator::Iterator",
                                                                                      Ty.apply
                                                                                        (Ty.path
                                                                                          "std::collections::hash::map::Keys")
                                                                                        []
                                                                                        [
                                                                                          Ty.apply
                                                                                            (Ty.path
                                                                                              "ruint::Uint")
                                                                                            [
                                                                                              Value.Integer
                                                                                                IntegerKind.Usize
                                                                                                256;
                                                                                              Value.Integer
                                                                                                IntegerKind.Usize
                                                                                                4
                                                                                            ]
                                                                                            [];
                                                                                          Ty.path
                                                                                            "revm_primitives::state::StorageSlot"
                                                                                        ],
                                                                                      [],
                                                                                      "next",
                                                                                      []
                                                                                    |),
                                                                                    [ iter ]
                                                                                  |)
                                                                                |),
                                                                                [
                                                                                  fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      (let _ :=
                                                                                        M.is_struct_tuple (|
                                                                                          γ,
                                                                                          "core::option::Option::None"
                                                                                        |) in
                                                                                      M.alloc (|
                                                                                        M.never_to_any (|
                                                                                          M.read (|
                                                                                            M.break (||)
                                                                                          |)
                                                                                        |)
                                                                                      |)));
                                                                                  fun γ =>
                                                                                    ltac:(M.monadic
                                                                                      (let γ0_0 :=
                                                                                        M.SubPointer.get_struct_tuple_field (|
                                                                                          γ,
                                                                                          "core::option::Option::Some",
                                                                                          0
                                                                                        |) in
                                                                                      let key :=
                                                                                        M.copy (|
                                                                                          γ0_0
                                                                                        |) in
                                                                                      let~ _ :=
                                                                                        M.alloc (|
                                                                                          M.call_closure (|
                                                                                            M.get_associated_function (|
                                                                                              Ty.apply
                                                                                                (Ty.path
                                                                                                  "std::collections::hash::map::Entry")
                                                                                                []
                                                                                                [
                                                                                                  Ty.apply
                                                                                                    (Ty.path
                                                                                                      "ruint::Uint")
                                                                                                    [
                                                                                                      Value.Integer
                                                                                                        IntegerKind.Usize
                                                                                                        256;
                                                                                                      Value.Integer
                                                                                                        IntegerKind.Usize
                                                                                                        4
                                                                                                    ]
                                                                                                    [];
                                                                                                  Ty.path
                                                                                                    "revm::db::states::reverts::RevertToSlot"
                                                                                                ],
                                                                                              "or_insert",
                                                                                              []
                                                                                            |),
                                                                                            [
                                                                                              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::db::states::reverts::RevertToSlot";
                                                                                                      Ty.path
                                                                                                        "std::hash::random::RandomState"
                                                                                                    ],
                                                                                                  "entry",
                                                                                                  []
                                                                                                |),
                                                                                                [
                                                                                                  storage;
                                                                                                  M.read (|
                                                                                                    M.read (|
                                                                                                      key
                                                                                                    |)
                                                                                                  |)
                                                                                                ]
                                                                                              |);
                                                                                              Value.StructTuple
                                                                                                "revm::db::states::reverts::RevertToSlot::Destroyed"
                                                                                                []
                                                                                            ]
                                                                                          |)
                                                                                        |) in
                                                                                      M.alloc (|
                                                                                        Value.Tuple
                                                                                          []
                                                                                      |)))
                                                                                ]
                                                                              |) in
                                                                            M.alloc (|
                                                                              Value.Tuple []
                                                                            |)))
                                                                        |)))
                                                                  ]
                                                                |)) in
                                                            storage));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::function::Fn",
                                                                  Ty.function
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "&")
                                                                            []
                                                                            [
                                                                              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"
                                                                                ]
                                                                            ]
                                                                        ]
                                                                    ]
                                                                    (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::db::states::reverts::RevertToSlot";
                                                                        Ty.path
                                                                          "std::hash::random::RandomState"
                                                                      ]),
                                                                  [
                                                                    Ty.tuple
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [
                                                                            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"
                                                                              ]
                                                                          ]
                                                                      ]
                                                                  ],
                                                                  "call",
                                                                  []
                                                                |),
                                                                [
                                                                  previous_storage_from_update;
                                                                  Value.Tuple [ updated_storage ]
                                                                ]
                                                              |)
                                                            |)))
                                                      ]
                                                    |)
                                                  |) in
                                                M.alloc (|
                                                  Value.StructTuple
                                                    "core::option::Option::Some"
                                                    [
                                                      Value.StructRecord
                                                        "revm::db::states::reverts::AccountRevert"
                                                        [
                                                          ("account", M.read (| info_revert |));
                                                          ("storage",
                                                            M.read (| previous_storage |));
                                                          ("previous_status",
                                                            Value.StructTuple
                                                              "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                                              []);
                                                          ("wipe_storage", Value.Bool false)
                                                        ]
                                                    ]
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let _ :=
                                                  M.is_struct_tuple (|
                                                    γ,
                                                    "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                                  |) in
                                                M.alloc (|
                                                  Value.StructTuple
                                                    "core::option::Option::Some"
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "revm::db::states::reverts::AccountRevert",
                                                          "new_selfdestructed_again",
                                                          []
                                                        |),
                                                        [
                                                          Value.StructTuple
                                                            "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                                            [];
                                                          Value.StructTuple
                                                            "revm::db::states::reverts::AccountInfoRevert::DeleteIt"
                                                            [];
                                                          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",
                                                              []
                                                            |),
                                                            []
                                                          |);
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::clone::Clone",
                                                              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"
                                                                ],
                                                              [],
                                                              "clone",
                                                              []
                                                            |),
                                                            [ updated_storage ]
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.alloc (|
                                                  M.never_to_any (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::panicking::panic_fmt",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Arguments",
                                                            "new_v1",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.read (|
                                                                    Value.String
                                                                      "internal error: entered unreachable code: Invalid state transfer to DestroyedNew from "
                                                                  |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_debug",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&mut")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "revm::db::states::bundle_account::BundleAccount"
                                                                          ]
                                                                      ]
                                                                    |),
                                                                    [ self ]
                                                                  |)
                                                                ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |)
                                                |)))
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::db::states::bundle_account::BundleAccount",
                                          "status"
                                        |),
                                        Value.StructTuple
                                          "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                          []
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm::db::states::bundle_account::BundleAccount",
                                          "info"
                                        |),
                                        M.read (| updated_info |)
                                      |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::function::Fn",
                                            Ty.function
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply
                                                      (Ty.path "&mut")
                                                      []
                                                      [
                                                        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"
                                                          ]
                                                      ];
                                                    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"
                                                      ]
                                                  ]
                                              ]
                                              (Ty.tuple []),
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.apply
                                                    (Ty.path "&mut")
                                                    []
                                                    [
                                                      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"
                                                        ]
                                                    ];
                                                  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"
                                                    ]
                                                ]
                                            ],
                                            "call",
                                            []
                                          |),
                                          [
                                            extend_storage;
                                            Value.Tuple
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "revm::db::states::bundle_account::BundleAccount",
                                                  "storage"
                                                |);
                                                M.read (| updated_storage |)
                                              ]
                                          ]
                                        |)
                                      |) in
                                    ret))
                              ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                              |) in
                            let~ ret :=
                              M.copy (|
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "revm::db::states::reverts::AccountRevert",
                                                "new_selfdestructed_from_bundle",
                                                []
                                              |),
                                              [
                                                M.read (| info_revert |);
                                                M.read (| self |);
                                                M.alloc (|
                                                  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",
                                                      []
                                                    |),
                                                    []
                                                  |)
                                                |)
                                              ]
                                            |)
                                          |) in
                                        let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::option::Option::Some",
                                            0
                                          |) in
                                        let revert_state := M.copy (| γ0_0 |) in
                                        M.alloc (|
                                          Value.StructTuple
                                            "core::option::Option::Some"
                                            [ M.read (| revert_state |) ]
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (M.match_operator (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm::db::states::bundle_account::BundleAccount",
                                            "status"
                                          |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.find_or_pattern (|
                                                  γ,
                                                  [
                                                    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 []));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let _ :=
                                                          M.is_struct_tuple (|
                                                            γ,
                                                            "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                                          |) in
                                                        Value.Tuple []))
                                                  ],
                                                  M.closure
                                                    (fun γ =>
                                                      ltac:(M.monadic
                                                        match γ with
                                                        | [] =>
                                                          ltac:(M.monadic
                                                            (M.alloc (|
                                                              Value.StructTuple
                                                                "core::option::Option::None"
                                                                []
                                                            |)))
                                                        | _ =>
                                                          M.impossible "wrong number of arguments"
                                                        end))
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let _ :=
                                                  M.is_struct_tuple (|
                                                    γ,
                                                    "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                                  |) in
                                                M.alloc (|
                                                  Value.StructTuple
                                                    "core::option::Option::Some"
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path
                                                            "revm::db::states::reverts::AccountRevert",
                                                          "new_selfdestructed_again",
                                                          []
                                                        |),
                                                        [
                                                          Value.StructTuple
                                                            "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                                            [];
                                                          Value.StructTuple
                                                            "revm::db::states::reverts::AccountInfoRevert::RevertTo"
                                                            [
                                                              M.call_closure (|
                                                                M.get_associated_function (|
                                                                  Ty.apply
                                                                    (Ty.path "core::option::Option")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "revm_primitives::state::AccountInfo"
                                                                    ],
                                                                  "unwrap_or_default",
                                                                  []
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_trait_method (|
                                                                      "core::clone::Clone",
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "core::option::Option")
                                                                        []
                                                                        [
                                                                          Ty.path
                                                                            "revm_primitives::state::AccountInfo"
                                                                        ],
                                                                      [],
                                                                      "clone",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        M.read (| self |),
                                                                        "revm::db::states::bundle_account::BundleAccount",
                                                                        "info"
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]
                                                              |)
                                                            ];
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::iter::traits::iterator::Iterator",
                                                              Ty.apply
                                                                (Ty.path
                                                                  "std::collections::hash::map::Drain")
                                                                []
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "ruint::Uint")
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        256;
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        4
                                                                    ]
                                                                    [];
                                                                  Ty.path
                                                                    "revm_primitives::state::StorageSlot"
                                                                ],
                                                              [],
                                                              "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.path
                                                                      "revm_primitives::state::StorageSlot";
                                                                    Ty.path
                                                                      "std::hash::random::RandomState"
                                                                  ]
                                                              ]
                                                            |),
                                                            [
                                                              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"
                                                                    ],
                                                                  "drain",
                                                                  []
                                                                |),
                                                                [
                                                                  M.SubPointer.get_struct_record_field (|
                                                                    M.read (| self |),
                                                                    "revm::db::states::bundle_account::BundleAccount",
                                                                    "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",
                                                              []
                                                            |),
                                                            []
                                                          |)
                                                        ]
                                                      |)
                                                    ]
                                                |)));
                                            fun γ =>
                                              ltac:(M.monadic
                                                (M.alloc (|
                                                  M.never_to_any (|
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::panicking::panic_fmt",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "core::fmt::Arguments",
                                                            "new_v1",
                                                            []
                                                          |),
                                                          [
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.read (|
                                                                    Value.String
                                                                      "internal error: entered unreachable code: Invalid state to DestroyedAgain from "
                                                                  |)
                                                                ]
                                                            |);
                                                            M.alloc (|
                                                              Value.Array
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::rt::Argument",
                                                                      "new_debug",
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path "&mut")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "revm::db::states::bundle_account::BundleAccount"
                                                                          ]
                                                                      ]
                                                                    |),
                                                                    [ self ]
                                                                  |)
                                                                ]
                                                            |)
                                                          ]
                                                        |)
                                                      ]
                                                    |)
                                                  |)
                                                |)))
                                          ]
                                        |)))
                                  ]
                                |)
                              |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "status"
                                |),
                                Value.StructTuple
                                  "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                  []
                              |) in
                            let~ _ :=
                              M.write (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::bundle_account::BundleAccount",
                                  "info"
                                |),
                                Value.StructTuple "core::option::Option::None" []
                              |) in
                            let~ _ :=
                              M.alloc (|
                                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"
                                      ],
                                    "clear",
                                    []
                                  |),
                                  [
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "revm::db::states::bundle_account::BundleAccount",
                                      "storage"
                                    |)
                                  ]
                                |)
                              |) in
                            ret))
                      ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [ Ty.path "revm::db::states::reverts::AccountRevert" ],
                      "and_then",
                      [
                        Ty.path "revm::db::states::reverts::AccountRevert";
                        Ty.function
                          [ Ty.tuple [ Ty.path "revm::db::states::reverts::AccountRevert" ] ]
                          (Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "revm::db::states::reverts::AccountRevert" ])
                      ]
                    |),
                    [
                      M.read (| account_revert |);
                      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.match_operator (|
                                            M.alloc (| Value.Tuple [] |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let γ :=
                                                    M.use
                                                      (M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path
                                                              "revm::db::states::reverts::AccountRevert",
                                                            "is_empty",
                                                            []
                                                          |),
                                                          [ acc ]
                                                        |)
                                                      |)) 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"
                                                      [ M.read (| acc |) ]
                                                  |)))
                                            ]
                                          |)
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_update_and_create_revert :
          M.IsAssociatedFunction Self "update_and_create_revert" update_and_create_revert.
      End Impl_revm_db_states_bundle_account_BundleAccount.
    End bundle_account.
  End states.
End db.
