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

Module precompile.
  Axiom PrecompileResult :
    (Ty.path "revm_primitives::precompile::PrecompileResult") =
      (Ty.apply
        (Ty.path "core::result::Result")
        []
        [
          Ty.tuple [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
          Ty.path "revm_primitives::precompile::PrecompileError"
        ]).
  
  Axiom StandardPrecompileFn :
    (Ty.path "revm_primitives::precompile::StandardPrecompileFn") =
      (Ty.function
        [ Ty.apply (Ty.path "&") [] [ Ty.path "alloy_primitives::bytes_::Bytes" ]; Ty.path "u64" ]
        (Ty.apply
          (Ty.path "core::result::Result")
          []
          [
            Ty.tuple [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
            Ty.path "revm_primitives::precompile::PrecompileError"
          ])).
  
  Axiom EnvPrecompileFn :
    (Ty.path "revm_primitives::precompile::EnvPrecompileFn") =
      (Ty.function
        [
          Ty.apply (Ty.path "&") [] [ Ty.path "alloy_primitives::bytes_::Bytes" ];
          Ty.path "u64";
          Ty.apply (Ty.path "&") [] [ Ty.path "revm_primitives::env::Env" ]
        ]
        (Ty.apply
          (Ty.path "core::result::Result")
          []
          [
            Ty.tuple [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
            Ty.path "revm_primitives::precompile::PrecompileError"
          ])).
  
  (* Trait *)
  (* Empty module 'StatefulPrecompile' *)
  
  (* Trait *)
  (* Empty module 'StatefulPrecompileMut' *)
  
  Axiom StatefulPrecompileArc :
    (Ty.path "revm_primitives::precompile::StatefulPrecompileArc") =
      (Ty.apply
        (Ty.path "alloc::sync::Arc")
        []
        [
          Ty.dyn [ ("revm_primitives::precompile::StatefulPrecompile::Trait", []) ];
          Ty.path "alloc::alloc::Global"
        ]).
  
  Axiom StatefulPrecompileBox :
    (Ty.path "revm_primitives::precompile::StatefulPrecompileBox") =
      (Ty.apply
        (Ty.path "alloc::boxed::Box")
        []
        [
          Ty.dyn [ ("revm_primitives::precompile::StatefulPrecompileMut::Trait", []) ];
          Ty.path "alloc::alloc::Global"
        ]).
  
  (*
  Enum Precompile
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "Standard";
          item :=
            StructTuple
              [
                Ty.function
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "alloy_primitives::bytes_::Bytes" ];
                    Ty.path "u64"
                  ]
                  (Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [
                      Ty.tuple [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
                      Ty.path "revm_primitives::precompile::PrecompileError"
                    ])
              ];
          discriminant := None;
        };
        {
          name := "Env";
          item :=
            StructTuple
              [
                Ty.function
                  [
                    Ty.apply (Ty.path "&") [] [ Ty.path "alloy_primitives::bytes_::Bytes" ];
                    Ty.path "u64";
                    Ty.apply (Ty.path "&") [] [ Ty.path "revm_primitives::env::Env" ]
                  ]
                  (Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [
                      Ty.tuple [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
                      Ty.path "revm_primitives::precompile::PrecompileError"
                    ])
              ];
          discriminant := None;
        };
        {
          name := "Stateful";
          item :=
            StructTuple
              [
                Ty.apply
                  (Ty.path "alloc::sync::Arc")
                  []
                  [
                    Ty.dyn [ ("revm_primitives::precompile::StatefulPrecompile::Trait", []) ];
                    Ty.path "alloc::alloc::Global"
                  ]
              ];
          discriminant := None;
        };
        {
          name := "StatefulMut";
          item :=
            StructTuple
              [
                Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [
                    Ty.dyn [ ("revm_primitives::precompile::StatefulPrecompileMut::Trait", []) ];
                    Ty.path "alloc::alloc::Global"
                  ]
              ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_precompile_Precompile.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::Precompile".
    
    (* 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::precompile::Precompile::Standard",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::Precompile::Standard"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.function
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "alloy_primitives::bytes_::Bytes" ];
                                  Ty.path "u64"
                                ]
                                (Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [
                                    Ty.tuple
                                      [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
                                    Ty.path "revm_primitives::precompile::PrecompileError"
                                  ]),
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::Env",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::Precompile::Env"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.function
                                [
                                  Ty.apply
                                    (Ty.path "&")
                                    []
                                    [ Ty.path "alloy_primitives::bytes_::Bytes" ];
                                  Ty.path "u64";
                                  Ty.apply (Ty.path "&") [] [ Ty.path "revm_primitives::env::Env" ]
                                ]
                                (Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [
                                    Ty.tuple
                                      [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
                                    Ty.path "revm_primitives::precompile::PrecompileError"
                                  ]),
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::Stateful",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::Precompile::Stateful"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.apply
                                (Ty.path "alloc::sync::Arc")
                                []
                                [
                                  Ty.dyn
                                    [ ("revm_primitives::precompile::StatefulPrecompile::Trait", [])
                                    ];
                                  Ty.path "alloc::alloc::Global"
                                ],
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::StatefulMut",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::Precompile::StatefulMut"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.apply
                                (Ty.path "alloc::boxed::Box")
                                []
                                [
                                  Ty.dyn
                                    [
                                      ("revm_primitives::precompile::StatefulPrecompileMut::Trait",
                                        [])
                                    ];
                                  Ty.path "alloc::alloc::Global"
                                ],
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_precompile_Precompile.
  
  Module Impl_core_convert_From_ref__alloy_primitives_bytes__Bytesu64Tocore_result_Result_Tuple_u64_alloy_primitives_bytes__Bytes__revm_primitives_precompile_PrecompileError_for_revm_primitives_precompile_Precompile.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::Precompile".
    
    (*
        fn from(p: StandardPrecompileFn) -> Self {
            Precompile::Standard(p)
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ p ] =>
        ltac:(M.monadic
          (let p := M.alloc (| p |) in
          Value.StructTuple "revm_primitives::precompile::Precompile::Standard" [ M.read (| p |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [
          (* T *)
          Ty.function
            [ Ty.apply (Ty.path "&") [] [ Ty.path "alloy_primitives::bytes_::Bytes" ]; Ty.path "u64"
            ]
            (Ty.apply
              (Ty.path "core::result::Result")
              []
              [
                Ty.tuple [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
                Ty.path "revm_primitives::precompile::PrecompileError"
              ])
        ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_ref__alloy_primitives_bytes__Bytesu64Tocore_result_Result_Tuple_u64_alloy_primitives_bytes__Bytes__revm_primitives_precompile_PrecompileError_for_revm_primitives_precompile_Precompile.
  
  Module Impl_core_convert_From_ref__alloy_primitives_bytes__Bytesu64ref__revm_primitives_env_EnvTocore_result_Result_Tuple_u64_alloy_primitives_bytes__Bytes__revm_primitives_precompile_PrecompileError_for_revm_primitives_precompile_Precompile.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::Precompile".
    
    (*
        fn from(p: EnvPrecompileFn) -> Self {
            Precompile::Env(p)
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ p ] =>
        ltac:(M.monadic
          (let p := M.alloc (| p |) in
          Value.StructTuple "revm_primitives::precompile::Precompile::Env" [ M.read (| p |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [
          (* T *)
          Ty.function
            [
              Ty.apply (Ty.path "&") [] [ Ty.path "alloy_primitives::bytes_::Bytes" ];
              Ty.path "u64";
              Ty.apply (Ty.path "&") [] [ Ty.path "revm_primitives::env::Env" ]
            ]
            (Ty.apply
              (Ty.path "core::result::Result")
              []
              [
                Ty.tuple [ Ty.path "u64"; Ty.path "alloy_primitives::bytes_::Bytes" ];
                Ty.path "revm_primitives::precompile::PrecompileError"
              ])
        ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_ref__alloy_primitives_bytes__Bytesu64ref__revm_primitives_env_EnvTocore_result_Result_Tuple_u64_alloy_primitives_bytes__Bytes__revm_primitives_precompile_PrecompileError_for_revm_primitives_precompile_Precompile.
  
  Module Impl_core_convert_From_alloc_sync_Arc_Dyn_revm_primitives_precompile_StatefulPrecompile_Trait_alloc_alloc_Global_for_revm_primitives_precompile_Precompile.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::Precompile".
    
    (*
        fn from(p: StatefulPrecompileArc) -> Self {
            Precompile::Stateful(p)
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ p ] =>
        ltac:(M.monadic
          (let p := M.alloc (| p |) in
          Value.StructTuple "revm_primitives::precompile::Precompile::Stateful" [ M.read (| p |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [
          (* T *)
          Ty.apply
            (Ty.path "alloc::sync::Arc")
            []
            [
              Ty.dyn [ ("revm_primitives::precompile::StatefulPrecompile::Trait", []) ];
              Ty.path "alloc::alloc::Global"
            ]
        ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_alloc_sync_Arc_Dyn_revm_primitives_precompile_StatefulPrecompile_Trait_alloc_alloc_Global_for_revm_primitives_precompile_Precompile.
  
  Module Impl_core_convert_From_alloc_boxed_Box_Dyn_revm_primitives_precompile_StatefulPrecompileMut_Trait_alloc_alloc_Global_for_revm_primitives_precompile_Precompile.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::Precompile".
    
    (*
        fn from(p: StatefulPrecompileBox) -> Self {
            Precompile::StatefulMut(p)
        }
    *)
    Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ p ] =>
        ltac:(M.monadic
          (let p := M.alloc (| p |) in
          Value.StructTuple
            "revm_primitives::precompile::Precompile::StatefulMut"
            [ M.read (| p |) ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::convert::From"
        Self
        (* Trait polymorphic types *)
        [
          (* T *)
          Ty.apply
            (Ty.path "alloc::boxed::Box")
            []
            [
              Ty.dyn [ ("revm_primitives::precompile::StatefulPrecompileMut::Trait", []) ];
              Ty.path "alloc::alloc::Global"
            ]
        ]
        (* Instance *) [ ("from", InstanceField.Method from) ].
  End Impl_core_convert_From_alloc_boxed_Box_Dyn_revm_primitives_precompile_StatefulPrecompileMut_Trait_alloc_alloc_Global_for_revm_primitives_precompile_Precompile.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_precompile_Precompile.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::Precompile".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            match self {
                Precompile::Standard(_) => f.write_str("Standard"),
                Precompile::Env(_) => f.write_str("Env"),
                Precompile::Stateful(_) => f.write_str("Stateful"),
                Precompile::StatefulMut(_) => f.write_str("StatefulMut"),
            }
        }
    *)
    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::precompile::Precompile::Standard",
                        0
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Standard" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::Env",
                        0
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Env" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::Stateful",
                        0
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Stateful" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::StatefulMut",
                        0
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "StatefulMut" |) ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_precompile_Precompile.
  
  Module Impl_revm_primitives_precompile_Precompile.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::Precompile".
    
    (*
        pub fn new_stateful<P: StatefulPrecompile + 'static>(p: P) -> Self {
            Self::Stateful(Arc::new(p))
        }
    *)
    Definition new_stateful (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ P ], [ p ] =>
        ltac:(M.monadic
          (let p := M.alloc (| p |) in
          Value.StructTuple
            "revm_primitives::precompile::Precompile::Stateful"
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "alloc::sync::Arc") [] [ P; Ty.path "alloc::alloc::Global" ],
                  "new",
                  []
                |),
                [ M.read (| p |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_stateful : M.IsAssociatedFunction Self "new_stateful" new_stateful.
    
    (*
        pub fn new_stateful_mut<P: StatefulPrecompileMut + 'static>(p: P) -> Self {
            Self::StatefulMut(Box::new(p))
        }
    *)
    Definition new_stateful_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ P ], [ p ] =>
        ltac:(M.monadic
          (let p := M.alloc (| p |) in
          Value.StructTuple
            "revm_primitives::precompile::Precompile::StatefulMut"
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "alloc::boxed::Box") [] [ P; Ty.path "alloc::alloc::Global" ],
                  "new",
                  []
                |),
                [ M.read (| p |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new_stateful_mut :
      M.IsAssociatedFunction Self "new_stateful_mut" new_stateful_mut.
    
    (*
        pub fn call(&mut self, bytes: &Bytes, gas_price: u64, env: &Env) -> PrecompileResult {
            match self {
                Precompile::Standard(p) => p(bytes, gas_price),
                Precompile::Env(p) => p(bytes, gas_price, env),
                Precompile::Stateful(p) => p.call(bytes, gas_price, env),
                Precompile::StatefulMut(p) => p.call_mut(bytes, gas_price, env),
            }
        }
    *)
    Definition call (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; bytes; gas_price; env ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let bytes := M.alloc (| bytes |) in
          let gas_price := M.alloc (| gas_price |) in
          let env := M.alloc (| env |) 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::precompile::Precompile::Standard",
                        0
                      |) in
                    let p := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.read (| M.read (| p |) |),
                        [ M.read (| bytes |); M.read (| gas_price |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::Env",
                        0
                      |) in
                    let p := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.read (| M.read (| p |) |),
                        [ M.read (| bytes |); M.read (| gas_price |); M.read (| env |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::Stateful",
                        0
                      |) in
                    let p := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "revm_primitives::precompile::StatefulPrecompile",
                          Ty.dyn [ ("revm_primitives::precompile::StatefulPrecompile::Trait", []) ],
                          [],
                          "call",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.apply
                                (Ty.path "alloc::sync::Arc")
                                []
                                [
                                  Ty.dyn
                                    [ ("revm_primitives::precompile::StatefulPrecompile::Trait", [])
                                    ];
                                  Ty.path "alloc::alloc::Global"
                                ],
                              [],
                              "deref",
                              []
                            |),
                            [ M.read (| p |) ]
                          |);
                          M.read (| bytes |);
                          M.read (| gas_price |);
                          M.read (| env |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::Precompile::StatefulMut",
                        0
                      |) in
                    let p := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "revm_primitives::precompile::StatefulPrecompileMut",
                          Ty.dyn
                            [ ("revm_primitives::precompile::StatefulPrecompileMut::Trait", []) ],
                          [],
                          "call_mut",
                          []
                        |),
                        [
                          M.read (| M.read (| p |) |);
                          M.read (| bytes |);
                          M.read (| gas_price |);
                          M.read (| env |)
                        ]
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_call : M.IsAssociatedFunction Self "call" call.
  End Impl_revm_primitives_precompile_Precompile.
  
  (*
  Enum PrecompileError
  {
    const_params := [];
    ty_params := [];
    variants :=
      [
        {
          name := "OutOfGas";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Blake2WrongLength";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Blake2WrongFinalIndicatorFlag";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "ModexpExpOverflow";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "ModexpBaseOverflow";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "ModexpModOverflow";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Bn128FieldPointNotAMember";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Bn128AffineGFailedToCreate";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Bn128PairLength";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "BlobInvalidInputLength";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "BlobMismatchedVersion";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "BlobVerifyKzgProofFailed";
          item := StructTuple [];
          discriminant := None;
        };
        {
          name := "Other";
          item := StructTuple [ Ty.path "alloc::string::String" ];
          discriminant := None;
        }
      ];
  }
  *)
  
  Module Impl_core_clone_Clone_for_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    (* 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::precompile::PrecompileError::OutOfGas"
                      |) in
                    M.alloc (|
                      Value.StructTuple "revm_primitives::precompile::PrecompileError::OutOfGas" []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Blake2WrongLength"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::Blake2WrongLength"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Blake2WrongFinalIndicatorFlag"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::Blake2WrongFinalIndicatorFlag"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::ModexpExpOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::ModexpExpOverflow"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::ModexpBaseOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::ModexpBaseOverflow"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::ModexpModOverflow"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::ModexpModOverflow"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Bn128FieldPointNotAMember"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::Bn128FieldPointNotAMember"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Bn128AffineGFailedToCreate"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::Bn128AffineGFailedToCreate"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Bn128PairLength"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::Bn128PairLength"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::BlobInvalidInputLength"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::BlobInvalidInputLength"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::BlobMismatchedVersion"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::BlobMismatchedVersion"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::BlobVerifyKzgProofFailed"
                      |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::BlobVerifyKzgProofFailed"
                        []
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Other",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      Value.StructTuple
                        "revm_primitives::precompile::PrecompileError::Other"
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::clone::Clone",
                              Ty.path "alloc::string::String",
                              [],
                              "clone",
                              []
                            |),
                            [ M.read (| __self_0 |) ]
                          |)
                        ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => 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_precompile_PrecompileError.
  
  Module Impl_core_fmt_Debug_for_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    (* 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::precompile::PrecompileError::OutOfGas"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "OutOfGas" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Blake2WrongLength"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Blake2WrongLength" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Blake2WrongFinalIndicatorFlag"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Blake2WrongFinalIndicatorFlag" |)
                        ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::ModexpExpOverflow"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "ModexpExpOverflow" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::ModexpBaseOverflow"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "ModexpBaseOverflow" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::ModexpModOverflow"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "ModexpModOverflow" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Bn128FieldPointNotAMember"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Bn128FieldPointNotAMember" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Bn128AffineGFailedToCreate"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Bn128AffineGFailedToCreate" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Bn128PairLength"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "Bn128PairLength" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::BlobInvalidInputLength"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "BlobInvalidInputLength" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::BlobMismatchedVersion"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "BlobMismatchedVersion" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::BlobVerifyKzgProofFailed"
                      |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.path "core::fmt::Formatter",
                          "write_str",
                          []
                        |),
                        [ M.read (| f |); M.read (| Value.String "BlobVerifyKzgProofFailed" |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.read (| γ |) in
                    let γ1_0 :=
                      M.SubPointer.get_struct_tuple_field (|
                        γ,
                        "revm_primitives::precompile::PrecompileError::Other",
                        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 "Other" |); __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_precompile_PrecompileError.
  
  Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::marker::StructuralPartialEq"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_marker_StructuralPartialEq_for_revm_primitives_precompile_PrecompileError.
  
  Module Impl_core_cmp_PartialEq_for_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    (* 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::precompile::PrecompileError" ]
                  |),
                  [ M.read (| self |) ]
                |)
              |) in
            let~ __arg1_discr :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (|
                    "core::intrinsics::discriminant_value",
                    [ Ty.path "revm_primitives::precompile::PrecompileError" ]
                  |),
                  [ 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::precompile::PrecompileError::Other",
                                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::precompile::PrecompileError::Other",
                                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 "alloc::string::String" ],
                                  [ Ty.apply (Ty.path "&") [] [ Ty.path "alloc::string::String" ] ],
                                  "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_precompile_PrecompileError.
  
  Module Impl_core_cmp_Eq_for_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    (* 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_precompile_PrecompileError.
  
  Module Impl_core_hash_Hash_for_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    (* 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::precompile::PrecompileError" ]
                  |),
                  [ 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::precompile::PrecompileError::Other",
                        0
                      |) in
                    let __self_0 := M.alloc (| γ1_0 |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::hash::Hash",
                          Ty.path "alloc::string::String",
                          [],
                          "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_precompile_PrecompileError.
  
  Module Impl_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    (*
        pub fn other(err: impl Into<String>) -> Self {
            Self::Other(err.into())
        }
    *)
    Definition other (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [ impl_Into_String_ ], [ err ] =>
        ltac:(M.monadic
          (let err := M.alloc (| err |) in
          Value.StructTuple
            "revm_primitives::precompile::PrecompileError::Other"
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::Into",
                  impl_Into_String_,
                  [ Ty.path "alloc::string::String" ],
                  "into",
                  []
                |),
                [ M.read (| err |) ]
              |)
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_other : M.IsAssociatedFunction Self "other" other.
  End Impl_revm_primitives_precompile_PrecompileError.
  
  Module Impl_core_error_Error_for_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    Axiom Implements :
      M.IsTraitInstance
        "core::error::Error"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [].
  End Impl_core_error_Error_for_revm_primitives_precompile_PrecompileError.
  
  Module Impl_core_fmt_Display_for_revm_primitives_precompile_PrecompileError.
    Definition Self : Ty.t := Ty.path "revm_primitives::precompile::PrecompileError".
    
    (*
        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
            let s = match self {
                Self::OutOfGas => "out of gas",
                Self::Blake2WrongLength => "wrong input length for blake2",
                Self::Blake2WrongFinalIndicatorFlag => "wrong final indicator flag for blake2",
                Self::ModexpExpOverflow => "modexp exp overflow",
                Self::ModexpBaseOverflow => "modexp base overflow",
                Self::ModexpModOverflow => "modexp mod overflow",
                Self::Bn128FieldPointNotAMember => "field point not a member of bn128 curve",
                Self::Bn128AffineGFailedToCreate => "failed to create affine g point for bn128 curve",
                Self::Bn128PairLength => "bn128 invalid pair length",
                Self::BlobInvalidInputLength => "invalid blob input length",
                Self::BlobMismatchedVersion => "mismatched blob version",
                Self::BlobVerifyKzgProofFailed => "verifying blob kzg proof failed",
                Self::Other(s) => s,
            };
            f.write_str(s)
        }
    *)
    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~ s :=
              M.copy (|
                M.match_operator (|
                  self,
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::OutOfGas"
                          |) in
                        Value.String "out of gas"));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::Blake2WrongLength"
                          |) in
                        M.alloc (| M.read (| Value.String "wrong input length for blake2" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::Blake2WrongFinalIndicatorFlag"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "wrong final indicator flag for blake2" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::ModexpExpOverflow"
                          |) in
                        M.alloc (| M.read (| Value.String "modexp exp overflow" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::ModexpBaseOverflow"
                          |) in
                        M.alloc (| M.read (| Value.String "modexp base overflow" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::ModexpModOverflow"
                          |) in
                        M.alloc (| M.read (| Value.String "modexp mod overflow" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::Bn128FieldPointNotAMember"
                          |) in
                        M.alloc (|
                          M.read (| Value.String "field point not a member of bn128 curve" |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::Bn128AffineGFailedToCreate"
                          |) in
                        M.alloc (|
                          M.read (|
                            Value.String "failed to create affine g point for bn128 curve"
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::Bn128PairLength"
                          |) in
                        M.alloc (| M.read (| Value.String "bn128 invalid pair length" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::BlobInvalidInputLength"
                          |) in
                        M.alloc (| M.read (| Value.String "invalid blob input length" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::BlobMismatchedVersion"
                          |) in
                        M.alloc (| M.read (| Value.String "mismatched blob version" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let _ :=
                          M.is_struct_tuple (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::BlobVerifyKzgProofFailed"
                          |) in
                        M.alloc (| M.read (| Value.String "verifying blob kzg proof failed" |) |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ := M.read (| γ |) in
                        let γ1_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "revm_primitives::precompile::PrecompileError::Other",
                            0
                          |) in
                        let s := M.alloc (| γ1_0 |) in
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "alloc::string::String",
                              [],
                              "deref",
                              []
                            |),
                            [ M.read (| s |) ]
                          |)
                        |)))
                  ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
                [ M.read (| f |); M.read (| s |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "core::fmt::Display"
        Self
        (* Trait polymorphic types *) []
        (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
  End Impl_core_fmt_Display_for_revm_primitives_precompile_PrecompileError.
End precompile.
