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

Module env.
  (* StructRecord
    {
      name := "Env";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("cfg", Ty.path "revm_primitives::env::CfgEnv");
          ("block", Ty.path "revm_primitives::env::BlockEnv");
          ("tx", Ty.path "revm_primitives::env::TxEnv")
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_env_Env.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::Env".
    
    (* 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::Env"
            [
              ("cfg",
                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::Env",
                      "cfg"
                    |)
                  ]
                |));
              ("block",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "revm_primitives::env::BlockEnv",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::Env",
                      "block"
                    |)
                  ]
                |));
              ("tx",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "revm_primitives::env::TxEnv",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::Env",
                      "tx"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_Env.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_env_Env.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::Env".
    
    (* 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 "Env" |);
              M.read (| Value.String "cfg" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::env::Env",
                "cfg"
              |);
              M.read (| Value.String "block" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::env::Env",
                "block"
              |);
              M.read (| Value.String "tx" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::Env",
                  "tx"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_Env.
  
  Module Impl_core_default_Default_for_revm_primitives_env_Env.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::Env".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_primitives::env::Env"
            [
              ("cfg",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::env::CfgEnv",
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("block",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::env::BlockEnv",
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("tx",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::env::TxEnv",
                    [],
                    "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_Env.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_Env.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::Env".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_Env.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_env_Env.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::Env".
    
    (* 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::env::CfgEnv",
                  [ Ty.path "revm_primitives::env::CfgEnv" ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::Env",
                    "cfg"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::env::Env",
                    "cfg"
                  |)
                ]
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "revm_primitives::env::BlockEnv",
                    [ Ty.path "revm_primitives::env::BlockEnv" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::Env",
                      "block"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::env::Env",
                      "block"
                    |)
                  ]
                |)))
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.path "revm_primitives::env::TxEnv",
                  [ Ty.path "revm_primitives::env::TxEnv" ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::Env",
                    "tx"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::env::Env",
                    "tx"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_Env.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_env_Env.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::Env".
    
    (* 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_env_Env.
  
  Module Impl_revm_primitives_env_Env.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::Env".
    
    (*
        pub fn clear(&mut self) {
            *self = Self::default();
        }
    *)
    Definition clear (ε : 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.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::env::Env",
                    [],
                    "default",
                    []
                  |),
                  []
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_clear : M.IsAssociatedFunction Self "clear" clear.
    
    (*
        pub fn boxed(cfg: CfgEnv, block: BlockEnv, tx: TxEnv) -> Box<Self> {
            Box::new(Self { cfg, block, tx })
        }
    *)
    Definition boxed (ε : 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.apply
                (Ty.path "alloc::boxed::Box")
                []
                [ Ty.path "revm_primitives::env::Env"; Ty.path "alloc::alloc::Global" ],
              "new",
              []
            |),
            [
              Value.StructRecord
                "revm_primitives::env::Env"
                [ ("cfg", M.read (| cfg |)); ("block", M.read (| block |)); ("tx", M.read (| tx |))
                ]
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_boxed : M.IsAssociatedFunction Self "boxed" boxed.
    
    (*
        pub fn effective_gas_price(&self) -> U256 {
            if let Some(priority_fee) = self.tx.gas_priority_fee {
                min(self.tx.gas_price, self.block.basefee + priority_fee)
            } else {
                self.tx.gas_price
            }
        }
    *)
    Definition effective_gas_price (ε : 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 (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.SubPointer.get_struct_record_field (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_primitives::env::Env",
                          "tx"
                        |),
                        "revm_primitives::env::TxEnv",
                        "gas_priority_fee"
                      |) in
                    let γ0_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "core::option::Option::Some",
                        0
                      |) in
                    let priority_fee := M.copy (| γ0_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (|
                          "core::cmp::min",
                          [
                            Ty.apply
                              (Ty.path "ruint::Uint")
                              [
                                Value.Integer IntegerKind.Usize 256;
                                Value.Integer IntegerKind.Usize 4
                              ]
                              []
                          ]
                        |),
                        [
                          M.read (|
                            M.SubPointer.get_struct_record_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm_primitives::env::Env",
                                "tx"
                              |),
                              "revm_primitives::env::TxEnv",
                              "gas_price"
                            |)
                          |);
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::arith::Add",
                              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
                                  ]
                                  []
                              ],
                              "add",
                              []
                            |),
                            [
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm_primitives::env::Env",
                                    "block"
                                  |),
                                  "revm_primitives::env::BlockEnv",
                                  "basefee"
                                |)
                              |);
                              M.read (| priority_fee |)
                            ]
                          |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::Env",
                        "tx"
                      |),
                      "revm_primitives::env::TxEnv",
                      "gas_price"
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_effective_gas_price :
      M.IsAssociatedFunction Self "effective_gas_price" effective_gas_price.
    
    (*
        pub fn calc_data_fee(&self) -> Option<U256> {
            self.block.get_blob_gasprice().map(|blob_gas_price| {
                U256::from(blob_gas_price).saturating_mul(U256::from(self.tx.get_total_blob_gas()))
            })
        }
    *)
    Definition calc_data_fee (ε : 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 "u128" ],
              "map",
              [
                Ty.apply
                  (Ty.path "ruint::Uint")
                  [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                  [];
                Ty.function
                  [ Ty.tuple [ Ty.path "u128" ] ]
                  (Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [])
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "revm_primitives::env::BlockEnv",
                  "get_blob_gasprice",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::Env",
                    "block"
                  |)
                ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let blob_gas_price := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "saturating_mul",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        "from",
                                        [ Ty.path "u128" ]
                                      |),
                                      [ M.read (| blob_gas_price |) ]
                                    |);
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        "from",
                                        [ Ty.path "u64" ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_primitives::env::TxEnv",
                                            "get_total_blob_gas",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm_primitives::env::Env",
                                              "tx"
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_calc_data_fee :
      M.IsAssociatedFunction Self "calc_data_fee" calc_data_fee.
    
    (*
        pub fn calc_max_data_fee(&self) -> Option<U256> {
            self.tx.max_fee_per_blob_gas.map(|max_fee_per_blob_gas| {
                max_fee_per_blob_gas.saturating_mul(U256::from(self.tx.get_total_blob_gas()))
            })
        }
    *)
    Definition calc_max_data_fee (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    []
                ],
              "map",
              [
                Ty.apply
                  (Ty.path "ruint::Uint")
                  [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                  [];
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "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 ]
                    [])
              ]
            |),
            [
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::Env",
                    "tx"
                  |),
                  "revm_primitives::env::TxEnv",
                  "max_fee_per_blob_gas"
                |)
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let max_fee_per_blob_gas := M.copy (| γ |) in
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "saturating_mul",
                                    []
                                  |),
                                  [
                                    M.read (| max_fee_per_blob_gas |);
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        "from",
                                        [ Ty.path "u64" ]
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_primitives::env::TxEnv",
                                            "get_total_blob_gas",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm_primitives::env::Env",
                                              "tx"
                                            |)
                                          ]
                                        |)
                                      ]
                                    |)
                                  ]
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_calc_max_data_fee :
      M.IsAssociatedFunction Self "calc_max_data_fee" calc_max_data_fee.
    
    (*
        pub fn validate_block_env<SPEC: Spec>(&self) -> Result<(), InvalidHeader> {
            // `prevrandao` is required for the merge
            if SPEC::enabled(SpecId::MERGE) && self.block.prevrandao.is_none() {
                return Err(InvalidHeader::PrevrandaoNotSet);
            }
            // `excess_blob_gas` is required for Cancun
            if SPEC::enabled(SpecId::CANCUN) && self.block.blob_excess_gas_and_price.is_none() {
                return Err(InvalidHeader::ExcessBlobGasNotSet);
            }
            Ok(())
        }
    *)
    Definition validate_block_env (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ SPEC ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "revm_primitives::specification::Spec",
                                      SPEC,
                                      [],
                                      "enabled",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::MERGE"
                                        []
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                              [ Value.Integer IntegerKind.Usize 32 ]
                                              []
                                          ],
                                        "is_none",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_primitives::env::Env",
                                            "block"
                                          |),
                                          "revm_primitives::env::BlockEnv",
                                          "prevrandao"
                                        |)
                                      ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::result::InvalidHeader::PrevrandaoNotSet"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "revm_primitives::specification::Spec",
                                      SPEC,
                                      [],
                                      "enabled",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::CANCUN"
                                        []
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ],
                                        "is_none",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_primitives::env::Env",
                                            "block"
                                          |),
                                          "revm_primitives::env::BlockEnv",
                                          "blob_excess_gas_and_price"
                                        |)
                                      ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::result::InvalidHeader::ExcessBlobGasNotSet"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_validate_block_env :
      M.IsAssociatedFunction Self "validate_block_env" validate_block_env.
    
    (*
        pub fn validate_tx<SPEC: Spec>(&self) -> Result<(), InvalidTransaction> {
            // BASEFEE tx check
            if SPEC::enabled(SpecId::LONDON) {
                if let Some(priority_fee) = self.tx.gas_priority_fee {
                    if priority_fee > self.tx.gas_price {
                        // or gas_max_fee for eip1559
                        return Err(InvalidTransaction::PriorityFeeGreaterThanMaxFee);
                    }
                }
    
                // check minimal cost against basefee
                if !self.cfg.is_base_fee_check_disabled()
                    && self.effective_gas_price() < self.block.basefee
                {
                    return Err(InvalidTransaction::GasPriceLessThanBasefee);
                }
            }
    
            // Check if gas_limit is more than block_gas_limit
            if !self.cfg.is_block_gas_limit_disabled()
                && U256::from(self.tx.gas_limit) > self.block.gas_limit
            {
                return Err(InvalidTransaction::CallerGasLimitMoreThanBlock);
            }
    
            // EIP-3860: Limit and meter initcode
            if SPEC::enabled(SpecId::SHANGHAI) && self.tx.transact_to.is_create() {
                let max_initcode_size = self
                    .cfg
                    .limit_contract_code_size
                    .map(|limit| limit.saturating_mul(2))
                    .unwrap_or(MAX_INITCODE_SIZE);
                if self.tx.data.len() > max_initcode_size {
                    return Err(InvalidTransaction::CreateInitCodeSizeLimit);
                }
            }
    
            // Check if the transaction's chain id is correct
            if let Some(tx_chain_id) = self.tx.chain_id {
                if tx_chain_id != self.cfg.chain_id {
                    return Err(InvalidTransaction::InvalidChainId);
                }
            }
    
            // Check that access list is empty for transactions before BERLIN
            if !SPEC::enabled(SpecId::BERLIN) && !self.tx.access_list.is_empty() {
                return Err(InvalidTransaction::AccessListNotSupported);
            }
    
            // - For CANCUN and later, check that the gas price is not more than the tx max
            // - For before CANCUN, check that `blob_hashes` and `max_fee_per_blob_gas` are empty / not set
            if SPEC::enabled(SpecId::CANCUN) {
                // Presence of max_fee_per_blob_gas means that this is blob transaction.
                if let Some(max) = self.tx.max_fee_per_blob_gas {
                    // ensure that the user was willing to at least pay the current blob gasprice
                    let price = self.block.get_blob_gasprice().expect("already checked");
                    if U256::from(price) > max {
                        return Err(InvalidTransaction::BlobGasPriceGreaterThanMax);
                    }
    
                    // there must be at least one blob
                    if self.tx.blob_hashes.is_empty() {
                        return Err(InvalidTransaction::EmptyBlobs);
                    }
    
                    // The field `to` deviates slightly from the semantics with the exception
                    // that it MUST NOT be nil and therefore must always represent
                    // a 20-byte address. This means that blob transactions cannot
                    // have the form of a create transaction.
                    if self.tx.transact_to.is_create() {
                        return Err(InvalidTransaction::BlobCreateTransaction);
                    }
    
                    // all versioned blob hashes must start with VERSIONED_HASH_VERSION_KZG
                    for blob in self.tx.blob_hashes.iter() {
                        if blob[0] != VERSIONED_HASH_VERSION_KZG {
                            return Err(InvalidTransaction::BlobVersionNotSupported);
                        }
                    }
    
                    // ensure the total blob gas spent is at most equal to the limit
                    // assert blob_gas_used <= MAX_BLOB_GAS_PER_BLOCK
                    if self.tx.blob_hashes.len() > MAX_BLOB_NUMBER_PER_BLOCK as usize {
                        return Err(InvalidTransaction::TooManyBlobs);
                    }
                }
            } else {
                if !self.tx.blob_hashes.is_empty() {
                    return Err(InvalidTransaction::BlobVersionedHashesNotSupported);
                }
                if self.tx.max_fee_per_blob_gas.is_some() {
                    return Err(InvalidTransaction::MaxFeePerBlobGasNotSupported);
                }
            }
    
            if SPEC::enabled(SpecId::PRAGUE) {
                if !self.tx.eof_initcodes.is_empty() {
                    // If initcode is set other fields must be empty
                    if !self.tx.blob_hashes.is_empty() {
                        return Err(InvalidTransaction::BlobVersionedHashesNotSupported);
                    }
                    // EOF Create tx extends EIP-1559 tx. It must have max_fee_per_blob_gas
                    if self.tx.max_fee_per_blob_gas.is_some() {
                        return Err(InvalidTransaction::MaxFeePerBlobGasNotSupported);
                    }
                    // EOF Create must have a to address
                    if matches!(self.tx.transact_to, TransactTo::Call(_)) {
                        return Err(InvalidTransaction::EofCrateShouldHaveToAddress);
                    }
                } else {
                    // If initcode is set check its bounds.
                    if self.tx.eof_initcodes.len() > 256 {
                        return Err(InvalidTransaction::EofInitcodesNumberLimit);
                    }
                    if self
                        .tx
                        .eof_initcodes_hashed
                        .iter()
                        .any(|(_, i)| i.len() >= MAX_INITCODE_SIZE)
                    {
                        return Err(InvalidTransaction::EofInitcodesSizeLimit);
                    }
                }
            } else {
                // Initcode set when not supported.
                if !self.tx.eof_initcodes.is_empty() {
                    return Err(InvalidTransaction::EofInitcodesNotSupported);
                }
            }
    
            Ok(())
        }
    *)
    Definition validate_tx (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ SPEC ], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "revm_primitives::specification::Spec",
                                    SPEC,
                                    [],
                                    "enabled",
                                    []
                                  |),
                                  [
                                    Value.StructTuple
                                      "revm_primitives::specification::SpecId::LONDON"
                                      []
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.SubPointer.get_struct_record_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm_primitives::env::Env",
                                          "tx"
                                        |),
                                        "revm_primitives::env::TxEnv",
                                        "gas_priority_fee"
                                      |) in
                                    let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::option::Option::Some",
                                        0
                                      |) in
                                    let priority_fee := M.copy (| γ0_0 |) in
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::cmp::PartialOrd",
                                                      Ty.apply
                                                        (Ty.path "ruint::Uint")
                                                        [
                                                          Value.Integer IntegerKind.Usize 256;
                                                          Value.Integer IntegerKind.Usize 4
                                                        ]
                                                        [],
                                                      [
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          []
                                                      ],
                                                      "gt",
                                                      []
                                                    |),
                                                    [
                                                      priority_fee;
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "revm_primitives::env::Env",
                                                          "tx"
                                                        |),
                                                        "revm_primitives::env::TxEnv",
                                                        "gas_price"
                                                      |)
                                                    ]
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::result::Result::Err"
                                                      [
                                                        Value.StructTuple
                                                          "revm_primitives::result::InvalidTransaction::PriorityFeeGreaterThanMaxFee"
                                                          []
                                                      ]
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        LogicalOp.and (|
                                          UnOp.not (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "revm_primitives::env::CfgEnv",
                                                "is_base_fee_check_disabled",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "revm_primitives::env::Env",
                                                  "cfg"
                                                |)
                                              ]
                                            |)
                                          |),
                                          ltac:(M.monadic
                                            (M.call_closure (|
                                              M.get_trait_method (|
                                                "core::cmp::PartialOrd",
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                [
                                                  Ty.apply
                                                    (Ty.path "ruint::Uint")
                                                    [
                                                      Value.Integer IntegerKind.Usize 256;
                                                      Value.Integer IntegerKind.Usize 4
                                                    ]
                                                    []
                                                ],
                                                "lt",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_primitives::env::Env",
                                                      "effective_gas_price",
                                                      []
                                                    |),
                                                    [ M.read (| self |) ]
                                                  |)
                                                |);
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "revm_primitives::env::Env",
                                                    "block"
                                                  |),
                                                  "revm_primitives::env::BlockEnv",
                                                  "basefee"
                                                |)
                                              ]
                                            |)))
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructTuple
                                                "revm_primitives::result::InvalidTransaction::GasPriceLessThanBasefee"
                                                []
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::env::CfgEnv",
                                        "is_block_gas_limit_disabled",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm_primitives::env::Env",
                                          "cfg"
                                        |)
                                      ]
                                    |)
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialOrd",
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            []
                                        ],
                                        "gt",
                                        []
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [],
                                              "from",
                                              [ Ty.path "u64" ]
                                            |),
                                            [
                                              M.read (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "revm_primitives::env::Env",
                                                    "tx"
                                                  |),
                                                  "revm_primitives::env::TxEnv",
                                                  "gas_limit"
                                                |)
                                              |)
                                            ]
                                          |)
                                        |);
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_primitives::env::Env",
                                            "block"
                                          |),
                                          "revm_primitives::env::BlockEnv",
                                          "gas_limit"
                                        |)
                                      ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::result::InvalidTransaction::CallerGasLimitMoreThanBlock"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "revm_primitives::specification::Spec",
                                      SPEC,
                                      [],
                                      "enabled",
                                      []
                                    |),
                                    [
                                      Value.StructTuple
                                        "revm_primitives::specification::SpecId::SHANGHAI"
                                        []
                                    ]
                                  |),
                                  ltac:(M.monadic
                                    (M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::env::TransactTo",
                                        "is_create",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_primitives::env::Env",
                                            "tx"
                                          |),
                                          "revm_primitives::env::TxEnv",
                                          "transact_to"
                                        |)
                                      ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ max_initcode_size :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                                  "unwrap_or",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "core::option::Option")
                                        []
                                        [ Ty.path "usize" ],
                                      "map",
                                      [
                                        Ty.path "usize";
                                        Ty.function
                                          [ Ty.tuple [ Ty.path "usize" ] ]
                                          (Ty.path "usize")
                                      ]
                                    |),
                                    [
                                      M.read (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_primitives::env::Env",
                                            "cfg"
                                          |),
                                          "revm_primitives::env::CfgEnv",
                                          "limit_contract_code_size"
                                        |)
                                      |);
                                      M.closure
                                        (fun γ =>
                                          ltac:(M.monadic
                                            match γ with
                                            | [ α0 ] =>
                                              ltac:(M.monadic
                                                (M.match_operator (|
                                                  M.alloc (| α0 |),
                                                  [
                                                    fun γ =>
                                                      ltac:(M.monadic
                                                        (let limit := M.copy (| γ |) in
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "usize",
                                                            "saturating_mul",
                                                            []
                                                          |),
                                                          [
                                                            M.read (| limit |);
                                                            Value.Integer IntegerKind.Usize 2
                                                          ]
                                                        |)))
                                                  ]
                                                |)))
                                            | _ => M.impossible "wrong number of arguments"
                                            end))
                                    ]
                                  |);
                                  M.read (|
                                    M.get_constant (|
                                      "revm_primitives::constants::MAX_INITCODE_SIZE"
                                    |)
                                  |)
                                ]
                              |)
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.gt (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "bytes::bytes::Bytes",
                                              "len",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::deref::Deref",
                                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                                  [],
                                                  "deref",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "revm_primitives::env::Env",
                                                      "tx"
                                                    |),
                                                    "revm_primitives::env::TxEnv",
                                                    "data"
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |),
                                          M.read (| max_initcode_size |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructTuple
                                                "revm_primitives::result::InvalidTransaction::CreateInitCodeSizeLimit"
                                                []
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm_primitives::env::Env",
                                "tx"
                              |),
                              "revm_primitives::env::TxEnv",
                              "chain_id"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let tx_chain_id := M.copy (| γ0_0 |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        BinOp.ne (|
                                          M.read (| tx_chain_id |),
                                          M.read (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "revm_primitives::env::Env",
                                                "cfg"
                                              |),
                                              "revm_primitives::env::CfgEnv",
                                              "chain_id"
                                            |)
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructTuple
                                                "revm_primitives::result::InvalidTransaction::InvalidChainId"
                                                []
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "revm_primitives::specification::Spec",
                                        SPEC,
                                        [],
                                        "enabled",
                                        []
                                      |),
                                      [
                                        Value.StructTuple
                                          "revm_primitives::specification::SpecId::BERLIN"
                                          []
                                      ]
                                    |)
                                  |),
                                  ltac:(M.monadic
                                    (UnOp.not (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [
                                              Ty.tuple
                                                [
                                                  Ty.path
                                                    "alloy_primitives::bits::address::Address";
                                                  Ty.apply
                                                    (Ty.path "alloc::vec::Vec")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path "ruint::Uint")
                                                        [
                                                          Value.Integer IntegerKind.Usize 256;
                                                          Value.Integer IntegerKind.Usize 4
                                                        ]
                                                        [];
                                                      Ty.path "alloc::alloc::Global"
                                                    ]
                                                ];
                                              Ty.path "alloc::alloc::Global"
                                            ],
                                          "is_empty",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm_primitives::env::Env",
                                              "tx"
                                            |),
                                            "revm_primitives::env::TxEnv",
                                            "access_list"
                                          |)
                                        ]
                                      |)
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::result::InvalidTransaction::AccessListNotSupported"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "revm_primitives::specification::Spec",
                                    SPEC,
                                    [],
                                    "enabled",
                                    []
                                  |),
                                  [
                                    Value.StructTuple
                                      "revm_primitives::specification::SpecId::CANCUN"
                                      []
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.SubPointer.get_struct_record_field (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm_primitives::env::Env",
                                        "tx"
                                      |),
                                      "revm_primitives::env::TxEnv",
                                      "max_fee_per_blob_gas"
                                    |) in
                                  let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let max := M.copy (| γ0_0 |) in
                                  let~ price :=
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply
                                            (Ty.path "core::option::Option")
                                            []
                                            [ Ty.path "u128" ],
                                          "expect",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "revm_primitives::env::BlockEnv",
                                              "get_blob_gasprice",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "revm_primitives::env::Env",
                                                "block"
                                              |)
                                            ]
                                          |);
                                          M.read (| Value.String "already checked" |)
                                        ]
                                      |)
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::cmp::PartialOrd",
                                                      Ty.apply
                                                        (Ty.path "ruint::Uint")
                                                        [
                                                          Value.Integer IntegerKind.Usize 256;
                                                          Value.Integer IntegerKind.Usize 4
                                                        ]
                                                        [],
                                                      [
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          []
                                                      ],
                                                      "gt",
                                                      []
                                                    |),
                                                    [
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.apply
                                                              (Ty.path "ruint::Uint")
                                                              [
                                                                Value.Integer IntegerKind.Usize 256;
                                                                Value.Integer IntegerKind.Usize 4
                                                              ]
                                                              [],
                                                            "from",
                                                            [ Ty.path "u128" ]
                                                          |),
                                                          [ M.read (| price |) ]
                                                        |)
                                                      |);
                                                      max
                                                    ]
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::result::Result::Err"
                                                      [
                                                        Value.StructTuple
                                                          "revm_primitives::result::InvalidTransaction::BlobGasPriceGreaterThanMax"
                                                          []
                                                      ]
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path
                                                              "alloy_primitives::bits::fixed::FixedBytes")
                                                            [ Value.Integer IntegerKind.Usize 32 ]
                                                            [];
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      "is_empty",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "revm_primitives::env::Env",
                                                          "tx"
                                                        |),
                                                        "revm_primitives::env::TxEnv",
                                                        "blob_hashes"
                                                      |)
                                                    ]
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::result::Result::Err"
                                                      [
                                                        Value.StructTuple
                                                          "revm_primitives::result::InvalidTransaction::EmptyBlobs"
                                                          []
                                                      ]
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.path "revm_primitives::env::TransactTo",
                                                      "is_create",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "revm_primitives::env::Env",
                                                          "tx"
                                                        |),
                                                        "revm_primitives::env::TxEnv",
                                                        "transact_to"
                                                      |)
                                                    ]
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::result::Result::Err"
                                                      [
                                                        Value.StructTuple
                                                          "revm_primitives::result::InvalidTransaction::BlobCreateTransaction"
                                                          []
                                                      ]
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  let~ _ :=
                                    M.use
                                      (M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::collect::IntoIterator",
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path
                                                      "alloy_primitives::bits::fixed::FixedBytes")
                                                    [ Value.Integer IntegerKind.Usize 32 ]
                                                    []
                                                ],
                                              [],
                                              "into_iter",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "slice")
                                                    []
                                                    [
                                                      Ty.apply
                                                        (Ty.path
                                                          "alloy_primitives::bits::fixed::FixedBytes")
                                                        [ Value.Integer IntegerKind.Usize 32 ]
                                                        []
                                                    ],
                                                  "iter",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::deref::Deref",
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path
                                                              "alloy_primitives::bits::fixed::FixedBytes")
                                                            [ Value.Integer IntegerKind.Usize 32 ]
                                                            [];
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      [],
                                                      "deref",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "revm_primitives::env::Env",
                                                          "tx"
                                                        |),
                                                        "revm_primitives::env::TxEnv",
                                                        "blob_hashes"
                                                      |)
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let iter := M.copy (| γ |) in
                                              M.loop (|
                                                ltac:(M.monadic
                                                  (let~ _ :=
                                                    M.match_operator (|
                                                      M.alloc (|
                                                        M.call_closure (|
                                                          M.get_trait_method (|
                                                            "core::iter::traits::iterator::Iterator",
                                                            Ty.apply
                                                              (Ty.path "core::slice::iter::Iter")
                                                              []
                                                              [
                                                                Ty.apply
                                                                  (Ty.path
                                                                    "alloy_primitives::bits::fixed::FixedBytes")
                                                                  [
                                                                    Value.Integer
                                                                      IntegerKind.Usize
                                                                      32
                                                                  ]
                                                                  []
                                                              ],
                                                            [],
                                                            "next",
                                                            []
                                                          |),
                                                          [ iter ]
                                                        |)
                                                      |),
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let _ :=
                                                              M.is_struct_tuple (|
                                                                γ,
                                                                "core::option::Option::None"
                                                              |) in
                                                            M.alloc (|
                                                              M.never_to_any (|
                                                                M.read (| M.break (||) |)
                                                              |)
                                                            |)));
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (let γ0_0 :=
                                                              M.SubPointer.get_struct_tuple_field (|
                                                                γ,
                                                                "core::option::Option::Some",
                                                                0
                                                              |) in
                                                            let blob := M.copy (| γ0_0 |) in
                                                            M.match_operator (|
                                                              M.alloc (| Value.Tuple [] |),
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (let γ :=
                                                                      M.use
                                                                        (M.alloc (|
                                                                          BinOp.ne (|
                                                                            M.read (|
                                                                              M.call_closure (|
                                                                                M.get_trait_method (|
                                                                                  "core::ops::index::Index",
                                                                                  Ty.apply
                                                                                    (Ty.path
                                                                                      "alloy_primitives::bits::fixed::FixedBytes")
                                                                                    [
                                                                                      Value.Integer
                                                                                        IntegerKind.Usize
                                                                                        32
                                                                                    ]
                                                                                    [],
                                                                                  [ Ty.path "usize"
                                                                                  ],
                                                                                  "index",
                                                                                  []
                                                                                |),
                                                                                [
                                                                                  M.read (| blob |);
                                                                                  Value.Integer
                                                                                    IntegerKind.Usize
                                                                                    0
                                                                                ]
                                                                              |)
                                                                            |),
                                                                            M.read (|
                                                                              M.get_constant (|
                                                                                "revm_primitives::constants::VERSIONED_HASH_VERSION_KZG"
                                                                              |)
                                                                            |)
                                                                          |)
                                                                        |)) in
                                                                    let _ :=
                                                                      M.is_constant_or_break_match (|
                                                                        M.read (| γ |),
                                                                        Value.Bool true
                                                                      |) in
                                                                    M.alloc (|
                                                                      M.never_to_any (|
                                                                        M.read (|
                                                                          M.return_ (|
                                                                            Value.StructTuple
                                                                              "core::result::Result::Err"
                                                                              [
                                                                                Value.StructTuple
                                                                                  "revm_primitives::result::InvalidTransaction::BlobVersionNotSupported"
                                                                                  []
                                                                              ]
                                                                          |)
                                                                        |)
                                                                      |)
                                                                    |)));
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.alloc (| Value.Tuple [] |)))
                                                              ]
                                                            |)))
                                                      ]
                                                    |) in
                                                  M.alloc (| Value.Tuple [] |)))
                                              |)))
                                        ]
                                      |)) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                BinOp.gt (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "alloc::vec::Vec")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path
                                                              "alloy_primitives::bits::fixed::FixedBytes")
                                                            [ Value.Integer IntegerKind.Usize 32 ]
                                                            [];
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      "len",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "revm_primitives::env::Env",
                                                          "tx"
                                                        |),
                                                        "revm_primitives::env::TxEnv",
                                                        "blob_hashes"
                                                      |)
                                                    ]
                                                  |),
                                                  M.rust_cast
                                                    (M.read (|
                                                      M.get_constant (|
                                                        "revm_primitives::constants::MAX_BLOB_NUMBER_PER_BLOCK"
                                                      |)
                                                    |))
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.return_ (|
                                                  Value.StructTuple
                                                    "core::result::Result::Err"
                                                    [
                                                      Value.StructTuple
                                                        "revm_primitives::result::InvalidTransaction::TooManyBlobs"
                                                        []
                                                    ]
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          UnOp.not (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "alloc::vec::Vec")
                                                  []
                                                  [
                                                    Ty.apply
                                                      (Ty.path
                                                        "alloy_primitives::bits::fixed::FixedBytes")
                                                      [ Value.Integer IntegerKind.Usize 32 ]
                                                      [];
                                                    Ty.path "alloc::alloc::Global"
                                                  ],
                                                "is_empty",
                                                []
                                              |),
                                              [
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "revm_primitives::env::Env",
                                                    "tx"
                                                  |),
                                                  "revm_primitives::env::TxEnv",
                                                  "blob_hashes"
                                                |)
                                              ]
                                            |)
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          M.return_ (|
                                            Value.StructTuple
                                              "core::result::Result::Err"
                                              [
                                                Value.StructTuple
                                                  "revm_primitives::result::InvalidTransaction::BlobVersionedHashesNotSupported"
                                                  []
                                              ]
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  []
                                              ],
                                            "is_some",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.read (| self |),
                                                "revm_primitives::env::Env",
                                                "tx"
                                              |),
                                              "revm_primitives::env::TxEnv",
                                              "max_fee_per_blob_gas"
                                            |)
                                          ]
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructTuple
                                                "revm_primitives::result::InvalidTransaction::MaxFeePerBlobGasNotSupported"
                                                []
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "revm_primitives::specification::Spec",
                                    SPEC,
                                    [],
                                    "enabled",
                                    []
                                  |),
                                  [
                                    Value.StructTuple
                                      "revm_primitives::specification::SpecId::PRAGUE"
                                      []
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.path "alloy_primitives::bytes_::Bytes";
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "is_empty",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "revm_primitives::env::Env",
                                                  "tx"
                                                |),
                                                "revm_primitives::env::TxEnv",
                                                "eof_initcodes"
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  UnOp.not (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "alloc::vec::Vec")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path
                                                                "alloy_primitives::bits::fixed::FixedBytes")
                                                              [ Value.Integer IntegerKind.Usize 32 ]
                                                              [];
                                                            Ty.path "alloc::alloc::Global"
                                                          ],
                                                        "is_empty",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| self |),
                                                            "revm_primitives::env::Env",
                                                            "tx"
                                                          |),
                                                          "revm_primitives::env::TxEnv",
                                                          "blob_hashes"
                                                        |)
                                                      ]
                                                    |)
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::result::Result::Err"
                                                      [
                                                        Value.StructTuple
                                                          "revm_primitives::result::InvalidTransaction::BlobVersionedHashesNotSupported"
                                                          []
                                                      ]
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "core::option::Option")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "ruint::Uint")
                                                            [
                                                              Value.Integer IntegerKind.Usize 256;
                                                              Value.Integer IntegerKind.Usize 4
                                                            ]
                                                            []
                                                        ],
                                                      "is_some",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.read (| self |),
                                                          "revm_primitives::env::Env",
                                                          "tx"
                                                        |),
                                                        "revm_primitives::env::TxEnv",
                                                        "max_fee_per_blob_gas"
                                                      |)
                                                    ]
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::result::Result::Err"
                                                      [
                                                        Value.StructTuple
                                                          "revm_primitives::result::InvalidTransaction::MaxFeePerBlobGasNotSupported"
                                                          []
                                                      ]
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.match_operator (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "revm_primitives::env::Env",
                                                    "tx"
                                                  |),
                                                  "revm_primitives::env::TxEnv",
                                                  "transact_to"
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "revm_primitives::env::TransactTo::Call",
                                                          0
                                                        |) in
                                                      M.alloc (| Value.Bool true |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (M.alloc (| Value.Bool false |)))
                                                ]
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.return_ (|
                                                  Value.StructTuple
                                                    "core::result::Result::Err"
                                                    [
                                                      Value.StructTuple
                                                        "revm_primitives::result::InvalidTransaction::EofCrateShouldHaveToAddress"
                                                        []
                                                    ]
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let~ _ :=
                                    M.match_operator (|
                                      M.alloc (| Value.Tuple [] |),
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (let γ :=
                                              M.use
                                                (M.alloc (|
                                                  BinOp.gt (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "alloc::vec::Vec")
                                                          []
                                                          [
                                                            Ty.path
                                                              "alloy_primitives::bytes_::Bytes";
                                                            Ty.path "alloc::alloc::Global"
                                                          ],
                                                        "len",
                                                        []
                                                      |),
                                                      [
                                                        M.SubPointer.get_struct_record_field (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.read (| self |),
                                                            "revm_primitives::env::Env",
                                                            "tx"
                                                          |),
                                                          "revm_primitives::env::TxEnv",
                                                          "eof_initcodes"
                                                        |)
                                                      ]
                                                    |),
                                                    Value.Integer IntegerKind.Usize 256
                                                  |)
                                                |)) in
                                            let _ :=
                                              M.is_constant_or_break_match (|
                                                M.read (| γ |),
                                                Value.Bool true
                                              |) in
                                            M.alloc (|
                                              M.never_to_any (|
                                                M.read (|
                                                  M.return_ (|
                                                    Value.StructTuple
                                                      "core::result::Result::Err"
                                                      [
                                                        Value.StructTuple
                                                          "revm_primitives::result::InvalidTransaction::EofInitcodesNumberLimit"
                                                          []
                                                      ]
                                                  |)
                                                |)
                                              |)
                                            |)));
                                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                      ]
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::iter::traits::iterator::Iterator",
                                                    Ty.apply
                                                      (Ty.path "std::collections::hash::map::Iter")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path
                                                            "alloy_primitives::bits::fixed::FixedBytes")
                                                          [ Value.Integer IntegerKind.Usize 32 ]
                                                          [];
                                                        Ty.path "alloy_primitives::bytes_::Bytes"
                                                      ],
                                                    [],
                                                    "any",
                                                    [
                                                      Ty.function
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "&")
                                                                    []
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path
                                                                          "alloy_primitives::bits::fixed::FixedBytes")
                                                                        [
                                                                          Value.Integer
                                                                            IntegerKind.Usize
                                                                            32
                                                                        ]
                                                                        []
                                                                    ];
                                                                  Ty.apply
                                                                    (Ty.path "&")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "alloy_primitives::bytes_::Bytes"
                                                                    ]
                                                                ]
                                                            ]
                                                        ]
                                                        (Ty.path "bool")
                                                    ]
                                                  |),
                                                  [
                                                    M.alloc (|
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path
                                                              "std::collections::hash::map::HashMap")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path
                                                                  "alloy_primitives::bits::fixed::FixedBytes")
                                                                [ Value.Integer IntegerKind.Usize 32
                                                                ]
                                                                [];
                                                              Ty.path
                                                                "alloy_primitives::bytes_::Bytes";
                                                              Ty.path
                                                                "std::hash::random::RandomState"
                                                            ],
                                                          "iter",
                                                          []
                                                        |),
                                                        [
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| self |),
                                                              "revm_primitives::env::Env",
                                                              "tx"
                                                            |),
                                                            "revm_primitives::env::TxEnv",
                                                            "eof_initcodes_hashed"
                                                          |)
                                                        ]
                                                      |)
                                                    |);
                                                    M.closure
                                                      (fun γ =>
                                                        ltac:(M.monadic
                                                          match γ with
                                                          | [ α0 ] =>
                                                            ltac:(M.monadic
                                                              (M.match_operator (|
                                                                M.alloc (| α0 |),
                                                                [
                                                                  fun γ =>
                                                                    ltac:(M.monadic
                                                                      (let γ0_0 :=
                                                                        M.SubPointer.get_tuple_field (|
                                                                          γ,
                                                                          0
                                                                        |) in
                                                                      let γ0_1 :=
                                                                        M.SubPointer.get_tuple_field (|
                                                                          γ,
                                                                          1
                                                                        |) in
                                                                      let i := M.copy (| γ0_1 |) in
                                                                      BinOp.ge (|
                                                                        M.call_closure (|
                                                                          M.get_associated_function (|
                                                                            Ty.path
                                                                              "bytes::bytes::Bytes",
                                                                            "len",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "core::ops::deref::Deref",
                                                                                Ty.path
                                                                                  "alloy_primitives::bytes_::Bytes",
                                                                                [],
                                                                                "deref",
                                                                                []
                                                                              |),
                                                                              [ M.read (| i |) ]
                                                                            |)
                                                                          ]
                                                                        |),
                                                                        M.read (|
                                                                          M.get_constant (|
                                                                            "revm_primitives::constants::MAX_INITCODE_SIZE"
                                                                          |)
                                                                        |)
                                                                      |)))
                                                                ]
                                                              |)))
                                                          | _ =>
                                                            M.impossible "wrong number of arguments"
                                                          end))
                                                  ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (|
                                              M.read (|
                                                M.return_ (|
                                                  Value.StructTuple
                                                    "core::result::Result::Err"
                                                    [
                                                      Value.StructTuple
                                                        "revm_primitives::result::InvalidTransaction::EofInitcodesSizeLimit"
                                                        []
                                                    ]
                                                |)
                                              |)
                                            |)
                                          |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        UnOp.not (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "alloc::vec::Vec")
                                                []
                                                [
                                                  Ty.path "alloy_primitives::bytes_::Bytes";
                                                  Ty.path "alloc::alloc::Global"
                                                ],
                                              "is_empty",
                                              []
                                            |),
                                            [
                                              M.SubPointer.get_struct_record_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "revm_primitives::env::Env",
                                                  "tx"
                                                |),
                                                "revm_primitives::env::TxEnv",
                                                "eof_initcodes"
                                              |)
                                            ]
                                          |)
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructTuple
                                                "revm_primitives::result::InvalidTransaction::EofInitcodesNotSupported"
                                                []
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_validate_tx : M.IsAssociatedFunction Self "validate_tx" validate_tx.
    
    (*
        pub fn validate_tx_against_state<SPEC: Spec>(
            &self,
            account: &mut Account,
        ) -> Result<(), InvalidTransaction> {
            // EIP-3607: Reject transactions from senders with deployed code
            // This EIP is introduced after london but there was no collision in past
            // so we can leave it enabled always
            if !self.cfg.is_eip3607_disabled() && account.info.code_hash != KECCAK_EMPTY {
                return Err(InvalidTransaction::RejectCallerWithCode);
            }
    
            // Check that the transaction's nonce is correct
            if let Some(tx) = self.tx.nonce {
                let state = account.info.nonce;
                match tx.cmp(&state) {
                    Ordering::Greater => {
                        return Err(InvalidTransaction::NonceTooHigh { tx, state });
                    }
                    Ordering::Less => {
                        return Err(InvalidTransaction::NonceTooLow { tx, state });
                    }
                    _ => {}
                }
            }
    
            let mut balance_check = U256::from(self.tx.gas_limit)
                .checked_mul(self.tx.gas_price)
                .and_then(|gas_cost| gas_cost.checked_add(self.tx.value))
                .ok_or(InvalidTransaction::OverflowPaymentInTransaction)?;
    
            if SPEC::enabled(SpecId::CANCUN) {
                // if the tx is not a blob tx, this will be None, so we add zero
                let data_fee = self.calc_max_data_fee().unwrap_or_default();
                balance_check = balance_check
                    .checked_add(U256::from(data_fee))
                    .ok_or(InvalidTransaction::OverflowPaymentInTransaction)?;
            }
    
            // Check if account has enough balance for gas_limit*gas_price and value transfer.
            // Transfer will be done inside `*_inner` functions.
            if balance_check > account.info.balance {
                if self.cfg.is_balance_check_disabled() {
                    // Add transaction cost to balance to ensure execution doesn't fail.
                    account.info.balance = balance_check;
                } else {
                    return Err(InvalidTransaction::LackOfFundForMaxFee {
                        fee: Box::new(balance_check),
                        balance: Box::new(account.info.balance),
                    });
                }
            }
    
            Ok(())
        }
    *)
    Definition validate_tx_against_state
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [ SPEC ], [ self; account ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let account := M.alloc (| account |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                LogicalOp.and (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_primitives::env::CfgEnv",
                                        "is_eip3607_disabled",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm_primitives::env::Env",
                                          "cfg"
                                        |)
                                      ]
                                    |)
                                  |),
                                  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 ]
                                            []
                                        ],
                                        "ne",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| account |),
                                            "revm_primitives::state::Account",
                                            "info"
                                          |),
                                          "revm_primitives::state::AccountInfo",
                                          "code_hash"
                                        |);
                                        M.get_constant (|
                                          "revm_primitives::utilities::KECCAK_EMPTY"
                                        |)
                                      ]
                                    |)))
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::result::InvalidTransaction::RejectCallerWithCode"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm_primitives::env::Env",
                                "tx"
                              |),
                              "revm_primitives::env::TxEnv",
                              "nonce"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let tx := M.copy (| γ0_0 |) in
                          let~ state :=
                            M.copy (|
                              M.SubPointer.get_struct_record_field (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| account |),
                                  "revm_primitives::state::Account",
                                  "info"
                                |),
                                "revm_primitives::state::AccountInfo",
                                "nonce"
                              |)
                            |) in
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::Ord",
                                  Ty.path "u64",
                                  [],
                                  "cmp",
                                  []
                                |),
                                [ tx; state ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructRecord
                                                "revm_primitives::result::InvalidTransaction::NonceTooHigh"
                                                [
                                                  ("tx", M.read (| tx |));
                                                  ("state", M.read (| state |))
                                                ]
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
                                  M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructRecord
                                                "revm_primitives::result::InvalidTransaction::NonceTooLow"
                                                [
                                                  ("tx", M.read (| tx |));
                                                  ("state", M.read (| state |))
                                                ]
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)));
                              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ balance_check :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "revm_primitives::result::InvalidTransaction"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::option::Option")
                                  []
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                "ok_or",
                                [ Ty.path "revm_primitives::result::InvalidTransaction" ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ],
                                    "and_then",
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [];
                                      Ty.function
                                        [
                                          Ty.tuple
                                            [
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                []
                                            ]
                                        ]
                                        (Ty.apply
                                          (Ty.path "core::option::Option")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ])
                                    ]
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        "checked_mul",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [],
                                            "from",
                                            [ Ty.path "u64" ]
                                          |),
                                          [
                                            M.read (|
                                              M.SubPointer.get_struct_record_field (|
                                                M.SubPointer.get_struct_record_field (|
                                                  M.read (| self |),
                                                  "revm_primitives::env::Env",
                                                  "tx"
                                                |),
                                                "revm_primitives::env::TxEnv",
                                                "gas_limit"
                                              |)
                                            |)
                                          ]
                                        |);
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm_primitives::env::Env",
                                              "tx"
                                            |),
                                            "revm_primitives::env::TxEnv",
                                            "gas_price"
                                          |)
                                        |)
                                      ]
                                    |);
                                    M.closure
                                      (fun γ =>
                                        ltac:(M.monadic
                                          match γ with
                                          | [ α0 ] =>
                                            ltac:(M.monadic
                                              (M.match_operator (|
                                                M.alloc (| α0 |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let gas_cost := M.copy (| γ |) in
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "ruint::Uint")
                                                            [
                                                              Value.Integer IntegerKind.Usize 256;
                                                              Value.Integer IntegerKind.Usize 4
                                                            ]
                                                            [],
                                                          "checked_add",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| gas_cost |);
                                                          M.read (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.SubPointer.get_struct_record_field (|
                                                                M.read (| self |),
                                                                "revm_primitives::env::Env",
                                                                "tx"
                                                              |),
                                                              "revm_primitives::env::TxEnv",
                                                              "value"
                                                            |)
                                                          |)
                                                        ]
                                                      |)))
                                                ]
                                              |)))
                                          | _ => M.impossible "wrong number of arguments"
                                          end))
                                  ]
                                |);
                                Value.StructTuple
                                  "revm_primitives::result::InvalidTransaction::OverflowPaymentInTransaction"
                                  []
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.tuple [];
                                            Ty.path "revm_primitives::result::InvalidTransaction"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path "revm_primitives::result::InvalidTransaction"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "revm_primitives::specification::Spec",
                                    SPEC,
                                    [],
                                    "enabled",
                                    []
                                  |),
                                  [
                                    Value.StructTuple
                                      "revm_primitives::specification::SpecId::CANCUN"
                                      []
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          let~ data_fee :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        []
                                    ],
                                  "unwrap_or_default",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "revm_primitives::env::Env",
                                      "calc_max_data_fee",
                                      []
                                    |),
                                    [ M.read (| self |) ]
                                  |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.write (|
                              balance_check,
                              M.read (|
                                M.match_operator (|
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::Try",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              [];
                                            Ty.path "revm_primitives::result::InvalidTransaction"
                                          ],
                                        [],
                                        "branch",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "core::option::Option")
                                              []
                                              [
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  []
                                              ],
                                            "ok_or",
                                            [ Ty.path "revm_primitives::result::InvalidTransaction"
                                            ]
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                "checked_add",
                                                []
                                              |),
                                              [
                                                M.read (| balance_check |);
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "ruint::Uint")
                                                      [
                                                        Value.Integer IntegerKind.Usize 256;
                                                        Value.Integer IntegerKind.Usize 4
                                                      ]
                                                      [],
                                                    "from",
                                                    [
                                                      Ty.apply
                                                        (Ty.path "ruint::Uint")
                                                        [
                                                          Value.Integer IntegerKind.Usize 256;
                                                          Value.Integer IntegerKind.Usize 4
                                                        ]
                                                        []
                                                    ]
                                                  |),
                                                  [ M.read (| data_fee |) ]
                                                |)
                                              ]
                                            |);
                                            Value.StructTuple
                                              "revm_primitives::result::InvalidTransaction::OverflowPaymentInTransaction"
                                              []
                                          ]
                                        |)
                                      ]
                                    |)
                                  |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::ops::control_flow::ControlFlow::Break",
                                            0
                                          |) in
                                        let residual := M.copy (| γ0_0 |) in
                                        M.alloc (|
                                          M.never_to_any (|
                                            M.read (|
                                              M.return_ (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::try_trait::FromResidual",
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.tuple [];
                                                        Ty.path
                                                          "revm_primitives::result::InvalidTransaction"
                                                      ],
                                                    [
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [
                                                          Ty.path "core::convert::Infallible";
                                                          Ty.path
                                                            "revm_primitives::result::InvalidTransaction"
                                                        ]
                                                    ],
                                                    "from_residual",
                                                    []
                                                  |),
                                                  [ M.read (| residual |) ]
                                                |)
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ0_0 :=
                                          M.SubPointer.get_struct_tuple_field (|
                                            γ,
                                            "core::ops::control_flow::ControlFlow::Continue",
                                            0
                                          |) in
                                        let val := M.copy (| γ0_0 |) in
                                        val))
                                  ]
                                |)
                              |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::cmp::PartialOrd",
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        []
                                    ],
                                    "gt",
                                    []
                                  |),
                                  [
                                    balance_check;
                                    M.SubPointer.get_struct_record_field (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| account |),
                                        "revm_primitives::state::Account",
                                        "info"
                                      |),
                                      "revm_primitives::state::AccountInfo",
                                      "balance"
                                    |)
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.match_operator (|
                            M.alloc (| Value.Tuple [] |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ :=
                                    M.use
                                      (M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_primitives::env::CfgEnv",
                                            "is_balance_check_disabled",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "revm_primitives::env::Env",
                                              "cfg"
                                            |)
                                          ]
                                        |)
                                      |)) in
                                  let _ :=
                                    M.is_constant_or_break_match (|
                                      M.read (| γ |),
                                      Value.Bool true
                                    |) in
                                  let~ _ :=
                                    M.write (|
                                      M.SubPointer.get_struct_record_field (|
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| account |),
                                          "revm_primitives::state::Account",
                                          "info"
                                        |),
                                        "revm_primitives::state::AccountInfo",
                                        "balance"
                                      |),
                                      M.read (| balance_check |)
                                    |) in
                                  M.alloc (| Value.Tuple [] |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (M.alloc (|
                                    M.never_to_any (|
                                      M.read (|
                                        M.return_ (|
                                          Value.StructTuple
                                            "core::result::Result::Err"
                                            [
                                              Value.StructRecord
                                                "revm_primitives::result::InvalidTransaction::LackOfFundForMaxFee"
                                                [
                                                  ("fee",
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "alloc::boxed::Box")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "ruint::Uint")
                                                              [
                                                                Value.Integer IntegerKind.Usize 256;
                                                                Value.Integer IntegerKind.Usize 4
                                                              ]
                                                              [];
                                                            Ty.path "alloc::alloc::Global"
                                                          ],
                                                        "new",
                                                        []
                                                      |),
                                                      [ M.read (| balance_check |) ]
                                                    |));
                                                  ("balance",
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "alloc::boxed::Box")
                                                          []
                                                          [
                                                            Ty.apply
                                                              (Ty.path "ruint::Uint")
                                                              [
                                                                Value.Integer IntegerKind.Usize 256;
                                                                Value.Integer IntegerKind.Usize 4
                                                              ]
                                                              [];
                                                            Ty.path "alloc::alloc::Global"
                                                          ],
                                                        "new",
                                                        []
                                                      |),
                                                      [
                                                        M.read (|
                                                          M.SubPointer.get_struct_record_field (|
                                                            M.SubPointer.get_struct_record_field (|
                                                              M.read (| account |),
                                                              "revm_primitives::state::Account",
                                                              "info"
                                                            |),
                                                            "revm_primitives::state::AccountInfo",
                                                            "balance"
                                                          |)
                                                        |)
                                                      ]
                                                    |))
                                                ]
                                            ]
                                        |)
                                      |)
                                    |)
                                  |)))
                            ]
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_validate_tx_against_state :
      M.IsAssociatedFunction Self "validate_tx_against_state" validate_tx_against_state.
  End Impl_revm_primitives_env_Env.
  
  (* StructRecord
    {
      name := "CfgEnv";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("chain_id", Ty.path "u64");
          ("kzg_settings", Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings");
          ("perf_analyse_created_bytecodes", Ty.path "revm_primitives::env::AnalysisKind");
          ("limit_contract_code_size",
            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_env_CfgEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CfgEnv".
    
    (* 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::CfgEnv"
            [
              ("chain_id",
                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::env::CfgEnv",
                      "chain_id"
                    |)
                  ]
                |));
              ("kzg_settings",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::CfgEnv",
                      "kzg_settings"
                    |)
                  ]
                |));
              ("perf_analyse_created_bytecodes",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "revm_primitives::env::AnalysisKind",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::CfgEnv",
                      "perf_analyse_created_bytecodes"
                    |)
                  ]
                |));
              ("limit_contract_code_size",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::CfgEnv",
                      "limit_contract_code_size"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_CfgEnv.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_env_CfgEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CfgEnv".
    
    (* 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 "CfgEnv" |);
              M.read (| Value.String "chain_id" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::env::CfgEnv",
                "chain_id"
              |);
              M.read (| Value.String "kzg_settings" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::env::CfgEnv",
                "kzg_settings"
              |);
              M.read (| Value.String "perf_analyse_created_bytecodes" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::env::CfgEnv",
                "perf_analyse_created_bytecodes"
              |);
              M.read (| Value.String "limit_contract_code_size" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::CfgEnv",
                  "limit_contract_code_size"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_CfgEnv.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_env_CfgEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CfgEnv".
    
    (* 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_env_CfgEnv.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_CfgEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CfgEnv".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_CfgEnv.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_env_CfgEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CfgEnv".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            LogicalOp.and (|
              LogicalOp.and (|
                BinOp.eq (|
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::CfgEnv",
                      "chain_id"
                    |)
                  |),
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::env::CfgEnv",
                      "chain_id"
                    |)
                  |)
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings",
                      [ Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings" ],
                      "eq",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::CfgEnv",
                        "kzg_settings"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm_primitives::env::CfgEnv",
                        "kzg_settings"
                      |)
                    ]
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.path "revm_primitives::env::AnalysisKind",
                    [ Ty.path "revm_primitives::env::AnalysisKind" ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::CfgEnv",
                      "perf_analyse_created_bytecodes"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::env::CfgEnv",
                      "perf_analyse_created_bytecodes"
                    |)
                  ]
                |)))
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                  [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ] ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::CfgEnv",
                    "limit_contract_code_size"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::env::CfgEnv",
                    "limit_contract_code_size"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_CfgEnv.
  
  Module Impl_revm_primitives_env_CfgEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CfgEnv".
    
    (*
        pub fn with_chain_id(mut self, chain_id: u64) -> Self {
            self.chain_id = chain_id;
            self
        }
    *)
    Definition with_chain_id (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; chain_id ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let chain_id := M.alloc (| chain_id |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  self,
                  "revm_primitives::env::CfgEnv",
                  "chain_id"
                |),
                M.read (| chain_id |)
              |) in
            self
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_with_chain_id :
      M.IsAssociatedFunction Self "with_chain_id" with_chain_id.
    
    (*
        pub fn is_eip3607_disabled(&self) -> bool {
            false
        }
    *)
    Definition is_eip3607_disabled (ε : 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_eip3607_disabled :
      M.IsAssociatedFunction Self "is_eip3607_disabled" is_eip3607_disabled.
    
    (*
        pub fn is_balance_check_disabled(&self) -> bool {
            false
        }
    *)
    Definition is_balance_check_disabled
        (ε : 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_balance_check_disabled :
      M.IsAssociatedFunction Self "is_balance_check_disabled" is_balance_check_disabled.
    
    (*
        pub fn is_gas_refund_disabled(&self) -> bool {
            false
        }
    *)
    Definition is_gas_refund_disabled (ε : 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_gas_refund_disabled :
      M.IsAssociatedFunction Self "is_gas_refund_disabled" is_gas_refund_disabled.
    
    (*
        pub fn is_base_fee_check_disabled(&self) -> bool {
            false
        }
    *)
    Definition is_base_fee_check_disabled
        (ε : 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_base_fee_check_disabled :
      M.IsAssociatedFunction Self "is_base_fee_check_disabled" is_base_fee_check_disabled.
    
    (*
        pub fn is_block_gas_limit_disabled(&self) -> bool {
            false
        }
    *)
    Definition is_block_gas_limit_disabled
        (ε : 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_block_gas_limit_disabled :
      M.IsAssociatedFunction Self "is_block_gas_limit_disabled" is_block_gas_limit_disabled.
    
    (*
        pub fn is_beneficiary_reward_disabled(&self) -> bool {
            false
        }
    *)
    Definition is_beneficiary_reward_disabled
        (ε : 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_beneficiary_reward_disabled :
      M.IsAssociatedFunction Self "is_beneficiary_reward_disabled" is_beneficiary_reward_disabled.
  End Impl_revm_primitives_env_CfgEnv.
  
  Module Impl_core_default_Default_for_revm_primitives_env_CfgEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CfgEnv".
    
    (*
        fn default() -> Self {
            Self {
                chain_id: 1,
                perf_analyse_created_bytecodes: AnalysisKind::default(),
                limit_contract_code_size: None,
                #[cfg(feature = "c-kzg")]
                kzg_settings: crate::kzg::EnvKzgSettings::Default,
                #[cfg(feature = "memory_limit")]
                memory_limit: (1 << 32) - 1,
                #[cfg(feature = "optional_balance_check")]
                disable_balance_check: false,
                #[cfg(feature = "optional_block_gas_limit")]
                disable_block_gas_limit: false,
                #[cfg(feature = "optional_eip3607")]
                disable_eip3607: false,
                #[cfg(feature = "optional_gas_refund")]
                disable_gas_refund: false,
                #[cfg(feature = "optional_no_base_fee")]
                disable_base_fee: false,
                #[cfg(feature = "optional_beneficiary_reward")]
                disable_beneficiary_reward: false,
            }
        }
    *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_primitives::env::CfgEnv"
            [
              ("chain_id", Value.Integer IntegerKind.U64 1);
              ("perf_analyse_created_bytecodes",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::env::AnalysisKind",
                    [],
                    "default",
                    []
                  |),
                  []
                |));
              ("limit_contract_code_size", Value.StructTuple "core::option::Option::None" []);
              ("kzg_settings",
                Value.StructTuple "revm_primitives::kzg::env_settings::EnvKzgSettings::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_CfgEnv.
  
  (* StructRecord
    {
      name := "BlockEnv";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("number",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("coinbase", Ty.path "alloy_primitives::bits::address::Address");
          ("timestamp",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("gas_limit",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("basefee",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("difficulty",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("prevrandao",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [
                Ty.apply
                  (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                  [ Value.Integer IntegerKind.Usize 32 ]
                  []
              ]);
          ("blob_excess_gas_and_price",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_env_BlockEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlockEnv".
    
    (* 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::BlockEnv"
            [
              ("number",
                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::env::BlockEnv",
                      "number"
                    |)
                  ]
                |));
              ("coinbase",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "alloy_primitives::bits::address::Address",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::BlockEnv",
                      "coinbase"
                    |)
                  ]
                |));
              ("timestamp",
                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::env::BlockEnv",
                      "timestamp"
                    |)
                  ]
                |));
              ("gas_limit",
                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::env::BlockEnv",
                      "gas_limit"
                    |)
                  ]
                |));
              ("basefee",
                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::env::BlockEnv",
                      "basefee"
                    |)
                  ]
                |));
              ("difficulty",
                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::env::BlockEnv",
                      "difficulty"
                    |)
                  ]
                |));
              ("prevrandao",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        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::env::BlockEnv",
                      "prevrandao"
                    |)
                  ]
                |));
              ("blob_excess_gas_and_price",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::BlockEnv",
                      "blob_excess_gas_and_price"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_BlockEnv.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_env_BlockEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlockEnv".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ names :=
              M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      M.read (| Value.String "number" |);
                      M.read (| Value.String "coinbase" |);
                      M.read (| Value.String "timestamp" |);
                      M.read (| Value.String "gas_limit" |);
                      M.read (| Value.String "basefee" |);
                      M.read (| Value.String "difficulty" |);
                      M.read (| Value.String "prevrandao" |);
                      M.read (| Value.String "blob_excess_gas_and_price" |)
                    ]
                |)
              |) in
            let~ values :=
              M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::BlockEnv",
                        "number"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::BlockEnv",
                        "coinbase"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::BlockEnv",
                        "timestamp"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::BlockEnv",
                        "gas_limit"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::BlockEnv",
                        "basefee"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::BlockEnv",
                        "difficulty"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::BlockEnv",
                        "prevrandao"
                      |);
                      M.alloc (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_primitives::env::BlockEnv",
                          "blob_excess_gas_and_price"
                        |)
                      |)
                    ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_fields_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "BlockEnv" |);
                  M.read (| names |);
                  M.read (| values |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_revm_primitives_env_BlockEnv.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_BlockEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlockEnv".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_BlockEnv.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_env_BlockEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlockEnv".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            LogicalOp.and (|
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    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::env::BlockEnv",
                              "number"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "revm_primitives::env::BlockEnv",
                              "number"
                            |)
                          ]
                        |),
                        ltac:(M.monadic
                          (M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialEq",
                              Ty.path "alloy_primitives::bits::address::Address",
                              [ Ty.path "alloy_primitives::bits::address::Address" ],
                              "eq",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm_primitives::env::BlockEnv",
                                "coinbase"
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| other |),
                                "revm_primitives::env::BlockEnv",
                                "coinbase"
                              |)
                            ]
                          |)))
                      |),
                      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::env::BlockEnv",
                              "timestamp"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "revm_primitives::env::BlockEnv",
                              "timestamp"
                            |)
                          ]
                        |)))
                    |),
                    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::env::BlockEnv",
                            "gas_limit"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "revm_primitives::env::BlockEnv",
                            "gas_limit"
                          |)
                        ]
                      |)))
                  |),
                  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::env::BlockEnv",
                          "basefee"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm_primitives::env::BlockEnv",
                          "basefee"
                        |)
                      ]
                    |)))
                |),
                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::env::BlockEnv",
                        "difficulty"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm_primitives::env::BlockEnv",
                        "difficulty"
                      |)
                    ]
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          []
                      ],
                    [
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                            [ Value.Integer IntegerKind.Usize 32 ]
                            []
                        ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::BlockEnv",
                      "prevrandao"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::env::BlockEnv",
                      "prevrandao"
                    |)
                  ]
                |)))
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ],
                  [
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::BlockEnv",
                    "blob_excess_gas_and_price"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::env::BlockEnv",
                    "blob_excess_gas_and_price"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_BlockEnv.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_env_BlockEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlockEnv".
    
    (* 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_env_BlockEnv.
  
  Module Impl_core_hash_Hash_for_revm_primitives_env_BlockEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlockEnv".
    
    (* 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::env::BlockEnv",
                      "number"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.path "alloy_primitives::bits::address::Address",
                    [],
                    "hash",
                    [ __H ]
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::BlockEnv",
                      "coinbase"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            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::env::BlockEnv",
                      "timestamp"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            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::env::BlockEnv",
                      "gas_limit"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            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::env::BlockEnv",
                      "basefee"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            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::env::BlockEnv",
                      "difficulty"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::hash::Hash",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        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::env::BlockEnv",
                      "prevrandao"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::hash::Hash",
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ],
                  [],
                  "hash",
                  [ __H ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::BlockEnv",
                    "blob_excess_gas_and_price"
                  |);
                  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_BlockEnv.
  
  Module Impl_revm_primitives_env_BlockEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlockEnv".
    
    (*
        pub fn set_blob_excess_gas_and_price(&mut self, excess_blob_gas: u64) {
            self.blob_excess_gas_and_price = Some(BlobExcessGasAndPrice::new(excess_blob_gas));
        }
    *)
    Definition set_blob_excess_gas_and_price
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self; excess_blob_gas ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let excess_blob_gas := M.alloc (| excess_blob_gas |) in
          M.read (|
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::BlockEnv",
                  "blob_excess_gas_and_price"
                |),
                Value.StructTuple
                  "core::option::Option::Some"
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_primitives::env::BlobExcessGasAndPrice",
                        "new",
                        []
                      |),
                      [ M.read (| excess_blob_gas |) ]
                    |)
                  ]
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_set_blob_excess_gas_and_price :
      M.IsAssociatedFunction Self "set_blob_excess_gas_and_price" set_blob_excess_gas_and_price.
    
    (*
        pub fn get_blob_gasprice(&self) -> Option<u128> {
            self.blob_excess_gas_and_price
                .as_ref()
                .map(|a| a.blob_gasprice)
        }
    *)
    Definition get_blob_gasprice (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.apply
                    (Ty.path "&")
                    []
                    [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ]
                ],
              "map",
              [
                Ty.path "u128";
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ]
                      ]
                  ]
                  (Ty.path "u128")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ],
                  "as_ref",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::BlockEnv",
                    "blob_excess_gas_and_price"
                  |)
                ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let a := M.copy (| γ |) in
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| a |),
                                    "revm_primitives::env::BlobExcessGasAndPrice",
                                    "blob_gasprice"
                                  |)
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_blob_gasprice :
      M.IsAssociatedFunction Self "get_blob_gasprice" get_blob_gasprice.
    
    (*
        pub fn get_blob_excess_gas(&self) -> Option<u64> {
            self.blob_excess_gas_and_price
                .as_ref()
                .map(|a| a.excess_blob_gas)
        }
    *)
    Definition get_blob_excess_gas (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.apply
                    (Ty.path "&")
                    []
                    [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ]
                ],
              "map",
              [
                Ty.path "u64";
                Ty.function
                  [
                    Ty.tuple
                      [
                        Ty.apply
                          (Ty.path "&")
                          []
                          [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ]
                      ]
                  ]
                  (Ty.path "u64")
              ]
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::option::Option")
                    []
                    [ Ty.path "revm_primitives::env::BlobExcessGasAndPrice" ],
                  "as_ref",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::BlockEnv",
                    "blob_excess_gas_and_price"
                  |)
                ]
              |);
              M.closure
                (fun γ =>
                  ltac:(M.monadic
                    match γ with
                    | [ α0 ] =>
                      ltac:(M.monadic
                        (M.match_operator (|
                          M.alloc (| α0 |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let a := M.copy (| γ |) in
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| a |),
                                    "revm_primitives::env::BlobExcessGasAndPrice",
                                    "excess_blob_gas"
                                  |)
                                |)))
                          ]
                        |)))
                    | _ => M.impossible "wrong number of arguments"
                    end))
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_blob_excess_gas :
      M.IsAssociatedFunction Self "get_blob_excess_gas" get_blob_excess_gas.
    
    (*
        pub fn clear(&mut self) {
            *self = Self::default();
        }
    *)
    Definition clear (ε : 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.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::env::BlockEnv",
                    [],
                    "default",
                    []
                  |),
                  []
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_clear : M.IsAssociatedFunction Self "clear" clear.
  End Impl_revm_primitives_env_BlockEnv.
  
  Module Impl_core_default_Default_for_revm_primitives_env_BlockEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlockEnv".
    
    (*
        fn default() -> Self {
            Self {
                number: U256::ZERO,
                coinbase: Address::ZERO,
                timestamp: U256::from(1),
                gas_limit: U256::MAX,
                basefee: U256::ZERO,
                difficulty: U256::ZERO,
                prevrandao: Some(B256::ZERO),
                blob_excess_gas_and_price: Some(BlobExcessGasAndPrice::new(0)),
            }
        }
    *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_primitives::env::BlockEnv"
            [
              ("number", M.read (| M.get_constant (| "ruint::ZERO" |) |));
              ("coinbase",
                M.read (| M.get_constant (| "alloy_primitives::bits::address::ZERO" |) |));
              ("timestamp",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    "from",
                    [ Ty.path "i32" ]
                  |),
                  [ Value.Integer IntegerKind.I32 1 ]
                |));
              ("gas_limit", M.read (| M.get_constant (| "ruint::MAX" |) |));
              ("basefee", M.read (| M.get_constant (| "ruint::ZERO" |) |));
              ("difficulty", M.read (| M.get_constant (| "ruint::ZERO" |) |));
              ("prevrandao",
                Value.StructTuple
                  "core::option::Option::Some"
                  [ M.read (| M.get_constant (| "alloy_primitives::bits::fixed::ZERO" |) |) ]);
              ("blob_excess_gas_and_price",
                Value.StructTuple
                  "core::option::Option::Some"
                  [
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_primitives::env::BlobExcessGasAndPrice",
                        "new",
                        []
                      |),
                      [ 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_env_BlockEnv.
  
  (* StructRecord
    {
      name := "TxEnv";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("caller", Ty.path "alloy_primitives::bits::address::Address");
          ("gas_limit", Ty.path "u64");
          ("gas_price",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("transact_to", Ty.path "revm_primitives::env::TransactTo");
          ("value",
            Ty.apply
              (Ty.path "ruint::Uint")
              [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
              []);
          ("data", Ty.path "alloy_primitives::bytes_::Bytes");
          ("nonce", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ]);
          ("chain_id", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ]);
          ("access_list",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.tuple
                  [
                    Ty.path "alloy_primitives::bits::address::Address";
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          [];
                        Ty.path "alloc::alloc::Global"
                      ]
                  ];
                Ty.path "alloc::alloc::Global"
              ]);
          ("gas_priority_fee",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [
                Ty.apply
                  (Ty.path "ruint::Uint")
                  [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                  []
              ]);
          ("blob_hashes",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [
                Ty.apply
                  (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                  [ Value.Integer IntegerKind.Usize 32 ]
                  [];
                Ty.path "alloc::alloc::Global"
              ]);
          ("max_fee_per_blob_gas",
            Ty.apply
              (Ty.path "core::option::Option")
              []
              [
                Ty.apply
                  (Ty.path "ruint::Uint")
                  [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                  []
              ]);
          ("eof_initcodes",
            Ty.apply
              (Ty.path "alloc::vec::Vec")
              []
              [ Ty.path "alloy_primitives::bytes_::Bytes"; Ty.path "alloc::alloc::Global" ]);
          ("eof_initcodes_hashed",
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.apply
                  (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                  [ Value.Integer IntegerKind.Usize 32 ]
                  [];
                Ty.path "alloy_primitives::bytes_::Bytes";
                Ty.path "std::hash::random::RandomState"
              ])
        ];
    } *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_env_TxEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TxEnv".
    
    (* 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::TxEnv"
            [
              ("caller",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "alloy_primitives::bits::address::Address",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "caller"
                    |)
                  ]
                |));
              ("gas_limit",
                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::env::TxEnv",
                      "gas_limit"
                    |)
                  ]
                |));
              ("gas_price",
                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::env::TxEnv",
                      "gas_price"
                    |)
                  ]
                |));
              ("transact_to",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "revm_primitives::env::TransactTo",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "transact_to"
                    |)
                  ]
                |));
              ("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::env::TxEnv",
                      "value"
                    |)
                  ]
                |));
              ("data",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.path "alloy_primitives::bytes_::Bytes",
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "data"
                    |)
                  ]
                |));
              ("nonce",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "nonce"
                    |)
                  ]
                |));
              ("chain_id",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "chain_id"
                    |)
                  ]
                |));
              ("access_list",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "access_list"
                    |)
                  ]
                |));
              ("gas_priority_fee",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        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::env::TxEnv",
                      "gas_priority_fee"
                    |)
                  ]
                |));
              ("blob_hashes",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          [];
                        Ty.path "alloc::alloc::Global"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "blob_hashes"
                    |)
                  ]
                |));
              ("max_fee_per_blob_gas",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "core::option::Option")
                      []
                      [
                        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::env::TxEnv",
                      "max_fee_per_blob_gas"
                    |)
                  ]
                |));
              ("eof_initcodes",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "alloy_primitives::bytes_::Bytes"; Ty.path "alloc::alloc::Global" ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "eof_initcodes"
                    |)
                  ]
                |));
              ("eof_initcodes_hashed",
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "std::collections::hash::map::HashMap")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          [];
                        Ty.path "alloy_primitives::bytes_::Bytes";
                        Ty.path "std::hash::random::RandomState"
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "eof_initcodes_hashed"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_TxEnv.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_env_TxEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TxEnv".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            let~ names :=
              M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      M.read (| Value.String "caller" |);
                      M.read (| Value.String "gas_limit" |);
                      M.read (| Value.String "gas_price" |);
                      M.read (| Value.String "transact_to" |);
                      M.read (| Value.String "value" |);
                      M.read (| Value.String "data" |);
                      M.read (| Value.String "nonce" |);
                      M.read (| Value.String "chain_id" |);
                      M.read (| Value.String "access_list" |);
                      M.read (| Value.String "gas_priority_fee" |);
                      M.read (| Value.String "blob_hashes" |);
                      M.read (| Value.String "max_fee_per_blob_gas" |);
                      M.read (| Value.String "eof_initcodes" |);
                      M.read (| Value.String "eof_initcodes_hashed" |)
                    ]
                |)
              |) in
            let~ values :=
              M.alloc (|
                M.alloc (|
                  Value.Array
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "caller"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "gas_limit"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "gas_price"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "transact_to"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "value"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "data"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "nonce"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "chain_id"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "access_list"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "gas_priority_fee"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "blob_hashes"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "max_fee_per_blob_gas"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "revm_primitives::env::TxEnv",
                        "eof_initcodes"
                      |);
                      M.alloc (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_primitives::env::TxEnv",
                          "eof_initcodes_hashed"
                        |)
                      |)
                    ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "core::fmt::Formatter",
                  "debug_struct_fields_finish",
                  []
                |),
                [
                  M.read (| f |);
                  M.read (| Value.String "TxEnv" |);
                  M.read (| names |);
                  M.read (| values |)
                ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_revm_primitives_env_TxEnv.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_TxEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TxEnv".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_TxEnv.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_env_TxEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TxEnv".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          LogicalOp.and (|
            LogicalOp.and (|
              LogicalOp.and (|
                LogicalOp.and (|
                  LogicalOp.and (|
                    LogicalOp.and (|
                      LogicalOp.and (|
                        LogicalOp.and (|
                          LogicalOp.and (|
                            LogicalOp.and (|
                              LogicalOp.and (|
                                LogicalOp.and (|
                                  LogicalOp.and (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "alloy_primitives::bits::address::Address",
                                        [ Ty.path "alloy_primitives::bits::address::Address" ],
                                        "eq",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "revm_primitives::env::TxEnv",
                                          "caller"
                                        |);
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| other |),
                                          "revm_primitives::env::TxEnv",
                                          "caller"
                                        |)
                                      ]
                                    |),
                                    ltac:(M.monadic
                                      (BinOp.eq (|
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| self |),
                                            "revm_primitives::env::TxEnv",
                                            "gas_limit"
                                          |)
                                        |),
                                        M.read (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| other |),
                                            "revm_primitives::env::TxEnv",
                                            "gas_limit"
                                          |)
                                        |)
                                      |)))
                                  |),
                                  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::env::TxEnv",
                                          "gas_price"
                                        |);
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| other |),
                                          "revm_primitives::env::TxEnv",
                                          "gas_price"
                                        |)
                                      ]
                                    |)))
                                |),
                                ltac:(M.monadic
                                  (M.call_closure (|
                                    M.get_trait_method (|
                                      "core::cmp::PartialEq",
                                      Ty.path "revm_primitives::env::TransactTo",
                                      [ Ty.path "revm_primitives::env::TransactTo" ],
                                      "eq",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "revm_primitives::env::TxEnv",
                                        "transact_to"
                                      |);
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| other |),
                                        "revm_primitives::env::TxEnv",
                                        "transact_to"
                                      |)
                                    ]
                                  |)))
                              |),
                              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::env::TxEnv",
                                      "value"
                                    |);
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| other |),
                                      "revm_primitives::env::TxEnv",
                                      "value"
                                    |)
                                  ]
                                |)))
                            |),
                            ltac:(M.monadic
                              (M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                  [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                                  "eq",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "revm_primitives::env::TxEnv",
                                    "data"
                                  |);
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| other |),
                                    "revm_primitives::env::TxEnv",
                                    "data"
                                  |)
                                ]
                              |)))
                          |),
                          ltac:(M.monadic
                            (M.call_closure (|
                              M.get_trait_method (|
                                "core::cmp::PartialEq",
                                Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                                [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ] ],
                                "eq",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "revm_primitives::env::TxEnv",
                                  "nonce"
                                |);
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| other |),
                                  "revm_primitives::env::TxEnv",
                                  "nonce"
                                |)
                              ]
                            |)))
                        |),
                        ltac:(M.monadic
                          (M.call_closure (|
                            M.get_trait_method (|
                              "core::cmp::PartialEq",
                              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ],
                              [ Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ] ],
                              "eq",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "revm_primitives::env::TxEnv",
                                "chain_id"
                              |);
                              M.SubPointer.get_struct_record_field (|
                                M.read (| other |),
                                "revm_primitives::env::TxEnv",
                                "chain_id"
                              |)
                            ]
                          |)))
                      |),
                      ltac:(M.monadic
                        (M.call_closure (|
                          M.get_trait_method (|
                            "core::cmp::PartialEq",
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.tuple
                                  [
                                    Ty.path "alloy_primitives::bits::address::Address";
                                    Ty.apply
                                      (Ty.path "alloc::vec::Vec")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [];
                                        Ty.path "alloc::alloc::Global"
                                      ]
                                  ];
                                Ty.path "alloc::alloc::Global"
                              ],
                            [
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [
                                  Ty.tuple
                                    [
                                      Ty.path "alloy_primitives::bits::address::Address";
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [];
                                          Ty.path "alloc::alloc::Global"
                                        ]
                                    ];
                                  Ty.path "alloc::alloc::Global"
                                ]
                            ],
                            "eq",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "revm_primitives::env::TxEnv",
                              "access_list"
                            |);
                            M.SubPointer.get_struct_record_field (|
                              M.read (| other |),
                              "revm_primitives::env::TxEnv",
                              "access_list"
                            |)
                          ]
                        |)))
                    |),
                    ltac:(M.monadic
                      (M.call_closure (|
                        M.get_trait_method (|
                          "core::cmp::PartialEq",
                          Ty.apply
                            (Ty.path "core::option::Option")
                            []
                            [
                              Ty.apply
                                (Ty.path "ruint::Uint")
                                [
                                  Value.Integer IntegerKind.Usize 256;
                                  Value.Integer IntegerKind.Usize 4
                                ]
                                []
                            ],
                          [
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [
                                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::env::TxEnv",
                            "gas_priority_fee"
                          |);
                          M.SubPointer.get_struct_record_field (|
                            M.read (| other |),
                            "revm_primitives::env::TxEnv",
                            "gas_priority_fee"
                          |)
                        ]
                      |)))
                  |),
                  ltac:(M.monadic
                    (M.call_closure (|
                      M.get_trait_method (|
                        "core::cmp::PartialEq",
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [
                            Ty.apply
                              (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                              [ Value.Integer IntegerKind.Usize 32 ]
                              [];
                            Ty.path "alloc::alloc::Global"
                          ],
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [
                              Ty.apply
                                (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                                [ Value.Integer IntegerKind.Usize 32 ]
                                [];
                              Ty.path "alloc::alloc::Global"
                            ]
                        ],
                        "eq",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "revm_primitives::env::TxEnv",
                          "blob_hashes"
                        |);
                        M.SubPointer.get_struct_record_field (|
                          M.read (| other |),
                          "revm_primitives::env::TxEnv",
                          "blob_hashes"
                        |)
                      ]
                    |)))
                |),
                ltac:(M.monadic
                  (M.call_closure (|
                    M.get_trait_method (|
                      "core::cmp::PartialEq",
                      Ty.apply
                        (Ty.path "core::option::Option")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ],
                      [
                        Ty.apply
                          (Ty.path "core::option::Option")
                          []
                          [
                            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::env::TxEnv",
                        "max_fee_per_blob_gas"
                      |);
                      M.SubPointer.get_struct_record_field (|
                        M.read (| other |),
                        "revm_primitives::env::TxEnv",
                        "max_fee_per_blob_gas"
                      |)
                    ]
                  |)))
              |),
              ltac:(M.monadic
                (M.call_closure (|
                  M.get_trait_method (|
                    "core::cmp::PartialEq",
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "alloy_primitives::bytes_::Bytes"; Ty.path "alloc::alloc::Global" ],
                    [
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [ Ty.path "alloy_primitives::bytes_::Bytes"; Ty.path "alloc::alloc::Global"
                        ]
                    ],
                    "eq",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::TxEnv",
                      "eof_initcodes"
                    |);
                    M.SubPointer.get_struct_record_field (|
                      M.read (| other |),
                      "revm_primitives::env::TxEnv",
                      "eof_initcodes"
                    |)
                  ]
                |)))
            |),
            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 "alloy_primitives::bits::fixed::FixedBytes")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [];
                      Ty.path "alloy_primitives::bytes_::Bytes";
                      Ty.path "std::hash::random::RandomState"
                    ],
                  [
                    Ty.apply
                      (Ty.path "std::collections::hash::map::HashMap")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          [];
                        Ty.path "alloy_primitives::bytes_::Bytes";
                        Ty.path "std::hash::random::RandomState"
                      ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::TxEnv",
                    "eof_initcodes_hashed"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::env::TxEnv",
                    "eof_initcodes_hashed"
                  |)
                ]
              |)))
          |)))
      | _, _, _ => 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_TxEnv.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_env_TxEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TxEnv".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              Value.DeclaredButUndefined,
              [
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      Value.DeclaredButUndefined,
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              Value.DeclaredButUndefined,
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (M.match_operator (|
                                      Value.DeclaredButUndefined,
                                      [
                                        fun γ =>
                                          ltac:(M.monadic
                                            (M.match_operator (|
                                              Value.DeclaredButUndefined,
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (M.match_operator (|
                                                      Value.DeclaredButUndefined,
                                                      [
                                                        fun γ =>
                                                          ltac:(M.monadic
                                                            (M.match_operator (|
                                                              Value.DeclaredButUndefined,
                                                              [
                                                                fun γ =>
                                                                  ltac:(M.monadic
                                                                    (M.match_operator (|
                                                                      Value.DeclaredButUndefined,
                                                                      [
                                                                        fun γ =>
                                                                          ltac:(M.monadic
                                                                            (M.match_operator (|
                                                                              Value.DeclaredButUndefined,
                                                                              [
                                                                                fun γ =>
                                                                                  ltac:(M.monadic
                                                                                    (M.match_operator (|
                                                                                      Value.DeclaredButUndefined,
                                                                                      [
                                                                                        fun γ =>
                                                                                          ltac:(M.monadic
                                                                                            (M.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_env_TxEnv.
  
  (*
  Enum TxType
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Legacy";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Eip1559";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "BlobTx";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "EofCreate";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_revm_primitives_env_TxEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TxEnv".
    
    (*
        pub fn get_total_blob_gas(&self) -> u64 {
            GAS_PER_BLOB * self.blob_hashes.len() as u64
        }
    *)
    Definition get_total_blob_gas (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          BinOp.Wrap.mul (|
            M.read (| M.get_constant (| "revm_primitives::constants::GAS_PER_BLOB" |) |),
            M.rust_cast
              (M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [];
                      Ty.path "alloc::alloc::Global"
                    ],
                  "len",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::TxEnv",
                    "blob_hashes"
                  |)
                ]
              |))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_total_blob_gas :
      M.IsAssociatedFunction Self "get_total_blob_gas" get_total_blob_gas.
    
    (*
        pub fn clear(&mut self) {
            *self = Self::default();
        }
    *)
    Definition clear (ε : 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.write (|
                M.read (| self |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::default::Default",
                    Ty.path "revm_primitives::env::TxEnv",
                    [],
                    "default",
                    []
                  |),
                  []
                |)
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_clear : M.IsAssociatedFunction Self "clear" clear.
  End Impl_revm_primitives_env_TxEnv.
  
  Module Impl_core_default_Default_for_revm_primitives_env_TxEnv.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TxEnv".
    
    (*
        fn default() -> Self {
            Self {
                caller: Address::ZERO,
                gas_limit: u64::MAX,
                gas_price: U256::ZERO,
                gas_priority_fee: None,
                transact_to: TransactTo::Call(Address::ZERO), // will do nothing
                value: U256::ZERO,
                data: Bytes::new(),
                chain_id: None,
                nonce: None,
                access_list: Vec::new(),
                blob_hashes: Vec::new(),
                max_fee_per_blob_gas: None,
                eof_initcodes: Vec::new(),
                eof_initcodes_hashed: HashMap::new(),
                #[cfg(feature = "optimism")]
                optimism: OptimismFields::default(),
            }
        }
    *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic
          (Value.StructRecord
            "revm_primitives::env::TxEnv"
            [
              ("caller", M.read (| M.get_constant (| "alloy_primitives::bits::address::ZERO" |) |));
              ("gas_limit", M.read (| M.get_constant (| "core::num::MAX" |) |));
              ("gas_price", M.read (| M.get_constant (| "ruint::ZERO" |) |));
              ("gas_priority_fee", Value.StructTuple "core::option::Option::None" []);
              ("transact_to",
                Value.StructTuple
                  "revm_primitives::env::TransactTo::Call"
                  [ M.read (| M.get_constant (| "alloy_primitives::bits::address::ZERO" |) |) ]);
              ("value", M.read (| M.get_constant (| "ruint::ZERO" |) |));
              ("data",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "alloy_primitives::bytes_::Bytes",
                    "new",
                    []
                  |),
                  []
                |));
              ("chain_id", Value.StructTuple "core::option::Option::None" []);
              ("nonce", Value.StructTuple "core::option::Option::None" []);
              ("access_list",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.tuple
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  [];
                                Ty.path "alloc::alloc::Global"
                              ]
                          ];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |));
              ("blob_hashes",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          [];
                        Ty.path "alloc::alloc::Global"
                      ],
                    "new",
                    []
                  |),
                  []
                |));
              ("max_fee_per_blob_gas", Value.StructTuple "core::option::Option::None" []);
              ("eof_initcodes",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "alloy_primitives::bytes_::Bytes"; Ty.path "alloc::alloc::Global" ],
                    "new",
                    []
                  |),
                  []
                |));
              ("eof_initcodes_hashed",
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "std::collections::hash::map::HashMap")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                          [ Value.Integer IntegerKind.Usize 32 ]
                          [];
                        Ty.path "alloy_primitives::bytes_::Bytes";
                        Ty.path "std::hash::random::RandomState"
                      ],
                    "new",
                    []
                  |),
                  []
                |))
            ]))
      | _, _, _ => 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_TxEnv.
  
  (* StructRecord
    {
      name := "BlobExcessGasAndPrice";
      const_params := [];
      ty_params := [];
      fields := [ ("excess_blob_gas", Ty.path "u64"); ("blob_gasprice", Ty.path "u128") ];
    } *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_env_BlobExcessGasAndPrice.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlobExcessGasAndPrice".
    
    (* 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::BlobExcessGasAndPrice"
            [
              ("excess_blob_gas",
                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::env::BlobExcessGasAndPrice",
                      "excess_blob_gas"
                    |)
                  ]
                |));
              ("blob_gasprice",
                M.call_closure (|
                  M.get_trait_method (| "core::clone::Clone", Ty.path "u128", [], "clone", [] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::BlobExcessGasAndPrice",
                      "blob_gasprice"
                    |)
                  ]
                |))
            ]))
      | _, _, _ => 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_BlobExcessGasAndPrice.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_env_BlobExcessGasAndPrice.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlobExcessGasAndPrice".
    
    (* 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 "BlobExcessGasAndPrice" |);
              M.read (| Value.String "excess_blob_gas" |);
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_primitives::env::BlobExcessGasAndPrice",
                "excess_blob_gas"
              |);
              M.read (| Value.String "blob_gasprice" |);
              M.alloc (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::BlobExcessGasAndPrice",
                  "blob_gasprice"
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_BlobExcessGasAndPrice.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_BlobExcessGasAndPrice.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlobExcessGasAndPrice".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_BlobExcessGasAndPrice.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_env_BlobExcessGasAndPrice.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlobExcessGasAndPrice".
    
    (* 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 (|
            BinOp.eq (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_primitives::env::BlobExcessGasAndPrice",
                  "excess_blob_gas"
                |)
              |),
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "revm_primitives::env::BlobExcessGasAndPrice",
                  "excess_blob_gas"
                |)
              |)
            |),
            ltac:(M.monadic
              (BinOp.eq (|
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::BlobExcessGasAndPrice",
                    "blob_gasprice"
                  |)
                |),
                M.read (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_primitives::env::BlobExcessGasAndPrice",
                    "blob_gasprice"
                  |)
                |)
              |)))
          |)))
      | _, _, _ => 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_BlobExcessGasAndPrice.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_env_BlobExcessGasAndPrice.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlobExcessGasAndPrice".
    
    (* 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_BlobExcessGasAndPrice.
  
  Module Impl_core_hash_Hash_for_revm_primitives_env_BlobExcessGasAndPrice.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlobExcessGasAndPrice".
    
    (* 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.path "u64", [], "hash", [ __H ] |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "revm_primitives::env::BlobExcessGasAndPrice",
                      "excess_blob_gas"
                    |);
                    M.read (| state |)
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "u128", [], "hash", [ __H ] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_primitives::env::BlobExcessGasAndPrice",
                    "blob_gasprice"
                  |);
                  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_BlobExcessGasAndPrice.
  
  Module Impl_revm_primitives_env_BlobExcessGasAndPrice.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::BlobExcessGasAndPrice".
    
    (*
        pub fn new(excess_blob_gas: u64) -> Self {
            let blob_gasprice = calc_blob_gasprice(excess_blob_gas);
            Self {
                excess_blob_gas,
                blob_gasprice,
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ excess_blob_gas ] =>
        ltac:(M.monadic
          (let excess_blob_gas := M.alloc (| excess_blob_gas |) in
          M.read (|
            let~ blob_gasprice :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "revm_primitives::utilities::calc_blob_gasprice", [] |),
                  [ M.read (| excess_blob_gas |) ]
                |)
              |) in
            M.alloc (|
              Value.StructRecord
                "revm_primitives::env::BlobExcessGasAndPrice"
                [
                  ("excess_blob_gas", M.read (| excess_blob_gas |));
                  ("blob_gasprice", M.read (| blob_gasprice |))
                ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  End Impl_revm_primitives_env_BlobExcessGasAndPrice.
  
  (*
  Enum TransactTo
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Call";
          item := StructTuple [ Ty.path "alloy_primitives::bits::address::Address" ];
          discriminant := None;
        };
        {
          name := "Create";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_env_TransactTo.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TransactTo".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::env::TransactTo::Call",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::env::TransactTo::Call"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "alloy_primitives::bits::address::Address",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::env::TransactTo::Create" |) in
                    M.alloc (| Value.StructTuple "revm_primitives::env::TransactTo::Create" [] |)))
              ]
            |)
          |)))
      | _, _, _ => 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_TransactTo.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_env_TransactTo.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TransactTo".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::env::TransactTo::Call",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_tuple_field1_finish",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Call" |); __self_0 ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::env::TransactTo::Create" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Create" |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_TransactTo.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_TransactTo.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TransactTo".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_TransactTo.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_env_TransactTo.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TransactTo".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::TransactTo" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::TransactTo" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              LogicalOp.and (|
                BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                ltac:(M.monadic
                  (M.read (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_0,
                                "revm_primitives::env::TransactTo::Call",
                                0
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ0_1,
                                "revm_primitives::env::TransactTo::Call",
                                0
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "alloy_primitives::bits::address::Address" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.path "alloy_primitives::bits::address::Address" ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                      ]
                    |)
                  |)))
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_revm_primitives_env_TransactTo.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_env_TransactTo.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TransactTo".
    
    (* 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_TransactTo.
  
  Module Impl_core_hash_Hash_for_revm_primitives_env_TransactTo.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TransactTo".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::TransactTo" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
                  [ __self_discr; M.read (| state |) ]
                |)
              |) in
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::env::TransactTo::Call",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::hash::Hash",
                          Ty.path "alloy_primitives::bits::address::Address",
                          [],
                          "hash",
                          [ __H ]
                        |),
                        [ M.read (| __self_0 |); M.read (| state |) ]
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_revm_primitives_env_TransactTo.
  
  Module Impl_revm_primitives_env_TransactTo.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::TransactTo".
    
    (*
        pub fn call(address: Address) -> Self {
            Self::Call(address)
        }
    *)
    Definition call (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ address ] =>
        ltac:(M.monadic
          (let address := M.alloc (| address |) in
          Value.StructTuple "revm_primitives::env::TransactTo::Call" [ M.read (| address |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_call : M.IsAssociatedFunction Self "call" call.
    
    (*
        pub fn create() -> Self {
            Self::Create
        }
    *)
    Definition create (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic (Value.StructTuple "revm_primitives::env::TransactTo::Create" []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_create : M.IsAssociatedFunction Self "create" create.
    
    (*
        pub fn is_call(&self) -> bool {
            matches!(self, Self::Call(_))
        }
    *)
    Definition is_call (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::env::TransactTo::Call",
                        0
                      |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_call : M.IsAssociatedFunction Self "is_call" is_call.
    
    (*
        pub fn is_create(&self) -> bool {
            matches!(self, Self::Create)
        }
    *)
    Definition is_create (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::env::TransactTo::Create" |) in
                    M.alloc (| Value.Bool true |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_is_create : M.IsAssociatedFunction Self "is_create" is_create.
  End Impl_revm_primitives_env_TransactTo.
  
  (*
  Enum CreateScheme
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Create";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Create2";
          item :=
            StructRecord
              [
                ("salt",
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [])
              ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_env_CreateScheme.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CreateScheme".
    
    (* 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_CreateScheme.
  
  Module Impl_core_marker_Copy_for_revm_primitives_env_CreateScheme.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CreateScheme".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::Copy"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_Copy_for_revm_primitives_env_CreateScheme.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_env_CreateScheme.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CreateScheme".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::env::CreateScheme::Create" |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Create" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "revm_primitives::env::CreateScheme::Create2",
                        "salt"
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "debug_struct_field1_finish",
                          []
                        |),
                        [
                          M.read (| f |);
                          M.read (| Value.String "Create2" |);
                          M.read (| Value.String "salt" |);
                          __self_0
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Debug"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Debug_for_revm_primitives_env_CreateScheme.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_env_CreateScheme.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CreateScheme".
    
    (* 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_CreateScheme.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_CreateScheme.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CreateScheme".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_CreateScheme.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_env_CreateScheme.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CreateScheme".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::CreateScheme" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::CreateScheme" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (|
              LogicalOp.and (|
                BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |),
                ltac:(M.monadic
                  (M.read (|
                    M.match_operator (|
                      M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                            let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                            let γ0_0 := M.read (| γ0_0 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_record_field (|
                                γ0_0,
                                "revm_primitives::env::CreateScheme::Create2",
                                "salt"
                              |) in
                            let __self_0 := M.alloc (| γ2_0 |) in
                            let γ0_1 := M.read (| γ0_1 |) in
                            let γ2_0 :=
                              M.SubPointer.get_struct_record_field (|
                                γ0_1,
                                "revm_primitives::env::CreateScheme::Create2",
                                "salt"
                              |) in
                            let __arg1_0 := M.alloc (| γ2_0 |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        []
                                    ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ]
                                  ],
                                  "eq",
                                  []
                                |),
                                [ __self_0; __arg1_0 ]
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Bool true |)))
                      ]
                    |)
                  |)))
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_revm_primitives_env_CreateScheme.
  
  Module Impl_core_hash_Hash_for_revm_primitives_env_CreateScheme.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::CreateScheme".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::CreateScheme" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ _ :=
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
                  [ __self_discr; M.read (| state |) ]
                |)
              |) in
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_record_field (|
                        γ,
                        "revm_primitives::env::CreateScheme::Create2",
                        "salt"
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::hash::Hash",
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [],
                          [],
                          "hash",
                          [ __H ]
                        |),
                        [ M.read (| __self_0 |); M.read (| state |) ]
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_revm_primitives_env_CreateScheme.
  
  (*
  Enum AnalysisKind
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Raw";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Analyse";
          item := StructTuple [];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_env_AnalysisKind.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::AnalysisKind".
    
    (* Clone *)
    Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          M.read (|
            M.match_operator (|
              self,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ := M.is_struct_tuple (| γ, "revm_primitives::env::AnalysisKind::Raw" |) in
                    M.alloc (| Value.StructTuple "revm_primitives::env::AnalysisKind::Raw" [] |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (| γ, "revm_primitives::env::AnalysisKind::Analyse" |) in
                    M.alloc (|
                      Value.StructTuple "revm_primitives::env::AnalysisKind::Analyse" []
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_AnalysisKind.
  
  Module Impl_core_default_Default_for_revm_primitives_env_AnalysisKind.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::AnalysisKind".
    
    (* Default *)
    Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [] =>
        ltac:(M.monadic (Value.StructTuple "revm_primitives::env::AnalysisKind::Analyse" []))
      | _, _, _ => 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_AnalysisKind.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_env_AnalysisKind.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::AnalysisKind".
    
    (* Debug *)
    Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; f ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let f := M.alloc (| f |) in
          M.call_closure (|
            M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
            [
              M.read (| f |);
              M.read (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (| γ, "revm_primitives::env::AnalysisKind::Raw" |) in
                        M.alloc (| M.read (| Value.String "Raw" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::env::AnalysisKind::Analyse"
                          |) in
                        M.alloc (| M.read (| Value.String "Analyse" |) |)))
                  ]
                |)
              |)
            ]
          |)))
      | _, _, _ => 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_AnalysisKind.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_env_AnalysisKind.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::AnalysisKind".
    
    (* Eq *)
    Definition assert_receiver_is_total_eq
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ self ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          Value.Tuple []))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::Eq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
  End Impl_core_cmp_Eq_for_revm_primitives_env_AnalysisKind.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_AnalysisKind.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::AnalysisKind".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_env_AnalysisKind.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_env_AnalysisKind.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::AnalysisKind".
    
    (* PartialEq *)
    Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; other ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let other := M.alloc (| other |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::AnalysisKind" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::AnalysisKind" ]
                  |),
                  [ M.read (| other |) ]
                |)
              |) in
            M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::cmp::PartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("eq", InstanceField.Method eq) ].
  End Impl_core_cmp_PartialEq_for_revm_primitives_env_AnalysisKind.
  
  Module Impl_core_hash_Hash_for_revm_primitives_env_AnalysisKind.
    Definition Self : Ty.t := Ty.path "revm_primitives::env::AnalysisKind".
    
    (* Hash *)
    Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ __H ], [ self; state ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let state := M.alloc (| state |) in
          M.read (|
            let~ __self_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::env::AnalysisKind" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::hash::Hash", Ty.path "isize", [], "hash", [ __H ] |),
                [ __self_discr; M.read (| state |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::hash::Hash"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("hash", InstanceField.Method hash) ].
  End Impl_core_hash_Hash_for_revm_primitives_env_AnalysisKind.
End env.
