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

Module db.
  Module states.
    Module transition_account.
      (* StructRecord
        {
          name := "TransitionAccount";
          const_params := [];
          ty_params := [];
          fields :=
            [
              ("info",
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "revm_primitives::state::AccountInfo" ]);
              ("status", Ty.path "revm::db::states::account_status::AccountStatus");
              ("previous_info",
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.path "revm_primitives::state::AccountInfo" ]);
              ("previous_status", Ty.path "revm::db::states::account_status::AccountStatus");
              ("storage",
                Ty.apply
                  (Ty.path "std::collections::hash::map::HashMap")
                  []
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [];
                    Ty.path "revm_primitives::state::StorageSlot";
                    Ty.path "std::hash::random::RandomState"
                  ]);
              ("storage_was_destroyed", Ty.path "bool")
            ];
        } *)
      
      Module Impl_core_clone_Clone_for_revm_db_states_transition_account_TransitionAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::transition_account::TransitionAccount".
        
        (* 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::transition_account::TransitionAccount"
                [
                  ("info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "info"
                        |)
                      ]
                    |));
                  ("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::transition_account::TransitionAccount",
                          "status"
                        |)
                      ]
                    |));
                  ("previous_info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "previous_info"
                        |)
                      ]
                    |));
                  ("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::transition_account::TransitionAccount",
                          "previous_status"
                        |)
                      ]
                    |));
                  ("storage",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "revm_primitives::state::StorageSlot";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "storage"
                        |)
                      ]
                    |));
                  ("storage_was_destroyed",
                    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::transition_account::TransitionAccount",
                          "storage_was_destroyed"
                        |)
                      ]
                    |))
                ]))
          | _, _, _ => 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_transition_account_TransitionAccount.
      
      Module Impl_core_fmt_Debug_for_revm_db_states_transition_account_TransitionAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::transition_account::TransitionAccount".
        
        (* 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 (|
                let~ names :=
                  M.alloc (|
                    M.alloc (|
                      Value.Array
                        [
                          M.read (| Value.String "info" |);
                          M.read (| Value.String "status" |);
                          M.read (| Value.String "previous_info" |);
                          M.read (| Value.String "previous_status" |);
                          M.read (| Value.String "storage" |);
                          M.read (| Value.String "storage_was_destroyed" |)
                        ]
                    |)
                  |) in
                let~ values :=
                  M.alloc (|
                    M.alloc (|
                      Value.Array
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::transition_account::TransitionAccount",
                            "info"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::transition_account::TransitionAccount",
                            "status"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::transition_account::TransitionAccount",
                            "previous_info"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::transition_account::TransitionAccount",
                            "previous_status"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::transition_account::TransitionAccount",
                            "storage"
                          |);
                          M.alloc (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::transition_account::TransitionAccount",
                              "storage_was_destroyed"
                            |)
                          |)
                        ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "core::fmt::Formatter",
                      "debug_struct_fields_finish",
                      []
                    |),
                    [
                      M.read (| f |);
                      M.read (| Value.String "TransitionAccount" |);
                      M.read (| names |);
                      M.read (| values |)
                    ]
                  |)
                |)
              |)))
          | _, _, _ => 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_transition_account_TransitionAccount.
      
      Module Impl_core_marker_StructuralPartialEq_for_revm_db_states_transition_account_TransitionAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::transition_account::TransitionAccount".
        
        Axiom Implements :
          M.IsTraitInstance
            "core::marker::StructuralPartialEq"
            Self
            (* Trait polymorphic types *) []
            (* Instance *) [].
      End Impl_core_marker_StructuralPartialEq_for_revm_db_states_transition_account_TransitionAccount.
      
      Module Impl_core_cmp_PartialEq_for_revm_db_states_transition_account_TransitionAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::transition_account::TransitionAccount".
        
        (* 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 (|
                    LogicalOp.and (|
                      LogicalOp.and (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm_primitives::state::AccountInfo" ],
                            [
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [ Ty.path "revm_primitives::state::AccountInfo" ]
                            ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::transition_account::TransitionAccount",
                              "info"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "revm::db::states::transition_account::TransitionAccount",
                              "info"
                            |)
                          ]
                        |),
                        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::transition_account::TransitionAccount",
                                "status"
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| other |),
                                "revm::db::states::transition_account::TransitionAccount",
                                "status"
                              |)
                            ]
                          |)))
                      |),
                      ltac:(M.monadic
                        (M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "revm_primitives::state::AccountInfo" ],
                            [
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [ Ty.path "revm_primitives::state::AccountInfo" ]
                            ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::transition_account::TransitionAccount",
                              "previous_info"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "revm::db::states::transition_account::TransitionAccount",
                              "previous_info"
                            |)
                          ]
                        |)))
                    |),
                    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::transition_account::TransitionAccount",
                            "previous_status"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "revm::db::states::transition_account::TransitionAccount",
                            "previous_status"
                          |)
                        ]
                      |)))
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "revm_primitives::state::StorageSlot";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [
                          Ty.apply
                            (Ty.path "std::collections::hash::map::HashMap")
                            []
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                [];
                              Ty.path "revm_primitives::state::StorageSlot";
                              Ty.path "std::hash::random::RandomState"
                            ]
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "storage"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "storage"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::transition_account::TransitionAccount",
                        "storage_was_destroyed"
                      |)
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm::db::states::transition_account::TransitionAccount",
                        "storage_was_destroyed"
                      |)
                    |)
                  |)))
              |)))
          | _, _, _ => 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_transition_account_TransitionAccount.
      
      Module Impl_core_cmp_Eq_for_revm_db_states_transition_account_TransitionAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::transition_account::TransitionAccount".
        
        (* 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.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_transition_account_TransitionAccount.
      
      Module Impl_core_default_Default_for_revm_db_states_transition_account_TransitionAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::transition_account::TransitionAccount".
        
        (* Default *)
        Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [] =>
            ltac:(M.monadic
              (Value.StructRecord
                "revm::db::states::transition_account::TransitionAccount"
                [
                  ("info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("status",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("previous_info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("previous_status",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "revm::db::states::account_status::AccountStatus",
                        [],
                        "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_primitives::state::StorageSlot";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |));
                  ("storage_was_destroyed",
                    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_transition_account_TransitionAccount.
      
      Module Impl_revm_db_states_transition_account_TransitionAccount.
        Definition Self : Ty.t := Ty.path "revm::db::states::transition_account::TransitionAccount".
        
        (*
            pub fn new_empty_eip161(storage: StorageWithOriginalValues) -> Self {
                Self {
                    info: Some(AccountInfo::default()),
                    status: AccountStatus::InMemoryChange,
                    previous_info: None,
                    previous_status: AccountStatus::LoadedNotExisting,
                    storage,
                    storage_was_destroyed: false,
                }
            }
        *)
        Definition new_empty_eip161 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ storage ] =>
            ltac:(M.monadic
              (let storage := M.alloc (| storage |) in
              Value.StructRecord
                "revm::db::states::transition_account::TransitionAccount"
                [
                  ("info",
                    Value.StructTuple
                      "core::option::Option::Some"
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::default::Default",
                            Ty.path "revm_primitives::state::AccountInfo",
                            [],
                            "default",
                            []
                          |),
                          []
                        |)
                      ]);
                  ("status",
                    Value.StructTuple
                      "revm::db::states::account_status::AccountStatus::InMemoryChange"
                      []);
                  ("previous_info", Value.StructTuple "core::option::Option::None" []);
                  ("previous_status",
                    Value.StructTuple
                      "revm::db::states::account_status::AccountStatus::LoadedNotExisting"
                      []);
                  ("storage", M.read (| storage |));
                  ("storage_was_destroyed", Value.Bool false)
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_new_empty_eip161 :
          M.IsAssociatedFunction Self "new_empty_eip161" new_empty_eip161.
        
        (*
            pub fn has_new_contract(&self) -> Option<(B256, &Bytecode)> {
                let present_new_codehash = self.info.as_ref().map(|info| &info.code_hash);
                let previous_codehash = self.previous_info.as_ref().map(|info| &info.code_hash);
                if present_new_codehash != previous_codehash {
                    return self
                        .info
                        .as_ref()
                        .and_then(|info| info.code.as_ref().map(|c| (info.code_hash, c)));
                }
                None
            }
        *)
        Definition has_new_contract (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ present_new_codehash :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ]
                              ],
                            "map",
                            [
                              Ty.apply
                                (Ty.path "&")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                    [ Value.Integer IntegerKind.Usize 32 ]
                                    []
                                ];
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [ Ty.path "revm_primitives::state::AccountInfo" ]
                                    ]
                                ]
                                (Ty.apply
                                  (Ty.path "&")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                      [ Value.Integer IntegerKind.Usize 32 ]
                                      []
                                  ])
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ],
                                "as_ref",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::transition_account::TransitionAccount",
                                  "info"
                                |)
                              ]
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let info := M.copy (| γ |) in
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| info |),
                                                "revm_primitives::state::AccountInfo",
                                                "code_hash"
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      |) in
                    let~ previous_codehash :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ]
                              ],
                            "map",
                            [
                              Ty.apply
                                (Ty.path "&")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                    [ Value.Integer IntegerKind.Usize 32 ]
                                    []
                                ];
                              Ty.function
                                [
                                  Ty.tuple
                                    [
                                      Ty.apply
                                        (Ty.path "&")
                                        []
                                        [ Ty.path "revm_primitives::state::AccountInfo" ]
                                    ]
                                ]
                                (Ty.apply
                                  (Ty.path "&")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                      [ Value.Integer IntegerKind.Usize 32 ]
                                      []
                                  ])
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ],
                                "as_ref",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm::db::states::transition_account::TransitionAccount",
                                  "previous_info"
                                |)
                              ]
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let info := M.copy (| γ |) in
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| info |),
                                                "revm_primitives::state::AccountInfo",
                                                "code_hash"
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.match_operator (|
                        M.alloc (| Value.Tuple [] |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ :=
                                M.use
                                  (M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "&")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path
                                                    "alloy_primitives::bits::fixed::FixedBytes")
                                                  [ Value.Integer IntegerKind.Usize 32 ]
                                                  []
                                              ]
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloy_primitives::bits::fixed::FixedBytes")
                                                    [ Value.Integer IntegerKind.Usize 32 ]
                                                    []
                                                ]
                                            ]
                                        ],
                                        "ne",
                                        []
                                      |),
                                      [ present_new_codehash; previous_codehash ]
                                    |)
                                  |)) in
                              let _ :=
                                M.is_constant_or_break_match (|
                                  M.read (| γ |),
                                  Value.Bool true
                                |) in
                              M.alloc (|
                                M.never_to_any (|
                                  M.read (|
                                    M.return_ (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "&")
                                                []
                                                [ Ty.path "revm_primitives::state::AccountInfo" ]
                                            ],
                                          "and_then",
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path
                                                    "alloy_primitives::bits::fixed::FixedBytes")
                                                  [ Value.Integer IntegerKind.Usize 32 ]
                                                  [];
                                                Ty.apply
                                                  (Ty.path "&")
                                                  []
                                                  [ Ty.path "revm_primitives::bytecode::Bytecode" ]
                                              ];
                                            Ty.function
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      []
                                                      [
                                                        Ty.path
                                                          "revm_primitives::state::AccountInfo"
                                                      ]
                                                  ]
                                              ]
                                              (Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [
                                                  Ty.tuple
                                                    [
                                                      Ty.apply
                                                        (Ty.path
                                                          "alloy_primitives::bits::fixed::FixedBytes")
                                                        [ Value.Integer IntegerKind.Usize 32 ]
                                                        [];
                                                      Ty.apply
                                                        (Ty.path "&")
                                                        []
                                                        [
                                                          Ty.path
                                                            "revm_primitives::bytecode::Bytecode"
                                                        ]
                                                    ]
                                                ])
                                          ]
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "revm_primitives::state::AccountInfo" ],
                                              "as_ref",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "revm::db::states::transition_account::TransitionAccount",
                                                "info"
                                              |)
                                            ]
                                          |);
                                          M.closure
                                            (fun γ =>
                                              ltac:(M.monadic
                                                match γ with
                                                | [ α0 ] =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      M.alloc (| α0 |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let info := M.copy (| γ |) in
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path "core::option::Option")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path "&")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "revm_primitives::bytecode::Bytecode"
                                                                      ]
                                                                  ],
                                                                "map",
                                                                [
                                                                  Ty.tuple
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "alloy_primitives::bits::fixed::FixedBytes")
                                                                        [
                                                                          Value.Integer
                                                                            IntegerKind.Usize
                                                                            32
                                                                        ]
                                                                        [];
                                                                      Ty.apply
                                                                        (Ty.path "&")
                                                                        []
                                                                        [
                                                                          Ty.path
                                                                            "revm_primitives::bytecode::Bytecode"
                                                                        ]
                                                                    ];
                                                                  Ty.function
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path "&")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "revm_primitives::bytecode::Bytecode"
                                                                            ]
                                                                        ]
                                                                    ]
                                                                    (Ty.tuple
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloy_primitives::bits::fixed::FixedBytes")
                                                                          [
                                                                            Value.Integer
                                                                              IntegerKind.Usize
                                                                              32
                                                                          ]
                                                                          [];
                                                                        Ty.apply
                                                                          (Ty.path "&")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "revm_primitives::bytecode::Bytecode"
                                                                          ]
                                                                      ])
                                                                ]
                                                              |),
                                                              [
                                                                M.call_closure (|
                                                                  M.get_associated_function (|
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::option::Option")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "revm_primitives::bytecode::Bytecode"
                                                                      ],
                                                                    "as_ref",
                                                                    []
                                                                  |),
                                                                  [
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| info |),
                                                                      "revm_primitives::state::AccountInfo",
                                                                      "code"
                                                                    |)
                                                                  ]
                                                                |);
                                                                M.closure
                                                                  (fun γ =>
                                                                    ltac:(M.monadic
                                                                      match γ with
                                                                      | [ α0 ] =>
                                                                        ltac:(M.monadic
                                                                          (M.match_operator (|
                                                                            M.alloc (| α0 |),
                                                                            [
                                                                              fun γ =>
                                                                                ltac:(M.monadic
                                                                                  (let c :=
                                                                                    M.copy (|
                                                                                      γ
                                                                                    |) in
                                                                                  Value.Tuple
                                                                                    [
                                                                                      M.read (|
                                                                                        M.SubPointer.get_struct_record_field (|
                                                                                          M.read (|
                                                                                            info
                                                                                          |),
                                                                                          "revm_primitives::state::AccountInfo",
                                                                                          "code_hash"
                                                                                        |)
                                                                                      |);
                                                                                      M.read (| c |)
                                                                                    ]))
                                                                            ]
                                                                          |)))
                                                                      | _ =>
                                                                        M.impossible
                                                                          "wrong number of arguments"
                                                                      end))
                                                              ]
                                                            |)))
                                                      ]
                                                    |)))
                                                | _ => M.impossible "wrong number of arguments"
                                                end))
                                        ]
                                      |)
                                    |)
                                  |)
                                |)
                              |)));
                          fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                        ]
                      |) in
                    M.alloc (| Value.StructTuple "core::option::Option::None" [] |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_has_new_contract :
          M.IsAssociatedFunction Self "has_new_contract" has_new_contract.
        
        (*
            pub fn previous_balance(&self) -> U256 {
                self.previous_info
                    .as_ref()
                    .map(|info| info.balance)
                    .unwrap_or_default()
            }
        *)
        Definition previous_balance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        []
                    ],
                  "unwrap_or_default",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [ Ty.path "revm_primitives::state::AccountInfo" ]
                        ],
                      "map",
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [];
                        Ty.function
                          [
                            Ty.tuple
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ]
                              ]
                          ]
                          (Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [])
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "revm_primitives::state::AccountInfo" ],
                          "as_ref",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::transition_account::TransitionAccount",
                            "previous_info"
                          |)
                        ]
                      |);
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let info := M.copy (| γ |) in
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| info |),
                                            "revm_primitives::state::AccountInfo",
                                            "balance"
                                          |)
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_previous_balance :
          M.IsAssociatedFunction Self "previous_balance" previous_balance.
        
        (*
            pub fn current_balance(&self) -> U256 {
                self.info
                    .as_ref()
                    .map(|info| info.balance)
                    .unwrap_or_default()
            }
        *)
        Definition current_balance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        []
                    ],
                  "unwrap_or_default",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [
                          Ty.apply
                            (Ty.path "&")
                            []
                            [ Ty.path "revm_primitives::state::AccountInfo" ]
                        ],
                      "map",
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [];
                        Ty.function
                          [
                            Ty.tuple
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "revm_primitives::state::AccountInfo" ]
                              ]
                          ]
                          (Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [])
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [ Ty.path "revm_primitives::state::AccountInfo" ],
                          "as_ref",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "revm::db::states::transition_account::TransitionAccount",
                            "info"
                          |)
                        ]
                      |);
                      M.closure
                        (fun γ =>
                          ltac:(M.monadic
                            match γ with
                            | [ α0 ] =>
                              ltac:(M.monadic
                                (M.match_operator (|
                                  M.alloc (| α0 |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let info := M.copy (| γ |) in
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| info |),
                                            "revm_primitives::state::AccountInfo",
                                            "balance"
                                          |)
                                        |)))
                                  ]
                                |)))
                            | _ => M.impossible "wrong number of arguments"
                            end))
                    ]
                  |)
                ]
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_current_balance :
          M.IsAssociatedFunction Self "current_balance" current_balance.
        
        (*
            pub fn balance_delta(&self) -> Option<I256> {
                let previous_balance = self.previous_balance();
                let current_balance = self.current_balance();
                let delta = I256::try_from(previous_balance.abs_diff(current_balance)).ok()?;
                if current_balance >= previous_balance {
                    Some(delta)
                } else {
                    delta.checked_neg()
                }
            }
        *)
        Definition balance_delta (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.catch_return (|
                ltac:(M.monadic
                  (M.read (|
                    let~ previous_balance :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm::db::states::transition_account::TransitionAccount",
                            "previous_balance",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |) in
                    let~ current_balance :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "revm::db::states::transition_account::TransitionAccount",
                            "current_balance",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |) in
                    let~ delta :=
                      M.copy (|
                        M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::ops::try_trait::Try",
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "alloy_primitives::signed::int::Signed")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                [],
                                "branch",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "alloy_primitives::signed::int::Signed")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [];
                                        Ty.path
                                          "alloy_primitives::signed::errors::BigIntConversionError"
                                      ],
                                    "ok",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::convert::TryFrom",
                                        Ty.apply
                                          (Ty.path "alloy_primitives::signed::int::Signed")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            []
                                        ],
                                        "try_from",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [],
                                            "abs_diff",
                                            []
                                          |),
                                          [
                                            M.read (| previous_balance |);
                                            M.read (| current_balance |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Break",
                                    0
                                  |) in
                                let residual := M.copy (| γ0_0 |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        M.call_closure (|
                                          M.get_trait_method (|
                                            "core::ops::try_trait::FromResidual",
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "alloy_primitives::signed::int::Signed")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  []
                                              ],
                                            [
                                              Ty.apply
                                                (Ty.path "core::option::Option")
                                                []
                                                [ Ty.path "core::convert::Infallible" ]
                                            ],
                                            "from_residual",
                                            []
                                          |),
                                          [ M.read (| residual |) ]
                                        |)
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ =>
                              ltac:(M.monadic
                                (let γ0_0 :=
                                  M.SubPointer.get_struct_tuple_field (|
                                    γ,
                                    "core::ops::control_flow::ControlFlow::Continue",
                                    0
                                  |) in
                                let val := M.copy (| γ0_0 |) in
                                val))
                          ]
                        |)
                      |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialOrd",
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [],
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ],
                                      "ge",
                                      []
                                    |),
                                    [ current_balance; previous_balance ]
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              Value.StructTuple "core::option::Option::Some" [ M.read (| delta |) ]
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloy_primitives::signed::int::Signed")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [],
                                  "checked_neg",
                                  []
                                |),
                                [ M.read (| delta |) ]
                              |)
                            |)))
                      ]
                    |)
                  |)))
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_balance_delta :
          M.IsAssociatedFunction Self "balance_delta" balance_delta.
        
        (*
            pub fn update(&mut self, other: Self) {
                self.info = other.info.clone();
                self.status = other.status;
        
                // if transition is from some to destroyed drop the storage.
                // This need to be done here as it is one increment of the state.
                if matches!(
                    other.status,
                    AccountStatus::Destroyed | AccountStatus::DestroyedAgain
                ) {
                    self.storage = other.storage;
                    self.storage_was_destroyed = true;
                } else {
                    // update changed values to this transition.
                    for (key, slot) in other.storage.into_iter() {
                        match self.storage.entry(key) {
                            hash_map::Entry::Vacant(entry) => {
                                entry.insert(slot);
                            }
                            hash_map::Entry::Occupied(mut entry) => {
                                let value = entry.get_mut();
                                // if new value is same as original value. Remove storage entry.
                                if value.original_value() == slot.present_value() {
                                    entry.remove();
                                } else {
                                    // if value is different, update transition present value;
                                    value.present_value = slot.present_value;
                                }
                            }
                        }
                    }
                }
            }
        *)
        Definition update (ε : 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.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::transition_account::TransitionAccount",
                      "info"
                    |),
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          other,
                          "revm::db::states::transition_account::TransitionAccount",
                          "info"
                        |)
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.write (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm::db::states::transition_account::TransitionAccount",
                      "status"
                    |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        other,
                        "revm::db::states::transition_account::TransitionAccount",
                        "status"
                      |)
                    |)
                  |) in
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.match_operator (|
                              M.SubPointer.get_struct_record_field (|
                                other,
                                "revm::db::states::transition_account::TransitionAccount",
                                "status"
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.find_or_pattern (|
                                      γ,
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "revm::db::states::account_status::AccountStatus::Destroyed"
                                              |) in
                                            Value.Tuple []));
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let _ :=
                                              M.is_struct_tuple (|
                                                γ,
                                                "revm::db::states::account_status::AccountStatus::DestroyedAgain"
                                              |) in
                                            Value.Tuple []))
                                      ],
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [] => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                              ]
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::transition_account::TransitionAccount",
                              "storage"
                            |),
                            M.read (|
                              M.SubPointer.get_struct_record_field (|
                                other,
                                "revm::db::states::transition_account::TransitionAccount",
                                "storage"
                              |)
                            |)
                          |) in
                        let~ _ :=
                          M.write (|
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm::db::states::transition_account::TransitionAccount",
                              "storage_was_destroyed"
                            |),
                            Value.Bool true
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (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::IntoIter")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [];
                                      Ty.path "revm_primitives::state::StorageSlot"
                                    ],
                                  [],
                                  "into_iter",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_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 (|
                                        M.SubPointer.get_struct_record_field (|
                                          other,
                                          "revm::db::states::transition_account::TransitionAccount",
                                          "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 slot := M.copy (| γ1_1 |) in
                                                M.match_operator (|
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path
                                                            "std::collections::hash::map::HashMap")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "ruint::Uint")
                                                              [
                                                                Value.Integer IntegerKind.Usize 256;
                                                                Value.Integer IntegerKind.Usize 4
                                                              ]
                                                              [];
                                                            Ty.path
                                                              "revm_primitives::state::StorageSlot";
                                                            Ty.path "std::hash::random::RandomState"
                                                          ],
                                                        "entry",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "revm::db::states::transition_account::TransitionAccount",
                                                          "storage"
                                                        |);
                                                        M.read (| key |)
                                                      ]
                                                    |)
                                                  |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "std::collections::hash::map::Entry::Vacant",
                                                            0
                                                          |) in
                                                        let entry := M.copy (| γ0_0 |) in
                                                        let~ _ :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "std::collections::hash::map::VacantEntry")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path "ruint::Uint")
                                                                      [
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          256;
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          4
                                                                      ]
                                                                      [];
                                                                    Ty.path
                                                                      "revm_primitives::state::StorageSlot"
                                                                  ],
                                                                "insert",
                                                                []
                                                              |),
                                                              [
                                                                M.read (| entry |);
                                                                M.read (| slot |)
                                                              ]
                                                            |)
                                                          |) in
                                                        M.alloc (| Value.Tuple [] |)));
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let γ0_0 :=
                                                          M.SubPointer.get_struct_tuple_field (|
                                                            γ,
                                                            "std::collections::hash::map::Entry::Occupied",
                                                            0
                                                          |) in
                                                        let entry := M.copy (| γ0_0 |) in
                                                        let~ value :=
                                                          M.alloc (|
                                                            M.call_closure (|
                                                              M.get_associated_function (|
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "std::collections::hash::map::OccupiedEntry")
                                                                  []
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path "ruint::Uint")
                                                                      [
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          256;
                                                                        Value.Integer
                                                                          IntegerKind.Usize
                                                                          4
                                                                      ]
                                                                      [];
                                                                    Ty.path
                                                                      "revm_primitives::state::StorageSlot"
                                                                  ],
                                                                "get_mut",
                                                                []
                                                              |),
                                                              [ entry ]
                                                            |)
                                                          |) in
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      M.call_closure (|
                                                                        M.get_trait_method (|
                                                                          "core::cmp::PartialEq",
                                                                          Ty.apply
                                                                            (Ty.path "ruint::Uint")
                                                                            [
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                256;
                                                                              Value.Integer
                                                                                IntegerKind.Usize
                                                                                4
                                                                            ]
                                                                            [],
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "ruint::Uint")
                                                                              [
                                                                                Value.Integer
                                                                                  IntegerKind.Usize
                                                                                  256;
                                                                                Value.Integer
                                                                                  IntegerKind.Usize
                                                                                  4
                                                                              ]
                                                                              []
                                                                          ],
                                                                          "eq",
                                                                          []
                                                                        |),
                                                                        [
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "revm_primitives::state::StorageSlot",
                                                                                "original_value",
                                                                                []
                                                                              |),
                                                                              [ M.read (| value |) ]
                                                                            |)
                                                                          |);
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "revm_primitives::state::StorageSlot",
                                                                                "present_value",
                                                                                []
                                                                              |),
                                                                              [ slot ]
                                                                            |)
                                                                          |)
                                                                        ]
                                                                      |)
                                                                    |)) 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
                                                                            "std::collections::hash::map::OccupiedEntry")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path
                                                                                "ruint::Uint")
                                                                              [
                                                                                Value.Integer
                                                                                  IntegerKind.Usize
                                                                                  256;
                                                                                Value.Integer
                                                                                  IntegerKind.Usize
                                                                                  4
                                                                              ]
                                                                              [];
                                                                            Ty.path
                                                                              "revm_primitives::state::StorageSlot"
                                                                          ],
                                                                        "remove",
                                                                        []
                                                                      |),
                                                                      [ M.read (| entry |) ]
                                                                    |)
                                                                  |) in
                                                                M.alloc (| Value.Tuple [] |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let~ _ :=
                                                                  M.write (|
                                                                    M.SubPointer.get_struct_record_field (|
                                                                      M.read (| value |),
                                                                      "revm_primitives::state::StorageSlot",
                                                                      "present_value"
                                                                    |),
                                                                    M.read (|
                                                                      M.SubPointer.get_struct_record_field (|
                                                                        slot,
                                                                        "revm_primitives::state::StorageSlot",
                                                                        "present_value"
                                                                      |)
                                                                    |)
                                                                  |) in
                                                                M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |)))
                                                  ]
                                                |)))
                                          ]
                                        |) in
                                      M.alloc (| Value.Tuple [] |)))
                                  |)))
                            ]
                          |))))
                  ]
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_update : M.IsAssociatedFunction Self "update" update.
        
        (*
            pub fn create_revert(self) -> Option<AccountRevert> {
                let mut previous_account = self.original_bundle_account();
                previous_account.update_and_create_revert(self)
            }
        *)
        Definition create_revert (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              M.read (|
                let~ previous_account :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm::db::states::transition_account::TransitionAccount",
                        "original_bundle_account",
                        []
                      |),
                      [ self ]
                    |)
                  |) in
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm::db::states::bundle_account::BundleAccount",
                      "update_and_create_revert",
                      []
                    |),
                    [ previous_account; M.read (| self |) ]
                  |)
                |)
              |)))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_create_revert :
          M.IsAssociatedFunction Self "create_revert" create_revert.
        
        (*
            pub fn present_bundle_account(&self) -> BundleAccount {
                BundleAccount {
                    info: self.info.clone(),
                    original_info: self.previous_info.clone(),
                    storage: self.storage.clone(),
                    status: self.status,
                }
            }
        *)
        Definition present_bundle_account
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "revm::db::states::bundle_account::BundleAccount"
                [
                  ("info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "info"
                        |)
                      ]
                    |));
                  ("original_info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "previous_info"
                        |)
                      ]
                    |));
                  ("storage",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "revm_primitives::state::StorageSlot";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "storage"
                        |)
                      ]
                    |));
                  ("status",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::transition_account::TransitionAccount",
                        "status"
                      |)
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_present_bundle_account :
          M.IsAssociatedFunction Self "present_bundle_account" present_bundle_account.
        
        (*
            fn original_bundle_account(&self) -> BundleAccount {
                BundleAccount {
                    info: self.previous_info.clone(),
                    original_info: self.previous_info.clone(),
                    storage: StorageWithOriginalValues::new(),
                    status: self.previous_status,
                }
            }
        *)
        Definition original_bundle_account
            (ε : list Value.t)
            (τ : list Ty.t)
            (α : list Value.t)
            : M :=
          match ε, τ, α with
          | [], [], [ self ] =>
            ltac:(M.monadic
              (let self := M.alloc (| self |) in
              Value.StructRecord
                "revm::db::states::bundle_account::BundleAccount"
                [
                  ("info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "previous_info"
                        |)
                      ]
                    |));
                  ("original_info",
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::clone::Clone",
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [ Ty.path "revm_primitives::state::AccountInfo" ],
                        [],
                        "clone",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm::db::states::transition_account::TransitionAccount",
                          "previous_info"
                        |)
                      ]
                    |));
                  ("storage",
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "std::collections::hash::map::HashMap")
                          []
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              [];
                            Ty.path "revm_primitives::state::StorageSlot";
                            Ty.path "std::hash::random::RandomState"
                          ],
                        "new",
                        []
                      |),
                      []
                    |));
                  ("status",
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm::db::states::transition_account::TransitionAccount",
                        "previous_status"
                      |)
                    |))
                ]))
          | _, _, _ => M.impossible "wrong number of arguments"
          end.
        
        Axiom AssociatedFunction_original_bundle_account :
          M.IsAssociatedFunction Self "original_bundle_account" original_bundle_account.
      End Impl_revm_db_states_transition_account_TransitionAccount.
    End transition_account.
  End states.
End db.
