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

Module db.
  Module states.
    Module reverts.
      (* StructTuple
        {
          name := "Reverts";
          const_params := [];
          ty_params := [];
          fields :=
            [
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.tuple
                        [
                          Ty.path "alloy_primitives::bits::address::Address";
                          Ty.path "revm::db::states::reverts::AccountRevert"
                        ];
                      Ty.path "alloc::alloc::Global"
                    ];
                  Ty.path "alloc::alloc::Global"
                ]
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        (* 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.StructTuple
                "revm::db::states::reverts::Reverts"
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.tuple
                                [
                                  Ty.path "alloy_primitives::bits::address::Address";
                                  Ty.path "revm::db::states::reverts::AccountRevert"
                                ];
                              Ty.path "alloc::alloc::Global"
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_tuple_field (|
                        M.read (| self |),
                        "revm::db::states::reverts::Reverts",
                        0
                      |)
                    ]
                  |)
                ]))
          | _, _, _ => 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_reverts_Reverts.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        (* 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_tuple_field1_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "Reverts" |);
                  M.alloc (|
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "revm::db::states::reverts::Reverts",
                      0
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_reverts_Reverts.
      
      Module Impl_core_default_Default_for_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        (* Default *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructTuple
                "revm::db::states::reverts::Reverts"
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.tuple
                                [
                                  Ty.path "alloy_primitives::bits::address::Address";
                                  Ty.path "revm::db::states::reverts::AccountRevert"
                                ];
                              Ty.path "alloc::alloc::Global"
                            ];
                          Ty.path "alloc::alloc::Global"
                        ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |)
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_revm_db_states_reverts_Reverts.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_reverts_Reverts.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        (* 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
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [
                          Ty.tuple
                            [
                              Ty.path "alloy_primitives::bits::address::Address";
                              Ty.path "revm::db::states::reverts::AccountRevert"
                            ];
                          Ty.path "alloc::alloc::Global"
                        ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.tuple
                              [
                                Ty.path "alloy_primitives::bits::address::Address";
                                Ty.path "revm::db::states::reverts::AccountRevert"
                              ];
                            Ty.path "alloc::alloc::Global"
                          ];
                        Ty.path "alloc::alloc::Global"
                      ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "revm::db::states::reverts::Reverts",
                    0
                  |);
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| other |),
                    "revm::db::states::reverts::Reverts",
                    0
                  |)
                ]
              |)))
          | _, _, _ => 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_reverts_Reverts.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        (* 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.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_reverts_Reverts.
      
      Module Impl_core_ops_deref_Deref_for_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        (*     type Target = Vec<Vec<(Address, AccountRevert)>>; *)
        Definition _Target : Ty.t :=
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [
              Ty.apply
                (Ty.path "alloc::vec::Vec")
                []
                [
                  Ty.tuple
                    [
                      Ty.path "alloy_primitives::bits::address::Address";
                      Ty.path "revm::db::states::reverts::AccountRevert"
                    ];
                  Ty.path "alloc::alloc::Global"
                ];
              Ty.path "alloc::alloc::Global"
            ].
        
        (*
            fn deref(&self) -> &Self::Target {
                &self.0
            }
        *)
        Definition deref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "revm::db::states::reverts::Reverts",
                0
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::ops::deref::Deref"
            Self
            (* Trait polymorphic types *) []
            (* Instance *)
            [ ("Target", InstanceField.Ty _Target); ("deref", InstanceField.Method deref) ].
      End Impl_core_ops_deref_Deref_for_revm_db_states_reverts_Reverts.
      
      Module Impl_core_ops_deref_DerefMut_for_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        (*
            fn deref_mut(&mut self) -> &mut Self::Target {
                &mut self.0
            }
        *)
        Definition deref_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "revm::db::states::reverts::Reverts",
                0
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::ops::deref::DerefMut"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("deref_mut", InstanceField.Method deref_mut) ].
      End Impl_core_ops_deref_DerefMut_for_revm_db_states_reverts_Reverts.
      
      Module Impl_revm_db_states_reverts_Reverts.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::Reverts".
        
        (*
            pub fn new(reverts: Vec<Vec<(Address, AccountRevert)>>) -> Self {
                Self(reverts)
            }
        *)
        Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ reverts ] =>
            ltac:(M.monadic
              (let reverts := M.alloc (| reverts |) in
              Value.StructTuple "revm::db::states::reverts::Reverts" [ M.read (| reverts |) ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
        
        (*
            pub fn sort(&mut self) {
                for revert in &mut self.0 {
                    revert.sort_by_key(|(address, _)| *address);
                }
            }
        *)
        Definition sort (ε : 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.use
                  (M.match_operator (|
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          Ty.apply
                            (Ty.path "&mut")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloc::vec::Vec")
                                    []
                                    [
                                      Ty.tuple
                                        [
                                          Ty.path "alloy_primitives::bits::address::Address";
                                          Ty.path "revm::db::states::reverts::AccountRevert"
                                        ];
                                      Ty.path "alloc::alloc::Global"
                                    ];
                                  Ty.path "alloc::alloc::Global"
                                ]
                            ],
                          [],
                          "into_iter",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_tuple_field (|
                            M.read (| self |),
                            "revm::db::states::reverts::Reverts",
                            0
                          |)
                        ]
                      |)
                    |),
                    [
                      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 "core::slice::iter::IterMut")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "alloc::vec::Vec")
                                              []
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.path
                                                      "alloy_primitives::bits::address::Address";
                                                    Ty.path
                                                      "revm::db::states::reverts::AccountRevert"
                                                  ];
                                                Ty.path "alloc::alloc::Global"
                                              ]
                                          ],
                                        [],
                                        "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 revert := M.copy (| γ0_0 |) in
                                        let~ _ :=
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "slice")
                                                  []
                                                  [
                                                    Ty.tuple
                                                      [
                                                        Ty.path
                                                          "alloy_primitives::bits::address::Address";
                                                        Ty.path
                                                          "revm::db::states::reverts::AccountRevert"
                                                      ]
                                                  ],
                                                "sort_by_key",
                                                [
                                                  Ty.path
                                                    "alloy_primitives::bits::address::Address";
                                                  Ty.function
                                                    [
                                                      Ty.tuple
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.path
                                                                    "alloy_primitives::bits::address::Address";
                                                                  Ty.path
                                                                    "revm::db::states::reverts::AccountRevert"
                                                                ]
                                                            ]
                                                        ]
                                                    ]
                                                    (Ty.path
                                                      "alloy_primitives::bits::address::Address")
                                                ]
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::deref::DerefMut",
                                                    Ty.apply
                                                      (Ty.path "alloc::vec::Vec")
                                                      []
                                                      [
                                                        Ty.tuple
                                                          [
                                                            Ty.path
                                                              "alloy_primitives::bits::address::Address";
                                                            Ty.path
                                                              "revm::db::states::reverts::AccountRevert"
                                                          ];
                                                        Ty.path "alloc::alloc::Global"
                                                      ],
                                                    [],
                                                    "deref_mut",
                                                    []
                                                  |),
                                                  [ M.read (| revert |) ]
                                                |);
                                                M.closure
                                                  (fun γ =>
                                                    ltac:(M.monadic
                                                      match γ with
                                                      | [ α0 ] =>
                                                        ltac:(M.monadic
                                                          (M.match_operator (|
                                                            M.alloc (| α0 |),
                                                            [
                                                              fun γ =>
                                                                ltac:(M.monadic
                                                                  (let γ := M.read (| γ |) in
                                                                  let γ1_0 :=
                                                                    M.SubPointer.get_tuple_field (|
                                                                      γ,
                                                                      0
                                                                    |) in
                                                                  let γ1_1 :=
                                                                    M.SubPointer.get_tuple_field (|
                                                                      γ,
                                                                      1
                                                                    |) in
                                                                  let address :=
                                                                    M.alloc (| γ1_0 |) in
                                                                  M.read (|
                                                                    M.read (| address |)
                                                                  |)))
                                                            ]
                                                          |)))
                                                      | _ =>
                                                        M.impossible "wrong number of arguments"
                                                      end))
                                              ]
                                            |)
                                          |) in
                                        M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.alloc (| Value.Tuple [] |)))
                          |)))
                    ]
                  |))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_sort : M.IsAssociatedFunction Self "sort" sort.
        
        (*
            pub fn extend(&mut self, other: Reverts) {
                self.0.extend(other.0);
            }
        *)
        Definition extend (ε : 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
              M.read (|
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::iter::traits::collect::Extend",
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.path "alloy_primitives::bits::address::Address";
                                    Ty.path "revm::db::states::reverts::AccountRevert"
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ];
                            Ty.path "alloc::alloc::Global"
                          ],
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.tuple
                                [
                                  Ty.path "alloy_primitives::bits::address::Address";
                                  Ty.path "revm::db::states::reverts::AccountRevert"
                                ];
                              Ty.path "alloc::alloc::Global"
                            ]
                        ],
                        "extend",
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.tuple
                                    [
                                      Ty.path "alloy_primitives::bits::address::Address";
                                      Ty.path "revm::db::states::reverts::AccountRevert"
                                    ];
                                  Ty.path "alloc::alloc::Global"
                                ];
                              Ty.path "alloc::alloc::Global"
                            ]
                        ]
                      |),
                      [
                        M.SubPointer.get_struct_tuple_field (|
                          M.read (| self |),
                          "revm::db::states::reverts::Reverts",
                          0
                        |);
                        M.read (|
                          M.SubPointer.get_struct_tuple_field (|
                            other,
                            "revm::db::states::reverts::Reverts",
                            0
                          |)
                        |)
                      ]
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_extend : M.IsAssociatedFunction Self "extend" extend.
        
        (*
            pub fn into_plain_state_reverts(mut self) -> PlainStateReverts {
                let mut state_reverts = PlainStateReverts::with_capacity(self.0.len());
                for reverts in self.0.drain(..) {
                    // pessimistically pre-allocate assuming _all_ accounts changed.
                    let mut accounts = Vec::with_capacity(reverts.len());
                    let mut storage = Vec::with_capacity(reverts.len());
                    for (address, revert_account) in reverts.into_iter() {
                        match revert_account.account {
                            AccountInfoRevert::RevertTo(acc) => accounts.push((address, Some(acc))),
                            AccountInfoRevert::DeleteIt => accounts.push((address, None)),
                            AccountInfoRevert::DoNothing => (),
                        }
                        if revert_account.wipe_storage || !revert_account.storage.is_empty() {
                            storage.push(PlainStorageRevert {
                                address,
                                wiped: revert_account.wipe_storage,
                                storage_revert: revert_account.storage.into_iter().collect::<Vec<_>>(),
                            });
                        }
                    }
                    state_reverts.accounts.push(accounts);
                    state_reverts.storage.push(storage);
                }
                state_reverts
            }
        *)
        Definition into_plain_state_reverts
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ state_reverts :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::db::states::changes::PlainStateReverts",
                        "with_capacity",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.tuple
                                      [
                                        Ty.path "alloy_primitives::bits::address::Address";
                                        Ty.path "revm::db::states::reverts::AccountRevert"
                                      ];
                                    Ty.path "alloc::alloc::Global"
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            "len",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_tuple_field (|
                              self,
                              "revm::db::states::reverts::Reverts",
                              0
                            |)
                          ]
                        |)
                      ]
                    |)
                  |) 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 "alloc::vec::drain::Drain")
                              []
                              [
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.tuple
                                      [
                                        Ty.path "alloy_primitives::bits::address::Address";
                                        Ty.path "revm::db::states::reverts::AccountRevert"
                                      ];
                                    Ty.path "alloc::alloc::Global"
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.tuple
                                          [
                                            Ty.path "alloy_primitives::bits::address::Address";
                                            Ty.path "revm::db::states::reverts::AccountRevert"
                                          ];
                                        Ty.path "alloc::alloc::Global"
                                      ];
                                    Ty.path "alloc::alloc::Global"
                                  ],
                                "drain",
                                [ Ty.path "core::ops::range::RangeFull" ]
                              |),
                              [
                                M.SubPointer.get_struct_tuple_field (|
                                  self,
                                  "revm::db::states::reverts::Reverts",
                                  0
                                |);
                                Value.StructTuple "core::ops::range::RangeFull" []
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        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 "alloc::vec::drain::Drain")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.tuple
                                                    [
                                                      Ty.path
                                                        "alloy_primitives::bits::address::Address";
                                                      Ty.path
                                                        "revm::db::states::reverts::AccountRevert"
                                                    ];
                                                  Ty.path "alloc::alloc::Global"
                                                ];
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          [],
                                          "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 reverts := M.copy (| γ0_0 |) in
                                          let~ accounts :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.tuple
                                                        [
                                                          Ty.path
                                                            "alloy_primitives::bits::address::Address";
                                                          Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            []
                                                            [
                                                              Ty.path
                                                                "revm_primitives::state::AccountInfo"
                                                            ]
                                                        ];
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "with_capacity",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.path
                                                                "alloy_primitives::bits::address::Address";
                                                              Ty.path
                                                                "revm::db::states::reverts::AccountRevert"
                                                            ];
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      "len",
                                                      []
                                                    |),
                                                    [ reverts ]
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          let~ storage :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.path
                                                        "revm::db::states::changes::PlainStorageRevert";
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "with_capacity",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.path
                                                                "alloy_primitives::bits::address::Address";
                                                              Ty.path
                                                                "revm::db::states::reverts::AccountRevert"
                                                            ];
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      "len",
                                                      []
                                                    |),
                                                    [ reverts ]
                                                  |)
                                                ]
                                              |)
                                            |) 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 "alloc::vec::into_iter::IntoIter")
                                                        []
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.path
                                                                "alloy_primitives::bits::address::Address";
                                                              Ty.path
                                                                "revm::db::states::reverts::AccountRevert"
                                                            ];
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      [],
                                                      "into_iter",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::iter::traits::collect::IntoIterator",
                                                          Ty.apply
                                                            (Ty.path "alloc::vec::Vec")
                                                            []
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.path
                                                                    "alloy_primitives::bits::address::Address";
                                                                  Ty.path
                                                                    "revm::db::states::reverts::AccountRevert"
                                                                ];
                                                              Ty.path "alloc::alloc::Global"
                                                            ],
                                                          [],
                                                          "into_iter",
                                                          []
                                                        |),
                                                        [ M.read (| reverts |) ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  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
                                                                        "alloc::vec::into_iter::IntoIter")
                                                                      []
                                                                      [
                                                                        Ty.tuple
                                                                          [
                                                                            Ty.path
                                                                              "alloy_primitives::bits::address::Address";
                                                                            Ty.path
                                                                              "revm::db::states::reverts::AccountRevert"
                                                                          ];
                                                                        Ty.path
                                                                          "alloc::alloc::Global"
                                                                      ],
                                                                    [],
                                                                    "next",
                                                                    []
                                                                  |),
                                                                  [ iter ]
                                                                |)
                                                              |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let _ :=
                                                                      M.is_struct_tuple (|
                                                                        γ,
                                                                        "core::option::Option::None"
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.never_to_any (|
                                                                        M.read (| M.break (||) |)
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ0_0 :=
                                                                      M.SubPointer.get_struct_tuple_field (|
                                                                        γ,
                                                                        "core::option::Option::Some",
                                                                        0
                                                                      |) in
                                                                    let γ1_0 :=
                                                                      M.SubPointer.get_tuple_field (|
                                                                        γ0_0,
                                                                        0
                                                                      |) in
                                                                    let γ1_1 :=
                                                                      M.SubPointer.get_tuple_field (|
                                                                        γ0_0,
                                                                        1
                                                                      |) in
                                                                    let address :=
                                                                      M.copy (| γ1_0 |) in
                                                                    let revert_account :=
                                                                      M.copy (| γ1_1 |) in
                                                                    let~ _ :=
                                                                      M.match_operator (|
                                                                        M.SubPointer.get_struct_record_field (|
                                                                          revert_account,
                                                                          "revm::db::states::reverts::AccountRevert",
                                                                          "account"
                                                                        |),
                                                                        [
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let γ0_0 :=
                                                                                M.SubPointer.get_struct_tuple_field (|
                                                                                  γ,
                                                                                  "revm::db::states::reverts::AccountInfoRevert::RevertTo",
                                                                                  0
                                                                                |) in
                                                                              let acc :=
                                                                                M.copy (| γ0_0 |) in
                                                                              M.alloc (|
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "alloc::vec::Vec")
                                                                                      []
                                                                                      [
                                                                                        Ty.tuple
                                                                                          [
                                                                                            Ty.path
                                                                                              "alloy_primitives::bits::address::Address";
                                                                                            Ty.apply
                                                                                              (Ty.path
                                                                                                "core::option::Option")
                                                                                              []
                                                                                              [
                                                                                                Ty.path
                                                                                                  "revm_primitives::state::AccountInfo"
                                                                                              ]
                                                                                          ];
                                                                                        Ty.path
                                                                                          "alloc::alloc::Global"
                                                                                      ],
                                                                                    "push",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    accounts;
                                                                                    Value.Tuple
                                                                                      [
                                                                                        M.read (|
                                                                                          address
                                                                                        |);
                                                                                        Value.StructTuple
                                                                                          "core::option::Option::Some"
                                                                                          [
                                                                                            M.read (|
                                                                                              acc
                                                                                            |)
                                                                                          ]
                                                                                      ]
                                                                                  ]
                                                                                |)
                                                                              |)));
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let _ :=
                                                                                M.is_struct_tuple (|
                                                                                  γ,
                                                                                  "revm::db::states::reverts::AccountInfoRevert::DeleteIt"
                                                                                |) in
                                                                              M.alloc (|
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "alloc::vec::Vec")
                                                                                      []
                                                                                      [
                                                                                        Ty.tuple
                                                                                          [
                                                                                            Ty.path
                                                                                              "alloy_primitives::bits::address::Address";
                                                                                            Ty.apply
                                                                                              (Ty.path
                                                                                                "core::option::Option")
                                                                                              []
                                                                                              [
                                                                                                Ty.path
                                                                                                  "revm_primitives::state::AccountInfo"
                                                                                              ]
                                                                                          ];
                                                                                        Ty.path
                                                                                          "alloc::alloc::Global"
                                                                                      ],
                                                                                    "push",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    accounts;
                                                                                    Value.Tuple
                                                                                      [
                                                                                        M.read (|
                                                                                          address
                                                                                        |);
                                                                                        Value.StructTuple
                                                                                          "core::option::Option::None"
                                                                                          []
                                                                                      ]
                                                                                  ]
                                                                                |)
                                                                              |)));
                                                                          fun γ =>
                                                                            ltac:(M.monadic
                                                                              (let _ :=
                                                                                M.is_struct_tuple (|
                                                                                  γ,
                                                                                  "revm::db::states::reverts::AccountInfoRevert::DoNothing"
                                                                                |) in
                                                                              M.alloc (|
                                                                                Value.Tuple []
                                                                              |)))
                                                                        ]
                                                                      |) in
                                                                    M.match_operator (|
                                                                      M.alloc (| Value.Tuple [] |),
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (let γ :=
                                                                              M.use
                                                                                (M.alloc (|
                                                                                  LogicalOp.or (|
                                                                                    M.read (|
                                                                                      M.SubPointer.get_struct_record_field (|
                                                                                        revert_account,
                                                                                        "revm::db::states::reverts::AccountRevert",
                                                                                        "wipe_storage"
                                                                                      |)
                                                                                    |),
                                                                                    ltac:(M.monadic
                                                                                      (UnOp.not (|
                                                                                        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"
                                                                                              ],
                                                                                            "is_empty",
                                                                                            []
                                                                                          |),
                                                                                          [
                                                                                            M.SubPointer.get_struct_record_field (|
                                                                                              revert_account,
                                                                                              "revm::db::states::reverts::AccountRevert",
                                                                                              "storage"
                                                                                            |)
                                                                                          ]
                                                                                        |)
                                                                                      |)))
                                                                                  |)
                                                                                |)) in
                                                                            let _ :=
                                                                              M.is_constant_or_break_match (|
                                                                                M.read (| γ |),
                                                                                Value.Bool true
                                                                              |) in
                                                                            let~ _ :=
                                                                              M.alloc (|
                                                                                M.call_closure (|
                                                                                  M.get_associated_function (|
                                                                                    Ty.apply
                                                                                      (Ty.path
                                                                                        "alloc::vec::Vec")
                                                                                      []
                                                                                      [
                                                                                        Ty.path
                                                                                          "revm::db::states::changes::PlainStorageRevert";
                                                                                        Ty.path
                                                                                          "alloc::alloc::Global"
                                                                                      ],
                                                                                    "push",
                                                                                    []
                                                                                  |),
                                                                                  [
                                                                                    storage;
                                                                                    Value.StructRecord
                                                                                      "revm::db::states::changes::PlainStorageRevert"
                                                                                      [
                                                                                        ("address",
                                                                                          M.read (|
                                                                                            address
                                                                                          |));
                                                                                        ("wiped",
                                                                                          M.read (|
                                                                                            M.SubPointer.get_struct_record_field (|
                                                                                              revert_account,
                                                                                              "revm::db::states::reverts::AccountRevert",
                                                                                              "wipe_storage"
                                                                                            |)
                                                                                          |));
                                                                                        ("storage_revert",
                                                                                          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"
                                                                                                ],
                                                                                              [],
                                                                                              "collect",
                                                                                              [
                                                                                                Ty.apply
                                                                                                  (Ty.path
                                                                                                    "alloc::vec::Vec")
                                                                                                  []
                                                                                                  [
                                                                                                    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.path
                                                                                                      "alloc::alloc::Global"
                                                                                                  ]
                                                                                              ]
                                                                                            |),
                                                                                            [
                                                                                              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_account,
                                                                                                      "revm::db::states::reverts::AccountRevert",
                                                                                                      "storage"
                                                                                                    |)
                                                                                                  |)
                                                                                                ]
                                                                                              |)
                                                                                            ]
                                                                                          |))
                                                                                      ]
                                                                                  ]
                                                                                |)
                                                                              |) in
                                                                            M.alloc (|
                                                                              Value.Tuple []
                                                                            |)));
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (M.alloc (|
                                                                              Value.Tuple []
                                                                            |)))
                                                                      ]
                                                                    |)))
                                                              ]
                                                            |) in
                                                          M.alloc (| Value.Tuple [] |)))
                                                      |)))
                                                ]
                                              |)) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.path
                                                                "alloy_primitives::bits::address::Address";
                                                              Ty.apply
                                                                (Ty.path "core::option::Option")
                                                                []
                                                                [
                                                                  Ty.path
                                                                    "revm_primitives::state::AccountInfo"
                                                                ]
                                                            ];
                                                          Ty.path "alloc::alloc::Global"
                                                        ];
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "push",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    state_reverts,
                                                    "revm::db::states::changes::PlainStateReverts",
                                                    "accounts"
                                                  |);
                                                  M.read (| accounts |)
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.path
                                                            "revm::db::states::changes::PlainStorageRevert";
                                                          Ty.path "alloc::alloc::Global"
                                                        ];
                                                      Ty.path "alloc::alloc::Global"
                                                    ],
                                                  "push",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    state_reverts,
                                                    "revm::db::states::changes::PlainStateReverts",
                                                    "storage"
                                                  |);
                                                  M.read (| storage |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                state_reverts
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_into_plain_state_reverts :
          M.IsAssociatedFunction Self "into_plain_state_reverts" into_plain_state_reverts.
      End Impl_revm_db_states_reverts_Reverts.
      
      (* StructRecord
        {
          name := "AccountRevert";
          const_params := [];
          ty_params := [];
          fields :=
            [
              ("account", Ty.path "revm::db::states::reverts::AccountInfoRevert");
              ("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::db::states::reverts::RevertToSlot";
                    Ty.path "std::hash::random::RandomState"
                  ]);
              ("previous_status", Ty.path "revm::db::states::account_status::AccountStatus");
              ("wipe_storage", Ty.path "bool")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_reverts_AccountRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountRevert".
        
        (* 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::reverts::AccountRevert"
                [
                  ("account",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "revm::db::states::reverts::AccountInfoRevert",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::reverts::AccountRevert",
                          "account"
                        |)
                      ]
                    |));
                  ("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::db::states::reverts::RevertToSlot";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::reverts::AccountRevert",
                          "storage"
                        |)
                      ]
                    |));
                  ("previous_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::reverts::AccountRevert",
                          "previous_status"
                        |)
                      ]
                    |));
                  ("wipe_storage",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.path "bool",
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::reverts::AccountRevert",
                          "wipe_storage"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_reverts_AccountRevert.
      
      Module Impl_core_default_Default_for_revm_db_states_reverts_AccountRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountRevert".
        
        (* Default *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "revm::db::states::reverts::AccountRevert"
                [
                  ("account",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "revm::db::states::reverts::AccountInfoRevert",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("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::db::states::reverts::RevertToSlot";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("previous_status",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("wipe_storage",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "bool",
                        [],
                        "default",
                        []
                      |),
                      []
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_revm_db_states_reverts_AccountRevert.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_reverts_AccountRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountRevert".
        
        (* 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 "AccountRevert" |);
                  M.read (| Value.String "account" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::reverts::AccountRevert",
                    "account"
                  |);
                  M.read (| Value.String "storage" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::reverts::AccountRevert",
                    "storage"
                  |);
                  M.read (| Value.String "previous_status" |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm::db::states::reverts::AccountRevert",
                    "previous_status"
                  |);
                  M.read (| Value.String "wipe_storage" |);
                  M.alloc (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::reverts::AccountRevert",
                      "wipe_storage"
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_reverts_AccountRevert.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_reverts_AccountRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountRevert".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_reverts_AccountRevert.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_reverts_AccountRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountRevert".
        
        (* 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.path "revm::db::states::reverts::AccountInfoRevert",
                        [ Ty.path "revm::db::states::reverts::AccountInfoRevert" ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::reverts::AccountRevert",
                          "account"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm::db::states::reverts::AccountRevert",
                          "account"
                        |)
                      ]
                    |),
                    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::db::states::reverts::RevertToSlot";
                              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"
                              ]
                          ],
                          "eq",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::reverts::AccountRevert",
                            "storage"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "revm::db::states::reverts::AccountRevert",
                            "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::reverts::AccountRevert",
                          "previous_status"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm::db::states::reverts::AccountRevert",
                          "previous_status"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::reverts::AccountRevert",
                        "wipe_storage"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm::db::states::reverts::AccountRevert",
                        "wipe_storage"
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => 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_reverts_AccountRevert.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_reverts_AccountRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountRevert".
        
        (* 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_reverts_AccountRevert.
      
      Module Impl_revm_db_states_reverts_AccountRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountRevert".
        
        (*
            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::db::states::reverts::RevertToSlot";
                        Ty.path "std::hash::random::RandomState"
                      ],
                    "len",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::reverts::AccountRevert",
                      "storage"
                    |)
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_size_hint : M.IsAssociatedFunction Self "size_hint" size_hint.
        
        (*
            pub fn new_selfdestructed_again(
                status: AccountStatus,
                account: AccountInfoRevert,
                mut previous_storage: StorageWithOriginalValues,
                updated_storage: StorageWithOriginalValues,
            ) -> Self {
                // Take present storage values as the storages that we are going to revert to.
                // As those values got destroyed.
                let mut previous_storage: HashMap<U256, RevertToSlot> = previous_storage
                    .drain()
                    .map(|(key, value)| (key, RevertToSlot::Some(value.present_value)))
                    .collect();
                for (key, _) in updated_storage {
                    previous_storage
                        .entry(key)
                        .or_insert(RevertToSlot::Destroyed);
                }
                AccountRevert {
                    account,
                    storage: previous_storage,
                    previous_status: status,
                    wipe_storage: false,
                }
            }
        *)
        Definition new_selfdestructed_again
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ status; account; previous_storage; updated_storage ] =>
            ltac:(M.monadic
              (let status := M.alloc (| status |) in
              let account := M.alloc (| account |) in
              let previous_storage := M.alloc (| previous_storage |) in
              let updated_storage := M.alloc (| updated_storage |) in
              M.read (|
                let~ previous_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::Drain")
                              []
                              [
                                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::Drain")
                              []
                              [
                                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_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",
                                []
                              |),
                              [ previous_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 key := M.copy (| γ0_0 |) in
                                              let value := M.copy (| γ0_1 |) in
                                              Value.Tuple
                                                [
                                                  M.read (| key |);
                                                  Value.StructTuple
                                                    "revm::db::states::reverts::RevertToSlot::Some"
                                                    [
                                                      M.read (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          value,
                                                          "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::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 (| 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::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~ _ :=
                                            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",
                                                      []
                                                    |),
                                                    [ previous_storage; M.read (| key |) ]
                                                  |);
                                                  Value.StructTuple
                                                    "revm::db::states::reverts::RevertToSlot::Destroyed"
                                                    []
                                                ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                M.alloc (|
                  Value.StructRecord
                    "revm::db::states::reverts::AccountRevert"
                    [
                      ("account", M.read (| account |));
                      ("storage", M.read (| previous_storage |));
                      ("previous_status", M.read (| status |));
                      ("wipe_storage", Value.Bool false)
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_selfdestructed_again :
          M.IsAssociatedFunction Self "new_selfdestructed_again" new_selfdestructed_again.
        
        (*
            pub fn new_selfdestructed_from_bundle(
                account_info_revert: AccountInfoRevert,
                bundle_account: &mut BundleAccount,
                updated_storage: &StorageWithOriginalValues,
            ) -> Option<Self> {
                match bundle_account.status {
                    AccountStatus::InMemoryChange
                    | AccountStatus::Changed
                    | AccountStatus::LoadedEmptyEIP161
                    | AccountStatus::Loaded => {
                        let mut ret = AccountRevert::new_selfdestructed_again(
                            bundle_account.status,
                            account_info_revert,
                            bundle_account.storage.drain().collect(),
                            updated_storage.clone(),
                        );
                        ret.wipe_storage = true;
                        Some(ret)
                    }
                    _ => None,
                }
            }
        *)
        Definition new_selfdestructed_from_bundle
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ account_info_revert; bundle_account; updated_storage ] =>
            ltac:(M.monadic
              (let account_info_revert := M.alloc (| account_info_revert |) in
              let bundle_account := M.alloc (| bundle_account |) in
              let updated_storage := M.alloc (| updated_storage |) in
              M.read (|
                M.match_operator (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| bundle_account |),
                    "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::LoadedEmptyEIP161"
                                  |) 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~ ret :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm::db::states::reverts::AccountRevert",
                                            "new_selfdestructed_again",
                                            []
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| bundle_account |),
                                                "revm::db::states::bundle_account::BundleAccount",
                                                "status"
                                              |)
                                            |);
                                            M.read (| account_info_revert |);
                                            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 (| bundle_account |),
                                                      "revm::db::states::bundle_account::BundleAccount",
                                                      "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.read (| updated_storage |) ]
                                            |)
                                          ]
                                        |)
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        M.SubPointer.get_struct_record_field (|
                                          ret,
                                          "revm::db::states::reverts::AccountRevert",
                                          "wipe_storage"
                                        |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      Value.StructTuple
                                        "core::option::Option::Some"
                                        [ M.read (| ret |) ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (| Value.StructTuple "core::option::Option::None" [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_selfdestructed_from_bundle :
          M.IsAssociatedFunction
            Self
            "new_selfdestructed_from_bundle"
            new_selfdestructed_from_bundle.
        
        (*
            pub fn new_selfdestructed(
                status: AccountStatus,
                account: AccountInfoRevert,
                mut storage: StorageWithOriginalValues,
            ) -> Self {
                // Zero all present storage values and save present values to AccountRevert.
                let previous_storage = storage
                    .iter_mut()
                    .map(|(key, value)| {
                        // take previous value and set ZERO as storage got destroyed.
                        ( *key, RevertToSlot::Some(value.present_value))
                    })
                    .collect();
        
                Self {
                    account,
                    storage: previous_storage,
                    previous_status: status,
                    wipe_storage: true,
                }
            }
        *)
        Definition new_selfdestructed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ status; account; storage ] =>
            ltac:(M.monadic
              (let status := M.alloc (| status |) in
              let account := M.alloc (| account |) in
              let storage := M.alloc (| storage |) in
              M.read (|
                let~ previous_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::IterMut")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "revm_primitives::state::StorageSlot"
                              ];
                            Ty.function
                              [
                                Ty.tuple
                                  [
                                    Ty.tuple
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ];
                                        Ty.apply
                                          (Ty.path "&mut")
                                          []
                                          [ 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::IterMut")
                              []
                              [
                                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 "&")
                                            []
                                            [
                                              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
                                  [
                                    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_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",
                                []
                              |),
                              [ 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 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",
                                                          "present_value"
                                                        |)
                                                      |)
                                                    ]
                                                ]))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |) in
                M.alloc (|
                  Value.StructRecord
                    "revm::db::states::reverts::AccountRevert"
                    [
                      ("account", M.read (| account |));
                      ("storage", M.read (| previous_storage |));
                      ("previous_status", M.read (| status |));
                      ("wipe_storage", Value.Bool true)
                    ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_selfdestructed :
          M.IsAssociatedFunction Self "new_selfdestructed" new_selfdestructed.
        
        (*
            pub fn is_empty(&self) -> bool {
                self.account == AccountInfoRevert::DoNothing
                    && self.storage.is_empty()
                    && !self.wipe_storage
            }
        *)
        Definition is_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              LogicalOp.and (|
                LogicalOp.and (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path "revm::db::states::reverts::AccountInfoRevert",
                      [ Ty.path "revm::db::states::reverts::AccountInfoRevert" ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::reverts::AccountRevert",
                        "account"
                      |);
                      M.alloc (|
                        Value.StructTuple
                          "revm::db::states::reverts::AccountInfoRevert::DoNothing"
                          []
                      |)
                    ]
                  |),
                  ltac:(M.monadic
                    (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"
                          ],
                        "is_empty",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::reverts::AccountRevert",
                          "storage"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (UnOp.not (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::reverts::AccountRevert",
                        "wipe_storage"
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_is_empty : M.IsAssociatedFunction Self "is_empty" is_empty.
      End Impl_revm_db_states_reverts_AccountRevert.
      
      (*
      Enum AccountInfoRevert
      {
        const_params := [];
        ty_params := [];
        variants :=
          [
            {
              name := "DoNothing";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "DeleteIt";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "RevertTo";
              item := StructTuple [ Ty.path "revm_primitives::state::AccountInfo" ];
              discriminant := None;
            }
          ];
      }
      *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_reverts_AccountInfoRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountInfoRevert".
        
        (* 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
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::reverts::AccountInfoRevert::DoNothing"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::reverts::AccountInfoRevert::DoNothing"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::reverts::AccountInfoRevert::DeleteIt"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::reverts::AccountInfoRevert::DeleteIt"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "revm::db::states::reverts::AccountInfoRevert::RevertTo",
                            0
                          |) in
                        let __self_0 := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::reverts::AccountInfoRevert::RevertTo"
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::clone::Clone",
                                  Ty.path "revm_primitives::state::AccountInfo",
                                  [],
                                  "clone",
                                  []
                                |),
                                [ M.read (| __self_0 |) ]
                              |)
                            ]
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => 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_reverts_AccountInfoRevert.
      
      Module Impl_core_default_Default_for_revm_db_states_reverts_AccountInfoRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountInfoRevert".
        
        (* Default *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructTuple "revm::db::states::reverts::AccountInfoRevert::DoNothing" []))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::default::Default"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("default", InstanceField.Method default) ].
      End Impl_core_default_Default_for_revm_db_states_reverts_AccountInfoRevert.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_reverts_AccountInfoRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountInfoRevert".
        
        (* 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.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::reverts::AccountInfoRevert::DoNothing"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_str",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "DoNothing" |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::reverts::AccountInfoRevert::DeleteIt"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_str",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "DeleteIt" |) ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "revm::db::states::reverts::AccountInfoRevert::RevertTo",
                            0
                          |) in
                        let __self_0 := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "debug_tuple_field1_finish",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "RevertTo" |); __self_0 ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => 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_reverts_AccountInfoRevert.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_reverts_AccountInfoRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountInfoRevert".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_reverts_AccountInfoRevert.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_reverts_AccountInfoRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountInfoRevert".
        
        (* 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
              M.read (|
                let~ __self_discr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [ Ty.path "revm::db::states::reverts::AccountInfoRevert" ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ __arg1_discr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [ Ty.path "revm::db::states::reverts::AccountInfoRevert" ]
                      |),
                      [ M.read (| other |) ]
                    |)
                  |) in
                M.alloc (|
                  LogicalOp.and (|
                    BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                    ltac:(M.monadic
                      (M.read (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                          [
                            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 γ0_0 := M.read (| γ0_0 |) in
                                let γ2_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_0,
                                    "revm::db::states::reverts::AccountInfoRevert::RevertTo",
                                    0
                                  |) in
                                let __self_0 := M.alloc (| γ2_0 |) in
                                let γ0_1 := M.read (| γ0_1 |) in
                                let γ2_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_1,
                                    "revm::db::states::reverts::AccountInfoRevert::RevertTo",
                                    0
                                  |) in
                                let __arg1_0 := M.alloc (| γ2_0 |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [ Ty.path "revm_primitives::state::AccountInfo" ],
                                      [
                                        Ty.apply
                                          (Ty.path "&")
                                          []
                                          [ Ty.path "revm_primitives::state::AccountInfo" ]
                                      ],
                                      "eq",
                                      []
                                    |),
                                    [ __self_0; __arg1_0 ]
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                          ]
                        |)
                      |)))
                  |)
                |)
              |)))
          | _, _, _ => 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_reverts_AccountInfoRevert.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_reverts_AccountInfoRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountInfoRevert".
        
        (* 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.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_reverts_AccountInfoRevert.
      
      Module Impl_core_hash_Hash_for_revm_db_states_reverts_AccountInfoRevert.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::AccountInfoRevert".
        
        (* Hash *)
        Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ __H ], [ self; state ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let state := M.alloc (| state |) in
              M.read (|
                let~ __self_discr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [ Ty.path "revm::db::states::reverts::AccountInfoRevert" ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::hash::Hash",
                        Ty.path "isize",
                        [],
                        "hash",
                        [ __H ]
                      |),
                      [ __self_discr; M.read (| state |) ]
                    |)
                  |) in
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "revm::db::states::reverts::AccountInfoRevert::RevertTo",
                            0
                          |) in
                        let __self_0 := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::hash::Hash",
                              Ty.path "revm_primitives::state::AccountInfo",
                              [],
                              "hash",
                              [ __H ]
                            |),
                            [ M.read (| __self_0 |); M.read (| state |) ]
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::hash::Hash"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("hash", InstanceField.Method hash) ].
      End Impl_core_hash_Hash_for_revm_db_states_reverts_AccountInfoRevert.
      
      (*
      Enum RevertToSlot
      {
        const_params := [];
        ty_params := [];
        variants :=
          [
            {
              name := "Some";
              item :=
                StructTuple
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      []
                  ];
              discriminant := None;
            };
            {
              name := "Destroyed";
              item := StructTuple [];
              discriminant := None;
            }
          ];
      }
      *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_reverts_RevertToSlot.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::RevertToSlot".
        
        (* 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
              M.read (|
                M.match_operator (|
                  Value.DeclaredButUndefined,
                  [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
                |)
              |)))
          | _, _, _ => 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_reverts_RevertToSlot.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_reverts_RevertToSlot.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::RevertToSlot".
        
        (* 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.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "revm::db::states::reverts::RevertToSlot::Some",
                            0
                          |) in
                        let __self_0 := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "debug_tuple_field1_finish",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "Some" |); __self_0 ]
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::reverts::RevertToSlot::Destroyed"
                          |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "core::fmt::Formatter",
                              "write_str",
                              []
                            |),
                            [ M.read (| f |); M.read (| Value.String "Destroyed" |) ]
                          |)
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => 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_reverts_RevertToSlot.
      
      Module Impl_core_marker_Copy_for_revm_db_states_reverts_RevertToSlot.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::RevertToSlot".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_revm_db_states_reverts_RevertToSlot.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_reverts_RevertToSlot.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::RevertToSlot".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_reverts_RevertToSlot.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_reverts_RevertToSlot.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::RevertToSlot".
        
        (* 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
              M.read (|
                let~ __self_discr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [ Ty.path "revm::db::states::reverts::RevertToSlot" ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ __arg1_discr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [ Ty.path "revm::db::states::reverts::RevertToSlot" ]
                      |),
                      [ M.read (| other |) ]
                    |)
                  |) in
                M.alloc (|
                  LogicalOp.and (|
                    BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                    ltac:(M.monadic
                      (M.read (|
                        M.match_operator (|
                          M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                          [
                            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 γ0_0 := M.read (| γ0_0 |) in
                                let γ2_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_0,
                                    "revm::db::states::reverts::RevertToSlot::Some",
                                    0
                                  |) in
                                let __self_0 := M.alloc (| γ2_0 |) in
                                let γ0_1 := M.read (| γ0_1 |) in
                                let γ2_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ0_1,
                                    "revm::db::states::reverts::RevertToSlot::Some",
                                    0
                                  |) in
                                let __arg1_0 := M.alloc (| γ2_0 |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      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.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ]
                                      ],
                                      "eq",
                                      []
                                    |),
                                    [ __self_0; __arg1_0 ]
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                          ]
                        |)
                      |)))
                  |)
                |)
              |)))
          | _, _, _ => 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_reverts_RevertToSlot.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_reverts_RevertToSlot.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::RevertToSlot".
        
        (* 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.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_reverts_RevertToSlot.
      
      Module Impl_core_hash_Hash_for_revm_db_states_reverts_RevertToSlot.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::RevertToSlot".
        
        (* Hash *)
        Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [ __H ], [ self; state ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let state := M.alloc (| state |) in
              M.read (|
                let~ __self_discr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [ Ty.path "revm::db::states::reverts::RevertToSlot" ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ _ :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::hash::Hash",
                        Ty.path "isize",
                        [],
                        "hash",
                        [ __H ]
                      |),
                      [ __self_discr; M.read (| state |) ]
                    |)
                  |) in
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "revm::db::states::reverts::RevertToSlot::Some",
                            0
                          |) in
                        let __self_0 := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::hash::Hash",
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [],
                              [],
                              "hash",
                              [ __H ]
                            |),
                            [ M.read (| __self_0 |); M.read (| state |) ]
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom Implements :
          M.IsTraitInstance
            "core::hash::Hash"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [ ("hash", InstanceField.Method hash) ].
      End Impl_core_hash_Hash_for_revm_db_states_reverts_RevertToSlot.
      
      Module Impl_revm_db_states_reverts_RevertToSlot.
        Definition Self : Ty.t := Ty.path "revm::db::states::reverts::RevertToSlot".
        
        (*
            pub fn to_previous_value(self) -> U256 {
                match self {
                    RevertToSlot::Some(value) => value,
                    RevertToSlot::Destroyed => U256::ZERO,
                }
            }
        *)
        Definition to_previous_value (ε : 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 (|
                  self,
                  [
                    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
                        value));
                    fun γ =>
                      ltac:(M.monadic
                        (let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::reverts::RevertToSlot::Destroyed"
                          |) in
                        M.get_constant (| "ruint::ZERO" |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_to_previous_value :
          M.IsAssociatedFunction Self "to_previous_value" to_previous_value.
      End Impl_revm_db_states_reverts_RevertToSlot.
    End reverts.
  End states.
End db.
