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

Module env.
  Module handler_cfg.
    (* StructRecord
      {
        name := "HandlerCfg";
        const_params := [];
        ty_params := [];
        fields := [ ("spec_id", Ty.path "revm_primitives::specification::SpecId") ];
      } *)
    
    Module Impl_core_clone_Clone_for_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      (* 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_env_handler_cfg_HandlerCfg.
    
    Module Impl_core_marker_Copy_for_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::Copy"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_Copy_for_revm_primitives_env_handler_cfg_HandlerCfg.
    
    Module Impl_core_fmt_Debug_for_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      (* 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_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "HandlerCfg" |);
                M.read (| Value.String "spec_id" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::handler_cfg::HandlerCfg",
                    "spec_id"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_env_handler_cfg_HandlerCfg.
    
    Module Impl_core_cmp_Eq_for_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      (* 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_env_handler_cfg_HandlerCfg.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_handler_cfg_HandlerCfg.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      (* 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::specification::SpecId",
                [ Ty.path "revm_primitives::specification::SpecId" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::handler_cfg::HandlerCfg",
                  "spec_id"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "revm_primitives::env::handler_cfg::HandlerCfg",
                  "spec_id"
                |)
              ]
            |)))
        | _, _, _ => 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_env_handler_cfg_HandlerCfg.
    
    Module Impl_core_hash_Hash_for_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      (* 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::specification::SpecId",
                [],
                "hash",
                [ __H ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::handler_cfg::HandlerCfg",
                  "spec_id"
                |);
                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_env_handler_cfg_HandlerCfg.
    
    Module Impl_core_default_Default_for_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      (*
          fn default() -> Self {
              Self::new(SpecId::default())
          }
      *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                "new",
                []
              |),
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::specification::SpecId",
                    [],
                    "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_env_handler_cfg_HandlerCfg.
    
    Module Impl_revm_primitives_env_handler_cfg_HandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::HandlerCfg".
      
      (*
          pub fn new(spec_id: SpecId) -> Self {
              cfg_if::cfg_if! {
                  if #[cfg(all(feature = "optimism-default-handler",
                      not(feature = "negate-optimism-default-handler")))] {
                          let is_optimism = true;
                  } else if #[cfg(feature = "optimism")] {
                      let is_optimism = false;
                  }
              }
              Self {
                  spec_id,
                  #[cfg(feature = "optimism")]
                  is_optimism,
              }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ spec_id ] =>
          ltac:(M.monadic
            (let spec_id := M.alloc (| spec_id |) in
            Value.StructRecord
              "revm_primitives::env::handler_cfg::HandlerCfg"
              [ ("spec_id", M.read (| spec_id |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub fn is_optimism(&self) -> bool {
              cfg_if::cfg_if! {
                  if #[cfg(feature = "optimism")] {
                      self.is_optimism
                  } else {
                      false
                  }
              }
          }
      *)
      Definition is_optimism (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            Value.Bool false))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_is_optimism : M.IsAssociatedFunction Self "is_optimism" is_optimism.
    End Impl_revm_primitives_env_handler_cfg_HandlerCfg.
    
    (* StructRecord
      {
        name := "CfgEnvWithHandlerCfg";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("cfg_env", Ty.path "revm_primitives::env::CfgEnv");
            ("handler_cfg", Ty.path "revm_primitives::env::handler_cfg::HandlerCfg")
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg".
      
      (* 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::env::handler_cfg::CfgEnvWithHandlerCfg"
              [
                ("cfg_env",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm_primitives::env::CfgEnv",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                        "cfg_env"
                      |)
                    ]
                  |));
                ("handler_cfg",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                        "handler_cfg"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_env_handler_cfg_CfgEnvWithHandlerCfg.
    
    Module Impl_core_fmt_Debug_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg".
      
      (* 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 "CfgEnvWithHandlerCfg" |);
                M.read (| Value.String "cfg_env" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                  "cfg_env"
                |);
                M.read (| Value.String "handler_cfg" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                    "handler_cfg"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_env_handler_cfg_CfgEnvWithHandlerCfg.
    
    Module Impl_core_cmp_Eq_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg".
      
      (* 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.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_env_handler_cfg_CfgEnvWithHandlerCfg.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg".
      
      (* 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.path "revm_primitives::env::CfgEnv",
                  [ Ty.path "revm_primitives::env::CfgEnv" ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                    "cfg_env"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                    "cfg_env"
                  |)
                ]
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                    [ Ty.path "revm_primitives::env::handler_cfg::HandlerCfg" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                      "handler_cfg"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                      "handler_cfg"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => 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_env_handler_cfg_CfgEnvWithHandlerCfg.
    
    Module Impl_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg".
      
      (*
          pub fn new(cfg_env: CfgEnv, handler_cfg: HandlerCfg) -> Self {
              Self {
                  cfg_env,
                  handler_cfg,
              }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ cfg_env; handler_cfg ] =>
          ltac:(M.monadic
            (let cfg_env := M.alloc (| cfg_env |) in
            let handler_cfg := M.alloc (| handler_cfg |) in
            Value.StructRecord
              "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg"
              [ ("cfg_env", M.read (| cfg_env |)); ("handler_cfg", M.read (| handler_cfg |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub fn new_with_spec_id(cfg_env: CfgEnv, spec_id: SpecId) -> Self {
              Self::new(cfg_env, HandlerCfg::new(spec_id))
          }
      *)
      Definition new_with_spec_id (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ cfg_env; spec_id ] =>
          ltac:(M.monadic
            (let cfg_env := M.alloc (| cfg_env |) in
            let spec_id := M.alloc (| spec_id |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                "new",
                []
              |),
              [
                M.read (| cfg_env |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                    "new",
                    []
                  |),
                  [ M.read (| spec_id |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_with_spec_id :
        M.IsAssociatedFunction Self "new_with_spec_id" new_with_spec_id.
    End Impl_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
    
    Module Impl_core_ops_deref_DerefMut_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg".
      
      (*
          fn deref_mut(&mut self) -> &mut Self::Target {
              &mut self.cfg_env
          }
      *)
      Definition deref_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
              "cfg_env"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::deref::DerefMut"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deref_mut", InstanceField.Method deref_mut) ].
    End Impl_core_ops_deref_DerefMut_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
    
    Module Impl_core_ops_deref_Deref_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg".
      
      (*     type Target = CfgEnv; *)
      Definition _Target : Ty.t := Ty.path "revm_primitives::env::CfgEnv".
      
      (*
          fn deref(&self) -> &Self::Target {
              &self.cfg_env
          }
      *)
      Definition deref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
              "cfg_env"
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::deref::Deref"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Target", InstanceField.Ty _Target); ("deref", InstanceField.Method deref) ].
    End Impl_core_ops_deref_Deref_for_revm_primitives_env_handler_cfg_CfgEnvWithHandlerCfg.
    
    (* StructRecord
      {
        name := "EnvWithHandlerCfg";
        const_params := [];
        ty_params := [];
        fields :=
          [
            ("env",
              Ty.apply
                (Ty.path "alloc::boxed::Box")
                []
                [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ]);
            ("handler_cfg", Ty.path "revm_primitives::env::handler_cfg::HandlerCfg")
          ];
      } *)
    
    Module Impl_core_clone_Clone_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      (* 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::env::handler_cfg::EnvWithHandlerCfg"
              [
                ("env",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.apply
                        (Ty.path "alloc::boxed::Box")
                        []
                        [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ],
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                        "env"
                      |)
                    ]
                  |));
                ("handler_cfg",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::clone::Clone",
                      Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                      [],
                      "clone",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                        "handler_cfg"
                      |)
                    ]
                  |))
              ]))
        | _, _, _ => 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_env_handler_cfg_EnvWithHandlerCfg.
    
    Module Impl_core_fmt_Debug_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      (* 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 "EnvWithHandlerCfg" |);
                M.read (| Value.String "env" |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                  "env"
                |);
                M.read (| Value.String "handler_cfg" |);
                M.alloc (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                    "handler_cfg"
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_env_handler_cfg_EnvWithHandlerCfg.
    
    Module Impl_core_default_Default_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      (* Default *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructRecord
              "revm_primitives::env::handler_cfg::EnvWithHandlerCfg"
              [
                ("env",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.apply
                        (Ty.path "alloc::boxed::Box")
                        []
                        [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ],
                      [],
                      "default",
                      []
                    |),
                    []
                  |));
                ("handler_cfg",
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::default::Default",
                      Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                      [],
                      "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_env_handler_cfg_EnvWithHandlerCfg.
    
    Module Impl_core_cmp_Eq_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      (* 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.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_env_handler_cfg_EnvWithHandlerCfg.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      (* 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 "alloc::boxed::Box")
                    []
                    [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ],
                  [
                    Ty.apply
                      (Ty.path "alloc::boxed::Box")
                      []
                      [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                    "env"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                    "env"
                  |)
                ]
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                    [ Ty.path "revm_primitives::env::handler_cfg::HandlerCfg" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                      "handler_cfg"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                      "handler_cfg"
                    |)
                  ]
                |)))
            |)))
        | _, _, _ => 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_env_handler_cfg_EnvWithHandlerCfg.
    
    Module Impl_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      (*
          pub fn new(env: Box<Env>, handler_cfg: HandlerCfg) -> Self {
              Self { env, handler_cfg }
          }
      *)
      Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ env; handler_cfg ] =>
          ltac:(M.monadic
            (let env := M.alloc (| env |) in
            let handler_cfg := M.alloc (| handler_cfg |) in
            Value.StructRecord
              "revm_primitives::env::handler_cfg::EnvWithHandlerCfg"
              [ ("env", M.read (| env |)); ("handler_cfg", M.read (| handler_cfg |)) ]))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
      
      (*
          pub fn new_with_spec_id(env: Box<Env>, spec_id: SpecId) -> Self {
              Self::new(env, HandlerCfg::new(spec_id))
          }
      *)
      Definition new_with_spec_id (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ env; spec_id ] =>
          ltac:(M.monadic
            (let env := M.alloc (| env |) in
            let spec_id := M.alloc (| spec_id |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                "new",
                []
              |),
              [
                M.read (| env |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "revm_primitives::env::handler_cfg::HandlerCfg",
                    "new",
                    []
                  |),
                  [ M.read (| spec_id |) ]
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_with_spec_id :
        M.IsAssociatedFunction Self "new_with_spec_id" new_with_spec_id.
      
      (*
          pub fn new_with_cfg_env(cfg: CfgEnvWithHandlerCfg, block: BlockEnv, tx: TxEnv) -> Self {
              Self::new(Env::boxed(cfg.cfg_env, block, tx), cfg.handler_cfg)
          }
      *)
      Definition new_with_cfg_env (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ cfg; block; tx ] =>
          ltac:(M.monadic
            (let cfg := M.alloc (| cfg |) in
            let block := M.alloc (| block |) in
            let tx := M.alloc (| tx |) in
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                "new",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (| Ty.path "revm_primitives::env::Env", "boxed", [] |),
                  [
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        cfg,
                        "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                        "cfg_env"
                      |)
                    |);
                    M.read (| block |);
                    M.read (| tx |)
                  ]
                |);
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    cfg,
                    "revm_primitives::env::handler_cfg::CfgEnvWithHandlerCfg",
                    "handler_cfg"
                  |)
                |)
              ]
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_new_with_cfg_env :
        M.IsAssociatedFunction Self "new_with_cfg_env" new_with_cfg_env.
      
      (*
          pub const fn spec_id(&self) -> SpecId {
              self.handler_cfg.spec_id
          }
      *)
      Definition spec_id (ε : 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.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                  "handler_cfg"
                |),
                "revm_primitives::env::handler_cfg::HandlerCfg",
                "spec_id"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_spec_id : M.IsAssociatedFunction Self "spec_id" spec_id.
    End Impl_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
    
    Module Impl_core_ops_deref_DerefMut_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      (*
          fn deref_mut(&mut self) -> &mut Self::Target {
              &mut self.env
          }
      *)
      Definition deref_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                "env"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::deref::DerefMut"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deref_mut", InstanceField.Method deref_mut) ].
    End Impl_core_ops_deref_DerefMut_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
    
    Module Impl_core_ops_deref_Deref_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
      Definition Self : Ty.t := Ty.path "revm_primitives::env::handler_cfg::EnvWithHandlerCfg".
      
      (*     type Target = Env; *)
      Definition _Target : Ty.t := Ty.path "revm_primitives::env::Env".
      
      (*
          fn deref(&self) -> &Self::Target {
              &self.env
          }
      *)
      Definition deref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::env::handler_cfg::EnvWithHandlerCfg",
                "env"
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::deref::Deref"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Target", InstanceField.Ty _Target); ("deref", InstanceField.Method deref) ].
    End Impl_core_ops_deref_Deref_for_revm_primitives_env_handler_cfg_EnvWithHandlerCfg.
  End handler_cfg.
End env.
