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

Module db.
  Module states.
    Module account_status.
      (*
      Enum AccountStatus
      {
        const_params := [];
        ty_params := [];
        variants :=
          [
            {
              name := "LoadedNotExisting";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "Loaded";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "LoadedEmptyEIP161";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "InMemoryChange";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "Changed";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "Destroyed";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "DestroyedChanged";
              item := StructTuple [];
              discriminant := None;
            };
            {
              name := "DestroyedAgain";
              item := StructTuple [];
              discriminant := None;
            }
          ];
      }
      *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        (* 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.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_account_status_AccountStatus.
      
      Module Impl_core_marker_Copy_for_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::Copy"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_Copy_for_revm_db_states_account_status_AccountStatus.
      
      Module Impl_core_default_Default_for_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        (* Default *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructTuple
                "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                []))
          | _, _, _ => 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_account_status_AccountStatus.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        (* 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", "write_str", [] |),
                [
                  M.read (| f |);
                  M.read (|
                    M.match_operator (|
                      self,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                              |) in
                            M.alloc (| M.read (| Value.String "LoadedNotExisting" |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::Loaded"
                              |) in
                            M.alloc (| M.read (| Value.String "Loaded" |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                              |) in
                            M.alloc (| M.read (| Value.String "LoadedEmptyEIP161" |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::InMemoryChange"
                              |) in
                            M.alloc (| M.read (| Value.String "InMemoryChange" |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::Changed"
                              |) in
                            M.alloc (| M.read (| Value.String "Changed" |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::Destroyed"
                              |) in
                            M.alloc (| M.read (| Value.String "Destroyed" |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                              |) in
                            M.alloc (| M.read (| Value.String "DestroyedChanged" |) |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ := M.read (| γ |) in
                            let _ :=
                              M.is_struct_tuple (|
                                γ,
                                "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                              |) in
                            M.alloc (| M.read (| Value.String "DestroyedAgain" |) |)))
                      ]
                    |)
                  |)
                ]
              |)))
          | _, _, _ => 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_account_status_AccountStatus.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_account_status_AccountStatus.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        (* 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::account_status::AccountStatus" ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                let~ __arg1_discr :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_function (|
                        "core::intrinsics::discriminant_value",
                        [ Ty.path "revm::db::states::account_status::AccountStatus" ]
                      |),
                      [ M.read (| other |) ]
                    |)
                  |) in
                M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
              |)))
          | _, _, _ => 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_account_status_AccountStatus.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        (* 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
              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_account_status_AccountStatus.
      
      Module Impl_core_hash_Hash_for_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        (* 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::account_status::AccountStatus" ]
                      |),
                      [ M.read (| self |) ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::hash::Hash",
                      Ty.path "isize",
                      [],
                      "hash",
                      [ __H ]
                    |),
                    [ __self_discr; M.read (| state |) ]
                  |)
                |)
              |)))
          | _, _, _ => 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_account_status_AccountStatus.
      
      Module Impl_revm_db_states_account_status_AccountStatus.
        Definition Self : Ty.t := Ty.path "revm::db::states::account_status::AccountStatus".
        
        (*
            pub fn is_not_modified(&self) -> bool {
                matches!(
                    self,
                    AccountStatus::LoadedNotExisting
                        | AccountStatus::Loaded
                        | AccountStatus::LoadedEmptyEIP161
                )
            }
        *)
        Definition is_not_modified (ε : 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
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Loaded"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_is_not_modified :
          M.IsAssociatedFunction Self "is_not_modified" is_not_modified.
        
        (*
            pub fn was_destroyed(&self) -> bool {
                matches!(
                    self,
                    AccountStatus::Destroyed
                        | AccountStatus::DestroyedChanged
                        | AccountStatus::DestroyedAgain
                )
            }
        *)
        Definition was_destroyed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Destroyed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_was_destroyed :
          M.IsAssociatedFunction Self "was_destroyed" was_destroyed.
        
        (*
            pub fn is_storage_known(&self) -> bool {
                matches!(
                    self,
                    AccountStatus::LoadedNotExisting
                        | AccountStatus::InMemoryChange
                        | AccountStatus::Destroyed
                        | AccountStatus::DestroyedChanged
                        | AccountStatus::DestroyedAgain
                )
            }
        *)
        Definition is_storage_known (ε : 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
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Destroyed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_is_storage_known :
          M.IsAssociatedFunction Self "is_storage_known" is_storage_known.
        
        (*
            pub fn is_modified_and_not_destroyed(&self) -> bool {
                matches!(self, AccountStatus::Changed | AccountStatus::InMemoryChange)
            }
        *)
        Definition is_modified_and_not_destroyed
            (ε : 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
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Changed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_is_modified_and_not_destroyed :
          M.IsAssociatedFunction Self "is_modified_and_not_destroyed" is_modified_and_not_destroyed.
        
        (*
            pub fn on_created(&self) -> AccountStatus {
                match self {
                    // if account was destroyed previously just copy new info to it.
                    AccountStatus::DestroyedAgain
                    | AccountStatus::Destroyed
                    | AccountStatus::DestroyedChanged => AccountStatus::DestroyedChanged,
                    // if account is loaded from db.
                    AccountStatus::LoadedNotExisting
                    // Loaded empty eip161 to creates is not possible as CREATE2 was added after EIP-161
                    | AccountStatus::LoadedEmptyEIP161
                    | AccountStatus::Loaded
                    | AccountStatus::Changed
                    | AccountStatus::InMemoryChange => {
                        // If account is loaded and not empty this means that account has some balance.
                        // This means that account cannot be created.
                        // We are assuming that EVM did necessary checks before allowing account to be created.
                        AccountStatus::InMemoryChange
                    }
                }
            }
        *)
        Definition on_created (ε : 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
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Destroyed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.StructTuple
                                        "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                        []
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Loaded"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Changed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.StructTuple
                                        "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                        []
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_on_created : M.IsAssociatedFunction Self "on_created" on_created.
        
        (*
            pub fn on_touched_empty_post_eip161(&self) -> AccountStatus {
                match self {
                    // Account can be touched but not existing. The status should remain the same.
                    AccountStatus::LoadedNotExisting => AccountStatus::LoadedNotExisting,
                    // Account can be created empty and only then touched.
                    AccountStatus::InMemoryChange
                    | AccountStatus::Destroyed
                    | AccountStatus::LoadedEmptyEIP161 => AccountStatus::Destroyed,
                    // Transition to destroy the account.
                    AccountStatus::DestroyedAgain | AccountStatus::DestroyedChanged => {
                        AccountStatus::DestroyedAgain
                    }
                    // Account statuses considered unreachable.
                    AccountStatus::Loaded | AccountStatus::Changed => {
                        unreachable!("Wrong state transition, touch empty is not possible from {self:?}");
                    }
                }
            }
        *)
        Definition on_touched_empty_post_eip161
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Destroyed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.StructTuple
                                        "revm::db::states::account_status::AccountStatus::Destroyed"
                                        []
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.StructTuple
                                        "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                        []
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Loaded"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Changed"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic_fmt", [] |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_v1",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (|
                                                        Value.String
                                                          "internal error: entered unreachable code: Wrong state transition, touch empty is not possible from "
                                                      |)
                                                    ]
                                                |);
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_debug",
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "revm::db::states::account_status::AccountStatus"
                                                              ]
                                                          ]
                                                        |),
                                                        [ self ]
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_on_touched_empty_post_eip161 :
          M.IsAssociatedFunction Self "on_touched_empty_post_eip161" on_touched_empty_post_eip161.
        
        (*
            pub fn on_touched_created_pre_eip161(&self, had_no_info: bool) -> Option<AccountStatus> {
                match self {
                    AccountStatus::LoadedEmptyEIP161 => None,
                    AccountStatus::DestroyedChanged => {
                        if had_no_info {
                            None
                        } else {
                            Some(AccountStatus::DestroyedChanged)
                        }
                    }
                    AccountStatus::Destroyed | AccountStatus::DestroyedAgain => {
                        Some(AccountStatus::DestroyedChanged)
                    }
                    AccountStatus::InMemoryChange | AccountStatus::LoadedNotExisting => {
                        Some(AccountStatus::InMemoryChange)
                    }
                    AccountStatus::Loaded | AccountStatus::Changed => {
                        unreachable!("Wrong state transition, touch crate is not possible from {self:?}")
                    }
                }
            }
        *)
        Definition on_touched_created_pre_eip161
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self; had_no_info ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let had_no_info := M.alloc (| had_no_info |) in
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                          |) in
                        M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                          |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.use had_no_info in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple
                                    "core::option::Option::Some"
                                    [
                                      Value.StructTuple
                                        "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                        []
                                    ]
                                |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Destroyed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.StructTuple
                                        "core::option::Option::Some"
                                        [
                                          Value.StructTuple
                                            "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                            []
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.StructTuple
                                        "core::option::Option::Some"
                                        [
                                          Value.StructTuple
                                            "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                            []
                                        ]
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Loaded"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Changed"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      M.never_to_any (|
                                        M.call_closure (|
                                          M.get_function (| "core::panicking::panic_fmt", [] |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_v1",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (|
                                                        Value.String
                                                          "internal error: entered unreachable code: Wrong state transition, touch crate is not possible from "
                                                      |)
                                                    ]
                                                |);
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.path "core::fmt::rt::Argument",
                                                          "new_debug",
                                                          [
                                                            Ty.apply
                                                              (Ty.path "&")
                                                              []
                                                              [
                                                                Ty.path
                                                                  "revm::db::states::account_status::AccountStatus"
                                                              ]
                                                          ]
                                                        |),
                                                        [ self ]
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                        |)
                                      |)
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_on_touched_created_pre_eip161 :
          M.IsAssociatedFunction Self "on_touched_created_pre_eip161" on_touched_created_pre_eip161.
        
        (*
            pub fn on_changed(&self, had_no_nonce_and_code: bool) -> AccountStatus {
                match self {
                    // If the account was loaded as not existing, promote it to changed.
                    // This account was likely created by a balance transfer.
                    AccountStatus::LoadedNotExisting => AccountStatus::InMemoryChange,
                    // Change on empty account, should transfer storage if there is any.
                    // There is possibility that there are storage entries inside db.
                    // That storage is used in merkle tree calculation before state clear EIP.
                    AccountStatus::LoadedEmptyEIP161 => AccountStatus::InMemoryChange,
                    // The account was loaded as existing.
                    AccountStatus::Loaded => {
                        if had_no_nonce_and_code {
                            // account is fully in memory
                            AccountStatus::InMemoryChange
                        } else {
                            // can be contract and some of storage slots can be present inside db.
                            AccountStatus::Changed
                        }
                    }
        
                    // On change, the "changed" type account statuses are preserved.
                    // Any checks for empty accounts are done outside of this fn.
                    AccountStatus::Changed => AccountStatus::Changed,
                    AccountStatus::InMemoryChange => AccountStatus::InMemoryChange,
                    AccountStatus::DestroyedChanged => AccountStatus::DestroyedChanged,
        
                    // If account is destroyed and then changed this means this is
                    // balance transfer.
                    AccountStatus::Destroyed | AccountStatus::DestroyedAgain => {
                        AccountStatus::DestroyedChanged
                    }
                }
            }
        *)
        Definition on_changed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self; had_no_nonce_and_code ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              let had_no_nonce_and_code := M.alloc (| had_no_nonce_and_code |) in
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::account_status::AccountStatus::InMemoryChange"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::LoadedEmptyEIP161"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::account_status::AccountStatus::InMemoryChange"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::Loaded"
                          |) in
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.use had_no_nonce_and_code in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  Value.StructTuple
                                    "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                    []
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (M.alloc (|
                                  Value.StructTuple
                                    "revm::db::states::account_status::AccountStatus::Changed"
                                    []
                                |)))
                          ]
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::Changed"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::account_status::AccountStatus::Changed"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::InMemoryChange"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::account_status::AccountStatus::InMemoryChange"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Destroyed"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.StructTuple
                                        "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                        []
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_on_changed : M.IsAssociatedFunction Self "on_changed" on_changed.
        
        (*
            pub fn on_selfdestructed(&self) -> AccountStatus {
                match self {
                    // Non existing account can't be destroyed.
                    AccountStatus::LoadedNotExisting => AccountStatus::LoadedNotExisting,
                    // If account is created and selfdestructed in the same block, mark it as destroyed again.
                    // Note: there is no big difference between Destroyed and DestroyedAgain in this case,
                    // but was added for clarity.
                    AccountStatus::DestroyedChanged
                    | AccountStatus::DestroyedAgain
                    | AccountStatus::Destroyed => AccountStatus::DestroyedAgain,
        
                    // Transition to destroyed status.
                    _ => AccountStatus::Destroyed,
                }
            }
        *)
        Definition on_selfdestructed (ε : 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::account_status::AccountStatus::LoadedNotExisting"
                          |) in
                        M.alloc (|
                          Value.StructTuple
                            "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                            []
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.find_or_pattern (|
                          γ,
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                  |) in
                                Value.Tuple []));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let _ :=
                                  M.is_struct_tuple (|
                                    γ,
                                    "revm::db::states::account_status::AccountStatus::Destroyed"
                                  |) in
                                Value.Tuple []))
                          ],
                          M.closure
                            (fun γ =>
                              ltac:(M.monadic
                                match γ with
                                | [] =>
                                  ltac:(M.monadic
                                    (M.alloc (|
                                      Value.StructTuple
                                        "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                        []
                                    |)))
                                | _ => M.impossible "wrong number of arguments"
                                end))
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          Value.StructTuple
                            "revm::db::states::account_status::AccountStatus::Destroyed"
                            []
                        |)))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_on_selfdestructed :
          M.IsAssociatedFunction Self "on_selfdestructed" on_selfdestructed.
        
        (*
            pub fn transition(&mut self, other: Self) {
                *self = match (self.was_destroyed(), other.was_destroyed()) {
                    (true, false) => Self::DestroyedChanged,
                    (false, false) if *self == Self::InMemoryChange => Self::InMemoryChange,
                    _ => other,
                };
            }
        *)
        Definition transition (ε : 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.write (|
                    M.read (| self |),
                    M.read (|
                      M.match_operator (|
                        M.alloc (|
                          Value.Tuple
                            [
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm::db::states::account_status::AccountStatus",
                                  "was_destroyed",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |);
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "revm::db::states::account_status::AccountStatus",
                                  "was_destroyed",
                                  []
                                |),
                                [ 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 _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ0_0 |),
                                  Value.Bool true
                                |) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ0_1 |),
                                  Value.Bool false
                                |) in
                              M.alloc (|
                                Value.StructTuple
                                  "revm::db::states::account_status::AccountStatus::DestroyedChanged"
                                  []
                              |)));
                          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 _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ0_0 |),
                                  Value.Bool false
                                |) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ0_1 |),
                                  Value.Bool false
                                |) in
                              let γ :=
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.path "revm::db::states::account_status::AccountStatus",
                                      [ Ty.path "revm::db::states::account_status::AccountStatus" ],
                                      "eq",
                                      []
                                    |),
                                    [
                                      M.read (| self |);
                                      M.alloc (|
                                        Value.StructTuple
                                          "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                          []
                                      |)
                                    ]
                                  |)
                                |) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                Value.StructTuple
                                  "revm::db::states::account_status::AccountStatus::InMemoryChange"
                                  []
                              |)));
                          fun γ => ltac:(M.monadic other)
                        ]
                      |)
                    |)
                  |) in
                M.alloc (| Value.Tuple [] |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_transition : M.IsAssociatedFunction Self "transition" transition.
      End Impl_revm_db_states_account_status_AccountStatus.
    End account_status.
  End states.
End db.
