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

Module state.
  Axiom State :
    (Ty.path "revm_primitives::state::State") =
      (Ty.apply
        (Ty.path "std::collections::hash::map::HashMap")
        []
        [
          Ty.path "alloy_primitives::bits::address::Address";
          Ty.path "revm_primitives::state::Account";
          Ty.path "std::hash::random::RandomState"
        ]).
  
  Axiom TransientStorage :
    (Ty.path "revm_primitives::state::TransientStorage") =
      (Ty.apply
        (Ty.path "std::collections::hash::map::HashMap")
        []
        [
          Ty.tuple
            [
              Ty.path "alloy_primitives::bits::address::Address";
              Ty.apply
                (Ty.path "ruint::Uint")
                [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                []
            ];
          Ty.apply
            (Ty.path "ruint::Uint")
            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
            [];
          Ty.path "std::hash::random::RandomState"
        ]).
  
  Axiom Storage :
    (Ty.path "revm_primitives::state::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"
        ]).
  
  (* StructRecord
    {
      name := "Account";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("info", Ty.path "revm_primitives::state::AccountInfo");
          ("storage",
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.apply
                  (Ty.path "ruint::Uint")
                  [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                  [];
                Ty.path "revm_primitives::state::StorageSlot";
                Ty.path "std::hash::random::RandomState"
              ]);
          ("status", Ty.path "revm_primitives::state::AccountStatus")
        ];
    } *)
  
  Module Impl_core_fmt_Debug_for_revm_primitives_state_Account.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::Account".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field3_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "Account" |);
              M.read (| Value.String "info" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::Account",
                "info"
              |);
              M.read (| Value.String "storage" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::Account",
                "storage"
              |);
              M.read (| Value.String "status" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::state::Account",
                  "status"
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_revm_primitives_state_Account.
  
  Module Impl_core_clone_Clone_for_revm_primitives_state_Account.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::Account".
    
    (* 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_primitives::state::Account"
            [
              ("info",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "revm_primitives::state::AccountInfo",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "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_primitives::state::Account",
                      "storage"
                    |)
                  ]
                |));
              ("status",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "revm_primitives::state::AccountStatus",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "status"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_revm_primitives_state_Account.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_state_Account.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::Account".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_state_Account.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_state_Account.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::Account".
    
    (* 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 (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.path "revm_primitives::state::AccountInfo",
                  [ Ty.path "revm_primitives::state::AccountInfo" ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::state::Account",
                    "info"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::state::Account",
                    "info"
                  |)
                ]
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply
                      (Ty.path "std::collections::hash::map::HashMap")
                      []
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [];
                        Ty.path "revm_primitives::state::StorageSlot";
                        Ty.path "std::hash::random::RandomState"
                      ],
                    [
                      Ty.apply
                        (Ty.path "std::collections::hash::map::HashMap")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [];
                          Ty.path "revm_primitives::state::StorageSlot";
                          Ty.path "std::hash::random::RandomState"
                        ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "storage"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::state::Account",
                      "storage"
                    |)
                  ]
                |)))
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.path "revm_primitives::state::AccountStatus",
                  [ Ty.path "revm_primitives::state::AccountStatus" ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::state::Account",
                    "status"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::state::Account",
                    "status"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_revm_primitives_state_Account.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_state_Account.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::Account".
    
    (* 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.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_primitives_state_Account.
  
  Module Impl_core_default_Default_for_revm_primitives_state_Account.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::Account".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_primitives::state::Account"
            [
              ("info",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::state::AccountInfo",
                    [],
                    "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",
                    []
                  |),
                  []
                |));
              ("status",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::state::AccountStatus",
                    [],
                    "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_primitives_state_Account.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    (*     Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_tuple_field1_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "AccountStatus" |);
              M.alloc (|
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "revm_primitives::state::AccountStatus",
                  0
                |)
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_clone_Clone_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    (*     Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::clone::Clone"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("clone", InstanceField.Method clone) ].
  End Impl_core_clone_Clone_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_marker_Copy_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    (*     PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.path "revm_primitives::state::_::InternalBitFlags",
              [ Ty.path "revm_primitives::state::_::InternalBitFlags" ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "revm_primitives::state::AccountStatus",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "revm_primitives::state::AccountStatus",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    (*     Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_cmp_PartialOrd_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    (*     PartialOrd *)
    Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialOrd",
              Ty.path "revm_primitives::state::_::InternalBitFlags",
              [ Ty.path "revm_primitives::state::_::InternalBitFlags" ],
              "partial_cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "revm_primitives::state::AccountStatus",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "revm_primitives::state::AccountStatus",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialOrd"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
  End Impl_core_cmp_PartialOrd_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_cmp_Ord_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    (*     Ord *)
    Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::Ord",
              Ty.path "revm_primitives::state::_::InternalBitFlags",
              [],
              "cmp",
              []
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "revm_primitives::state::AccountStatus",
                0
              |);
              M.SubPointer.get_struct_tuple_field (|
                M.read (| other |),
                "revm_primitives::state::AccountStatus",
                0
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Ord"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
  End Impl_core_cmp_Ord_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_hash_Hash_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    (*     Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::hash::Hash",
              Ty.path "revm_primitives::state::_::InternalBitFlags",
              [],
              "hash",
              [ __H ]
            |),
            [
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "revm_primitives::state::AccountStatus",
                0
              |);
              M.read (| state |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_revm_primitives_state_AccountStatus.
  
  Module Impl_core_default_Default_for_revm_primitives_state_AccountStatus.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountStatus".
    
    (*
        fn default() -> Self {
            Self::Loaded
        }
    *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic (M.read (| M.get_constant (| "revm_primitives::state::Loaded" |) |)))
      | _, _, _ => 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_primitives_state_AccountStatus.
  
  Module Impl_revm_primitives_state_Account.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::Account".
    
    (*
        pub fn new_not_existing() -> Self {
            Self {
                info: AccountInfo::default(),
                storage: HashMap::new(),
                status: AccountStatus::LoadedAsNotExisting,
            }
        }
    *)
    Definition new_not_existing (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_primitives::state::Account"
            [
              ("info",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::state::AccountInfo",
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("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.get_constant (| "revm_primitives::state::LoadedAsNotExisting" |) |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_not_existing :
      M.IsAssociatedFunction Self "new_not_existing" new_not_existing.
    
    (*
        pub fn mark_selfdestruct(&mut self) {
            self.status |= AccountStatus::SelfDestructed;
        }
    *)
    Definition mark_selfdestruct (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::BitOrAssign",
                    Ty.path "revm_primitives::state::AccountStatus",
                    [ Ty.path "revm_primitives::state::AccountStatus" ],
                    "bitor_assign",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "status"
                    |);
                    M.read (| M.get_constant (| "revm_primitives::state::SelfDestructed" |) |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_mark_selfdestruct :
      M.IsAssociatedFunction Self "mark_selfdestruct" mark_selfdestruct.
    
    (*
        pub fn unmark_selfdestruct(&mut self) {
            self.status -= AccountStatus::SelfDestructed;
        }
    *)
    Definition unmark_selfdestruct (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::SubAssign",
                    Ty.path "revm_primitives::state::AccountStatus",
                    [ Ty.path "revm_primitives::state::AccountStatus" ],
                    "sub_assign",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "status"
                    |);
                    M.read (| M.get_constant (| "revm_primitives::state::SelfDestructed" |) |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unmark_selfdestruct :
      M.IsAssociatedFunction Self "unmark_selfdestruct" unmark_selfdestruct.
    
    (*
        pub fn is_selfdestructed(&self) -> bool {
            self.status.contains(AccountStatus::SelfDestructed)
        }
    *)
    Definition is_selfdestructed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "revm_primitives::state::AccountStatus",
              "contains",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::Account",
                "status"
              |);
              M.read (| M.get_constant (| "revm_primitives::state::SelfDestructed" |) |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_selfdestructed :
      M.IsAssociatedFunction Self "is_selfdestructed" is_selfdestructed.
    
    (*
        pub fn mark_touch(&mut self) {
            self.status |= AccountStatus::Touched;
        }
    *)
    Definition mark_touch (ε : 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~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::BitOrAssign",
                    Ty.path "revm_primitives::state::AccountStatus",
                    [ Ty.path "revm_primitives::state::AccountStatus" ],
                    "bitor_assign",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "status"
                    |);
                    M.read (| M.get_constant (| "revm_primitives::state::Touched" |) |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_mark_touch : M.IsAssociatedFunction Self "mark_touch" mark_touch.
    
    (*
        pub fn unmark_touch(&mut self) {
            self.status -= AccountStatus::Touched;
        }
    *)
    Definition unmark_touch (ε : 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~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::SubAssign",
                    Ty.path "revm_primitives::state::AccountStatus",
                    [ Ty.path "revm_primitives::state::AccountStatus" ],
                    "sub_assign",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "status"
                    |);
                    M.read (| M.get_constant (| "revm_primitives::state::Touched" |) |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unmark_touch : M.IsAssociatedFunction Self "unmark_touch" unmark_touch.
    
    (*
        pub fn is_touched(&self) -> bool {
            self.status.contains(AccountStatus::Touched)
        }
    *)
    Definition is_touched (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "revm_primitives::state::AccountStatus",
              "contains",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::Account",
                "status"
              |);
              M.read (| M.get_constant (| "revm_primitives::state::Touched" |) |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_touched : M.IsAssociatedFunction Self "is_touched" is_touched.
    
    (*
        pub fn mark_created(&mut self) {
            self.status |= AccountStatus::Created;
        }
    *)
    Definition mark_created (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::bit::BitOrAssign",
                    Ty.path "revm_primitives::state::AccountStatus",
                    [ Ty.path "revm_primitives::state::AccountStatus" ],
                    "bitor_assign",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "status"
                    |);
                    M.read (| M.get_constant (| "revm_primitives::state::Created" |) |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_mark_created : M.IsAssociatedFunction Self "mark_created" mark_created.
    
    (*
        pub fn unmark_created(&mut self) {
            self.status -= AccountStatus::Created;
        }
    *)
    Definition unmark_created (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::ops::arith::SubAssign",
                    Ty.path "revm_primitives::state::AccountStatus",
                    [ Ty.path "revm_primitives::state::AccountStatus" ],
                    "sub_assign",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::Account",
                      "status"
                    |);
                    M.read (| M.get_constant (| "revm_primitives::state::Created" |) |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_unmark_created :
      M.IsAssociatedFunction Self "unmark_created" unmark_created.
    
    (*
        pub fn is_loaded_as_not_existing(&self) -> bool {
            self.status.contains(AccountStatus::LoadedAsNotExisting)
        }
    *)
    Definition is_loaded_as_not_existing
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "revm_primitives::state::AccountStatus",
              "contains",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::Account",
                "status"
              |);
              M.read (| M.get_constant (| "revm_primitives::state::LoadedAsNotExisting" |) |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_loaded_as_not_existing :
      M.IsAssociatedFunction Self "is_loaded_as_not_existing" is_loaded_as_not_existing.
    
    (*
        pub fn is_created(&self) -> bool {
            self.status.contains(AccountStatus::Created)
        }
    *)
    Definition is_created (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "revm_primitives::state::AccountStatus",
              "contains",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::Account",
                "status"
              |);
              M.read (| M.get_constant (| "revm_primitives::state::Created" |) |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_created : M.IsAssociatedFunction Self "is_created" is_created.
    
    (*
        pub fn is_empty(&self) -> bool {
            self.info.is_empty()
        }
    *)
    Definition is_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "revm_primitives::state::AccountInfo",
              "is_empty",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::Account",
                "info"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_empty : M.IsAssociatedFunction Self "is_empty" is_empty.
    
    (*
        pub fn changed_storage_slots(&self) -> impl Iterator<Item = (&U256, &StorageSlot)> {
            self.storage.iter().filter(|(_, slot)| slot.is_changed())
        }
    *)
    Definition changed_storage_slots (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::iter::traits::iterator::Iterator",
              Ty.apply
                (Ty.path "std::collections::hash::map::Iter")
                []
                [
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [];
                  Ty.path "revm_primitives::state::StorageSlot"
                ],
              [],
              "filter",
              [
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [
                            Ty.tuple
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ];
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.path "revm_primitives::state::StorageSlot" ]
                              ]
                          ]
                      ]
                  ]
                  (Ty.path "bool")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "std::collections::hash::map::HashMap")
                    []
                    [
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [];
                      Ty.path "revm_primitives::state::StorageSlot";
                      Ty.path "std::hash::random::RandomState"
                    ],
                  "iter",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::state::Account",
                    "storage"
                  |)
                ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ := M.read (| γ |) in
                                let γ1_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                                let γ1_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                                let slot := M.alloc (| γ1_1 |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "revm_primitives::state::StorageSlot",
                                    "is_changed",
                                    []
                                  |),
                                  [ M.read (| M.read (| slot |) |) ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_changed_storage_slots :
      M.IsAssociatedFunction Self "changed_storage_slots" changed_storage_slots.
  End Impl_revm_primitives_state_Account.
  
  Module Impl_core_convert_From_revm_primitives_state_AccountInfo_for_revm_primitives_state_Account.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::Account".
    
    (*
        fn from(info: AccountInfo) -> Self {
            Self {
                info,
                storage: HashMap::new(),
                status: AccountStatus::Loaded,
            }
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ info ] =>
        ltac:(M.monadic
          (let info := M.alloc (| info |) in
          Value.StructRecord
            "revm_primitives::state::Account"
            [
              ("info", M.read (| 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.get_constant (| "revm_primitives::state::Loaded" |) |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *) [ (* T *) Ty.path "revm_primitives::state::AccountInfo" ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_revm_primitives_state_AccountInfo_for_revm_primitives_state_Account.
  
  (* StructRecord
    {
      name := "StorageSlot";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("previous_or_original_value",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("present_value",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              [])
        ];
    } *)
  
  Module Impl_core_fmt_Debug_for_revm_primitives_state_StorageSlot.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::StorageSlot".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field2_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "StorageSlot" |);
              M.read (| Value.String "previous_or_original_value" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::StorageSlot",
                "previous_or_original_value"
              |);
              M.read (| Value.String "present_value" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::state::StorageSlot",
                  "present_value"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_primitives_state_StorageSlot.
  
  Module Impl_core_clone_Clone_for_revm_primitives_state_StorageSlot.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::StorageSlot".
    
    (* 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_primitives::state::StorageSlot"
            [
              ("previous_or_original_value",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::StorageSlot",
                      "previous_or_original_value"
                    |)
                  ]
                |));
              ("present_value",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::StorageSlot",
                      "present_value"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_primitives_state_StorageSlot.
  
  Module Impl_core_default_Default_for_revm_primitives_state_StorageSlot.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::StorageSlot".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_primitives::state::StorageSlot"
            [
              ("previous_or_original_value",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("present_value",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    [],
                    "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_primitives_state_StorageSlot.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_state_StorageSlot.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::StorageSlot".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_state_StorageSlot.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_state_StorageSlot.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::StorageSlot".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply
                  (Ty.path "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.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::state::StorageSlot",
                  "previous_or_original_value"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "revm_primitives::state::StorageSlot",
                  "previous_or_original_value"
                |)
              ]
            |),
            ltac:(M.monadic
              (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.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::state::StorageSlot",
                    "present_value"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::state::StorageSlot",
                    "present_value"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_primitives_state_StorageSlot.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_state_StorageSlot.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::StorageSlot".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_revm_primitives_state_StorageSlot.
  
  Module Impl_core_hash_Hash_for_revm_primitives_state_StorageSlot.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::StorageSlot".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    [],
                    "hash",
                    [ __H ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::StorageSlot",
                      "previous_or_original_value"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::hash::Hash",
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [],
                  [],
                  "hash",
                  [ __H ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::state::StorageSlot",
                    "present_value"
                  |);
                  M.read (| state |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_revm_primitives_state_StorageSlot.
  
  Module Impl_revm_primitives_state_StorageSlot.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::StorageSlot".
    
    (*
        pub fn new(original: U256) -> Self {
            Self {
                previous_or_original_value: original,
                present_value: original,
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ original ] =>
        ltac:(M.monadic
          (let original := M.alloc (| original |) in
          Value.StructRecord
            "revm_primitives::state::StorageSlot"
            [
              ("previous_or_original_value", M.read (| original |));
              ("present_value", M.read (| original |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn new_changed(previous_or_original_value: U256, present_value: U256) -> Self {
            Self {
                previous_or_original_value,
                present_value,
            }
        }
    *)
    Definition new_changed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ previous_or_original_value; present_value ] =>
        ltac:(M.monadic
          (let previous_or_original_value := M.alloc (| previous_or_original_value |) in
          let present_value := M.alloc (| present_value |) in
          Value.StructRecord
            "revm_primitives::state::StorageSlot"
            [
              ("previous_or_original_value", M.read (| previous_or_original_value |));
              ("present_value", M.read (| present_value |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_changed : M.IsAssociatedFunction Self "new_changed" new_changed.
    
    (*
        pub fn is_changed(&self) -> bool {
            self.previous_or_original_value != self.present_value
        }
    *)
    Definition is_changed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.apply
                (Ty.path "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 ]
                  []
              ],
              "ne",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::StorageSlot",
                "previous_or_original_value"
              |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::StorageSlot",
                "present_value"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_changed : M.IsAssociatedFunction Self "is_changed" is_changed.
    
    (*
        pub fn original_value(&self) -> U256 {
            self.previous_or_original_value
        }
    *)
    Definition original_value (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_primitives::state::StorageSlot",
              "previous_or_original_value"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_original_value :
      M.IsAssociatedFunction Self "original_value" original_value.
    
    (*
        pub fn present_value(&self) -> U256 {
            self.present_value
        }
    *)
    Definition present_value (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_primitives::state::StorageSlot",
              "present_value"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_present_value :
      M.IsAssociatedFunction Self "present_value" present_value.
  End Impl_revm_primitives_state_StorageSlot.
  
  (* StructRecord
    {
      name := "AccountInfo";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("balance",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("nonce", Ty.path "u64");
          ("code_hash",
            Ty.apply
              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
              [ Value.Integer IntegerKind.Usize 32 ]
              []);
          ("code",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.path "revm_primitives::bytecode::Bytecode" ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_state_AccountInfo.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountInfo".
    
    (* 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_primitives::state::AccountInfo"
            [
              ("balance",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::AccountInfo",
                      "balance"
                    |)
                  ]
                |));
              ("nonce",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Ty.path "u64", [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::AccountInfo",
                      "nonce"
                    |)
                  ]
                |));
              ("code_hash",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::AccountInfo",
                      "code_hash"
                    |)
                  ]
                |));
              ("code",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "revm_primitives::bytecode::Bytecode" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::AccountInfo",
                      "code"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_primitives_state_AccountInfo.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_state_AccountInfo.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountInfo".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "core::fmt::Formatter",
              "debug_struct_field4_finish",
              []
            |),
            [
              M.read (| f |);
              M.read (| Value.String "AccountInfo" |);
              M.read (| Value.String "balance" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::AccountInfo",
                "balance"
              |);
              M.read (| Value.String "nonce" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::AccountInfo",
                "nonce"
              |);
              M.read (| Value.String "code_hash" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::AccountInfo",
                "code_hash"
              |);
              M.read (| Value.String "code" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::state::AccountInfo",
                  "code"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_primitives_state_AccountInfo.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_state_AccountInfo.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountInfo".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              Value.DeclaredButUndefined,
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      Value.DeclaredButUndefined,
                                      [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
                                    |)))
                              ]
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_revm_primitives_state_AccountInfo.
  
  Module Impl_core_default_Default_for_revm_primitives_state_AccountInfo.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountInfo".
    
    (*
        fn default() -> Self {
            Self {
                balance: U256::ZERO,
                code_hash: KECCAK_EMPTY,
                code: Some(Bytecode::default()),
                nonce: 0,
            }
        }
    *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_primitives::state::AccountInfo"
            [
              ("balance", M.read (| M.get_constant (| "ruint::ZERO" |) |));
              ("code_hash",
                M.read (| M.get_constant (| "revm_primitives::utilities::KECCAK_EMPTY" |) |));
              ("code",
                Value.StructTuple
                  "core::option::Option::Some"
                  [
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.path "revm_primitives::bytecode::Bytecode",
                        [],
                        "default",
                        []
                      |),
                      []
                    |)
                  ]);
              ("nonce", Value.Integer IntegerKind.U64 0)
            ]))
      | _, _, _ => 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_primitives_state_AccountInfo.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_state_AccountInfo.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountInfo".
    
    (*
        fn eq(&self, other: &Self) -> bool {
            self.balance == other.balance
                && self.nonce == other.nonce
                && self.code_hash == other.code_hash
        }
    *)
    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 (|
              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.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::state::AccountInfo",
                    "balance"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::state::AccountInfo",
                    "balance"
                  |)
                ]
              |),
              ltac:(M.monadic
                (BinOp.eq (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::AccountInfo",
                      "nonce"
                    |)
                  |),
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::state::AccountInfo",
                      "nonce"
                    |)
                  |)
                |)))
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                    [ Value.Integer IntegerKind.Usize 32 ]
                    [],
                  [
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      []
                  ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::state::AccountInfo",
                    "code_hash"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::state::AccountInfo",
                    "code_hash"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_primitives_state_AccountInfo.
  
  Module Impl_core_hash_Hash_for_revm_primitives_state_AccountInfo.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountInfo".
    
    (*
        fn hash<H: Hasher>(&self, state: &mut H) {
            self.balance.hash(state);
            self.nonce.hash(state);
            self.code_hash.hash(state);
        }
    *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    [],
                    "hash",
                    [ H ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::AccountInfo",
                      "balance"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "u64", [], "hash", [ H ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::AccountInfo",
                      "nonce"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.apply
                      (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [],
                    [],
                    "hash",
                    [ H ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::state::AccountInfo",
                      "code_hash"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_revm_primitives_state_AccountInfo.
  
  Module Impl_revm_primitives_state_AccountInfo.
    Definition Self : Ty.t := Ty.path "revm_primitives::state::AccountInfo".
    
    (*
        pub fn new(balance: U256, nonce: u64, code_hash: B256, code: Bytecode) -> Self {
            Self {
                balance,
                nonce,
                code: Some(code),
                code_hash,
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ balance; nonce; code_hash; code ] =>
        ltac:(M.monadic
          (let balance := M.alloc (| balance |) in
          let nonce := M.alloc (| nonce |) in
          let code_hash := M.alloc (| code_hash |) in
          let code := M.alloc (| code |) in
          Value.StructRecord
            "revm_primitives::state::AccountInfo"
            [
              ("balance", M.read (| balance |));
              ("nonce", M.read (| nonce |));
              ("code", Value.StructTuple "core::option::Option::Some" [ M.read (| code |) ]);
              ("code_hash", M.read (| code_hash |))
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        pub fn without_code(mut self) -> Self {
            self.take_bytecode();
            self
        }
    *)
    Definition without_code (ε : 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~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "revm_primitives::state::AccountInfo",
                    "take_bytecode",
                    []
                  |),
                  [ self ]
                |)
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_without_code : M.IsAssociatedFunction Self "without_code" without_code.
    
    (*
        pub fn is_empty(&self) -> bool {
            let code_empty = self.is_empty_code_hash() || self.code_hash == B256::ZERO;
            code_empty && self.balance == U256::ZERO && self.nonce == 0
        }
    *)
    Definition is_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            let~ code_empty :=
              M.alloc (|
                LogicalOp.or (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "revm_primitives::state::AccountInfo",
                      "is_empty_code_hash",
                      []
                    |),
                    [ M.read (| self |) ]
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          [],
                        [
                          Ty.apply
                            (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            []
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_primitives::state::AccountInfo",
                          "code_hash"
                        |);
                        M.get_constant (| "alloy_primitives::bits::fixed::ZERO" |)
                      ]
                    |)))
                |)
              |) in
            M.alloc (|
              LogicalOp.and (|
                LogicalOp.and (|
                  M.read (| code_empty |),
                  ltac:(M.monadic
                    (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.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_primitives::state::AccountInfo",
                          "balance"
                        |);
                        M.get_constant (| "ruint::ZERO" |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (BinOp.eq (|
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::state::AccountInfo",
                        "nonce"
                      |)
                    |),
                    Value.Integer IntegerKind.U64 0
                  |)))
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_empty : M.IsAssociatedFunction Self "is_empty" is_empty.
    
    (*
        pub fn exists(&self) -> bool {
            !self.is_empty()
        }
    *)
    Definition exists_ (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          UnOp.not (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_primitives::state::AccountInfo",
                "is_empty",
                []
              |),
              [ M.read (| self |) ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_exists_ : M.IsAssociatedFunction Self "exists_" exists_.
    
    (*
        pub fn has_no_code_and_nonce(&self) -> bool {
            self.is_empty_code_hash() && self.nonce == 0
        }
    *)
    Definition has_no_code_and_nonce (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          LogicalOp.and (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_primitives::state::AccountInfo",
                "is_empty_code_hash",
                []
              |),
              [ M.read (| self |) ]
            |),
            ltac:(M.monadic
              (BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::state::AccountInfo",
                    "nonce"
                  |)
                |),
                Value.Integer IntegerKind.U64 0
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_has_no_code_and_nonce :
      M.IsAssociatedFunction Self "has_no_code_and_nonce" has_no_code_and_nonce.
    
    (*
        pub fn code_hash(&self) -> B256 {
            self.code_hash
        }
    *)
    Definition code_hash (ε : 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.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_primitives::state::AccountInfo",
              "code_hash"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_code_hash : M.IsAssociatedFunction Self "code_hash" code_hash.
    
    (*
        pub fn is_empty_code_hash(&self) -> bool {
            self.code_hash == KECCAK_EMPTY
        }
    *)
    Definition is_empty_code_hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_trait_method (|
              "core::cmp::PartialEq",
              Ty.apply
                (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                [ Value.Integer IntegerKind.Usize 32 ]
                [],
              [
                Ty.apply
                  (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                  [ Value.Integer IntegerKind.Usize 32 ]
                  []
              ],
              "eq",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::AccountInfo",
                "code_hash"
              |);
              M.get_constant (| "revm_primitives::utilities::KECCAK_EMPTY" |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_empty_code_hash :
      M.IsAssociatedFunction Self "is_empty_code_hash" is_empty_code_hash.
    
    (*
        pub fn take_bytecode(&mut self) -> Option<Bytecode> {
            self.code.take()
        }
    *)
    Definition take_bytecode (ε : 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.path "revm_primitives::bytecode::Bytecode" ],
              "take",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::state::AccountInfo",
                "code"
              |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_take_bytecode :
      M.IsAssociatedFunction Self "take_bytecode" take_bytecode.
    
    (*
        pub fn from_balance(balance: U256) -> Self {
            AccountInfo {
                balance,
                ..Default::default()
            }
        }
    *)
    Definition from_balance (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ balance ] =>
        ltac:(M.monadic
          (let balance := M.alloc (| balance |) in
          M.struct_record_update
            (M.call_closure (|
              M.get_trait_method (|
                "core::default::Default",
                Ty.path "revm_primitives::state::AccountInfo",
                [],
                "default",
                []
              |),
              []
            |))
            [ ("balance", M.read (| balance |)) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_from_balance : M.IsAssociatedFunction Self "from_balance" from_balance.
  End Impl_revm_primitives_state_AccountInfo.
End state.
